Circom 语言教程与 circomlib 演示

Circom 语言教程与 circomlib 演示

本教程介绍了 Circom 语言及其使用方法,以及常见的陷阱。我们还将解释 circomlib 库的一部分,以介绍常见的设计模式。

关于生产使用的说明

Circom 是学习 zk-snarks 的绝佳工具。然而,由于它是相当底层的,因此意外添加微妙的错误的可能性更多。在实际应用中,程序员应考虑使用更高级的零知识编程语言。在部署持有用户资金的智能合约之前,你应始终进行审计,但对于 zk 电路来说,这一点尤为重要,因为攻击向量不太为人所知。

前提条件

虽然在 Circom 中编程而不理解R1CS(Rank 1 Constraint System)是可能的,但如果你理解了它,你将更容易开发出对该语言的心理模型。Circom 本质上是一个用于创建 Rank 1 Constraint System 的对人更友好的封装。

强烈建议你首先学习它,否则你将无法完全理解“underconstrained”这个术语的背景。我们还建议你阅读我们的zk 电路文章,以了解它们存在的动机。

安装

按照这里的步骤安装 circom

你还需要安装snarkjs

npm install -g snarkjs@latest

Hello World

zk-circuits 的 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

记住,在处理算术电路时,所有操作都在有限域中进行,所以你看到的巨大数字实际上是“-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.a ] * [ main.b ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.s1 ] = 0
[INFO]  snarkJS: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.s1 ] * [ main.c ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.out ] = 0

通过一些代数运算,我们可以得到以下结果

a * b  = s1
s1 * c = out

我们可以看到这与电路中的相同计算相匹配。

计算见证(witness)

运行以下命令以创建生成见证向量的代码

circom multiply.circom --r1cs --sym --wasm

这将重新生成 R1CS 和符号(symbol)文件,并创建一个名为 multiply_js/的文件夹。切换到该文件夹。

接下来,我们需要在该文件夹中创建一个 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;

现在我们使用以下命令计算并导出证明:

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"
]

计算得到的证明具有值[1, 30, 2, 3, 5, 6]。2、3 和 5 是输入,6 是中间信号 s1,它是 2 和 3 的乘积。

这符合 R1CS 变量的预期布局,形式为[1, out, a, b, c, s1]。

公共输入

如果我们想要将某些输入设为公共输入怎么办?例如,在 nullifier 方案中,我们对两个数字的连接进行哈希,并稍后揭示其中一个数字。

动机:nullifier 方案

快速说明一下,nullifier 方案通过连接两个数字然后对它们进行哈希运算来工作。它们在我们有一组哈希值的情况下使用,我们想要证明我们知道其中一个哈希值的原像(preimage: 原始的值),而不暴露它是哪一个。

如果哈希值只是一个数字的哈希,那么揭示该数字将会表明我们知道哈希对应的原像是哪一个。然而,如果我们不揭示任何信息,我们可以重复多次证明我们知道其中一个哈希值的原像(preimage)的操作。如果这个操作涉及从智能合约中提取资金,那将是非常有问题的!

通过揭示两个哈希数字中的一个,我们不能再次使用原像,但我们也不会揭示我们所知道哈希的原像是哪一个,因为仅揭示两个数字中的一个是不够的。

以下是 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)。

一个 R1CS 必须是固定且不可变的,这意味着一旦定义了行数或列数,我们就不能更改它们,也不能更改矩阵或证明的值。这就是为什么最后一行有一个硬编码的参数 Powers(6),这个大小必须是固定的。

然而,如果我们以后想要重用这段代码来支持不同大小的电路,那么让模板能够根据需要改变大小会更加方便。因此,组件可以接受参数来参数化控制流和数据结构,但这必须是每个电路固定的。

变量

上面的示例等同于以下内容

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只是用于跟踪循环迭代的记账变量,在构建电路时使用,它不是约束的一部分。

信号(Signal) vs 变量(variable)

信号是不可变的,旨在成为 R1CS 的列之一。变量不是 R1CS 的一部分。它用于在 R1CS 之外计算值,用来帮助定义 R1CS。

将信号视为“不可变变量”和变量视为“可变变量”(某些语言的赋值方式)是不准确的。信号不可变的原因是因为 R1CS 中的见证条目具有固定的值。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 &lt;-- a * b;
    c === a * b;
}

