Thử nghiệm tượng trưng với Halmos: Tận dụng các thử nghiệm hiện có để xác minh chính thức

Xác minh chính thức — quá trình sử dụng các phương pháp toán học để “kiểm tra” một chương trình hoặc hợp đồng thông minh trên bất kỳ số lượng đầu vào nào — thường được coi là giải pháp thay thế ngắn gọn hơn, toàn diện hơn so với thử nghiệm truyền thống để viết mã chất lượng cao hơn, an toàn hơn. Nhưng trên thực tế, xác minh chính thức là một quá trình tương tác và không giới hạn. Giống như thử nghiệm đơn vị, các nhà phát triển phải tự động xác định và xếp lớp trên các thông số kỹ thuật chính thức, lặp lại cách tiếp cận của họ khi mã và phân tích của họ phát triển. Hơn nữa, xác minh chính thức chỉ có hiệu quả như thông số kỹ thuật của nó, điều này có thể tốn thời gian để viết (và thường đi kèm với đường cong học tập dốc). 

Đối với nhiều nhà phát triển thấy quá trình này khó khăn, các bài kiểm tra đơn vị thường là con đường hiệu quả hơn về chi phí và thời gian để xác định tính chính xác của chương trình. Trong thực tế, xác minh chính thức không phải là một thay thế toàn diện hơn cho thử nghiệm đơn vị, mà là một bổ sung. Các quy trình này có những điểm mạnh và hạn chế khác nhau, mang lại sự đảm bảo thậm chí còn lớn hơn khi được sử dụng cùng nhau. Các nhà phát triển sẽ luôn cần viết các bài kiểm tra đơn vị — vậy nếu chúng ta có thể sử dụng các thuộc tính tương tự để xác minh chính thức thì sao?

Halmos, công cụ xác minh chính thức mã nguồn mở của chúng tôi, cho phép các nhà phát triển tái sử dụng các thuộc tính tương tự được viết cho các bài kiểm tra đơn vị cho các thông số kỹ thuật chính thức thông qua thử nghiệm tượng trưng. Thay vì phải tạo một tập hợp các thuộc tính mạnh mẽ ngay từ đầu, các nhà phát triển có thể tránh công việc trùng lặp và cải thiện các thử nghiệm của họ một vài thông số kỹ thuật tại một thời điểm mà không cần bắt đầu lại từ đầu. Chúng tôi đã thiết kế công cụ này để sử dụng, cùng với các công cụ khác trong quy trình xác minh chính thức, như một bước chuyển tiếp sang xác minh chính thức; các nhà phát triển có thể bắt đầu với một vài phân tích với nỗ lực tối thiểu, trước khi bổ sung thêm sau này trong quy trình.

Trong bài đăng này, chúng tôi đề cập đến những thách thức của xác minh chính thức và khả năng thu hẹp khoảng cách giữa thử nghiệm đơn vị và xác minh chính thức bằng thử nghiệm tượng trưng. Sau đó, chúng tôi xem qua bản demo của Halmos bằng cách sử dụng mã hợp đồng thông minh hiện có và xem nhanh các công cụ xác minh chính thức khác (nhiều nguồn mở) có sẵn cho nhà phát triển.

Xác minh chính thức so với thử nghiệm

xác minh chính thức — thường được các nhà phát triển blockchain ưa chuộng vì tính chặt chẽ và toàn diện của nó — là quá trình chứng minh tính đúng đắn của một chương trình bằng cách xác minh rằng nó đáp ứng các thuộc tính đúng đắn nhất định. Các thuộc tính, dành riêng cho chương trình, thường được cung cấp bên ngoài và được thể hiện bằng ngôn ngữ hoặc ký hiệu chính thức được hỗ trợ bởi công cụ xác minh đang được sử dụng. Các nhà phát triển thường coi xác minh chính thức là một giải pháp bấm nút để tự động kiểm tra các thuộc tính trong tất cả các tình huống có thể xảy ra, nhưng trên thực tế, xác minh chính thức có thể là một quy trình tốn nhiều công sức và có tính tương tác cao.

