search

lambdaclass / cairo-vm

cairo-vm is a Rust implementation of the Cairo VM. Cairo (CPU Algebraic Intermediate Representation) is a programming language for writing provable programs, where one party can prove to another that a certain computation was executed correctly without the need for this party to re-execute the same program.
https://lambdaclass.github.io/cairo-vm
Apache License 2.0
485 stars 133 forks source link

Cairo1 proven with Stone fails STARK verification on programs with recursion #1705

Closed Okm165 closed 2 months ago

Okm165 commented 2 months ago

Exploring Cairo1-run Proving

Setup: Cairo1 program ➔ Cairo1-run (recursive layout) ➔ Stone Prover ➔ cairo0-verifier (recursive layout debug mode)

Issue: Some programs work well, while others fail during the cairo0-verifier stage, specifically on the verify_oods that suggests layout/constraint mismatch.

List of Programs Tried:

Working:

Not Working:

Observation: There seems to be an issue with regular recursion, but it's possible there's another underlying problem. I investigate further but insights and help would be greatly appreciated. Cheers

pefontana commented 2 months ago

Hi @Okm165 ! Thanks for the report. Yes, we are still working on the proving. Can you try running this program with this branch https://github.com/lambdaclass/cairo-vm/pull/1704/files. We still need to merge it but the Fibonacci and Factorial programs can be verified with stone prover

fmoletta commented 2 months ago

Hello! which branch did you run this on?

Okm165 commented 2 months ago

Hey it was main branch

Okm165 commented 2 months ago

Hi guys ;) There seems to be a problem with proof mode run of cairo1-run: branch: cairo-lang-2.6.3 commit: b72f5a93ffeb7de43c2b357ca1555d543c599b0d

This works as expected:

cargo run --release ../cairo_programs/cairo-1-programs/simple.cairo --print_output

Program Output : true

But proof mode makes it fail:

cargo run --release ../cairo_programs/cairo-1-programs/simple.cairo --trace_file program.trace --memory_file program.memory --air_public_input air_public_inpuy.json --air_private_input air_private_input.json --proof_mode

Error: VirtualMachine(Memory(AddressNotRelocatable))

Do u know what happens? Am i doing smth wrong?

Okm165 commented 2 months ago

Issue solved! branch: cairo-lang-2.6.3 commit: b72f5a93ffeb7de43c2b357ca1555d543c599b0d

All previously failing programs are now successfully running -> proving ->verifying (recursive layout) Thanks for help guys!

Some Stats:

What kind of changes does cairo-lang-2.6.3 introduce?

Okm165 commented 2 months ago

@fmoletta Do u know approx. when cairo-lang-2.6.3 is going to be merged to main?

fmoletta commented 2 months ago

@fmoletta Do u know approx. when cairo-lang-2.6.3 is going to be merged to main?

We are soon merging #1709 which bumps the compiler version to 2.6.3 and also skips gas checks during compilation