template MultiplySame() {
    signal input a;
    signal input b;
    signal output c;

    c &lt;== a * b;
}

&lt;==操作符先计算,然后赋值,然后添加约束。如果你只想约束,使用===

通常,当你试图强制&lt;--分配正确的值时,你需要使用===操作符。当我们查看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 不需要存在输出信号,因为那只是对公共输入的一种语法糖。请记住,从零知识证明的角度来看,“输入”只是见证向量的一个条目,因此从零知识证明的角度来看,一切都是输入。在上面的示例中,没有输出信号,但这是一个具有适当约束的完全有效的电路。

将模板连接在一起

Circom 模板是可重用和可组合的,如下面的示例所示。在这里,Square 是 SumOfSquares 使用的一个模板。请注意,输入 a 和 b 如何“连接(wired)”到组件 Square()。

pragma circom 2.1.6;

template Square() {

    signal input in;
    signal output out;

    out &lt;== in * in;
}

template SumOfSquares() {
    signal input a;
    signal input b;
    signal output out;

    component sq1 = Square();
    component sq2 = Square();

    // 连接(wiring)组件
    sq1.in &lt;== a;
    sq2.in &lt;== b;

    out &lt;== sq1.out + sq2.out;
}

component main = SumOfSquares();

你可以将&lt;==运算符视为通过引用它们的输入或输出将组件“连接”在一起。

组件的多个输入

上面的 Square 示例接受单个信号作为输入,但如果一个组件接受多个输入,通常将其指定为一个数组 in[n]。下面的组件接受两个数字并返回它们的乘积:

template Mul {

    signal input in[2]; // takes two inputs
    signal output out; // single output

    out &lt;== in[0] * in[1];
}

了解如何将模板连接在一起是我们引入电路库的前提,我们将在接下来的部分中展示。

信号命名约定

按照惯例,将输入信号命名为 in 或作为数组 in[],将输出信号命名为 out 或 out[]。

不安全的 Powers,请注意&lt;--

当遇到二次约束问题时,使用<--运算符来消除编译器警告可能是诱人的。下面的代码可以编译,并且似乎实现了与我们之前的 powers 示例相同的功能。

pragma circom 2.1.6;

template Powers {
    signal input a;
    signal output powers[6];

    powers[0] &lt;== a;
    powers[1] &lt;== a * a;
    powers[2] &lt;-- a ** 3;
    powers[3] &lt;-- a ** 4;
    powers[4] &lt;-- a ** 5;
    powers[5] &lt;-- 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)是零知识应用中安全漏洞的主要来源,因此请再三检查约束是否按照你的预期在 R1CS 中生成!

这就是为什么我们强调在学习 Circom 语言之前要先理解 R1CS(Rank 1 Constraint Systems),否则会有一整类难以检测的错误!

何时使用 <--

如果 &lt;-- 导致了欠约束(Underconstraints),为什么语言会包含这样的陷阱?

当使用电路描述算法而不是自然代码描述算法时,应采用“计算,然后约束”的思维方式。有些操作仅通过纯约束模型非常困难。考虑以下示例。

Circomlib

Iden3 维护着一个有用的 circom 模板仓库,称为 circomlib。此时,我们已经掌握了足够的 Circom 知识,可以开始学习这些模板了。现在是介绍一个简单但有用的模板,演示了 &lt;-- 的使用的好时机。

IsZero

IsZero 模板在输入信号为零时返回 1,非零时返回零。

如果你花一些时间思考如何仅使用乘法来测试一个数是否为零,你会发现自己陷入困境;这将变成一个非常困难的问题。

让我们看看 circomlib 组件 IsZero 是如何实现这一点的。

template IsZero() {
  signal input in;
  signal output out;

  signal inv;

  inv &lt;-- in!=0 ? 1/in : 0;

  out &lt;== -in*inv +1;
  in*out === 0;
}

在上面的示例中,inv 是一个辅助输入信号,使得创建一个有效电路更容易。我们在 R1CS 之外计算 inv,使其成为零或 x 的倒数,然后将 inv 作为约束的一部分强制为正确值。这遵循“计算,然后约束”的模式。

