简介
本章展示了 Circom 代码与其编译成的 Rank 1 Constraint System (R1CS) 之间的关系。
理解 R1CS 对于理解 Circom 至关重要，所以如果您还没有了解过相关知识，请务必温习一下 Rank 1 Constraint Systems。
为了解释 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 章节中所看到的内容，见证向量（witness vector） 应该写成 [1, a, b, c]，相应的 R1CS 可以写成：
如果 a = 3，b = 4，且 c = 12，则上述运算将变为：
在 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 键。
“non-linear constraints”（非线性约束）等于 1（见红框），因为底层的 R1CS 有一个行约束，其中包含两个信号之间的乘法。这是符合预期的，因为我们只有一个 ===。
template , component , main
- Templates（模板）定义了电路的蓝图，就像在 OOP（面向对象编程）中，类定义了对象的结构一样。
- component（组件）是 template 的实例化，类似于在面向对象编程中对象是类的实例。
// create template
template SomeCircuit() {
// .... stuff
}
// instantiate template
component main = SomeCircuit();
需要编写 component main = SomeCircuit() 是因为 Circom 要求有且仅有一个顶层组件 main，用于定义将被编译的电路结构。
signal input
- Signal inputs（信号输入）是将从组件外部提供的值。（Circom 不会强制要求实际提供一个值——这取决于开发者去确保这些值被实际提供。如果不这样做，可能会导致安全漏洞——这将在后面的章节中探讨。）
- Input signals（输入信号）是不可变的，不能被更改。
- Signals（信号）实际上就是 Rank 1 Constraint System 见证向量中的变量。
Circom 的有限域
Circom 在阶数为 21888242871839275222246405745257275088548364400416034343698204186575808495617 的有限域（finite field）中执行算术运算，我们将其简称为 。它是一个 254 位数字，对应于 bn128 椭圆曲线的曲线阶数。这条曲线被广泛使用，特别是在 EVM 中通过预编译提供的曲线就是它。由于 Circom 旨在用于在 Ethereum 上开发 ZK-SNARK 应用程序，因此使其域大小与 bn128 曲线的阶数相匹配是合理的。
Circom 允许通过命令行参数更改默认的阶数。
以下内容对读者来说应该是显而易见的：
p在mod p下与0同余；p-1是 有限域mod p中的最大整数。- 传入大于
p-1的值将导致溢出（overflow）。
示例 2：BinaryXY
让我们看第二个例子来结束本节。
考虑一个电路，它验证传递给它的值是否为二进制值，即 0 或 1。
如果输入变量为 x 和 y，则约束系统将是：
(1): x * (x - 1) === 0
(2): y * (y - 1) === 0
回顾一下，根据定义，R1CS 中的每个约束最多只能有一个变量之间的乘法。
x(x-1) === 0 检查 x 是否为二进制数字*
- 此多项式表达式只有 2 个根。
- 即，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 中，我们可以选择将输入声明为单独的信号，或者声明一个包含所有输入的数组。在 Circom 中，更常规的做法是将所有输入分组到一个名为 in 的信号数组中，而不是提供单独的输入 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();
只接受满足约束的见证（witnesses）
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 docs 中找到），而--wasm用于生成 wasm 代码，以便在给定输入 JSON 时填充 R1CS 的见证（见后面的小节演示）。- 根据需要，替换要编译的电路名称
somecircuit.circom。
预期输出如下：
- 观察到 non-linear constraints（非线性约束）列为 1，这表示
a * b === c。 - Wires 是 R1CS 中的列数。在这个例子中，我们有一个常数（constant）列和三个信号
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 目录包含用于见证生成（witness generation）的产物：
somecircuit.wasmgenerate_witness.jswitness_calculator.js
generate_witness.js 文件是我们在下一节将要使用的文件，另外两个文件是 generate_witness.js 的辅助文件。
通过为电路提供输入值，这些产物将计算出必要的中间值，并创建一个可用于生成 ZK 证明的见证（witness）。
2. 计算见证（Witness）
为了生成见证，我们必须为电路提供公开输入值。我们通过在 somecircuit_js 目录中创建一个 inputs.json 文件来实现这一点。
假设我们要为输入值 a=1、b=2、c=2 创建见证。JSON 文件将如下所示：
{"a": "1","b": "2","c": "2"}
Circom 期望使用字符串而不是数字，因为 JavaScript 无法精确处理大于 的整数（来源）。
在 somecircuit_js 目录中运行以下命令：
node generate_witness.js **somecircuit.wasm** inputs.json witness.wtns
输出的计算见证保存为一个 witness.wtns 文件。
检查计算得出的见证：witness.wtns
如果您运行 cat witness.wtns，输出将是乱码。
这是因为 witness.wtns 是一个二进制文件，其格式可以被 snarkjs 接收。
为了获得人类可读的格式，我们通过 snarkjs wtns export json witness.wtns 将其导出为 JSON。然后我们使用 cat witness.json 查看该 JSON 文件：
- 第一个
1是见证的常数部分，它始终为1。我们得出a = 1、b = 2以及c = 2，因为我们输入的 JSON 是{"a": "1","b": "2","c": "2"}。 - snarkjs 摄取（ingest）
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：
2188824287183927522224640574525727508854836440041603434369820418657580849561621888242871839275222246405745257275088548364400416034343698204186575808495616(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 Puzzles 仓库中的这些谜题，来测试您对本章内容的理解和学习情况。每个谜题都要求您填写缺失的逻辑。您只需通过运行单元测试即可检查您的答案。