Circom编译器化简后移除关键约束的技术问询

我在测试circomlib中n=8的Num2Bits模板时，观察到以下现象：

未化简的R1CS #

[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.out[0] ] * [ main.out[0] ] - [  ] = 0
[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.out[1] ] * [ main.out[1] ] - [  ] = 0
[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.out[2] ] * [ main.out[2] ] - [  ] = 0
[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.out[3] ] * [ main.out[3] ] - [  ] = 0
[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.out[4] ] * [ main.out[4] ] - [  ] = 0
[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.out[5] ] * [ main.out[5] ] - [  ] = 0
[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.out[6] ] * [ main.out[6] ] - [  ] = 0
[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.out[7] ] * [ main.out[7] ] - [  ] = 0
[INFO]  snarkJS: [  ] * [  ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.out[0] +21888242871839275222246405745257275088548364400416034343698204186575808495615main.out[1] +21888242871839275222246405745257275088548364400416034343698204186575808495613main.out[2] +21888242871839275222246405745257275088548364400416034343698204186575808495609main.out[3] +21888242871839275222246405745257275088548364400416034343698204186575808495601main.out[4] +21888242871839275222246405745257275088548364400416034343698204186575808495585main.out[5] +218... ] = 0

开启完全化简后的R1CS #

[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.out[0] ] * [ main.out[0] ] - [  ] = 0
[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.out[1] ] * [ main.out[1] ] - [  ] = 0
[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.out[2] ] * [ main.out[2] ] - [  ] = 0
[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.out[3] ] * [ main.out[3] ] - [  ] = 0
[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.out[4] ] * [ main.out[4] ] - [  ] = 0
[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.out[5] ] * [ main.out[5] ] - [  ] = 0
[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.out[6] ] * [ main.out[6] ] - [  ] = 0
[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.out[7] ] * [ main.out[7] ] - [  ] = 0

为何最后一条用于检查比特和与原始输入对应关系的约束会被移除？这条约束看起来是R1CS必须包含的关键约束，是否有我忽略的点？

解答 #

这条约束被移除的核心原因是它是一个冗余的恒等式约束，具体拆解如下：

1. 约束的本质
   你看到的最后一条约束是线性约束形式：0*0 - (线性组合) = 0，等价于要求线性组合 = 0。结合circomlib中Num2Bits模板的实现，这个线性组合实际对应sum(out[i] * 2^i) - in = 0，也就是要求输出比特的加权和等于输入值。

2. 冗余性的来源
   Num2Bits模板中，输出比特out[i]是通过<--赋值语句定义的：out[i] <-- (in >> i) & 1。在circom编译过程中，<--是计算赋值，意味着编译器会直接将out[i]替换为(in >> i) & 1的表达式，而不是将其作为独立变量处理。

   此时，sum(out[i] * 2^i)的结果必然等于输入in（这是二进制数的基本性质），因此这条约束就变成了in - in = 0，也就是恒成立的无意义约束。

3. 保留的约束的作用
   化简后保留的8条二次约束，每条对应out[i] * (out[i] - 1) = 0（模椭圆曲线域下等价于你看到的(p-1 + out[i]) * out[i] = 0，其中p是BN254的阶），作用是强制每个out[i]只能取0或1——这才是Num2Bits模板真正需要的约束，确保输出是合法的二进制比特。

总结来说，那条线性约束在模板实现逻辑下是完全冗余的，化简器会自动识别并移除这类恒等式约束，不会影响电路的正确性。

内容的提问来源于stack exchange，提问作者The Bor