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.
• For a Simplicity-Haskell development environment, type nix-shell --arg coq false.
• Typing nix-shell will provide a full C, Coq and Haskell development environment.

Building the C project manually

Install the GNU Compiler Collection and GNU Make. Binary packages are available for Debian (apt install gcc make) and other Linux distributions.

1. Open a command line.
2. Change directory to the C directory of this repository.
3. To run tests: make check
4. To install globally: make install
5. To install locally: make install out=/path/to/dir
6. To remove generated files: make clean

Building the Coq project manually

Requires Coq 8.15.0, CompCert 3.11 and VST 2.11. Packages in the Coq ecosystem are managed by the opam package manager.

Installing Coq

1. Install opam using your distribution's package manager.
2. opam init
3. eval $(opam env)
4. opam pin -j$(nproc) add coq 8.15.0

Optional: Installing CoqIDE

CoqIDE is a user-friendly GUI for writing proofs in Coq.

1. opam install -j$(nproc) coqide

Installing CompCert

1. opam repo add coq-released https://coq.inria.fr/opam/released
2. opam install -j$(nproc) coq-compcert

Installing VST

We need a custom build and cannot use opam for this step.

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

Building the Simplicity Coq library

1. Change into the Coq directory of this repository
2. coq_makefile -f _CoqProject -o CoqMakefile
3. make -f CoqMakefile -j$(nproc)

Optional: Installing the library

1. make -f CoqMakefile install

Building the Haskell project manually

Install the Glasgow Haskell Compiler and Cabal. Binary packages are available for Debian (apt install ghc cabal-install) and other Linux distributions.

1. Open a command line.
2. Change directory to the root directory of this repository.
3. cabal repl Simplicity
4. Cabal will build the project and open a GHCi prompt.

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.