Binius STARKs原理解析及优化思考

1. 引言

STARKs效率低下的一个主要原因是实际程序中大多数数值较小，但为确保基于Merkle树证明的安全性，使用Reed-Solomon编码对数据进行扩展时，许多额外的冗余值会占据整个域。降低域的大小成为了关键策略。

第1代STARKs编码位宽为252bit，第2代为64bit，第3代为32bit，但32bit编码位宽仍存在大量浪费空间。相比之下,二进制域允许直接对位操作，编码紧凑高效而无任意浪费空间，即第4代STARKs。

Binius采用二进制域，需完全依赖扩域来保证其安全性和实际可用性。大多数Prover计算中涉及的多项式无需进入扩域，而只需在基域下操作，从而在小域中实现了高效率。然而，随机点检查和FRI计算仍需深入到更大的扩域中，以确保所需的安全性。

Binius提出了一种创新的解决方案:首先，使用多变量（具体是多线性）多项式代替单变量多项式，通过其在"超立方体"上的取值来表示整个计算轨迹；其次，将超立方体视为方形，基于该方形进行Reed-Solomon扩展。这种方法在确保安全性的同时，极大提升了编码效率与计算性能。

2. 原理解析

Binius包括五项关键技术:

1. 基于塔式二进制域的算术化
2. 改编版HyperPlonk乘积与置换检查
3. 新的多线性移位论证
4. 改进版Lasso查找论证
5. 小域多项式承诺方案

2.1 有限域:基于towers of binary fields的算术化

塔式二进制域支持高度高效的算术操作，支持简化的算术化过程。二进制域的元素具有唯一且直接的表示方式，可以灵活地在不同大小的域之间转换和打包。

2.2 PIOP:改编版HyperPlonk Product和PermutationCheck

Binius采用了一系列核心检查机制，包括GateCheck、PermutationCheck、LookupCheck、MultisetCheck、ProductCheck、ZeroCheck、SumCheck和BatchCheck。

相比HyperPlonk，Binius在以下方面做出改进:

• ProductCheck优化
• 除零问题的处理
• 跨列PermutationCheck

2.3 PIOP:新的multilinear shift argument

Binius采用Packing和移位运算符两个关键方法来处理虚拟多项式。

2.4 PIOP:改编版Lasso lookup argument

Lasso协议由三个组件构成:

• 大表的虚拟多项式抽象
• 小表查找
• 多集合检查

Binius引入了乘法版本的Lasso协议，要求证明方和验证方联合递增协议的"内存计数"操作，不是通过简单的加1递增，而是通过二进制域中的乘法生成元来递增。

2.5 PCS:改编版Brakedown PCS

Binius多项式承诺主要使用:

• 小域多项式承诺与扩展域评估
• 小域通用构造
• 块级编码与Reed-Solomon码技术

3. 优化思考

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计算开销权衡

• 减少证明方的数据传输
• 减少证明方评估点的数量
• 代数插值优化

3.3 Sumcheck PIOP优化:基于小域的Sumcheck协议

• 切换轮次的影响与改进因子
• 基域大小对性能的影响
• Karatsuba算法的优化收益
• 内存效率的提升

3.4 PCS 优化:FRI-Binius降低Binius proof size

FRI-Binius实现了二进制域FRI折叠机制,带来4个方面的创新:

• 扁平化多项式
• 子空间消失多项式
• 代数基打包
• 环交换SumCheck

4. 小结

Binius基本完全移除了Prover的commit承诺瓶颈,新的瓶颈在于Sumcheck协议。FRI-Binius方案为FRI变体,可从域证明层中消除嵌入开销。目前,Irreducible团队正在开发其递归层,并与Polygon团队合作构建Binius-based zkVM;JoltzkVM正从Lasso转向Binius;Ingonyama团队正在实现FPGA版本的Binius。