This repository contains an experimental, work-in-progress definition of the Ethereum Virtual Machine (EVM) for the Rocq Prover using the Mathematical Components (MathComp) library. The focus is on ease-of-reasoning inside Rocq (e.g., for refinement) rather than efficient executability of definitions.
- Rocq Prover, version 9.0.1
- Rocq Stdlib, version 9.0.0
- Mathematical Components, version 2.4.0
- CoqWord, version 3.2
- Coq Record Update, version 0.3.6
We recommend installing dependencies via opam.
To build manually when all dependencies are installed, do:
git clone https://github.com/palmskog/mcevm.git
cd mcevm
make # or make -j <number-of-cores-on-your-machine> The MathComp EVM definition builds on a library dubbed mcmword for machine words defined using the CoqWord library, adapted from the formalization of the Jasmin language and compiler.
The library is licensed under the MIT license.
A legacy EVM definition in Rocq dubbed lemevm that serves as a comparison point for the MathComp EVM. Adapted from https://github.com/aa755/EVMOpSemCoq - originally generated from Lem sources at https://github.com/pirapira/eth-isabelle
The library is licensed under the Apache-2.0 license.
This library contains the experimental Rocq EVM definition, dubbed mcevm.
The library is licensed under the Apache-2.0 license.