Simplicity

Simplicity is a blockchain programming language designed as an alternative to Bitcoin script.

The language and implementation is still under development.

Contents

This project contains

• A Haskell implementation of Simplicity's language semantics, type inference engine, serialization functions, and some example Simplicity code.
• A Coq implementation of Simplicity's formal denotational and operational semantics.

Build

Building with Nix

Software artifacts can be built using Nix.

• To build the Haskell project, run nix-build -A haskell.
• To use the Haskell project, try nix-shell -p "(import ./default.nix {}).haskellPackages.ghcWithPackages (pkgs: [pkgs.Simplicity])".
• To build the Coq project, run nix-build -A coq.

Building without Nix

Building the Coq project

These instructions assume you start within the simplicity root directory of this repository.

Coq 8.12.0 is most easily installed via opam by following the instruction at https://coq.inria.fr/opam-using.html.

1. Install opam using your distribution's package manager.
2. opam init
3. eval $(opam env)
4. opam pin -j$(nproc) add coq 8.12.0
5. opam install -j$(nproc) coqide # optional step

Next we use opam to install the CompCert dependency

1. opam repo add coq-released https://coq.inria.fr/opam/released
2. opam install -j$(nproc) coq-compcert.3.7+8.12~coq_platform~open_source

While the VST dependency is available via opam, we need a custom build.

1. wget -O - https://github.com/PrincetonUniversity/VST/archive/v2.6.tar.gz | tar -xvzf -
2. cd VST-2.6
   1. make -j$(nproc) default_target sha
   2. make install
   3. install -d $(coqc -where)/user-contrib/sha
   4. install -m 0644 -t $(coqc -where)/user-contrib/sha sha/*.v sha/*.vo
   5. cd ..

Now we can build (and install) the Simplicity Coq library.

1. cd Coq
   1. coq_makefile -f _CoqProject -o CoqMakefile
   2. make -f CoqMakefile -j$(nproc)
   3. make -f CoqMakefile install # optional

Documentation

Detailed documentation can be found in the Simplicity-TR.tm TeXmacs file. A recent PDF version can be found in the pdf branch.

Further Resources

• Our paper that originally introduced Simplicity. Some of the finer details are out of date, but it is still a good introduction.
• BPASE 2018 presentation of the above paper (slides).
• Scale by the Bay 2018 presentation that illustrates formal verification of Simplicity in Agda (slides).

Contact

Interested parties are welcome to join the Simplicity mailing list. Issues and pull-requests can be made through GitHub's interface.