理解 PLONK(七):Lookup Gate

传统上我们通过编写算术电路来表达逻辑或者计算。而算术电路只有两种基本门:「加法门」与「乘法门」。当然通过组合,我们可以基于加法和乘法构造复杂一点的元件(Gadget)来复用,但是在电路处理过程中,这些 Gadget 还是会被展开成加法门和乘法门的组合。

自然我们想问:能否使用除加法和乘法之外的「新计算门」?

Plonk 相关的工作给出了一个令人兴奋的扩展:我们有能力构造出更复杂些的基本计算单元。如果一个计算的输入和输出满足一个预先设定的多项式的话,那么这个计算可以作为基本计算单元,这个改进被称为 「Custom Gate」,实际上你可以理解为这是一种多输入的「多项式门」。

故事还没有结束,论文 GW20 又给出了一个制造「Lookup Gate」的方法。这个门的输入输出没有必要局限于多项式关系,而是可以表达「任意的预定义关系」。What? 任意的关系?是的,你没听错,尽管这有点令人难以置信。

思路不难理解:如果我们在电路之外预设一个表格,表中每一行表示特定计算的输入输出关系,例如:

in1in2in3out
1234
5678
1159

这个表格就代表一个 Lookup 门的定义。如果你问我这个门究竟表达了什么计算,我无法回答(乱写的)。不过只要能给出这样一张表格,我们就可以在电路里面接入一个门,它的输入输出关系「存在于表中的某一行」。

这种门被称为 Lookup Gate,即查表门(或查表约束)。

如果当我们在 Plonk 电路中接入查表门,那么 Plonk 协议就要检查这个门的输入输出是否合法,然后就会去查我们实现预设的表格,看看其输入输出关系是否能在表中找到对应的一行。如果表中存在这样的条目,那么这个门就合法,否则被视为非法。

在现实应用中,最多采用查表方式的门是关于位运算。如一个 8-bit 异或运算,只需要 大小的表格即可。此外对于采用大量位运算的 SHA256算法,也可以通过建立一个 Spread Table 来大大加速各种位运算的效率。

基本思路

实现查表门的一个关键技术是 Lookup Argument 协议,即如何证明一条(或多条)记录是否存在于一个公开的表中。

可能有朋友会条件反射想到 Merkle Tree,如果我们把表格按行计算 hash,这些 hash 就可以产生一个 Merkle Root,然后通过 Merkle Path 就能证明一条记录是否存在表格中。但是这个方法(以及所有的 Vector Commitment 方案)不适合查表场景。原因有两个,一是这种方案会暴露记录在表格中的位置。假如 Prover 想隐藏记录的信息,即在查询证明不暴露位置,那么仅 Merkle Tree 就难以胜任了。理论点说,这里我们需要 Set-Membership Argument,而非 Vector-Membership Argument。第二个原因:如果有大量的记录条目(比如条目数量为 )需要查表,那么所产生的证明即 Merkle Path,可能会比较大,最坏情况是

简而言之,我们需要一种新的,并且高效的查表协议。本文介绍两个常见的查表协议,为了简化表述,我们先只考虑单列表格的查询,然后再扩展到多列表格的情况。

Halo2-lookup 方案

基于 Permutation Argument,Halo2 给出了一个简洁易懂的 Lookup Argument 方案。

假如我们有一个表格向量 ,表格中不存在相同元素。然后有一个查询向量 ,我们接下来要证明 ,请注意 中会有重复元素。

我们引入一个关键的辅助向量 ,它是 的一个重新排序(置换),使得 中的所有查询记录都按照 的顺序进行排序,比如 ,那么重排后,

可以看出, 中的重复元素被放在了一起,并且整体上按照 中元素出现的顺序。我们把 中连续重复元素的第一个标记出来:

我们再引入一个辅助向量 ,它是对 的重新排序,使得 中被标记元素可以正好对应到 中相同位置上的元素:

请注意看 ,其中被方框标记的元素和 中相同位置的方框元素值完全相同,未被标记的元素则没有出现在 中。

于是我们可以找出一个规律: 中的每一个未标记元素等于它左边的相邻元素,而每一个被标记元素等于 同位置元素,即 或者

将两个向量 与重排向量 通过 Lagrange Basis 进行多项式编码,我们得到 , , ,他们会满足下面的等式:

但上面这个等式不足以约束重排向量的可靠性。考虑如果 ,也会满足上面的等式,但是 并不是合法的查询记录。因此,我们还要加入一条约束防止出现 上 循环回卷导致的漏洞:要求 两个向量的第一个元素必须相同, 即 ,用多项式约束表达如下:

剩下的工作是证明 满足某一个「置换」关系,且 也满足某个「置换」关系。由于,这两个置换关系只不需要约束具体的置换向量,因此我们可以直接采用 Grand Product Argument 来约束这两个置换关系:

下面重新整理下这个协议

协议框架

公共输入:表格向量

秘密输入:查询向量

预处理:Prover 和 Verifier 构造

第一步:Prover 构造多项式并发送承诺

第二步:Verifier 发送挑战数

第三步:Prover 构造多项式并发送承诺

第四步:Verififer 发送挑战数

第五步:Prover 计算并发送商多项式

第六步:Verifier 发送挑战数

第七步:Prover 发送 ,并附带上 evaluation proofs(略去)

第八步:Verifier 验证(注意这里为了简化,去掉了KZG10的聚合优化和线性化优化)

Plookup 方案

然后我们再看看论文 GW20 给出的方案 —— Plookup。与 Halo2-lookup 相比,Plookup 可以省去 向量。

重申一下 Plookup 证明的场景:Verifier 已知表格 向量,Prover 拥有一个秘密的查询向量 ,Prover 要证明 中的每一个元素都在 中,即

方案 Plookup 只需要引入一个辅助向量 ,它被定义为 上的重排,且向量元素的排列遵照 中各个元素出现的顺序。

举例说明,假设 ,如果 ,那么 。可以看到,和 Halo2-lookup 中的 一样, 中相等的元素被排在了一起。

如果向量 满足 ,并且 ,那么就可以证明

第一个关键点是因为 中的查询记录是任意的,查询顺序并没有遵守 中的元素顺序。而通过辅助向量 ,我们就可以把 的查询记录进行重新排序,这有利于排查 中元素的合法性,确保每一个 都出现在 中。但如何保证由 Prover 构造的 是按照 的元素顺序进行排序的?Plookup 用了一个直接但巧妙的方法,考虑把 中的每一个元素和他相邻下一个元素绑在一起,然后可以构成一个新的 Multiset;同样,我们把 中的每一个元素与相邻下一个元素组成一个元组,并构成一个 Multiset;我们还要把 中的每一个元素和它自身构成一个二元组 Multiset。我们用 来表示这三个新的 Multiset,并证明它们满足一定的关系,从而保证 排序的正确性。

这个方法与 Permutation Argument 的基本思想非常类似。回忆下,我们在 Permutation Argument 中,利用了 绑定元素和其位置的「二元组」的 Multiset 来保证任一个 都会出现在位置 上;通过与另一个二元组 Multiset 的相等,可以证明 满足置换函数 。比如下面这个置换函数为奇偶互换的例子:

假设两个向量 ,如果它们满足上面的 Multiset 相等关系,我们可以知 ,满足奇偶互换的关系。

另一个关键点是如何保证 中的元素都在 中出现?这个问题被归结到一个新问题,即 中那些相邻的重复元素一定来自于 ,假如 中有 个重复元素,那么我们可以要求其中第一个来自于 ,剩下的 个元素来自于 。如果 中一旦出现了一个不在 中的元素(假设为 ),那么因为 的重排,那么 中一定会出现 (假设 ),这时在 中一定会出现 这样两个元素,它们无法出现在 这个 Multiset中,也不会出现在 中。

