Open gwdjkspnado opened 1 year ago
It seems assert(c > pMinusOne)
should fail at compile time as no c
can be greater than pMinusOne
. This fails as it should in https://github.com/Zokrates/ZoKrates/pull/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
Description
In the code below, variable
b
is provided with valuep - 1
during runtime, wherep
is the largest value of the finite field; variablec
is assigned to be3
. The variablepMinusOne
is a constant variable statically assigned to bep - 1
. As such, variableb
holds the same value as variablepMinusOne
during runtime, andc > b
should have the same truth value asc > pMinusOne
. However,c > b
evaluates to true butc > pMinusOne
evaluates to false.Moreover, if you comment out the line
assert(c > pMinusOne);
, the verification passes.Environment
Steps to Reproduce
Save the code above into
buggy_input.zok
. Create a fileinput.json
and add the following content:Run the following commands from CLI:
You would see the following output:
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: