تست نمادین با هالموس: استفاده از تست های موجود برای تایید رسمی

راستی‌آزمایی رسمی – فرآیند استفاده از روش‌های ریاضی برای «بازرسی» یک برنامه یا قرارداد هوشمند در هر تعداد ورودی – معمولاً به‌عنوان جایگزین مختصرتر و جامع‌تر برای آزمایش سنتی برای نوشتن کد با کیفیت بالاتر و ایمن‌تر دیده می‌شود. اما در واقعیت، تأیید رسمی یک فرآیند باز و تعاملی است. درست مانند تست واحد، توسعه‌دهندگان باید به صورت پویا مشخصات رسمی را تعریف کرده و لایه‌بندی کنند و رویه خود را همزمان با تکامل کدها و تحلیل‌ها تکرار کنند. علاوه بر این، تأیید رسمی تنها به اندازه مشخصات آن مؤثر است، که نوشتن آن می تواند زمان بر باشد (و اغلب با یک منحنی یادگیری تند همراه است). 

برای بسیاری از توسعه دهندگان که این فرآیند را دلهره آور می دانند، تست های واحد اغلب راه مقرون به صرفه تر و به صرفه تر برای بررسی صحت یک برنامه هستند. در عمل، تأیید رسمی جایگزین جامع تری برای آزمایش واحد نیست، بلکه یک جایگزین مکمل است. این فرآیندها دارای نقاط قوت و محدودیت های متفاوتی هستند که در صورت استفاده با هم، اطمینان بیشتری را ارائه می دهند. توسعه‌دهندگان همیشه نیاز به نوشتن تست‌های واحد دارند - پس چه می‌شود اگر بتوانیم از همان ویژگی‌ها برای تأیید رسمی استفاده کنیم؟

هالموس، ابزار تأیید رسمی منبع باز ما، به توسعه دهندگان این امکان را می دهد استفاده مجدد همان ویژگی هایی که برای تست های واحد برای مشخصات رسمی از طریق آزمایش نمادین نوشته شده است. توسعه‌دهندگان به‌جای ایجاد مجموعه‌ای قوی از ویژگی‌ها از همان ابتدا، می‌توانند از کارهای تکراری اجتناب کنند و تست‌های خود را در یک زمان، بدون شروع از ابتدا، چند ویژگی را بهبود بخشند. ما این ابزار را برای استفاده، در کنار سایر ابزارها در فرآیند تأیید رسمی، به عنوان یک رمپ به تأیید رسمی طراحی کردیم. توسعه‌دهندگان می‌توانند قبل از افزودن بیشتر در مراحل بعدی، با چند تحلیل با حداقل تلاش شروع کنند.

در این پست، چالش‌های تأیید رسمی، و پتانسیل پر کردن شکاف بین آزمایش واحد و تأیید رسمی با آزمایش نمادین را پوشش می‌دهیم. سپس با استفاده از کد قرارداد هوشمند موجود، نسخه آزمایشی Halmos را مرور می‌کنیم و نگاهی گذرا به سایر ابزارهای تأیید رسمی (بسیاری از منبع باز) در دسترس توسعه‌دهندگان می‌اندازیم.

تأیید رسمی در مقابل آزمایش

تایید رسمی - به طور کلی توسط توسعه دهندگان بلاک چین به دلیل سختگیری و جامعیت آن مورد علاقه است - فرآیند اثبات صحت یک برنامه با تأیید اینکه آیا ویژگی های صحت خاصی را برآورده می کند. ویژگی‌هایی که مختص برنامه هستند، معمولاً به صورت خارجی ارائه می‌شوند و با استفاده از یک زبان یا نماد رسمی که توسط ابزار تأیید مورد استفاده پشتیبانی می‌شود، بیان می‌شوند. توسعه دهندگان اغلب تأیید رسمی را به عنوان یک راه حل فشاری برای آزمایش ویژگی ها در تمام سناریوهای ممکن به طور خودکار درک می کنند، اما در واقعیت، تأیید رسمی می تواند یک فرآیند کار فشرده و بسیار تعاملی باشد.

