Cardano Ledger

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:

• 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.

Some user documentation is published on Read the Docs

Haddock code documentation of the latest master branch is available here.

Repository structure

The directory structure of this repository is as follows:

• Byron
  • ledger
    • formal-spec
    • executable-spec
    • implementation
  • chain
    • formal-spec
    • executable-spec
  • cddl
• Shelley
  • design-spec
  • formal-spec
  • implementation
  • tests
  • cddl
• Allegra - Timelocks
  • formal-spec
  • implementation
  • tests
• Mary - Multi-Assets
  • formal-spec
  • implementation
  • tests
• Alonzo - Smart Contracts
  • formal-spec
  • implementation
  • cddl
  • tests
• Babbage
  • formal-spec
  • implementation
  • cddl
  • tests
• Conway - Governance
  • formal-spec
  • implementation
  • cddl
  • tests
• Libraries

Building

It is recommended to use nix for building everything in this repository. Make sure you have a recent version of nix by following this guide.

Haskell files can be built with cabal inside of a nix shell, which can be entered by invoking nix develop from the root directory.

Nix Cache

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=

Building the LaTeX documents and executable specifications

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

Building individual LaTeX documents

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

Testing

From the root directory invoke nix develop to enter a nix shell, then 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 overridden in flake.nix if one desires to run the Byron tests with a different version of the mainnet epochs.

Submitting an issue

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.

Contributing

See CONTRIBUTING.

Using git fsck

There's some ancient history in the repo that causes git fsck version 2.44.0 or later to report errors when running semantic checks on an old version of the .gitmodules file.

This can be overcome by running git config fsck.skipList .git-fsck-skiplist once, sometime after cloning.

However, the problem prevents cloning if you have transfer.fsckObjects enabled in your global git configuration. You can overcome this by downloading the skiplist file before you clone and then specifying it in a config option to the clone command:

$ curl -sSLO https://raw.githubusercontent.com/IntersectMBO/cardano-ledger/refs/heads/master/.git-fsck-skiplist
$ git clone -c fetch.fsck.skipList=.git-fsck-skiplist ...
...
$ rm .git-fsck-skiplist