Giống như xác minh chính thức, kiểm thử đơn vị liên quan đến việc đánh giá xem chương trình có hoạt động như mong đợi hay không; Tuy nhiên, thử nghiệm chỉ kiểm tra hành vi của chương trình đối với một số đầu vào, trong khi xác minh chính thức có thể kiểm tra nó tất cả các đầu vào có thể. Cả thử nghiệm và xác minh chính thức đều yêu cầu mô tả hành vi dự kiến ​​của chương trình (với các trường hợp thử nghiệm được sử dụng trong thử nghiệm và các đặc tả chính thức được sử dụng trong xác minh chính thức). Tuy nhiên, khi được sử dụng cùng nhau, chúng có thể cung cấp khả năng kiểm tra chương trình kỹ lưỡng hơn. Ví dụ, thử nghiệm có hiệu quả trong việc tìm ra các lỗi và lỗi đơn giản, nhưng nhìn chung sẽ nhanh hơn và dễ thực hiện hơn. Xác minh chính thức, mặc dù cồng kềnh hơn để sử dụng, nhưng đủ mạnh để chứng minh không có lỗi hoặc phát hiện ra các lỗi tinh vi dễ bỏ sót trong quá trình kiểm tra hoặc đánh giá mã.

chi phí kỹ thuật

Một trong những thách thức chính của xác minh chính thức là chi phí viết và duy trì các thông số kỹ thuật chính thức. Quá trình này thường liên quan đến nhiệm vụ tốn thời gian là viết thủ công các thông số kỹ thuật bằng ngôn ngữ chuyên biệt (mà nhiều nhà phát triển sẽ cần học trước). Quá trình này cũng tăng dần, thường bắt đầu bằng việc viết các thuộc tính đơn giản và xác minh chúng trước, sau đó dần dần thêm các thuộc tính phức tạp hơn lên trên. Giống như thử nghiệm, đây là một quy trình không giới hạn, không có điểm dừng rõ ràng và người ta chỉ có thể thêm nhiều thuộc tính nhất có thể trong khung thời gian có sẵn. Ngoài ra, khi các nhà phát triển thay đổi mã khi nó đang được xác minh, họ cũng phải cập nhật các thông số kỹ thuật hiện có của mình, dẫn đến nỗ lực bảo trì thêm. Những yếu tố này có thể làm cho việc xác minh chính thức trở thành một nhiệm vụ khó khăn đối với một số nhà phát triển do dự cam kết chi phí bổ sung.

Và mặc dù thử nghiệm và xác minh chính thức có thể cải thiện chất lượng mã khi được sử dụng cùng nhau, cả hai đều yêu cầu mô tả (đôi khi tương tự) về hành vi dự kiến ​​của chương trình bằng các ngôn ngữ và định dạng khác nhau. Việc viết và duy trì các mô tả này tốn nhiều công sức và việc duy trì hai dạng khác nhau của cùng một mô tả có thể giống như nỗ lực trùng lặp. Điều này đặt ra câu hỏi sau: Có thể mô tả hành vi dự kiến ​​theo cách mà các nhà phát triển có thể sử dụng cho cả thử nghiệm và xác minh không?

Thu hẹp khoảng cách giữa thử nghiệm và xác minh chính thức bằng thử nghiệm tượng trưng và Halmos

Thử nghiệm tượng trưng, ​​thực hành chạy thử nghiệm với đầu vào tượng trưng, ​​là một phương pháp xác minh chính thức hiệu quả giúp giảm chi phí đặc tả. Cách tiếp cận này cho phép sử dụng các trường hợp thử nghiệm giống nhau cho cả thử nghiệm và xác minh chính thức. Không giống như thử nghiệm truyền thống, xác minh rằng chương trình hoạt động chính xác đối với một bộ đầu vào giới hạn, thử nghiệm tượng trưng kiểm tra chương trình cho tất cả các đầu vào có thể, do đó, một chương trình vượt qua thử nghiệm tượng trưng có thể được coi là đã được xác minh chính thức.

