本文记录我对著名的 Quadratic Arithmetic Programs: from Zero to Hero | by Vitalik Buterin | Medium 的理解。但已经按照更容易理解的思路重写,并且增加了诸多更为深入的内容。

这篇文章会介绍如何将一个命题转换为电路(或者说分解到每个操作的子问题),然后构建 R1CS 约束系统(或者说一系列的等式约束),进一步转换为 QAP(或者说一个能同时实现这些约束的多项式),最后构建一个简单的证明系统。


引入

先理解我们要解决什么问题。

比如,你想证明对于一个很复杂的函数 ,当函数值为 时,你真的知道一个解是 . 并且这个问题计算需要花费大量的时间(得解一个复杂的方程,可能需要指数级别的时间),而验证这个问题只需要很快的时间(比如只需要对数级别的时间)。而你,需要给别人验证的机会,证明你知道答案并且你的答案是对的,但你不需要给出你答案

这种场景,零知识证明就会发挥作用。你就是 Prover,证明者,要证明你知道答案。别人会挑战你,和你交谈,从而确认你真的知道答案,这些人就是 Verifier。

实现零知识证明有很多方案,我们这次需要理解一种叫 QAP 的方法。

让我们用更有条理的方式梳理 QAP 方法:

以下输入给 Prover:

  • 一个需要证明的程序。一个命题。或者一个计算任务。反正都可以抽象为一个数学命题。
  • 一些证明过程用到的秘密。你不想泄露的知识。比如答案。

输出:

  • 证明。证明是一个数学对象,能够让 Verifier 验证你确实知道秘密,但不会泄露任何关于秘密的知识。换句话说,不会为 Verifier 自己计算出秘密降低任何一丝计算量。

然后这个输出再输入给 Verifier。

Verifier 输出:

  • 一个验证结果,接受或拒绝。

为了理解容易,以经典例题, 为例,看看如何零知识地证明 Prover 知道 是方程的解。这个过程会比较漫长,我会做最细致的分解,帮助自己,以及可能的读者理解,以及重理解。

从源程序到代数电路(Computation to Circuit)

输入:

def qeval(x):
    y = x**3
    return x + y + 5

输出:

一个“电路”。其实就是一种汇编语句,或者硬件描述语言。

sym_1 = x * x
y = sym_1 * x  
sym_2 = y + x  
~out = sym_2 + 5

它相当于把输入按照编译器编译的方式展平。这很好理解。这一步的目的就是把复杂的程序简单化,变成简单指令的集合。或者说分解为电路的简单连接。

从代数电路到一阶约束系统(Circuit to R1CS)

R1CS(Rank-1 Constraint System) 是由三个向量构成的向量组,分别是 。解向量 满足以下约束条件:,其中 表示向量内积, 表示算数乘法。 表示方程的

解。

电路虽然很简单了,但它却是线性执行的。所以我们为了提高验证效率,就必须把它转换成向量运算。所以 R1CS 出现的目的很明确,把电路的约束转换成上面这个向量运算约束。

这个转换必须不损失任何信息量。方法是这样的:

首先,把所有中间变量编号,从 0 开始。

变量名位置
~one0
x1
~out2
sym_13
y4
sym_25

其中这里我们引入一个虚拟变量(dummy variable)叫做 ~one,这样我们就可以表示 1.

然后就是构造向量 实际上,对于赋值语句 c = a op b,我们只需要把对应位置标 1,即可生成对应的向量

对于 sym_1 = x * x,第一个 x 对应位置是 1,得到对应向量 . 第二个也一样。

可以结合我画的图理解:

据此继续算出各个电路成分对应的向量:

sym_1 = x * x
a = [0, 1, 0, 0, 0, 0]  
b = [0, 1, 0, 0, 0, 0]  
c = [0, 0, 0, 1, 0, 0]

y = sym_1 * x  
a = [0, 0, 0, 1, 0, 0]  
b = [0, 1, 0, 0, 0, 0]  
c = [0, 0, 0, 0, 1, 0]

