【session 2】Exercise - isNegative 的input in 应该是-1 还是21888242871839275222246405745257275088548364400416034343698204186575808495616？

[abbylow]

以下代码是我根据Sign template所做的解答

由于isNegative的input signal in不是Array，我加了一步，用Num2Bits转换in。

代码

pragma circom 2.1.2;

include "circomlib/compconstant.circom";

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

    component n2b = Num2Bits(254);
    component comp = CompConstant(10944121435919637611123202872628637544274182200208017171849102093287904247808);

    n2b.in <== in;
    comp.in <== n2b.out;
    out <== comp.out;
}

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

/* INPUT = {
    "in": "-1"
} */

疑问

如果我的in是-1，得到的output是out = 0而非预想的1，为什么呢？

当10944121435919637611123202872628637544274182200208017171849102093287904247808 < in <= 21888242871839275222246405745257275088548364400416034343698204186575808495616，out是1 （这部分是符合题目要求的）

但我对题目的解读是，in是-1的时候应该也能返回out=1

尝试过的解决方法

我觉得问题出在转换-1去bit的部分，所以单独跑了一次Num2Bits，发现-1在Num2Bits里等于4294967295（也就是2^32-1）

pragma circom 2.1.2;

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;
    log(in);
}


component main = Num2Bits(254);

/* INPUT = {
    "in": "-1"
} */

如果要让IsNegative在in = -1时，返回1，要怎么写呢？

[dajuguan]

首先说明为什么-1会变成4294967295，这可能是由于circom里面表示负数实际上将负数转换为了32位的补码，其二进制表示为11111111111111111111111111111111,即10进制的4294967295。
其次需要说明的是，为什么不能直接输入-1。这个问题涉及到有限域上负数定义的心智模型，即为什么(p/2,p-1]定义为负数? p = 21888242871839275222246405745257275088548364400416034343698204186575808495617.
首先需要明确的是，负数在有限域上并非只是一个数，而是一组mod p相同的数。
考虑 p=7的有限域上的运算:
$$(-1) mod 7 = (7-1) mod 7 = 6 mod 7.$$
那么似乎我们只需要circom在处理输入时，将-1转换为p-1就可以表示负数，这样在circom上书写负数也很简单，为什么要这么麻烦地限定(p/2,p-1]来表示负数呢？
这里是为了表示的一致性，考虑更小的负数-5的表示：
$$(-5) mod 7 = 2 mod 7 .$$ 在此种情况下 -5实际上与2在有限域上是一致的，那么-5实际上应该是负数还是正数呢？
这个问题就很显然了，必须定义[0,2/p)的为正数这样才有所谓的正数。而如果用-5去表示的话，会让人很困惑，因为他实际上应该是正数2。因此直接用-1表示，就会违背负数表示的一致性。

[abbylow]

让我尝试理解一下你的解答，意思是input应该就是p-1而不是-1对吧？

那输入input的人需要提前知道prime number是多少了，若如微信群里讨论的那般，替换了babyjubjub成别的prime number，那之前输入的input需要被重新计算了。我不确定这是不是一个concern，就是想问一下有没有允许用户输入-1就能行的方法。

另外想确认一下，以上回答的

为什么要这么麻烦地限定(2/p,p-1]来表示负数呢？

这里应该是(p/2, p-1]吧？

必须定义[0,2/p)的为正数这样才有所谓的正数

这里应该是[0, p/2)？

[dajuguan]

感谢指出，已修正。群里的讨论是有道理的，不应该把必须知道prime number的负担留给开发者，直接提供-1这样的API给开发者，并在文档中说明负数的范围实际上会更好。这里Circom处理的确实不是很好，具体而言，首先他会在此处把-1转换为arrFr=[0,0,0,0,0,0,0,-1]:

                const arrFr = toArray32(BigInt(fArr[i]) % this.prime, this.n32) //this.n32=8
                for (let j = 0; j < this.n32; j++) {
                    this.instance.exports.writeSharedRWMemory(
                        j,
                        arrFr[this.n32 - 1 - j]
                    )
                }

然后再调用writeSharedRWMemory将这些值写入电路中，问题其实出在了这里：

在调用i32 store的时候猜测会把其转换为32位的补码表示。

[abbylow]

那么我们确认是zkRepl的问题了，我按https://zkiap.com/snarkjs 的步骤自己安装了circom和snarkjs

circuit.circom

pragma circom 2.1.2;

template Num2Bits(n) {
    signal input in;
    signal output out[n];
    var lc1=0;
log("in", in);
    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;
    }
log("lc1", lc1);
    lc1 === in;
}

component main = Num2Bits(254);

input.json
{"in": -1}

用circom circuit.circom --r1cs --wasm --sym创建需要用来证明的文件
然后cd circuit_js里运算witness

node generate_witness.js circuit.wasm ../input.json ../witness.wtns

这里可以确定的是circom可以接受-1为input，不需要输入input的人事先知道prime number的值

mystery solved 🫶🏻