先计算，后约束 - 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 的 数独教程，所以我们在这里不提供示例。

示例 3：模逆元

假设我们要计算信号 in 的乘法逆元，即找到一个信号 out，使得 out * in === 1。

计算乘法逆元的一种方法是使用费马小定理：

$$ x^{-1}=x^{p-2}\pmod p $$

但是，使用如此大的指数（Circom 的默认值是 $p\approx2^{254}$）将导致大量的乘法和一个非常大的电路。 相反，最好在电路外部计算乘法逆元，然后证明我们有正确的乘法逆元。 例如：

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

  // 费马小定理
  // 计算：
  // 请注意 -2 = p - 2 mod p
  var inv = in ** (-2);
  out <-- inv;

  // 然后约束
  out * in === 1;
}

component main = MulInv();

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

Circom 中的模除法

Circom 将 / 运算符解释为模除法，因此值 n 的逆元可以计算为：

inv <-- 1 / n;

上面的模板可以更简洁地写成：

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

  // 计算
  out <-- 1 / in;

  // 然后约束
  out * in === 1;
}

component main = MulInv();

模除法是非二次运算，因此只能与变量或细箭头赋值一起使用——即，需要在电路外计算。

示例 4：IsZero

动机

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

以下约束集将不起作用：

// 等于 42
x === 42

// 小于 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。 我们可以约束它们中的至少一个为真，如下所示：

// 两个信号中至少有一个不为零
x_eq_42 * x_lt_16 === 1;

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

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

在这里，我们设计一个电路，如果输入为 0 则返回 1，否则返回 0（出于好奇，此函数的名称是 克罗内克 delta 函数）。

如果我们完全使用加法和乘法来编写这样的函数，我们的函数将是一个多项式，它在可以为 0 的位置数量上受到限制。换句话说，如果我们希望我们的函数在我们的有限域中的每个地方都为零，那么我们的多项式的次数将几乎与有限域的阶数一样大，这是不切实际的。

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

我们需要一组约束，如果 in 为 0，则要求 out 为 1，如果 in 非零，则要求 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 为零，因为零没有乘法逆元。 我们现在有以下约束：

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

请注意，inv 本身不受约束，但在此情况下这并不重要。

第一个约束 in * inv + out === 1; 仅用于禁止 in 和 out 都为零。 如果 in 和 out 都为零，则无论 inv 的值如何，约束都将被违反。

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

• in 是否为零。
• in 的乘法逆元。

Circomlib 中的 IsZero 组件完成了本节中概述的约束：

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

  signal inv;

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

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

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

非确定性输入

在电路外计算的值，使我们能够使用更简洁的约束，称为“建议输入”或“非确定性输入”。 上述电路中的 inv 信号是建议输入或非确定性输入的示例。

示例 5：IsEqual

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

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 模板将信号分解为 n 位，如模板参数所指定：

template Num2Bits(n) {
  signal input in; // 数字
  signal output out[n]; // 二进制输出
  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$ 大于有限域，我们可能会遇到 别名错误。 这在该章节中进一步解释。

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

用动画可以最好地显示它计算二进制数组的方式，我们在这里显示：

https://img.learnblockchain.cn/2025/04/16/Num2Bits.mp4

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

Num2Bits 模板是模板 LessThan 和用于比较信号相对值的其他模板中的核心组件。

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

要了解如何在电路中有效地比较二进制数的大小，请查看我们关于 算术电路 中的相关部分，然后将该处的讨论与 Circomlib 中的 LessThan 模板 进行比较。

示例 7：IsMax

要证明一个项目是列表中的最大值，我们必须证明它 1) 大于或等于每个元素，并且 2) 它也存在于列表中。 要理解第二个要求，请考虑 100 不是列表 [4,5,6] 的最大值，即使 100 大于或等于列表中的每个项目。

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

为了确保 out 等于列表中的至少一个项目，它将对每个其他信号进行 IsEqual 比较求和。 如果总和为零，那么我们知道 out 不在列表中。 因此，我们约束该总和不为零：

template IsMax() {
  signal input in[3];
  signal output out;

  // 像往常一样计算最大值
  var maxx = in[0];
  for (var i = 1; i < 3; i++) {
    if (in[i] > maxx) {
      maxx = in[i];
    }
  }

  // 提出最大值，但尚未约束它
  out <-- maxx;

  // 最大值必须 ≥ 每个其他元素
  signal gte0;
  signal gte1;
  signal gte2;

  // gte0 <== GreaterEqThan(252)([out, in[0]]);
  // 是以下简写
  // component gte0 = GreaterEqThan(252);
  // gte0[0] <== out;
  // gte0[1] <== in[0];
  // 252 是为了确保我们没有足够的
  // 位来编码大于什么
  // 适合默认有限域的数字，该数字
  // 会导致别名问题
  gte0 <== GreaterEqThan(252)([out, in[0]]);
  gte1 <== GreaterEqThan(252)([out, in[1]]);
  gte2 <== GreaterEqThan(252)([out, in[2]]);
  gte0 === 1;
  gte1 === 1;
  gte2 === 1;

  // 最大值必须等于至少一个元素
  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);
  // 如果 IsZero 是 1，我们有违规
  iz === 0;
}

以其当前形式，我们的电路被硬编码为仅支持长度为 3 的数组。 但是，如果能够拥有一个用于任意长度输入的模板，那就太好了。 这是即将到来的章节的主题。

练习题

编写一个 Circom 函数，使用二次公式找到 2 次多项式的根。 请记住，一切都是在有限域上完成的，因此你需要使用第一个示例中的模平方根。

然后，编写约束，使两个根（如果存在）满足多项式。 将多项式作为三个系数的数组传递给 Circom 模板。

• 原文链接： rareskills.io/post/compu...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～