MartinSchere/cardano-ledger

The ledger implementation and specifications of the Cardano blockchain.

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

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
• Timelocks and Multi-Assets
  • formal-spec
  • implementation
  • tests
• Smart Contracts
  • formal-spec
  • implementation
  • tests
• Libraries

Building

It is recommended to use nix for building everything in this repository. Haskell files can be built with cabal inside of a nix shell.

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

Building the LaTeX documents and executable specifications

When using nix the documents and Haskell code can be readily built by running:

nix build

The 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.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:

nix-shell --pure --run make

For a continuous compilation of the LaTeX file run:

nix-shell --pure --run "make watch"

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.