EMBED unpack undefined behavior

[alv-around]

Undefined behavior of EMBED's unpack

I found an undefined behavior in an edge case when unpacking fields into bool arrays. More concretely, when you are trying to unpack a field into a bit array of length > 254 bits. I think the compiler assumes that the bit size of a field is 254 bits, and that is the case for the curve bn128, but the bls12_381 has 255 bits. So if you are writting a circuit for the latter curve you can run into the following error.

Environment

• Compiler version: zokrates:0.8.7 (but this should still occur in 0.8.8)
• Operating system: macos Sonoma (M1)

Steps to Reproduce

the way unpack is implemented unpack(a) will return a bool array of length <= 254 if a < $2^{254}$ and only a larger array of length n if $2^{n-1} \le a < 2^{n}$. This leads to obscure consequences..

Take the following code.

from "EMBED" import unpack;

def main() {
    field p_minus_one_bn128 = 21888242871839275222246405745257275088548364400416034343698204186575808495616;

    bool[4] five = unpack(5);
    assert(five == [false, true, false, true]);

    bool[254] p_254b = unpack(p_minus_one_bn128);
    assert(p_254b == [true, true, false, false, false, false, false, true, true, false, false, true, false, false, false, true, false, false, true, true, true, false, false, true, true, true, false, false, true, false, true, true, true, false, false, false, false, true, false, false, true, true, false, false, false, true, true, false, true, false, false, false, false, false, false, false, true, false, true, false, false, true, true, false, true, true, true, false, false, false, false, true, false, true, false, false, false, false, false, true, false, false, false, true, false, true, true, false, true, true, false, true, true, false, true, false, false, false, false, false, false, true, true, false, false, false, false, false, false, true, false, true, false, true, true, false, false, false, false, true, false, true, true, true, false, true, false, false, true, false, true, false, false, false, false, false, true, true, false, false, true, true, true, true, true, false, true, false, false, false, false, true, false, false, true, false, false, false, false, true, true, true, true, false, false, true, true, false, true, true, true, false, false, true, false, true, true, true, false, false, false, false, true, false, false, true, false, false, false, true, false, true, false, false, false, false, true, true, true, true, true, false, false, false, false, true, true, true, true, true, false, true, false, true, true, false, false, true, false, false, true, true, true, true, true, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false]);

    bool[255] p_255b = unpack(p_minus_one_bn128);
    assert(p_255b == [false, true, true, false, false, false, false, false, true, true, false, false, true, false, false, false, true, false, false, true, true, true, false, false, true, true, true, false, false, true, false, true, true, true, false, false, false, false, true, false, false, true, true, false, false, false, true, true, false, true, false, false, false, false, false, false, false, true, false, true, false, false, true, true, false, true, true, true, false, false, false, false, true, false, true, false, false, false, false, false, true, false, false, false, true, false, true, true, false, true, true, false, true, true, false, true, false, false, false, false, false, false, true, true, false, false, false, false, false, false, true, false, true, false, true, true, false, false, false, false, true, false, true, true, true, false, true, false, false, true, false, true, false, false, false, false, false, true, true, false, false, true, true, true, true, true, false, true, false, false, false, false, true, false, false, true, false, false, false, false, true, true, true, true, false, false, true, true, false, true, true, true, false, false, true, false, true, true, true, false, false, false, false, true, false, false, true, false, false, false, true, false, true, false, false, false, false, true, true, true, true, true, false, false, false, false, true, true, true, true, true, false, true, false, true, true, false, false, true, false, false, true, true, true, true, true, true, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false, false]);
}

Lets assume I want to write a circuit on bls12_381, the following curve should pass. However, the compiler throws an assertion error on the third assert. Note that the arrays used in the 2nd and 3rd assert are exactly the same but for the additional false at the beginning of the 3rd array representing the trailing zero.

This is the root cause, that in order for the jubjub implementation to work atm, the stdlib has to make the case distinction between values that are <$2^{254) and when values are <$2{255}

Proposal

The proposal would be to modify this threshold either to bitsize of the bigger curve, 255 bit, or to the arbitrary length of 256 bits.

This will not have a negative impact on circuits on smaller curves as the affected values at the moment would be wrapped by the modulo.

The other case, when p is larger than the boolean array, is handled by ZoKrates with an exception (#955) .which I see no objection:

    bool[253] p_253b = unpack(p_bn128);
    assert(p_253b == [true, false, false, false, ...]);

error message:

Cannot unpack `21888242871839275222246405745257275088548364400416034343698204186575808495616` to `bool[253]`: value is too large

[alv-around]

I just find out that this problem is solve by adding the -c bls12_381 to the flag 🙈