Zokrates/ZoKrates

Different result on two equivalent less-than comparisons

gwdjkspnado opened this issue · 2 comments

Description

In the code below, variable b is provided with value p - 1 during runtime, where p is the largest value of the finite field; variable c is assigned to be 3. The variable pMinusOne is a constant variable statically assigned to be p - 1. As such, variable b holds the same value as variable pMinusOne during runtime, and c > b should have the same truth value as c > pMinusOne. However, c > b evaluates to true but c > pMinusOne evaluates to false.

const field pMinusOne = 21888242871839275222246405745257275088548364400416034343698204186575808495616;

def main(private field b, private field c) {
    // During runtime, c is 3f, b is pMinusOne
    assert(c > b);          // This constraint passes
    assert(c > pMinusOne);  // This constraint is equivalent as above, but fails
}

Moreover, if you comment out the line assert(c > pMinusOne);, the verification passes.

Environment

  • Compiler version: 0.8.7
  • Operating system: Ubuntu 22.04 LTS

Steps to Reproduce

Save the code above into buggy_input.zok. Create a file input.json and add the following content:

[
    "21888242871839275222246405745257275088548364400416034343698204186575808495616",
    "3"
]

Run the following commands from CLI:

zokrates compile -i buggy_input.zok
zokrates setup
zokrates compute-witness --abi --stdin <input.json
zokrates generate-proof
zokrates verify

You would see the following output:

Compilation failed:

buggy_input.zok:
        Assertion failed (buggy_input.zok:6:5)
make: *** [Makefile:13: out] Error 1

The error messages says that line 6 (assert(c > pMinusOne);) fails.

Comment out line 6 and re-run the commands above, you would see the verification passes:

zokrates compile -i buggy_input.zok
Compiling buggy_input.zok

Compiled code written to 'out'
Number of constraints: 258
zokrates setup
Performing setup...
Verification key written to 'verification.key'
Proving key written to 'proving.key'
Setup completed
zokrates compute-witness --abi --stdin <input.json
Computing witness...
Witness file written to 'witness'
zokrates generate-proof
Generating proof...
Proof written to 'proof.json'
zokrates verify
Performing verification...
PASSED
dark64 commented

It seems assert(c > pMinusOne) should fail at compile time as no c can be greater than pMinusOne. This fails as it should in #1309

@Schaeff any thoughts?

I mean, the issue here is that assert(c > b) at line 5 should fail if the b and c are fed with 21888242871839275222246405745257275088548364400416034343698204186575808495616 a.k.a. pMinusOne, and 3, respectively. However, the verification passes, meaning that somehow the verifier mistakenly thinks that 3 > 21888242871839275222246405745257275088548364400416034343698204186575808495616 is true, which is definitely wrong.

To see that, you can save the following code into buggy_input.zok:

const field pMinusOne = 21888242871839275222246405745257275088548364400416034343698204186575808495616;

def main(private field b, private field c) {
    // During runtime, c is 3f, b is pMinusOne
    assert(c > b);          // This constraint passes the verification when b is given 3 and c is assigned pMinusOne during runtime. This is unexpected.
}

Also, save the following into input.json as runtime input for variable b and c:

[
    "21888242871839275222246405745257275088548364400416034343698204186575808495616",
    "3"
]

Then run the following:

zokrates compile -i buggy_input.zok
zokrates setup
zokrates compute-witness --abi --stdin <input.json
zokrates generate-proof
zokrates verify

You would see the following output, meaning that the verification thinks assert(c > b) passes, which is unexpected:

Compiling buggy_input.zok

Compiled code written to 'out'
Number of constraints: 258
Performing setup...                                                                                                  
Verification key written to 'verification.key'
Proving key written to 'proving.key'
Setup completed
Computing witness...
Witness file written to 'witness'
Generating proof...
Proof written to 'proof.json'
Performing verification...
PASSED