Halmos là một công cụ xác minh chính thức được thiết kế để thử nghiệm tượng trưng. Thay vì yêu cầu các thông số kỹ thuật riêng biệt hoặc học một ngôn ngữ mới, Halmos sử dụng các bài kiểm tra hiện có làm thông số kỹ thuật chính thức. Việc chạy thử nghiệm thông qua Halmos sẽ tự động xác minh rằng chúng vượt qua tất cả các đầu vào có thể có hoặc cung cấp các phản ví dụ. Điều này không chỉ loại bỏ nhu cầu viết đặc tả bổ sung mà còn cho phép sử dụng lại các bài kiểm tra được viết để kiểm tra đơn vị hoặc làm mờ, cho các mục đích xác minh chính thức.

Do đó, các nhà phát triển có thể linh hoạt hơn để chọn từ một loạt các tùy chọn đảm bảo chất lượng, bao gồm thử nghiệm đơn vị, làm mờ và xác minh chính thức, tùy thuộc vào nhu cầu hiện tại của họ. Chẳng hạn, các bài kiểm tra có thể nhanh chóng xác định các lỗi đơn giản, có thể với sự trợ giúp của bộ lọc mờ tạo đầu vào ngẫu nhiên, sau đó Halmos có thể tăng thêm độ tin cậy vào tính chính xác của chương trình trên tất cả các đầu vào.

Ví dụ: Thử nghiệm các isPowerOfTwo() chức năng

Như một ví dụ, hãy xem xét những điều sau đây isPowerOfTwo() Hàm xác định xem một số đã cho có phải là lũy thừa của hai hay không. Chức năng này sử dụng một thuật toán thao tác bit về hiệu quả, nhưng có thể khó chứng minh tính đúng đắn của nó, đặc biệt trong trường hợp đầu vào không phải là lũy thừa của hai.

Hãy tưởng tượng thử nghiệm sau đây cho isPowerOfTwo() chức năng: nó so sánh đầu ra thực tế của chức năng với đầu ra dự kiến ​​cho một đầu vào nhất định. Đây là một phép thử được tham số hóa (còn được gọi là phép thử dựa trên thuộc tính), nghĩa là bạn có thể dễ dàng chạy nó với các giá trị đầu vào khác nhau, có thể bằng các công cụ làm mờ như Foundry.

Bạn có thể sử dụng bài kiểm tra này để kiểm tra isPowerOfTwo() chức năng thông qua thử nghiệm đơn vị hoặc thử nghiệm lông tơ, chạy nó với một lựa chọn đầu vào. Các thử nghiệm như thế này không thể chính thức chứng minh tính đúng đắn của hàm, vì không thể chạy thử nghiệm cho mọi đầu vào có thể về mặt tính toán.

Tuy nhiên, Halmos cho phép các nhà phát triển sử dụng lại các thử nghiệm có sẵn này để xác minh chính thức mà chỉ cần thêm một chút nỗ lực. Công cụ kiểm tra xem các bài kiểm tra có vượt qua tất cả các đầu vào có thể hay không bằng cách thực hiện kiểm tra tượng trưng và sau đó xác minh rằng xác nhận không bao giờ bị vi phạm, (hoặc, nếu xác nhận is vi phạm, bằng cách cung cấp một phản ví dụ). Điều này có nghĩa là nếu thử nghiệm vượt qua Halmos, thì tính chính xác của hàm được xác minh chính thức, nghĩa là thuật toán được triển khai chính xác và đã được trình biên dịch dịch chính xác thành mã byte.

Hạn chế: Giới hạn thực thi tượng trưng

Nhìn chung, không thể thực hiện kiểm tra tượng trưng hoàn toàn tự động, vì điều này sẽ yêu cầu giải quyết vấn đề vấn đề tạm dừng, được biết đến là không thể quyết định được. Một lý do cho điều này là thường không thể tự động xác định số lần một vòng lặp sẽ lặp lại một cách tượng trưng. Kết quả là, xác minh chính thức hoàn toàn tự động nói chung là không thể quyết định.

