Verifying Cairo proofs on Ethereum
written by Jason Park on

We have been working with StarkWare on building the EVM adapter, and are pleased to announce that we have recently successfully verified Cairo proofs on the Ethereum mainnet! We are furthering the work of Andrew Milson and Aditya Bisht who have reached this milestone before us, and we believe that this is a big step forward towards making StarkWare’s technology more accessible to the open-source community.

In this post, we’d like to share some background into how Cairo programs are verified on Ethereum, and perhaps motivate some of our readers to try out our code.

image

StarkWare’s SHARP

As an L2, Starknet needs to post proofs of numerous transactions posted on its network to L1. Most of the transactions just invoke a function of a Cairo program, and proving that means proving the execution of the invoked Cairo program. This results in a pretty large proof (for reference, a simple fibonacci program proving that its 10th step is 144 is 166kb!) that needs to be uploaded to L1, which also scales linearly for each proof.

In order to reduce this overhead, StarkWare uses SHARP (Shared Prover) to aggregate multiple transactions (i.e. multiple executions of multiple Cairo programs) into a single proof. As the following diagram shows (from the documentation), SHARP refers to the entire backend stack that takes as input Cairo jobs (i.e. Cairo programs and corresponding function calls) creates a single proof of execution of all of them, and submits the proof to L1, where a SHARP verifier is deployed.

SHARP

Bootloader

Internally, SHARP uses a Cairo program called the bootloader to create a single aggregated proof (the code is public here, although you’ll find that it’s missing some python files necessary for processing hints when you try to run it).

The short version of how the bootloader program works is that it loads the bytecode of the Cairo programs that it’s proving in-memory and executes them. The difference between this and a normal execution of a Cairo program is that the bytecode of a Cairo program is normally included in the public part of the memory, but the bootloader program keeps them private. Instead, it computes the hash of the bytecode and makes it public, allowing anyone to verify it separately. This way, you can reduce the cost of proving Cairo program execution, as you can remove the constraints needed to make each program public.

Another interesting point is that the bootloader also supports recursive proving. In other words, you can provide as input not only Cairo programs, but also Cairo proofs. More specifically, the bootloader program can be seen as having an outer program and an inner program (named “simple bootloader”), whose execution can be verified in the outer program. This recursive functionality allows SHARP to incrementally create proofs of Cairo program executions instead of proving many at once, which means they can prove transactions as they are received, and they can prove them on relatively slower devices.

Adapting Cairo proofs for Ethereum

This single proof is not yet suitable for L1, however, because the size of the proof increases based on the number of programs being proved and can also fluctuate based on the types of programs being proved, potentially exceeding Ethereum’s gas price limit.

To solve this problem, the SHARP verifier on Ethereum splits the Cairo proof into multiple components (Merkle tree, FRI, Memory Page, Main) and uploads each proofs separately. This document and our own STARK book provide a good overview of how the verifier works.

Introducing stark-evm-adapter

And this is where our work enters!

stark-evm-adapter is a library for parsing a Cairo proof to be compatible with the SHARP verifier on Ethereum. We also included an example demo that showcases the e2e flow of creating a Cairo proof and verifying it on-chain given a Cairo program and an input.

Some key differentiators:

  • Unlike previous work that used the ministark prover to create a Cairo proof, our code uses the StarkWare’s Stone prover to create a Cairo proof.
  • Showcases StarkWare’s functionality of the bootloader program (compressing multiple proofs of multiple programs into one), which is essential for efficient proof verification.
  • Distribute a Rust library that 3rd dapp/services can easily adopt into their own code.

You can either integrate this library into your system or modify our example to prove your own Cairo programs.

What’s next?

The library can be used as of now, but we are still working on some details before officially releasing it. We are also planning to integrate this library into our definitive Stone CLI in the near future, so stay tuned for more updates!