如果我们想表达“x 可以等于 5 或 6”,我们可以简单地使用以下约束:
(x - 6) * (x - 5) === 0
然而,假设我们想要表达“x 小于 5 或者 x 大于 17”。在这种情况下,我们不能直接将这两个条件结合起来,因为如果 x 小于 5,它将违反 x 大于 17 的约束,反之亦然。
解决方案是为不同的条件(例如,x 小于 5,或大于 17)创建指示器(indicator)信号,然后对这些指示器应用约束。
Circomlib 比较器库
Circomlib comparator library 包含一个 LessThan 组件,它返回 0 或 1 来指示 in[0] 是否小于 in[1]。关于这个组件如何工作,已在 Arithmetic Circuit 章节中进行了描述。但作为总结,假设 x 和 y 最大为 3 位(bits)。如果我们计算 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 位数字,我们可以通过检查最高有效位是否被置位(set)来判断 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 will be explained in the next section
out <== LessThan(252)([a, b]);
}
component main = Example();
/* INPUT = {
"a": "9",
"b": "10"
} */
252 从何而来
在 finite field(有限域,这正是 Circom 所使用的)中的数字不能以“小于”或“大于”进行相互比较,因为典型的不等式代数定律并不适用。
例如,如果 ,那么当 为正数时, 应该始终成立。然而,在有限域中并非如此。我们可以选择一个 ,使其成为 的加法逆元,即 。然后我们就会得出一个荒谬的结论:0 大于一个非零数。例如,如果 且 并且 ,我们有 。但是,如果我们给 和 都加上 ,那么我们就会得到 。
252 指定了 LessThan 组件中的位数,用于限制 x 和 y 的最大值,以便能够进行有意义的比较(上一节中使用了 4 位作为示例)。
Circom 可以在有限域中容纳高达 253 位的数字。出于在 Alias Check 章节中讨论的安全原因,我们不应该将一个域元素转换为能够编码大于该域的数字的二进制表示。因此,Circom 不允许使用超过 252 位来实例化比较模板(source code)。
然而,回想一下,对于 LessThan(n),我们需要计算 z = 2^n + (x - y),并且 2^n 需要比 x 或 y 大一位。因此,x 和 y 最大只能是 位。由于 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 门(与非门)。对于所有组合,NAND 门都返回 1,除非两个输入都是 1,其真值表如下:
| a | b | out |
|---|---|---|
| 0 | 0 | 1 |
| 0 | 1 | 1 |
| 1 | 0 | 1 |
| 1 | 1 | 0 |
因此,我们可以创建一个指示 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 中的至少两个
在这个例子中,我们试图表达 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 is not constrained, so x and y can have any values!
}
同样,以下电路也没有强制 x 小于 100。如果 x 小于 100,LessThan 的输出为 1,但代码并没有对该输出进行约束以确保这确实成立。
template MissingConstraint2() {
signal input x;
component lt = LessThan(252);
lt.in[0] <== x;
lt.in[1] <== 100;
// x could be ≥ 100 since lt.out is allowed to be 0 or any other arbitrary value
}