الاختبار الرمزي مع Halmos: الاستفادة من الاختبارات الحالية للتحقق الرسمي

التحقق الرسمي - عملية استخدام الأساليب الرياضية "لفحص" برنامج أو عقد ذكي عبر أي عدد من المدخلات - يُنظر إليه عمومًا على أنه البديل الأكثر إيجازًا وشمولية للاختبار التقليدي لكتابة رمز أعلى جودة وأكثر أمانًا. لكن في الواقع ، يعتبر التحقق الرسمي عملية تفاعلية مفتوحة النهاية. تمامًا مثل اختبار الوحدة ، يجب على المطورين تحديد المواصفات الرسمية ووضع طبقات عليها ديناميكيًا ، والتكرار في نهجهم مع تطور التعليمات البرمجية والتحليلات الخاصة بهم. علاوة على ذلك ، يكون التحقق الرسمي بنفس فعالية مواصفاته ، والتي يمكن أن تستغرق وقتًا طويلاً في الكتابة (وغالبًا ما تأتي مع منحنى تعليمي حاد). 

بالنسبة للعديد من المطورين الذين يجدون العملية شاقة ، غالبًا ما تكون اختبارات الوحدة هي المسار الأكثر فعالية من حيث التكلفة والأكثر فاعلية من حيث الوقت لمعرفة مدى صحة البرنامج. في الممارسة العملية ، لا يعد التحقق الرسمي بديلاً أكثر شمولاً لاختبار الوحدة ، ولكنه بديل مكمل. هذه العمليات لها نقاط قوة وقيود مختلفة ، مما يوفر ضمانًا أكبر عند استخدامها معًا. سيحتاج المطورون دائمًا إلى كتابة اختبارات الوحدة - فماذا لو تمكنا من استخدام نفس الخصائص للتحقق الرسمي؟

هالموس، أداة التحقق الرسمية مفتوحة المصدر الخاصة بنا ، تتيح للمطورين إعادة استخدام نفس الخصائص المكتوبة لاختبارات الوحدة للمواصفات الشكلية من خلال الاختبار الرمزي. بدلاً من الاضطرار إلى إنشاء مجموعة قوية من الخصائص من البداية ، يمكن للمطورين تجنب العمل المكرر وتحسين اختباراتهم ببعض المواصفات في وقت واحد دون البدء من نقطة الصفر. لقد صممنا هذه الأداة للاستخدام ، جنبًا إلى جنب مع الآخرين في عملية التحقق الرسمية ، كنقطة انطلاق نحو التحقق الرسمي ؛ يمكن للمطورين البدء ببعض التحليلات بأقل جهد ، قبل إضافة المزيد لاحقًا في العملية.

في هذا المنشور ، نغطي تحديات التحقق الرسمي ، وإمكانية سد الفجوة بين اختبار الوحدة والتحقق الرسمي باختبار رمزي. ثم نتصفح عرضًا توضيحيًا لـ Halmos باستخدام رمز العقد الذكي الحالي ، ونلقي نظرة سريعة على أدوات التحقق الرسمية الأخرى (العديد من المصادر المفتوحة) المتاحة للمطورين.

التحقق الرسمي مقابل الاختبار

التحقق الرسمي - يفضلها مطورو blockchain بشكل عام لدقتها وشمولها - هي عملية إثبات صحة البرنامج عن طريق التحقق من أنه يفي بخصائص معينة للصحة. عادةً ما يتم توفير الخصائص الخاصة بالبرنامج خارجيًا ويتم التعبير عنها باستخدام لغة أو تدوين رسمي تدعمه أداة التحقق المستخدمة. غالبًا ما ينظر المطورون إلى التحقق الرسمي على أنه حل الضغط على زر لاختبار الخصائص عبر جميع السيناريوهات الممكنة تلقائيًا ، ولكن في الواقع ، يمكن أن يكون التحقق الرسمي عملية كثيفة العمالة وتفاعلية للغاية.

