License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2023.7
URN: urn:nbn:de:0030-drops-183820
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18382/
Avigad, Jeremy ;
Goldberg, Lior ;
Levit, David ;
Seginer, Yoav ;
Titelman, Alon
A Proof-Producing Compiler for Blockchain Applications
Abstract
Cairo is a programming language for running decentralized applications (dapps) at scale. Programs written in the Cairo language are compiled to machine code for the Cairo CPU architecture, and cryptographic protocols are used to verify the results of the execution traces efficiently on blockchain. We explain how we have extended the Cairo 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 computations with an elliptic curve over a large finite field, as well as their use in the validation of cryptographic signatures.
BibTeX - Entry
@InProceedings{avigad_et_al:LIPIcs.ITP.2023.7,
author = {Avigad, Jeremy and Goldberg, Lior and Levit, David and Seginer, Yoav and Titelman, Alon},
title = {{A Proof-Producing Compiler for Blockchain Applications}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {7:1--7:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18382},
URN = {urn:nbn:de:0030-drops-183820},
doi = {10.4230/LIPIcs.ITP.2023.7},
annote = {Keywords: formal verification, smart contracts, interactive proof systems}
}
