Halmos ile sembolik testler: Resmi doğrulama için mevcut testlerden yararlanma

Resmi doğrulama - herhangi bir sayıda girdi genelinde bir programı veya akıllı sözleşmeyi "incelemek" için matematiksel yöntemler kullanma süreci - genellikle daha yüksek kaliteli, daha güvenli kod yazmak için geleneksel testlere göre daha özlü, daha kapsamlı bir alternatif olarak görülür. Ancak gerçekte resmi doğrulama, açık uçlu ve etkileşimli bir süreçtir. Birim testi gibi, geliştiricilerin de dinamik olarak tanımlamaları ve resmi spesifikasyonları katmanlandırmaları, kodları ve analizleri geliştikçe yaklaşımlarını yinelemeleri gerekir. Ayrıca, resmi doğrulama yalnızca, yazması zaman alan (ve genellikle dik bir öğrenme eğrisiyle birlikte gelen) belirtimleri kadar etkilidir. 

Süreci göz korkutucu bulan birçok geliştirici için, birim testleri genellikle bir programın doğruluğunu araştırmak için daha uygun maliyetli ve zaman açısından daha verimli bir yoldur. Uygulamada, resmi doğrulama birim testine göre daha kapsamlı bir alternatif değil, tamamlayıcıdır. Bu süreçlerin farklı güçleri ve sınırlamaları vardır ve birlikte kullanıldıklarında daha da fazla güvence sağlarlar. Geliştiricilerin her zaman birim testleri yazması gerekecek - peki ya aynı özellikleri resmi doğrulama için kullanabilseydik?

ağıraçık kaynaklı resmi doğrulama aracımız, geliştiricilerin yeniden Sembolik test yoluyla resmi spesifikasyonlar için birim testleri için yazılan aynı özellikler. Geliştiriciler, en baştan sağlam bir özellikler seti oluşturmak zorunda kalmak yerine, tekrar eden çalışmalardan kaçınabilir ve testlerini sıfırdan başlamadan her seferinde birkaç belirtimi geliştirebilir. Bu aracı, diğerlerinin yanı sıra resmi doğrulama sürecinde kullanılmak üzere, resmi doğrulamaya giden bir rampa olarak tasarladık; geliştiriciler, süreçte daha fazlasını eklemeden önce minimum çabayla birkaç analizle başlayabilir.

Bu yazıda, resmi doğrulamanın zorluklarını ve birim testi ile resmi doğrulama arasındaki boşluğu sembolik testle kapatma potansiyelini ele alıyoruz. Ardından, mevcut akıllı sözleşme kodunu kullanarak bir Halmos demosunu inceliyoruz ve geliştiricilerin kullanımına sunulan diğer resmi doğrulama araçlarına (birçoğu açık kaynak) hızlıca göz atıyoruz.

Resmi doğrulama ve test

Resmi doğrulama - genellikle blok zinciri geliştiricileri tarafından titizliği ve kapsamlılığı nedeniyle tercih edilir - belirli doğruluk özelliklerini karşıladığını doğrulayarak bir programın doğruluğunu kanıtlama sürecidir. Programa özgü özellikler genellikle harici olarak sağlanır ve kullanılan doğrulama aracı tarafından desteklenen resmi bir dil veya notasyon kullanılarak ifade edilir. Geliştiriciler genellikle resmi doğrulamayı, özellikleri tüm olası senaryolarda otomatik olarak test etmek için bir düğme çözümü olarak algılarlar, ancak gerçekte resmi doğrulama emek yoğun ve oldukça etkileşimli bir süreç olabilir.

Resmi doğrulama gibi, birim testi de bir programın beklendiği gibi çalışıp çalışmadığının değerlendirilmesini içerir; test etme, ancak programın davranışını yalnızca biraz girdiler, resmi doğrulama ise bunu kontrol edebilir herşey olası girişler Hem test etme hem de resmi doğrulama, programın beklenen davranışının bir açıklamasını gerektirir (testte kullanılan test senaryoları ve resmi doğrulamada kullanılan resmi spesifikasyonlarla birlikte). Ancak birlikte kullanıldıklarında bir programın daha kapsamlı bir şekilde incelenmesini sağlayabilirler. Örneğin test etme, basit hataları ve hataları bulmada etkilidir, ancak genellikle daha hızlı ve gerçekleştirilmesi daha kolaydır. Resmi doğrulama, kullanımı daha külfetli olsa da, hataların olmadığını kanıtlayacak veya testlerde veya kod incelemelerinde gözden kaçması kolay ince hataları ortaya çıkaracak kadar güçlüdür.

