Skip to content

IntersectMBO/cardano-ledger

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Cardano Ledger

CEH GitHub Workflow Status (master) Haddock (master)

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.

Repository structure

The directory structure of this repository is as follows:

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.