“计算后约束”（Compute then constrain）是 ZK 电路中的一种设计模式，即首先在不施加约束的情况下计算出算法的正确输出。然后通过强制执行与算法相关的不变量来验证该解的正确性。

计算后约束的动机

如果仅仅局限于使用加法、乘法以及赋值并约束（==>），那么许多计算在建模时将极具挑战性，并且需要极大数量的加法和乘法。

例如，计算一个数的平方根需要多次迭代估算。这将使电路规模变得相当庞大。

因此，更实用的做法通常是在电路外部运行计算——即在计算答案时不生成任何约束——然后配置当且仅当计算出的答案正确时才会满足的约束。

我们将展示 Circomlib 中 Bitify 和 Comparator 库的大量示例，这些库大量使用了这种模式。

Circom 中的“细箭头” <-- 操作符及其与 <== 的区别

<== 操作符在为一个 signal 赋值的同时创建一个约束。由于约束必须是二次的（quadratic），我们无法执行如下操作：

Copy
template InputEqualsZero() {
  signal input in;
  signal output out;
  
  // out = 1 if in == 0
  out <== in == 0 ? 1 : 0;
}

component main = InputEqualsZero();

编译上述电路将导致非二次约束（non-quadratic constraints）错误，因为三元运算符不能直接表示为 signals 之间的单一乘法。事实上，Circom 直接拒绝任何非乘法或加法的 signals 操作。

乍一看，似乎 Circom 无法为我们计算 out，而是要求将其作为 public input 提供。然而，如果涉及大量 signals，这将非常不便。

我们需要一种机制来告诉 Circom：“将此 signal 作为一个关于其他 signals 的函数进行计算和赋值，但不要创建约束。”该操作的语法是 <-- 操作符：

Copy
template InputEqualsZero() {
  signal input in;
  signal output out;
  
  // out = 1 if in == 0
  out <-- in == 0 ? 1 : 0;
}

component main = InputEqualsZero();

操作 in == 0 ? 1 : 0; 有时被称为“电路外计算（out-of-circuit computations）”或“提示（hint）”。

上述代码可以通过编译，但 out 和 in 并没有被施加任何约束。

<-- 操作符非常方便，因为它允许我们在不生成约束的情况下计算值，从而消除了手动提供某些 signal 值的需要。然而，它也是安全漏洞的来源之一。

Circom 并不强制要求开发者在使用 <-- 后创建相应的约束，这已成为 Circom 中严重和高危漏洞的常见来源。即使开发者没有添加任何约束，从而编写出非常危险的代码，编译器甚至不会给出警告或提示。未约束的 signals 可以取任何值，从而允许电路为荒谬的陈述生成 ZK 证明。

我们将在以后的教程 exploiting underconstrained circuits 中教授如何利用误用 <-- 操作符的 Circom 代码。现在，只需将其视为一种操作，它省去了我们亲自提供特定 signal 值的麻烦，但仍然要求我们稍后对该 signal 施加约束。

通过示例可以最好地理解计算和约束，本章的其余部分将提供这些示例。

示例 1：模平方根

一个数 $q$ 的模平方根（modular square root）是一个数 $r$，使得 $r^2=q\pmod p$。然而，并非所有 field 元素都有模平方根。模拟平方根正确计算的约束非常直观（尽管计算平方根本身并非如此）。

考虑以下代码，它证明了 out 是 in 的模平方根：

Copy
function sqrt(n) {
  // do some magic (see the next code block)
  return r;
}

template ValidSqrt() {
  signal input in;
  signal output out; // sqrt(in)
  
  out <-- sqrt(in);
  out * out === in; // ensure sqrt was correct
  // the `*` is implicity done modulo p
}

在这里，out <-- sqrt(in) 将平方根赋值给 out，而不添加约束。

Circomlib 中的 pointbits 文件提供了计算模平方根的函数。请注意，函数必须声明在 Circom template 之外。在 Circom 中，“函数（function）”仅仅是为了方便将相关的代码放入一个包含的块中。

