This repository contains the formal ledger specifications that are intended to eventually replace the existing formal specifications of the Cardano ledger found here. This project is currently incomplete and work in progress.
This repository currently contains two specifications---the work in progress specification for Cardano (up to and including the Conway era) and a small example that was produced for the Midnight project (but is unrelated to any actual Midnight code/features). Each specification is executable and contains some documentation in the form of a PDF document. They can be built by following the steps below.
| Formal Specification | HTML Version | Haskell Tests |
|---|---|---|
| Full Cardano Ledger | Ledger.PDF | UTXOW test |
| Conway | Ledger.PDF | UTXOW test |
| Midnight Example | MidnightExample.PDF | LEDGER test |
Note: the HTML versions of the specifications are interactive, but many modules currently contain LaTeX code which is used to generate the PDF. We intend to fix this eventually.
git clone https://github.com/IntersectMBO/formal-ledger-specifications.git
cd formal-ledger-specifications
Invoke the following nix-build commands from inside the formal-ledger-specifications directory.
nix-build -A ledger.docs # generate the PDF spec of the Cardano ledger
nix-build -A midnight.docs # generate the PDF spec of the Midnight example
nix-build -A ledger.hsSrc # extract the Haskell code of the Cardano ledger
nix-build -A midnight.hsSrc # extract the Haskell code of the Midnight example
The hsExe is a cabal package, which can be loaded into GHCI like this:
nix-shell -A run --command "cabal repl --build-depends 'cardano-ledger'"
λ> :m Lib
λ> :i UTxOState
Building the hsExe derivation will also run the test suite, which you can manually do using cabal test.
If you would like more detailed information and/or you want to contribute to the Agda formalization of the spec, please see the CONTRIBUTING.md file.
Please submit a new issue if you find problems with, and/or wish to comment on, this repository.