Source: https://rareskills.io/zh-cn/post/r1cs-to-qap
为了让从 R1CS 到 QAP 的转换不那么抽象,我们来看一个真实的例子。
假设我们要对以下 算术电路 进行编码
$z = x^{4} - 5y^{2}x^{2}$
将其转换为 秩 1 约束系统 后,变为
$\begin{aligned} v_1 &= xx \\ v_2 &= v_1 * v_1 && //x^4\\ v_3 &= -5yy \\ -v_2 + z &= v_3 * v_1 && //-5y^2 * x^2\\ \end{aligned}$
<aside> 💡 💡 这里最绕的是:为什么要把一个式子拆成这么多行?因为 R1CS 规定每一行只能做『一次乘法』。就像做菜时菜谱只允许你一步炒一样东西:$x^4$ 不能一口气算出来,得先算 $v_1=x\cdot x$(得到 $x^2$),再算 $v_2=v_1\cdot v_1$(得到 $x^4$)。每多一个乘号,就多一行约束。
</aside>
我们需要为将要进行操作的 有限域 选择一个特征值。当我们稍后将其与 椭圆曲线 结合时,我们的素数域的阶需要等于椭圆曲线的阶。(这两者不匹配是一个非常常见的错误)。
<aside> 💡 💡 一句话理解:后面所有运算都要在『时钟数字』里做。想象一个只有 0~78 的钟面,走到 79 就回到 0。选素数 79 只是为了举例时数字小、好算;真到了和椭圆曲线配合时,这个钟面的大小必须和椭圆曲线的『一圈格子数』完全一样,否则两套系统对不上号。
</aside>
但现在,为了便于管理,我们将选择一个较小的数字。我们选择素数 79。
首先,我们定义矩阵 $\mathbf{L}$ 、 $\mathbf{R}$ 和 $\mathbf{O}$ 如下:
import numpy as np
# 1, out, x, y, v1, v2, v3
L = np.array([
[0, 0, 1, 0, 0, 0, 0],
[0, 0, 0, 0, 1, 0, 0],
[0, 0, 0, -5, 0, 0, 0],
[0, 0, 0, 0, 0, 0, 1],
])
R = np.array([
[0, 0, 1, 0, 0, 0, 0],
[0, 0, 0, 0, 1, 0, 0],
[0, 0, 0, 1, 0, 0, 0],
[0, 0, 0, 0, 1, 0, 0],
])
O = np.array([
[0, 0, 0, 0, 1, 0, 0],
[0, 0, 0, 0, 0, 1, 0],
[0, 0, 0, 0, 0, 0, 1],
[0, 1, 0, 0, 0, -1, 0],
])
<aside> 💡 💡 打个比方:这三个矩阵就是把 R1CS 的每行约束抄成『配料表』。表头是 7 个变量 $[1, out, x, y, v_1, v_2, v_3]$,每一行对应一条约束,格子里的数字是该变量在这条约束里的系数。比如 $\mathbf{L}$ 第一行 $[0,0,1,0,0,0,0]$ 就表示『这条约束等号左边的乘数是 $x$』。$\mathbf{L}$ 管左乘数、$\mathbf{R}$ 管右乘数、$\mathbf{O}$ 管结果。
</aside>
为了验证我们正确构建了 R1CS(手动操作时很容易出错!),我们创建一个有效的 witness 并进行矩阵乘法运算:
x = 4
y = -2
v1 = x * x
v2 = v1 * v1 # x^4
v3 = -5*y * y
z = v3*v1 + v2 # -5y^2 * x^2
# witness
a = np.array([1, z, x, y, v1, v2, v3])
assert all(np.equal(np.matmul(L, a) * np.matmul(R, a), np.matmul(O, a))), "not equal"
<aside> 💡 💡 为什么要做这步:witness 就是把每个变量的真实数值填进一张『名单』 $a=[1, out, x, y, v_1, v_2, v_3]$。这行 assert 在逐条核对:每条约束里『左边那列点名单』乘『右边那列点名单』,是不是正好等于『结果那列点名单』。全部对上,才说明矩阵没抄错、这组数确实满足电路。
</aside>
下一步是将它转换为一个域数组。在 Numpy 中进行模运算会变得非常混乱,但使用 galois 库则非常直观。这在我们关于有限域的文章中已经介绍过,但这里简要回顾一下如何使用它:
import galois
GF = galois.GF(79)
a = GF(70)
b = GF(10)
print(a + b)
# prints 1
我们不能向它传递像 GF(-1) 这样的负值,否则会抛出异常。要将负数转换为它们在域中的同余表示,我们可以将曲线的阶加到它们上面。为了避免正值“溢出”,我们对其取曲线阶的模。