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

1. 引言

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

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

相比于 Goldilocks、BabyBear、Mersenne31 等近几年新研究发现的有限域,二进制域的研究可追溯到上个世纪 80 年代。当前,二进制域已经广泛应用于密码学中,典型例子包括:

• 高级加密标准(AES),基于 F28 域;

• Galois 消息认证码(GMAC),基于 F2128 域;

• QR 码,使用基于 F28 的 Reed-Solomon 编码;

• 原始 FRI 和 zk-STARK 协议,以及进入 SHA-3 决赛的 Grøstl 哈希函数,该函数基于 F28 域,是一种非常适合递归的哈希算法。

当采用较小的域时,扩域操作对于确保安全性愈发重要。而 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):PIOP 作为证明系统的核心,将输入的计算关系转化为可以验证的多项式等式。不同的 PIOP 协议通过与验证者的交互,允许证明者逐步发送多项式,使得验证者通过查询少量多项式的评估结果即可验证计算是否正确。现有的 PIOP 协议包括:PLONK PIOP、Spartan PIOP 和 HyperPlonk PIOP 等,它们各自对多项式表达式的处理方式有所不同,从而影响整个 SNARK 系统的性能与效率。

• 多项式承诺方案(Polynomial Commitment Scheme, PCS):多项式承诺方案用于证明 PIOP 生成的多项式等式是否成立。PCS 是一种密码学工具,通过它,证明者可以承诺某个多项式并在稍后验证该多项式的评估结果,同时隐藏多项式的其他信息。常见的多项式承诺方案有 KZG、Bulletproofs、FRI(Fast Reed-Solomon IOPP)和 Brakedown 等。不同的 PCS 具有不同的性能、安全性和适用场景。

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

• Halo2:由 PLONK PIOP 与 Bulletproofs PCS 结合,并基于 Pasta 曲线。Halo2 设计时,注重于可扩展性,以及移除 ZCash 协议中的 trusted setup。

• Plonky2:采用 PLONK PIOP 与 FRI PCS 结合,并基于 Goldilocks 域。Plonky2 是为了实现高效递归的。在设计这些系统时,选择的 PIOP 和 PCS 必须与所使用的有限域或椭圆曲线相匹配,以确保系统的正确性、性能和安全性。这些组合的选择不仅影响 SNARK 的证明大小和验证效率,还决定了系统是否能够在无需可信设置的前提下实现透明性,是否可以支持递归证明或聚合证明等扩展功能。

Binius:HyperPlonk PIOP + Brakedown PCS + 二进制域。具体而言,Binius 包括五项关键技术,以实现其高效性和安全性。首先,基于塔式二进制域(towers of binary fields)的算术化构成了其计算的基础,能够在二进制域内实现简化的运算。其次,Binius 在其交互式 Oracle 证明协议(PIOP)中,改编了 HyperPlonk 乘积与置换检查,确保了变量及其置换之间的安全高效的一致性检查。第三,协议引入了一个新的多线性移位论证,优化了在小域上验证多线性关系的效率。第四,Binius 采用了改进版的 Lasso 查找论证,为查找机制提供了灵活性和强大的安全性。最后,协议使用了小域多项式承诺方案(Small-Field PCS),使其能够在二进制域上实现高效的证明系统,并减少了通常与大域相关的开销。

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

如图 1 所示,一个 128 位字符串:该字符串可以在二进制域的上下文中以多种方式进行解释。它可以被视为 128 位二进制域中的一个独特元素,或者被解析为两个 64 位塔域元素、四个 32 位塔域元素、16 个 8 位塔域元素,或 128 个 F2 域元素。这种表示的灵活性不需要任何计算开销,只是对位字符串的类型转换(typecast),是一个非常有趣且有用的属性。同时,小域元素可以被打包为更大的域元素而不需要额外的计算开销。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 通过对