A verified algebraic representation of Cairo program execution
Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon, Titelman
TL;DR
This paper verifies the correctness of an algebraic encoding of Cairo program execution traces within the STARK proof system using the Lean 3 proof assistant, enhancing trust in cryptographic blockchain proofs.
Contribution
It provides a formal verification of Cairo's algebraic execution trace encoding, improving reliability in cryptographic proof systems.
Findings
Verified the correctness of Cairo's algebraic encoding
Formal proof using Lean 3
Supports secure blockchain verification
Abstract
Cryptographic interactive proof systems provide an efficient and scalable means of verifying the results of computation on blockchain. A prover constructs a proof, off-chain, that the execution of a program on a given input terminates with a certain result. The prover then publishes a certificate that can be verified efficiently and reliably modulo commonly accepted cryptographic assumptions. The method relies on an algebraic encoding of execution traces of programs. Here we report on a verification of the correctness of such an encoding of the Cairo model of computation with respect to the STARK interactive proof system, using the Lean 3 proof assistant.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsCryptography and Data Security · Cryptographic Implementations and Security · Security and Verification in Computing