先指示再约束 - 在 Circom 中复杂约束条件的方法

如果我们想表达 “x 可以等于 5 或 6”，我们可以简单地使用以下约束：

(x - 6) * (x - 5) === 0

然而，假设我们想表达 “x 小于 5 或者 x 大于 17”。在这种情况下，我们不能直接组合这两个条件，因为如果 x 小于 5，它会违反 x 大于 17 的约束，反之亦然。

解决方案是创建不同条件的 指示器 信号（例如，x 小于 5，或者大于 17），然后对指示器施加约束。

Circomlib 比较器库

Circomlib 比较器库 包含一个 LessThan 组件，它返回 0 或 1 来指示 in[0] 是否小于 in[1]。这个组件的工作原理在 算术电路 章节中有所描述。但作为总结，假设 x 和 y 最大为 3 位。如果我们计算 z = 2^3 + (x - y)，那么如果 x 小于 y，z 将小于 2^3，反之亦然 (2^3 = 8)。由于 z 是一个 4 位数字，我们可以通过仅查看最高有效位来有效地检查 z 是否小于 2^3。2^3 在二进制中是 1000₂。每个大于或等于 2^3 的 4 位数字的最高有效位等于 1，而每个小于 2^3 的 4 位数字的最高有效位等于 0。

对于一般的 n 位数字，我们可以通过检查最高有效位是否设置来检查 x 是否大于或等于 2^n。因此，我们可以推广，如果 x 和 y 是 n-1 位数字，那么我们可以通过检查 2^(n-1) + (x - y) 的最高有效位是否被设置来检测 x < y。

这是一个使用 LessThan 模板的最小示例：

include "circomlib/comparators.circom";

template Example () {
  signal input a;
  signal input b;
  signal output out;

  // 252 将在下一节中解释
  out <== LessThan(252)([a, b]);
}

component main = Example();

/* INPUT = {
  "a": "9",
  "b": "10"
} */

252 的来源

有限域（Circom 使用的）中的数字不能相互比较为“小于”或“大于”，因为不等式的典型代数定律不成立。

例如，如果 $x > y$，那么如果 $c$ 为正数，则 $x+c>y+c$ 应该始终成立。然而，这在有限域中是不成立的。我们可以选择 $c$，使其为 $x$ 的加法逆元，即 $x + c=0\mod p$。然后我们最终会得到一个无意义的陈述，即 0 大于一个非零数。例如，如果 $p = 7$ 且 $x=2$ 且 $y=1$，我们有 $x>y$。但是，如果我们给 $x$ 和 $y$ 都加上 $6$，那么我们就有了 \$0>1$。

252 指定了 LessThan 组件中的位数，以限制 x 和 y 的大小，以便可以进行有意义的比较（上面的部分使用了 4 位作为示例）。

Circom 可以在有限域中保存最大 253 位的数字。出于 别名检查 章节中讨论的安全原因，我们不应该将域元素转换为可以编码大于该域的数字的二进制表示。因此，Circom 不允许使用超过 252 位的比较模板 (源代码)。

然而，回想一下，对于 LessThan(n)，我们需要计算 z = 2^n + (x - y)，并且 2^n 需要比 x 或 y 大一位。因此，x 和 y 最大需要 $2^{n-1}$ 位。由于 Circom 支持最大 253 位的数字，因此 x 和 y 必须最大为 252 位。

x 小于 5 或 x 大于 17

值得庆幸的是，Circomlib 库将为我们完成大部分工作。我们将使用 LessThan 和 GreaterThan 组件的输出信号来 指示 x 是否小于 5 或大于 17。

然后，我们通过使用 OR 组件（在底层只是 out <== a + b - a * b）来 约束 它们中的至少一个为 1。

pragma circom 2.1.6;

include "circomlib/comparators.circom";
include "circomlib/gates.circom";

template DisjointExample1() {
  signal input x;

  signal indicator1;
  signal indicator2;

  indicator1 <== LessThan(252)([x, 5]);
  indicator2 <== GreaterThan(252)([x, 17]);

  component or = OR();
  or.a <== indicator1;
  or.b <== indicator2;

  or.out === 1;
}