举几个例子,假设 的长度为 , 如果 ,那么 向量在各个位置上都相等。

假设增加一条查询记录,即 ,那么 ,这时候 只有唯一的表达,

假设 为不出现在 中的元素,那么 一定没有办法塞入到 S 中,因为在 中,和 相邻的元素 。因此

假设 ,那么 也只有唯一的表达, ,同样可以检验:

更形式化一些,我们可以用数学归纳法推导:先从 为空开始推理, 。这样我们只要检查 满足 Multiset 意义上的相等,就可以满足 ,且

现在看归纳步,假设 ,如果我们在 中添加一个新元素 ,且 ,那么在 中会比 额外多一个元素 。因为 ,那么重排向量 中一定包含了相邻的两个 ,其中一个来自 ,另一个来自于 。因此,我们可以得出结论:

另一种情况, 假设 ,如果我们在 添加的新元素 ,即是一条违法查询,假设为 。那么 中存在与 相邻的两个元素, ,即 。它们构成了 中的两个异类元素 ,导致

到此为止,我们已经可以确信,通过验证 相等就可以判定 是正确的重排,并且 中的每一个元素都出现在 中。接下来我们把这个问题转换成多项式之间的约束关系。

首先 Prover 借助 Verifier 提供的挑战数 ,把 中的每一个二元组元素进行「折叠」,转换成单值。这样新约束等式为:

然后 Prover 再借助 Verifier 提供的一个挑战数 ,把上面的 Multiset Equality Argument 归结到 Grand Product Argument:

不过这里请注意的是,在 Plookup 论文方案中,并没有采用上面的证明转换形式。而是调换了 的使用顺序:

归结后的 Grand Product 约束等式为:

注:个人认为,上述两种证明转换形式没有本质上的区别。为了方便理解论文,我们后文遵从 Plookup 原论文的方式。

接下来,我们要对向量进行多项式编码,但是这里会遇到一个新问题。即 多项式的次数会超出 的次数或 的次数,特别当 的长度接近或者等于 的大小, 的次数可能超出 的大小。Plookup 的解决方式是将 拆成两半, ,但是 的最后一个元素要等于 的第一个元素:

这样做的目的是,确保能在两个向量中描述 中相邻两个元素的绑定关系。比如 ,那么 ,而 ,可以看出他们头尾相接。

这样一来, 的长度最长也只能是 ,但如果 要按照 对齐,那么 的长度就不够了(无法在长度为 的乘法子群上编码成多项式)。为了解决这个问题,Plookup 选择把 的有效长度限制在 ,所谓有效长度是指, 的实际长度为 ,但是其最后一条查询记录并不考虑其合法性。

于是 向量可以拆成两个长度为 的向量,其中一半 ,另一半

接下来 Prover 要引入 Accumulator 辅助向量 来证明 Grand Product:

我们仍然看下这样一个例子: ,于是 ,拆成两个头尾相接的向量: 。那么,我们可以把相邻元素构成的二元组向量写出来:

\begin{split} F &= (f_i, f_i) & = & {(2,2), (4,4), (4,4)}\ T &=(t_i, t_i) & = & {(1,2), (2,3), (3,4)}\ S^{lo} &= (s^{lo}_i, s^{lo}_i) & = & {(1,2), (2,2), (2,3)}\ S^{hi} &= (s^{hi}_i, s^{hi}_i) & = & {(3,4), (4,4), (4,4)}\ \end{split}

容易检验,他们满足下面的关系:

于是,利用一个辅助函数 ,我们定义

进行编码,我们可以得到 多项式,它应该满足下面三条约束:

此外,根据 的递推关系, 还要满足下面的约束:

总共有四条多项式约束,这里略去完整的协议。

Plonkup 的优化

在论文 Plonkup 论文中给出了一个简化方法,可以去除一个多项式约束。在 Plookup 方案中, 向量被拆分成两个向量, ,但要要求这两个向量头尾相接。

