Formalization of Ethereum Virtual Machine in Lem

This repository contains

an EVM implementation in Lem lem/evm.lem
a Keccak-256 implementation in Lem lem/keccak.lem
a form of functional correctness defined in Lem lem/evmNonExec.lem
a relational semantics that captures the environment's nondeterministic behavior RelationalSem.thy
some example verified contracts in example
a parser that parses hex code and emits an Isabelle/HOL expression representing the program parser/hexparser.rb

When you see \<Rightarrow> in the source, try using the Isabelle2017 interface. There you see ⇒ instead.

Lem?

Lem is a language that can be translated into Coq, Isabelle/HOL, HOL4, OCaml, HTML and LaTeX.

Isabelle2017
lem
OCaml 4.02.3
opam 1.2.2
Some opam packages: use opam install ocamlfind batteries yojson bignum easy-format bisect_ppx ocamlbuild sha secp256k1
ECC-OCaml from mrsmkl
secp256k1
- On Ubuntu Artful, apt install secp256k1-0 secp256k1-dev is enough
- On older versions of Ubuntu, installation from the current master branch is necessary
- configure option --enable-module-recovery is needed

First translate the Lem definitions into Isabelle/HOL:

$ make lem-thy

Then, use Isabelle2017 to open ./examples/AlwaysFail.thy. The prerequisite Isabelle/HOL files are automatically opened.

Make sure the tests submodule is cloned

$ git submodule init tests
$ git submodule update tests

Extract the OCaml definitions

$ make lem-ocaml

And move to tester directory.

$ cd tester

One way is to run the VM Test.

$ sh compile.sh
$ ./runVmTest.native

(When ./runVmTest.native takes an argument, it executes only the test cases whose names contain the argument as a substring.)

Another way is to run the VM Test and measure the coverage.

$ sh measure_coverage.sh

Moreover, it's possible to run Blockchain Tests.

$ ./runBlockchainTest.native

make doc produces output/document.pdf as well as lem/*.pdf.
make lem-thy compiles the Lem sources into Isabelle/HOL
make lem-hol compiles the Lem sources into HOL4
make lem-coq; cd lem; make compiles the Lem sources into Coq (and then compiles the Coq sources)
make lem-pdf compiles some of the Lem sources into PDF through LaTeX
make all-isabelle checks all Isabelle/HOL sources (but not the ones compiled from Lem)
make does everything above
script/gen_coq.sh generates a distribution useful for Coq users