An Operational Semantics for Yul
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866910509408714752 |
|---|---|
| author | Koutavas, Vasileios Lin, Yu-Yang Tzevelekos, Nikos |
| author_facet | Koutavas, Vasileios Lin, Yu-Yang Tzevelekos, Nikos |
| contents | We present a big-step and small-step operational semantics for Yul -- the intermediate language used by the Solidity compiler to produce EVM bytecode -- in a mathematical notation that is congruous with the literature of programming languages, lends itself to language proofs, and can serve as a precise, widely accessible specification for the language. Our two semantics stay faithful to the original, informal specification of the language but also clarify under-specified cases such as void function calls. Our presentation allows us to prove the equivalence between the two semantics. We also implement the small-step semantics in an interpreter for Yul which avails of optimisations that are provably correct. We have tested the interpreter using tests from the Solidity compiler and our own. We envisage that this work will enable the development of verification and symbolic execution technology directly in Yul, contributing to the Ethereum security ecosystem, as well as aid the development of a provably sound future type system. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_01365 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | An Operational Semantics for Yul Koutavas, Vasileios Lin, Yu-Yang Tzevelekos, Nikos Programming Languages We present a big-step and small-step operational semantics for Yul -- the intermediate language used by the Solidity compiler to produce EVM bytecode -- in a mathematical notation that is congruous with the literature of programming languages, lends itself to language proofs, and can serve as a precise, widely accessible specification for the language. Our two semantics stay faithful to the original, informal specification of the language but also clarify under-specified cases such as void function calls. Our presentation allows us to prove the equivalence between the two semantics. We also implement the small-step semantics in an interpreter for Yul which avails of optimisations that are provably correct. We have tested the interpreter using tests from the Solidity compiler and our own. We envisage that this work will enable the development of verification and symbolic execution technology directly in Yul, contributing to the Ethereum security ecosystem, as well as aid the development of a provably sound future type system. |
| title | An Operational Semantics for Yul |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2407.01365 |