A Lem formalization of EVM and some Isabelle/HOL proofs
Isabelle OCaml Standard ML TeX Coq Makefile Other
Clone or download
Latest commit d0bb02b Apr 16, 2018
Permalink
Failed to load latest commit information.
Hoare Gas price belongs to the transaction not the block Dec 15, 2017
HoareWithInvariant Add the induction hypothesis to triples Oct 23, 2017
Word_Lib Update proofs to Isabelle-2017 Oct 16, 2017
attic Update proofs to Isabelle-2017 Oct 16, 2017
document Fix typos Nov 1, 2016
example Add Vault.thy Dec 14, 2017
julia fixed permission problem Aug 11, 2017
lem Gas price belongs to the transaction not the block Dec 15, 2017
parser Remove invalid DUP representations Jan 13, 2017
script Add a script that generates a Coq destribution Apr 11, 2017
sep_algebra Progress on HoareTripleForInstruction.thy cleanup. Jul 5, 2017
simple_wallet_document Fix the build of simple wallet document Feb 14, 2017
tester Imppelent hash of transaction Apr 13, 2018
tests @ ed484d9 Add Circle CI setting Jun 29, 2017
.gitignore testing script for julia Aug 11, 2017
.gitmodules Add a submodule with https Jan 10, 2017
.travis.yml Remove opam upgrade to fix #481 Mar 29, 2018
ContractSem.thy Show termination of sha3_update Mar 29, 2018
EvmFacts.thy Merge branch 'master' into dispatcher_ex_mbegel Nov 21, 2017
GlobalTriple.thy Rename 'next' in block.lem into 'step' Oct 16, 2017
HISTORY Release note Mar 5, 2017
HashMap.thy functional extensionality lemma was renamed Mar 14, 2017
LICENSE Document HOL4 extraction Jan 11, 2017
Makefile Rename rlp.lem into rlplem.lem to avoid name collision with Rlp.ml ex… Dec 14, 2017
NOTICE Add CSIRO NOTICE as requested by Data61 legal. Mar 16, 2017
Parse.thy cleanup + fix parse_bytecode gen correct swap & dup insts. Oct 10, 2017
ProgramInAvl.thy Remove Annotation instruction because it produces and instruction of … Jan 11, 2017
README.md Add a dependency information in README Dec 19, 2017
ROOT Add the induction hypothesis to triples Oct 23, 2017
RelationalSem.thy Rename `no_annotation_failure` into `invariant_holds` because the ann… Jul 27, 2017
StoreByteList.thy started writing proof for balance preservation Apr 25, 2017
TODO Came up with some todos. May 3, 2016
circle.yml Try to add coqharness Dec 18, 2017
comment.sty Setup Isabelle/HOL document generation Oct 23, 2016
document_generation.sh Use the newer Isabelle version Dec 31, 2016
isabelle.sty Setup Isabelle/HOL document generation Oct 23, 2016
isabellesym.sty Setup Isabelle/HOL document generation Oct 23, 2016
isabelletags.sty Setup Isabelle/HOL document generation Oct 23, 2016
pdfsetup.sty Setup Isabelle/HOL document generation Oct 23, 2016
railsetup.sty Setup Isabelle/HOL document generation Oct 23, 2016
wallet_generation.sh Try verbose isabelle build to keep Travis from taking silence as failure Oct 13, 2017

README.md

Formalization of Ethereum Virtual Machine in Lem

Build Status CircleCI

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.

Prerequisites

  • 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

How to read the proofs

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.

How to run VM tests and state tests

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

Makefile goals

  • 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

Links