先指示再约束 - 在 Circom 中复杂约束条件的方法
- RareSkills
- 发布于 2025-04-16 10:13
- 阅读 902
本文介绍了在 Circom 中使用 indicator signals 和 Circomlib comparator library 来实现复杂约束条件的方法。
如果我们想表达 “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。
| 数字 | 二进制表示 | 是否大于或等于 2^3 |
|---|---|---|
| 15 | 1111 | 是 |
| 14 | 1110 | 是 |
| 13 | 1101 | 是 |
| … | ||
| 10 | 1010 | 是 |
| 9 | 1001 | 是 |
| 8 (2^3) | 1000 | 是 |
| 7 | 0111 | 否 |
| 6 | 0110 | 否 |
| … | ||
| 2 | 0010 | 否 |
| 1 | 0001 | 否 |
| 0 | 0000 | 否 |
对于一般的 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 大一位。因...