Với những hạn chế cơ bản này, Halmos ưu tiên tự động hóa hơn là hoàn thiện. Cuối cùng, Halmos được thiết kế để thực hiện lý luận tượng trưng có giới hạn cho các vòng lặp không giới hạn (trong đó số lần lặp phụ thuộc vào đầu vào của chương trình) hoặc mảng có độ dài thay đổi (bao gồm cả chuỗi). Điều này hy sinh một số tính đầy đủ, nhưng cho phép Halmos tránh yêu cầu người dùng cung cấp các chú thích bổ sung, chẳng hạn như bất biến vòng lặp.

Ví dụ, xem xét phiên bản lặp lại sau đây của isPowerOfTwo() chức năng, có tính năng vòng lặp while không giới hạn, trong đó số lần lặp lại vòng lặp được xác định bởi số bit tối thiểu cần thiết để biểu thị số đầu vào.

Halmos chỉ lặp lại vòng lặp không giới hạn này một cách tượng trưng cho đến một giới hạn được chỉ định. Chẳng hạn, nếu giới hạn được đặt thành 3, Halmos sẽ lặp lại vòng lặp tối đa 3 lần và sẽ không xem xét các giá trị đầu vào có thể khiến vòng lặp lặp lại hơn 3 lần (nghĩa là bất kỳ giá trị nào lớn hơn hoặc bằng 2^3 ). Trong trường hợp cụ thể này, đặt giới hạn thành 256 hoặc cao hơn sẽ cho phép Halmos hoàn thành.

Demo: Xác minh chính thức ERC721A với Halmos

Để chứng minh khả năng của Halmos, chúng tôi đã sử dụng nó để kiểm tra một cách tượng trưng và xác minh chính thức ERC721A, một triển khai tiêu chuẩn ERC721 được tối ưu hóa về khí đốt, cho phép đúc hàng loạt với chi phí gần như tương đương với đúc đơn lẻ. ERC721A bao gồm một số cải tiến tối ưu hóa để đạt được hiệu quả này; ví dụ: gas có thể được tiết kiệm bằng cách trì hoãn cập nhật dữ liệu quyền sở hữu mã thông báo cho đến khi mã thông báo được chuyển, không phải tại thời điểm đúc. Điều này yêu cầu sử dụng các thuật toán và cấu trúc dữ liệu phức tạp để truy xuất thông tin quyền sở hữu một cách hiệu quả từ cấu trúc dữ liệu lười biếng. Và mặc dù việc tối ưu hóa này cải thiện hiệu quả sử dụng gas, nhưng nó cũng làm tăng độ phức tạp của mã và gây khó khăn cho việc chứng minh tính đúng đắn của việc triển khai. Điều này làm cho ERC721A trở thành ứng cử viên sáng giá để xác minh chính thức, vì nó có thể tăng độ tin cậy trong quá trình triển khai và mang lại lợi ích cho người dùng tiềm năng.

Thuộc tính thử nghiệm tượng trưng

Do các thử nghiệm hiện có cho ERC721A được viết bằng JavaScript với Hardhat (hiện không được Halmos hỗ trợ), nên chúng tôi đã viết các thử nghiệm mới trong Solidity cho các chức năng điểm đầu vào chính: mint(), burn()và transfer(). Các thử nghiệm này đã kiểm tra để đảm bảo rằng mỗi chức năng cập nhật chính xác quyền sở hữu và số dư mã thông báo, đồng thời chỉ ảnh hưởng đến những người dùng có liên quan mà không làm thay đổi số dư hoặc quyền sở hữu của những người dùng khác. Điều thứ hai là không tầm thường để chứng minh do sử dụng thuật toán cấu trúc dữ liệu lười biếng trong ERC721A. Ví dụ: bài kiểm tra sau đây kiểm tra xem transfer() cập nhật chính xác quyền sở hữu của mã thông báo được chỉ định:

Một thử nghiệm khác kiểm tra xem transfer() chức năng không làm thay đổi số dư cho các địa chỉ khác, điều này rất khó chứng minh như đã đề cập trước đó:

