A verified algebraic representation of Cairo program execution
summary
Formal proof that the algebraic encoding used to generate real STARK certificates implies an actual Cairo execution: the project formalizes the Cairo machine model, exports the exact polynomials used by StarkWare, and proves in Lean 3 that whenever the published table and random challenges (outside three small bad sets) satisfy the STARK polynomial constraints, then there exists a full memory assignment and a valid step‑by‑step execution trace. The formalization is complete and runnable online.
AI-written summary · about
chapters (19)
- 0:00Introduction
- 3:38Cryptographic proof protocols
- 6:00The verification project
- 7:03Stark protocol
- 8:10Algebraic intermediate representation
- 9:22Machine model
- 10:18Whitepaper specification
- 11:02Instructions
- 11:40Constraints
- 13:45Code
- 14:57Global constraints
- 16:19Solution
- 16:54Main Theorem
- 17:40Formal Theorem
- 17:59Public Data
- 18:13Execution Sequence
- 18:33Related work
- 19:13Blockchain and smart contracts
- 21:13Rollups
related talks
18mAirScript: Arithmetization for zk-STARKs
01h 35mSTARK – Zero-Knowledge Proof Protocol
14mStatic Analysis for Zero-Knowledge Programming Languages
44mTooling for building zkEVM: PIL and Circom
20mFoundational Integration Verification of a Cryptographic Server
16mDecentralized and Permissionless ZK-Rollups
01h 08mTutorial on Proof Systems
23mThe Last Yard: Foundational End-to-End Verification of High-Speed Cryptography