Binius STARK'ların Prensip Analizi ve Optimizasyon Düşünceleri

1 Giriş

Elli eğri tabanlı SNARK'lar ile karşılaştırıldığında, STARK'lar hash tabanlı SNARK'lar olarak düşünülebilir. Şu anda STARK'ların verimsiz olmasının ana nedenlerinden biri, gerçek programlardaki çoğu sayının oldukça küçük olmasıdır; örneğin döngü indeksleri, Boolean değerler, sayaçlar vb. Ancak, Merkle ağaçları tabanlı kanıtların güvenliğini sağlamak için Reed-Solomon kodlaması kullanarak verileri genişletirken, birçok fazlalık değer tüm alanı kaplayabilir, bu durumda orijinal değerler çok küçük olsa bile. Bu sorunu çözmek için alan boyutunu azaltmak kritik bir strateji haline gelmiştir.

1. nesil STARKs kodlama genişliği 252 bit, 2. nesil 64 bit, 3. nesil 32 bit, ancak 32 bit kodlama hala büyük miktarda israf alanına sahiptir. Buna karşın, ikili alan doğrudan bitlere işlem yapmaya izin verir, kodlama sıkı ve verimli olup israf olmadan, 4. nesil STARKs olarak görülebilir.

Son yıllarda keşfedilen Goldilocks, BabyBear, Mersenne31 gibi sonlu alanlarla karşılaştırıldığında, ikili alanların araştırması 1980'li yıllara kadar uzanmaktadır. Günümüzde ikili alanlar, AES(F28 alanı), GMAC(F2128 alanı), QR kodu(F28'in Reed-Solomon kodlaması) gibi kriptografide yaygın olarak kullanılmaktadır. Orijinal FRI ve zk-STARK protokolleri ile SHA-3 finale kalan Grøstl hash fonksiyonu da F28 alanına dayanmaktadır.

Küçük alanlar kullanıldığında, genişletme işlemleri güvenliği sağlamak için giderek daha önemli hale gelir. Binius'un kullandığı ikili alan, güvenlik ve kullanılabilirliği sağlamak için tamamen genişletmeye bağımlıdır. Çoğu Prover hesaplamasında yer alan çok terimli polinomlar, yalnızca temel alanda işlem yaparak küçük alanda yüksek verimlilik sağlar. Ancak rastgele nokta kontrolü ve FRI hesaplamaları, gerekli güvenliği sağlamak için daha büyük bir genişletme alanında gerçekleştirilmelidir.

İkili alan üzerine inşa edilen kanıt sistemlerinde iki pratik sorun bulunmaktadır:

1. STARKs'te iz hesaplanırken kullanılan alan boyutu, polinomun derecesinden büyük olmalıdır.
2. STARKs'da Merkle ağaçlarının taahhüdü sırasında Reed-Solomon kodlaması yapılmalı ve kullanılan alan boyutu, kodlama genişletildikten sonra boyuttan büyük olmalıdır.

Binius, bu iki sorunu ayrı ayrı ele alan yenilikçi bir çözüm sunuyor:

1. Tek değişkenli polinom yerine çok değişkenli ( çoklu lineer ) çok terimli polinom kullanarak, "hiperküp" üzerindeki değerleri ile tüm hesaplama izini temsil et.
2. Süper küpün her boyutunun uzunluğu 2 olduğundan, STARKs gibi standart Reed-Solomon genişlemesi yapılamaz, ancak süper küp bir kare olarak düşünülebilir ve bu kareye dayalı olarak Reed-Solomon genişlemesi yapılabilir.

Bu yöntem, güvenliği sağlarken kodlama verimliliğini ve hesaplama performansını büyük ölçüde artırmıştır.

2 Prensip Analizi

Şu anda çoğu SNARKs sistemi genellikle iki bölümden oluşur:

1. Bilgi teorisi çoklu etkileşimli kehanet makinesi kanıtı ( PIOP ): Güvenilir bir sistemin temeli olarak, girilen hesaplama ilişkisini doğrulanabilir çok terimli eşitliklere dönüştürür. Doğrulayıcı ile etkileşim kurarak, kanıtlayıcı aşama aşama çok terimli ifadeleri gönderir ve doğrulayıcı, birkaç çok terimli sorgulayarak hesaplama doğruluğunu doğrulayabilir. Mevcut PIOP protokolleri arasında PLONK PIOP, Spartan PIOP ve HyperPlonk PIOP gibi seçenekler bulunmaktadır.

