This is a study note of Cairo Resource Guide. The guide covers the background, coding, SHARP and end-to-end system with Cairo.
1 Hello Cairo
This is from the blog Hello, Cairo. Cairo is a Turing-complete programming language for generating STARK proofs for general computation.
The idea is to provide an off-chain Prover that processes large computations (like large batches of transactions), and produces exponentially smaller validity proofs, which are in turn verified on-chain.
Cairo stands for CPU Algebraic Intermediate Representation (AIR). It includes a single AIR that verifies the instruction set of this CPU. It builds zero knowledge proofs for general computation. A single AIR means a single Verifier in a smart contract written in Solidity. Each Cairo program
P resides in the virtual machine’s memory to process data
D. The Cairo AIR verifies the computational integrity of executing
D, and the correctness of the post-execution state of the system.
With Cairo, new business logic doesn’t require a new smart contract, it only requires a different Cairo program. Consequently, the business logic and the proof system are demarcated. A single AIR means that a single proof to assert the integrity of a bunch of different program execution.
Cairo’s AIR is relatively simple, which leads to efficiency and low amortized costs for both the on-chain Verifier and the off-chain proving service. One only needs to audit the business logic written in Cairo code.
2 Cairo and Blockchain
Cairo is a language for writing provable programs: running a Cairo program implementing some business logic produces a trace that can then be sent to a trustless prover, which generates a STARK proof for the validity of the statement or computation represented by the Cairo program. The proof can then be verified using a verifier (which may or may not be on-chain). The verifying of the proof is exponentially cheaper than executing the bussiness logic. The combination of off-chain proof of complex business logic and on-chain quick verification provides a scalable solution to dApps.
Currently Cairo is stateless that each Cairo run is independent of an external state and of other Cairo runs. The Cairo pattern of keeping a state is to compress state as a Merkle root – a single Ethereum word that has a size of 32 bytes. A state change will trigger an on-chain dApp to update state with the new root as an input.
The SHARP has three components: an off-chain prover, an on-chain verifier smart contract, and an on-chain fact registry contract. The prover takes a Cairo program’s execution trace, proves its validity, and sends the proof to the verifier. The verifier verifis the proof and writes a fact attesting the proof validity to the Fact Registry. Other smart contract can use the facts in Fact Registry for their processing.
The SHARP collects traces of several, possibly unrelated, programs that run successfully and creates a STARK proof. each batch of programs is called a train that to be dispatched to the prover when the batch is large enough or the time is due.
The Shapr sends a proof for a batch of programs to on-chain verifier. The verifier write a fact in the Fact Registry fro each program in the train.
The fact is a 32-byte hash value that is a Keccak function of two components: a Pedersen hash of the compiled program and a Keccak hash of the program otuput (a list of field elements).
The computation, transmission and storage on Ethereum are very expensive. The SHARP significantly saves all three.