مثل التحقق الرسمي ، يتضمن اختبار الوحدة تقييم ما إذا كان البرنامج يعمل كما هو متوقع ؛ الاختبار ، مع ذلك ، يتحقق فقط من سلوك البرنامج لـ بعض المدخلات ، بينما يمكن التحقق الرسمي من التحقق من ذلك من جميع المدخلات الممكنة. يتطلب كل من الاختبار والتحقق الرسمي وصفًا للسلوك المتوقع للبرنامج (مع حالات الاختبار المستخدمة في الاختبار والمواصفات الرسمية المستخدمة في التحقق الرسمي). ولكن عند استخدامها معًا ، يمكن أن توفر فحصًا أكثر شمولاً للبرنامج. الاختبار ، على سبيل المثال ، فعال في العثور على الأخطاء والأخطاء البسيطة ، ولكنه بشكل عام أسرع وأسهل في الأداء. في حين أن التحقق الرسمي أكثر تعقيدًا في الاستخدام ، إلا أنه قوي بما يكفي لإثبات عدم وجود أخطاء أو الكشف عن الأخطاء الدقيقة التي يسهل تفويتها في الاختبار أو مراجعات الكود.

المواصفات العامة

أحد التحديات الرئيسية للتحقق الرسمي هو النفقات العامة للكتابة والحفاظ على المواصفات الرسمية. غالبًا ما تتضمن هذه العملية مهمة تستغرق وقتًا طويلاً تتمثل في كتابة المواصفات يدويًا باستخدام لغة متخصصة (سيحتاج العديد من المطورين إلى تعلمها أولاً). هذه العملية هي أيضًا تدريجية ، تبدأ عادةً بكتابة الخصائص البسيطة والتحقق منها أولاً ، ثم إضافة المزيد من الخصائص المعقدة تدريجياً في الأعلى. مثل الاختبار ، إنها عملية مفتوحة ، بدون نقطة توقف واضحة ، ويمكن للمرء فقط إضافة أكبر عدد ممكن من الخصائص ضمن الإطار الزمني المتاح. بالإضافة إلى ذلك ، عندما يغير المطورون الكود أثناء التحقق منه ، يجب عليهم أيضًا تحديث مواصفاتهم الحالية ، مما يؤدي إلى جهود صيانة إضافية. يمكن أن تجعل هذه العوامل التحقق الرسمي مهمة شاقة لبعض المطورين الذين يترددون في الالتزام بالمصروفات الزائدة.

وعلى الرغم من أن الاختبار والتحقق الرسمي يمكن أن يحسنا جودة الكود عند استخدامهما معًا ، فإن كلاهما يتطلب (أحيانًا متشابهة) أوصافًا للسلوك المتوقع للبرنامج بلغات وأشكال مختلفة. تتطلب كتابة هذه الأوصاف والحفاظ عليها جهدًا كثيفًا ، وقد يبدو الحفاظ على شكلين مختلفين من نفس الوصف كجهد مكرر. يثير هذا السؤال التالي: هل من الممكن وصف السلوك المتوقع بطريقة يمكن للمطورين استخدامها في كل من الاختبار والتحقق؟

سد الفجوة بين الاختبار والتحقق الرسمي بالاختبار الرمزي و Halmos

يعد الاختبار الرمزي ، وهو ممارسة إجراء الاختبارات بمدخلات رمزية ، طريقة تحقق رسمية فعالة تقلل من النفقات العامة للمواصفات. يتيح هذا النهج استخدام حالات الاختبار نفسها لكل من الاختبار والتحقق الرسمي. على عكس الاختبار التقليدي ، الذي يتحقق من أن البرنامج يعمل بشكل صحيح لمجموعة محدودة من المدخلات ، يتحقق الاختبار الرمزي من البرنامج بحثًا عن جميع المدخلات الممكنة ، وبالتالي يمكن اعتبار البرنامج الذي يجتاز الاختبار الرمزي محققًا رسميًا.

