【session 2】有推荐或者规范的circom写法么

[lkiversonlk]

circom的写法感觉非常灵活，比如exercise里的IsZero，除了标准答案的写法外，写成:

pragma circom 2.1.2;
include "circomlib/poseidon.circom";
// include "https://github.com/0xPARC/circom-secp256k1/blob/master/circuits/bigint.circom";
template IsZero () {
    signal input in;
    signal output out;
    var a;
    if (in > 0) {
        a = 1;
    } else {
        a = 0;
    }
    out <-- a;
    out * (out -1) === 0;
}
component main = IsZero();
/* INPUT = {
   "in": "8"
} */

也能编译通过，看起来没问题，但是这种写法是否可行？
circom电路有类似best practise的参考么

[qizhou]

我认为这个代码是有问题的。<--的语句是pre-prove提供的witness，但是电路并没有约束a的具体数值。这样的话即使a为任意一个{0,1} （跟in独立的），该电路都可以通过验证的。也就是电路等价于：

pragma circom 2.1.2;
include "circomlib/poseidon.circom";
// include "https://github.com/0xPARC/circom-secp256k1/blob/master/circuits/bigint.circom";
template IsZero () {
    signal input in;
    signal output out;
    signal input a;
    out <== a;
    out * (out -1) === 0;
}

回到原来的代码：

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

    signal inv;

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

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

其中inv也是pre-prove的一个witness，但是inv不满足in!=0 ? 1/in : 0，电路是无法通过的。可以简单的演算如下：

• 如果in > 0，那么out必须为0，否则 in * out === 0无法成立，又因为 out === -in * inv + 1 使得 in * inv = 1，所以inv 必须是 1/in才能够通过电路约束。
• 如果in === 0, 那么in * out === 0的约束，使得out可以是任意一个数。又因为 out === -in * inv + 1，使得 out ===1 ，所以必须out === 1 才能够通过电路约束。（注意在这种情况下，inv可以是任意的值，但是不影响电路的约束的正确性）。

[qizhou]

也不行的，所有的<--都是preprove生成的，没有电路约束的。介绍可以看课程这一段https://youtu.be/El64GK_rM6c?t=3602。

[lkiversonlk]

我重新看了遍，现在的理解是：

1. 只有 <==和===才会被编译到最后的约束系统里
2. <--和一些其他的计算，是为了方便根据input 生成 prove用的，即使没有这些计算，prover手动算出来放到最后proving过程里也可以。
3. 之前的错误答案里的计算和赋值，只是实现了“prover不作恶情况下如何根据input计算出正确的值”，并不能防止“恶意的prover用错误值通过verify”， 因为这些没有进入最后的约束里。

[LowLowCoder-Mel]

我的理解哈,

1. 理解操作符的含义
   circom的文档中说 signal 只能使用 <-- 或 <== 进行赋值， <== 这个操作符的含义是给 signal 赋值的同时也生成了约束，
   <-- 操作符一般只有在分配表达式无法包含在约束中时才会使用。
2. 什么样的表达式无法包含在约束中的

• 表达式需要使用某些函数或操作符，这些函数或操作符在 Circom 的约束语言中不可用。例如，表达式包含一个复杂的算法或加密函数。
• 表达式的计算需要更复杂的数据结构，例如数组或哈希表。约束语言可能无法处理这些结构。
• 表达式需要使用来自外部源的数据，例如区块链上的交易数据或其他外部应用程序的状态。
  在这些情况下，我们可能就需要使用单向箭头符号 <-- 进行信号分配，以便将输入数据输入到电路中进行计算。
  这种方法具有一定的风险，因为它可能会导致电路出现的安全性问题。建议尽量是使用 <== 或者 ==> 操作符

3. 上述问题的讨论

pragma circom 2.1.2;

include "circomlib/poseidon.circom";

template IsZero() {
    signal input in;
    signal output out;
    signal a;
    a <-- in != 0 ? 1 : 0;
    out <== a;
}

component main { public [in] } = IsZero();

/* INPUT = {
    "in": "100"
} */

我在 zkrepl 里面跑是可以正常编译并通过的。语法上应该可以通过的， 但是这么改写可能会存在一定的安全性隐患。 因为 a 只是被赋值但是并未产生相应的约束。 编译器也是温馨的提示这行代码: "The assigned signal a is not constrained here."

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

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

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

这种写法我认为会更加的严谨一些。

以上为为个人理解，如果不对地方 望各位大佬指正。

[lkiversonlk]

补充下几个点，确认下理解是一样的：

template IsZero() {
    signal input in;
    signal output out;
    signal a;
    a <-- in != 0 ? 1 : 0;
    out <== a;
}

这个写法是错的，不止是不严谨，因为约束里没有约束a，prover最后可以用一个 (in, a, out) = (5, 0, 0)过验证，满足out = a, 但是这个明显是个错误的isZero结果.

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

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

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

这个写法的核心其实是最后两个约束

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

假设inv可以任意值，in * out = 0，所以in和out必须至少有一个为0，然后我们只需要排除in, out同时为0，就可以达到:

if in == 0, out != 0
if out == 0, in != 0

也就是isZero的实际含义。

排除in = out = 0, 就靠out <== -in*inv +1;这一句，因为in, out 同时为0时候，无论inv为任何值，这个等式都不可能成立。

这才是这个约束的精妙之处，至于上面的赋值:

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

只是用来做preprove生成验证结果用的，其实核心约束系统里要忽略掉这一句

[qwang98]

补充下几个点，确认下理解是一样的：

template IsZero() {
    signal input in;
    signal output out;
    signal a;
    a <-- in != 0 ? 1 : 0;
    out <== a;
}

这个写法是错的，不止是不严谨，因为约束里没有约束a，prover最后可以用一个 (in, a, out) = (5, 0, 0)过验证，满足out = a, 但是这个明显是个错误的isZero结果.

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

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

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

这个写法的核心其实是最后两个约束

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

假设inv可以任意值，in * out = 0，所以in和out必须至少有一个为0，然后我们只需要排除in, out同时为0，就可以达到:

if in == 0, out != 0
if out == 0, in != 0

也就是isZero的实际含义。

排除in = out = 0, 就靠out <== -in*inv +1;这一句，因为in, out 同时为0时候，无论inv为任何值，这个等式都不可能成立。

这才是这个约束的精妙之处，至于上面的赋值:

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

只是用来做preprove生成验证结果用的，其实核心约束系统里要忽略掉这一句

还有个问题：用作赋值的intermediate参数，就是a，有这样的赋值：a <-- in != 0 ? 1 : 0;
是否可以说已经限定了a只能是1或者0
那prover是否还可以强行给a赋值？
比如你上面说的（5，0，0）的情况

[qwang98]

还有个问题：用作赋值的intermediate参数，就是a，有这样的赋值：a <-- in != 0 ? 1 : 0;
是否可以说已经限定了a只能是1或者0
那prover是否还可以强行给a赋值？
比如你上面说的（5，0，0）的情况