但为什么将 inv 设为信号而不是变量?它似乎只是临时使用。如果我们将 inv 设置为变量并将 <-- 替换为 =,我们将得到非二次约束错误,因为我们将信号与变量相乘,而该变量是从某个非平凡计算中派生出来的——这个计算肯定涉及多个乘法。

此外,信号 inv 仍然受到约束。

作为读者的练习,请绘制一个真值表,显示以下可能的组合。

out: {1,0}

inv: {0, in^{-1}, invalid}

in: {0, non-zero}

你会发现只有在 in 为 0 时,将 out 设置为 1 才能满足约束条件,在 in 为非零时,将 out 设置为 0。你不能随意更改 inv,它必须遵循规则。这说明了“先计算,然后约束”的模式。

箭头创建了一个约束并赋予了一个值。在上面的代码中,out 被约束为等于-in inv + 1。然而,最后一行并没有将 in out 赋值为零。相反,它强制要求 in * out 确切等于零。

尽管通常情况下你会使用三元运算符(或类似 C 语法)与变量一起使用,但如果使用<--运算符,你可以使用传统的编程语法与信号一起使用。

读者练习:你能否创建一个与 IsZero 相反的模板,而不使用 IsZero 模板?

在约束信号乘积时,请使用 IsEqual 模板而不是===

当比较相等的组件时,你可以使用IsEqual 模板,它会对输入进行减法运算,并通过 IsZero 组件进行处理 - 如果它们相等,则输出将为零。

以下两个部分展示了这一动机。

template IsEqual() {
    signal input in[2];
    signal output out;

    component isz = IsZero();

    in[1] - in[0] ==> isz.in;

    isz.out ==> out;
}

如果操作不是二次的,===和<==将不会创建约束

这是另一个需要注意的欠约束陷阱

template FactorOfFiveFootgun() {

    signal input in;
    signal output out;

    out &lt;== 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

解决方案是将 IsEqual 模板连接起来以强制执行相等性。这留给读者作为练习。

示例:计算平均值

假设我们想要计算一个信号数组的平均值。在常规编程中,这很容易实现,但仅使用二次约束,这将异常困难。

解决方案是使用常规编程计算平均值,然后将输出约束为正确的值。

n 个信号的平均值等于它们的总和除以信号的数量。在有限域中,除法等同于乘以倒数,因此我们需要将信号相加,然后乘以数组长度的倒数。

我们需要证明长度的倒数确实是长度的倒数,因为我们在没有约束的情况下计算它。

以下内容看起来是正确的,但实际上并不能实现所需的行为:

pragma circom 2.1.6;

include "node_modules/circomlib/circuits/comparators.circom";

template AverageWrong(n) {

    signal input in[n];
    signal denominator;
    signal output out;

    // sum up the inputsvar sum;
    for (var i = 0; i &lt; n; i++) {
        sum += in[i];
    }

    // compute the denominator
    denominator_inv &lt;-- 1 / n;

    // "force" the denominator to be equal to the inverse of n1 === denominator_inv * n; // this does not create a constraint!// sum / denominator
    out &lt;== sum * denominator_inv;
}

component main  = AverageWrong(5);

当编译上述电路时,我们得到零个约束!

在将信号与常量进行比较时,请使用 IsEqual 组件,而不是===

以下是正确的方法:

pragma circom 2.1.6;

include "node_modules/circomlib/circuits/comparators.circom";

template Average(n) {

    signal input in[n];
    signal denominator_inv;
    signal output out;

    var sum;
    for (var i = 0; i &lt; n; i++) {
        sum += in[i];
    }

    denominator_inv &lt;-- 1 / n;

    component eq = IsEqual();
    eq.in[0] &lt;== 1;
    eq.in[1] &lt;== denominator_inv * n;

    out &lt;== sum * denominator_inv;

}

component main  = Average(5);

现在,当我们计算 R1CS 时,我们实际上可以看到总和被约束为信号的总和,分母被约束为 n 的倒数。

具体来说,你可以看到 R1CS 将 n 个数组相加并乘以分母,然后检查它是否等于输出。

以下三个约束确保分母确实正确计算。

[INFO]  snarkJS: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.in[0] +21888242871839275222246405745257275088548364400416034343698204186575808495616main.in[1] +21888242871839275222246405745257275088548364400416034343698204186575808495616main.in[2] +21888242871839275222246405745257275088548364400416034343698204186575808495616main.in[3] +21888242871839275222246405745257275088548364400416034343698204186575808495616main.in[4] ] * [ main.denominator ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.out ] = 0

