This repository contains an implementation of a semantics for the Yul laguage using the Isabelle/HOL proof assistant. It is compatible with Isabelle2021.
Design goals are to create a maintainable formal semantics of Yul - including a reference interpreter - suitable for use in verifying Solidity compiler transformations.
The Yul language is designed to be integrated with a machine language, such that Yul captures control-flow and variable-assignment, and the machine language's primitives capture the remaining functionality. Such a combination is called a Yul Dialect. In this repository we focus on the Yul/EVM Dialect.
The repository is organized as follows:
Yul
: Implementation of Yul syntax and control-flow semantics
YulSyntax
: Yul semantics AST data structure
YulSemanticsSingleStep
: executable reference interpreter for Yul
YulDialect
: Useful primitives for defining dialects of Yul
YulSemantics
: inductive semantics for Yul; currently incomplete
Word_Lib
: A copy of the "Word_Lib" entry from the Isabelle Archive of Formal Proofs
(as of Isabelle2021, several useful operations on Isabelle machine words have been
moved out of the standard library and into this entry)
EVM
: an implementation of a substantial subset of the EVM virtual machine
for use in defining the Yul/EVM dialect.
Based on LLL tests from Solidity.
MiniEvm
: An implementation of a large subset of EVM operations. Currently does not model gas accounting or cross-contract calls. Used in the EVM dialect.
LowLevelEvm
: An implementation of a datatype for EVM bytecodes, currently incomplete
GlobalEvm
: An attempt at modeling global Ethereum state and cross-contract behaviors, currently incomplete
EvmTests
: Tests for the EVM implementation contained in EVM
Keccak
: Isabelle implementation of Keccak256, drawn from eth-isabelle
Dialects
: Instantiations of Yul to different dialects; most importantly, EVM
EvmDialect
: the Yul/EVM dialectYulTests
: Tests for the Yul interpreter, including the EVM dialect