Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Different result on two equivalent less-than comparisons #1327

Open
gwdjkspnado opened this issue Jun 14, 2023 · 2 comments
Open

Different result on two equivalent less-than comparisons #1327

gwdjkspnado opened this issue Jun 14, 2023 · 2 comments

Comments

@gwdjkspnado
Copy link

gwdjkspnado commented Jun 14, 2023

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
Copy link
Member

dark64 commented Jul 25, 2023

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?

@gwdjkspnado
Copy link
Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants