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 C implementation of a minimal, consensus-critical Simplicity runtime for full nodes.
• A Haskell implementation of Simplicity's language semantics, type inference engine, serialization functions, and some example Simplicity code.
• A Haskell code generator that exports Simplicity constants to C and Rust.
• A Coq implementation of Simplicity's formal denotational and operational semantics.

Build

Use Nix for the easiest build. Alternatively, use GNU Autotools.

C project

Nix

Change into the root directory of this repository.

Build the nix package.

nix-build -A c

Enter a nix shell to develop the project manually (see below).

nix-shell --arg coq false --arg haskell false

Use arguments to enable / disable the other projects.

Manual

Change into the C directory of this repository.

Build the project using make.

make -j$(nproc)

To install the project, run make.

make install # use "out=/path/to/dir" for local install

To run the tests, run make.

make check

Haskell project

Nix

Change into the root directory of this repository.

Build the nix package.

nix-build -A haskell

Enter a nix shell to develop the project manually (see below).

nix-shell --arg c false --arg coq false

Use arguments to enable / disable the other projects.

Manual

Install the Glasgow Haskell Compiler and Cabal.

Change into the root directory of this repository.

Build the project using cabal.

cabal build

To run tests, run cabal.

cabal test # use --test-options="+RTS -N -RTS" for parallel jobs

To enter an interactive GHCi prompt with the project loaded, run cabal.

cabal repl Simplicity

Coq project

Nix

Change into the root directory of this repository.

Build the nix package.

nix-build -A coq

Enter a nix shell to develop the project manually (see below).

The shell provides Coq, CompCert and VST.

nix-shell --arg c false --arg haskell false

Use arguments to enable / disable the other projects.

Manual

Install the opam package manager.

Enter the opam environment in your shell.

opam init
eval $(opam env)

Install the Coq theorem prover.

opam pin -j$(nproc) add coq 8.17.1

Install the CompCert certified C compiler.

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

Install a custom version of the Verified Software Toolchain.

You cannot use opam for this step!

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

Enter the Coq directory of this repository.

Build the project using make.

coq_makefile -f _CoqProject -o CoqMakefile
make -f CoqMakefile -j$(nproc)

To install the project, run make.

make -f CoqMakefile install

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.
• Scale by the Bay 2018 presentation that illustrates formal verification of Simplicity in Agda (slides).
• Our library rust-simplicity that implements Simplicity in Rust.

Contact

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