[new]Zk-SNARKs系列文章(part2)(科普)

在对Zk-SNARK进行更严谨的定义之前，必须先了解一些背景知识。
一般来说，零知识协议的一个复杂因素是，为了使它们适用于一个特定用例，必须彻底改变其原始问题。

考虑一下Alice想向Bob证明她知道下列方程式的解：
$x^2-4=0$

诚然，在这种情况下其方程的解是微不足道的，这些问题并不需要零知识证明，
因为任何人都能轻易得出答案。但虽然如此，为了简单起见，这是本系列文章中所涉及到的示例，
但应该牢记在心的是，这些方程式在实际中的阶数很容易变成一百万，甚至更多，而不仅仅只是二次多项式。

那么如何对这个问题进行编码呢？
首先是用代码表示这个问题，比如用Python:
def f(x):
    y = x ** 2 - 4;

对于Alice来说，她的目标是评估在X取某些值时，
其对应的y值的确为0，显然这会出现两个问题：
一是Bob在未获取X值的情况下能得以窥见y值为0;
二是由于Alice是运行整个程序的人，所以Bob无法获知Alice实际上运行的是不是约定的程序，她可以直接运行y=0来进行作弊。

上述两个问题都是非常棘手的问题，但解决它们的方法却并不复杂，
即可以将其转换成QAP(Quadratic Arithmetic Program)，
它包含三个步骤：1）代码平化(code flattening),2)转换至R1CS(Rank1 Constraint System),3）最后是制定QAP;

代码平化的目标是把原始包含复杂语句和表达式的代码转换成满足特定形式的语句序列：

1)x=y(y可以是变量或数字)
2)x=y(op)z(其中op$\in$(+,-,*,/).y,z可以是变量或数字，甚至其子表达式)

一个比较简单的理解方式是将这些语句视为算数电路的门，那么上述代码平化后的结果是：
def f(x):
    out_1 = x * x 
    y = out - 4 
    
 接下来要做的是将其转换成R1CS。
 简单来说，R1CS 是一个三元矢量列表，并且它的解向量满足：
 <$\vec a_i$,$\vec s$>*<$\vec b_i$,$\vec s$>-<$\vec c_i,\vec s$>=0  $\forall i$
<*,*> 表示的是两个矢量的点积，三元组可以用来定义约束，需要找到满足方程式的解向量。

有一个更自然的方法将代码平化后的结果转换为R1CS。

首先定义一个向量用于保存程序所使用的所有变量，其所有元素都是变量，并且该解向量会被赋给每个变量。

在本例中，解向量 $\vec s_i$=$\begin{pmatrix} 1\\x\\out\\y\\ \end{pmatrix}$

值得留意的是解向量的第一个元素 1 是为了对常数进行编码而设计的，会马上对其进行解释。

接下来是依次对平化后的代码进行处理并定义合适的$\vec a_i,\vec b_i,\vec c_i$以对当前行的计算进行编码。

以第一行代码为例，其对应的向量依次为：
$\vec a_1 = \begin{matrix}(0&1&0&0) \end{matrix}$
$\vec b_1 = \begin{matrix}(0&1&0&0) \end{matrix}$
$\vec c_1 = \begin{matrix}(0&0&1&0) \end{matrix}$

第二行代码对应的向量依次为：
$\vec a_2 = \begin{matrix}(-4&0&1&0) \end{matrix}$
$\vec b_2 = \begin{matrix}(1&0&0&0) \end{matrix}$
$\vec c_2 = \begin{matrix}(0&0&0&1) \end{matrix}$

可以注意到之前定义$\vec a_2$向量时，其第一个元素 1 在表示约束 -4 时派上了用场。

第一行:
<$\vec a_1$,$\vec s$>*<$\vec b_1$,$\vec s$>-<$\vec c_1,\vec s$>=$\sum_{i=1}^n a_{1,i}s_i$*$\sum_{i=1}^n b_{1,i}s_i$-$\sum_{i=1}^n c_{1,i}s_i$=x*x-out=0

第二行：
<$\vec a_2$,$\vec s$>*<$\vec b_2$,$\vec s$>-<$\vec c_2,\vec s$>=$\sum_{i=1}^n a_{2,i}s_i$*$\sum_{i=1}^n b_{2,i}s_i$-$\sum_{i=1}^n c_{2,i}s_i$=out-4-y=0

至此，已经成功把上面的python程序转化成一系列的约束，程序内部的逻辑已经“转移”到约束三元组$(\vec a_i,\vec b_i,\vec c_i)$。
这也意味着，运行程序等同于寻找到合适的解向量赋值，使其满足 R1CS 方程式。