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

1. 引言

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

第 1 代 STARKs 編碼位寬爲 252bit,第 2 代 STARKs 編碼位寬爲 64bit,第 3 代 STARKs 編碼位寬爲 32bit,但 32bit 編碼位寬仍然存在大量的浪費空間。相較而言,二進制域允許直接對位進行操作,編碼緊湊高效而無任意浪費空間,即第 4 代 STARKs。

相比於 Goldilocks、BabyBear、Mersenne31 等近幾年新研究發現的有限域,二進制域的研究可追溯到上個世紀 80 年代。當前,二進制域已經廣泛應用於密碼學中,典型例子包括:

• 高級加密標準(AES),基於 F28 域;

• Galois 消息認證碼(GMAC),基於 F2128 域;

• QR 碼,使用基於 F28 的 Reed-Solomon 編碼;

• 原始 FRI 和 zk-STARK 協議,以及進入 SHA-3 決賽的 Grøstl 哈希函數,該函數基於 F28 域,是一種非常適合遞歸的哈希算法。

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

基於二進制域來構建證明系統時,存在 2 個實際問題:STARKs 中計算 trace 表示時,所用域大小應大於多項式的階;STARKs 中 Merkle tree 承諾時,需做 Reed-Solomon 編碼,所用域大小應大於編碼擴展後的大小。

Binius 提出了一種創新的解決方案,分別處理這兩個問題,並通過兩種不同的方式表示相同的數據來實現:首先,使用多變量(具體是多線性)多項式代替單變量多項式,通過其在"超立方體"(hypercubes)上的取值來表示整個計算軌跡;其次,由於超立方體每個維度的長度均爲 2,因此無法像 STARKs 那樣進行標準的 Reed-Solomon 擴展,但可以將超立方體視爲方形(square),基於該方形進行 Reed-Solomon 擴展。這種方法在確保安全性的同時,極大提升了編碼效率與計算性能。

2. 原理解析

當前大多數 SNARKs 系統的構建通常包含以下兩部分:

• 信息理論多項式交互預言機證明(Information-Theoretic Polynomial Interactive Oracle Proof, PIOP):PIOP 作爲證明系統的核心,將輸入的計算關係轉化爲可以驗證的多項式等式。不同的 PIOP 協議通過與驗證者的交互,允許證明者逐步發送多項式,使得驗證者通過查詢少量多項式的評估結果即可驗證計算是否正確。現有的 PIOP 協議包括:PLONK PIOP、Spartan PIOP 和 HyperPlonk PIOP 等,它們各自對多項式表達式的處理方式有所不同,從而影響整個 SNARK 系統的性能與效率。

• 多項式承諾方案(Polynomial Commitment Scheme, PCS):多項式承諾方案用於證明 PIOP 生成的多項式等式是否成立。PCS 是一種密碼學工具,通過它,證明者可以承諾某個多項式並在稍後驗證該多項式的評估結果,同時隱藏多項式的其他信息。常見的多項式承諾方案有 KZG、Bulletproofs、FRI(Fast Reed-Solomon IOPP)和 Brakedown 等。不同的 PCS 具有不同的性能、安全性和適用場景。

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

• Halo2:由 PLONK PIOP 與 Bulletproofs PCS 結合,並基於 Pasta 曲線。Halo2 設計時,注重於可擴展性,以及移除 ZCash 協議中的 trusted setup。

• Plonky2:採用 PLONK PIOP 與 FRI PCS 結合,並基於 Goldilocks 域。Plonky2 是爲了實現高效遞歸的。在設計這些系統時,選擇的 PIOP 和 PCS 必須與所使用的有限域或橢圓曲線相匹配,以確保系統的正確性、性能和安全性。這些組合的選擇不僅影響 SNARK 的證明大小和驗證效率,還決定了系統是否能夠在無需可信設置的前提下實現透明性,是否可以支持遞歸證明或聚合證明等擴展功能。

Binius:HyperPlonk PIOP + Brakedown PCS + 二進制域。具體而言,Binius 包括五項關鍵技術,以實現其高效性和安全性。首先,基於塔式二進制域(towers of binary fields)的算術化構成了其計算的基礎,能夠在二進制域內實現簡化的運算。其次,Binius 在其交互式 Oracle 證明協議(PIOP)中,改編了 HyperPlonk 乘積與置換檢查,確保了變量及其置換之間的安全高效的一致性檢查。第三,協議引入了一個新的多線性移位論證,優化了在小域上驗證多線性關係的效率。第四,Binius 採用了改進版的 Lasso 查找論證,爲查找機制提供了靈活性和強大的安全性。最後,協議使用了小域多項式承諾方案(Small-Field PCS),使其能夠在二進制域上實現高效的證明系統,並減少了通常與大域相關的開銷。

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 + Y 2 的簡化規則。

如圖 1 所示,一個 128 位字符串:該字符串可以在二進制域的上下文中以多種方式進行解釋。它可以被視爲 128 位二進制域中的一個獨特元素,或者被解析爲兩個 64 位塔域元素、四個 32 位塔域元素、16 個 8 位塔域元素,或 128 個 F2 域元素。這種表示的靈活性不需要任何計算開銷,只是對位字符串的類型轉換(typecast),是一個非常有趣且有用的屬性。同時,小域元素可以被打包爲更大的域元素而不需要額外的計算開銷。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 通過對