你好世界Circom

介绍

本章展示了 Circom 代码与其编译成的 Rank 1 Constraint System (R1CS) 之间的关系。

理解 R1CS 对于理解 Circom 至关重要，所以如果你还没有复习过 Rank 1 Constraint System，请务必复习一下。

为了解释 Circom 的工作原理，我们将从几个例子开始。

示例 1：简单乘法

假设我们正在创建 ZK 证明，以评估某人是否知道两个任意数字的乘积：c = a * b。

换句话说，对于某些 a 和 b，我们希望验证用户是否计算出了 c 的正确值。

用伪代码表示，验证如下（注意，这不是 Circom 代码）：

def someVerification(a, b, c):
  res = a * b 
  assert res == c, "invalid calculation"

因此，我们的 R1CS 只有一个约束，即以下约束：

assert c == a * b

R1CS 以结构化的矩阵格式表达这样的约束。根据我们在 R1CS 章节 中看到的内容，见证向量 $\mathbf{w}$ 应该写成 [1, a, b, c]，并且相应的 R1CS 可以写成：

$$ \begin{bmatrix} 0&1&0&0\\ \end{bmatrix}\mathbf{w} \circ \begin{bmatrix} 0&0&1&0\\ \end{bmatrix}\mathbf{w} = \begin{bmatrix} 0&0&0&1\\ \end{bmatrix}\mathbf{w} $$

如果 a = 3, b = 4, 并且 c = 12, 上面的操作将会是：

$$ \begin{bmatrix} 0&1&0&0\\ \end{bmatrix} \begin{bmatrix} 1\\ 3\\ 4\\ 12\\ \end{bmatrix} \circ \begin{bmatrix} 0&0&1&0\\ \end{bmatrix}\begin{bmatrix} 1\\ 3\\ 4\\ 12\\ \end{bmatrix} = \begin{bmatrix} 0&0&0&1\\ \end{bmatrix}\begin{bmatrix} 1\\ 3\\ 4\\ 12\\ \end{bmatrix} $$

以下是如何在 Circom 中编写上述约束：

template SomeCircuit() {
  // inputs
  signal input a;
  signal input b;
  signal input c;

  // constraints 
  c === a * b;
}

component main = SomeCircuit();

• 给定输入 a、b、c，电路验证 a * b 是否确实等于 c。
• 该电路用于验证，不是 用于计算。这就是为什么 c（计算的输出）也是所需的输入之一。
• === 运算符以先前在 R1CS 形式中表达的方式定义约束。=== 的行为类似于断言，因此如果提供无效输入，电路将不满意。在上面的代码中，c === a * b 约束 c 的值等于 a 和 b 的乘积。

zkRepl，一个 Circom 在线 IDE

对于快速实验，zkRepl 是一个非常棒且方便的工具。

我们可以通过将输入作为注释提供，来方便地在 zkRepl 中测试上面的代码：

注意： 使用 zkrepl 时，输入作为 JSON 对象在注释中提供。要测试代码是否编译以及输入是否满足电路，请使用 shift-enter。

“非线性约束”等于 1（参见红色框），因为底层 R1CS 具有一行约束，其中包含两个信号之间的乘法。这是预期的，因为我们只有一个 ===。

template , component , main

• Templates (模板) 定义了电路的蓝图，就像类定义了 OOP（面向对象编程）中对象的结构一样。
• Component (组件) 是模板的实例化，类似于对象是面向对象编程中类的实例。

// create template
template SomeCircuit() {
  // .... stuff
}

// instantiate template 
component main = SomeCircuit();

需要 component main = SomeCircuit()，因为 Circom 需要一个顶层组件 main 来定义要编译的电路结构。

signal input

• Signal inputs (信号输入) 是将从组件外部提供的值。(Circom 不强制实际提供一个值 —— 这取决于开发人员来确保实际提供这些值。如果它们没有提供，这可能会导致安全漏洞 —— 这将在后面的章节中探讨。)
• 输入信号是不可变的，不能被更改。
• 信号正是 Rank 1 Constraint System 见证向量中的变量。