مانند تأیید رسمی، آزمایش واحد شامل ارزیابی اینکه آیا یک برنامه همانطور که انتظار می رود کار می کند یا خیر. با این حال، آزمایش فقط رفتار برنامه را بررسی می کند برخی از ورودی ها، در حالی که تأیید رسمی می تواند آن را بررسی کند تمام ورودی های ممکن هم آزمایش و هم تأیید رسمی نیاز به شرح رفتار مورد انتظار برنامه (با موارد آزمایشی مورد استفاده در آزمایش و مشخصات رسمی مورد استفاده در تأیید رسمی) دارند. اما، هنگامی که با هم استفاده می شوند، می توانند بررسی کامل تری از یک برنامه ارائه دهند. برای مثال، آزمایش در یافتن باگ‌ها و اشتباهات ساده مؤثر است، اما عموماً سریع‌تر و آسان‌تر انجام می‌شود. تأیید رسمی، اگرچه استفاده از آن دشوارتر است، اما به اندازه کافی قدرتمند است تا عدم وجود خطاها را ثابت کند یا اشکالات ظریفی را آشکار کند که در آزمایش یا بررسی کد به راحتی از دست می‌روند.

سربار مشخصات

یکی از چالش های اصلی تأیید رسمی، سربار نوشتن و حفظ مشخصات رسمی است. این فرآیند اغلب شامل کار وقت گیر نوشتن دستی مشخصات با استفاده از یک زبان تخصصی است (که بسیاری از توسعه دهندگان باید ابتدا آن را بیاموزند). این فرآیند همچنین افزایشی است، معمولاً با نوشتن ویژگی‌های ساده و تأیید آنها ابتدا شروع می‌شود، سپس به تدریج ویژگی‌های پیچیده‌تر را در بالا اضافه می‌کند. مانند آزمایش، این یک فرآیند با پایان باز است، بدون نقطه توقف مشخص، و تنها می‌توان تا آنجا که ممکن است در بازه زمانی موجود، ویژگی‌ها را اضافه کرد. علاوه بر این، زمانی که توسعه‌دهندگان کد را در حین تأیید تغییر می‌دهند، باید مشخصات موجود خود را نیز به‌روزرسانی کنند، که منجر به تلاش‌های اضافی برای تعمیر و نگهداری می‌شود. این عوامل می توانند تأیید رسمی را برای برخی از توسعه دهندگانی که در تعهد به هزینه های اضافی مردد هستند، کاری دلهره آور تبدیل کند.

و اگرچه آزمایش و تأیید رسمی می تواند کیفیت کد را در صورت استفاده با هم بهبود بخشد، هر دو نیاز به توصیف (گاهی مشابه) از رفتار مورد انتظار یک برنامه در زبان ها و فرمت های مختلف دارند. نوشتن و حفظ این توصیفات کار فشرده ای است، و حفظ دو شکل متفاوت از یک توصیف می تواند مانند تلاش تکراری باشد. این سؤال زیر را ایجاد می کند: آیا می توان رفتار مورد انتظار را به گونه ای توصیف کرد که توسعه دهندگان بتوانند هم برای آزمایش و هم برای تأیید استفاده کنند؟

پر کردن شکاف بین آزمایش و تأیید رسمی با آزمایش نمادین و هالموس

تست نمادین، تمرین اجرای تست‌ها با ورودی‌های نمادین، یک روش تأیید رسمی مؤثر است که سربار مشخصات را کاهش می‌دهد. این رویکرد استفاده از موارد آزمایشی یکسان را هم برای آزمایش و هم برای تأیید رسمی امکان پذیر می کند. برخلاف آزمایش سنتی، که تأیید می‌کند که یک برنامه برای مجموعه محدودی از ورودی‌ها درست کار می‌کند، آزمایش نمادین برنامه را برای همه ورودی‌های ممکن بررسی می‌کند، بنابراین برنامه‌ای که آزمایش نمادین را پشت سر می‌گذارد می‌تواند به طور رسمی تأیید شده در نظر گرفته شود.