kết quả xác minh

Chúng tôi đã tiến hành thử nghiệm xác minh bằng cách sử dụng Halmos trên hợp đồng thông minh ERC721A bằng cách viết tổng số Kiểm tra 19. Các bài kiểm tra được chạy qua Halmos với giới hạn không kiểm soát vòng lặp là 3, mất 16 phút để hoàn thành. Chi tiết về thời gian xác minh có thể được nhìn thấy trong bảng bên dưới. Thử nghiệm được tiến hành trên MacBook Pro với chip M1 Pro và bộ nhớ 16 GB.

Thử nghiệm	Thời gian
testBurnBalanceCập nhật	6.67
testBurnNextTokenIdUnchanged	1.40
kiểm traĐốtKhácCân bằngBảo quản	5.69
kiểm traBurnOtherOwnershipPreservation	189.70
testBurnOwnershipCập nhật	3.81
testBurnYêu cầu	71.95
testMintBalanceCập nhật	0.20
testMintNextTokenIdUpdate	0.18
testMintKhácCân bằngBảo quản	0.26
testMintKhácQuyền sở hữuBảo quản	5.74
testMintOwnershipCập nhật	1.38
testMintYêu cầu	0.09
testTransferBalanceKhông thay đổi	9.03
kiểm traTransferBalanceCập nhật	53.53
testTransferNextTokenIdUnchanged	4.47
kiểm traChuyển khoảnKhácSố dưBảo quản	19.57
kiểm traChuyển nhượngKhácQuyền sở hữuBảo quản	430.61
kiểm traChuyển quyền sở hữuCập nhật	18.71
thử nghiệmChuyển yêu cầu	149.18

Trong khi hầu hết các bài kiểm tra được hoàn thành chỉ trong vài giây, một số bài kiểm tra mất vài phút. Các bài kiểm tra tốn thời gian này rất khó xác minh do tính chất phức tạp của các trường hợp được xem xét và có liên quan chặt chẽ đến tính chính xác của thuật toán cấu trúc dữ liệu lười biếng.

Nhìn chung, kết quả của thử nghiệm này chỉ ra rằng Halmos có thể xác minh hiệu quả tính chính xác của mã hợp đồng thông minh. Nó mang lại sự tự tin ngày càng tăng về tính toàn vẹn của mã, bất chấp sự phức tạp và các trường hợp tiềm ẩn của hợp đồng thông minh.

Thử nghiệm với lỗi tiêm

Để chứng minh tính hiệu quả của lập luận có giới hạn của Halmos, chúng tôi đã sử dụng nó để phát hiện lỗi trong phiên bản trước của hợp đồng ERC721A. Phiên bản này gặp sự cố xử lý sai tràn số học và có khả năng cho phép đúc hàng loạt một số lượng lớn mã thông báo, điều này có thể phá vỡ tính toàn vẹn của cấu trúc dữ liệu lười biếng và khiến một số người dùng mất quyền sở hữu mã thông báo của họ (một sự cố quyết định trong phiên bản hiện tại). Chúng tôi đã chạy cùng một bộ gồm 19 thử nghiệm cho ERC721A trên phiên bản lỗi và Halmos có thể tìm thấy một ví dụ ngược lại cho các thuộc tính của mint() chức năng. Cụ thể, Halmos đã cung cấp các giá trị đầu vào dẫn đến kịch bản khai thác được mô tả ở trên. Kết quả của thí nghiệm này chỉ ra rằng, mặc dù chưa hoàn chỉnh, nhưng lý luận có giới hạn của Halmos có thể là một cách hiệu quả để phát hiện và ngăn chặn các lỗi có thể khai thác trong hợp đồng thông minh.

Công việc có liên quan

Các công cụ xác minh chính thức cho mã byte hợp đồng thông minh Ethereum đã được phát triển bởi nhiều nhóm khác nhau. Những công cụ này, bao gồm cả Halmos, có thể được sử dụng để giúp đảm bảo tính bảo mật và tính chính xác của hợp đồng thông minh. So sánh và hiểu các tính năng, khả năng và hạn chế khác nhau của các công cụ này có thể giúp các nhà phát triển chọn công cụ phù hợp nhất cho nhu cầu riêng của họ.

