A Proof-Producing Compiler for Blockchain Applications
Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman
cs.CR
Jan 25, 2025 · v1
TL;DR
Extends the CairoZero compiler so users can prove in the Lean 3 proof assistant that compiled code meets functional specifications.
Abstract
CairoZero is a programming language for running decentralized applications (dApps) at scale. Programs written in the CairoZero language are compiled to machine code for the Cairo CPU architecture and cryptographic protocols are used to verify the results of execution efficiently on blockchain. We explain how we have extended the CairoZero compiler with tooling that enables users to prove, in the Lean 3 proof assistant, that compiled code satisfies high-level functional specifications. We demonstrate the success of our approach by verifying primitives for computation with the secp256k1 and secp256r1 curves over a large finite field as well as the validation of cryptographic signatures using the former. We also verify a mechanism for simulating a read-write dictionary data structure in a read-only setting. Finally, we reflect on our methodology and discuss some of the benefits of our approach.
Problem
Decentralized applications on blockchain execute autonomously with financial consequences, yet there is no systematic way to prove that compiled CairoZero code satisfies high-level functional specifications. The gap between source-level intent and machine-code behavior leaves critical smart contract primitives unverified.
Approach
The authors extend the CairoZero compiler with tooling that generates Lean 3 proof obligations from compiled code, enabling users to prove that machine code satisfies high-level specifications. The methodology involves formalizing the Cairo machine model (with its three-register CPU and read-only memory), translating assembly to machine code with verified semantics, and bridging CairoZero source to assembly. Lean 3 is used for all verification.
Results
The approach successfully verifies primitives for computation with the secp256k1 and secp256r1 elliptic curves over a large finite field, validation of ECDSA cryptographic signatures, and a mechanism for simulating read-write dictionary data structures in a read-only memory setting.