Spesifikasyon ek yükü

Resmi doğrulamanın ana zorluklarından biri, resmi şartnamelerin yazılması ve sürdürülmesinin ek yüküdür. Bu süreç genellikle spesifikasyonları özel bir dil kullanarak manuel olarak yazmak gibi zaman alan bir görevi içerir (birçok geliştiricinin önce bunu öğrenmesi gerekir). Süreç ayrıca artımlıdır, genellikle basit özelliklerin yazılması ve önce bunların doğrulanmasıyla başlar, ardından kademeli olarak daha karmaşık özelliklerin üstüne eklenmesiyle başlar. Test gibi, açık uçlu bir süreçtir, net bir durma noktası yoktur ve kişi yalnızca mevcut zaman çerçevesi içinde mümkün olduğu kadar çok özellik ekleyebilir. Ek olarak, geliştiriciler doğrulanırken kodu değiştirdiklerinde, mevcut teknik özelliklerini de güncellemeleri gerekir, bu da fazladan bakım çabalarına yol açar. Bu faktörler, fazladan ek yükü üstlenmekten çekinen bazı geliştiriciler için resmi doğrulamayı yıldırıcı bir görev haline getirebilir.

Test etme ve resmi doğrulama, birlikte kullanıldıklarında kod kalitesini iyileştirebilse de, her ikisi de bir programın beklenen davranışının farklı dillerde ve biçimlerde (bazen benzer) açıklamalarını gerektirir. Bu açıklamaları yazmak ve sürdürmek yoğun emek gerektirir ve aynı açıklamanın iki farklı biçimini sürdürmek, tekrarlanan bir çaba gibi gelebilir. Bu, şu soruyu gündeme getiriyor: Beklenen davranışı, geliştiricilerin hem test hem de doğrulama için kullanabileceği bir şekilde tanımlamak mümkün mü?

Sembolik test ve Halmos ile test etme ve resmi doğrulama arasındaki boşluğu doldurma

Sembolik test, sembolik girdilerle test çalıştırma pratiği, spesifikasyon ek yükünü azaltan etkili bir resmi doğrulama yöntemidir. Bu yaklaşım, hem test hem de resmi doğrulama için aynı test durumlarının kullanılmasını sağlar. Bir programın sınırlı bir dizi girdi için doğru çalıştığını doğrulayan geleneksel testten farklı olarak, sembolik test programı tüm olası girdiler için kontrol eder, bu nedenle sembolik testi geçen bir program resmi olarak doğrulanmış olarak kabul edilebilir.

Halmos, sembolik testler için tasarlanmış resmi bir doğrulama aracıdır. Halmos, ayrı spesifikasyonlar gerektirmek veya yeni bir dil öğrenmek yerine mevcut testleri resmi spesifikasyonlar olarak kullanır. Halmos aracılığıyla testler yapmak, olası tüm girdileri geçtiklerini otomatik olarak doğrular veya karşı örnekler sağlar. Bu sadece ek spesifikasyon yazma ihtiyacını ortadan kaldırmakla kalmaz, aynı zamanda birim testi veya bulanıklaştırma için yazılmış testlerin resmi doğrulama amacıyla yeniden kullanılmasına da izin verir.

Böylece geliştiriciler, mevcut ihtiyaçlarına bağlı olarak birim testi, belirsizleştirme ve resmi doğrulama dahil olmak üzere bir dizi kalite güvence seçeneği arasından seçim yapma konusunda daha fazla esnekliğe sahip olur. Örneğin testler, muhtemelen rasgele girdiler üreten bir fuzzer'ın yardımıyla basit hataları hızlı bir şekilde belirleyebilir ve ardından Halmos, programın tüm girdiler genelinde doğruluğuna olan güveni daha da artırabilir.

Örnek: isPowerOfTwo() işlev

Örnek olarak, aşağıdakileri göz önünde bulundurun isPowerOfTwo() verilen bir sayının ikinin katı olup olmadığını belirleyen işlev. Bu işlev bir bit işleme algoritması Ancak, özellikle girdinin ikinin kuvveti olmadığı durumlarda, doğruluğunu kanıtlamak zor olabilir.

