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 约束。

图片 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。然后，你需要约束：

• Sumcheck：所有 bit 位组合在一起等于原始 op,a=∑2ⁱlimb_a_i

• Bitwise check per bit：limb_a_i∗limb_b_i=limb_c_i

总共占用 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）。

图 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 协议

介绍

Plookup 是一个协议，作用是检查一个阶小于 n 的多项式 f∈F_<n[x]，在 n 阶乘法群 H 上的值包含在一个 d 维的表 F^d 中。一个典型的场景是 zk-snark 中做 rangecheck，校验所有多项式在 H 上的值都在[0, m]上。

符号说明

• H={g,...,gⁿ⁺¹}是 F 上一个 n+1 阶的乘法群，对于 f∈F[x] 来说，若 f_i=f(gⁱ),i∈[n+1]，那么可以用 f_i 表示 f(gⁱ) ，其中 [n+1]表示 {1,2,3...,n+1}。

• 向量 f∈Fⁿ ，也可以用多项式 f∈F_＜n[x] 来表示，其中 f(gⁱ)=f_i 。

• 给定两个向量 f∈Fⁿ， t∈F^d，用 f⊂t 表示 {f_i}_i∈[n]⊂{t_i}_i∈[d]。

预处理

• 假设 d=n+1

   a. 如果 d ≤ n ，把最后⼀个元素重复 n − d + 1 次。

   b. d 最多为 n + 1 ，因为群只有 n + 1 阶。

• 用多项式 t ∈ F_<n+1 [x]表示 lookup 的值

  a.  t 是 n + 1 个有限域元素的集合， t.degree() < n + 1 。

• 用 f ∈ F_<n [x]="" 表示输入的多项式

协议过程

• 用 s∈F2ⁿ⁺¹表示 (f,t) 合并之后的向量，然后用两个 F_＜n+1[X]上的多项式 h₁、h₂来表示：

h₁(gⁱ)=s_i,i∈[n+1]

h₂(gⁱ)=s_n+i,i∈[n+1]

s 中共有 2n+1 个元素， h₁表示 ，{s₁,s₂,...,s_n+1}，h2 表示 {s_n+1,s_n+2,....,s_2n+1}，即：

h₁(gⁿ⁺¹)=h₂(g)=s_n+1

• P 计算出 h₁、h₂并发送给可信第三方 I

• V 随机选择两个有限域 F 中的随机数 β、γ∈F 并发送给 P

• P 用和β和γ计算出一个多项式 Z∈F_<n+1[X]，定义如下：

  a. Z(g)=1

  b. 对 i∈[2,n]

  c. Z(gⁿ⁺¹)=1

• P 发送 Z 给 I

• V 检查 Z 的正确性，对每个 x∈H：

  a. L₁(x)(Z(x)−1)=0L_1(x)(Z(x)-1) = 0

  b.

  c. L_n+1(x)(h₁(x)-h₂(gx))=0

  d. L_n+1(x)(Z(x)−1)=0

• V 输出 acc 如果 6 中的等式都成立

协议理解

• 定义两个多项式 、F、G：

F(β,γ)=(1+β)ⁿΠ_i∈[n](γ+f_i)Π_i∈[d−1](γ(1+β)+t_i+βt_i+1)
G(β,γ)=Π_{i∈[n+d−1]}(γ(1+β)+s_i+βs_i+1)

其中 ，F≡G，d=n+1 ，当且仅当：

  a. f⊂t

  b. s 是 (f,t) 关于 t 的排序

此时将证明 f⊂t 转化为证明 F≡G ，即证明 s 是 (f,t) 的一个置换。

• P 在计算的 Z 是什么

• V 在校验什么

  a. V 检查 a 和 d 是验证 Z(g)=1 以及 Z(gⁿ⁺¹)=1

  b. V 检查 c 是验证 h₁(gⁿ⁺¹)=h₂(g) 。

  c. V 检查 b 是验证

Halo2 Lookup 协议

介绍

Halo2 的 look up 协议是对给定长度是 2^k 的两列数据 A 和 S ，证明 A 中的每个 cell 都在 S 中， S 中的一些 cell 可以不在 A 中，此外

• S 可以是固定的也可以是可变的。

  a. S 可变的情况是包含 trace 中的列，值不是固定的。

• A 和 S 可以包含重复数据，如果 A 和 S 不是 2^k 大小，则需要补齐到 2^k 。

  a. 把 A 用 S 中的一些数据补齐。

  b. 把 S 用最后一个数据补齐。

