This repository contains the formal specifications, executable models, and implementations of the Cardano Ledger.
The documents are built in our CI and can be readily accessed using the following links:
| Era | Design Documents | Formal Specification | CDDL |
|---|---|---|---|
| Byron | Chain Spec, Ledger Spec | CDDL | |
| Shelley | Design | Spec | CDDL |
| Allegra & Mary | Multi-Currency, UTXOma | Spec | CDDL |
| Alonzo | eUTXO | Spec | CDDL |
| Babbage | batch-verification, CIP-31, CIP-32, CIP-33 | Spec | CDDL |
Other Documents:
- Non-integer calculations specification: details on the parts of the Shelley specification that use real numbers.
- Stake pool ranking specification: details for a robust stake pool ranking mechanism.
- Explanation of the small-step-semantics framework: a guide to the notation and style used by our ledger rules.
In addition, there is a formalization of the Ledger Specification in Isabelle/HOL which can be found here.
The directory structure of this repository is as follows:
It is recommended to use nix for building everything in this repository.
Haskell files can be built with cabal inside of a nix shell.
When using nix it is recommended that you setup the cache, so that it can
reuse built artifacts, reducing the compilation times dramatically:
If you are using NixOS add the snippet below to your
/etc/nixos/configuration.nix:
nix.binaryCaches = [
"https://cache.nixos.org"
"https://hydra.iohk.io"
];
nix.binaryCachePublicKeys = [
"hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ="
];
If you are using the nix package manager next to another operating system put
the following in /etc/nix/nix.conf if you have a system-wide nix
installation , or in ~/.config/nix/nix.conf if you have a local installation:
substituters = https://hydra.iohk.io https://cache.nixos.org/
trusted-public-keys = hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
When using nix the documents and Haskell code can be readily
built by running:
nix buildThe LaTeX documents will be places inside directories named result*, e.g.:
result-2/ledger-spec.pdf
result-3/delegation_design_spec.pdf
result-4/non-integer-calculations.pdf
result-5/small-step-semantics.pdf
result-6/ledger-spec.pdf
result/blockchain-spec.pdfChange to the latex directory where the latex document is (e.g. eras/shelley/formal-spec
for the ledger specification corresponding to the Shelley release, or
eras/byron/ledger/formal-spec for the ledger specification corresponding to
the Byron release). Then, build the latex document by running:
nix-shell --pure --run makeFor a continuous compilation of the LaTeX file run:
nix-shell --pure --run "make watch"Issues can be filed in the GitHub Issue tracker.
However, note that this is pre-release software, so we will not usually be providing support.
See CONTRIBUTING.