Circom

算数电路与布尔电路

只使用加法和乘法的电路称为算数电路（Arithmetic Circuit），对于算数电路中的变量称为信号（Signal），例如：

$0 === (a-1)(b-2)$

这里的 === 表示约束，例如这里就要求 $a=1$ 或 $b=2$。

而对于 >= ，假设 $a,b \in \{0,1\}^{n-1}$，可以表示为 $2^{n-1} + (a-b) = c$，然后看 $c$ 的最高位，1则 $a \ge b$，0则 $a < b$。

Circom

template GreaterEq(n) {
    signal input a;
    signal input b;
    signal output out;

    signal c;
    signal bits[n];

    c <== (1 << (n-1)) + a - b;

    component n2b = Num2Bits(n);
    c ==> n2b.in;

    for (var i = 0; i < n; i++) {
        bits[i] <== n2b.out[i];
    }

    out <== bits[n-1];
}

布尔电路转算数电路：

这里电路的输出值是整个等式的真值

• 0或1：$x(x-1)===0$
• 与：$xy===1$
• 非：$(1-x)===1$
• 或：$x+y-xy===1$
• 异或：$x+y-2xy===1$

符号

1. <== (约束赋值)

   • 同时进行赋值和添加约束
   • 将右侧的值赋给左侧的信号，并创建约束确保等式成立
   • 示例：out <== in1 * in2;

2. === (纯约束)

   • 仅添加约束，不进行赋值
   • 用于验证两个表达式相等，但不改变任何信号的值
   • 示例：out === in1 * in2;

3. <-- (纯赋值)

   • 仅进行赋值，不添加约束
   • 将右侧的值赋给左侧的信号，但不创建任何约束验证
   • 示例：out <-- in1 * in2;

实用电路

判零

判零

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

    signal inv;

    inv <-- in!=0 ? 1/in : 0;

    out <== -in*inv +1;
    in*out === 0;
}

相等

相等

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

    component isz = IsZero();

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

    isz.out ==> out;
}