协议过程

• 令 H={1,w,w²,...,w^2k−1}

• P 计算 A 和 S 的置换 A′ 和 S′

  a. A′是 A 的一种排序，将相同的值放在相邻的 cell 上，不同值之间随机排。

  b. S′ 是 S 的一种排序， A′中不同值中的第一个 cell 要与 S′中在对应行的值相同，其他行随机。

  c. A′ 和 S′ 满足 A′_i=S′_i或者 A′_i=A′_i−1。

•  P 计算多项式 Z：

  a. 

  b. 

• V 校验 A′和 S′，对 H 上的每个 x 满足：

  a. (A′(X)−S′(X))(A′(X)−A′(w⁻¹X))=0

  b. L₀(X)(A′(X)−S′(X))=0

• V 校验 Z ，对 H 上的每个 x 满足：

  a. Z(wX)(A′(X)+β)(S′(X)+γ)−Z(X)(A(X)+β)(S(X)+γ)=0

  b. L0(X)(1−Z(X))=0

• V 输出 acc 如果 4 和 5 中的等式都成立。

疑问：协议只针对扩充后的 A , S 间的关系进行校验，那怎么保证对 S 是有效的扩充？
假如，A={1,2}，S={3,4}，两者不满足 subset argument，扩充后变为，A={1,2,3,4}，S={1,2,3,4}，可以通过 subset 论证，这是不合理的，却能证明通过？

支持 ZK

• 最后加 t 行随机数，只用前面 0～u=2^k−t−1 行存放数据

a. 第 u 行放 Z(x)。

• 多项式 q_blind把最后 t 行置为 1，其他为 0

• 多项式 q_last把第 u 行置为 1，其他都为 0，即最后一行数据 cell

• V 校验改成

 a. (1−(q_last(X)+q_blind(X)))(Z(wX)(A′(X)+β)(S′(X)+γ)−Z(X)(A(X)+β)(S(X)+γ))=0

 b. (1−(q_last(X)+q_blind(X)))(A′(X)−S′(X))(A′(X)−A′(w−1X))=0

为什么这里要加 q_blind(X)？第 u 行存储的是 Z(wx) ，不需要参与校验。

  a. L₀(X)(1−Z(X))=0

  b. L₀(X)(A′(X)−S′(X))=0

  c. q_last(X)(Z(X)²−Z(X))=0

Z(w^u) 可以是 1 或 0，因为可能出现 A_i+β=0 或 S_i+γ=0。

Extend - 1 : Vector Lookup

假设 P 有 ω个多项式 f₁,...,f_ω∈F_<n[X]和一个 d 行 ω列的数据表 t∗∈(F^ω)d^t ，现在要证明 ∀j∈[n],(f₁(g^j),...,f_ω(g^j))∈t∗，需要先将 {f_i}_i∈[ω]和 {t_i}_i∈[ω]转化为前面一列数据的情况。

• 对 t∗中 ω列数据计算出 ω个多项式，第 i 列多项式 ，ti∈F<d[X]，ti(gj)=ti,j∗,j∈[d]

• V 选择一个随机数 α 发送给 P

• P 重新计算需要 lookup 的多项式和数据

  a. f:=Σ_i∈ωαⁱf_i

  b. t:=Σ_i∈ωαⁱt_i

• P 和 V 使用 f 和 t 进行前面的 lookup 过程

Extend - 2 : Multi-tables

更进一步，假设 P 有多个数据表 t*₁,...,t*_l ，其中 t*_i∈(F^ω)^d/l对每个 i∈[n]要证明 j=j(i)∈[l] , (f₁(g^j),...,f_ω(g^j))∈t*_j，例如证明 witness 中的每一行数据都在某个数据表中。像 vector lookup 一样，要将这种情况转化为只有一个多项式和一列数据的情况。

• 将 t*₁,...,t*_l个表组成一个 t*∈(F^ω+1)^d，每个子表都增加一列拼接起来

对每个 ，j∈[l]，i∈[d/l]，t∗中都有一行元素 (j,(t*_j)i)

• 计算多项式 q∈F_<n[X]， q(gⁱ)=j(i)

• 使用 Vector lookup 证明 ，(q(gⁱ),f₁(gⁱ),...,f_ω(gⁱ))∈t*，i∈[n]

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.OlaVM：

https://olavm.org/

2.Plookup 协议：

https://eprint.iacr.org/2020/315.pdf

3.Halo2 的 Lookup argument：

https://zcash.github.io/halo2/design/proving-system/lookup.html