Cardano Ledger Conformance Testing

20250923-cl-fls-conformance-testing.md

fls/cl conformance tests notes

These notes describe running conformance tests on the Cardano blockchain ledger---specifically, we test the native Haskell implementation against the Agda-generated Haskell code of the formal specification.

We'll create

fls = a directory where we clone the formal-ledger-specifications repo.

cl = a directory where we clone the cardano-ledger repo.

in our $HOME directory, but the choice of location is arbitrary.

1. Clone the formal-ledger-specifications repository.

   In the directory fls/master clone the formal-ledger-specifications repository, as follows:

   cd              # enter $HOME directory
   mkdir -p fls
   cd fls
   git clone https://github.com/IntersectMBO/formal-ledger-specifications.git master
   cd master

   We're now in fls/master, the project root of formal-ledger-specifications, on the master branch.

2. Generate Haskell code from the Agda formalization.

   In the fls/master directory, enter

   nix develop --command fls-shake hs
   

   Upon completion, this results in

   fls/master/dist/hs
   

3. Clone the cardano-ledger repository.

   In the directory cl/master clone the cardano-ledger repository, as follows:

   cd              # enter $HOME directory
   mkdir -p cl
   cd cl
   git clone https://github.com/IntersectMBO/cardano-ledger.git master
   cd master

4. Edit the cabal.project file.

   Comment out the following block:

   source-repository-package
     type: git
     location: https://github.com/IntersectMBO/formal-ledger-specifications.git
     subdir: hs
     -- !WARNING!:
     -- MAKE SURE THIS POINTS TO A COMMIT IN `*-artifacts` BEFORE MERGE!
     tag: 61f0683c62adf1efe67f14e11dc0edfe884c348f
   

   and place the following at the bottom of the packages: section:

   /home/your-user-name/fls/master/dist/hs
   

   Important. Replace /home/you-user-name/ with your actual $HOME directory!

5. Enter the default Nix development shell.

   cd
   cd cl/master
   nix develop
   

6. Run some tests!

   For example, to run tests concerning the CERTS rule,

   cabal test cardano-ledger-conformance --test-options='--match "CERTS"'