Circom 约束

Rank 1 Constraint System 在每个约束中最多包含一次信号间的乘法。这被称为“二次”（quadratic）约束。任何包含除加法或乘法之外操作的约束，都会被 Circom 拒绝，并抛出“Non quadratic constraints are not allowed”错误。

以下两个示例将无法编译，因为它们在每个约束中包含多个信号间的乘法。

非二次约束示例 1

编译以下代码将导致如下 error: [T3001]: Non quadratic constraints are not allowe

Copy
template QuadraticViolation1() {
  signal input a;
  signal input b;
  signal input c;
  signal input d;
  
  // two multiplications per constraint
  // is not allowed
  a * b === c * d;
}

非二次约束示例 2

与上一个示例类似，以下约束在信号之间包含两次乘法。

Copy
template QuadraticViolation2() {
  signal input a;
  signal input b;
  signal input c;
  signal input d;
  
  // two multiplications per constraint
  // is not allowed
  a * b * c === d;
}

常数乘法不计算在内

因此，以下示例即使包含多个乘法也能正常编译。

Copy
a * b === c;

2*a * 3*b === 4*c; // integer coefficients allowed

a * b + c === d; // addition and one multiplication allowed

a + b + c === d; // multiplication is optional

a * b + c === d + e + f; // no restrictions on number of additions

二次型与 R1CS

回想一下，在算术化（arithmetization）中，我们将验证程序展平为一系列中间步骤，其中每个中间步骤在未知变量之间仅包含一次乘法。

考虑以下验证示例：

Copy
def someProblem(x, y, out):
  res = y^2 + 4*(x^2)*y -2 
  assert out == res, "incorrect inputs";

转换为 R1CS 会得到：

Copy
v1  === y * y
v2  === x * x 
out === v1 + (4v2 * y) - 2

• R1CS 格式要求我们将问题重构为中间步骤，使信号之间只有 1 次乘法操作，以符合二次约束的限制。
• 这构成了我们的约束系统。

因此，R1CS 的表示将是：

Copy
//     Cw = Aw * Bw
       v1  = y * y
       v2  = x * x 
out -v1 +2 = (4v2 * y)

由于我们之前确保了每个约束只有一个乘法，因此我们能够以向量形式表达该约束系统，这就是 R1CS。

引起非二次约束的非乘法操作符示例

如果在约束中使用了非法操作（非加法或乘法），Circom 编译器将报错“Non quadratic constraints are not allowed!”。

在这里，我们提供一些示例。

示例 1：信号不能用于索引信号数组

以下操作将导致违反二次约束。从数组索引到加法和乘法没有直接的转换方式。以下代码会导致错误 Non-quadratic constraint was detected statically, using unknown index will cause the constraint to be non-quadratic：

Copy
template KMustEqual5(n) {

  signal input in[n];
  signal input k;
  
  // not allowed
  in[k] === 5;
}

从技术上讲，实现数组索引仍然是可能的，但这需要一个更复杂的解决方案，我们将在后面的章节中展示。

示例 2：信号不能使用诸如 % 和 << 的操作

以下约束将产生“Non quadratic constraints are not allowed!”违规错误：

Copy
template Example() {
  signal input a;
  signal input b;
  
  // not allowed
  a === b % 5;
  
  // not allowed
  a === b << 2;
}

Circom 如何处理除法

有些微妙的是，Circom 允许除以一个常数的“除法”，因为它可以简单地替换为乘以该数字的乘法逆元（multiplicative inverse）。因此，以下代码是有效的：

Copy
template Example() {
  signal input a;
  signal input b;
  
  a === b / 2;
}

component main = Example();

然而，不允许对信号进行除法运算，因为这意味着我们需要计算信号的乘法逆元，而这无法直接转换为仅包含加法和乘法的操作。计算乘法逆元通常使用扩展欧几里得算法（extended euclidean algorithm），这需要循环和条件语句——这些操作无法原生地用加法和乘法表达。

Copy
template Example() {
  signal input a;
  signal input b;
  signal input c;
  
  // not allowed
  a === b / c;
}

component main = Example();

相反，允许信号的减法，因为它直接转换为乘以常数 -1：

Copy
template Example() {
  signal input a;
  signal input b;
  
  // allowed
  a === b - a;
  
  // equivalent
  a === b + -1*a
}

component main = Example();

与乘以模逆元不同，整数除法由 \ 表示，并且不允许将其应用于信号：

Copy
template Example() {
  signal input a;
  signal input b;
  
  // can only use \ with variables
  // not signals
  a === b \ 2;
}

component main = Example();

对于变量（variables），既可以使用整数除法，也可以使用“普通”除法（即乘以除数的乘法逆元）。

另一方面，对于信号（signals），只允许（上述意义上的）“普通”除法。

总结

一个约束在信号之间只能包含一次乘法，但对加法的数量没有限制。

这看起来似乎使得这种限制无法表达除了简单算术之外的任何有趣计算，但在本系列教程的后面我们将看到，存在许多巧妙的设计模式来绕过这一限制。

一旦我们理解了这些设计模式，就可以将它们组合起来，以对复杂得多的算法进行建模。