için aşağıdaki testi hayal edin. isPowerOfTwo() işlev: işlevin gerçek çıktısını belirli bir girdi için beklenen çıktıyla karşılaştırır. Bu, parametreleştirilmiş bir testtir (özellik tabanlı test olarak da bilinir), farklı girdi değerleriyle, muhtemelen Foundry gibi bulanıklaştırma araçlarıyla kolayca çalıştırabileceğiniz anlamına gelir.

incelemek için bu testi kullanabilirsiniz. isPowerOfTwo() birim testi veya bulanıklık testi aracılığıyla işlev görür ve onu çeşitli girdilerle çalıştırır. Bu tür testler, testi olası her girdi için çalıştırmak hesaplama açısından mümkün olmadığından, işlevin doğruluğunu resmi olarak kanıtlayamaz.

Ancak Halmos, geliştiricilerin önceden var olan bu testleri yalnızca biraz ekstra çabayla resmi doğrulama için yeniden kullanmalarına izin verir. Araç, testin sembolik olarak yürütülmesini gerçekleştirerek ve ardından iddianın asla ihlal edilmediğini doğrulayarak (veya, iddia is ihlal, bir karşı örnek sağlayarak). Bu, test Halmos'u geçerse, işlevin doğruluğunun resmi olarak doğrulandığı, yani algoritmanın doğru bir şekilde uygulandığı ve derleyici tarafından bayt koduna doğru bir şekilde çevrildiği anlamına gelir.

Sınırlama: Sınırlı sembolik yürütme

Tam otomatik, eksiksiz sembolik test gerçekleştirmek genellikle mümkün değildir, çünkü bu, aşağıdaki sorunun çözülmesini gerektirecektir: durma problemiolduğu bilinen karar verilemez. Bunun bir nedeni, bir döngünün sembolik olarak kaç kez yinelenmesi gerektiğini otomatik olarak belirlemenin genellikle imkansız olmasıdır. Sonuç olarak, tam otomatik resmi doğrulama genellikle karar verilemez.

Bu temel sınırlamalar göz önüne alındığında Halmos, otomasyona eksiksizliğe öncelik verir. Bu amaçla Halmos, sınırsız döngüler (yineleme sayısının program girişlerine bağlı olduğu) veya değişken uzunluklu diziler (dizeler dahil) için sınırlı sembolik akıl yürütme gerçekleştirmek üzere tasarlanmıştır. Bu, bütünlükten biraz ödün verir, ancak Halmos'un, kullanıcının döngü değişmezleri gibi ek açıklamalar sağlamasını gerektirmekten kaçınmasına olanak tanır.

Örneğin, aşağıdaki yinelemeli sürümünü göz önünde bulundurun. isPowerOfTwo() döngü yinelemelerinin sayısının giriş sayısını temsil etmek için gereken minimum bit sayısı tarafından belirlendiği, sınırsız bir while döngüsü içeren işlev.

Halmos, bu sınırsız döngüyü yalnızca belirli bir sınıra kadar sembolik olarak yineler. Örneğin, sınır 3'e ayarlanırsa, Halmos döngüyü en fazla 3 kez yineler ve döngünün 3 defadan fazla yinelenmesine neden olacak girdi değerlerini dikkate almaz (yani, 2^3'e eşit veya daha büyük değerler) ). Bu özel durumda, sınırın 256 veya daha yükseğe ayarlanması Halmos'un tamamlanmasını sağlar.

Demo: Halmos ile ERC721A'nın resmi doğrulaması

Halmos'un yeteneklerini göstermek için onu sembolik olarak test etmek ve resmi olarak doğrulamak için kullandık. ERC721A, ERC721 standardının, tek basımla hemen hemen aynı maliyette toplu basıma izin veren, yüksek oranda gaz açısından optimize edilmiş bir uygulaması. ERC721A birkaç yenilikçi içerir optimizasyonlar bu verimliliği elde etmek için; örneğin, belirteç sahiplik verilerindeki güncellemeleri, basım sırasında değil, belirteç aktarılana kadar geciktirerek gaz tasarrufu yapılabilir. Bu, sahiplik bilgilerini tembel veri yapısından verimli bir şekilde almak için karmaşık veri yapılarının ve algoritmaların kullanılmasını gerektirir. Ve bu optimizasyon gaz verimliliğini iyileştirmesine rağmen, kod karmaşıklığını da artırır ve uygulamanın doğruluğunu kanıtlamayı zorlaştırır. Bu, uygulamaya olan güveni artırabileceği ve potansiyel kullanıcılara fayda sağlayabileceği için ERC721A'yı resmi doğrulama için iyi bir aday yapar.