Circom 的有限域

Circom 在一个 有限域 中执行算术运算，其阶数为 21888242871839275222246405745257275088548364400416034343698204186575808495617，我们将其简称为 $p$。它是一个 254 位数字，对应于 bn128 椭圆曲线的曲线阶数。该曲线被广泛使用，特别是在 EVM 中通过预编译提供该曲线。由于 Circom 旨在用于开发以太坊上的 ZK-SNARK 应用程序，因此使字段大小与 bn128 曲线的曲线阶数匹配是有意义的。

Circom 允许通过命令行参数更改默认顺序。

以下内容对于读者来说应该是很明显的：

• p 在 mod p 下与 0 同余；
• p-1 是 有限域 mod p 中最大的整数。
• 传递大于 p-1 的值将导致溢出。

示例 2：BinaryXY

让我们看第二个例子来结束本节。

考虑一个电路，该电路验证传递给它的值是否为二进制，即 0 或 1。

如果输入变量是 x 和 y，则约束系统将是：

(1):  x * (x - 1) === 0
(2):  y * (y - 1) === 0

回想一下，根据定义，R1CS 中的每个约束最多只能有一个变量之间的乘法。

• x (x-1) === 0 检查 x 是否为二进制数字

• 这个多项式表达式只有 2 个根。

• I.e., x = 0 或 x = 1.

用 Circom 表示

template IsBinary() {

  signal input x;
  signal input y;

  x * (x - 1) === 0;
  y * (y - 1) === 0;
}

component main = IsBinary();

替代表达方式：使用数组

在 Circom 中，我们可以选择将输入声明为 separate signals (单独的信号)，或者声明一个包含所有输入的 array (数组)。在 Circom 中，更常见的是将所有输入分组到一个名为 in 的信号 array (数组) 中，而不是提供单独的输入 x 和 y。

按照惯例，我们将之前的电路表示如下。数组的索引从零开始，正如你通常期望的那样：

template IsBinary() {

  // array of 2 input signals
  signal input in[2];

  in[0] * (in[0] - 1) === 0;
  in[1] * (in[1] - 1) === 0;
}

// instantiate template 
component main = IsBinary();

只有满足约束的见证才会被接受

Circom 只能为实际满足电路的输入生成证明。在以下电路（直接从上面的代码复制）中，我们提供 [0, 2] 作为输入，该输入仅接受 {0,1} 作为数组的任何元素。

对于 0，我们有 0 * (0 - 1) === 0，这是可以的。但是，对于 2 * (2-1) === 2，我们有一个约束冲突，如下图中的红色框所示。

在命令行中使用 Circom

本节介绍常用的 Circom 命令。我们假设读者已经安装了 Circom 和所需的依赖项。

创建一个新目录，并在其中添加一个名为 somecircuit.circom 的文件，其中包含以下代码：

pragma circom 2.1.8;

template SomeCircuit() {
  // inputs
  signal input a;
  signal input b;
  signal input c;

  // constraints 
  c  === a * b;
}

component main = SomeCircuit();

1. 编译电路

在终端中，执行以下命令进行编译：

circom somecircuit.circom --r1cs --sym --wasm

• --r1cs 标志表示输出一个 r1cs 文件，--sym 标志为变量提供人类可读的名称（更多信息可以在 sym 文档 中找到），--wasm 用于生成 wasm 代码，以在给定输入 JSON 的情况下填充 R1CS 的见证（在后面的章节中展示）。
• 根据需要更改要编译的电路名称 somecircuit.circom。

这是预期的输出：

• 观察到非线性约束被列为 1，表明 a * b === c。
• Wires (连线) 是 R1CS 中的列数。在此示例中，我们有一个 constant column (常数列) 和三个信号 a、b、c。

