中间信号与子组件

Circom 的主要目的是编译成 Rank 1 Constraint System (R1CS)，但其辅助目的是填充 witness。

对于大多数电路来说，一些信号的值决定了其余信号的值。

例如，向以下模板提供 c 作为输入可能显得有点多余，因为它的值完全取决于 a 和 b：

template Mul() {
  signal input a;
  signal input b;
  signal input c;

  c === a * b;
}

接下来是一个更具激励性的例子。

分解非二次约束

假设我们要为 a * b * c === d 创建一个 R1CS。由于 R1CS 允许每个约束一次乘法，因此我们必须创建另一个信号 s 和一个额外的约束来分解乘法：

template Mul3() {
  signal input a;
  signal input b;
  signal input c;
  signal input d;

  signal input s;

  s === a * b;
  d === s * c;
}

每次我们进行多次乘法运算时，都提供另一个输入将非常繁琐，尤其是在具有大量乘法运算的更大电路中。此外，上面示例中 s 的值确定性地取决于 a 和 b。

中间信号和赋值

为了避免提供 s 的麻烦，Circom 提供了 ==> 和 <== 运算符，用于将 s 的值分配为由 Circom 计算得到（请记住 Circom 的部分功能是生成 witness）。因此，s 的值不需要作为输入提供。==> 和 <== 运算符（精确地）表示“分配和约束”：

template Mul3() {
  signal input a;
  signal input b;
  signal input c;
  signal input d;

  // 不再是输入
  signal s;

  a * b ==> s;
  s * c === d;
}

Circom 对箭头的方向很灵活，a * b ==> s 与 s <== a * b 含义相同。

在上面的代码中，s 被称为 中间信号。中间信号是一个使用 signal 关键字定义的信号，没有 input 关键字。因此，signal s 是一个中间信号，但 signal input a 不是。

上述两个模板之间的底层 R1CS 是相同的。==> 只是省去了我们提供作为输入一部分的 s 值的麻烦。

假设 witness 向量 $\mathbf{w}$ 表示为 [1, a, b, c, d, s]，则底层 R1CS 如下：

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

这可以被认为是将 witness [1, a, b, c, d, _] 传递给 Circom，Circom 基于输入计算完整的 witness [1, a, b, c, d, s]。

对 s 的赋值发生在 R1CS 之外。R1CS 仅检查 witness 向量 $\mathbf{w}$ 是否满足矩阵方程。R1CS 期望提供 witness，并且不计算其任何值。这种方法简化了电路设计并减少了手动工作，同时保持 R1CS 结构不变。

信号值不能用 <== 重新分配

信号表示 witness 向量中的一个具体条目。因此，一旦设置了值，就无法更改它。因此，以下代码将无法编译：

template CannotReassign() {
  signal input a;
  signal input b;

  signal c;

  c <== a * b;

  // 不允许
  // c 已经设置
  c <== a * a;
}

实际示例：检查数组的乘积

电路中的乘法越多，==> 运算符就越方便，因为它节省了提供额外输入信号的麻烦。

假设我们想要强制输入信号 k 是数组 in[n] 中所有信号的乘积的结果。换句话说，我们正在检查：

$$ \prod_{i=0}^{n – 1}\texttt{in}[i]===k $$

这将引入大量的中间信号。为了保持代码的整洁，我们可以将所有中间信号分配给一个单独的数组，如下所示：

template KProd(n) {
  signal input in[n];
  signal input k;

  // 中间信号数组
  signal s[n];

  s[0] <== in[0];
  for (var i = 1; i < n; i++) {
    s[i] <== s[i - 1] * in[i];
  }

  k === s[n - 1];
}

基于上面的代码，s[n - 1] 保存着值

$$ \prod_{i=0}^{n – 1}\texttt{in}[i] $$

然后我们可以约束它等于 k。

将 Circom 分解为模板

现在我们了解了 <== 运算符，我们可以了解 Circom 如何使用模板来使代码更模块化。

与我们的 Mul3 示例类似，假设我们有一个电路，它接受 3 个输入并强制它们的乘积为第 4 个（以下是重新生成的代码）：

template Mul3() {
  signal input a;
  signal input b;
  signal input c;
  signal input d; // d === a * b * c

  // 不再是输入
  signal s;

  a * b ==> s;
  s * c === d;
}

但是假设我们需要对八个输入执行两次此操作。在这种情况下，可能会很想为输入 (a,b,c,d) 和 (x,y,z,u) 复制并粘贴代码两次，这将很难看。

template Mul3x2() {
  signal input a;
  signal input b;
  signal input c;
  signal input d; // d === a * b * c

  signal input x;
  signal input y;
  signal input z;
  signal input u; // u === x * y * z

  // 此处为丑陋的代码
}

