doc build

docs/_build/html/.buildinfo

@@ -1,4 +1,4 @@
 # Sphinx build info version 1
 # This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
-config: a33cec51924f7f1b8a36f8df6c388707
+config: 5175dcb8d16d9296e3364f66757ea522
 tags: 645f666f9bcd5a90fca523b33c5a78b7

docs/_build/html/_sources/correctness.rst.txt

@@ -1,3 +1,5 @@
-*****
+.. _correctness:
+
+************
 Correctness
-*****
+************

docs/_build/html/_sources/implementation.rst.txt

@@ -0,0 +1,3 @@
+*****
+Implementation
+*****

docs/_build/html/_sources/index.rst.txt

@@ -11,14 +11,16 @@ Welcome to elle's documentation!
    :caption: Contents:
 
    overview
+   installation
    usage
    syntax
    semantics
+   implementation
    correctness
 
 Indices and tables
 ==================
 
-* :ref:`genindex`
-* :ref:`modindex`
-* :ref:`search`
+.. * :ref:`genindex`
+.. * :ref:`modindex`
+.. * :ref:`search`

docs/_build/html/_sources/installation.rst.txt

@@ -0,0 +1,197 @@
+*************
+Installation
+*************
+
+Elle's installation is quite straightforward if
+all you want to do is use the FourL frontend as described in
+:doc:`usage`, 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 <https://github.com/mmalvarez/eth-isabelle>`_
+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   
+
+.. _end-user-installation:
+
+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 example:
+
+::
+   
+   > cd eth-isabelle/elle/generated
+   # output snipped
+   > make
+   # output snipped
+   > ./llllc ../tests/if.lll
+   6001600a576003600d565b60025b
+
+Usage of ``llllc`` is described further in :doc:`usage`
+
+To help inspect the output of ``llllc``, you may find it useful to use the
+EVM bytecode parser contained in eth-isabelle:
+`eth-isabelle/parser/hexparser.rb <https://github.com/mmalvarez/eth-isabelle/blob/master/parser/hexparser.rb>`
+
+You'll need an installation of Ruby (tested with 2.5.1p57) to use this tool. It takes hex bytecodes like those
+output by ``llllc`` (or other compilers for Ethereum, such as Solidity LLL) on standard input and outputs
+(on standard output)
+a series of mnemonics describing the opcodes in the input.
+
+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 :doc:`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_.
+

docs/_build/html/_sources/overview.rst.txt

@@ -1,3 +1,43 @@
-*****
+.. _overview:
+
+*********
 Overview
-*****
+*********
+
+Elle is a compiler focused on generating code for the
+`Ethereum Virutal Machine (EVM) <https://jellopaper.org/evm/>`_.
+What sets is apart from other Ethereum compiler technologies is that
+it is *foundationally verified*: that is, it is implemented inside of
+`Isabelle <https://isabelle.in.tum.de/>`_, a *proof assistant* that enables programmers to state
+and prove *mathematical theorems* about their code. In the case of
+Elle, a theorem exists stating that the behavior of the code output by the
+Elle compiler matches the behavior of its input (see :doc:`correctness`).
+
+Assuming we trust the model
+of Elle's source language (an LLL/Yul/WASM-like structured programming
+layer on top of EVM) and the semantics of EVM (drawn from the `Eth-Isabelle <https://github.com/pirapira/eth-isabelle>`_ project,
+we can have complete confidence that Elle generates EVM programs that match the
+programmer's intent: that is, that behave the same way that input programs are supposed
+to behave.
+
+In the rest of this documentation, we'll cover
+:doc:`how to install Elle <installation>`, and then
+:doc:`how to use Elle's FourL frontend <usage>` as
+to compile smart contracts written in the LLL language into EVM
+bytecode. Next, we'll dive into the details of Elle's source-level representation,
+covering its :doc:`syntax <syntax>` and its :doc:`formal semantics <semantics>`. Next, we'll talk about
+:doc:`the internals of the implementation <implementation>` of the Elle compiler
+(along with the FourL frontend) as well
+as Elle's :doc:`correctness proof <correctness>`.
+
+Elle is intended to be supplanted by `Gazelle <https://github.com/mmalvarez/gazelle>`_, a
+generalized platform inspired by Elle for
+building verified compilers that allows for greater ease of adaptation
+than the Elle system.
+As such, Elle itself is unlikely to see significant changes at this point. Nonetheless, Elle as it exists is a useful
+system: it can be used to compile real-world LLL smart contracts; namely Dan Ellison's
+`Echo <https://media.consensys.net/deploying-your-first-lll-contract-part-2-910d9eff497e>`_ smart contract,
+Ben Edgington's `LLL-ERC20 <https://github.com/benjaminion/LLL_erc20/blob/master/erc20.lll>`_
+token contract,
+and the LLL implementation of the `ENS registry <https://github.com/ensdomains/ens/blob/master/contracts/ENS.lll>`_.
+For these examples, see the `tests <https://github.com/mmalvarez/eth-isabelle/tree/master/elle/tests>`_ directory.

docs/_build/html/_sources/usage.rst.txt

@@ -1,3 +1,3 @@
 *****
 Usage of the LLL Frontend
-****
+*****