A Formalization of the Yul Language and Some Verified Yul Code Transformations
Alessandro Coglio (Kestrel Institute), Eric McCarthy (Kestrel Institute)
TL;DR
This paper formalizes the Yul language used in Ethereum smart contract compilation, providing a rigorous foundation and verified transformations to ensure correctness in compiler processes.
Contribution
It introduces a formal ACL2-based model of Yul's syntax and semantics, along with verified code transformations for improved compiler reliability.
Findings
Formal ACL2 model of Yul syntax and semantics
Verified correctness proofs for specific Yul transformations
Enhanced assurance of compiler transformation correctness
Abstract
Yul is an intermediate language used in the compilation of the Solidity programming language for Ethereum smart contracts. The compiler applies customizable sequences of transformations to Yul code. To help ensure the correctness of these transformations and their sequencing, we used the ACL2 theorem prover to develop a formalization of the syntax and semantics of Yul, proofs relating static and dynamic semantics, a formalization of some Yul code transformations, and correctness proofs for these transformations.
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.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.