Sembolik test özellikleri

ERC721A için mevcut testler Hardhat ile JavaScript'te yazıldığından (şu anda Halmos tarafından desteklenmemektedir), ana giriş noktası işlevleri için Solidity'de yeni testler yazdık: mint(), burn(), ve transfer(). Bu testler, her işlevin token sahipliğini ve bakiyesini doğru bir şekilde güncellediğini ve diğer kullanıcıların bakiyesini veya sahipliğini değiştirmeden yalnızca ilgili kullanıcıları etkilediğini kontrol etti. İkincisi, ERC721A'da tembel veri yapısı algoritmasının kullanılması nedeniyle kanıtlanması önemsiz değildir. Örneğin, aşağıdaki test, transfer() işlev, belirtilen belirtecin sahipliğini doğru şekilde günceller:

Başka bir test, transfer() işlevi, daha önce bahsedildiği gibi kanıtlanması zor olan diğer adresler için dengeyi değiştirmez:

Doğrulama sonuçları

ERC721A akıllı sözleşmesi üzerinde Halmos kullanarak toplam yazarak bir doğrulama deneyi gerçekleştirdik. 19 Testi. Testler, tamamlanması 3 dakika süren 16'lük bir döngü açma sınırıyla Halmos aracılığıyla gerçekleştirildi. Doğrulama süresinin dökümü aşağıdaki tabloda görülebilir. Deney, M1 Pro çipi ve 16 GB belleğe sahip bir MacBook Pro üzerinde gerçekleştirildi.

test	Zamanlar)
testBurnBalanceGüncelleme	6.67
testBurnNextTokenIdDeğişmedi	1.40
testBurnOtherBalanceKoruma	5.69
testBurnOtherOwnershipKoruma	189.70
testBurnOwnershipGüncelleme	3.81
testBurnGereksinimleri	71.95
testMintBalanceGüncelleme	0.20
testMintNextTokenIdGüncelleme	0.18
testMintOtherBalanceKoruma	0.26
testMintOtherSahiplik Koruması	5.74
testMintOwnershipGüncelleme	1.38
testMintGereksinimleri	0.09
testTransferBalanceDeğişmedi	9.03
testTransferBalanceGüncelleme	53.53
testTransferNextTokenIdDeğişmedi	4.47
testTransferOtherBalanceKoruma	19.57
testTransferOtherSahiplikKoruma	430.61
testTransferSahiplikGüncelleme	18.71
testTransferGereksinimleri	149.18

Testlerin çoğu birkaç saniye içinde tamamlanırken, birkaçı birkaç dakika sürdü. Bu zaman alıcı testlerin, dikkate alınması gereken vakaların karmaşık doğası nedeniyle doğrulanması zordu ve tembel veri yapısı algoritmasının doğruluğu ile yakından ilgiliydi.

Genel olarak, bu deneyin sonuçları, Halmos'un akıllı sözleşme kodunun doğruluğunu etkili bir şekilde doğrulayabildiğini gösteriyor. Akıllı sözleşmenin karmaşıklığına ve potansiyel uç durumlarına rağmen, kodun bütünlüğüne daha fazla güven sağlar.

Enjekte edilen hatalarla denemeler yapın

Halmos'un sınırlı akıl yürütmesinin etkinliğini göstermek için, onu ERC721A sözleşmesinin önceki bir sürümündeki hataları tespit etmek için kullandık. Bu sürümde, aritmetik taşmayı yanlış işleyen ve potansiyel olarak çok sayıda belirteci toplu olarak basmaya izin veren bir sorun vardı; bu, tembel veri yapısının bütünlüğünü bozabilir ve bazı kullanıcıların belirteç sahipliğini kaybetmesine neden olabilir (bir sorun çözüldü geçerli sürümde). Buggy versiyonunda ERC19A için aynı 721 test setini çalıştırdık ve Halmos, ERCXNUMXA'nın özellikleri için bir karşı örnek bulabildi. mint() işlev. Özellikle Halmos, yukarıda açıklanan açıklardan yararlanma senaryosuna yol açan girdi değerleri sağladı. Bu deneyin sonuçları, eksik olmasına rağmen, Halmos'un sınırlı muhakemesinin akıllı sözleşmelerdeki kötüye kullanılabilir hataları tespit etme ve önleme konusunda etkili bir yol olabileceğini göstermektedir.

