This repository contains a formal model of the EVM and Yul in Lean 4. Where applicable, the underlying EVM primops are used directly by the Yul model.
Everything here is work in progress and is subject to change therefore.
Requirements
- Python packages: coincurve, typing-extensions, pycryptodome, eth-typing, py-ecc
Project structure
Primops
The Operation describing all of the primitive operations:
EvmYul/Operations.lean
The semantic function primCall associated with the ADT:
EvmYul/Yul/PrimOps.lean
EVM
The model of the EVM state EVM.State:
EvmYul/EVM/State.lean
The semantic function step:
EvmYul/EVM/Semantics.lean
Yul
The ADT Stmt mutually defined with Expr and FunctionDefinition describing Yul:
EvmYul/Yul/Ast.lean
The model of the Yul state YUL.State:
EvmYul/Yul/State.lean
The semantic function exec mutually defined with eval (and some misc. functions):
EvmYul/Yul/Interpreter.lean
Conformance testing
A git submodule with EVM conformance tests is in:
EthereumTests/
The test running infrastructure can be found in:
Conform/
To execute conformance tests, make sure the EthereumTests directory is the appropriate git submodule and run:
lake exec conform