本教程介绍了 Circom 语言及其使用方法,以及常见的陷阱。我们还将解释 circomlib 库的很大一部分内容,以引入常见的设计模式。
关于生产环境使用的注意事项
Circom 是学习 ZK-SNARKS 的出色工具。然而,由于它非常底层,因此更容易意外引入难以察觉的 bug。在实际应用中,程序员应考虑使用更高级的零知识编程语言(level zero knowledge programming languages)。在部署持有用户资金的智能合约之前,您应该始终进行审计,这对于 ZK 电路(ZK circuits)来说尤为重要,因为其攻击向量较不为人知。
前置条件
虽然在不了解什么是 Rank 1 Constraint System 的情况下也可以在 Circom 中进行编程,但如果了解的话,您在构建该语言的心智模型时会轻松得多。Circom 本质上是一个用于创建 Rank 1 Constraint System(一阶约束系统)的符合人体工程学的包装器。
安装
按照这里的步骤安装 circom
您还需要安装 snarkjs
npm install -g snarkjs@latest
Hello World
ZK 电路的 Hello World 是进行一次乘法运算,所以让我们从这里开始。
pragma circom 2.1.6;
template Multiply() {
signal input a;
signal input b;
signal output out;
out <== a * b;
}
component main = Multiply();
将上述代码保存为 multiply.circom 并在终端运行
circom multiply.circom
template instances: 1
Everything went okay, circom safe
以确保它能正常编译。
生成 R1CS 文件
要将电路转换为 R1CS,请运行以下终端命令:
circom multiply.circom --r1cs --sym
--r1cs 标志告诉 circom 生成一个 R1CS 文件,--sym 标志意味着“保存变量名”。这很快就会变得清晰明了。
将创建两个新文件:
multiply.r1cs
multiply.sym
如果打开 multiply.r1cs,您将看到一堆二进制数据,但在 .sym 文件中,您会看到变量的名称。
要读取 R1CS 文件,我们像下面这样使用 snarkjs:
snarkjs r1cs print multiply.r1cs
我们将得到以下输出
[INFO] snarkJS: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.a ] * [ main.b ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.out ] = 0
请记住,在处理算术电路时,一切都是在有限域(finite field)中进行的,因此您看到的这个庞大数字本质上是 -1。该 R1CS 方程等价于
-1 * a * b - (-1*out) = 0;
通过一点代数运算,我们可以看到这等同于 a * b = out,也就是我们原始的电路。
代数运算的步骤如下:
-1 * a * b - (-1*out) = 0;
-1 * a * b = -1*out;
a * b = out;
不允许非二次约束!
一个有效的 R1CS 必须在每个约束中恰好包含一个乘法(约束是 R1CS 中的一行,即 Circom 中的 <== 或 ===)。如果我们尝试进行两次(或更多次)乘法,这将会失败。所有包含多个乘法的约束都需要拆分为两个约束。请考虑以下(无法编译的)示例:
pragma circom 2.1.6;
template Multiply() {
signal input a;
signal input b;
signal input c;
signal output out;
out <== a * b * c;
}
component main = Multiply();
当我们运行 circom multiply.circom 时,将得到以下错误:
error[T3001]: Non quadratic constraints are not allowed!
┌─ "multiply.circom":9:3
│
9 │ out <== a * b * c;
│ ^^^^^^^^^^^^^^^^^ found here
│
= call trace:
->Multiply
previous errors were found
Circom 中的约束由 <== 运算符表示。对于这个特定的约束,我们为一个约束执行了两次乘法。要解决这个问题,我们需要创建一个单独的约束,以便每个约束只有一个乘法。
拆分非二次约束
修复上述问题很简单。我们引入一个中间信号 s1 并让它约束第一次乘法,然后将 s1 的输出与第三个输入结合。现在我们有两个约束和两次乘法,正如 Circom 所期望的那样。
pragma circom 2.1.6;
template Multiply() {
signal input a;
signal input b;
signal input c;
signal s1;
signal output out;
s1 <== a * b;
out <== s1 * c;
}
component main = Multiply();
当我们重新生成并打印 R1CS 时,得到如下内容:
[INFO] snarkJS: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.s1 ] * [ main.c ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.out ] = 0
通过一点代数运算,这转换为
a * b = s1
s1 * c = out
我们可以看到,这编码了与我们电路相同的计算。
计算 witness(见证)
运行以下命令以创建生成 witness 向量的代码:
circom multiply.circom --r1cs --sym --wasm
这将重新生成 R1CS 和符号文件,但同时还会创建一个名为 multiply_js/ 的文件夹。cd 进入该文件夹。
接下来,我们需要在该文件夹中创建一个 input.json 文件。这是一个映射,将指定为输入的信号名称映射到证明者将提供给它们的值。让我们将 input.json 设置为以下值:
{"a": "2","b": "3","c": "5"}
如果之前没有创建 .sym 文件,Circom 就无法知道我们试图映射到哪些输入信号。因为 s1 和 out 不是输入信号,我们不为它们创建键值对。这里的 a、b 和 c 对应于输入信号的名称。
signal input a;
signal input b;
signal input c;
现在我们使用以下命令计算并导出 witness:
node generate_witness.js multiply.wasm input.json witness.wtns
snarkjs wtns export json witness.wtns
cat witness.json
[
"1",
"30",
"2",
"3",
"5",
"6"
]
计算出的 witness 的值为 [1, 30, 2, 3, 5, 6]。2、3 和 5 是输入,而 6 是中间信号 s1,它是 2 和 3 的乘积。
这符合预期的 R1CS 变量布局格式:[1, out, a, b, c, s1]。
公开输入(Public inputs)
如果我们想将部分输入公开怎么办?例如,在 Nullifier(废止符)方案中,我们将两个数字拼接后进行哈希处理,并在此后揭示其中一个数字。
动机:Nullifier(废止符)方案
顺便提一下,Nullifier 方案的原理是将两个数字拼接后进行哈希处理。它们用于这样一种场景:我们有一组哈希值,并且我们想要证明我们知道其中一个哈希值的原像,但不想透露具体是哪一个。
如果哈希仅仅是一个数字的哈希,那么揭示该数字就会暴露我们知道哪个哈希的原像。然而,如果我们不透露任何信息,我们就可以多次重复“证明我们知道某个哈希原像”的操作。如果这个操作涉及从智能合约中提取资金,这将会是一个严重的问题!
通过揭示两个被哈希的数字中的一个,我们就无法重复使用原像,但同时我们也没有暴露我们知道哪一个哈希的原像,因为仅仅揭示两个数字中的一个是不足够的。
以下是 Circom 实现公开输入的方法:
template SomePublic() {
signal input a;
signal input b;
signal input c;
signal v;
signal output out;
v <== a * b;
out <== c * v;
}
component main {public [a, c]} = SomePublic();
在上面的示例中,a 和 c 是公开输入,但 b 保持隐藏。请注意在实例化主组件时使用的 public 关键字。
Circom 中的数组
让我们创建一个计算输入值的 n 次方的组件。
手动编写 n 次信号输入会非常繁琐,因此 Circom 提供了一种数组类型的信号来实现这一点。代码如下:
pragma circom 2.1.6;
template Powers(n) {
signal input a;
signal output powers[n];
powers[0] <== a;
for (var i = 1; i < n; i++) {
powers[i] <== powers[i - 1] * a;
}
}
component main = Powers(6);
这个示例引入了几个新的语法特性:模板参数和变量。
模板参数
在上面的示例中,我们看到模板被参数 n 参数化了,即 Powers(n)。
Rank 1 Constraint System 必须是固定且不可变的,这意味着一旦定义,我们就不能更改行数或列数,也不能更改矩阵或 witness 的值。这就是为什么最后一行硬编码了参数 Powers(6),这个大小必须是固定的。
然而,如果以后我们想复用此代码来支持不同大小的电路,那么让模板能够动态更改其大小会更符合人体工程学。因此,组件可以接受参数来参数化控制流和数据结构,但这在每个电路中必须是固定的。
Circom 变量
上面的例子等同于以下内容:
pragma circom 2.1.6;
template Powers() {
signal input a;
signal output powers[6];
powers[0] <== a;
powers[1] <== powers[0] * a;
powers[2] <== powers[1] * a;
powers[3] <== powers[2] * a;
powers[4] <== powers[3] * a;
powers[5] <== powers[4] * a;
}
component main = Powers();
虽然我们得到了一个完全相同的 R1CS,但那段代码非常丑陋。然而,这个例子有效地说明了任何在计算中使用变量的电路都可以重写为不包含变量的形式。
变量构建了存在于 R1CS 外部的辅助代码。它们有助于定义电路,但它们不是电路的一部分。
变量 var i 仅仅是在构建电路时用于跟踪循环迭代的记账工具,它并不属于约束的一部分。
信号与变量
信号是不可变的,并且旨在成为 R1CS 的列之一。变量不是 R1CS 的一部分。它是用于在 R1CS 之外计算值以帮助定义 R1CS 的。
像某些语言所定义的那样,将信号视为“不可变变量”,将变量视为“可变变量”,这是不准确的。信号不可变的原因在于 R1CS 中的 witness 条目具有固定值。在 R1CS 中,一个值会改变的解向量是没有意义的,因为您无法为它创建证明。
<--、<== 和 === 运算符是与信号一起使用的,而不是变量。我们很快就会解释这些不熟悉的运算符。
当处理变量时,Circom 表现得就像普通的类 C 语言一样。运算符 =、==、>=、<= 和 !=、++、-- 的行为符合您的预期。这就是为什么循环的示例看起来很眼熟。
以下示例是不允许的:
signal a;
a = 2; // using a variable assignment for a signal
var v;
v <-- a + b; // using a signal assignment for a variable is not allowed
=== 与 <==
以下电路是等价的:
pragma circom 2.1.6;
template Multiply() {
signal input a;
signal input b;
signal output c;
c <-- a * b;
c === a * b;
}
template MultiplySame() {
signal input a;
signal input b;
signal output c;
c <== a * b;
}
<== 运算符先计算,再赋值,然后添加一个约束。如果您只想进行约束,请使用 ===。
通常,当您试图强制要求 <-- 分配了正确的值时,会使用 === 运算符。在我们查看 IsZero 模板时,您将看到它的实际应用。
但在那之前,让我们看一个真实的例子。假设我们希望证明者同时提供输入和输出。这就是我们使用 === 运算符的方法。
pragma circom 2.1.6;
template Multiply() {
signal input a;
signal input b;
signal input c;
c === a * b;
}
component main {public [c]} = Multiply();
Circom 并不要求输出信号一定要存在,因为那仅仅是公开输入的语法糖。记住,从零知识证明的角度来看,“输入”仅仅是 witness 向量的一个条目,所以一切都是输入。在上述示例中,并没有输出信号,但这依然是一个带有适当约束的完全有效的电路。
将模板连接在一起
如下例所示,Circom 模板是可重用且可组合的。在这里,Square 是 SumOfSquares 所使用的一个模板。请注意输入 a 和 b 是如何“连接”到组件 Square() 的。
pragma circom 2.1.6;
template Square() {
signal input in;
signal output out;
out <== in * in;
}
template SumOfSquares() {
signal input a;
signal input b;
signal output out;
component sq1 = Square();
component sq2 = Square();
// wiring the components together
sq1.in <== a;
sq2.in <== b;
out <== sq1.out + sq2.out;
}
component main = SumOfSquares();
您可以将 <== 运算符理解为通过引用组件的输入或输出来将它们“连接”在一起。
组件的多个输入
上面的 Square 示例将单个信号作为输入,但如果一个组件有多个输入,按照惯例通常将其指定为 array in[n]。以下组件接受两个数字并返回它们的乘积:
template Mul {
signal input in[2]; // takes two inputs
signal output out; // single output
out <== in[0] * in[1];
}
了解如何将模板连接在一起是引入电路库的前提条件,我们将在接下来的部分中展示这一点。
信号命名惯例
按照惯例,输入信号通常命名为 in 或 array in[],而 output 信号则命名为 out 或 out[]。
不安全的次方运算,小心使用 <--
当遇到二次约束问题时,您可能会想使用 <-- 运算符来消除编译器的报错。以下代码可以编译,且似乎实现了与我们之前的次方运算示例相同的功能。
pragma circom 2.1.6;
template Powers {
signal input a;
signal output powers[6];
powers[0] <== a;
powers[1] <== a * a;
powers[2] <-- a ** 3;
powers[3] <-- a ** 4;
powers[4] <-- a ** 5;
powers[5] <-- a ** 6;
}
component main = Powers();
然而,当我们生成 R1CS 时,我们却只有一个约束!
(base) ➜ hello-circom circom bad-powers.circom --r1cs
template instances: 1
non-linear constraints: 1 ### only one constraint ###
linear constraints: 0
public inputs: 0
public outputs: 6
private inputs: 1
private outputs: 0
wires: 7
labels: 8
Written successfully: ./powers.r1cs
Everything went okay, circom safe
由于只有一个约束,证明者只需正确设置数组中的第一个元素,而其他 5 个元素可以填入任何他们想要的值!您绝对不能相信由这样一种电路生成的证明!
欠约束(Underconstraints)是零知识应用中主要的安全性 bug 来源,因此请反复检查约束是否如您预期地在 R1CS 中生成!
这就是为什么我们强调在学习 Circom 语言之前要先了解 Rank 1 Constraint System,否则有一整类的 bug 是您难以察觉的!
您可以在我们的另一个教程中学习如何利用欠约束的 ZK 电路(exploit underconstrained ZK circuits)。
何时使用 <--
如果 <-- 会导致欠约束,为什么该语言还要包含这样一个容易搬起石头砸自己脚的设计(foot gun)呢?
当使用电路而不是自然代码来描述算法时,应该采用的思维模式是“先计算,后约束(compute, then constrain)”。某些操作如果仅用纯约束来建模会极其困难。下一节将展示此类情形的一个例子。
Circomlib
Iden3 维护了一个名为 circomlib 的有用的 Circom 模板库。至此,我们已经具备了足够的 Circom 前置知识来开始研究这些模板,而现在正是引入一个展示 <-- 用法的简单且实用的模板的好时机。
IsZero
IsZero 模板在输入信号为零时返回 1,在输入信号为非零时返回 0。
如果您花些时间思考如何仅通过乘法来测试一个数字是否为零,您会发现自己陷入困境;事实证明,这是一个极其困难的问题。
让我们看看 circomlib 组件 IsZero 是如何实现这一点的。
template IsZero() {
signal input in;
signal output out;
signal inv;
inv <-- in!=0 ? 1/in : 0;
out <== -in*inv +1;
in*out === 0;
}
在上述示例中,inv 是一个辅助输入信号,旨在更容易地创建有效电路。我们在 R1CS 外部计算出 inv 为零或者为 in 的倒数,然后将其作为约束的一部分强制要求 inv 必须正确。这遵循了“先计算,后约束”的模式。
信号 inv 依然被约束为零或是 in 的模逆元。
作为读者的一个练习,请画出展示以下可能组合的真值表:
out:
inv:
in:
您将看到,要满足这些约束,只有当 in 为 0 时将 out 设为 1,以及当 in 为非零时将 out 设为 0。您不能随意篡改 inv,它必须遵循规则。这充分阐释了“先计算,后约束”的模式。
该箭头创建了一个约束同时赋值。在上面的代码中,out 被约束为等于 -in*inv + 1。然而,最后一行并没有将 0 赋值给 in*out。相反,它强制要求 in*out 确实等于 0。
尽管您通常会在处理变量时使用三元运算符(或通常的类 C 语法),但如果您使用 <-- 运算符,您也可以将传统编程语法应用于信号。
**读者练习:**您能在不使用 IsZero 模板的情况下,创建一个实现与 IsZero 相反功能的模板吗?
如果操作不是二次的并且开启了优化器,=== 和 <== 不会创建约束
这里需要留意一个编译器的怪异现象(quirk):
template FactorOfFiveFootgun() {
signal input in;
signal output out;
out <== in * 5;
}
component main = FactorOfFiveFootgun();
在这里,我们声明我们知道 x,使得 5x = out,其中 out 是公开的。因此,如果 out 是 100,我们期望 x 为 20,对吗?但如果我们查看 R1CS,我们会发现它实际上是空的,没有创建任何约束!
这是因为,尽管 <== 代表一个约束,但编译器优化器会消除那些不包含乘法的约束。
当我们将电路编译为 R1CS 时,我们看到它是空的。
(base) ➜ hello-circom circom footgun.circom --r1cs
template instances: 1
non-linear constraints: 0 ### no constraints ###
linear constraints: 0
public inputs: 0
public outputs: 1
private inputs: 1
private outputs: 0
wires: 2
labels: 3
Written successfully: ./footgun.r1cs
Everything went okay, circom safe
然而,如果我们在编译电路时通过以下命令关闭优化器:
circom footgun.circom --r1cs --O0
那么我们会看到一个约束被创建了:
template instances: 1
non-linear constraints: 0
linear constraints: 1 ### Constraint created here
public inputs: 0
private inputs: 1
public outputs: 1
wires: 3
labels: 3
Written successfully: ./footgun.r1cs
Everything went okay
始终健全性检查(sanity check)编译器创建的约束数量。
Circom 中的函数
让 Circom 显得有点令人困惑的一点是,它既是一种用于创建算术约束的语言,又是一种通过编程方式创建约束的语言,并且还是一种用于执行常规计算的语言。
以下是一个将计算分离到函数中的示例。请注意,这里的“平均值”是使用模算术(modular arithmetic)计算的,因此它并不等同于传统的算术平均值。
pragma circom 2.1.6;
include "node_modules/circomlib/circuits/comparators.circom";
function invert(x) {
return 1 / x;
}
template Average(n) {
signal input in[n];
signal denominator;
signal output out;
var sum;
for (var i = 0; i < n; i++) {
sum += in[i];
}
denominator <-- invert(n);
component eq = IsEqual();
eq.in[0] <== denominator;
eq.in[1] <== n;
0 === eq.out;
out <== sum * denominator;
}
component main = Average(5);
如果约束依赖于条件的值,那么它在约束生成阶段可能是未知的
在编写 circom 代码时,还有一个容易犯的错误:信号不能作为 if 语句或循环的输入。
template IsOver21() {
signal input age;
signal output oldEnough;
if (age >= 21) {
oldEnough <== 1;
} else {
oldEnough <== 0;
}
}
如果您尝试编译上述代码,您将得到本节标题中所述的错误。如果您使用信号来决定循环的执行次数,您也会遇到类似的错误(不信可以试试!)。不允许这样做的原因在于,我们将 R1CS 中约束的数量变成了 R1CS 输入之一的函数,但这毫无意义。
那么,我们该如何检查某人是否年满 21 岁呢?
这实际上比看起来要难,因为在有限域中比较数字是相当棘手的。
在 Circom 中比较数字的陷阱
如果 ,那么那个巨大的数字实际上是大于 1 还是小于 1 呢?
您无法在有限域中比较数字,因为说一个数字大于另一个数字并没有任何意义。
然而,我们仍然希望能比较数字!
在进行任何比较之前,第一个要求是它们必须小于有限域的大小,我们会将有限域中的任何数字视为正整数,并小心防范下溢和溢出。
如果您想一下如何表示以下语句:
仅使用纯粹的 R1CS 表示方式,您会遇到瓶颈。这是不可能做到的。
只要我们强制数字保持在有限域的阶(field order)范围内,我们就可以有意义地比较它们。但把 > 运算符直接转换为一组二次约束是不可能的。
但是,如果我们把域元素转换为数字的二进制表示形式,就可以进行比较。
现在我们可以再引入两个 circomlib 模板:Num2Bits 和 LessThan,其动机是为了比较整数。
Num2Bits
下面的 circomlib Num2Bits 模板展示了 circom 如何将一个信号转换成一个包含其二进制表示形式的信号数组。
template Num2Bits(n) {
signal input in;
signal output out[n];
var lc1=0;
// this serves as an accumulator to "recompute" in bit-by-bit
var e2=1;
for (var i = 0; i<n; i++) {
out[i] <-- (in >> i) & 1;
out[i] * (out[i] -1 ) === 0; // force out[i] to be 1 or 0
lc1 += out[i] * e2; //add to the accumulator if the bit is 1
e2 = e2+e2; // takes on values 1,2,4,8,...
}
lc1 === in;
}
约束一个数字可以用 个比特位表示,等同于说它小于 。
LessThan
在不使用普通的 < 和 > 运算符、且只进行一次二进制转换的情况下,我们如何比较两个 9,999 或更小的数字呢?如果允许我们进行两次二进制转换,这很容易,但这会使电路变得更大。
这是一个棘手的问题,但以下是 circomlib 的做法。
假设我们正在比较 和 。
由于我们的输入可取到的最大值是 9,999,我们给 加上 10,000,然后从 加上 10,000 的和中减去 。
无论如何, 都将是正数,即使 是 9,999 而 是 0。因为我们在这里处理的是有限域元素,我们不希望发生任何下溢,在这种情况下,下溢也不可能发生。
关键在于。如果 ,那么 将介于 10,000 到 19,999 之间;如果 , 将在 的范围内。
要判断一个数字是否在 的范围内,我们只需要看万位的数字,即 1x,xxx。如果那里有一个 ,我们就知道 在 的范围内;如果我们得到的格式是 0x,xxx,那么 必定在最初是大于 的。
Circom 只是在二进制而不是十进制表示法中做着同样的事情。
在十进制的类比中,我们将 10,000 加到一个保证不会大于 9,999 的数字上。在二进制的情况下,我们将以下二进制数:
加到一个保证最多具有 个比特位的数字上。请注意,将 1 左移 位,即 1 << n 是:
要理解为什么会这样,考虑一下当我们计算 1 << 0 和 1 << 1 时, 会变成什么。
这是 Circom 中的 LessThan 模板:
template LessThan(n) {
assert(n <= 252);
signal input in[2];
signal output out;
component n2b = Num2Bits(n+1);
// add 1 << n then subtract the number we are comparing
n2b.in <== in[0] + (1<<n) - in[1];
// check if the n-th bit is 1 or 0
out <== 1-n2b.out[n];
}
该代码通过 进行参数化,即数字在比特位上的最大长度,不过这里有一个强制的 252 位上限,以保持在有限域大小的限制以下,从而避免 别名 bug(alias bug)。
数字不能大于 ,因此加上 1<<n 确保了 in[0] + (1<<n) 这个项始终大于 in[1]。它们的差值被转换为二进制,如果最高位仍然是 1,则表示 in[0] 大于 in[1]。最终的项是 1 减去该位,因此这反转了该位是否存在。
因此,如果 in[0] 小于 in[1],该组件将约束 out 为 1,否则为 0。
Over21 的功能示例
既然我们已经拥有了必备的工具箱,让我们来制作一个真正有效的年龄检查器。
Circomlib 提供了一个名为 GreaterThan 的比较器,它其实是 LessThan 稍微变形得来的,所以我们在这里不再解释它。感兴趣的读者可以直接查阅源代码。
要使用 circomlib 模板,请创建一个空的 node_modules/ 目录,然后运行:
npm install circomlib
然后创建以下电路:
pragma circom 2.1.6;
include "node_modules/circomlib/circuits/comparators.circom";
template Over21() {
signal input age;
signal input ageLimit;
signal output oldEnough;
// 8 bits is plenty to store age
component gt = GreaterThan(8);
gt.in[0] <== age;
gt.in[1] <== 21;
0 === gt.out;
oldEnough <== gt.out;
}
component main = Over21();
这是验证年龄确实超过 21 岁的安全方法(尽管在实际应用中,您需要一个权威机构来证明年龄)。
Comparators.circom
该文件中提供的比较器有:
IsZeroIsEqual(将两个输入相减并将其传递给 IsZero)LessThanLessEqThan(派生自 LessThan)GreaterThan(派生自 LessThan)GreaterEqThan(派生自 LessThan)ForceEqualIfEnabled
最后一个是做什么的?
ForceEqualIfEnabled
ForceEqualIfEnabled 模板的代码如下所示:
template ForceEqualIfEnabled() {
signal input enabled;
signal input in[2];
component isz = IsZero();
in[1] - in[0] ==> isz.in;
(1 - isz.out)*enabled === 0;
}
ForceEqualIfEnabled 允许我们“开启和关闭约束”。它的行为类似于条件约束,或者说一个 if 语句。如果 enabled 为 0,那么 in[0] 是否等于 in[1] 就无所谓了;该约束实际上被忽略了,因为最终的约束将是 0 === 0。另一方面,如果 enabled 不为 0,那么 1 - isz.out 必须为 0(即 in[1] 等于 in[0]),约束才能通过。
Circom 的 assert
令人困惑的是,Circom 拥有一个 assert 语句,它的功能与您的预期并不完全相符。
它仅仅是一个安全检查,防止开发者创建具有不良特性的电路。
例如,我们可能会使用它来确保模板不会用长度为零的数组进行初始化,如果那样会导致可能被零除的错误。
您应始终假设恶意的证明者可以随意复制电路代码,删除 assert 语句,然后生成证明。该证明将与电路兼容,因为电路没有将 assert 语句纳入(为约束)。
布尔运算符
希望您现在已经知道,不能对信号使用本应针对变量的运算符。以下代码将无法编译:
template And() {
signal input in[2];
signal output c;
c <== in[0] && in[1];
}
请记住,信号是有限域元素,而 && 不是适用于有限域元素的有效运算符。
然而,如果您将 a 和 b 约束为 0 和 1,您就可以约束 c、a 和 b 遵循 AND(与)门的行为。
template And() {
signal input in[2];
signal output c;
// force inputs to be zero or one
in[0] === in[0] * in[0];
in[1] === in[1] * in[1];
// c will be 1 iff in[0] and in[1] are 1
c <== in[0] * in[1];
}
思考如何完成其他布尔运算(NOT、OR、NAND、NOR、XOR 和 XNOR)对读者来说是一个有用的练习。尽管每个布尔门都可以由一个 NAND(与非)门构成,但这会使电路大得不必要,所以不要过度重用布尔门。
解决方案位于 circomlib 的 gates.circom 文件中。请注意,它们并没有将输入约束为零或一,这取决于电路设计者去实现。
对 ZK 友好的哈希函数
您可以想象,使用电路生成方法来构建一个哈希函数会非常庞大。让我们看看一个接受 256 比特位输入的 sha256 哈希器会有多大:
pragma circom 2.0.0;
include "node_modules/circomlib/circuits/sha256/sha256.circom";
component main = Sha256(256);
这个看似不起眼的小电路将产生近 30,000 个约束:
(base) ➜ hello-circom circom Sha256-example.circom --r1cs
template instances: 99
non-linear constraints: 29380 ### WOW! ###
linear constraints: 0
public inputs: 0
public outputs: 256
private inputs: 256
private outputs: 0
wires: 29325
labels: 204521
Written successfully: ./Sha256-example.r1cs
Everything went okay, circom safe
传统的密码学哈希函数具有这么多约束的原因在于,它们对 32 位数字进行操作,因此有限域元素必须受到约束以“模拟”32 位数字。
这给证明者带来了巨大的工作量。作为回应,研究社区已开发出了为电路表示形式而优化的哈希函数。除了 sha256 之外,您还会发现:
- Mimc
- Pedersen
- Poseidon
另一方面,对 ZK 友好的哈希函数直接使用有限域元素,并避免了增加大量约束的操作(例如位移或 XOR 操作)。
比较哈希函数输出 R1CS 的大小是留给读者的一个练习。请记住,某些函数将“轮数(rounds)”作为参数,这自然会增加电路的大小。
ZK 友好的哈希函数是一个宏大的主题,最好在单独的讨论中进行,因此我们将推迟到未来的文章中再讨论。
剩下的内容呢?
其余的模板由于足够短小而不言自明,或者是与零知识数字签名方案及计算椭圆曲线相关的。
在 ZK 电路内部计算椭圆曲线的动机在于,某些对 ZK 友好的哈希函数依赖于椭圆曲线作为核心原语。
这是另一个宏大的主题,我们将推迟到另一篇文章中讨论。
从真实的现实世界示例中学习 Circom
两个值得研究的经典且易于上手的电路是 Tornado Cash 和 Semaphore。
在 RareSkills 了解更多
学习 circom 的最佳方式就是使用它。我们的 Zero Knowledge Puzzles 提供了复杂性递增的小型挑战,以便您学习该语言。这里提供了一个带有单元测试的开发环境,在您成功完成谜题时通知您。请注意,欠约束的电路也可能通过测试,因为在通常情况下测试欠约束是极其困难的。至少,您应该检查生成的约束数量,并确保该数量是合理的。
本材料是我们零知识课程的一部分。请查看项目以了解更多。
最初发布于 2023 年 9 月 26 日