A Lem formalization of EVM and some Isabelle/HOL proofs
Isabelle OCaml Standard ML TeX Coq Makefile Other
Clone or download
Pull request Compare This branch is 658 commits behind pirapira:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
attic
document
example
lem
parser
simple_wallet_document
tester
tests @ ed484d9
.gitignore
.gitmodules
.travis.yml
ContractSem.thy
HISTORY
Hoare.thy
HoareTripleForInstructions.thy
HoareTripleForInstructions2.thy
LICENSE
Makefile
ProgramInAvl.thy
README.md
ROOT
RelationalSem.thy
TODO
comment.sty
document_generation.sh
isabelle.sty
isabellesym.sty
isabelletags.sty
pdfsetup.sty
railsetup.sty
wallet_generation.sh

README.md

Formalization of Ethereum Virtual Machine in Lem

Build Status

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 Isabelle2016-1 interface. There you see instead.

Lem?

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

Prerequisites

  • Isabelle2016-1
  • lem
  • OCaml 4.02.3
  • opam 1.2.2
  • Some opam packages: use opam install ocamlfind batteries yojson bignum easy-format bisect_ppx ocamlbuild

How to read the proofs

First translate the Lem definitions into Isabelle/HOL:

$ make lem-thy

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

How to run VM 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

Makefile goals

  • make deed produces a verified PDF document for the Deed contract in output/document.pdf. Make sure that isabelle points to Isabelle2016-1/bin/isabelle (not earlier versions).
  • 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

Links