【session 2】在了解了约束后，对于Num2Bits电路突然产生了疑惑

[HurmousDay]

在了解完 只有 === 和 <== 才能产生约束后，我对于 Num2Bits 这一案例产生了疑惑

Num2Bits 的原始代码如下：

template Num2Bits(n) {
    signal input in;      
    signal output out[n]; 
    var lc1=0;            

    var e2=1; 
    for (var i = 0; i<n; i++) {      
        out[i] <-- (in >> i) & 1;    
        out[i] * (out[i] -1 ) === 0; 
        lc1 += out[i] * e2;
        e2 = e2+e2;
    }

    lc1 === in; 
}

在只考虑约束电路的时候，Nums2Bits代码变成了如下形式（只保留 === 与 <===）

template Num2Bits(n) {
    signal input in;      
    signal output out[n]; 

    for (var i = 0; i<n; i++) {       
        out[i] * (out[i] -1 ) === 0; 
    }
    lc1 === in; 
}

此时的lc1变量虽然收到了约束，但是如果由我们自己伪造输入lc1，完全可以将其输入为跟 in相等的值。那么此时的约束不是仅剩下了 out[i]*(out[i]-1) === 0
我们是不是该增加一个约束 lc1 与 out的关系呢？这样感觉逻辑才能完备

[lkiversonlk]

lc1不能伪造哈，lc1是一个var，不是signal，这个var是根据out计算出来的, 不是能自己随便给的，跟signal不一样。

这个电路里其实有in, out两个signal, lc1本质上是根据out signal计算出来的一个值，所以实际约束是：

1. out必须是一个0/1数组
2. out按位加和(即lc1)必须等于in