在Python中将R1CS转换为有限域上的二次算术程序(QAP)

为了使 R1CS 到 QAP 的转换不那么抽象，让我们使用一个真实的例子。

假设我们要编码以下算术电路：

$$z = x⁴ – 5y²x²$$

转换为秩 1 约束系统，这变为：

$$ \begin{align} 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{align*} $$

我们需要选择一个特征，以便在有限域上进行。稍后，当我们将其与椭圆曲线结合时，我们的素数域的阶数需要与椭圆曲线的阶数相等。（不匹配这两者是一个很常见的错误）

但现在，我们将选择一个小数字以便于处理。我们选择素数 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],
])

为了验证我们是否正确构建了 R1CS（在手动操作时很容易出错!），我们创建一个有效的见证并进行矩阵乘法：

x = 4
y = -2
v1 = x * x
v2 = v1 * v1        # x^4
v3 = -5*y * y
z = v3*v1 + v2    # -5y^2 * x^2

## 见证
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))), "不相等"

Python 中的有限域算术

下一步是将其转换为域数组。在 Numpy 中进行模运算会变得非常麻烦，但使用 galois 库非常简单。这在我们关于有限域的文章中已经介绍过，这里是如何使用它的简要回顾：

import galois

GF = galois.GF(79)

a = GF(70)
b = GF(10)

print(a + b)
## 输出 1

我们不能给负值，例如 GF(-1)，否则它将引发异常。要将负数转换为其在域中的同余表示，我们可以将曲线的阶数加到它们上面。为了避免“溢出”正值，我们用曲线的阶数进行取模运算。

L = (L + 79) % 79
R = (R + 79) % 79
O = (O + 79) % 79

我们的新矩阵为：

### 新的 L, R, O 值
'''
L

[[ 0  0  1  0  0  0  0]
 [ 0  0  0  0  1  0  0]
 [ 0  0  0 74  0  0  0]
 [ 0  0  0  0  0  0  1]]

R

[[ 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

[[ 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 78  0]]
'''

现在我们可以通过将它们用 GF 包装来简单地转换为域数组。同时，我们...