Mặc dù Halmos là một bổ sung có giá trị cho bộ công cụ có sẵn để xác minh hợp đồng thông minh, nhưng nó nhằm bổ sung (không thay thế) các công cụ hiện có. Các nhà phát triển có thể kết hợp Halmos với các công cụ khác để đạt được mức độ đảm bảo cao hơn trong hợp đồng của họ. Dưới đây, chúng tôi so sánh Halmos với một vài công cụ chính thức đã chọn hỗ trợ mã byte EVM.

• K là một khung xác minh chính thức mạnh mẽ cho phép xác minh suy diễn và chứng minh định lý tương tác. Lý thuyết và triển khai cơ bản của nó mang lại mức độ biểu cảm cao, làm cho nó phù hợp để xác minh các chương trình và thuật toán phức tạp. Tuy nhiên, cần lưu ý rằng K không được thiết kế tập trung nhiều vào xác minh tự động và thiếu một số tính năng tự động nhất định có thể đòi hỏi nhiều nỗ lực thủ công hơn trong quá trình xác minh. Để sử dụng khung K, các thông số kỹ thuật chính thức được viết bằng ngôn ngữ K, ngôn ngữ này phải được học trước khi sử dụng. Sức mạnh của nó đặc biệt hữu ích trong việc xác minh các hệ thống phức tạp, có thể khó phân tích bằng suy luận tự động.
• chứng chỉ là một công cụ xác minh chính thức cho các hợp đồng thông minh tập trung vào xác minh tự động và hỗ trợ kiểm tra mô hình giới hạn, tương tự như Halmos. Để sử dụng Certora, các nhà phát triển phải học ngôn ngữ mới của họ, CVL, để viết thông số kỹ thuật. Ngôn ngữ này cho phép mô tả ngắn gọn nhiều thuộc tính quan trọng thông qua các bất biến hợp đồng, một tính năng mà Halmos hiện không hỗ trợ. Mặc dù là một công cụ độc quyền, nguồn đóng, Certora cung cấp công cụ xác minh chính thức mạnh mẽ, với sự phát triển liên tục và hỗ trợ người dùng tốt.
  
  Mặt khác, Halmos là một công cụ nguồn mở có quy mô nhỏ hơn và hiện thiếu một số tính năng do Certora cung cấp, nhưng nó nhằm phục vụ như một hàng hóa công cộng và được dự định là một giải pháp thích hợp để nhanh chóng xác minh các hợp đồng thông minh mà không cần sự cần thiết phải thiết lập và bảo trì rộng rãi.
• HEVM là một công cụ xác minh chính thức khác tương tự như Halmos. Nó trước đây là một phần của DappTools, tiền thân của Foundry. Cả HEVM và Halmos đều có đặc điểm là không yêu cầu thông số kỹ thuật riêng biệt và có thể thực hiện một cách tượng trưng các thử nghiệm hiện có để xác định các vi phạm xác nhận. Điều này cho phép người dùng sử dụng cả hai công cụ thay thế cho nhau hoặc chạy song song chúng cho cùng các thử nghiệm, cung cấp cho họ nhiều tùy chọn để thử nghiệm tượng trưng.
  
  Cần lưu ý rằng, mặc dù có những điểm tương đồng, HEVM và Halmos đã được phát triển độc lập và khác nhau về chi tiết triển khai; đặc biệt là về tối ưu hóa và chiến lược lý luận tượng trưng. Ngoài ra, HEVM được viết bằng Haskell, trong khi Halmos được viết bằng Python, cung cấp khả năng tiếp xúc với hệ sinh thái Python phong phú. Khả năng sử dụng cả hai công cụ mang đến cho người dùng nhiều tùy chọn và linh hoạt hơn để đảm bảo tính bảo mật và tính chính xác của hợp đồng thông minh.