2. Polinom taahhüt planı ( PCS ): PIOP tarafından üretilen çok terimli denklemin geçerliliğini kanıtlamak için kullanılır. PCS, bir kriptografik araçtır; kanıtlayıcı, belirli bir çok terimle taahhüt edebilir ve daha sonra değerlendirme sonuçlarını doğrulayabilirken, çok terimin diğer bilgilerini gizli tutar. Yaygın PCS'ler arasında KZG, Bulletproofs, FRI ve Brakedown bulunmaktadır.

İhtiyaçlara göre farklı PIOP ve PCS'yi seçerek ve uygun bir sonlu alan veya eliptik eğri ile birleştirerek, farklı özelliklere sahip kanıt sistemleri oluşturulabilir. Örneğin:

• Halo2:PLONK PIOP + Bulletproofs PCS + Pasta eğrisi
• Plonky2:PLONK PIOP + FRI PCS + Goldilocks alanı
• Binius: HyperPlonk PIOP + Brakedown PCS + ikili alan

Binius beş ana teknoloji içerir:

1. Kule tipi ikili alan tabanlı aritmetik: Hesaplama temeli oluşturma, ikili alanda basitleştirilmiş işlemler gerçekleştirme.

2. HyperPlonk çarpım ve permütasyon kontrolünü yeniden düzenleme: değişkenler ve permütasyonlar arasındaki verimli tutarlılık kontrolünü sağlama

3. Yeni çok çizgili kaydırma kanıtı: Küçük alanlarda çok çizgili ilişki doğrulama verimliliğini optimize etme

4. Lasso bulma kanıtını iyileştirme: Bulma mekanizmasına esneklik ve güvenlik sağlama

5. Küçük alan çok terimli taahhüt planı: İkili alanda verimli kanıt sistemleri gerçekleştirmek, büyük alanla ilgili maliyetleri azaltmak.

2.1 Sonlu Alan: Binary Alanların Kuleleri Temelinde Arithmetik

Kule tarzı ikili alan, hızlı doğrulanabilir hesaplamaların gerçekleştirilmesinde anahtar rol oynamaktadır, bunun başlıca nedeni verimli hesaplama ve verimli aritmetik işlemlerdir. İkili alan, esasen yüksek verimli aritmetik işlemleri destekler ve performansa duyarlı kriptografik uygulamalar için ideal bir seçimdir. İkili alan yapısı, basitleştirilmiş aritmetik süreçleri destekler; ikili alanda gerçekleştirilen işlemler, kompakt ve kolayca doğrulanabilir cebirsel biçimlerde ifade edilebilir. Bu özellikler, kule yapısının katmanlı özelliklerini tam olarak kullanabilme yeteneği ile birleştiğinde, ikili alanları Binius gibi ölçeklenebilir kanıt sistemleri için özellikle uygun hale getirir.

"canonical", ikili alan içindeki elemanların benzersiz ve doğrudan gösterim biçimini ifade eder. Örneğin, temel ikili alan F2'de, herhangi bir k bitlik dize doğrudan k bitlik ikili alan elemanına haritalanabilir. Bu, asal alandan farklıdır; asal alan belirli bir bit sayısı içinde bu tür bir standart gösterim sunamaz. 32 bitlik asal alan 32 bit içinde yer alabilirken, her 32 bitlik dize benzersiz bir alan elemanıyla eşleşmez; oysa ikili alan bu birbiriyle eşleşme kolaylığını sağlar.

Fp asal alanında, yaygın azaltma yöntemleri Barrett azaltması, Montgomery azaltması ve Mersenne-31 veya Goldilocks-64 gibi belirli sonlu alanlar için özel azaltma yöntemlerini içerir. İkili alanda F2k, yaygın azaltma yöntemleri özel azaltma ( gibi AES'in kullandığı ), Montgomery azaltması ( gibi POLYVAL'ın kullandığı ) ve tekrarlamalı azaltma ( gibi Tower )'dir.

Makale "Prime Field ile Binary Field ECC Donanım Uygulamaları Tasarım Alanını Keşfetmek"de, ikili alanın toplama ve çarpma işlemlerinde taşma gerektirmediği ve ikili alanın kare alma işleminin son derece verimli olduğu belirtilmiştir, çünkü (X + Y)2 = X2 + Y2 basitleştirilmiş kuralını izlemektedir.