Copy
function sqrt(n) {

    if (n == 0) {
        return 0;
    }

    // Test that have solution
    var res = n ** ((-1) >> 1);
//        if (res!=1) assert(false, "SQRT does not exists");
    if (res!=1) return 0;

    var m = 28;
    var c = 19103219067921713944291392827692070036145651957329286315305642004821462161904;
    var t = n ** 81540058820840996586704275553141814055101440848469862132140264610111;
    var r = n ** ((81540058820840996586704275553141814055101440848469862132140264610111+1)>>1);
    var sq;
    var i;
    var b;
    var j;

    while ((r != 0)&&(t != 1)) {
        sq = t*t;
        i = 1;
        while (sq!=1) {
            i++;
            sq = sq*sq;
        }

        // b = c ^ m-i-1
        b = c;
        for (j=0; j< m-i-1; j ++) b = b*b;

        m = i;
        c = b*b;
        t = t*c;
        r = r*b;
    }

    if (r < 0 ) {
        r = -r;
    }

    return r;
}

模平方根有两个解：平方根本身及其加法逆元（additive inverse）。因此，我们可以如下生成这两个解：

Copy
template ValidSqrt() {
  signal input in;
  signal output out1; // sqrt(in)
  signal output out2; // -sqrt(in)
  
  out1 <-- sqrt(in);
  out2 <-- out1 * -1; // Computation Step (Unconstrained)
  out1 * out1 === in; // Verification Step (Constraint-Based):
  out2 * out2 === in; // Verification Step
}

警告： 此处展示的代码是针对 Circom 的默认 field size 硬编码的。如果您将 Circom 配置为使用其他 field，它可能会产生错误的答案！

上述示例表明，如果不考虑约束，计算平方根要简单得多——如果我们试图仅使用乘法和加法来计算平方根，电路规模将变得不合理地庞大。随后可以通过约束来强制保证结果的正确性。

这说明了 Circom 是如何兼具传统编程语言和约束生成 DSL 的特性的。代码中 function sqrt(n) 部分是传统编程，而约束 in === out * out 则生成了约束。

示例 2：数独

如果某种计算在通过约束建模时过于困难或计算成本过高——也就是说，如果它需要许多门（gates）和中间 signals——那么可以简单地将其作为输入提供，并假设 prover 通过其他方式获得了答案。

要真正解开一个数独谜题，必须运行一种搜索算法来寻找可能的解，通常是使用深度优先搜索。然而，我们不需要直接证明我们运行了搜索算法——生成一个有效的解足以证明我们运行了搜索算法。因为互联网上已经有大量针对 Circom 的 Sudoku tutorials，我们在此不再赘述示例。

示例 3：模逆

假设我们要计算 signal in 的乘法逆元（multiplicative inverse），即找到一个 signal out，使得 out * in === 1。

计算乘法逆元的一种方法是使用费马小定理（Fermat’s Little Theorem）：

然而，使用如此大的指数（Circom 的默认值为 $p\approx2^{254}$）会导致大量乘法和极其庞大的电路。相反，更好的做法是在电路外部计算乘法逆元，然后证明我们拥有正确的乘法逆元。例如：

Copy
template MulInv() {
  signal input in;
  signal output out;
  
  // Fermat's little theorem
  // compute:
  // note that -2 = p - 2 mod p
  var inv = in ** (-2);
  out <-- inv;
  
  // then constrain
  out * in === 1;
}

component main = MulInv();

这里，我们只有一个约束：out * in === 1，因此这非常高效。

Circom 中的模除

Circom 将 / 操作符解释为模除（modular division），因此一个值 n 的逆元可以如下计算：

Copy
inv <-- 1 / n;

上面的 template 可以写得更简洁一些：

Copy
template MulInv() {
  signal input in;
  signal output out;
  
  // compute
  out <-- 1 / in;
  
  // then constrain
  out * in === 1;
}

component main = MulInv();

模除是一种非二次运算，因此它只能用于 variables 或带有细箭头的赋值中——即它需要在电路外部计算。

示例 4：IsZero

动机

IsZero 电路在组合成更大的计算时非常方便。假设我们想要证明 x 小于 16 或 x 等于 42。

下面这组约束是行不通的：

Copy
// equal 42
x === 42