Alakalı iş

Ethereum akıllı sözleşme bayt kodu için resmi doğrulama araçları, çeşitli ekipler tarafından geliştirilmiştir. Halmos da dahil olmak üzere bu araçlar, akıllı sözleşmelerin güvenliğini ve doğruluğunu sağlamaya yardımcı olmak için kullanılabilir. Bu araçların farklı özelliklerini, yeteneklerini ve sınırlamalarını karşılaştırmak ve anlamak, geliştiricilerin benzersiz ihtiyaçları için en uygun olanı seçmelerine yardımcı olabilir.

Halmos, akıllı sözleşme doğrulaması için mevcut araç setine değerli bir katkı olsa da, mevcut araçları tamamlaması (değiştirmemesi) amaçlanmıştır. Geliştiriciler, sözleşmelerinde daha yüksek bir güvence düzeyi elde etmek için Halmos'u diğer araçlarla birleştirebilir. Aşağıda, Halmos'u EVM bayt kodunu destekleyen birkaç seçilmiş resmi araçla karşılaştırıyoruz.

• K tümdengelimli doğrulama ve etkileşimli teorem ispatı sağlayan güçlü bir resmi doğrulama çerçevesidir. Temel teorisi ve uygulaması, yüksek düzeyde ifade sağlar ve karmaşık programları ve algoritmaları doğrulamak için uygun hale getirir. Ancak, K'nin otomatik doğrulamaya büyük önem verilerek tasarlanmadığına ve doğrulama işlemi sırasında daha fazla manuel çaba gerektirebilecek belirli otomasyon özelliklerinden yoksun olduğuna dikkat edilmelidir. K çerçevesini kullanmak için, kullanımdan önce öğrenilmesi gereken resmi özellikler K dilinde yazılır. Gücü, otomatik muhakeme kullanarak analiz etmesi zor olabilecek karmaşık sistemlerin doğrulanmasında özellikle yararlıdır.
• Certora otomatik doğrulamaya odaklanan ve Halmos'a benzer şekilde sınırlı model kontrolünü destekleyen akıllı sözleşmeler için resmi bir doğrulama aracıdır. Certora'yı kullanmak için geliştiricilerin yeni dillerini öğrenmeleri gerekir. özgeçmiş, özellikleri yazmak için. Bu dil, Halmos'un şu anda desteklemediği bir özellik olan sözleşme değişmezleri aracılığıyla birçok kritik özelliğin özlü açıklamasına izin verir. Kapalı kaynaklı, tescilli bir araç olmasına rağmen Certora, sürekli geliştirme ve iyi kullanıcı desteği ile sağlam resmi doğrulama araçları sağlar.
  
  Öte yandan Halmos, daha küçük ölçekli ve şu anda Certora tarafından sağlanan bazı özelliklerden yoksun olan açık kaynaklı bir araçtır, ancak kamu malı olarak hizmet etmesi amaçlanmıştır ve akıllı sözleşmeleri hızlı bir şekilde doğrulamak için niş bir çözüm olarak tasarlanmıştır. kapsamlı kurulum ve bakım ihtiyacı.
• HEVM Halmos'a benzeyen başka bir resmi doğrulama aracıdır. Daha önce Foundry'nin öncüsü olan DappTools'un bir parçasıydı. Hem HEVM hem de Halmos, ayrı bir belirtim gerektirmeme özelliğine sahiptir ve iddia ihlallerini belirlemek için mevcut testleri sembolik olarak yürütebilir. Bu, kullanıcıların her iki aracı birbirinin yerine kullanmasına veya aynı testler için paralel olarak çalıştırmalarına olanak tanıyarak onlara sembolik test için birden fazla seçenek sunar.
  
  Benzerliklerine rağmen HEVM ve Halmos'un bağımsız olarak geliştirildiğini ve uygulama ayrıntılarında farklılık gösterdiğini belirtmek gerekir; özellikle optimizasyonlar ve sembolik muhakeme stratejileri açısından. Ek olarak, HEVM Haskell'de yazılırken, Halmos Python'da yazılır ve zengin Python ekosistemine maruz kalma sağlar. Her iki aracı da kullanma yeteneğine sahip olmak, kullanıcılara akıllı sözleşmelerin güvenliğini ve doğruluğunu sağlamak için daha fazla esneklik ve seçenek sunar.

