约束生成

为了理解 Circom 的构建部分，我们需要考虑以下类型的表达式：

• 常量值：仅允许常量值。
• 线性表达式：仅使用加法的表达式。也可以使用变量乘以常数来表示。例如，表达式 2*x + 3*y + 2 是允许的，因为它等效于 x + x + y + y + y + 2。
• 二次表达式：通过允许两个线性表达式相乘和线性表达式相加得到的表达式：A*B - C，其中 A、B 和 C 是线性表达式。例如，(2*x + 3*y + 2) * (x+y) + 6*x + y – 2。
• 非二次表达式：任何不属于上述类型的算术表达式。

Circom 允许程序员定义约束来定义算术电路。所有约束必须是 A*B + C = 0 形式的二次约束，其中 A、B 和 C 是信号的线性组合。Circom 会对定义的约束进行一些小的变换以符合 A*B + C = 0 的格式：

• 将等式的一侧移到另一侧。
• 应用加法的交换律。
• 乘（或除）常数。

使用运算符 === 来施加约束，它会创建给定等式约束的简化形式。

a*(a-1) === 0;
​

添加这样的约束还意味着在见证代码生成中添加一个 assert 语句。

约束生成可以与信号赋值结合使用，运算符 <== 的左侧是要赋值的信号。

out <== 1 - a*b;
​

等价于：

out <-- 1 - a*b;
out === 1 - a*b;
​

如前所述，使用 <-- 和 --> 运算符为信号赋值被认为是危险的，通常应该与 === 运算符结合使用，以通过约束描述所赋值的含义。例如：

a <-- b/c;
a*c === b;
​

在构建阶段，变量可以包含使用乘法、加法和其他变量或信号以及字段值构建的算术表达式。只有二次表达式允许包含在约束中。超过二次的其他算术表达式或使用其他算术运算符（如除法或幂运算）不允许作为约束。

template multi3() {
	 signal input in;
	 signal input in2;
	 signal input in3;
	 signal output out;
	 out <== in*in2*in3;
}
​

此模板会产生错误 "Non quadratic constraints are not allowed!"，因为它引入了约束 out === in*in2*in3，这不是二次约束。

以下示例展示了表达式的生成：

 signal input a;
 signal output b;
 var x = a*a;
 x += 3;
 b <== x;
​

最后一条指令产生约束 b === a * a + 3。

最后，程序员有时在开始使用 Circom 时会误用运算符 <--。他们通常会使用该运算符赋值一个二次表达式，结果没有添加约束。在这种情况下，需要同时执行赋值和添加约束的运算符是 <==。自 2.0.8 版本以来，如果出现这种情况，我们会发出警告。