与基于椭圆曲线的SNARKs不同,STARKs可以看作是基于哈希的SNARKs。目前STARKs效率低下的一个主要原因是,实际程序中的大部分值相对较小,比如for循环中的索引、布尔值和计数器。然而,为了确保Merkle树证明的安全性,采用Reed-Solomon编码对数据进行扩展,这导致了大量冗余值占用整个域,尽管原始值很小。为了解决这个效率问题,减少域的大小已成为关键策略。
如表1所示,第1代STARKs编码位宽为252bit,第2代STARKs编码位宽为64bit,第3代STARKs编码位宽为32bit,但32bit编码位宽仍然存在大量的浪费空间。相较而言,二进制域允许直接对位进行操作,编码紧凑高效而无任意浪费空间,即第4代STARKs。
表 1:STARKs 推导路径
与近期受到关注的有限域(如Goldilocks、BabyBear和Mersenne31)相比,二进制域的研究可以追溯到1980年代。如今,二进制域在密码学中被广泛应用,主要包括以下几个例子:
在使用较小的域时,域扩展操作对确保安全性变得尤为重要。Binius所采用的二进制域完全依赖于域扩展,以保证安全性和实用性。大多数与Prover操作相关的多项式计算无需进入扩展域,只需在基域中进行操作,从而在小域中实现高效率。然而,随机点检查和FRI计算仍需在更大的扩展域中进行,以确保必要的安全级别。
在基于二进制域构建证明系统时,有两个实际挑战:首先,STARKs中用于轨迹表示的域大小必须大于多项式的度数;其次,STARKs中用于Merkle树承诺的域大小需大于经过Reed-Solomon编码扩展后的大小。
Binius通过两种不同的方式来解决这两个问题,提供了一种创新的解决方案:首先,使用多变量(特别是多线性)多项式代替单变量多项式,通过在“超立方体”上的评估来表示整个计算轨迹;其次,由于超立方体的每个维度长度为2,无法像STARKs那样进行标准的Reed-Solomon扩展,但可以将超立方体视为一个正方形,并基于这个正方形进行Reed-Solomon扩展。这种方法不仅确保了安全性,还大幅提升了编码效率和计算性能。
现代大多数SNARK系统的构建通常包含两个主要组件:
通过选择不同的PIOP和PCS方案,并将它们与适当的有限域或椭圆曲线结合,可以构建具有不同特性的证明系统。例如:
在设计这些系统时,所选PIOP、PCS与有限域或椭圆曲线之间的兼容性对于确保系统的正确性、性能和安全性至关重要。这些组合会影响SNARK证明的大小、验证效率,并决定系统是否能够在没有可信设置的情况下实现透明性,以及是否支持递归证明或证明聚合等高级功能。
Binius结合了HyperPlonk PIOP与Brakedown PCS,并在二进制域中运作。具体来说,Binius结合了五项关键技术,以实现效率和安全性:
这些创新使Binius能够提供一个紧凑且高性能的SNARK系统,专为二进制域优化,同时保持强大的安全性和可扩展性。
塔式二进制域是实现快速可验证计算的关键,主要归因于两个方面:高效计算和高效算术化。二进制域本质上支持高度高效的算术操作,使其成为对性能要求敏感的密码学应用的理想选择。此外,二进制域结构支持简化的算术化过程,即在二进制域上执行的运算可以以紧凑且易于验证的代数形式表示。这些特性,加上能够通过塔结构充分利用其层次化的特性,使得二进制域特别适合于诸如Binius这样可扩展的证明系统。
图 1: 塔式二进制域
如图1所示,一个128位字符串:该字符串可以在二进制域的上下文中以多种方式进行解释。它可以被视为128位二进制域中的一个独特元素,或者被解析为两个64位塔域元素、四个32位塔域元素、16个8位塔域元素,或128个F2域元素。
这种表示的灵活性不需要任何计算开销,只是对位字符串的类型转换(typecast),是一个非常有趣且有用的属性。同时,小域元素可以被打包为更大的域元素而不需要额外的计算开销。
Binius协议利用了这一特性,以提高计算效率。此外,论文《On Efficient Inversion in Tower Fields of Characteristic Two》探讨了在n位塔式二进制域中(可分解为m位子域)进行乘法、平方和求逆运算的计算复杂度。
Binius协议中的PIOP设计借鉴了HyperPlonk,采用了一系列核心检查机制,用于验证多项式和多变量集合的正确性。这些核心检查包括:
尽管Binius与HyperPlonk在协议设计上有许多相似之处,但Binius在以下3个方面做出改进:
因此,Binius通过对现有PIOPSumCheck机制的改进,提升了协议的灵活性和效率,尤其在处理更复杂的多变量多项式验证时,提供了更强的功能支持。这些改进不仅解决了HyperPlonk中的局限性,还为未来基于二进制域的证明系统奠定了基础。
在Binius协议中,虚拟多项式的构造和处理是关键技术之一,能够有效地生成和操作从输入句柄或其他虚拟多项式派生出的多项式。以下是两个关键方法:
Lasso协议允许证明方承诺一个向量a ∈ Fm,并证明其所有元素均存在于一个预先指定的表t ∈ Fn 中。Lasso解锁了“查找奇点”(lookup singularities)的概念,并能适用于多线性多项式承诺方案。其效率体现在以下两个方面:
Lasso协议由以下三个组件构成:
Binius协议将Lasso适应于二进制域的操作,假设当前域是一个大特征的素数域(远大于被查找列的长度)。Binius引入了乘法版本的Lasso协议,要求证明方和验证方联合递增协议的“内存计数”操作,不是通过简单的加1递增,而是通过二进制域中的乘法生成元来递增。然而,这一乘法改编引入了更多的复杂性,与递增操作不同,乘法生成元并非在所有情况下递增,在0处存在单一轨道,这可能成为攻击点。为防止这种潜在的攻击,证明方必须承诺一个处处非零的读取计数向量,以确保协议的安全性。
构建BiniusPCS的核心思想是packing。Binius论文中提供了2种基于二进制域的Brakedown多项式承诺方案:一种是采用concatenated code来实例化;另一种采用block-level encoding技术,支持单独使用Reed-Solomon codes。第二种Brakedown PCS方案,简化了证明和验证流程,但proof size要比第一种略大一点,但所带来的简化和实现优势,做该取舍是值得的。
Binius多项式承诺主要使用小域多项式承诺与扩展域评估、小域通用构造和块级编码与Reed-Solomon码技术。
小域多项式承诺与扩展域评估:Binius协议中的承诺是在小域K上的多项式承诺,并在更大的扩展域L/K中进行评估。这种方法确保了每个多线性多项式t(X0,…,Xℓ−1)属于域K[X0,…,Xℓ−1],而评估点可以位于更大扩展域L中。承诺方案专门设计用于小域多项式,并能在扩展域上进行查询,同时保证承诺的安全性和效率。
小域通用构造:小域通用构造通过定义参数ℓ、域K及其相关的线性块码C,确保扩展域L足够大,以支持安全评估。为了在保持计算效率的同时提高安全性,协议通过扩展域的特性,以及采用线性块码对多项式进行编码,保证了承诺的稳健性。
块级编码与Reed-Solomon码:针对字段比线性块码字母表更小的多项式,Binius提出了块级编码方案。通过这一方案,即使在小域(如F2)中定义的多项式,也可以使用如F216这样的大字母表的Reed-Solomon码高效承诺。Reed-Solomon码之所以被选中,是因为它具有高效性和最大距离分离特性。该方案通过将消息打包并逐行编码,之后利用Merkle树进行承诺,简化了操作复杂度。块级编码允许小域多项式的高效承诺,而不会产生通常与大域相关的高计算开销,从而使得在F2等小域中承诺多项式成为可能,并在生成证明与验证中保持计算效率。
为了进一步提升Binius协议的性能,本文提出了四个关键优化点:
Binius论文引入一种基于lookup的方案,旨在实现高效的二进制域乘法运算。通过Lasso lookup argument 改编的二进制域乘法算法依赖于lookups和加法操作的线性关系,这些操作与单个word中的limbs数量成比例。虽然这一算法在某种程度上优化了乘法操作,但仍需要与limbs数量线性相关的辅助承诺。
GKR(Goldwasser-Kalai-Rothblum)协议中的核心思想是,证明方(P)和验证方(V)针对一个有限域F上的layered算术电路达成一致。该电路的每个节点有两个输入,用于计算所需的函数。为了减少验证方的计算复杂度,协议使用SumCheck协议,将关于电路输出门值的声明逐步简化为更低层的门值声明,直至最终将声明简化到关于输入的陈述。这样,验证方只需检查电路输入的正确性即可。
基于GKR的整数乘法运算算法,通过将“检查2个32-bit整数A和B是否满足 A·B =? C”,转换为“检查中(gA)B =? gC 是否成立”,借助GKR协议大幅减少承诺开销。与之前的Binius lookup方案相比,基于GKR的二进制域乘法运算只需一个辅助承诺,并且通过减少Sumchecks的开销,使该算法更加高效,特别是在Sumchecks操作比承诺生成更便宜的场景下。随着Binius优化的推进,基于GKR的乘法运算逐渐成为减少二进制域多项式承诺开销的有效途径。
论文《Some Improvements for the PIOP for ZeroCheck》在证明方(P)和验证方(V)之间调整工作量的分配,提出了多种优化方案,以权衡开销。该工作探索了不同的k值配置,使得在证明方和验证方之间达成了成本的权衡,特别是在减少传输数据和降低计算复杂性方面。
减少证明方的数据传输:通过将一部分工作转移给验证方V,从而降低证明方P发送的数据量。在第i轮中,证明方P需要向验证方V发送vi+1(X),其中X=0,…,d + 1。验证方V检查以下等式以验证数据的正确性:
vi = vi+1(0) + vi+1(1).
优化方法:证明方P可以选择不发送vi+1(1),而是让验证方V自行通过以下方式计算出该值
vi+1(1) = vi − vi+1(0).
此外,在第0轮,诚实的证明方P始终发送v1(0) = v1(1) = 0,这意味着无需进行任何评估计算,从而显著减少了计算和传输成本,降低至d2n−1CF + (d + 1)2n−1CG。
减少证明方评估点的数量:在协议的第i轮中,验证者在之前的i轮中已经发送了一个值序列r =(r0,…,ri−1)。当前协议要求证明者 (P) 发送多项式
vi+1(X) = ∑ δˆn(α,(r,X,x))C(r,X,x).x∈H −−1
优化方法:证明方P发送以下多项式这两个函数之间的关系是:
vi(X) = vi′(X)·δi+1((α0,…,αi),(r,X))
其中δˆi+1因为验证者拥有α和r,所以是完全已知的。这个修改的好处在于vi′(X)的次数比vi(X)少1,这意味着证明者需要评估的点更少。因此,主要的协议变化发生在轮次之间的检查环节。
此外,将原本的约束vi = vi+1(0)+vi+1(1) 优化为 (1−αi)vi′+1(0)+αivi′+1(1) = vi′(X)。则证明者需要评估和发送的数据更少,进一步减少传输的数据量。计算δˆn−i−1也比计算δˆn更高效。通过这两项改进,成本降低为大约:2n−1(d− 1)CF + 2n−1dCG。在常见的d=3情况下,这些优化使成本降低了5/3倍。
代数插值优化:对于诚实的证明者,C(x0,…,xn−1)在Hn上为零,可表示为:C(x0,…,xn-1)= ∑xi(xi-1)Qi(x0,…,xn-1)。虽然Qi不是唯一的,但可以通过多项式长除法构造一个有序的分解:从Rn=C开始,逐次除以xi(xi−1)来计算Qi和Ri,其中R0是C在Hn上的多线性扩展,且假设其为零。分析Qi的次数,可以得出:对于j> i,Qj 在 xi 上的次数与 C 相同;对于 j = i,次数减少 2;对于 j i,次数至多为 1。给定向量 r = (r0,…,ri),Qj(r,X) 对于所有 j ≤ i 都是多线性的。此外1)Qj(r,X) 是与 C(r,X) 在 Hn−i 上相等的唯一多线性多项式。对于任何 X 和 x ∈ Hn−i−1,可以表示为:
C(r,X,x) − Qi(r,X,x) = X(X − 1)Qi+1(r,X,x)
因此,在协议的每一轮中,仅引入一个新的Q,其评估值可以从C和先前的Q计算得出,实现插值优化。
Binius所实现的STARKs方案,其承诺开销很低,使得prover瓶颈不再是PCS,而在于sum-check协议。
图 2. 切换轮次与因子改进之间的关系
Ingonyama在2024年提出了针对基于小域的Sumcheck协议的改进方案(对应图2中的Algo3和Algo4算法),并开源了实现代码。算法4专注于将Karatsub算法合并到算法3中,以额外的基域乘法为代价来最小化扩域乘法次数,因此当扩域乘法比基域乘法昂贵得多时,算法4的性能会更好。
基于小域的Sumcheck协议的改进集中于切换轮次t的选择。切换轮次是指从优化算法切换回朴素算法的时间点,论文的实验表明,在最佳切换点时,改进因子达到最大值,随后呈现抛物线趋势。如果超过这一切换点,优化算法的性能优势减弱,效率下降。这是由于小域上的基域乘法与扩域乘法相比有更高的时间比率,因此在适当时机切换回朴素算法至关重要。
对于具体应用,如涉及Cubic Sumcheck(d = 3)的情况,基于小域的Sumcheck协议相较于朴素算法的改进达到了一个数量级。例如,在基域为GF[2]的情况下,算法4的性能比朴素算法高出近30倍。
论文的实验结果表明,较小的基域(如GF[2])能够使优化算法显示出更显著的优势。这是因为扩展域与基域乘法的时间比率在较小基域上更高,从而优化算法在此条件下表现出更高的改进因子。
Karatsuba算法在提升基于小域的Sumcheck性能方面表现出显著的效果。对于基域GF[2],算法3和算法4的峰值改进因子分别为6和30,表明算法4比算法3高效五倍。Karatsuba优化不仅提升了运行效率,也优化了算法的切换点,分别在算法3的t=5和算法4的t=8达到最佳。
基于小域的Sumcheck协议除了提升运行时间,还在内存效率方面表现出显著的优势。算法4的内存需求为O(d·t),而算法3的内存需求为O(2d·t)。当t=8时,算法4仅需0.26MB的内存,而算法3则需67MB来存储基域的乘积。这使得算法4在内存受限设备上表现出更强的适应性,尤其适用于资源有限的客户端证明环境。
Binius协议的一个主要缺陷在于其相对较大的证明大小,随着见证大小的平方根按O(√N)缩放。与更高效的系统相比,这种平方根大小的证明是一种局限性。相反,对数级(polylogarithmic)证明大小对于实现真正“简洁”的验证器至关重要,这在像Plonky3这样的先进系统中得到了验证,后者通过FRI等先进技术实现了对数级证明。
论文《Polylogarithmic Proofs for Multilinears over Binary Towers》,简称为FRI-Binius,实现了二进制域FRI折叠机制,带来4个方面的创新:
基于二进制域FRI-Binius的多线性多项式承诺方案(PCS)的核心思想为:FRI-Binius协议通过将初始的二进制域多线性多项式(定义于F2上)打包为定义在更大域K上的多线性多项式来操作。
在基于二进制域的FRI-BiniusPCS中,过程如下:
借助FRI-Binius,可将Binius证明大小减少一个数量级。这使得Binius的证明大小更加接近最先进的系统,同时保持与二进制域的兼容性。专为二进制域定制的FRI折叠技术,加上代数打包和SumCheck的优化,使得Binius能够在保持高效验证的同时,生成更加简洁的证明。
表 2:Binius 与 FRI-Binius 证明大小比较
表 3:Plonky3 FRI 与 FRI-Binius 比较
Binius的整个价值主张是,可为witnesses使用最小的power-of-two域,因此只需根据所需来选择域大小。Binius是“使用硬件、软件、与FPGA中加速的Sumcheck协议”的协同设计方案,可以以非常低的内存使用率来快速证明。Halo2和Plonky3等证明系统有4个占用大部分计算量的关键步骤:生成witness数据、对witness数据进行承诺、vanishingargument、openingproof。以Plonky3中的Keccak和Binius中的Grøstl哈希函数为例,二者对应的以上4大关键步骤计算量占比情况如图3所示:
图 3. 较小的承诺成本
由此可知,Binius中已基本完全移除了Prover的commit承诺瓶颈,新的瓶颈在于Sumcheck协议,而Sumcheck协议中大量多项式evaluations和域乘法等问题,可借助专用硬件高效解决。FRI-Binius方案,为FRI变体,可提供一个非常有吸引力的选择——从域证明层中消除嵌入开销,而不会导致聚合证明层的成本激增。当前,Irreducible团队正在开发其递归层,并 宣布与Polygon团队合作构建Binius-based zkVM; JoltzkVM正从Lasso转向Binius,以改进其递归性能;以及 Ingonyama团队正在实现FPGA版本的Binius.
与基于椭圆曲线的SNARKs不同,STARKs可以看作是基于哈希的SNARKs。目前STARKs效率低下的一个主要原因是,实际程序中的大部分值相对较小,比如for循环中的索引、布尔值和计数器。然而,为了确保Merkle树证明的安全性,采用Reed-Solomon编码对数据进行扩展,这导致了大量冗余值占用整个域,尽管原始值很小。为了解决这个效率问题,减少域的大小已成为关键策略。
如表1所示,第1代STARKs编码位宽为252bit,第2代STARKs编码位宽为64bit,第3代STARKs编码位宽为32bit,但32bit编码位宽仍然存在大量的浪费空间。相较而言,二进制域允许直接对位进行操作,编码紧凑高效而无任意浪费空间,即第4代STARKs。
表 1:STARKs 推导路径
与近期受到关注的有限域(如Goldilocks、BabyBear和Mersenne31)相比,二进制域的研究可以追溯到1980年代。如今,二进制域在密码学中被广泛应用,主要包括以下几个例子:
在使用较小的域时,域扩展操作对确保安全性变得尤为重要。Binius所采用的二进制域完全依赖于域扩展,以保证安全性和实用性。大多数与Prover操作相关的多项式计算无需进入扩展域,只需在基域中进行操作,从而在小域中实现高效率。然而,随机点检查和FRI计算仍需在更大的扩展域中进行,以确保必要的安全级别。
在基于二进制域构建证明系统时,有两个实际挑战:首先,STARKs中用于轨迹表示的域大小必须大于多项式的度数;其次,STARKs中用于Merkle树承诺的域大小需大于经过Reed-Solomon编码扩展后的大小。
Binius通过两种不同的方式来解决这两个问题,提供了一种创新的解决方案:首先,使用多变量(特别是多线性)多项式代替单变量多项式,通过在“超立方体”上的评估来表示整个计算轨迹;其次,由于超立方体的每个维度长度为2,无法像STARKs那样进行标准的Reed-Solomon扩展,但可以将超立方体视为一个正方形,并基于这个正方形进行Reed-Solomon扩展。这种方法不仅确保了安全性,还大幅提升了编码效率和计算性能。
现代大多数SNARK系统的构建通常包含两个主要组件:
通过选择不同的PIOP和PCS方案,并将它们与适当的有限域或椭圆曲线结合,可以构建具有不同特性的证明系统。例如:
在设计这些系统时,所选PIOP、PCS与有限域或椭圆曲线之间的兼容性对于确保系统的正确性、性能和安全性至关重要。这些组合会影响SNARK证明的大小、验证效率,并决定系统是否能够在没有可信设置的情况下实现透明性,以及是否支持递归证明或证明聚合等高级功能。
Binius结合了HyperPlonk PIOP与Brakedown PCS,并在二进制域中运作。具体来说,Binius结合了五项关键技术,以实现效率和安全性:
这些创新使Binius能够提供一个紧凑且高性能的SNARK系统,专为二进制域优化,同时保持强大的安全性和可扩展性。
塔式二进制域是实现快速可验证计算的关键,主要归因于两个方面:高效计算和高效算术化。二进制域本质上支持高度高效的算术操作,使其成为对性能要求敏感的密码学应用的理想选择。此外,二进制域结构支持简化的算术化过程,即在二进制域上执行的运算可以以紧凑且易于验证的代数形式表示。这些特性,加上能够通过塔结构充分利用其层次化的特性,使得二进制域特别适合于诸如Binius这样可扩展的证明系统。
图 1: 塔式二进制域
如图1所示,一个128位字符串:该字符串可以在二进制域的上下文中以多种方式进行解释。它可以被视为128位二进制域中的一个独特元素,或者被解析为两个64位塔域元素、四个32位塔域元素、16个8位塔域元素,或128个F2域元素。
这种表示的灵活性不需要任何计算开销,只是对位字符串的类型转换(typecast),是一个非常有趣且有用的属性。同时,小域元素可以被打包为更大的域元素而不需要额外的计算开销。
Binius协议利用了这一特性,以提高计算效率。此外,论文《On Efficient Inversion in Tower Fields of Characteristic Two》探讨了在n位塔式二进制域中(可分解为m位子域)进行乘法、平方和求逆运算的计算复杂度。
Binius协议中的PIOP设计借鉴了HyperPlonk,采用了一系列核心检查机制,用于验证多项式和多变量集合的正确性。这些核心检查包括:
尽管Binius与HyperPlonk在协议设计上有许多相似之处,但Binius在以下3个方面做出改进:
因此,Binius通过对现有PIOPSumCheck机制的改进,提升了协议的灵活性和效率,尤其在处理更复杂的多变量多项式验证时,提供了更强的功能支持。这些改进不仅解决了HyperPlonk中的局限性,还为未来基于二进制域的证明系统奠定了基础。
在Binius协议中,虚拟多项式的构造和处理是关键技术之一,能够有效地生成和操作从输入句柄或其他虚拟多项式派生出的多项式。以下是两个关键方法:
Lasso协议允许证明方承诺一个向量a ∈ Fm,并证明其所有元素均存在于一个预先指定的表t ∈ Fn 中。Lasso解锁了“查找奇点”(lookup singularities)的概念,并能适用于多线性多项式承诺方案。其效率体现在以下两个方面:
Lasso协议由以下三个组件构成:
Binius协议将Lasso适应于二进制域的操作,假设当前域是一个大特征的素数域(远大于被查找列的长度)。Binius引入了乘法版本的Lasso协议,要求证明方和验证方联合递增协议的“内存计数”操作,不是通过简单的加1递增,而是通过二进制域中的乘法生成元来递增。然而,这一乘法改编引入了更多的复杂性,与递增操作不同,乘法生成元并非在所有情况下递增,在0处存在单一轨道,这可能成为攻击点。为防止这种潜在的攻击,证明方必须承诺一个处处非零的读取计数向量,以确保协议的安全性。
构建BiniusPCS的核心思想是packing。Binius论文中提供了2种基于二进制域的Brakedown多项式承诺方案:一种是采用concatenated code来实例化;另一种采用block-level encoding技术,支持单独使用Reed-Solomon codes。第二种Brakedown PCS方案,简化了证明和验证流程,但proof size要比第一种略大一点,但所带来的简化和实现优势,做该取舍是值得的。
Binius多项式承诺主要使用小域多项式承诺与扩展域评估、小域通用构造和块级编码与Reed-Solomon码技术。
小域多项式承诺与扩展域评估:Binius协议中的承诺是在小域K上的多项式承诺,并在更大的扩展域L/K中进行评估。这种方法确保了每个多线性多项式t(X0,…,Xℓ−1)属于域K[X0,…,Xℓ−1],而评估点可以位于更大扩展域L中。承诺方案专门设计用于小域多项式,并能在扩展域上进行查询,同时保证承诺的安全性和效率。
小域通用构造:小域通用构造通过定义参数ℓ、域K及其相关的线性块码C,确保扩展域L足够大,以支持安全评估。为了在保持计算效率的同时提高安全性,协议通过扩展域的特性,以及采用线性块码对多项式进行编码,保证了承诺的稳健性。
块级编码与Reed-Solomon码:针对字段比线性块码字母表更小的多项式,Binius提出了块级编码方案。通过这一方案,即使在小域(如F2)中定义的多项式,也可以使用如F216这样的大字母表的Reed-Solomon码高效承诺。Reed-Solomon码之所以被选中,是因为它具有高效性和最大距离分离特性。该方案通过将消息打包并逐行编码,之后利用Merkle树进行承诺,简化了操作复杂度。块级编码允许小域多项式的高效承诺,而不会产生通常与大域相关的高计算开销,从而使得在F2等小域中承诺多项式成为可能,并在生成证明与验证中保持计算效率。
为了进一步提升Binius协议的性能,本文提出了四个关键优化点:
Binius论文引入一种基于lookup的方案,旨在实现高效的二进制域乘法运算。通过Lasso lookup argument 改编的二进制域乘法算法依赖于lookups和加法操作的线性关系,这些操作与单个word中的limbs数量成比例。虽然这一算法在某种程度上优化了乘法操作,但仍需要与limbs数量线性相关的辅助承诺。
GKR(Goldwasser-Kalai-Rothblum)协议中的核心思想是,证明方(P)和验证方(V)针对一个有限域F上的layered算术电路达成一致。该电路的每个节点有两个输入,用于计算所需的函数。为了减少验证方的计算复杂度,协议使用SumCheck协议,将关于电路输出门值的声明逐步简化为更低层的门值声明,直至最终将声明简化到关于输入的陈述。这样,验证方只需检查电路输入的正确性即可。
基于GKR的整数乘法运算算法,通过将“检查2个32-bit整数A和B是否满足 A·B =? C”,转换为“检查中(gA)B =? gC 是否成立”,借助GKR协议大幅减少承诺开销。与之前的Binius lookup方案相比,基于GKR的二进制域乘法运算只需一个辅助承诺,并且通过减少Sumchecks的开销,使该算法更加高效,特别是在Sumchecks操作比承诺生成更便宜的场景下。随着Binius优化的推进,基于GKR的乘法运算逐渐成为减少二进制域多项式承诺开销的有效途径。
论文《Some Improvements for the PIOP for ZeroCheck》在证明方(P)和验证方(V)之间调整工作量的分配,提出了多种优化方案,以权衡开销。该工作探索了不同的k值配置,使得在证明方和验证方之间达成了成本的权衡,特别是在减少传输数据和降低计算复杂性方面。
减少证明方的数据传输:通过将一部分工作转移给验证方V,从而降低证明方P发送的数据量。在第i轮中,证明方P需要向验证方V发送vi+1(X),其中X=0,…,d + 1。验证方V检查以下等式以验证数据的正确性:
vi = vi+1(0) + vi+1(1).
优化方法:证明方P可以选择不发送vi+1(1),而是让验证方V自行通过以下方式计算出该值
vi+1(1) = vi − vi+1(0).
此外,在第0轮,诚实的证明方P始终发送v1(0) = v1(1) = 0,这意味着无需进行任何评估计算,从而显著减少了计算和传输成本,降低至d2n−1CF + (d + 1)2n−1CG。
减少证明方评估点的数量:在协议的第i轮中,验证者在之前的i轮中已经发送了一个值序列r =(r0,…,ri−1)。当前协议要求证明者 (P) 发送多项式
vi+1(X) = ∑ δˆn(α,(r,X,x))C(r,X,x).x∈H −−1
优化方法:证明方P发送以下多项式这两个函数之间的关系是:
vi(X) = vi′(X)·δi+1((α0,…,αi),(r,X))
其中δˆi+1因为验证者拥有α和r,所以是完全已知的。这个修改的好处在于vi′(X)的次数比vi(X)少1,这意味着证明者需要评估的点更少。因此,主要的协议变化发生在轮次之间的检查环节。
此外,将原本的约束vi = vi+1(0)+vi+1(1) 优化为 (1−αi)vi′+1(0)+αivi′+1(1) = vi′(X)。则证明者需要评估和发送的数据更少,进一步减少传输的数据量。计算δˆn−i−1也比计算δˆn更高效。通过这两项改进,成本降低为大约:2n−1(d− 1)CF + 2n−1dCG。在常见的d=3情况下,这些优化使成本降低了5/3倍。
代数插值优化:对于诚实的证明者,C(x0,…,xn−1)在Hn上为零,可表示为:C(x0,…,xn-1)= ∑xi(xi-1)Qi(x0,…,xn-1)。虽然Qi不是唯一的,但可以通过多项式长除法构造一个有序的分解:从Rn=C开始,逐次除以xi(xi−1)来计算Qi和Ri,其中R0是C在Hn上的多线性扩展,且假设其为零。分析Qi的次数,可以得出:对于j> i,Qj 在 xi 上的次数与 C 相同;对于 j = i,次数减少 2;对于 j i,次数至多为 1。给定向量 r = (r0,…,ri),Qj(r,X) 对于所有 j ≤ i 都是多线性的。此外1)Qj(r,X) 是与 C(r,X) 在 Hn−i 上相等的唯一多线性多项式。对于任何 X 和 x ∈ Hn−i−1,可以表示为:
C(r,X,x) − Qi(r,X,x) = X(X − 1)Qi+1(r,X,x)
因此,在协议的每一轮中,仅引入一个新的Q,其评估值可以从C和先前的Q计算得出,实现插值优化。
Binius所实现的STARKs方案,其承诺开销很低,使得prover瓶颈不再是PCS,而在于sum-check协议。
图 2. 切换轮次与因子改进之间的关系
Ingonyama在2024年提出了针对基于小域的Sumcheck协议的改进方案(对应图2中的Algo3和Algo4算法),并开源了实现代码。算法4专注于将Karatsub算法合并到算法3中,以额外的基域乘法为代价来最小化扩域乘法次数,因此当扩域乘法比基域乘法昂贵得多时,算法4的性能会更好。
基于小域的Sumcheck协议的改进集中于切换轮次t的选择。切换轮次是指从优化算法切换回朴素算法的时间点,论文的实验表明,在最佳切换点时,改进因子达到最大值,随后呈现抛物线趋势。如果超过这一切换点,优化算法的性能优势减弱,效率下降。这是由于小域上的基域乘法与扩域乘法相比有更高的时间比率,因此在适当时机切换回朴素算法至关重要。
对于具体应用,如涉及Cubic Sumcheck(d = 3)的情况,基于小域的Sumcheck协议相较于朴素算法的改进达到了一个数量级。例如,在基域为GF[2]的情况下,算法4的性能比朴素算法高出近30倍。
论文的实验结果表明,较小的基域(如GF[2])能够使优化算法显示出更显著的优势。这是因为扩展域与基域乘法的时间比率在较小基域上更高,从而优化算法在此条件下表现出更高的改进因子。
Karatsuba算法在提升基于小域的Sumcheck性能方面表现出显著的效果。对于基域GF[2],算法3和算法4的峰值改进因子分别为6和30,表明算法4比算法3高效五倍。Karatsuba优化不仅提升了运行效率,也优化了算法的切换点,分别在算法3的t=5和算法4的t=8达到最佳。
基于小域的Sumcheck协议除了提升运行时间,还在内存效率方面表现出显著的优势。算法4的内存需求为O(d·t),而算法3的内存需求为O(2d·t)。当t=8时,算法4仅需0.26MB的内存,而算法3则需67MB来存储基域的乘积。这使得算法4在内存受限设备上表现出更强的适应性,尤其适用于资源有限的客户端证明环境。
Binius协议的一个主要缺陷在于其相对较大的证明大小,随着见证大小的平方根按O(√N)缩放。与更高效的系统相比,这种平方根大小的证明是一种局限性。相反,对数级(polylogarithmic)证明大小对于实现真正“简洁”的验证器至关重要,这在像Plonky3这样的先进系统中得到了验证,后者通过FRI等先进技术实现了对数级证明。
论文《Polylogarithmic Proofs for Multilinears over Binary Towers》,简称为FRI-Binius,实现了二进制域FRI折叠机制,带来4个方面的创新:
基于二进制域FRI-Binius的多线性多项式承诺方案(PCS)的核心思想为:FRI-Binius协议通过将初始的二进制域多线性多项式(定义于F2上)打包为定义在更大域K上的多线性多项式来操作。
在基于二进制域的FRI-BiniusPCS中,过程如下:
借助FRI-Binius,可将Binius证明大小减少一个数量级。这使得Binius的证明大小更加接近最先进的系统,同时保持与二进制域的兼容性。专为二进制域定制的FRI折叠技术,加上代数打包和SumCheck的优化,使得Binius能够在保持高效验证的同时,生成更加简洁的证明。
表 2:Binius 与 FRI-Binius 证明大小比较
表 3:Plonky3 FRI 与 FRI-Binius 比较
Binius的整个价值主张是,可为witnesses使用最小的power-of-two域,因此只需根据所需来选择域大小。Binius是“使用硬件、软件、与FPGA中加速的Sumcheck协议”的协同设计方案,可以以非常低的内存使用率来快速证明。Halo2和Plonky3等证明系统有4个占用大部分计算量的关键步骤:生成witness数据、对witness数据进行承诺、vanishingargument、openingproof。以Plonky3中的Keccak和Binius中的Grøstl哈希函数为例,二者对应的以上4大关键步骤计算量占比情况如图3所示:
图 3. 较小的承诺成本
由此可知,Binius中已基本完全移除了Prover的commit承诺瓶颈,新的瓶颈在于Sumcheck协议,而Sumcheck协议中大量多项式evaluations和域乘法等问题,可借助专用硬件高效解决。FRI-Binius方案,为FRI变体,可提供一个非常有吸引力的选择——从域证明层中消除嵌入开销,而不会导致聚合证明层的成本激增。当前,Irreducible团队正在开发其递归层,并 宣布与Polygon团队合作构建Binius-based zkVM; JoltzkVM正从Lasso转向Binius,以改进其递归性能;以及 Ingonyama团队正在实现FPGA版本的Binius.