A verified algebraic representation of Cairo program execution
Cryptography and Security
2021-12-16 v3 Logic in Computer Science
Programming Languages
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.
Keywords
Cite
@article{arxiv.2109.14534,
title = {A verified algebraic representation of Cairo program execution},
author = {Jeremy Avigad and Lior Goldberg and David Levit and Yoav Seginer and Alon Titelman},
journal= {arXiv preprint arXiv:2109.14534},
year = {2021}
}