Halmos هي أداة تحقق رسمية مصممة للاختبار الرمزي. بدلاً من طلب مواصفات منفصلة أو تعلم لغة جديدة ، تستخدم Halmos الاختبارات الحالية كمواصفات رسمية. سيؤدي إجراء الاختبارات من خلال Halmos تلقائيًا إلى التحقق من اجتيازها لجميع المدخلات الممكنة ، أو تقديم أمثلة مضادة. هذا لا يلغي الحاجة إلى كتابة مواصفات إضافية فحسب ، بل يسمح أيضًا بإعادة استخدام الاختبارات المكتوبة لاختبار الوحدة أو التشويش ، لأغراض التحقق الرسمي.

وبالتالي ، يتمتع المطورون بقدر أكبر من المرونة للاختيار من بين مجموعة من خيارات ضمان الجودة ، بما في ذلك اختبار الوحدة والتشويش والتحقق الرسمي ، اعتمادًا على احتياجاتهم الحالية. على سبيل المثال ، قد تحدد الاختبارات بسرعة أخطاء بسيطة ، ربما بمساعدة مصهر يولد مدخلات عشوائية ، ومن ثم يمكن أن تزيد Halmos الثقة في صحة البرنامج عبر جميع المدخلات.

مثال: اختبار isPowerOfTwo() وظيفة

كمثال ، ضع في اعتبارك ما يلي isPowerOfTwo() دالة ، تحدد ما إذا كان عدد معين هو أس اثنين. تستخدم هذه الوظيفة ملف خوارزمية معالجة البت من أجل الكفاءة ، ولكن قد يكون من الصعب إثبات صحتها ، لا سيما في الحالة التي لا يكون فيها الإدخال بقوة اثنين.

تخيل الاختبار التالي لـ isPowerOfTwo() دالة: تقارن الناتج الفعلي للوظيفة مع المخرجات المتوقعة لمدخل معين. هذا اختبار معلمات (يُعرف أيضًا باسم الاختبار القائم على الخصائص) ، مما يعني أنه يمكنك تشغيله بسهولة بقيم إدخال مختلفة ، ربما باستخدام أدوات التشويش مثل Foundry.

يمكنك استخدام هذا الاختبار لفحص isPowerOfTwo() تعمل من خلال اختبار الوحدة أو اختبار الزغب ، وتشغيلها مع مجموعة مختارة من المدخلات. لا يمكن لمثل هذه الاختبارات أن تثبت رسميًا صحة الوظيفة ، لأنه من غير المجدي من الناحية الحسابية تشغيل الاختبار لكل مدخلات ممكنة.

ومع ذلك ، تسمح Halmos للمطورين بإعادة استخدام هذه الاختبارات الموجودة مسبقًا للتحقق الرسمي ببذل جهد إضافي ضئيل. تتحقق الأداة من اجتياز الاختبارات لجميع المدخلات الممكنة عن طريق إجراء تنفيذ رمزي للاختبار ثم التحقق من عدم انتهاك التأكيد أبدًا ، (أو ، إذا كان التأكيد is انتهكت، من خلال توفير مثال مضاد). هذا يعني أنه في حالة اجتياز الاختبار لـ Halmos ، يتم التحقق رسميًا من صحة الوظيفة ، مما يعني أن الخوارزمية يتم تنفيذها بشكل صحيح وقد تمت ترجمتها بدقة بواسطة المترجم إلى رمز ثانوي.

القيد: تنفيذ رمزي مقيد

بشكل عام ، ليس من الممكن إجراء اختبار رمزي كامل وتلقائي بالكامل ، لأن هذا قد يتطلب حل وقف المشكلة، وهو معروف غير قابل للتقسيم. أحد أسباب ذلك هو أنه غالبًا ما يكون من المستحيل تحديد عدد المرات التي يجب أن تتكرر فيها الحلقة بشكل رمزي. ونتيجة لذلك ، فإن التحقق الرسمي التلقائي بالكامل غير قابل للتقرير بشكل عام.

