先计算，后约束 - ZK 电路设计模式

“计算然后约束”是 ZK 电路中的一种设计模式，其中算法的正确输出首先在没有约束的情况下进行计算。 然后通过执行与算法相关的不变量来验证解决方案的正确性。

计算然后约束的动机

如果仅限于使用加法、乘法和赋值然后约束 (==>)，那么许多计算将极难建模，并且需要大量的加法和乘法。

例如，计算一个数的平方根需要几个迭代估计。 这将使电路尺寸大大增加。

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

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

Circom 中的“细箭头” <-- 运算符及其与 <== 的不同之处

<== 运算符将一个值分配给一个信号并创建一个约束。 由于约束必须是二次的，因此我们无法执行以下操作：

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

  // 如果 in == 0，则 out = 1
  out <== in == 0 ? 1 : 0;
}

component main = InputEqualsZero();

编译上面的电路会导致非二次约束错误，因为三元运算符不能直接表示为信号之间的单个乘法。 事实上，Circom 直接拒绝任何非乘法或加法的信号操作。

起初，可能看起来 Circom 无法为我们计算 out，而是需要将其作为公共输入提供。 但是，如果涉及很多信号，这将非常不方便。

我们需要一种机制来告诉 Circom “计算并将此信号的值分配为其他信号的函数，但不创建约束。” 该操作的语法是 <-- 运算符：

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

  // 如果 in == 0，则 out = 1
  out <-- in == 0 ? 1 : 0;
}

component main = InputEqualsZero();

in == 0 ? 1 : 0; 操作有时被称为“电路外计算”或“提示”。

上面的代码可以编译，但是 out 和 in 没有应用任何约束。

<-- 运算符非常方便，因为它允许我们计算值而不生成约束，从而消除了手动提供某些信号值的需要。 然而，它也是安全漏洞的来源。

Circom 不强制开发者在使用 <-- 后创建适当的约束，这已成为 Circom 中关键和高危漏洞的常见来源。 即使开发者没有添加任何约束，从而创建了非常危险的代码，编译器甚至不会给出警告或提示。 未约束的信号可以取任何值，从而允许电路为无意义的语句生成 ZK 证明。

我们将在后面的教程 利用约束不足的电路 中，教你如何利用滥用 <-- 运算符的 Circom 代码。 现在，可以将其视为一种操作，它可以避免我们自己提供某些信号值的麻烦，同时仍然要求我们稍后约束该信号。

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

示例 1：模平方根

数字 $q$ 的模平方根是数字 $r$，使得 $r^2=q\pmod p$。 但是，并非所有字段元素都有模平方根。 对平方根的正确计算进行建模的约束很简单（尽管计算平方根并非如此）。

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

function sqrt(n) {
  // 做一些魔法（参见下一个代码块）
  return r;
}

template ValidSqrt() {
  signal input in;
  signal output out; // sqrt(in)

  out <-- sqrt(in);
  out * out === in; // 确保 sqrt 是正确的
  // `*` 隐式地以 p 为模完成
}

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

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

function sqrt(n) {

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

    // 测试是否具有解决方案
    var res = n ** ((-1) >> 1);
//        if (res!=1) assert(false, "SQRT 不存在");
    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;
}

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

template ValidSqrt() {
  signal input in;
  signal output out1; // sqrt(in)
  signal output out2; // -sqrt(in)

  out1 <-- sqrt(in);
  out2 <-- out1 * -1; // 计算步骤（无约束）
  out1 * out1 === in; // 验证步骤（基于约束）：
  out2 * out2 === in; // 验证步骤
}

警告： 此处提供的代码已硬编码为 Circom 的默认字段大小。 如果你将 Circom 配置为使用其他字段，它可能会产生错误的答案！

上面的示例演示了当约束不是问题时，计算平方根要简单得多——如果我们尝试仅使用乘法和加法来计算平方根，则电路将非常大。 然后可以通过约束来强制执行结果的正确性。

这说明了 Circom 如何既可以用作传统的编程语言，也可以用作约束生成 DSL。 代码的 sqrt(n) 函数部分是传统的编程，但是约束 in === out * out 会生成约束。

示例 2：数独

如果一个计算太困难或计算成本太高而无法通过约束建模——也就是说，如果它需要许多门和中间信号——你可以简单地将其作为输入提供，并假设证明者通过其他方式获得了答案。

要实际解决数独难题，必须运行搜索算法以寻找可能的解决方案，可能使用深度优先搜索。 但是，我们不需要证明我们直接运行了搜索算法——生成有效的解决方案足以证明我们运行了搜索算法。 因为互联网上已经有许多 Circom 的 [数独教程](https://github.com/nalinbhardwaj/snarky-sudoku/blob/main/circuit...