Skip to content
master
Switch branches/tags
Go to file
Code

Latest commit

Add missing combinators to Coq library.
Fold use of these combinators into the Simplicity programs.
90b2606

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
C
Oct 8, 2020
Nov 16, 2018

README.md

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

Contact

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

About

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

Resources

License

Releases

No releases published

Packages

No packages published