component main = DisjointExample1();

/* INPUT = {
  "x": "18"
} */

包含约束 or.out === 1; 非常重要，否则电路会接受 indicator1 和 indicator2 都为零的信号。我们将在本章的结尾处更详细地回到这一点。

简化代码

通过隐式地使用指示器信号，可以简化上面的代码，如下所示：

pragma circom 2.1.6;

include "circomlib/comparators.circom";
include "circomlib/gates.circom";

template DisjointExample1() {
  signal input x;

  component or = OR();
  or.a <== LessThan(252)([x, 5]);
  or.b <== GreaterThan(252)([x, 17]);
  or.out === 1;   
}

component main = DisjointExample1();

/* INPUT = {
  "x": "18"
} */

不同时满足 x < 100 且 y < 100

为了表达上面的情况，即 “x < 100 且 y < 100”，我们可以使用一个 NAND 门。对于所有的组合，除了两个输入都为 1 之外，NAND 门都返回 1，其真值表如下：

因此，我们可以创建一个指示信号，表示 x 小于 100，以及一个指示信号，表示 y 小于 100，并约束它们之间的 NAND 关系。

pragma circom 2.1.6;

include "circomlib/comparators.circom";
include "circomlib/gates.circom";

template DisjointExample2() {
  signal input x;
  signal input y;

  component nand = NAND();
  nand.a <== LessThan(252)([x, 100]);
  nand.b <== LessThan(252)([y, 100]);
  nand.out === 1;   
}

component main = DisjointExample2();

/* INPUT = {
  "x": "18",
  "y": "100"
} */

k 大于 x、y 或 z 中的至少 2 个

在这个例子中，我们试图表达 k 大于 x 和 y，或者 k 大于 x 和 z，或者 k 大于 y 和 z。k 可以大于 x、y 和 z，但这不是必需的。

由于表达上面这样复杂的逻辑表达式很冗长，所以简单的方法是把 k 大于的信号的数量加起来，然后检查这个数字是否大于等于 2。

pragma circom 2.1.6;

include "circomlib/comparators.circom";
include "circomlib/gates.circom";

template DisjointExample3(n) {
  signal input k;
  signal input x;
  signal input y;
  signal input z;

  signal totalGreaterThan;

  signal greaterThanX;
  signal greaterThanY;
  signal greaterThanZ;

  greaterThanX <== GreaterThan(252)([k, x]);
  greaterThanY <== GreaterThan(252)([k, y]);
  greaterThanZ <== GreaterThan(252)([k, z]);

  totalGreaterThan = greaterThanX + greaterThanY + greaterThanZ;

  signal atLeastTwo;
  atLeastTwo <== GreaterEqThan(252)([totalGreaterThan, 2]);
  atLeastTwo === 1;
}

component main = DisjointExample3();

/* INPUT = {
  "k": 20
  "x": 18,
  "y": 100,
  "z": 10
} */

不要忘记约束组件的输出！

有时，开发人员可能会忘记约束组件的输出，这可能会导致严重的安全漏洞！ 例如，以下代码可能看起来强制 x 和 y 都等于 1，但事实并非如此。x 和 y 可以为零（或任何其他任意值）。如果 x 和 y 为零，则 AND 门的 输出 将为零，但输出没有被约束为任何值。

template MissingConstraint1() {
  signal input x;
  signal input y;

  component and = AND();
  and.a <== x;
  and.b <== y;

  // and.out 没有约束，所以 x 和 y 可以有任何值！
}

类似地，以下电路不会强制 x 小于 100。如果 x 小于 100，则 LessThan 的输出为 1，但代码没有约束输出以确保这确实是真的。

template MissingConstraint2() {
  signal input x;

  component lt = LessThan(252);
  lt.in[0] <== x;
  lt.in[1] <== 100;

  // x 可以 ≥ 100，因为允许 lt.out 为 0 或任何其他任意值
}

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