编译器创建以下内容：

• somecircuit.r1cs 文件
• somecircuit.sym 文件
• somecircuit_js 目录

.r1cs 文件

• 此文件包含电路的 R1CS 约束系统，采用二进制格式。
• 可以与不同的工具堆栈一起使用，以构造证明/验证语句（例如 snarkjs、libsnark）。

请注意，R1CS 文件有点像二进制文件，因为运行 cat <file> 会给你乱码。

运行 snarkjs r1cs print somecircuit.r1cs，我们得到以下人类可读的输出：

[INFO]  snarkJS: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.a ] * [ main.b ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.c ] = 0

在 Circom 中，算术运算在有限域内进行，因此21888242871839275222246405745257275088548364400416034343698204186575808495616 实际上代表 -1。但是在 R1CS 文件中，约束运算符是 = 而不是 == 或 ===。

我们可以通过检查 -1 mod p 来确认这一点（在 Python 中：-1 % p），其中 p 是 Circom 有限域的阶数。如果我们翻译 snarkjs r1cs print somecircuit.r1cs 打印的大值，以得到负数，我们会得到：

[-1 * main.a] * [main.b] - [-1 * main.c] = 0

我们现在将上面的表达式转换为更熟悉的 a * b === c。代数运算如下所示：

[-1 * main.a] * [main.b] - [-1 * main.c] = 0

    [-main.a] * [main.b] - [-main.c] = 0 // distribute -1

     [main.a] * [main.b] + [-main.c] = 0 // multiply both sides by -1

     [main.a] * [main.b] = [main.c] // move -main.c to the other side

再次，观察到这与 somecircuit.circom 中描述的约束（a * b === c）匹配。

.sym 文件

somecircuit.sym 文件是在编译期间生成的 symbols file (符号文件)。此文件至关重要，因为：

• 它将人类可读的变量名称映射到 R1CS 中对应的位置以进行调试。
• 它有助于以更易于理解的格式打印约束系统，从而更容易验证和调试你的电路。

somecircuit_js 目录

somecircuit_js 目录包含用于见证生成的工件：

• somecircuit.wasm
• generate_witness.js
• witness_calculator.js

generate_witness.js 文件是我们在下一节中将要使用的文件，其他两个文件是 generate_witness.js 的助手。

通过为电路提供输入值，这些工件将计算必要的中间值并创建一个可用于生成 ZK 证明的见证。

2. 计算见证

要生成见证，我们必须为电路提供 public input values (公共输入值)。我们通过在 somecircuit_js 目录中创建一个 inputs.json 文件来实现。

假设我们要为输入值 a=1、b=2、c=2 创建一个见证。JSON 文件将如下所示：

{"a": "1","b": "2","c": "2"}

Circom 期望字符串而不是数字，因为 JavaScript 无法准确处理大于 $2^{53}$ 的整数 (来源)。

在 somecircuit_js 目录中运行以下命令：

node generate_witness.js **somecircuit.wasm** inputs.json witness.wtns

输出是计算出的见证，作为一个 witness.wtns 文件。

检查计算出的见证：witness.wtns

如果你运行 cat witness.wtns，输出将是乱码。

这是因为 witness.wtns 是 snarkjs 接受的格式的二进制文件。

要获得人类可读的形式，我们通过以下方式将其导出为 JSON：snarkjs wtns export json witness.wtns。然后我们使用 cat witness.json 查看 JSON：

• 第一个 1 是见证的常数部分，始终为 1。由于我们的输入 JSON 是 {"a": "1","b": "2","c": "2"}，因此我们有 a = 1、b = 2 和 c = 2。
• snarkjs 提取 witness.wtns 文件以输出 witness.json。
• 计算出的见证符合见证向量的 R1CS 布局：[1, a, b, c] = [1, 1, 2, 2]

示例：isbinary.circom