sym_2 = y + x  
a = [0, 1, 0, 0, 1, 0]  
b = [1, 0, 0, 0, 0, 0]  
c = [0, 0, 0, 0, 0, 1]


~out = sym_2 + 5
a = [5, 0, 0, 0, 0, 1]  
b = [1, 0, 0, 0, 0, 0]  
c = [0, 0, 1, 0, 0, 0]

如果你真的动手算了,就会发现 sym_2 = y + x 实际上要处理成 sym_2 = (y + x) * 1。这是因为约束必须是两个因式相乘,那么只能把 y + x 看作一个因式。这也就是引入 ~one 的原因。

最后就是 ,它是所有的变量值:

[1, 3, 35, 9, 27, 30]

计算过程是这样的,首先代入解 ,以及特殊值 ~one=1

变量名位置value
~one01
x13
~out2
sym_13
y4
sym_25

接下来,根据给定的规则计算并填充 “value” 列:

  1. sym_1 = x * x = 3 * 3 = 9
  2. y = sym_1 * x = 9 * 3 = 27
  3. sym_2 = y + x = 27 + 3 = 30
  4. ~out = sym_2 + 5 = 30 + 5 = 35

更新后的表格如下:

变量名位置value
~one01
x13
~out235
sym_139
y427
sym_2530

对应的向量就是

再加上矩阵 A:

矩阵 B:

矩阵 C:

对于矩阵的每一行 ,成立:

这就构成了 R1CS.

从 R1CS 到 QAP(R1CS to QAP)

下面这一步有一定跳跃性。我当时并不理解为什么要做,以及可以做这样的转换。下面是我思考后的答案:

R1CS 到 QAP 这一步,本质上就是把基于矩阵运算的约束,转换成关于多项式的约束。目的在于:

  1. 保持约束:这样的转换可以在不损失信息量的前提下保持约束
  2. 提高效率:转换后,稀疏的大矩阵运算变成了简单的多项式运算,提高了验证效率。

所以问题化为如何完成这样的转换。思考多项式的性质,多项式可以看成是空间中的曲线,因此点在曲线上就是满足约束。

因此问题进一步转换为如何找到一条曲线,满足和 R1CS 等价的约束。后者其实就是关于解 的方程,如果解正确,则满足约束,如果给出一个错误的解,那么 R1CS 等式不成立,对应于曲线就是点不在曲线上。

而因为 Prover 知道真实解 ,所以它有能力直接根据 R1CS 计算出曲线上的一些点。

因此现在的问题就是:

  1. 如何找到这些曲线上的点。
  2. 如何根据曲线上的一些点,求解出曲线的解析式。这个问题就很经典了,是多项式插值问题。

如何找到插值点

对于上述 R1CS,首先计算 的转置矩阵:

注意到 R1CS 约束等价于:

其中矩阵与 的乘积使用矩阵乘法, 表示 Hadamard 乘积(逐项乘积)。

实际上也可以具体计算验证,会发现:

可以验证。


那么,如果 A 中每个元素可以用 这个多项式表示(其中 表示第 列, 表示第 行,也即对第 个表达式的约束)。

由于 代表列向量, 同理,采取相同的操作。

展开等式后,我们可以得到以下逐个分量的等式:

给定等式 ,考虑到可加性,我们可以表示其加和为:

因此整个约束变成一个多项式的约束。这个约束就是 QAP 的多项式。

那么, 的含义明确后,我们就可以得到插值的点。

插值的点则可以通过矩阵的坐标 此坐标的值 获得,例如 经过 。这是因为当 。当

如何插值

就之前的例子继续, 经过 。目标是找到一个三次多项式 ,我们可以使用拉格朗日插值法或者牛顿插值法。

其实用哪种无所谓,因为只要 Prover 真的有 ,则多项式约束一定满足。插值的方法只决定了出错的时候错成什么样。