[INFO]  snarkJS: [ 51 +21888242871839275222246405745257275088548364400416034343698204186575808495616main.denominator ] * [ main.eq.isz.inv ] - [ 1 +21888242871839275222246405745257275088548364400416034343698204186575808495616main.eq.out ] = 0

[INFO]  snarkJS: [ 51 +21888242871839275222246405745257275088548364400416034343698204186575808495616main.denominator ] * [ main.eq.out ] - [  ] = 0

故事的寓意是始终对 R1CS 约束进行合理检查!

circom 中的函数

如果我们要处理大量变量,我们可以将它们封装到自己的函数中,以保持代码的整洁性。考虑以下示例。

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 &lt; n; i++) {
        sum += in[i];
    }

    denominator &lt;-- invert(n);

    component eq = IsEqual();
    eq.in[0] &lt;== denominator;
    eq.in[1] &lt;== n;

    out &lt;== sum * denominator;
}

component main  = Average(5);

约束取决于条件的值,而在约束生成阶段可能是未知的

在编写 circom 代码时,这是另一个容易犯的错误:信号不能作为 if 语句或循环的输入。

template IsOver21() {
    signal input age;
    signal output oldEnough;

    if (age >= 21) {
        oldEnough &lt;== 1;
    } else {
        oldEnough &lt;== 0;
    }
}

如果尝试编译上述代码,你将得到本节标题中的错误。如果使用信号确定执行循环的次数,也会出现类似的错误(试试看!)。之所以不允许这样做,是因为我们使 R1CS 中的约束数量成为 R1CS 输入之一的函数,但这是没有意义的。

那么我们如何检查某人是否超过 21 岁呢?

这实际上比看起来要困难,因为在有限域中比较数字是相当棘手的。

在 Circom 中比较数字的陷阱

如果 1 - 2 = 21888242871839275222246405745257275088548364400416034343698204186575808495616,那么这个巨大的数字实际上是大于 1 还是小于 1 呢?

在有限域中,无法比较数字,因为说一个数字比另一个数字大没有意义。

然而,我们仍然希望能够比较数字!

在进行任何比较之前,首先要求它们必须小于域的大小,并且我们将把域中的任何数字视为正整数,并小心防止下溢和上溢。

如果你思考一下如何使用纯粹的 R1CS 表示来表示以下语句

a > b

你会陷入困境。这是不可能的。

只要我们强制数字保持在域的顺序内,那么我们就可以有意义地比较它们。将 > 运算符转换为一组二次约束是不可能的。

然而,如果我们将一个域元素转换为数字的二进制表示,那么就可以进行比较。

现在我们可以引入另外两个 circomlib 模板:Num2Bits 和 LessThan,其目的是比较整数。

Num2Bits

如果我们不使用常规的 < 和 > 运算符,只使用一次二进制转换,如何比较两个小于等于 9,999 的数字呢?如果允许两次二进制转换,这很容易,但电路会变得更大。

这是一个棘手的问题,但这就是 circomlib 的解决方法。

假设我们正在比较 x 和 y。

由于我们的输入的最大值是 9,999,我们将 x 加上 10,000,并将 y 从 x 和 y 的和中减去。

z = (10,000 + x) - y

无论如何,z 都将是正数,即使 y 是 9,999,x 是 0。由于我们在处理域元素,我们不希望发生任何下溢,而在这种情况下,不会发生下溢。

这是关键部分。如果 x ≥ y,则 z 将在 10,000 到 19,999 之间,如果 x < y,则 z 将在 [0-9,999] 范围内。

要判断一个数字是否在范围[10,000-19,999]内,我们只需要查看万位上的数字,即1x,xxx。如果在这里有一个 1,那么我们就知道 z 在范围[10,000-19,999]内,如果是0x,xxx 的形式,那么 y 必须原本大于 x。