取而代之的是，我们可以将 Mul3 作为一个单独的模板，如下所示：

// 单独的模板
template Mul3() {
  signal input a;
  signal input b;
  signal input c;
  signal input d; // d === a * b * c

  // 不再是输入
  signal s;

  a * b ==> s;
  s * c === d;
}

// 主要组件
template Mul3x2() {
  signal input a;
  signal input b;
  signal input c;
  signal input d; // d === a * b * c

  signal input x;
  signal input y;
  signal input z;
  signal input u; // u === x * y * z

  component m3_1 = Mul3();
  m3_1.a <== a;
  m3_1.b <== b;
  m3_1.c <== c;
  m3_1.d <== d;

  component m3_2 = Mul3();
  m3_2.a <== x;
  m3_2.b <== y;
  m3_2.c <== z;
  m3_2.d <== u;
}

值得注意的是：

• 我们使用语法 component m3_1 = Mul3(); 声明组件。这与我们用来声明主组件的语法相同。
• 我们使用 <== 运算符“连接”信号。
• 上面的代码完全等同于复制并粘贴 Mul3 的核心逻辑两次。

从模板中传递结果

在某些情况下，如果子组件可以将其结果“传递回”创建它的组件，那将非常方便。

例如，以下主组件使用子组件 Square 来分配和约束 out 为 in 的平方。

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

  out <== in * in;
}

template Main() {
  signal input a;
  signal input b;
  signal input sumOfSquares;

  component a2 = Square();
  component b2 = Square();

  a2.in <== a;
  b2.in <== b;

  // 断言 a^2 + b^2 === sum of Squares
  a2.out + b2.out === sumOfSquares;
}

component main = Main();

在子组件的上下文中，输出信号是指期望通过 <== 运算符分配值的信号，并且可用于将值传递回创建它的组件。

在 main 组件的上下文中，输出信号的含义完全不同，我们将在后面的章节中对此进行解释。

示例：二进制转数字

circomlib 库 是一个用于各种常见操作的 Circom 模板库。其中一项操作是将二进制数组转换为信号。我们之前已经看到，这可以通过 $b_0+2b_1+4b2+…+2^{n-1}b{n-1}=v$ 来完成。以下是如何在单独的组件中执行此操作。以下模板可以在 Circom 库的 bitify.circom 文件中找到：

template Bits2Num(n) {
  signal input in[n];
  signal output out;

  // lc 是 "linear combination"（线性组合）的缩写
  // 它用作累加器变量
  var lc1=0;

  var e2 = 1;
  for (var i = 0; i<n; i++) {
    lc1 += in[i] * e2;
    e2 += e2 + e2; // 也可以是 e2 *= 2;
  }

  lc1 ==> out;
}

我们不需要从库中复制和粘贴代码，可以像其他语言导入其他文件一样“包含”它：

include "circomlib/bitify.circom";

template Main(n) {
  signal input in[n];
  signal input v;

  // 实例化 Bits2Num 组件
  component b2n = Bits2Num(n);

  // 循环遍历每个二进制值
  // 并将其分配并约束到
  // b2n 输入数组
  for (var i = 0; i < n; i++) {
    b2n.in[i] <== in[i];
  }

  b2n.out === v;
}

component main = Main(4);

/* INPUT = {"in": [1, 0, 0, 1], "v": 9} */

上面的组件可以在 zkrepl 中进行测试，但如果在本地运行，则需要根据目录的配置设置导入路径。通常，Circomlib 是使用 yarn 或 npm 安装的。

单行组件示例

无需单独将输入信号分配给组件，也可以将它们作为参数提供。这被称为“匿名组件”。 考虑以下示例：

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

  out <== in[0] * in[1];
}

template Example() {

  signal input a;
  signal input b;

  signal output out;

  // 单行实例化
  out <== Mul()([a, b]);
}

component main = Example();

不应忽略输出信号

输出信号必须是实例化它的组件中的约束的一部分。如果输出信号保持“浮动”，那么在某些情况下，恶意的证明者可以为其分配任何值。有关此的更多信息将在破解约束不足的电路中介绍。

总结

• <== 和 ==> 节省了我们在 input.json 中显式提供信号值的麻烦。
• 每当一个信号的值直接由另一个信号的值确定时，我们就可以使用 <== 或 ==>。
• <== 等效于 ==>。参数只是简单地颠倒了，但效果是相同的。
• 组件可以实例化其他子组件，并使用 <== 或 ==> 将值发送到它们的输入信号。
• 子组件的 output 信号应约束为等于实例化它的组件中的其他信号。

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