// less than 16
x === b_0 + 2*b_1 + 4*b_2 + 8*b_3
0 === b_0 * (b_0 - 1)
0 === b_1 * (b_1 - 1)
0 === b_2 * (b_2 - 1)
0 === b_3 * (b_3 - 1)

如果 x 是 42，它将违反底部的约束；如果它小于 16，它将违反 x === 42。

因此，我们真正需要的是子电路能够指示某个条件是否成立（即 x 等于 42 或小于 16），而不是强制某个条件成立。然后我们可以对这些指示器施加约束。例如，假设我们有指示器 x_eq_42 和 x_lt_16。我们可以用以下方式约束它们中至少有一个为真：

Copy
// at least one of the two signals is not zero
x_eq_42 * x_lt_16 === 1;

为了创建一个 x 等于 42 的指示器，我们想知道 x - 42 的值是否恰好为零。

设计一个电路来指示值为零

在这里，我们设计一个电路，如果输入为 0 则返回 1，否则返回 0（对于好奇的读者，这个函数的名称是 Kronecker Delta function）。

如果我们纯粹使用加法和乘法来编写这样一个函数，那么我们的函数将是一个多项式，其能够为 0 的位置数量是有限的。换句话说，如果我们希望我们的函数在有限域（finite field）中的任何地方都为零，那么我们的多项式的度（degree）将几乎与有限域的阶（order）一样大，这是不切实际的。

相反，我们设计一组约束，使 in 和 out 具有以下属性：

我们需要一组约束，要求如果 in 为 0，则 out 必须为 1；如果 in 为非 0，则 out 必须为 0。思考这种关系的另一种方式是：“in 或 out 中至少有一个必须为非零，但它们不能同时为零，也不能同时为非零。”

“in 和 out 中至少有一个必须为零”可以被建模为约束 in * out === 0。

在下表中，我们可以看到 in * out === 0 接受了“in 和 out 恰好有一个为零”的情况，并正确拒绝了 in 和 out 都为非零的情况：

约束 in * out === 0 的问题在于它并不能防止 in 和 out 都为 0 的情况（如上表标红部分所示）。

我们试图捕捉的缺失属性是 in 和 out 不能同时为零。

天真地想，我们可以用 in + out === 1 来实现。这意味着如果 in 为 1，则 out 必须为 0，反之亦然。然而，规范指出 in 可以是任何非零值，例如 100，而 100 + out 不可能是 1。

但是，如果我们能“把 100 变成 1”，就可以使约束生效。这可以通过在电路外部计算 in 的乘法逆元，然后应用约束 in * inv + out === 1 来实现。如果 in 为零，我们就使 inv 为零，因为零没有乘法逆元。现在我们有了如下约束：

Copy
in * inv + out === 1;
in * out === 0;

请注意，inv 本身并未受约束，但在这种情况下，这并不影响大局。

第一个约束 in * inv + out === 1; 仅仅是为了不允许 in 和 out 同时为零。如果 in 和 out 同时为零，则无论 inv 的值是多少，该约束都会被违反。

总结在电路外部完成的计算：

• 判断 in 是否为零。
• 计算 in 的乘法逆元。

Circomlib 中的 IsZero 组件实现了本节概述的约束：

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

  signal inv;

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

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

它首先在电路外计算 inv，然后约束：如果 in 为零，则 out 为 1；否则 out 为 0。

非确定性输入

那些在电路外计算并使我们能够使用更简洁约束的值被称为“建议输入（advice inputs）”或“非确定性输入（non-deterministic inputs）”。上述电路中的 inv signal 就是建议输入或非确定性输入的一个例子。

示例 5：IsEqual

Circomlib 中的 IsEqual 组件与 IsZero 密切相关——它检查输入之间的差值是否为零（如果是，那么它们一定彼此相等）：

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

  component isz = IsZero();

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

  isz.out ==> out;
}

示例 6：Num2Bits

Circomlib 中的 Num2Bits template 会按照 template 参数的指定，将一个 signal 分解为 n 个比特（bits）：

Copy
template Num2Bits(n) {
  signal input in; // number
  signal output out[n]; // binary output
  var lc1=0;

  var e2=1;
  for (var i = 0; i<n; i++) {
    out[i] <-- (in >> i) & 1;
    out[i] * (out[i] -1 ) === 0;
    lc1 += out[i] * e2;
    e2 = e2+e2;
  }

  lc1 === in;
}