Halmos یک ابزار تأیید رسمی است که برای آزمایش نمادین طراحی شده است. Halmos به جای نیاز به مشخصات جداگانه یا یادگیری یک زبان جدید، از تست های موجود به عنوان مشخصات رسمی استفاده می کند. اجرای آزمایش‌ها از طریق Halmos به‌طور خودکار تأیید می‌کند که همه ورودی‌های ممکن قبول شده‌اند یا نمونه‌های متقابل ارائه می‌کنند. این نه تنها نیاز به نوشتن مشخصات اضافی را از بین می‌برد، بلکه امکان استفاده مجدد از آزمایش‌های نوشته شده برای آزمایش واحد یا فاز کردن، برای اهداف تأیید رسمی را نیز فراهم می‌کند.

بنابراین، توسعه‌دهندگان انعطاف‌پذیری بیشتری برای انتخاب از میان طیف وسیعی از گزینه‌های تضمین کیفیت، از جمله تست واحد، فازبندی، و تأیید رسمی، بسته به نیازهای فعلی خود دارند. به عنوان مثال، آزمایش‌ها ممکن است به سرعت اشتباهات ساده را شناسایی کنند، احتمالاً با کمک یک فازر که ورودی‌های تصادفی تولید می‌کند، و سپس Halmos می‌تواند اعتماد به صحت برنامه را در همه ورودی‌ها افزایش دهد.

مثال: تست کردن isPowerOfTwo() تابع

به عنوان نمونه موارد زیر را در نظر بگیرید isPowerOfTwo() تابع، که تعیین می کند آیا یک عدد داده شده توان دو است یا خیر. این تابع از a استفاده می کند الگوریتم دستکاری بیت برای کارایی، اما اثبات درستی آن می تواند چالش برانگیز باشد، به ویژه در مواردی که ورودی توان دو نباشد.

تست زیر را برای isPowerOfTwo() تابع: خروجی واقعی تابع را با خروجی مورد انتظار برای یک ورودی معین مقایسه می کند. این یک تست پارامتری است (همچنین به عنوان تست مبتنی بر ویژگی شناخته می شود)، به این معنی که می توانید به راحتی آن را با مقادیر ورودی مختلف، احتمالاً با ابزارهای فازی مانند Foundry اجرا کنید.

می توانید از این تست برای بررسی آن استفاده کنید isPowerOfTwo() عملکرد را از طریق تست واحد یا تست فازی انجام دهید و آن را با انتخابی از ورودی ها اجرا کنید. تست‌هایی مانند این نمی‌توانند صحت تابع را به طور رسمی ثابت کنند، زیرا از نظر محاسباتی انجام تست برای هر ورودی ممکن غیرممکن است.

با این حال، هالموس به توسعه دهندگان این امکان را می دهد تا تنها با کمی تلاش بیشتر، از این آزمایشات از قبل برای تأیید رسمی استفاده کنند. این ابزار با اجرای نمادین آزمون و سپس تأیید اینکه ادعا هرگز نقض نشده است، بررسی می‌کند که آزمون‌ها برای همه ورودی‌های ممکن تأیید می‌شوند، (یا اگر ادعا is نقض، با ارائه یک مثال متقابل). این بدان معنی است که اگر آزمون Halmos را پشت سر بگذارد، صحت تابع به طور رسمی تأیید می شود، به این معنی که الگوریتم به درستی پیاده سازی شده و توسط کامپایلر به طور دقیق به کد بایت ترجمه شده است.

محدودیت: اجرای نمادین محدود

معمولاً انجام آزمایش نمادین کاملاً خودکار و کامل امکان پذیر نیست، زیرا این امر مستلزم حل آن است مشکل متوقف کردن، که معروف است غیر قابل تصمیم گیری. یکی از دلایل این امر این است که اغلب غیرممکن است که به طور خودکار تعیین کنیم که یک حلقه باید چند بار به صورت نمادین تکرار شود. در نتیجه، تأیید رسمی کاملاً خودکار به طور کلی غیرقابل تصمیم گیری است.

