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

1 引言

与基于椭圆曲线的SNARKs不同，STARKs可被视为基于哈希的SNARKs。目前STARKs效率低下的一个主要原因是:实际程序中大多数数值都较小,如循环索引、布尔值、计数器等。然而,为确保基于Merkle树证明的安全性,使用Reed-Solomon编码扩展数据时,许多冗余值会占据整个域,即使原始值很小。为解决这个问题,降低域大小成为关键策略。

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

与近年来发现的Goldilocks、BabyBear、Mersenne31等有限域相比,二进制域的研究可追溯到20世纪80年代。目前二进制域已广泛应用于密码学,如AES(F28域)、GMAC(F2128域)、QR码(F28的Reed-Solomon编码)等。原始FRI和zk-STARK协议,以及SHA-3决赛入围的Grøstl哈希函数也基于F28域。

使用较小域时,扩域操作对确保安全性愈发重要。Binius使用的二进制域完全依赖扩域来保证安全性和可用性。大多数Prover计算涉及的多项式只需在基域操作,从而在小域中实现高效率。但随机点检查和FRI计算仍需在更大的扩域中进行,以确保所需安全性。

基于二进制域构建证明系统时存在两个实际问题:

1. STARKs中计算trace表示时,所用域大小应大于多项式的阶
2. STARKs中Merkle树承诺时需做Reed-Solomon编码,所用域大小应大于编码扩展后的大小

Binius提出创新解决方案,分别处理这两个问题:

1. 使用多变量(多线性)多项式代替单变量多项式,通过其在"超立方体"上的取值表示整个计算轨迹
2. 由于超立方体每个维度长度为2,无法像STARKs那样进行标准Reed-Solomon扩展,但可将超立方体视为方形,基于该方形进行Reed-Solomon扩展

这种方法在确保安全性的同时,极大提升了编码效率与计算性能。

2 原理解析

当前大多数SNARKs系统通常包含两部分:

1. 信息理论多项式交互预言机证明(PIOP): 作为证明系统核心,将输入的计算关系转化为可验证的多项式等式。通过与验证者交互,证明者逐步发送多项式,使验证者通过查询少量多项式评估结果即可验证计算正确性。现有PIOP协议包括PLONK PIOP、Spartan PIOP和HyperPlonk PIOP等。

2. 多项式承诺方案(PCS): 用于证明PIOP生成的多项式等式是否成立。PCS是一种密码学工具,证明者可承诺某个多项式并稍后验证其评估结果,同时隐藏多项式其他信息。常见PCS有KZG、Bulletproofs、FRI和Brakedown等。

根据需求选择不同PIOP和PCS,并结合合适的有限域或椭圆曲线,可构建具有不同属性的证明系统。例如:

• Halo2:PLONK PIOP + Bulletproofs PCS + Pasta曲线
• Plonky2:PLONK PIOP + FRI PCS + Goldilocks域
• Binius:HyperPlonk PIOP + Brakedown PCS + 二进制域

Binius包括五项关键技术:

1. 基于塔式二进制域的算术化:构成计算基础,在二进制域内实现简化运算

2. 改编HyperPlonk乘积与置换检查:确保变量及置换间的高效一致性检查

3. 新的多线性移位论证:优化小域上多线性关系验证效率

4. 改进Lasso查找论证:为查找机制提供灵活性和安全性

5. 小域多项式承诺方案:在二进制域上实现高效证明系统,减少大域相关开销

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 + Y2的简化规则。

一个128位字符串可在二进制域上下文中以多种方式解释。它可被视为128位二进制域中的独特元素,或解析为两个64位塔域元素、四个32位塔域元素、16个8位塔域元素,或128个F2域元素。这种表示灵活性不需任何计算开销,只是对位字符串的类型转换,是非常有趣且有用的属性。同时,小域元素可被打包为更大的域元素而不需额外计算开销。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通过对现有PIOP SumCheck机制的改进,提升了协议的灵活性和效率,尤其在处理更复杂的多变量多项式验证时,提供了更强的功能支持。这些改进不仅解决了HyperPlonk中的局限性,还为未来基于二进制域的证明系统奠定了基础。

2.3 PIOP:新的 multilinear shift argument------适用于 boolean hypercube

在Binius协议中,虚拟多项式的构造和处理是关键技术之一,能有效地生成和操作从输入句柄或其他虚拟多项式派生出的多项式。以下是两个关键方法:

• Packing:该方法通过将词典序中相邻位置的较小元素打包成更大的元素来优化操作。Pack运算符针对大小为2κ的块操作,并将它们组合成高维域中的单个元素。通过多线性扩展(Multilinear Extension, MLE),这个虚拟多项式可以高效地评估和处理,将函数t转换为另一个多项式,从而提高了计算性能。

• 移位运算符:移位运算符重新排列块内的元素,基于给定偏移量o进行循环移位。该方法适用于大小为2b的块,每个块根据偏移量执行移位。移位运算符通过检测函数的支持来进行定义,确保在处理虚拟多项式时保持一致性和效率。评估该构造的复杂度随块大小线性增长,特别适用于处理大数据集或布尔超立方体中的高维场景。

2.4 PIOP:改编版Lasso lookup argument------适用于二进制域

Lasso协议允许证明方承诺一个向量a ∈ Fm,并证明其所有元素均存在于一个预先指定的表t ∈ Fn 中。Lasso解锁了"查找奇点"(lookup singularities)的概念,并能适用于多线性多项式承诺方案。其效率体现在以下两个方面:

• 证明效率:对于大小为n的表中的m次查找,证明方只需承诺m+n个域元素。这些域元素很小,均位于集合{0,...,m}中。在基于多次幂运算的承诺方案中,证明方的计算成本为O(m + n)次群运算(如