بالنظر إلى هذه القيود الأساسية ، تعطي Halmos الأولوية للأتمتة على الاكتمال. لتحقيق هذه الغاية ، تم تصميم Halmos لأداء التفكير الرمزي المحدود للحلقات غير المحدودة (حيث يعتمد عدد التكرارات على مدخلات البرنامج) أو المصفوفات متغيرة الطول (بما في ذلك السلاسل). يؤدي هذا إلى التضحية ببعض الاكتمال ، ولكنه يسمح لشركة Halmos بتجنب مطالبة المستخدم بتقديم تعليقات توضيحية إضافية مثل ثوابت الحلقة.

على سبيل المثال ، ضع في اعتبارك الإصدار التكراري التالي من isPowerOfTwo() وظيفة ، والتي تتميز بحلقة أثناء غير محدودة ، حيث يتم تحديد عدد تكرارات الحلقة بالحد الأدنى من البتات المطلوبة لتمثيل رقم الإدخال.

يكرر Halmos رمزياً هذه الحلقة غير المحدودة فقط إلى حد معين. على سبيل المثال ، إذا تم تعيين الحد على 3 ، فسيقوم Halmos بتكرار الحلقة 3 مرات على الأكثر ولن يأخذ في الاعتبار قيم الإدخال التي قد تتسبب في تكرار الحلقة أكثر من 3 مرات (على سبيل المثال ، أي قيم أكبر من أو تساوي 2 ^ 3 ). في هذه الحالة بالذات ، فإن تعيين الحد على 256 أو أعلى سيسمح بإكمال Halmos.

عرض توضيحي: التحقق الرسمي من ERC721A باستخدام Halmos

لإثبات قدرات Halmos ، استخدمناها لاختبار رمزياً والتحقق منها رسميًا ERC721A، وهو تنفيذ مُحسَّن للغاية للغاز لمعيار ERC721 يسمح بسك الدُفعات بنفس تكلفة سك واحدة تقريبًا. يتضمن ERC721A العديد من الابتكارات تحسينات لتحقيق هذه الكفاءة. على سبيل المثال ، يمكن حفظ الغاز عن طريق تأخير التحديثات لبيانات ملكية الرمز المميز حتى يتم نقل الرمز المميز ، وليس في وقت سك النقود. يتطلب ذلك استخدام هياكل وخوارزميات البيانات المعقدة لاسترداد معلومات الملكية بكفاءة من بنية البيانات البطيئة. وعلى الرغم من أن هذا التحسين يحسن من كفاءة الغاز ، إلا أنه يزيد أيضًا من تعقيد الكود ويجعل إثبات صحة التنفيذ أمرًا صعبًا. هذا يجعل ERC721A مرشحًا جيدًا للتحقق الرسمي ، حيث يمكن أن يزيد الثقة في التنفيذ ويفيد المستخدمين المحتملين.

خصائص الاختبار الرمزي

نظرًا لأن الاختبارات الحالية لـ ERC721A تمت كتابتها بلغة JavaScript باستخدام Hardhat (التي لا تدعمها Halmos حاليًا) ، فقد كتبنا اختبارات جديدة في Solidity لوظائف نقطة الدخول الرئيسية: mint(), burn()و transfer(). تحققت هذه الاختبارات من أن كل وظيفة تقوم بشكل صحيح بتحديث ملكية الرمز المميز والتوازن ، وتؤثر فقط على المستخدمين المعنيين دون تغيير رصيد أو ملكية المستخدمين الآخرين. هذا الأخير ليس بالأمر السهل إثباته بسبب استخدام خوارزمية بنية البيانات الكسولة في ERC721A. على سبيل المثال ، يتحقق الاختبار التالي من أن ملف transfer() تعمل الوظيفة بشكل صحيح على تحديث ملكية الرمز المميز المحدد:

اختبار آخر يتحقق من أن ملف transfer() وظيفة لا تغير التوازن لعناوين أخرى ، والتي من الصعب إثباتها كما ذكرنا سابقًا:

نتائج التحقق

أجرينا تجربة تحقق باستخدام Halmos على العقد الذكي ERC721A بكتابة ما مجموعه اختبار 19. تم إجراء الاختبارات من خلال Halmos مع حلقة متدرجة من 3 ، والتي استغرقت 16 دقيقة لإكمالها. يمكن رؤية تفاصيل وقت التحقق في الجدول أدناه. أجريت التجربة على جهاز MacBook Pro بشريحة M1 Pro وذاكرة 16 جيجابايت.

اختبار	الوقت (الأوقات)
testBurnBalanceUpdate	6.67
testBurnNextTokenIdUnchanged	1.40
testBurnOtherBalance الحماية	5.69
testBurnOtherOwnership الحماية	189.70
testBurnOwnershipUpdate	3.81
testBurnRequirements	71.95
testMintBalanceUpdate	0.20
testMintNextTokenIdUpdate	0.18
testMintOtherBalance حفظ	0.26
testMintOtherOwnership الحماية	5.74
testMintOwnershipUpdate	1.38
testMintRequirements	0.09
testTransferBalance غير متغير	9.03
testTransferBalanceUpdate	53.53
testTransferNextTokenIdUnchanged	4.47
testTransferOtherBalance الحماية	19.57
اختبار نقل ملكية أخرىحفظ	430.61
testTransferOwnershipUdate	18.71
testTransferRequirements	149.18

بينما تم الانتهاء من معظم الاختبارات في غضون ثوانٍ ، استغرق بعضها عدة دقائق. كانت هذه الاختبارات التي تستغرق وقتًا طويلاً صعبة التحقق بسبب الطبيعة المعقدة للحالات التي يجب النظر فيها ، وكانت مرتبطة ارتباطًا وثيقًا بصحة خوارزمية بنية البيانات الكسولة.

بشكل عام ، تشير نتائج هذه التجربة إلى أن Halmos قادرة على التحقق بشكل فعال من صحة رمز العقد الذكي. إنه يوفر ثقة متزايدة في نزاهة الكود ، على الرغم من التعقيد وحالات الحافة المحتملة للعقد الذكي.

جرب البق المحقون

لإثبات فعالية منطق Halmos المحدود ، استخدمناه لاكتشاف الأخطاء في إصدار سابق من عقد ERC721A. واجه هذا الإصدار مشكلة أدت إلى إساءة التعامل مع التدفق الحسابي ومن المحتمل أن يسمح بسك عدد كبير من الرموز المميزة ، مما قد يكسر سلامة بنية البيانات البطيئة ويؤدي إلى فقدان بعض المستخدمين لملكية الرمز المميز (مشكلة حل في الإصدار الحالي). أجرينا نفس المجموعة المكونة من 19 اختبارًا لـ ERC721A على إصدار عربات التي تجرها الدواب ، وتمكنت شركة Halmos من العثور على مثال مضاد لخصائص mint() وظيفة. على وجه التحديد ، قدمت Halmos قيم المدخلات التي أدت إلى سيناريو الاستغلال الموضح أعلاه. تشير نتائج هذه التجربة إلى أنه على الرغم من عدم اكتمالها ، فإن استدلال Halmos المحدود يمكن أن يكون وسيلة فعالة لاكتشاف الأخطاء التي يمكن استغلالها في العقود الذكية ومنعها.

الأعمال ذات الصلة

تم تطوير أدوات التحقق الرسمية للرمز الثانوي للعقد الذكي Ethereum بواسطة فرق مختلفة. يمكن استخدام هذه الأدوات ، بما في ذلك Halmos ، للمساعدة في ضمان أمان وصحة العقود الذكية. يمكن أن تساعد مقارنة وفهم الميزات والقدرات والقيود المختلفة لهذه الأدوات المطورين في اختيار أنسبها لاحتياجاتهم الفريدة.

