A Proof-Producing Compiler for Blockchain Applications
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866917902588837888 |
|---|---|
| author | Avigad, Jeremy Goldberg, Lior Levit, David Seginer, Yoav Titelman, Alon |
| author_facet | Avigad, Jeremy Goldberg, Lior Levit, David Seginer, Yoav Titelman, Alon |
| contents | CairoZero is a programming language for running decentralized applications (dApps) at scale. Programs written in the CairoZero language are compiled to machine code for the Cairo CPU architecture and cryptographic protocols are used to verify the results of execution efficiently on blockchain. We explain how we have extended the CairoZero 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 computation with the secp256k1 and secp256r1 curves over a large finite field as well as the validation of cryptographic signatures using the former. We also verify a mechanism for simulating a read-write dictionary data structure in a read-only setting. Finally, we reflect on our methodology and discuss some of the benefits of our approach. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_15002 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Proof-Producing Compiler for Blockchain Applications Avigad, Jeremy Goldberg, Lior Levit, David Seginer, Yoav Titelman, Alon Cryptography and Security Logic in Computer Science Programming Languages CairoZero is a programming language for running decentralized applications (dApps) at scale. Programs written in the CairoZero language are compiled to machine code for the Cairo CPU architecture and cryptographic protocols are used to verify the results of execution efficiently on blockchain. We explain how we have extended the CairoZero 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 computation with the secp256k1 and secp256r1 curves over a large finite field as well as the validation of cryptographic signatures using the former. We also verify a mechanism for simulating a read-write dictionary data structure in a read-only setting. Finally, we reflect on our methodology and discuss some of the benefits of our approach. |
| title | A Proof-Producing Compiler for Blockchain Applications |
| topic | Cryptography and Security Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2501.15002 |