请注意，对于上述代码中的 n，如果 $2^n$ 大于有限域，我们可能会遇到 alias bug。这将在那一章中作进一步解释。

从本质上讲，这段代码从最低有效位开始，循环遍历二进制表示中的每一位。在循环的每次迭代中，我们将值 [1,2,4,8,…,2^i] 存储在一个 variable e2 中，这是该位所代表的权重值。如果该位为 1（out[i] <-- (in >> i) & 1;），我们将该值累加到累加器 lc1 中。在循环的每次迭代中，我们约束读出的位实际上是 0 或 1（使用 out[i] * (out[i] -1 ) === 0;）。最后，我们约束计算得到的二进制值与原始值匹配（lc1 === in;）。

它计算二进制数组的过程最好用动画展示，我们在此演示：

与之前的示例类似，计算二进制值是在电路外部完成的，但随后我们会施加约束以确保该二进制数组是正确的。

Num2Bits template 是 LessThan template 以及其他用于比较 signals 相对大小的 template 的核心组件。

Field 元素（有限域中的数字）不能直接相互比较——它们需要首先转换为二进制数字。

要了解如何高效地在电路中比较二进制数字的大小，请复习我们在 Arithmetic Circuits 章节中的相关部分，然后将那里的讨论与 LessThan template in Circomlib 进行比较。

示例 7：IsMax

要证明某个项是列表中的最大值，我们必须证明 1）它大于或等于每个元素，以及 2）它也存在于该列表中。要理解第二个要求，想想看 100 并不是列表 [4,5,6] 的最大值，尽管 100 大于或等于列表中的每一项。

下面的电路使用传统的 for 循环在电路外部计算最大值，然后使用 GreaterEqThan 组件确保 out 大于或等于列表中的任何其他项。

为了确保 out 至少等于列表中的某一项，它对与其他每个 signal 的 IsEqual 比较结果进行了求和。如果总和为零，我们就知道 out 不在列表中。因此，我们约束该总和不能为零：

Copy

template IsMax() {
  signal input in[3];
  signal output out;
  
  // compute the max as usual
  var maxx = in[0];
  for (var i = 1; i < 3; i++) {
    if (in[i] > maxx) {
      maxx = in[i];
    }
  }
  
  // propose the max, but do not constrained it yet
  out <-- maxx;
  
  // max must be ≥ every other element
  signal gte0;
  signal gte1;
  signal gte2;
  
  // gte0 <== GreaterEqThan(252)([out, in[0]]);
  // is shorthand for
  // component gte0 = GreaterEqThan(252);
  // gte0[0] <== out;
  // gte0[1] <== in[0];
  // 252 is to ensure we don't have enough
  // bits to encode numbers larger than what
  // fits in the default finite field, which
  // would lead to aliasing issues
  gte0 <== GreaterEqThan(252)([out, in[0]]);
  gte1 <== GreaterEqThan(252)([out, in[1]]);
  gte2 <== GreaterEqThan(252)([out, in[2]]);
  gte0 === 1;
  gte1 === 1;
  gte2 === 1;
  
  // max must be equal to at least one element
  signal eq0;
  signal eq1;
  signal eq2;
  eq0 <== IsEqual()([out, in[0]]);
  eq1 <== IsEqual()([out, in[1]]);
  eq2 <== IsEqual()([out, in[2]]);
  
  signal iz;
  iz <== IsZero()(eq0 + eq1 + eq2);
  // if IsZero is 1, we have a violation
  iz === 0;
}

在当前形式下，我们的电路被硬编码为只支持长度为 3 的数组。然而，如果能有一个支持任意长度输入的 template 会更好。这将是我们后续章节的主题。

练习题

编写一个使用求根公式查找二次多项式（degree 2 polynomial）根的 Circom function。请记住，一切都是在有限域（finite field）上进行的，因此您需要使用第一个示例中的模平方根。

然后，编写约束条件，使这两个根（如果存在）满足该多项式。将该多项式作为包含三个系数的数组传递给 Circom template。