بينما تعد Halmos إضافة قيمة إلى مجموعة الأدوات المتاحة للتحقق الذكي من العقود ، إلا أنها تهدف إلى استكمال (وليس استبدال) الأدوات الحالية. يمكن للمطورين دمج Halmos مع أدوات أخرى لتحقيق مستوى أعلى من التأكيد في عقودهم. أدناه ، نقارن Halmos مع عدد قليل من الأدوات الرسمية المختارة التي تدعم الرمز الثنائي لـ EVM.

• K هو إطار تحقق رسمي قوي يتيح التحقق الاستنتاجي وإثبات النظرية التفاعلية. توفر نظريتها الأساسية وتنفيذها مستوى عاليًا من التعبيرية ، مما يجعلها مناسبة للتحقق من البرامج والخوارزميات المعقدة. ومع ذلك ، تجدر الإشارة إلى أن K لم يتم تصميمه مع التركيز الشديد على التحقق الآلي ويفتقر إلى بعض ميزات التشغيل الآلي التي قد تتطلب المزيد من الجهد اليدوي أثناء عملية التحقق. لاستخدام إطار عمل K ، تتم كتابة المواصفات الرسمية بلغة K ، والتي يجب تعلمها قبل الاستخدام. قوتها مفيدة بشكل خاص في التحقق من الأنظمة المعقدة ، والتي قد يكون من الصعب تحليلها باستخدام التفكير الآلي.
• Certora هي أداة تحقق رسمية للعقود الذكية التي تركز على التحقق الآلي وتدعم فحص النموذج المقيد ، على غرار Halmos. لاستخدام Certora ، يجب على المطورين تعلم لغتهم الجديدة ، CVL، من أجل كتابة المواصفات. تتيح هذه اللغة وصفًا موجزًا ​​للعديد من الخصائص الهامة من خلال ثوابت العقد ، وهي ميزة لا تدعمها شركة Halmos حاليًا. على الرغم من كونها أداة مملوكة ومغلقة المصدر ، إلا أن Certora توفر أدوات تحقق رسمية قوية ، مع التطوير المستمر والدعم الجيد للمستخدم.
  
  Halmos ، من ناحية أخرى ، هي أداة مفتوحة المصدر أصغر حجمًا وتفتقر حاليًا إلى بعض الميزات التي توفرها Certora ، ولكنها تهدف إلى أن تكون بمثابة منفعة عامة والمقصود منها أن تكون حلاً متخصصًا للتحقق بسرعة من العقود الذكية دون الحاجة إلى عمليات إعداد وصيانة مكثفة.
• هيفم هي أداة تحقق رسمية أخرى تشبه Halmos. كان في السابق جزءًا من DappTools ، وهو مقدمة لـ Foundry. يتمتع كل من HEVM و Halmos بميزة عدم طلب مواصفات منفصلة ويمكنهما تنفيذ الاختبارات الحالية رمزياً لتحديد انتهاكات التأكيد. يتيح ذلك للمستخدمين استخدام كلتا الأداتين بالتبادل أو تشغيلهما بالتوازي لنفس الاختبارات ، مما يوفر لهم خيارات متعددة للاختبار الرمزي.
  
  تجدر الإشارة إلى أنه على الرغم من أوجه التشابه بينهما ، فقد تم تطوير HEVM و Halmos بشكل مستقل ويختلفان في تفاصيل التنفيذ الخاصة بهما ؛ خاصة من حيث التحسينات واستراتيجيات التفكير الرمزي. بالإضافة إلى ذلك ، تمت كتابة HEVM بلغة Haskell ، بينما تمت كتابة Halmos بلغة Python ، مما يوفر التعرض لنظام Python البيئي الغني. إن امتلاك القدرة على استخدام كلتا الأداتين يمنح المستخدمين مزيدًا من المرونة والخيارات لضمان أمان وصحة العقود الذكية.

