Circom 中间信号与子组件

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 分解为模板

现在我们了解了...