让我们运行一个不那么简单的例子：isbinary.circom。约束的形式对于读者来说应该是熟悉的（回想一下示例 2）。

template IsBinary() {

  // array of 2 input signals
  signal input in[2];

  in[0] * (in[0] - 1) === 0;
  in[1] * (in[1] - 1) === 0;
}

// instantiate template 
component main = IsBinary();

编译电路

• circom isbinary.circom --r1cs --sym --wasm
• 终端输出的健全性检查：non-linear constraints: 2

这是有道理的，因为我们的电路包含两个断言，每个断言都涉及信号的乘法。

接下来，我们检查 R1CS 文件：命令 snarkjs r1cs print isbinary.r1cs 产生以下输出：

[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.in[0] ] * [ main.in[0] ] - [  ] = 0
[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.in[1] ] * [ main.in[1] ] - [  ] = 0

请注意，这个大数字与之前高亮显示的 -1 mod p 系数略有不同（即：21888242871839275222246405745257275088548364400416034343698204186575808495616）

观察末尾的附加数字 1：

• 21888242871839275222246405745257275088548364400416034343698204186575808495616
• 21888242871839275222246405745257275088548364400416034343698204186575808495616(1)

末尾有一个 1 的原因是 snarkjs 格式化输出的方式存在缺陷。它“试图”说 -1 1，但它们之间没有空格。

我们现在将代数地将 snarkjs 的输出转换为原始约束：

(in[0] - 1) * in[0] === 0
(in[1] - 1) * in[0] === 0

推导如下：

// original circom output
[ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.in[0] ] * [ main.in[0] ] - [  ] = 0
[ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.in[1] ] * [ main.in[1] ] - [  ] = 0

// remove empty terms
[ (21888242871839275222246405745257275088548364400416034343698204186575808495616)1 +main.in[0] ] * [ main.in[0] ] = 0
[ (21888242871839275222246405745257275088548364400416034343698204186575808495616)1 +main.in[1] ] * [ main.in[1] ] = 0

// rewrite p - 1 as -1
[ (-1)1 +main.in[0] ] * [ main.in[0] ] = 0
[ (-1)1 +main.in[1] ] * [ main.in[1] ] = 0

// simplify
[ main.in[0] - 1] * [ main.in[0] ] = 0
[ main.in[1] - 1] * [ main.in[1] ] = 0

生成见证

• 在 ./isbinary_js 目录中创建一个 inputs.json 文件。
• 我们将选择传递值 in[0] = 1，in[1] = 0。
• 我们将使用以下代码作为 inputs.json。

{"in": ["1","0"]}

• 生成 witness.wtns：node generate_witness.js isbinary.wasm inputs.json witness.wtns（在 isbinary_js 目录中）
• 现在已经创建了 witness.wtns，将其导出为 JSON，以便我们可以检查它：snarkjs wtns export json witness.wtns
• 我们将在执行 cat witness.json 时获得以下输出：

[
 "1",  // 1
 "1",  // in[0] 
 "0"   // in[1] 
]

• 计算出的信号与见证向量的 R1CS 布局 [1, in[0], in[1]] 相匹配，它们的各自的值也是如此。

生成 ZK 证明

创建 R1CS 后，读者可以按照 Circom 文档中的步骤生成 ZK 证明 和随附的智能合约验证器。

练习题

通过解决我们的 ZK 难题仓库中的这些难题来测试你对本章的理解/学习。每个难题都需要你填写缺失的逻辑。你可以通过简单地运行单元测试来检查你的答案。

• <https://github.com/RareSkills/zero-knowledge-puzzles/blob/main/BinaryXY/BinaryXY.circom>
• <https://github.com/RareSkills/zero-knowledge-puzzles/blob/main/MultiplyNoOut/MultiplyNoOut.circom>
• <https://github.com/RareSkills/zero-knowledge-puzzles/blob/main/FourBitBinary/FourBitBinary.circom>

• 原文链接： rareskills.io/post/hello...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～