هالموس مفتوح المصدر ، وهو حاليًا في مرحلته التجريبية. نحن نعمل بنشاط على الجديد ملامح والوظائف ، بما في ذلك رموز الغش الخاصة بـ Foundry والعديد من ميزات قابلية الاستخدام الرئيسية الأخرى. نقدر كثيرًا أفكارك حول الميزات الأكثر أهمية ، ونرحب بأي ملاحظات واقتراحات ومساهمات لجعل Halmos أداة أفضل للجميع.

**

الآراء المعبر عنها هنا هي آراء أفراد AH Capital Management، LLC ("a16z") المقتبس منهم وليست آراء a16z أو الشركات التابعة لها. تم الحصول على بعض المعلومات الواردة هنا من مصادر خارجية ، بما في ذلك من شركات محافظ الصناديق التي تديرها a16z. على الرغم من أنه مأخوذ من مصادر يُعتقد أنها موثوقة ، لم تتحقق a16z بشكل مستقل من هذه المعلومات ولا تقدم أي تعهدات حول الدقة الحالية أو الدائمة للمعلومات أو ملاءمتها لموقف معين. بالإضافة إلى ذلك ، قد يتضمن هذا المحتوى إعلانات جهات خارجية ؛ لم تقم a16z بمراجعة مثل هذه الإعلانات ولا تصادق على أي محتوى إعلاني وارد فيها.

يتم توفير هذا المحتوى لأغراض إعلامية فقط ، ولا ينبغي الاعتماد عليه كمشورة قانونية أو تجارية أو استثمارية أو ضريبية. يجب عليك استشارة مستشاريك بخصوص هذه الأمور. الإشارات إلى أي أوراق مالية أو أصول رقمية هي لأغراض توضيحية فقط ، ولا تشكل توصية استثمارية أو عرضًا لتقديم خدمات استشارية استثمارية. علاوة على ذلك ، هذا المحتوى غير موجه أو مخصص للاستخدام من قبل أي مستثمرين أو مستثمرين محتملين ، ولا يجوز الاعتماد عليه تحت أي ظرف من الظروف عند اتخاذ قرار بالاستثمار في أي صندوق تديره a16z. (سيتم تقديم عرض للاستثمار في صندوق a16z فقط من خلال مذكرة الاكتتاب الخاص واتفاقية الاشتراك والوثائق الأخرى ذات الصلة لأي صندوق من هذا القبيل ويجب قراءتها بالكامل.) أي استثمارات أو شركات محفظة مذكورة ، يشار إليها ، أو الموصوفة لا تمثل جميع الاستثمارات في السيارات التي تديرها a16z ، ولا يمكن أن يكون هناك ضمان بأن الاستثمارات ستكون مربحة أو أن الاستثمارات الأخرى التي تتم في المستقبل سيكون لها خصائص أو نتائج مماثلة. قائمة الاستثمارات التي أجرتها الصناديق التي يديرها Andreessen Horowitz (باستثناء الاستثمارات التي لم يمنحها المُصدر إذنًا لـ a16z للإفصاح علنًا عن الاستثمارات غير المعلنة في الأصول الرقمية المتداولة علنًا) على https://a16z.com/investments /.

الرسوم البيانية والرسوم البيانية المقدمة في الداخل هي لأغراض إعلامية فقط ولا ينبغي الاعتماد عليها عند اتخاذ أي قرار استثماري. الأداء السابق ليس مؤشرا على النتائج المستقبلية. المحتوى يتحدث فقط اعتبارًا من التاريخ المشار إليه. أي توقعات وتقديرات وتنبؤات وأهداف وآفاق و / أو آراء معبر عنها في هذه المواد عرضة للتغيير دون إشعار وقد تختلف أو تتعارض مع الآراء التي يعبر عنها الآخرون. يرجى الاطلاع على https://a16z.com/disclosures للحصول على معلومات إضافية مهمة.