با توجه به این محدودیت های اساسی، هالموس اتوماسیون را بر کامل بودن اولویت می دهد. برای این منظور، Halmos برای اجرای استدلال نمادین محدود برای حلقه‌های نامحدود (که در آن تعداد تکرارها به ورودی‌های برنامه بستگی دارد) یا آرایه‌های با طول متغیر (از جمله رشته‌ها) طراحی شده است. این یک مقدار کامل را قربانی می کند، اما به Halmos اجازه می دهد تا از الزام کاربر به ارائه حاشیه نویسی های اضافی مانند ثابت های حلقه اجتناب کند.

به عنوان مثال، نسخه تکراری زیر را در نظر بگیرید isPowerOfTwo() تابع، که دارای یک حلقه while نامحدود است، که در آن تعداد تکرارهای حلقه با حداقل تعداد بیت های مورد نیاز برای نمایش عدد ورودی تعیین می شود.

هالموس به صورت نمادین این حلقه نامحدود را فقط تا یک حد مشخص تکرار می کند. به عنوان مثال، اگر کران روی 3 تنظیم شود، هالموس حلقه را حداکثر 3 بار تکرار می کند و مقادیر ورودی را که باعث می شود حلقه بیش از 3 بار تکرار شود (یعنی هر مقدار بزرگتر یا مساوی 2^3) را در نظر نمی گیرد. ). در این مورد خاص، تنظیم کران روی 256 یا بالاتر به Halmos اجازه می دهد تا کامل شود.

نسخه ی نمایشی: تأیید رسمی ERC721A با Halmos

برای نشان دادن قابلیت‌های هالموس، از آن برای آزمایش نمادین و تأیید رسمی استفاده کردیم ERC721A، یک اجرای استاندارد ERC721 بهینه سازی شده برای گاز است که امکان ضربات دسته ای را تقریباً با همان هزینه ضربات تکی فراهم می کند. ERC721A شامل چندین نوآوری است بهینه سازی برای دستیابی به این کارایی؛ به عنوان مثال، گاز را می توان با به تاخیر انداختن به روز رسانی داده های مالکیت توکن تا زمان انتقال توکن، نه در زمان ضرب، ذخیره کرد. این امر مستلزم استفاده از ساختارهای داده پیچیده و الگوریتم‌ها برای بازیابی مؤثر اطلاعات مالکیت از ساختار داده تنبل است. و اگرچه این بهینه‌سازی راندمان گاز را بهبود می‌بخشد، اما پیچیدگی کد را نیز افزایش می‌دهد و اثبات درستی پیاده‌سازی را چالش‌برانگیز می‌کند. این امر ERC721A را به یک کاندیدای خوب برای تأیید رسمی تبدیل می کند، زیرا می تواند اعتماد به نفس را در پیاده سازی افزایش دهد و برای کاربران بالقوه مفید باشد.

ویژگی های آزمایش نمادین

از آنجایی که تست های موجود برای ERC721A در جاوا اسکریپت با هاردات نوشته شده بود (که در حال حاضر توسط Halmos پشتیبانی نمی شود)، ما تست های جدیدی را در Solidity برای توابع نقطه ورودی اصلی نوشتیم: mint(), burn()و transfer(). این آزمایش‌ها بررسی کردند که هر تابع به‌درستی مالکیت و موجودی رمز را به‌روزرسانی می‌کند و فقط بر کاربران مربوطه تأثیر می‌گذارد بدون اینکه تعادل یا مالکیت سایر کاربران را تغییر دهد. اثبات دومی به دلیل استفاده از الگوریتم ساختار داده تنبل در ERC721A غیر ضروری است. برای مثال، آزمایش زیر بررسی می‌کند که transfer() تابع به درستی مالکیت توکن مشخص شده را به روز می کند:

تست دیگری بررسی می کند که transfer() تابع تعادل آدرس‌های دیگر را تغییر نمی‌دهد، همانطور که قبلاً ذکر شد اثبات آن چالش برانگیز است:

نتایج تأیید

