eth-isabelle

by pirapira

pirapira / eth-isabelle

A Lem formalization of EVM and some Isabelle/HOL proofs

210 Stars 34 Forks Last release: Not found Other 1.5K Commits 2 Releases

Available items

No Items, yet!

The developer of this repository has not created any items for sale yet. Need a bug fixed? Help with integration? A different license? Create a request here:

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

\
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

We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.