Skip to content
A Lem formalization of EVM and some Isabelle/HOL proofs
Branch: master
Clone or download
Pull request Compare This branch is 389 commits behind pirapira:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
Hoare
attic
document
example
lem
parser
script
sep_algebra
simple_wallet_document
tester
tests @ ed484d9
.gitignore
.gitmodules
.travis.yml
ContractSem.thy
EvmFacts.thy
GlobalTriple.thy
HISTORY
HashMap.thy
LICENSE
Makefile
NOTICE
Parse.thy
ProgramInAvl.thy
README.md
ROOT
RelationalSem.thy
StoreByteList.thy
TODO
circle.yml
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 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 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

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 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 the state tests:

for j in `ls ../../tests/StateTests/*.json`
do
./stateTestReturnStatus.native $j || break
done

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
  • script/gen_coq.sh generates a distribution useful for Coq users

Links

You can’t perform that action at this time.