This folder contains a Lean formalization of the semantics of Cairo.
-
The file instructions.lean defines the Cairo machine code.
-
The file cpu.lean defines the CPU execution semantics.
-
The file assembly.lean models Cairo's assembly language and a translation to machine code.
-
The folder air_encoding contains a formal proof of the correctness of an algebraic encoding of this execution model that is used by STARK proofs. This is described in the paper A verified algebraic representation of Cairo program execution.
-
The folder soundness contains a Lean representation of Cairo's assembly language, Hoare semantics, and tactics that step through the effects of executing each instruction. These are all used by the Lean Cairo verifier.
-
The file util.lean contains generally useful definitions and theorems, some of which should eventually be moved to Lean's
mathlib.
The Lean files in this folder are released under an Apache license.