128 bit'lik bir dize, ikili alan bağlamında çeşitli şekillerde yorumlanabilir. Bu, 128 bit'lik ikili alandaki benzersiz bir öğe olarak görülebilir veya iki 64 bit'lik kule alan öğesi, dört 32 bit'lik kule alan öğesi, on altı 8 bit'lik kule alan öğesi veya 128 tane F2 alan öğesi olarak çözümlenebilir. Bu temsil esnekliği, herhangi bir hesaplama maliyeti olmadan, yalnızca bit dizisinin tür dönüşümü ile sağlanır ve son derece ilginç ve faydalı bir özelliktir. Aynı zamanda, küçük alan öğeleri, ek hesaplama maliyeti olmadan daha büyük alan öğelerine paketlenebilir. Binius protokolü, bu özelliği hesaplama verimliliğini artırmak için kullanır.

"On Efficient Inversion in Tower Fields of Characteristic Two" başlıklı makale, n bitlik kule ikili alanında ('in m bitlik alt alan )'e ayrılmasının çarpma, kare alma ve ters alma işlemlerinin hesaplama karmaşıklığını incelemektedir.

2.2 PIOP: Uyarlanmış HyperPlonk Ürünü ve Permutasyon Kontrolü------İkili alan için uygundur

Binius protokolündeki PIOP tasarımı HyperPlonk'tan esinlenmiştir ve çok terimli ve çok değişkenli kümelerin doğruluğunu doğrulamak için bir dizi temel kontrol mekanizması kullanmaktadır:

1. GateCheck: Gizli tanık ω ve açık girdi x'in devre işlem ilişkisi C(x, ω)=0'ı sağladığını doğrulayın, devrenin doğru çalıştığından emin olun.

2. PermutationCheck: İki çok değişkenli çok terimli f ve g'nin Boolean hiperküpü üzerindeki değerlendirme sonuçlarının bir permütasyon ilişkisi olup olmadığını doğrulamak f(x) = f(π(x)), çok terimli değişkenler arasındaki sıralamanın tutarlılığını sağlamak.

3. LookupCheck: Verilen arama tablosunda bir polinomun değerlendirmesinin doğruluğunu doğrulamak, yani f(Bμ) ⊆ T(Bμ), belirli değerlerin belirtilen aralıkta olduğunu garanti etmek.

4. MultisetCheck: İki çok değişkenli kümenin eşitliğini kontrol etme, yani {(x1,i,x2,)}i∈H={(y1,i,y2,)}i∈H, birden fazla küme arasında tutarlılığı sağlama.

5. ProductCheck: Rasyonel çok terimli polinomun Boolean hiperkümesindeki değerlendirmesinin belirli bir ifade edilen değer ile eşit olup olmadığını kontrol etme ∏x∈Hμ f(x) = s, polinom çarpımının doğruluğunu sağlama.

6. ZeroCheck: Bir çok değişkenli çok terimli polinomun Boolean hiperküpündeki herhangi bir noktada sıfır olup olmadığını doğrulamak ∏x∈Hμ f(x) = 0, ∀x ∈ Bμ, polinomun sıfır noktalarının dağılımını sağlamak.

7. SumCheck: Çok değişkenli polinomların toplamının belirtilen değer olup olmadığını kontrol eder ∑x∈Hμ f(x) = s. Çok değişkenli polinomların değerlendirme problemini tek değişkenli polinom değerlendirme problemlerine dönüştürerek doğrulayıcı tarafın hesaplama karmaşıklığını azaltır. Ayrıca, SumCheck toplu işleme de olanak tanır, rastgele sayılar kullanarak, birden fazla toplam doğrulama örneği için doğrusal kombinasyonlar oluşturur.

8. BatchCheck: SumCheck'e dayalı olarak, birden fazla çok değişkenli çok terimli polinomun değerlendirilmesinin doğruluğunu doğrulamak için protokol verimliliğini artırır.

Binius, HyperPlonk ile protokol tasarımı açısından birçok benzerliğe sahip olmasına rağmen, aşağıdaki 3 alanda iyileştirmeler yapmıştır:

• ProductCheck optimizasyonu: HyperPlonk'ta, ProductCheck'in U paydasının hiperküp üzerinde her yerde sıfır olmaması ve çarpımın belirli bir değere eşit olması gerekmektedir; Binius, bu değeri 1 olarak özelleştirerek bu kontrol sürecini basitleştirmiş ve hesaplama karmaşıklığını azaltmıştır.

• Sıfıra bölme problemi çözümü: HyperPlonk sıfıra bölme durumunu yeterince ele alamamıştır, bu da U'nun hiperküp üzerindeki sıfır olmayan problemini kesin olarak belirlemeyi imkansız hale getirir; Binius bu sorunu doğru bir şekilde ele almıştır, sıfır olan bir paydada bile Binius'un ProductCheck'i işlemeye devam edebilir ve herhangi bir çarpan değerine genişletilmesine izin verir.

• Sütunlar Arası Permutasyon Kontrolü: HyperPlonk bu özelliği desteklemiyor; Binius, birden fazla sütun arasında Permutasyon Kontrolü yapmayı destekleyerek, Binius'un daha karmaşık çok terimli sıralama durumlarını işleyebilmesini sağlar.

Bu nedenle, Binius mevcut PIOP SumCheck mekanizmasını geliştirerek protokolün esnekliğini ve verimliliğini artırdı. Özellikle daha karmaşık çok değişkenli polinom doğrulamalarını işlerken daha güçlü fonksiyon desteği sağladı. Bu iyileştirmeler yalnızca HyperPlonk'taki sınırlamaları gidermekle kalmayıp, aynı zamanda gelecekteki ikili alan tabanlı kanıt sistemleri için bir temel oluşturmuştur.

2.3 PIOP: Yeni çoklu kaydırma argümanı------boolean hiper kümesine uygundur

Binius protokolünde, sanal çok terimli ifadelerin oluşturulması ve işlenmesi, etkili bir şekilde giriş tutamaklarından veya diğer sanal çok terimli ifadelerden türetilen çok terimli ifadeleri oluşturup işletmesini sağlayan ana tekniklerden biridir. İşte iki ana yöntem:

• Paketleme: Bu yöntem, kelime dizisindeki komşu konumlarda bulunan daha küçük öğeleri daha büyük öğeler haline getirerek işlemi optimize eder. Pack operatörü 2κ boyutundaki blok işlemlerine yöneliktir ve bunları yüksek boyutlu alanlardaki tek bir öğe haline getirir. Çoklu lineer genişletme (Multilinear Extension, MLE) ile bu sanal polinom etkili bir şekilde değerlendirilebilir ve işlenebilir, fonksiyonu t başka bir polinoma dönüştürerek hesaplama performansını artırır.

• Kaydırma operatörü: Kaydırma operatörü, belirli bir kaydırma miktarı o'ya dayanarak blok içindeki öğeleri döngüsel olarak yeniden düzenler. Bu yöntem, her bir bloğun kaydırma yapıldığı 2b boyutundaki bloklar için geçerlidir. Kaydırma operatörü, sanal çok terimli ifadeleri işlerken tutarlılık ve verimliliği sağlamak için destek fonksiyonunu algılayarak tanımlanır. Bu yapının karmaşıklığı, blok boyutuyla doğrusal olarak artar ve özellikle büyük veri kümeleri veya Boole hiperküplerindeki yüksek boyutlu senaryoların işlenmesi için uygundur.

2.4 PIOP: uyarlama Lasso arama argümanı------ikili alan için uygundur

Lasso protokolü, kanıtlayıcının a ∈ Fm bir vektörünü taahhüt etmesine ve tüm elemanlarının önceden belirlenmiş bir tablo t ∈ Fn içinde bulunduğunu kanıtlamasına izin verir. Lasso, "sıfır noktalarını bulma" (lookup singularities) kavramını açığa çıkarmış ve çok değişkenli çok terimli taahhüt şemalarına uygulanabilir. Verimliliği aşağıdaki iki alanda kendini göstermektedir:

• Kanıt verimliliği: Boyutu n olan bir tabloda m kez arama yapılması durumunda, kanıtlayıcı sadece m+n alan öğesi taahhüt etmelidir. Bu alan öğeleri çok küçüktür ve {0,...,m} kümesinde yer alır. Çoklu üs alma işlemlerine dayanan taahhüt şemasında, kanıtlayıcının hesaplama maliyeti O(m + n) grup işlemi( kadar olur.