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.

翻译：本文为Yul——Solidity编译器用于生成EVM字节码的中间语言——提出了大步与小步操作语义。我们采用与编程语言文献相一致的数学符号进行形式化描述，这种表示方式既适用于语言证明，也可作为该语言精确且广泛可访问的规范。我们提出的两种语义在忠实于语言原始非形式化规范的同时，澄清了诸如空函数调用等未明确规定的语义场景。通过形式化表述，我们证明了两类语义的等价性。此外，我们基于小步语义实现了Yul解释器，其中采用了可证明正确的优化技术。该解释器已通过Solidity编译器测试集及自主设计的测试用例进行验证。我们预期此项工作将推动直接在Yul层面开发验证与符号执行技术，从而丰富以太坊安全生态体系，同时为未来可证明健全的类型系统构建提供支持。