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。