这里使用比较简单好懂的拉格朗日插值法。

拉格朗日插值法中,一个多项式 可以表示为:

其中 是点的个数, 是第 个点的 坐标,而 是拉格朗日基多项式,定义为:

对于我们的情况,我们有四个点,所以 ,且我们的点是 , , ,

我们可以计算出每个基多项式

用这些基多项式和点的 坐标来构建

简化一下:

这就是通过这四个点的三次多项式 的解析式。暴力展开得到各次系数:

这完全对应于 V 神给出的 多项式系数:

[-5.0, 9.166, -5.0, 0.833]

所以知道他怎么算出来的了吧

这样的过程还需要进行五次才能覆盖 A 的所有列。

(1,0) (1,1) (1,0) (1,0) (1,0) (1,0)
(2,0) (2,0) (2,0) (2,1) (2,0) (2,0)
(3,0) (3,1) (3,0) (3,0) (3,1) (3,0)
(4,5) (4,0) (4,0) (4,0) (4,0) (4,1)

此外还有 B、C。当然,交给计算机吧。

基于 QAP 的验证

下一个难点就是得到多项式之后,怎么应用到零知识证明中。我们知道零知识证明需要一个多项式 ,且可进行因式分解:

,其中 叫做目标多项式,是一系列零点乘积

这些零点是 Prover 和 Verifier 都知道的,但方程的解只有 Prover 知道。Verifier 只负责验证 是否整除

在本例中,存在以下对应关系:

  1. ,它对应于电路在 1、2、3、4 点等于0。
  2. 就是上面提到的多项式约束,它在 正确时为
  3. 基于上面两个算出来。这个计算过程由 Prover 执行。

对于第一点,读者可能会感觉到跳跃性,那我们回顾公式:

注意到对于任意 ,此算是总是成立,而 的定义域是 。所以我们可以断定 的一个零点。

或者从直观上理解,这意味着对于 为例,四个元件中除了第三个都会被消去,此时第三个电路成立。

一个常识是,经过某几个零点的多项式必须是按这几个零点因式分解式的整数倍。例如 ,有零点 ,那么 一定是 的整数倍。这一点告诉我们如何验证答案是否正确。


基于 QAP 的一种交互式零知识证明

据此我们已经掌握了从源程序到 QAP 的转换。我们可以设计一套零知识证明协议。

目的:Prover 证明自己知道使程序 成立的一个解是 . 但不能透露这个解给 Verifier

两方已知的信息

1. 源程序。
2. $p(x)$ 的一些零点。这些零点是各个元件的编号,从 1 开始。知道这些信息不需要预先知道 $p(x)$ 的表达式。

再次强调,Verifier 并不知道 ,换言之不知道 的系数。因为这些系数的计算依赖于知道 ,后者依赖于知道解向量。

Prover 的事前准备

  1. 将自己算出来的解 代入程序,得到一系列中间变量值。也即前文提到的
    • 务必注意的是,这里的 相关的 ,和 没有关系。前者是程序的输入,后者是 R1CS/QAP 中对不同元件的编号。千万不要把 代入 ,这完全错误。
  2. 基于 向量可以得到 的表达式。
  3. 问题转换为证明 Prover 知道 的所有系数。

交互过程

  1. Verifier
    1. 随机抽取一个数字 。发送给 Prover
  2. Prover
    1. 计算
    2. 代入 ,得到
    3. **如果 Prover 其实不知道 ,那么大概率算出来的 会产生余项。
  3. Verifier:
    1. 验证 满足,且 是一个整数,说明 Verifier 大概率没作弊。
  4. 重复此过程直到 Verifier 确信 Prover 没有碰运气。

这个协议可以让读者体会到 QAP 如何使用。

不过上面的交互协议太过于简陋,存在很多 Bug,并不会运用到真实世界。例如 值泄露给了 Prover,余项可能凑巧相消等等,因此需要同态加密、双线性配对等过程,来进一步重构、加固。