Halmos là mã nguồn mở và hiện đang trong giai đoạn thử nghiệm. Chúng tôi đang tích cực làm việc trên mới Tính năng, đặc điểm và chức năng, bao gồm mã gian lận Foundry và một số tính năng khả dụng quan trọng khác. Chúng tôi đánh giá rất cao suy nghĩ của bạn về tính năng nào là quan trọng nhất và hoan nghênh mọi phản hồi, đề xuất và đóng góp để biến Halmos thành một công cụ tốt hơn cho mọi người.

**

Các quan điểm được thể hiện ở đây là quan điểm của từng nhân viên AH Capital Management, LLC (“a16z”) được trích dẫn và không phải là quan điểm của a16z hoặc các chi nhánh của nó. Một số thông tin nhất định trong đây đã được lấy từ các nguồn của bên thứ ba, bao gồm từ các công ty danh mục đầu tư của các quỹ do a16z quản lý. Mặc dù được lấy từ các nguồn được cho là đáng tin cậy, a16z đã không xác minh độc lập thông tin đó và không đưa ra tuyên bố về tính chính xác hiện tại hoặc lâu dài của thông tin hoặc sự phù hợp của nó đối với một tình huống nhất định. Ngoài ra, nội dung này có thể bao gồm các quảng cáo của bên thứ ba; a16z đã không xem xét các quảng cáo đó và không xác nhận bất kỳ nội dung quảng cáo nào có trong đó.

Nội dung này chỉ được cung cấp cho mục đích thông tin và không được dựa vào như lời khuyên về pháp lý, kinh doanh, đầu tư hoặc thuế. Bạn nên tham khảo ý kiến ​​của các cố vấn của riêng mình về những vấn đề đó. Các tham chiếu đến bất kỳ chứng khoán hoặc tài sản kỹ thuật số nào chỉ dành cho mục đích minh họa và không cấu thành khuyến nghị đầu tư hoặc đề nghị cung cấp dịch vụ tư vấn đầu tư. Hơn nữa, nội dung này không hướng đến cũng như không nhằm mục đích sử dụng cho bất kỳ nhà đầu tư hoặc nhà đầu tư tiềm năng nào và không được dựa vào bất kỳ trường hợp nào khi đưa ra quyết định đầu tư vào bất kỳ quỹ nào do a16z quản lý. (Đề nghị đầu tư vào quỹ a16z sẽ chỉ được thực hiện bởi bản ghi nhớ phát hành riêng lẻ, thỏa thuận đăng ký và các tài liệu liên quan khác về bất kỳ quỹ nào như vậy và phải được đọc toàn bộ.) Bất kỳ khoản đầu tư hoặc công ty danh mục đầu tư nào được đề cập, đề cập đến, hoặc được mô tả không phải là đại diện cho tất cả các khoản đầu tư vào xe do a16z quản lý và không thể đảm bảo rằng các khoản đầu tư sẽ sinh lời hoặc các khoản đầu tư khác được thực hiện trong tương lai sẽ có các đặc điểm hoặc kết quả tương tự. Danh sách các khoản đầu tư được thực hiện bởi các quỹ do Andreessen Horowitz quản lý (không bao gồm các khoản đầu tư mà tổ chức phát hành không cho phép a16z tiết lộ công khai cũng như các khoản đầu tư không thông báo vào tài sản kỹ thuật số được giao dịch công khai) có tại https://a16z.com/investments /.

Các biểu đồ và đồ thị được cung cấp bên trong chỉ nhằm mục đích cung cấp thông tin và không nên dựa vào khi đưa ra bất kỳ quyết định đầu tư nào. Hiệu suất trong quá khứ không cho thấy kết quả trong tương lai. Nội dung chỉ nói kể từ ngày được chỉ định. Mọi dự đoán, ước tính, dự báo, mục tiêu, triển vọng và / hoặc ý kiến ​​thể hiện trong các tài liệu này có thể thay đổi mà không cần báo trước và có thể khác hoặc trái ngược với ý kiến ​​của người khác. Vui lòng xem https://a16z.com/disclosures để biết thêm thông tin quan trọng.