-------------------------------------------------------------------------------
-THE MODEL---------------------------------------------------------------------
-------------------------------------------------------------------------------
The pure Isabelle code is contained within the Model subdirectory.

Model/Wasm.thy contains the base definitions of reduction and typing.
Model/Wasm_Soundness.thy contains the type soundness result.
Model/Wasm_interpreter.thy contains the main definition of the interpreter.
Model/Wasm_Checker.thy contains the main definition of the typechecker.
Model/*_printing.thy files contain definitions relevant to code extraction.
Model/*_properties*.thy files contain auxiliary lemmas.

-Important definitions---------------------------------------------------------
b_e_typing - in Wasm.thy, line 492
The typing relation for core WebAssembly operations.

reduce - in Wasm.thy, line 857
The reduction relation for WebAssembly operations.

run_step - in Wasm_Interpreter.thy, line 129
Single step executable reduction function.

run_v - in Wasm_Interpreter.thy, line 533
Our interpreter wrapper for run_step.

b_e_type_checker - in Wasm_Checker.thy, line 59
Type checker for WebAssembly stacks.
-------------------------------------------------------------------------------

-Theorems----------------------------------------------------------------------
{preservation, progress} - in Wasm_Soundness.thy, line {6, 22}
Soundness of the type system with respect to the reduction relation.

run_step_sound - in Wasm_Interpreter_Properties.thy, line 2122
Soundness of the intepreter's one step function with respect to the reduction
relation.

b_e_typing_equiv_b_e_type_checker - in Wasm_Checker.thy, line 1831
Soundness and completeness of the type checker with respect to the typing
relation.
-------------------------------------------------------------------------------

To run the soundness proof, (assuming the isabelle tool is in the path)
run the following command in the Model directory:
isabelle process -T Wasm_Soundness

The proof should take less than three minutes to complete.
It has been tested on the Isabelle2016-1 release. Due to time constraints, it
has not been possible to adequately test the extremely recent Isabelle2017
release.

-------------------------------------------------------------------------------
-THE EXECUTABLE INTERPRETER----------------------------------------------------
-------------------------------------------------------------------------------
The OCaml code relevant to the executable interpreter is contained within the
Executable subdirectory.

The Reference_Interpreter subdirectory contains a (cannibalised) copy of the
WebAssembly working group's interpreter.
The Verified_Interpreter subdirectory contains our own code. The extracted
code of the model can be found at the top level, while the interface
subdirectory contains the "glue" code required to interface with the
reference interpreter.

Running `make` in the Executable directory will build the executable
interpreter. The build process requires ocamlbuild, and depends on the Bigarray
and Num OCaml libraries.
Tested on ocamlbuild 4.02.3.

For convenience, the code produced by our Isabelle definitions has been
pre-extracted. If you wish to build these from scratch, run `make extracted`
from the Executable folder to run the proofs and extraction from scratch and
move the results into the correct places. This can take a long time
(~5 minutes) and requires bash and isabelle in the path. For convenience, we
split the extracted modules into separate files to avoid circular compilation
issues in OCaml.

To run all core semantics tests, execute the following command after making the
interpreter.
./wasm_interpreter -i Reference_Interpreter/test/core/*.wast

Some of these tests involve printing values to the console, but there should be
no error messages.
