TL;DR

在上一篇文章Hello, OlaVM!中提到,OlaVM的愿景是建立一个高性能的ZKVM,本文将重点介绍使得OlaVM获得高性能的工具之一,Lookup argument。Lookup argument对缩减电路规模,以提高ZK效率有很重要的作用,在ZKVM的电路设计中被广泛应用,通过本篇文章你可以了解到:

1.Lookup argument在ZKVM中将发挥着怎样的作用?

2.Plookup协议原理。

3.Halo2的Lookup argument协议原理。

4.两个Lookup argument算法之间的联系。

The roles in ZKVM

所谓的ZKVM,其实就是用ZK约束VM所有的执行过程,VM的执行过程一般可以分为:指令执行,内存访问,内置函数执行等。在一个trace里执行对这些操作的约束看起来有点不切实际,首先,不同操作类型的约束对应不同的trace的宽度,如果其中一个约束对应的trace宽度特别大,就会造成其余约束对应trace的浪费;然后,一个trace里有太多不同的操作类型,就会引入更多的selector,不仅会增加多项式的个数,而且还会增加约束的阶;最后,由于群的阶限制,trace的行数不能超过这个群的阶,因此,应该尽量减少某种类型的操作所占用的trace行数。

因此,为了简单,我们需要:

a.把不同的操作类型分成多个子trace,然后分别证明,主trace和子trace之间需要通过Lookup argument来保证数据的一致性。

b.对于一些ZK-unfriendly计算,我们可以通过Lookup argument技术来缩减trace的规模,比如位运算等。

当然,也有其他的一些技术手段来减少trace规模,我们将在后面的文章中给予说明。

Lookup between trace tables

VM所有的执行过程会组成一个完整的trace,称为主trace,这里的完整是包含VM执行的所有状态,不会涉及到辅助状态,比如,方便ZK验证的一些扩展信息等;如前面所述,在主trace里面包含这种辅助信息,会使得主trace变得复杂,难于约束。因此,为了约束方便,通常会建立一些子trace,然后分别针对这些子trace进行约束,而主trace主要用来进行执行正确的程序约束和Context约束。

一文了解 Lookup Arguments

图片1. Lookup between traces

通过建立不同的子trace,我们把VM执行的不同操作进行划分,通过Lookup argument技术来保证了子trace的数据源于主trace。对于子trace里的数据有效性证明,需要根据具体的操作类型,生成不同的trace,然后用对应的约束去证明trace的有效性;特别是对于bitwise,rangcheck等zk-unfriendly操作。

Lookup for ZK-unfriendly operations

如前面所述,每个子trace的证明是独立的,所以获得一个尽可能小的trace,会提高 prover的效率。以bitwise为例,bitwise操作包含AND, XOR, NOT三种操作。如果想通过电路单纯的实现对bitwise操作的约束,那需要做的可能是,把每个op拆成多个2进制的limbs,如果这些op是32bit位宽,那就会拆分成32个limbs。然后,你需要约束:

一文了解 Lookup Arguments

总共占用3 + 32 * 3 = 99个trace cell,约束个数为3次sumcheck + 32次bitwise = 35个。

如果这个时候有一些真值表,对于AND, XOR, NOT计算,你可以定义三个表,这些表里存的是指定位宽的op进行bitwise计算的数据,比如8bit。对于32bit的op,只需要把它们拆分成4个8bit的limbs,然后这些op的limbs之间的bitwise关系,也不用对应的约束去实现,只需要在fixed table里进行Lookup即可,此时,总共占用了 3+ 4 * 3 = 15个trace cell, 约束个数为3次sumcheck + 1 次Lookup argument(支持Batch Looup)。

一文了解 Lookup Arguments

图2. Lookup in Arithmetic operations

Lookup argument不仅对bitwise操作的证明有极大的提升作用,对于rangeck操作同样。对于32bit的op,只需要把他拆分成2个16bit的limbs即可;这里有两个很好的设计,一个是会使得rangecheck占用更少的trace cells;另外一个是rangcheck的sum约束可以复用我们自定义的ADD-MUL约束。对于不同的计算类型,能够复用同一个约束,对整体的效率提升具有很大的帮助,如上图所示,对于自定义的ADD-MUL gate,它可以支持ADD,MUL,ADD-MUL,EQ,RANGECHECK五种计算类型的约束复用。

Plookup协议

介绍

一文了解 Lookup Arguments

符号说明

一文了解 Lookup Arguments

 

预处理

一文了解 Lookup Arguments 协议过程

一文了解 Lookup Arguments

协议理解

一文了解 Lookup Arguments

一文了解 Lookup Arguments

一文了解 Lookup Arguments

一文了解 Lookup Arguments

Halo 2 Lookup 协议

介绍

一文了解 Lookup Arguments

协议过程

一文了解 Lookup Arguments

支持ZK

一文了解 Lookup Arguments

Extend - 1 : Vector Lookup

一文了解 Lookup Arguments

Extend - 2 : Multi-tables

一文了解 Lookup Arguments

Links between Plookup and Lookup

Plookup协议与Halo2的lookup协议都能证明 f⊂t ,但两个协议的思想是不同的,区别如下:

Plookup需要使用 f 和 t 构建一个新的数列 s , f 和 t 中的元素都在 s 中至少出现一次,接着通过比较 s 和 t 中元素的非零距离集合是相等的来证明 s⊂t,最终 f⊂s⊂t→f⊂t 。

Halo2的lookup直接证明 f⊂t ,不需要构建新的数列,比plookup更简洁。

Plookup和Halo2 lookup都需要对集合进行排序和补齐,plookup补齐后 |t|=|f|+1 ,Halo2 lookup补齐后 |t|=|f|=2^k。

参考

1.Hello, OlaVM!:https://hackmd.io/@sin7y/H1yPj_J8i

2.OlaVM:https://olavm.org/

3.Plookup协议:https://eprint.iacr.org/2020/315.pdf

4.Halo2的Lookup argument:https://zcash.github.io/halo2/design/proving-system/lookup.html