ما یک آزمایش تأیید را با استفاده از Halmos در قرارداد هوشمند ERC721A با نوشتن کل انجام دادیم 19،XNUMX تست. آزمایش ها از طریق Halmos با یک حلقه باز کردن کران 3 انجام شد که تکمیل آن 16 دقیقه طول کشید. تفکیک زمان تایید در جدول زیر قابل مشاهده است. این آزمایش بر روی یک مک بوک پرو با تراشه M1 Pro و 16 گیگابایت حافظه انجام شد.

تست	بار)
testBurnBalanceUpdate	6.67
testBurnNextTokenIdUnchanged	1.40
testBurnOtherBalancePreservation	5.69
testBurnOtherOwnershipPreservation	189.70
testBurnOwnership Update	3.81
الزامات testBurn	71.95
testMintBalanceUpdate	0.20
testMintNextTokenIdUpdate	0.18
testMintOtherBalancePreservation	0.26
testMintOtherOwnershipPreservation	5.74
testMintOwnership Update	1.38
الزامات testMint	0.09
testTransferBalance بدون تغییر	9.03
testTransferBalanceUpdate	53.53
testTransferNextTokenIdUnchanged	4.47
testTransferOtherBalancePreservation	19.57
testTransferOtherOwnershipPreservation	430.61
testTransferOwnership Update	18.71
الزامات انتقال تست	149.18

در حالی که بیشتر تست ها در عرض چند ثانیه کامل شدند، چند تا از آنها چند دقیقه طول کشید. به دلیل ماهیت پیچیده مواردی که باید در نظر گرفته شوند، تأیید این آزمایش‌های زمان‌بر چالش برانگیز بود و ارتباط نزدیکی با درستی الگوریتم ساختار داده تنبل داشت.

به طور کلی، نتایج این آزمایش نشان می‌دهد که هالموس قادر است صحت کد قرارداد هوشمند را به طور مؤثر تأیید کند. علیرغم پیچیدگی و موارد لبه احتمالی قرارداد هوشمند، اطمینان بیشتری نسبت به یکپارچگی کد ایجاد می کند.

باگ های تزریق شده را آزمایش کنید

برای نشان دادن اثربخشی استدلال محدود Halmos، ما از آن برای شناسایی اشکالات در نسخه قبلی قرارداد ERC721A استفاده کردیم. این نسخه مشکلی داشت که سرریز حسابی را نادرست مدیریت کرد و به طور بالقوه امکان جمع آوری تعداد زیادی توکن را فراهم کرد، که می تواند یکپارچگی ساختار داده تنبل را شکسته و منجر به از دست دادن مالکیت توکن برخی از کاربران شود (یک مشکل مصمم در نسخه فعلی). ما همان مجموعه 19 تستی را برای ERC721A در نسخه باگ انجام دادیم و هالموس توانست یک مثال متقابل برای ویژگی های mint() تابع. به طور خاص، هالموس مقادیر ورودی را ارائه کرد که منجر به سناریوی اکسپلویت توصیف شده در بالا شد. نتایج این آزمایش نشان می‌دهد که علیرغم ناقص بودن، استدلال محدود هالموس می‌تواند راهی موثر برای شناسایی و جلوگیری از اشکالات قابل بهره‌برداری در قراردادهای هوشمند باشد.

کار مرتبط

ابزارهای تأیید رسمی برای بایت کد قرارداد هوشمند اتریوم توسط تیم های مختلف توسعه داده شده است. از این ابزارها، از جمله Halmos، می توان برای اطمینان از امنیت و صحت قراردادهای هوشمند استفاده کرد. مقایسه و درک ویژگی‌ها، قابلیت‌ها و محدودیت‌های مختلف این ابزارها می‌تواند به توسعه‌دهندگان کمک کند تا مناسب‌ترین ابزار را برای نیازهای منحصر به فرد خود انتخاب کنند.

در حالی که Halmos یک افزودنی ارزشمند به مجموعه ابزار موجود برای تأیید قراردادهای هوشمند است، اما به منظور تکمیل (نه جایگزین) ابزارهای موجود است. توسعه دهندگان می توانند Halmos را با ابزارهای دیگر ترکیب کنند تا به سطح بالاتری از اطمینان در قراردادهای خود دست یابند. در زیر، ما Halmos را با چند ابزار رسمی انتخاب شده که از بایت کد EVM پشتیبانی می کنند، مقایسه می کنیم.