ağır açık kaynak kodludur ve şu anda beta aşamasındadır. Aktif olarak yeni üzerinde çalışıyoruz Özellikler ve Foundry hile kodları ve diğer birkaç önemli kullanılabilirlik özelliği dahil olmak üzere işlevsellik. Hangi özelliklerin en önemli olduğu konusundaki düşüncelerinizi çok takdir ediyoruz ve Halmos'u herkes için daha iyi bir araç haline getirmek için her türlü geri bildirimi, öneriyi ve katkıyı memnuniyetle karşılıyoruz.

**

Burada ifade edilen görüşler, alıntı yapılan bireysel AH Capital Management, LLC (“a16z”) personelinin görüşleridir ve a16z veya iştiraklerinin görüşleri değildir. Burada yer alan belirli bilgiler, a16z tarafından yönetilen fonların portföy şirketleri de dahil olmak üzere üçüncü taraf kaynaklardan elde edilmiştir. a16z, güvenilir olduğuna inanılan kaynaklardan alınmış olsa da, bu tür bilgileri bağımsız olarak doğrulamamıştır ve bilgilerin mevcut veya kalıcı doğruluğu veya belirli bir duruma uygunluğu hakkında hiçbir beyanda bulunmaz. Ayrıca, bu içerik üçüncü taraf reklamlarını içerebilir; a16z, bu tür reklamları incelememiştir ve burada yer alan herhangi bir reklam içeriğini onaylamaz.

Bu içerik yalnızca bilgilendirme amaçlıdır ve yasal, ticari, yatırım veya vergi tavsiyesi olarak kullanılmamalıdır. Bu konularda kendi danışmanlarınıza danışmalısınız. Herhangi bir menkul kıymete veya dijital varlığa yapılan atıflar yalnızca açıklama amaçlıdır ve yatırım tavsiyesi veya yatırım danışmanlığı hizmetleri sağlama teklifi teşkil etmez. Ayrıca, bu içerik herhangi bir yatırımcıya veya muhtemel yatırımcılara yönelik değildir veya bu içerik tarafından kullanılması amaçlanmamıştır ve a16z tarafından yönetilen herhangi bir fona yatırım yapma kararı verilirken hiçbir koşulda bu içeriğe güvenilemez. (Bir a16z fonuna yatırım yapma teklifi, yalnızca tahsisli satış mutabakatı, abonelik sözleşmesi ve bu tür bir fonun diğer ilgili belgeleri ile yapılacaktır ve bunların tamamı okunmalıdır.) Bahsedilen, atıfta bulunulan veya atıfta bulunulan herhangi bir yatırım veya portföy şirketi veya a16z tarafından yönetilen araçlara yapılan tüm yatırımları temsil etmemektedir ve yatırımların karlı olacağına veya gelecekte yapılacak diğer yatırımların benzer özelliklere veya sonuçlara sahip olacağına dair hiçbir garanti verilemez. Andreessen Horowitz tarafından yönetilen fonlar tarafından yapılan yatırımların bir listesi (ihraççının a16z'nin kamuya açıklanmasına izin vermediği yatırımlar ve halka açık dijital varlıklara yapılan habersiz yatırımlar hariç) https://a16z.com/investments adresinde bulunabilir. /.

İçerisinde yer alan çizelgeler ve grafikler yalnızca bilgilendirme amaçlıdır ve herhangi bir yatırım kararı verirken bunlara güvenilmemelidir. Geçmiş performans gelecekteki sonuçların göstergesi değildir. İçerik yalnızca belirtilen tarih itibariyle konuşur. Bu materyallerde ifade edilen tüm tahminler, tahminler, tahminler, hedefler, beklentiler ve/veya görüşler önceden bildirilmeksizin değiştirilebilir ve farklı olabilir veya başkaları tarafından ifade edilen görüşlere aykırı olabilir. Ek önemli bilgiler için lütfen https://a16z.com/disclosures adresine bakın.