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

1 引言

STARKs效率低下的一個主要原因是實際程序中的大多數數值都較小，但爲了確保基於Merkle樹證明的安全性，使用Reed-Solomon編碼對數據進行擴展時，許多額外的冗餘值會佔據整個域。爲解決該問題，降低域的大小成爲了關鍵策略。

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

當採用較小的域時，擴域操作對於確保安全性愈發重要。而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）
• 多項式承諾方案（Polynomial Commitment Scheme, PCS）

Binius：HyperPlonk PIOP + Brakedown PCS + 二進制域。具體而言，Binius包括五項關鍵技術，以實現其高效性和安全性：

1. 基於塔式二進制域的算術化
2. 改編版HyperPlonk乘積與置換檢查
3. 新的多線性移位論證
4. 改進版Lasso查找論證
5. 小域多項式承諾方案

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

塔式二進制域是實現快速可驗證計算的關鍵，主要歸因於兩個方面：高效計算和高效算術化。二進制域本質上支持高度高效的算術操作，使其成爲對性能要求敏感的密碼學應用的理想選擇。此外，二進制域結構支持簡化的算術化過程，即在二進制域上執行的運算可以以緊湊且易於驗證的代數形式表示。

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

二進制域在加法和乘法運算中均無需引入進位，且二進制域的平方運算非常高效，因爲它遵循(X + Y )2 = X2 + Y 2 的簡化規則。

2.2 PIOP：改編版HyperPlonk Product和PermutationCheck

Binius協議中的PIOP設計借鑑了HyperPlonk，採用了一系列核心檢查機制，用於驗證多項式和多變量集合的正確性。這些核心檢查包括：

1. GateCheck
2. PermutationCheck
3. LookupCheck
4. MultisetCheck
5. ProductCheck
6. ZeroCheck
7. SumCheck
8. BatchCheck

Binius與HyperPlonk相比做出了以下改進：

• ProductCheck優化
• 除零問題的處理
• 跨列PermutationCheck

2.3 PIOP：新的 multilinear shift argument

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

• Packing
• 移位運算符

2.4 PIOP：改編版Lasso lookup argument

Lasso協議允許證明方承諾一個向量a ∈ Fm，並證明其所有元素均存在於一個預先指定的表t ∈ Fn 中。Lasso協議由以下三個組件構成：

• 大表的虛擬多項式抽象
• 小表查找
• 多集合檢查

Binius協議將Lasso適應於二進制域的操作，引入了乘法版本的Lasso協議。

2.5 PCS：改編版Brakedown PCS

構建BiniusPCS的核心思想是packing。Binius論文中提供了2種基於二進制域的Brakedown多項式承諾方案：

1. 採用concatenated code來實例化
2. 採用block-level encoding技術，支持單獨使用Reed-Solomon codes

Binius多項式承諾主要使用以下技術：

• 小域多項式承諾與擴展域評估
• 小域通用構造
• 塊級編碼與Reed-Solomon碼

3 優化思考

爲了進一步提升Binius協議的性能，本文提出了四個關鍵優化點：

1. GKR-based PIOP：針對二進制域乘法運算
2. ZeroCheck PIOP優化：在Prover與Verifier之間進行計算開銷權衡
3. Sumcheck PIOP優化：針對小域Sumcheck的優化
4. PCS 優化：通過FRI-Binius優化

3.1 GKR-based PIOP：基於GKR的二進制域乘法

基於GKR的整數乘法運算算法，通過將"檢查2個32-bit整數A和B是否滿足 A·B =? C"，轉換爲"檢查中(gA)B =? gC 是否成立"，借助GKR協議大幅減少承諾開銷。

3.2 ZeroCheck PIOP優化：Prover與Verifier計算開銷權衡

論文《Some Improvements for the PIOP for ZeroCheck》在證明方（P）和驗證方（V）之間調整工作量的分配，提出了多種優化方案，以權衡開銷。主要優化包括：

• 減少證明方的數據傳輸
• 減少證明方評估點的數量
• 代數插值優化

3.3 Sumcheck PIOP優化：基於小域的Sumcheck協議

Ingonyama在2024年提出了針對基於小域的Sumcheck協議的改進方案，並開源了實現代碼。主要優化包括：

• 切換輪次的影響與改進因子
• 基域大小對性能的影響
• Karatsuba算法的優化收益
• 內存效率的提升

3.4 PCS 優化：FRI-Binius降低Binius proof size

論文《Polylogarithmic Proofs for Multilinears over Binary Towers》，簡稱爲FRI-Binius，實現了二進制域FRI折疊機制，帶來4個方面的創新：

• 扁平化多項式
• 子空間消失多項式
• 代數基打包
• 環交換SumCheck

借助FRI-Binius，可將Binius證明大小減少一個數量級。

4 小結

Binius是"使用硬件、軟件、與FPGA中加速的Sumcheck協議"的協同設計方案，可以以非常低的內存使用率來快速證明。Binius中已基本完全移除了Prover的commit承諾瓶頸，新的瓶頸在於Sumcheck協議，而Sumcheck協議中大量多項式evaluations和域乘法等問題，可借助專用硬件高效解決。

FRI-Binius方案，爲FRI變體，可提供一個非常有吸引力的選擇——從域證明層中消除嵌入開銷，而不會導致聚合證明層的成本激增。當前，Irreducible團隊正在開發其遞歸層，並宣布與Polygon團隊合作構建Binius-based zkVM；JoltzkVM正從Lasso轉向Binius，以改進其遞歸性能；Ingonyama團隊正在實現FPGA版本的Binius。