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

1 引言

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

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

表 1: STARKs 衍化路徑

| 特徵 | 第1代STARKs | 第2代STARKs | 第3代STARKs | 第4代STARKs(Binius) | |------|-------------|-------------|-------------|---------------------| | 編碼位寬 | 252bit | 64bit | 32bit | 1bit | | 代表性系統 | StarkWare | Plonky2 | BabyBear | Binius |

相比於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通過對現有PIOPSumCheck機制的改進，提升了協議的靈活性和效率，尤其在處理更復雜的多變量多項式驗證時，提供了更強的功能支持。這些改進不僅解決了HyperPlonk中的局限性，還爲未來基於二進