Skip to content
A formal specification and executable model of the ledger rules introduced by the Shelley release
Branch: master
Clone or download
dnadales Add coverage for delegation traces (via DBLOCK transition system) (#570)
- Sync the executable spec with the formal spec:
  - We didn't check injectivity of the delegation map
  - We didn't check that we delegation epoch didn't lie past the next epoch.
- Fix the implementation of the `SDELEGS` and `ADELEGS` rule, where the
  delegation certificates where applied in the reverse order.
- Delete the applied delegation certificates. We used to keep past delegation
  certificates. However this led to unexpected behavior where an invalid
  certificate would be re-applied resulting in a delegation behavior that was
  hard to predict and reason with. 
- Improved the delegation certificate generators:
  - Take into account the allowed delegators that can delegate.
- In the tests adapt `expectedDms` so that the injectiviy constraint is taken
  into account when applying a sequence of delegation certificates.
  

Closes #562 
Closes #297
Latest commit 5eba028 Jun 17, 2019

README.md

Formal Models for Ledger Rules

Build Status Coverage Status

Formal and executable specifications for the new features to be introduced by Shelley.

The documents are built in our CI and can be readily accessed using the following links:

Repository structure

This repo contains formal (LaTeX) and executable (Haskell model) specs for both the Byron and Shelley eras of Cardano. The outline of the specs is as follows:

Build tools

For building LaTeX documents we use nix. Haskell files can be built either with nix or stack.

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 executable specifications 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. shelley/chain-and-ledger/formal-spec for the ledger specification corresponding to the Shelley release, or 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"

Testing the Haskell model

Change to the directory where the executable specifications are (e.g. shelley/chain-and-ledger/executable-spec for the executable ledger specifications corresponding to the Shelley release, or byron/ledger/executable-spec for the executable ledger specifications corresponding to the Byron release). Then run build the specs by running:

stack build

The tests can be run by executing:

stack test

While developing the models, it can be helpful to run ghcid in a separate shell:

make ghcid

or with tests included:

make ghcid-test

nix-build Infrastructure

The artifacts in this repository can be built and tested using nix. This is additionally used by the Hydra CI to test building, including cross-compilation for other systems.

To add a new Haskell project

To add a new Haskell project, you should do the following:

  1. Create the project in the usual way. It should have an appropriate .cabal file.
  2. Add the project to the top-level stack.yaml, configuring dependencies etc as needed. If your project's configuration deviates too far from the snapshot in ``cardano-prelude`, then you may have to submit a PR there to update that snapshot.
  3. At this point, test that your new project builds using stack build <project_name>.
  4. Run the regenerate script to rebuild the nix configuration from your stack.yaml file.
  5. Test that you can build your new project by running the following: nix build -f default.nix nix-tools.libs.<project_name>. If you have executables, then you may also try building these using the nix-tools.exes.<executable_name> attribute path. A good way to see what's available is to execute :l default.nix in nix repl. This will allow you to explore the potential attribute names.
  6. If you want your product to be tested by CI, add it to release.nix using the format specified in that file.

To add a new LaTeX specification

To add a new LaTeX specification, the easiest way is to copy from one of the existing specifications. You will want the Makefile and default.nix (say from the Shelley ledger spec).

  1. Copy these files into the root of your new LaTeX specification.
  2. Modify the DOCNAME in the Makefile.
  3. Update default.nix to:
    1. Make sure that the relative path in the first line is pointing to (lib.nix)[./nix/lib.nix]. This is used to pin the nixpkgs version used to build the LaTeX specifications.
    2. Update the buildInputs to add in any LaTeX packages you need in your document, and remove any unneeded ones.
    3. Alter the meta description field to reflect the nature of this document.
  4. Add a link to the package at the bottom of default.nix, following the existing examples.
  5. To require that your specification be built in CI, add it to the required-targets list in release.nix following the existing examples.

Additional documentation

You can find additional documentation on the nix infrastructure used in this repo in the following places:

Note that the user guide linked above is incomplete and does not correctly refer to projects built using iohk-nix, as this one is. A certain amount of trial and error may be required to make substantive changes!

You can’t perform that action at this time.