Installation¶
Contents
Elle’s installation is quite straightforward if all you want to do is use the FourL frontend as described in Usage of the LLL Frontend, and somewhat more involved if you want to be able to generate, build, check, or modify the implementation and proofs of Elle.
Getting Elle¶
In the rest of this file, let >
stand for a bash-compatible shell
prompt (that is, lines starting with >
are to be understood as input)
Clone Elle from the Github repo as follows:
> git clone https://github.com/mmalvarez/eth-isabelle
Later in this file, we assume that Elle is checked out into
a directory called eth-isabelle
. (This repository has this name because
it is a fork of Yoichi Hirai’s eth-isabelle <https://github.com/pirapira/eth-isabelle>
project specifying EVM in the Isabelle proof assistant.)
Since Elle is no longer under active development, the master
branch should
be stable enough to build reliably. For a version of Elle that is more guaranteed
to build successfully, try the ITP2019
branch, which contains an artifact
submission for the 2019 edition of the Interactive Theorem Proving conference:
> cd eth-isabelle
> git checkout ITP2019
Installation as an End-User of Elle¶
The following dependencies are required to build llllc
, the
FourL command-line interface to the FourL compiler frontend that makes
use of Elle’s verified compiler.
- Ocaml (tested with v4.05.0)
- OcamlBuild
- OCaml Zarith
On an Ubuntu-like system, these can be installed as follows:
> apt-get install ocaml ocamlbuild libzarith-ocaml libzarith-ocaml-dev
Once these dependencies are installed, navigate to eth-isabelle/elle/generated
and run make
. This should succeed and generate a file called llllc
.
When run on an lll file, it will print (to standard output) a hexadecimal
representation of the bytecode produced by the compiler for that smart contract
(similar to Solidity LLL’s command-line tool, but with fewer options and error
messages). Files to run llllc
on can be found in the eth-isabelle/elle/tests
directory.
For more details on using llllc
, see Basic Usage.
Installation for Modifying and Examining Elle¶
The Elle git repository includes the file eth-isabelle/elle/generated/FourL.ml <https://github.com/mmalvarez/eth-isabelle/blob/master/elle/generated/FourL.ml>. This file is generated from the formal Isabelle model contained in the rest of the Elle repository, and is all that is needed to build a working executable version of Elle/FourL as described in end-user-installation.
In order to work with the formal model directly, Isabelle itself is needed as a dependency. Elle requires Isabelle 2018, which can be downloaded here<https://isabelle.in.tum.de/website-Isabelle2018/index.html> (binaries for Linux, MacOS, and Windows are provided).
Once Isabelle is installed, the user will need to set up Lem, a framework used to generate the some of the Isabelle specifications used by Elle. In order to do this, first run the following, to update the Lem submodule contained in Elle’s git repository:
> cd eth-isabelle
> git submodule init
# output snipped
> git submodule update lem-installation
# output snipped
we have tested with the version of Lem having the Git hash of 0927743c1bd31d7bba20a54260ba4c4dd3ce49e9
.
Newer versions should also work. Older versions may not support generating code compatible with Isabelle2018.
In order to build Lem, run the following:
> cd lem-installation
> make
# output snipped
If this succeeds, it will generate an executable called lem
. Add it to your path, and ensure the
it will look for its libraries in the correct place, by running the following:
> `export PATH=$PWD/lem-installation/bin:$PATH`
> `export LEMLIB=$PWD/lem-installation/library`
Finally, navigate back to the root of the repository (eth-isabelle
), and run the following to
build the .thy
files that Elle depends on of from their Lem sources:
> make lem-thy
Examining Elle Sources¶
Isabelle allows .thy
files representing formal models and
proofs to be grouped together into sessions. Sessions make it easier
to automate the process of compiling Isabelle developments, as well
as allowing for caching the results of compilation and proof-checking
so that work does not need to be repeated each time Isabelle is
re-opened. Elle contains a session called ElleCorrect
, which
packs together all the files containing Elle’s correctness proofs into
a single session file.
However, in order to be able to
step through the proofs contained in the ElleCorrect
session,
it’s better not to run the ElleCorrect
session, since. Therefore,
to examine Elle’s proofs,
run Isabelle-Jedit, with the HOL
session
isabelle jedit -d ./lem -l HOL
For some proofs (particularly the more complex ones in elle/ElleCorrect
)
you will need to increase the editor’s limit on the number of allowed tracing
messages (or else the proofs will pause and appear to get stuck). To do this,
navigate through the Isabelle/JEdit menus as follows
Plugins > Plugin Options > Isabelle > General > Editor Tracing Messages
Increase this value to 30000.
The most interesting proofs are in eth-isabelle/elle/ElleCorrect
. The final
correctness theorems for the compiler are elle_alt_correct*
in eth-isabelle/elle/ElleCorrect/ElleAltSemantics.thy
For more details on the structure of Elle, see Implementation.
Recreating FourL.ml¶
The command-line binary version of the Elle-based FourL compiler depends on
FourL.ml
, an Ocaml file that is produced from a formal Isabelle model
via Isabelle’s built-in extraction mechanism. As such, FourL.ml can be regenerated
from Elle’s sources, provided Isabelle is installed. This can be done as follows:
> isabelle jedit -d ./lem -d ./elle -l ElleCorrect
This will open the ElleCorrect
session (building this session for the first time
can take some time - as much as a couple of hours on a 16Gb machine). Once this session
is done being processed, open the file eth-isabelle/elle/ElleCorrect/FourLExtract.thy
.
If that file is processed to the end (which can be forced by moving the cursor to the end of the file)
it will create a new version of eth-isabelle/elle/generated/FourL.ml
, which can then be built as
described in end-user-installation.