The condition n == 0 ? 0 : 2**n - in is not correct for computing the two's complement representation of in

[Unchain68]

There are a couple of issues with this code:

The condition n == 0 ? 0 : 2n - in is not correct for computing the two's complement representation of in. It should be in < 0 ? 2n + in : in instead, as I explained in a previous answer. This is because in two's complement representation, the most significant bit (i.e., the leftmost bit) is used to indicate the sign of the number, so we need to check if in is negative and compute the complement accordingly.

The assertion out[i] * (out[i] - 1) === 0 is not necessary and does not contribute to the correctness of the code. This assertion checks that out[i] is either 0 or 1, which is always true because of the bitwise operation used to compute out[i]. Therefore, it can be removed without affecting the behavior of the code.

Here is the corrected version of the code:

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

    component isZero;

    isZero = IsZero();

    var neg = in < 0 ? 2**n + in : in;

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

    in ==> isZero.in;

    lc1 + isZero.out * 2**n === (in < 0 ? 2**n + in : in);
}

Why this "The assertion out[i] * (out[i] - 1) === 0" is not nessary

The assertion out[i] * (out[i] - 1) === 0 in the Num2BitsNeg template is used to ensure that the value of each bit in the two's complement binary representation of the input is either 0 or 1. This assertion is necessary in the original Num2Bits template, which assumes that the input is non-negative and expects its two's complement binary representation to have exactly n bits.

However, in the Num2BitsNeg template, we first convert the input to its two's complement representation using var neg = in < 0 ? 2**n + in : in;. This means that neg can have up to n + 1 bits, depending on the value of in. Therefore, it is possible for the assertion out[i] * (out[i] - 1) === 0 to fail for certain inputs, because some of the bits in the two's complement representation of neg may be set to 0 or 1 beyond the first n bits.

In practice, this may not be a problem if the output of Num2BitsNeg is only used within a limited range of inputs (e.g., if we know that in is always within a certain range). However, if we want to ensure that the output of Num2BitsNeg is always correct for any value of in, we may need to modify the template to handle the extra bit in neg. One way to do this would be to add an extra output signal to Num2BitsNeg to represent the sign bit of neg, and modify the linear combination and zero-check to take this into account.