Unable to verify a Cairo 1 proof

[gswirski]

trafficstars

While working on cairo-hints, we’ve noticed that the latest lambdaworks prover for Cairo 1 is unable to verify a proof it successfully generated from cairo1-run’s trace and memory files (cairo1-run is part of cairo-vm).

Steps to reproduce

Sample program

I am using this example circuit:

# simple.cairo
fn main() -> bool {
    2 == 2
}

Trace and memory files

Inside cairo-vm's cairo1-run script:

cargo run ../cairo_programs/cairo-1-programs/simple.cairo --trace_file ../cairo_programs/cairo-1-programs/simple.trace --memory_fi
le ../cairo_programs/cairo-1-programs/simple.memory

When I create the memory and trace files using the latest cairo1-run in cairo-vm 1f98feff566dd2da016e439f5e8db912c6e39872, the proof generated fails verification after the 2nd step. In this version of cairo1-run I tried generating memory and trace files with and without the flag --proof_mode.

This seems to be a recent regression. When I create the memory and trace files with cairo1-run in cairo-vm v0.9.1 and cairo-vm v0.9.2, the proof generated by provers/cairo is verified successfully.

Proving and verification

I ran these commands in lambdaworks/provers/cairo (#212c040c5fa21fcb5095a0b1ac92501292517db0)

# PROVE
cargo run --release --features=cli,instruments,parallel prove simple.trace simple.memory simple.proof
# successfully creates simple.proof

# VERIFY
cargo run --release --features=cli,instruments,parallel verify simple.proof
# verification fails on step 2

Additional context

I noticed that the latest version of cairo-vm updated cairo-lang dependencies from v2.3.1 to v2.5.3 - maybe it is related?

Is lambdaworks prover and verifier expected to work with cairo-lang v2.5.3? Either way, it probably shouldn’t generate proofs that cannot be verified later.

[MauroToscano]

This must has been a change in the Cairo VM. I'll raise the issue to the VM team, and we'll pin the version here to use until it gets fixed.

[MauroToscano]

I have updated the docs here, until we get it fixed:

https://github.com/lambdaclass/lambdaworks/pull/809

[MauroToscano]

Can you try with ?

cargo run simple.cairo --trace_file simple.trace --memory_file simple.memory --proof_mode --layout small

There seems to be an issue of the VM not activating the output builtin correctly without small

[Eagle941]

@MauroToscano Setting small or all_cairo leads to correct proof verification.

Thank you for your help!