Binius STARKs原理解析及其優化思考

1 引言

與基於橢圓曲線的SNARKs不同，STARKs可被視爲基於哈希的SNARKs。目前STARKs效率低下的一個主要原因是:實際程序中大多數數值都較小,如循環索引、布爾值、計數器等。然而,爲確保基於Merkle樹證明的安全性,使用Reed-Solomon編碼擴展數據時,許多冗餘值會佔據整個域,即使原始值很小。爲解決這個問題,降低域大小成爲關鍵策略。

第1代STARKs編碼位寬爲252位,第2代爲64位,第3代爲32位,但32位編碼仍有大量浪費空間。相比之下,二進制域允許直接對位進行操作,編碼緊湊高效而無浪費,可視爲第4代STARKs。

與近年來發現的Goldilocks、BabyBear、Mersenne31等有限域相比,二進制域的研究可追溯到20世紀80年代。目前二進制域已廣泛應用於密碼學,如AES(F28域)、GMAC(F2128域)、QR碼(F28的Reed-Solomon編碼)等。原始FRI和zk-STARK協議,以及SHA-3決賽入圍的Grøstl哈希函數也基於F28域。

使用較小域時,擴域操作對確保安全性愈發重要。Binius使用的二進制域完全依賴擴域來保證安全性和可用性。大多數Prover計算涉及的多項式只需在基域操作,從而在小域中實現高效率。但隨機點檢查和FRI計算仍需在更大的擴域中進行,以確保所需安全性。

基於二進制域構建證明系統時存在兩個實際問題:

1. STARKs中計算trace表示時,所用域大小應大於多項式的階
2. STARKs中Merkle樹承諾時需做Reed-Solomon編碼,所用域大小應大於編碼擴展後的大小

Binius提出創新解決方案,分別處理這兩個問題:

1. 使用多變量(多線性)多項式代替單變量多項式,通過其在"超立方體"上的取值表示整個計算軌跡
2. 由於超立方體每個維度長度爲2,無法像STARKs那樣進行標準Reed-Solomon擴展,但可將超立方體視爲方形,基於該方形進行Reed-Solomon擴展

這種方法在確保安全性的同時,極大提升了編碼效率與計算性能。

2 原理解析

當前大多數SNARKs系統通常包含兩部分:

1. 信息理論多項式交互預言機證明(PIOP): 作爲證明系統核心,將輸入的計算關係轉化爲可驗證的多項式等式。通過與驗證者交互,證明者逐步發送多項式,使驗證者通過查詢少量多項式評估結果即可驗證計算正確性。現有PIOP協議包括PLONK PIOP、Spartan PIOP和HyperPlonk PIOP等。

2. 多項式承諾方案(PCS): 用於證明PIOP生成的多項式等式是否成立。PCS是一種密碼學工具,證明者可承諾某個多項式並稍後驗證其評估結果,同時隱藏多項式其他信息。常見PCS有KZG、Bulletproofs、FRI和Brakedown等。

根據需求選擇不同PIOP和PCS,並結合合適的有限域或橢圓曲線,可構建具有不同屬性的證明系統。例如:

• Halo2:PLONK PIOP + Bulletproofs PCS + Pasta曲線
• Plonky2:PLONK PIOP + FRI PCS + Goldilocks域
• Binius:HyperPlonk PIOP + Brakedown PCS + 二進制域

Binius包括五項關鍵技術:

1. 基於塔式二進制域的算術化:構成計算基礎,在二進制域內實現簡化運算

2. 改編HyperPlonk乘積與置換檢查:確保變量及置換間的高效一致性檢查

3. 新的多線性移位論證:優化小域上多線性關係驗證效率

4. 改進Lasso查找論證:爲查找機制提供靈活性和安全性

5. 小域多項式承諾方案:在二進制域上實現高效證明系統,減少大域相關開銷

2.1 有限域:基於towers of binary fields的算術化

塔式二進制域是實現快速可驗證計算的關鍵,主要歸因於高效計算和高效算術化。二進制域本質上支持高度高效的算術操作,成爲性能敏感密碼學應用的理想選擇。二進制域結構支持簡化的算術化過程,在二進制域上執行的運算可以緊湊易驗證的代數形式表示。這些特性加上能通過塔結構充分利用其層次特性,使二進制域特別適合Binius這樣的可擴展證明系統。

"canonical"指二進制域中元素的唯一且直接表示方式。例如,在基本二進制域F2中,任意k位字符串都可直接映射到k位二進制域元素。這與素數域不同,素數域無法在給定位數內提供這種規範表示。盡管32位素數域可包含在32位中,但並非每個32位字符串都能唯一對應一個域元素,而二進制域具備這種一對一映射便利性。

在素數域Fp中,常見歸約方法包括Barrett歸約、Montgomery歸約,以及針對Mersenne-31或Goldilocks-64等特定有限域的特殊歸約方法。在二進制域F2k中,常用歸約方法包括特殊歸約(如AES使用)、Montgomery歸約(如POLYVAL使用)和遞歸歸約(如Tower)。

論文《Exploring the Design Space of Prime Field vs. Binary Field ECC-Hardware Implementations》指出,二進制域在加法和乘法運算中均無需引入進位,且二進制域的平方運算非常高效,因爲它遵循(X + Y)2 = X2 + Y2的簡化規則。

一個128位字符串可在二進制域上下文中以多種方式解釋。它可被視爲128位二進制域中的獨特元素,或解析爲兩個64位塔域元素、四個32位塔域元素、16個8位塔域元素,或128個F2域元素。這種表示靈活性不需任何計算開銷,只是對位字符串的類型轉換,是非常有趣且有用的屬性。同時,小域元素可被打包爲更大的域元素而不需額外計算開銷。Binius協議利用這一特性提高計算效率。

論文《On Efficient Inversion in Tower Fields of Characteristic Two》探討了在n位塔式二進制域中(可分解爲m位子域)進行乘法、平方和求逆運算的計算復雜度。

2.2 PIOP:改編版HyperPlonk Product和PermutationCheck------適用於二進制域

Binius協議中的PIOP設計借鑑了HyperPlonk,採用一系列核心檢查機制驗證多項式和多變量集合的正確性:

1. GateCheck:驗證保密見證ω和公開輸入x是否滿足電路運算關係C(x,ω)=0,確保電路正確運行。

2. PermutationCheck:驗證兩個多變量多項式f和g在布爾超立方體上的求值結果是否爲置換關係f(x) = f(π(x)),確保多項式變量間的排列一致性。

3. LookupCheck:驗證多項式的求值是否在給定查找表中,即f(Bμ) ⊆ T(Bμ),確保某些值在指定範圍內。

4. MultisetCheck:檢查兩個多變量集合是否相等,即{(x1,i,x2,)}i∈H={(y1,i,y2,)}i∈H,保證多個集合間的一致性。

5. ProductCheck:檢測有理多項式在布爾超立方體上的求值是否等於某個聲明的值∏x∈Hμ f(x) = s,確保多項式乘積的正確性。

6. ZeroCheck:驗證一個多變量多項式在布爾超立方體上的任意點是否爲零∏x∈Hμ f(x) = 0,∀x ∈ Bμ,確保多項式的零點分布。

7. SumCheck:檢測多變量多項式的求和值是否爲聲明的值∑x∈Hμ f(x) = s。通過將多元多項式的求值問題轉化爲單變量多項式求值,降低驗證方的計算復雜度。此外,SumCheck還允許批處理,通過引入隨機數,構造線性組合實現對多個和校驗實例的批處理。

8. BatchCheck:基於SumCheck,驗證多個多變量多項式求值的正確性,以提高協議效率。

盡管Binius與HyperPlonk在協議設計上有許多相似之處,但Binius在以下3個方面做出改進:

• ProductCheck優化:在HyperPlonk中,ProductCheck要求分母U在超立方體上處處非零,且乘積必須等於特定值;Binius通過將該值特化爲1,簡化這一檢查過程,降低計算復雜度。

• 除零問題處理:HyperPlonk未能充分處理除零情況,導致無法斷言U在超立方體上的非零問題;Binius正確地處理了這一問題,即使在分母爲零的情況下,Binius的ProductCheck也能繼續處理,允許推廣到任意乘積值。

• 跨列PermutationCheck:HyperPlonk無此功能;Binius支持在多個列之間進行PermutationCheck,使Binius能夠處理更復雜的多項式排列情況。

因此,Binius通過對現有PIOP SumCheck機制的改進,提升了協議的靈活性和效率,尤其在處理更復雜的多變量多項式驗證時,提供了更強的功能支持。這些改進不僅解決了HyperPlonk中的局限性,還爲未來基於二進制域的證明系統奠定了基礎。

2.3 PIOP:新的 multilinear shift argument------適用於 boolean hypercube

在Binius協議中,虛擬多項式的構造和處理是關鍵技術之一,能有效地生成和操作從輸入句柄或其他虛擬多項式派生出的多項式。以下是兩個關鍵方法:

• Packing:該方法通過將詞典序中相鄰位置的較小元素打包成更大的元素來優化操作。Pack運算符針對大小爲2κ的塊操作,並將它們組合成高維域中的單個元素。通過多線性擴展(Multilinear Extension, MLE),這個虛擬多項式可以高效地評估和處理,將函數t轉換爲另一個多項式,從而提高了計算性能。

• 移位運算符:移位運算符重新排列塊內的元素,基於給定偏移量o進行循環移位。該方法適用於大小爲2b的塊,每個塊根據偏移量執行移位。移位運算符通過檢測函數的支持來進行定義,確保在處理虛擬多項式時保持一致性和效率。評估該構造的復雜度隨塊大小線性增長,特別適用於處理大數據集或布爾超立方體中的高維場景。

2.4 PIOP:改編版Lasso lookup argument------適用於二進制域

Lasso協議允許證明方承諾一個向量a ∈ Fm,並證明其所有元素均存在於一個預先指定的表t ∈ Fn 中。Lasso解鎖了"查找奇點"(lookup singularities)的概念,並能適用於多線性多項式承諾方案。其效率體現在以下兩個方面:

• 證明效率:對於大小爲n的表中的m次查找,證明方只需承諾m+n個域元素。這些域元素很小,均位於集合{0,...,m}中。在基於多次冪運算的承諾方案中,證明方的計算成本爲O(m + n)次羣運算(如