Binius STARKs原理解析及优化思考

1. 引言

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

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

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

Binius提出了一种创新的解决方案:首先，使用多变量（具体是多线性）多项式代替单变量多项式，通过其在"超立方体"（hypercubes）上的取值来表示整个计算轨迹；其次，由于超立方体每个维度的长度均为2，因此无法像STARKs那样进行标准的Reed-Solomon扩展，但可以将超立方体视为方形（square），基于该方形进行Reed-Solomon扩展。

2. 原理解析

Binius包括五项关键技术:

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

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

塔式二进制域的优势:

• 高效计算:二进制域本质上支持高度高效的算术操作
• 高效算术化:二进制域结构支持简化的算术化过程
• 规范表示:二进制域中元素有唯一且直接的表示方式

二进制域优势:

• 加法和乘法运算无需引入进位
• 平方运算非常高效,遵循(X + Y)^2 = X^2 + Y^2 的简化规则
• 表示灵活性:128位字符串可视为128位二进制域中的独特元素,或解析为多种塔域元素组合

2.2 PIOP:改编版HyperPlonk Product和PermutationCheck

Binius PIOP核心检查机制:

• GateCheck
• PermutationCheck
• LookupCheck
• MultisetCheck
• ProductCheck
• ZeroCheck
• SumCheck
• BatchCheck

Binius对HyperPlonk的改进:

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

2.3 PIOP:新的multilinear shift argument

关键方法:

• Packing:通过打包相邻元素优化操作
• 移位运算符:重新排列块内元素

2.4 PIOP:改编版Lasso lookup argument

Lasso协议组成:

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

Binius对Lasso的改编:

• 引入乘法版本的Lasso协议
• 要求证明方承诺一个处处非零的读取计数向量

2.5 PCS:改编版Brakedown PCS

核心思想:packing

两种基于二进制域的Brakedown多项式承诺方案:

1. 采用concatenated code实例化
2. 采用block-level encoding技术,支持单独使用Reed-Solomon codes

主要技术:

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

3. 优化思考

四个关键优化点:

3.1 GKR-based PIOP:基于GKR的二进制域乘法

相比Binius lookup方案的优势:

• 只需一个辅助承诺
• 减少Sumchecks开销

3.2 ZeroCheck PIOP优化:Prover与Verifier计算开销权衡

优化方法:

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

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

关键点:

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

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

FRI-Binius四个创新:

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

FRI-Binius PCS过程:

• 承诺阶段
• 评估阶段

4. 小结

Binius的价值主张:

• 可为witnesses使用最小的power-of-two域
• 协同设计方案,低内存使用率快速证明
• 基本移除Prover的commit承诺瓶颈
• 新瓶颈在于Sumcheck协议,可借助专用硬件高效解决

FRI-Binius方案:

• 从域证明层中消除嵌入开销
• 不会导致聚合证明层成本激增

当前进展:

• Irreducible团队开发递归层,与Polygon合作构建Binius-based zkVM
• JoltzkVM从Lasso转向Binius
• Ingonyama团队实现FPGA版本Binius