Need help with eth-isabelle?
Click the “chat” button below for chat support from the developer who created it, or find similar developers for support.

About the developer

pirapira
217 Stars 39 Forks Other 1.5K Commits 146 Opened issues

Description

A Lem formalization of EVM and some Isabelle/HOL proofs

Services available

!
?

Need anything else?

Contributors list

# 59,249
OCaml
TeX
Shell
bamboo
942 commits
# 240,350
OCaml
TeX
Shell
dapp
196 commits
# 499,721
OCaml
Shell
C
82 commits
# 732,847
OCaml
TeX
Shell
76 commits

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.