Circom中的符号变量

Circom 中的符号变量是指已从信号分配值的变量。

当一个信号被分配给一个变量时（从而将其转换为符号变量），该变量就变成了该信号以及应用于它的任何算术运算的容器。符号变量使用 var 关键字声明，就像其他变量一样。

例如，以下两个电路是等效的，即它们产生相同的底层 R1CS：

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

    a * b === c;
}

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

    // 符号变量 v “包含” a * b
    var v = a * b;

    // 底层逻辑是 a * b === c
    v === c;
}

在 ExampleB 中，符号变量 v 只是表达式 a * b 的占位符。ExampleA 和 ExampleB 都使用完全相同的 R1CS 编译，它们之间没有功能上的差异。

符号变量的使用场景

检查 $\sum\texttt{in}[i]=\texttt{sum}$

如果我们想在一个循环中对一个信号数组求和，符号变量非常方便。实际上，在循环中对信号求和是它们最常见的用例：

// 断言 in 的总和 === sum
template Sum(n) {
    signal input in[n];
    signal input sum;

    var accumulator;
    for (var i = 0; i < n; i++) {
        accumulator += in[i];
    }

    // in[0] + in[1] + in[2] + ... + in[n - 1] === sum
    accumulator === sum;
}

检查 in 是否为 k 的有效二进制表示

一个更有趣的例子是证明 in[n] 是 k 的二进制表示，k 是 n 的模板化值。在下面的电路中，我们检查：

$$ \texttt{in[0]}+2\cdot\texttt{in[1]}+4\cdot\texttt{in[2]} +\dots2^{n-1}\cdot\texttt{in[n-1]} == k $$

如果 in 中的所有信号都被约束为 $\set{0,1}$，那么这意味着 in[] 是 k 的二进制表示：

template IsBinaryRepresentation(n) {

    signal input in[n];
    signal input k;

    // in 仅为二进制
    for (v...