Circom 约束
Rank 1 约束系统在每个约束中最多有一个信号之间的乘法。这被称为“二次”约束。任何包含加法或乘法之外运算的约束都将被 Circom 拒绝，并显示“不允许非二次约束”错误。
以下两个例子将无法编译，因为它们每个约束中信号的乘法多于一个。
非二次约束示例 1
编译以下代码将导致以下 error: [T3001]: Non quadratic constraints are not allowe
template QuadraticViolation1() {
signal input a;
signal input b;
signal input c;
signal input d;
// 每个约束两个乘法
// 是不允许的
a * b === c * d;
}
非二次约束示例 2
与前面的例子类似，下面的约束有两个信号之间的乘法。
template QuadraticViolation2() {
signal input a;
signal input b;
signal input c;
signal input d;
// 每个约束两个乘法
// 是不允许的
a * b * c === d;
}
常数乘法不算
因此，即使有不止一个乘法，以下示例也会编译。
a * b === c;
2*a * 3*b === 4*c; // 允许整数系数
a * b + c === d; // 允许加法和一个乘法
a + b + c === d; // 乘法是可选的
a * b + c === d + e + f; // 对加法数量没有限制
二次型和 R1CS
回想一下，在算术化中，我们将验证程序展平为一系列中间步骤，其中每个中间步骤仅包含未知变量之间的单个乘法。
考虑以下验证示例：
def someProblem(x, y, out):
res = y^2 + 4*(x^2)*y -2
assert out == res, "incorrect inputs";
转换为 R1CS 会产生：
v1 === y * y
v2 === x * x
out === v1 + (4v2 * y) - 2
- R1CS 格式要求我们将问题重组为只有 1 个信号之间乘法运算的中间步骤，以遵守二次约束限制。
- 这创建了我们的约束系统。
因此，R1CS 表示将是：
// Cw = Aw * Bw
v1 = y * y
v2 = x * x
out -v1 +2 = (4v2 * y)
由于我们之前确保每个约束只有 1 个乘法，因此我们可以用向量形式表示约束系统，这是一个 R1CS。
导致非二次约束的非乘法运算符示例
如果在约束中使用了非法操作（不是加法或乘法），Circom 编译器将报告“不允许非二次约束！”错误。
在这里，我们提供一些例子。
示例 1：信号不能用于索引信号数组
以下操作将导致二次约束冲突。数组索引与加法和乘法之间没有直接转换。以下代码会导致错误 Non-quadratic constraint was detected statically, using unknown index will cause the constraint to be non-quadratic:
template KMustEqual5(n) {
signal input in[n];
signal input k;
// 不允许
in[k] === 5;
}
从技术上讲，仍然可以完成数组索引，但这需要一个更复杂的解决方案，我们将在后面的章节中展示。
示例 2：信号不能使用诸如 % 和 << 之类的操作
以下约束将创建一个“不允许非二次约束！”冲突：
template Example() {
signal input a;
signal input b;
// 不允许
a === b % 5;
// 不允许
a === b << 2;
}
Circom 如何处理除法
有点巧妙的是，Circom 将允许除以常数，因为它可以用该数字的乘法逆元乘法来简单地替换。因此，以下代码是有效的：
template Example() {
signal input a;
signal input b;
a === b / 2;
}
component main = Example();
但是，不允许划分信号，因为这意味着我们计算了信号的乘法逆元，它不能直接转换为仅加法和乘法。计算乘法逆元通常使用扩展欧几里得算法完成，这需要循环和条件语句——这些操作不能用加法和乘法原生表达。
template Example() {
signal input a;
signal input b;
signal input c;
// 不允许
a === b / c;
}
component main = Example();
相反，允许信号的减法，因为它直接转换为与常数 -1 的乘法：
template Example() {
signal input a;
signal input b;
// 允许
a === b - a;
// 等价于
a === b + -1*a
}
component main = Example();
整数除法，与乘以模逆元不同，由 `` 表示，并且不允许应用于信号：
template Example() {
signal input a;
signal input b;
// 只能将 \ 与变量一起使用
// 而不是信号
a === b \ 2;
}
component main = Example();
对于变量，你既有整数除法，也有“正常”除法（即，与除数的乘法逆元相乘）。
另一方面，对于信号，只允许“正常”除法（在上述意义上）。
总结
一个约束只能有信号之间的一个乘法，但对加法数量没有限制。
这种限制似乎使得除了简单算术之外不可能表达任何有趣的计算，但我们将在本教程系列的后面看到，存在许多巧妙的设计模式来解决此限制。
一旦我们理解了设计模式，我们就可以组合它们来建模更复杂的算法。
