EVM in Why3 from a state transition perspective

This package requires why3 to verify the correctness of the EVM specification and ocamlfind to build the automatically extracted EVM implementation. It is strongly suggested to use opam to install the dependencies.

For example, under Debian-based linux distributions, you can use

$ sudo apt-get install opam
$ opam init

to install opam and initialize it.

For the users who have already installed and properly configured opam, use

$ opam install why3 ocamlfind yojson

to install the Why3 Automated Theorem Prover.

Now typing make server will extract the OCaml implemention, compile it and the compiled target runs as a RPC server (for now not implemented yet).

First make sure that this repository is cloned and the executable server is properly built by

$ cd <EVM-Why3>
$ make server

clone the modified version of cita-vm at Cita-VM. And running

$ cd <Cita-VM>
$ git submodule init && git submodule update
$ export WHY3EVM=<EVM-Why3>
$ cargo build
$ cargo test

will show the test result.