Plonkup 给出了一种新的拆分方案,即按照 的奇偶项进行拆分,拆成

注意,这里不再需要限制 的长度为 ,而是可以到 ,这样 的长度可以到 ,拆分成两个长度为 的向量,之所以可以去除这个限制,是因为 之间的关系可以在 回卷到起始位置,这样只需要要求 即可。 向量可以重新定义为:

我们可以举一个简单的例子:假设 ,于是

容易检验,他们满足下面的关系:

我们也可以通过定义 ,并仔细检查每一项,确认只需要约束 就可以约束 的正确性。

这里辅助函数

于是多项式 只需要满足如下两条约束:

还有

多列表格与多表格扩展

通常查询表是一个多列的表,比如一个 8bit-XOR 计算表是一个三列的表。对于 Plookup 方案与 Halo2-lookup 方案,我们直接可以通过随机挑战数来把一个多列表格折叠成一个单列表格。

假如计算表格为 ,那么相应的查询记录也应该是个三列的表格,记为 。如果 ,对所有的 都成立,那么 是一个合法的查询记录。 通过向 Verifier 要一个随机挑战数 ,我们可以把计算表格横向折叠起来:

同样,Prover 在证明过程中,也将查询记录横向折叠起来:

接下来,Prover 和 Verifier 可以利用单列表格查询协议( Plookup 协议或 Halo2-lookup 协议)完成证明过程。

如果存在多张不同的表格,那么可以给这些表格增加公开的一列,用来标记表格编号,这样可以把多表格视为增加一列的多列的单一表格。

与 Plonk 协议的整合

由于计算表格 是一个预定义的多列表格,因此它可以在 Preprocessing 阶段进行承诺计算,并把这些表格的承诺作为后续协议交互的公开输入。

在 Plonk 协议中,因为我们把表格的查询视为一种特殊的门,因此查询记录 本质上正是 的折叠。为了区分「查询门」和「算术门」,我们还需要增加一个选择向量 ,标记 Witness table 中的某一行是算术门,还是查询门。

下面我们按照 Plonkup 论文中的协议,大概描述下如何将 Lookup Argument 整合进 Plonk 协议。

预处理:Prover 和 Verifier 构造

第一步:Prover 针对 表格的每一列,构造 使得

第二步:Verifier 发送随机数 ,用以折叠表格

第三步:Prover 构造并发送 ,分别编码 ,其中 计算如下

这里请注意,当 时,表示这一行约束不是查询门,因此需要填充上一个存在 中的值,这里我们取表格的最后一个元素作为查询记录填充。

Prover 计算 ,并拆分为 ,构造并发送

第四步: Verifier 发送随机数

第五步:Prover 构造(并发送)拷贝约束累乘多项式 ,使得

其中

Prover 构造(并发送)查询累乘多项式 ,使得:

其中

第六步:Verifier 发送随机挑战数

第七步:Prover 计算 ,并构造商多项式

后续步:Verifier 发送随机挑战数 ,Prover 打开各个多项式,Verifier 自行计算 ,并验证各个多项式在 处的计算证明,并验证这些打开点满足上面等式。

完整的协议请参考Plonkup论文 [2]。

Reference

  • [1] Ariel Gabizo, Dmitry Khovratovich. flookup: Fractional decomposition-based lookups in quasi-linear time independent of table size. https://eprint.iacr.org/2022/1447.

  • [2] Luke Pearson, Joshua Fitzgerald, Héctor Masip, Marta Bellés-Muñoz, and Jose Luis Muñoz-Tapia. PlonKup: Reconciling PlonK with plookup. https://eprint.iacr.org/2022/086.

  • [3] https://zcash.github.io/halo2/design/proving-system/lookup.html

  • [4] Ariel Gabizon. Multiset checks in PLONK and Plookup. https://hackmd.io/@arielg/ByFgSDA7D

  • [5] Modified Lookup Argument (improved). https://hackmd.io/_Q8YR_JLTvefW3kK92KOFgv