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 (var i = 0; i < n; i++) {
        in[i] * (in[i] - 1) === 0;
    }

    // in 是 k 的二进制表示
    var acc; // 符号变量
    var powersOf2 = 1; // 常规变量
    for (var i = 0; i < n; i++) {
        acc += powersOf2 * in[i];
        powersOf2 *= 2;
    }

    acc === k;
}

为什么符号变量有帮助

考虑之前证明 $\sum\texttt{in}[i]=\texttt{sum}$ 的例子。如果没有符号变量，表达

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

会非常笨拙，如果我们不知道 n 提前是多少的话。即使 n 是固定的，比如 32，手动输入 32 个变量也会很烦人。因此，符号变量使我们能够逐步构建 in[0] + in[1] + in[2] + ...，而无需显式写出信号。

带有符号变量的非二次约束

因为符号变量可以“包含”两个信号之间的乘法，如果我们不小心，它们会导致在一个约束中嵌入两个乘法。考虑以下示例，该示例将不会编译：

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

    // v “包含” a * b
    var v = a * b;

    // 错误：有两个
    // 乘法
    // 在这个约束中
    v === c * d;
}

在上面的代码中，符号变量 v 中有一个乘法，我们声明了 v == a*b。因此，约束 v === c * d; 等效于 a * b = c * d;。因此，上面的代码将无法编译。

任意运算符允许用于非符号变量

使用（非符号）变量进行诸如计算模数或位移之类的操作是被允许的。但是，这意味着该变量不能再用作约束的一部分：

// 这没有约束
// 但它会编译
template Ok() {
    signal input a;
    signal input b;

    var v = a % b;
}

上面的例子将编译，因为 v 没有在约束中使用。但是，如果我们在约束中使用 v，代码将不会编译。下面显示了一个示例：

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

    var v = a % b;

    // 非二次约束
    c === v;
}

符号变量不能用于确定循环的边界或条件

类似地，只有常规变量可以用于确定循环的边界或 if 语句的条件。如果使用了符号变量，则代码将不会编译：

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

    var v = a * b;

    // v 是一个符号变量
    // 在 if 语句中使用
    if (v == 0) {
        c === 0;
    } else {
        c === 1;
    }
}

总结

符号变量是从信号分配值的变量。它们最常用于将可参数化的信号数量加在一起，因为总和可以在 for 循环中累积。它们实际上是一个“容器”或“桶”，其中包含单个信号或添加或相乘在一起的信号集合。如果一个变量从未从信号分配值，那么它就不是一个符号变量。

由于符号变量包含信号，因此在使用它们时必须小心，以避免违反二次约束。

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