An Operational Semantics for Yul

TL;DR

This paper develops formal big-step and small-step operational semantics for Yul, the intermediate language of Solidity, providing a precise specification that supports verification, optimization, and future type system development.

Contribution

It introduces the first formal semantics for Yul, proves their equivalence, and implements a verified interpreter to enhance security and verification tools.

Findings

Semantics faithfully represent Yul's informal specification

Proved equivalence of big-step and small-step semantics

Implemented a verified interpreter for Yul

Abstract

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.