Circom 在二进制表示中做的事情与十进制表示相同。

以下是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&lt;n; i++) {
        out[i] &lt;-- (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

现在我们掌握了 Num2Bits,理解LessThan 模板应该很简单。

template LessThan(n) {
    assert(n &lt;= 252);
    signal input in[2];
    signal output out;

    component n2b = Num2Bits(n+1);

    n2b.in &lt;== in[0] + (1&lt;&lt;n) - in[1];

    out &lt;== 1-n2b.out[n];
}

该代码是由 n 参数化的,n 是数字的最大位数,但有一个强制上限为 252 位。

这些数字不能大于 2^n,因此添加 1<<n 确保 in[0] + (1<<n)始终大于 in[1]。差异被转换为二进制,如果最高位仍为 1,则 in[0]大于 in[1]。最终的项是 1 减去该位,因此这反转了该位是否存在。

因此,如果 in[0]小于 in[1],该组件返回 1。

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] &lt;== age;
    gt.in[1] &lt;== 21;

    oldEnough &lt;== gt.out;
}

component main = Over21();

这是验证年龄是否真的超过 21 的安全方式(尽管在实际应用中,你需要有一个权威机构来证明年龄)。

Comparators.circom

这个文件中提供的比较器有:

  • IsZero
  • IsEqual(将两个输入相减并将结果传递给 IsZero)
  • LessThan
  • LessEqThan(由 LessThan 派生)
  • GreaterThan(由 LessThan 派生)
  • GreaterEqThan(由 LessThan 派生)
  • 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 模板的行为类似于 assert 语句,通过包含一个约束条件来确保输入必须相等。它不会返回 true 或 false(这里没有输出信号来返回零或一),而是会导致电路不可满足,如果输入不相等。

Circom assert

令人困惑的是,Circom 有一个 assert 语句,但它并不完全符合你的期望。

assert 语句不会添加任何约束,它只是对非恶意证明者的输入进行一次健全性检查。

例如,我们可以使用它来确保模板不会初始化长度为零的数组,如果这样做可能导致除以零的情况。

你应该始终假设恶意证明者可以复制电路代码,删除 assert 语句,并创建一个证明。该证明将与电路兼容,因为电路不包含 assert 语句。

布尔运算符

希望你现在已经知道不能在信号上使用变量的运算符。以下代码将无法编译:

template And() {

    signal input in[2];
    signal output c;

    c &lt;== in[0] && in[1];
}

记住,信号是域元素,&&不是域元素的有效运算符。

然而,如果将 a 和 b 约束为零和 1,你可以使用乘法来实现相同的效果:

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 &lt;== in[0] * in[1];
}

读者可以思考如何实现其他布尔运算,如非、或、与非、或非、异或和同或。虽然每个布尔门都可以由与非门构建,但这会使电路比必要的更大,所以不要过度重用门。

解决方案在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

这给证明者带来了大量的工作。作为回应,研究界已经提出了针对电路表示进行优化的哈希函数。除了 sha256 之外,你还会发现:

  • Mimc
  • Pedersen
  • Poseidon

读者可以比较哈希函数的输出 R1CS 的大小。请记住,其中一些函数将“轮数”作为参数,这自然会增加电路的大小。

ZK 友好的哈希函数是一个庞大的主题,最好单独讨论,因此我们将其推迟到以后的文章中。

其他的呢?

其余的模板足够小,可以自解释,或者与零知识数字签名方案和计算椭圆曲线相关。

在 zk 电路中计算椭圆曲线的动机是一些 zk 友好的哈希函数依赖于椭圆曲线作为核心原语。

这是另一个庞大的主题,我们将其推迟到另一篇文章中。

从真实世界的例子中学习 Circom

两个经典而易于理解的电路供学习的例子是Tornado CashSemaphore


本翻译由 DeCert.me 协助支持, 在 DeCert 构建可信履历,为自己码一个未来。

点赞 1
收藏 0
分享
本文参与登链社区写作激励计划 ,好文好收益,欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
翻译小组
翻译小组
0x9e64...7c84
大家看到好的文章可以在 GitHub 提 Issue: https://github.com/lbc-team/Pioneer/issues 欢迎关注我的 Twitter: https://twitter.com/UpchainDAO