【session 2】中间signal可以不在电路里给出计算方式而在实际prove里提供么？

[lkiversonlk]

举个简单的例子:

pragma circom 2.1.2;
include "circomlib/poseidon.circom";

template IsZero() {
    signal input in;
    signal input out;

    signal inv;

    inv <-- in!=0 ? 1/in : 0;

    out === -in*inv +1;
    in*out === 0;
}
component main { public [out]} = IsZero();

//0 success, 1 failed
/* INPUT = {
   "in": "3",
   "out": "0"    
} */

这个电路就是用来证明我知道一个值，它是非零而不暴露这个值本身。

问题在于这一句:

inv <-- in!=0 ? 1/in : 0;

如果把这一句改成如下:

pragma circom 2.1.2;
include "circomlib/poseidon.circom";

template IsZero() {
    signal input in;
    signal input out;

    signal inv;

    inv <-- 2;
    //inv <-- in!=0 ? 1/in : 0;

    out === -in*inv +1;
    in*out === 0;
}
component main { public [out]} = IsZero();

//0 success, 1 failed
/* INPUT = {
   "in": "3",
   "out": "0"    
} */

编译是可以通过的，但是下面的assertion会fail掉，但是按照之前另一个讨论的结果，这个赋值只是做preprove，并不会影响最终的约束生成。

那我们应该可以用这个改后的代码生成的约束系统，和我们自己另外生成的正确的prove key去通过verify？
这个过程有哪里可以参考么？

补充一个问题：

template IsZero() {
    signal input in;
    signal input out;

    signal inv;

    inv <-- in!=0 ? 1/in : 0;

    out === -in*inv +1;
    in*out === 0;
}

如果in在该域内没有倒数，这个preprove是不是就没法进行，只能自己手动去提供？

[izayl]

可能是你没 get 到文章里的隐含意思。

题目可以理解为：

写一个电路，input 为任意数字，当 input 为 0 时，output 为 1，当 input 不为 0 时，output 为 0。

所以在这个前提下，需要有一个赋值操作，一个约束。

赋值：out <== -in*inv + 1 ，这里 out 只能为 1 或者 0，
约束：in * out === 0, 保证 in 为 0，这里当然也可以换其他的证明 in 为 0 的方式，用 in * out 是为了在给 out 加一个约束

[lkiversonlk]

不是哎，其实我想问的是怎么自己手动生成verification.

 inv <-- 2;

这么写之后assertion肯定会fail，这个是预期中的，但是理论上生成的verifier code还是可以用的，只是preprove部分有问题，如果手动生成verification应该是可以过verify的，想问下这个怎么具体操作。

[lkiversonlk]

郭老师在会上已经回答了，这个是可以自己去单独生成verification的。