• K یک چارچوب تأیید رسمی قدرتمند است که تأیید قیاسی و اثبات قضیه تعاملی را امکان پذیر می کند. تئوری زیربنایی و اجرای آن سطح بالایی از بیان را ارائه می دهد و آن را برای تأیید برنامه ها و الگوریتم های پیچیده مناسب می کند. با این حال، باید توجه داشت که K با تاکید زیاد بر تأیید خودکار طراحی نشده است و فاقد ویژگی‌های اتوماسیون خاصی است که می‌تواند به تلاش دستی بیشتری در طول فرآیند تأیید نیاز داشته باشد. برای استفاده از فریم ورک K، مشخصات رسمی به زبان K نوشته شده است که قبل از استفاده باید یاد بگیرید. قدرت آن به ویژه در تأیید سیستم های پیچیده مفید است، که ممکن است تجزیه و تحلیل با استفاده از استدلال خودکار چالش برانگیز باشد.
• سرتورا یک ابزار تأیید رسمی برای قراردادهای هوشمند است که بر تأیید خودکار تمرکز دارد و از بررسی مدل محدود، مشابه Halmos پشتیبانی می‌کند. برای استفاده از Certora، توسعه دهندگان باید زبان جدید خود را یاد بگیرند، CVL، به منظور نوشتن مشخصات. این زبان امکان توصیف مختصر بسیاری از ویژگی‌های حیاتی را از طریق متغیرهای قراردادی فراهم می‌کند، ویژگی که Halmos در حال حاضر از آن پشتیبانی نمی‌کند. با وجود اینکه Certora یک ابزار اختصاصی و منبع بسته است، ابزار تأیید رسمی قوی، با توسعه مداوم و پشتیبانی کاربر خوب را ارائه می دهد.
  
  از سوی دیگر، هالموس یک ابزار منبع باز است که در مقیاس کوچکتر است و در حال حاضر فاقد برخی از ویژگی های ارائه شده توسط Certora است، اما قرار است به عنوان یک کالای عمومی خدمت کند و به عنوان یک راه حل تخصصی برای تأیید سریع قراردادهای هوشمند بدون استفاده از نیاز به راه اندازی و نگهداری گسترده
• HEVM یکی دیگر از ابزارهای تأیید رسمی است که شبیه Halmos است. قبلاً بخشی از DappTools بود که پیشروی Foundry است. هر دو HEVM و Halmos دارای ویژگی عدم نیاز به مشخصات جداگانه هستند و می توانند به طور نمادین آزمایش های موجود را برای شناسایی تخلفات ادعایی اجرا کنند. این به کاربران اجازه می دهد تا از هر دو ابزار به جای یکدیگر استفاده کنند یا آنها را به صورت موازی برای آزمایش های یکسان اجرا کنند و چندین گزینه برای آزمایش نمادین در اختیار آنها قرار دهد.
  
  شایان ذکر است که علیرغم شباهت‌هایشان، HEVM و Halmos به طور مستقل توسعه یافته‌اند و در جزئیات پیاده‌سازی متفاوت هستند. به ویژه از نظر بهینه سازی ها و استراتژی های استدلال نمادین. علاوه بر این، HEVM به زبان Haskell نوشته شده است، در حالی که Halmos به زبان Python نوشته شده است و قرار گرفتن در معرض اکوسیستم غنی پایتون را فراهم می کند. داشتن قابلیت استفاده از هر دو ابزار به کاربران انعطاف پذیری و گزینه های بیشتری برای اطمینان از امنیت و صحت قراردادهای هوشمند می دهد.

هالموس منبع باز است و در حال حاضر در مرحله بتا است. ما فعالانه در حال کار بر روی موارد جدید هستیم امکانات و عملکرد، از جمله کدهای تقلب Foundry و چندین ویژگی کاربردی کلیدی دیگر. ما از نظرات شما در مورد اینکه کدام ویژگی مهمتر است بسیار قدردانی می کنیم و از هرگونه بازخورد، پیشنهاد و مشارکت برای تبدیل Halmos به ابزاری بهتر برای همه استقبال می کنیم.

