先指示再约束 - 在 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 大一位。因...