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, PDF | |
Shelley | Design | Spec | CDDL |
Allegra | Same as Mary era below | Same as Mary era below | CDDL |
Mary | Multi-Currency, UTXOma | Spec | CDDL |
Alonzo | eUTXO | Spec | CDDL |
Babbage | batch-verification, CIP-31, CIP-32, CIP-33 | Spec | CDDL |
Conway | CIP-1694 | Spec (WIP) | CDDL |
Other Documents:
In addition, there is a formalization of the Ledger Specification in Isabelle/HOL which can be found here.
Some user documentation is published on Read the Docs
Haddock code documentation of the latest master branch is available 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.
Make sure you have a recent version of nix
by following this guide
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.settings = {
experimental-features = [ "nix-command" "flakes" ];
substituters = [
"https://cache.nixos.org"
"https://cache.iog.io"
];
trusted-public-keys = [
"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
:
experimental-features = nix-command flakes
substituters = https://cache.iog.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 build .#specs
The LaTeX documents will be placed inside a directory named result
, e.g.:
result/byron-ledger.pdf
result/shelley-delegation.pdf
result/non-integer-calculations.pdf
result/small-step-semantics.pdf
result/shelley-ledger.pdf
result/byron-blockchain.pdf
Change 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:
cd <myLaTexDir>
nix develop --command make
For a continuous compilation of the LaTeX
file run:
cd <myLaTexDir>
nix develop --command make watch
Run cabal test all
to run all tests or cabal test <package>
to run the tests for a specific package.
Note: The CARDANO_MAINNET_MIRROR
environment variable can be overriden in flake.nix
if one desires to run
the Byron tests with a different version of the mainnet epochs.
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.