**

نظرات بیان شده در اینجا نظرات پرسنل AH Capital Management, LLC ("a16z") نقل شده است و نظرات a16z یا شرکت های وابسته به آن نیست. برخی از اطلاعات موجود در اینجا از منابع شخص ثالث، از جمله از شرکت‌های سبد سرمایه‌ای که توسط a16z مدیریت می‌شوند، به‌دست آمده است. در حالی که a16z از منابعی گرفته شده است که قابل اعتماد هستند، اما a16z به طور مستقل چنین اطلاعاتی را تأیید نکرده است و هیچ گونه نمایشی در مورد صحت فعلی یا پایدار اطلاعات یا مناسب بودن آن برای یک موقعیت خاص ارائه نمی کند. علاوه بر این، این محتوا ممکن است شامل تبلیغات شخص ثالث باشد. aXNUMXz چنین تبلیغاتی را بررسی نکرده و محتوای تبلیغاتی موجود در آن را تایید نمی کند.

این محتوا فقط برای مقاصد اطلاعاتی ارائه شده است و نباید به عنوان مشاوره حقوقی، تجاری، سرمایه گذاری یا مالیاتی به آن اعتماد کرد. شما باید در مورد این موارد با مشاوران خود مشورت کنید. ارجاع به هر گونه اوراق بهادار یا دارایی دیجیتال فقط برای مقاصد توضیحی است و به منزله توصیه یا پیشنهاد سرمایه گذاری برای ارائه خدمات مشاوره سرمایه گذاری نیست. علاوه بر این، این محتوا برای هیچ سرمایه‌گذار یا سرمایه‌گذار بالقوه‌ای هدایت نشده و برای استفاده از آن در نظر گرفته نشده است، و تحت هیچ شرایطی نمی‌توان هنگام تصمیم‌گیری برای سرمایه‌گذاری در هر صندوقی که توسط a16z مدیریت می‌شود، به آن اعتماد کرد. (پیشنهاد سرمایه گذاری در یک صندوق a16z فقط توسط یادداشت قرار دادن خصوصی، قرارداد اشتراک و سایر اسناد مربوط به هر صندوق انجام می شود و باید به طور کامل خوانده شود.) هر گونه سرمایه گذاری یا شرکت پرتفوی ذکر شده، ارجاع شده، یا شرح داده شده نشان دهنده همه سرمایه گذاری ها در وسایل نقلیه تحت مدیریت a16z نیست، و نمی توان اطمینان داشت که سرمایه گذاری ها سودآور هستند یا سایر سرمایه گذاری های انجام شده در آینده ویژگی ها یا نتایج مشابهی خواهند داشت. فهرستی از سرمایه‌گذاری‌های انجام‌شده توسط صندوق‌های تحت مدیریت آندریسن هوروویتز (به استثنای سرمایه‌گذاری‌هایی که ناشر مجوز افشای عمومی a16z و همچنین سرمایه‌گذاری‌های اعلام‌نشده در دارایی‌های دیجیتالی عمومی را ارائه نکرده است) در https://a16z.com/investments موجود است. /.

نمودارها و نمودارهای ارائه شده در داخل صرفاً برای مقاصد اطلاعاتی هستند و هنگام تصمیم گیری برای سرمایه گذاری نباید به آنها اعتماد کرد. عملکرد گذشته نشان دهنده نتایج آینده نیست. محتوا فقط از تاریخ مشخص شده صحبت می کند. هر گونه پیش بینی، تخمین، پیش بینی، هدف، چشم انداز، و/یا نظرات بیان شده در این مطالب بدون اطلاع قبلی ممکن است تغییر کند و ممکن است متفاوت یا مغایر با نظرات بیان شده توسط دیگران باشد. لطفاً برای اطلاعات مهم بیشتر به https://a16z.com/disclosures مراجعه کنید.