IntersectMBO · javierdiaz72 · Sep 23, 2025 · Sep 24, 2025 · Sep 24, 2025 · Sep 24, 2025
@@ -8,47 +8,43 @@ The specification is both *formal* (meaning that is machine-checked and amenable
 
 The project is comprised by the following subdirectories:
 
-* `Axiom`: The Agda set theory library
+* `src`: Files comprising the formal specification
 
-* `Data`: Extensions to the Agda standard library
+  - `Foreign`: General utilities to automatically generate Haskell code from Agda code
 
-* `Foreign`: General utilities to automatically generate Haskell code from Agda code
+  - `Interface`: General-purpose type classes not included in the Agda standard library
 
-* `Interface`: General-purpose type classes not included in the Agda standard library
+  - `InterfaceLibrary`: Interfaces exposed by other Cardano components, currently only for the Ledger Layer
 
-* `InterfaceLibrary`: Interfaces exposed by other Cardano components, currently only for the Ledger Layer
+    - `Common`: Component-agnostic features (e.g. stake pool distributions)
 
-  - `Common`: Component-agnostic features (e.g. stake pool distributions)
+  - `Ledger`: Components borrowed from the Ledger specification, most of them actually not Ledger-specific (e.g. slots, epochs, cryptographic primitives)
 
-* `Ledger`: Components borrowed from the Ledger specification, most of them actually not Ledger-specific (e.g. slots, epochs, cryptographic primitives)
+  - `latex`: Auxiliary $$\LaTeX$$-related files required to generate the PDF version of the specification (e.g. fonts, references and static content)
 
-* `Reflection`: Extensions to the reflection support in the Agda standard library
+  - `Spec`: Root directory of the specification
 
-* `Tactic`: General-purpose tactics not included in the Agda standard library
+    - `<STS>.lagda` (e.g. `TickNonce.lagda` for TICKN): The definition of `<STS>` in a human-readable format
 
-* `latex`: Auxiliary $$\LaTeX$$-related files required to generate the PDF version of the specification (e.g. fonts, references and static content)
+    - `<STS>/Properties.agda` (e.g. `TickNonce/Properties.agda` for TICKN): Proofs of properties about `<STS>`. In particular, this file contains a proof that `<STS>` can be 'computed' by a given function. This means that we have an executable version of `<STS>` which is guaranteed to be correct
 
-* `Spec`: Root directory of the specification
+    - `PDF.lagda`: Source Agda file from which the corresponding PDF file is generated
 
-  - `<STS>.lagda` (e.g. `TickNonce.lagda` for TICKN): The definition of `<STS>` in a human-readable format
+    - `Foreign`: Machinery required for the automatic generation of an executable (Haskell) version of the Agda specification
 
-  - `<STS>/Properties.agda` (e.g. `TickNonce/Properties.agda` for TICKN): Proofs of properties about `<STS>`. In particular, this file contains a proof that `<STS>` can be 'computed' by a given function. This means that we have an executable version of `<STS>` which is guaranteed to be correct
+      - `HSConsensus/<STS>.agda` (e.g. `HSConsensus/TickNonce.agda` for TICKN): Contains the code to automatically generate the Haskell types used by `<STS>` and a \*`Step` Haskell function to execute `<STS>`
 
-  - `PDF.lagda`: Source Agda file from which the corresponding PDF file is generated
+      - `ExternalFunctions.agda`: Automatically generates a Haskell record of 'external functions'. An external function is a function used by the Agda specification whose Haskell version should be provided by the calling environment. Dummy external functions are also available
 
-  - `Foreign`: Machinery required for the automatic generation of an executable (Haskell) version of the Agda specification
+      - `HSTypes.agda`: Generates Haskell versions for common Agda types used in the specification, such as sets and maps
 
-    - `HSConsensus/<STS>.agda` (e.g. `HSConsensus/TickNonce.agda` for TICKN): Contains the code to automatically generate the Haskell types used by `<STS>` and a \*`Step` Haskell function to execute `<STS>`
+      - `HSConsensus.agda`: Top-level Agda module from which the executable specification is generated
 
-    - `ExternalFunctions.agda`: Automatically generates a Haskell record of 'external functions'. An external function is a function used by the Agda specification whose Haskell version should be provided by the calling environment. Dummy external functions are also available
+* `src-lib-exts`: Extensions to the Agda standard library (`stdlib`), the IOG prelude library (`iog-prelude`), etc
 
-    - `HSTypes.agda`: Generates Haskell versions for common Agda types used in the specification, such as sets and maps
+* `conformance-example`: A Haskell test suite for the executable specification
 
-    - `HSConsensus.agda`: Top-level Agda module from which the executable specification is generated
-
-  - `hs-src`: A Haskell test suite for the executable specification
-
-  	- `test/<STS>Spec.hs` (e.g. `test/TickNonceSpec.hs` for TICKN): A Haskell program that tests the executable version of `<STS>`
+  - `test/<STS>Spec.hs` (e.g. `test/TickNonceSpec.hs` for TICKN): A Haskell program that tests the executable version of `<STS>`
 
 ## Generating the PDF file
 
@@ -132,22 +128,26 @@ It is possible to perform the above-mentioned tasks without the use of Nix, usin
 
 - Install [latexmk](https://ctan.org/pkg/latexmk/) and [XeTeX](https://xetex.sourceforge.net/)
 
-- Install Agda version `2.7.0` (e.g. follow the instructions in <https://agda.readthedocs.io/en/v2.7.0/getting-started/installation.html#step-1-install-agda>
+- Install Agda version `2.8.0` (e.g. follow the instructions in <https://agda.readthedocs.io/en/v2.8.0/getting-started/installation.html#step-1-install-agda>
 )
 
 - In a folder `<LIB>`, clone the dependencies and checkout the respective commits/tags:
 
   | *Dependency*                                                       | *Tag/commit*                               |
   |--------------------------------------------------------------------|--------------------------------------------|
-  | [agda-stdlib](https://github.com/agda/agda-stdlib)                 | `v2.1.1`                                   |
-  | [agda-stdlib-classes](https://github.com/agda/agda-stdlib-classes) | `73f4da05aeea040fea4587629f9fd83a8f04e656` |
-  | [agda-stdlib-meta](https://github.com/agda/agda-stdlib-meta)       | `v2.1.1`                                   |
+  | [agda-stdlib](https://github.com/agda/agda-stdlib)                 | `v2.3`                                     |
+  | [agda-stdlib-classes](https://github.com/agda/agda-stdlib-classes) | `v2.3`                                     |
+  | [agda-stdlib-meta](https://github.com/agda/agda-stdlib-meta)       | `v2.3`                                     |
+  | [agda-sets](https://github.com/input-output-hk/agda-sets)          | `31512b000317a577230e9ba5081b693801104851` |
+  | [iog-prelude](https://github.com/input-output-hk/iog-agda-prelude) | `e25670dcea694f321cbcd7a0bb704b82d5d7b266` |
 
 - Create a file `<LIB>/libraries` with the following content:
 ```
 <LIB>/agda-stdlib/standard-library.agda-lib
 <LIB>/agda-stdlib-classes/agda-stdlib-classes.agda-lib
 <LIB>/agda-stdlib-meta/agda-stdlib-meta.agda-lib
+<LIB>/agda-sets/abstract-set-theory.agda-lib
+<LIB>/iog-prelude/iog-prelude.agda-lib
 ```
 
 - Instead of `agda` use `agda --library-file <LIB>/libraries`. For example, to typecheck `Everything.agda`:

@@ -1,8 +1,8 @@
 cabal-version:      3.0
-name:               cardano-consensus-executable-spec
+name:               conformance-example
 version:            0.1.0.0
-synopsis: Executable Formal Specification of Ouroboros Consensus
-description: The Haskell code generated from the Agda executable formal specification of the consensus layer for the Ouroboros blockchain protocol
+synopsis: Test programs for the executable formal specification of Ouroboros Consensus
+description: Test programs that exercise the Haskell code generated from the Agda executable formal specification of the consensus layer for the Ouroboros blockchain protocol
 license: Apache-2.0
 license-files:
   LICENSE
@@ -34,7 +34,7 @@ test-suite test
         TickForecastSpec
         ChainHeadSpec
     build-depends:
-        cardano-consensus-executable-spec,
+        conformance-example,
         hspec,
         HUnit,
         text

@@ -3,4 +3,8 @@ depend:
   standard-library
   standard-library-classes
   standard-library-meta
-include: .
+  abstract-set-theory
+  iog-prelude
+include:
+  src
+  src-lib-exts
@@ -1,5 +1,5 @@
 {-# OPTIONS --safe #-}
-module Reflection.Ext where
+module stdlib-meta.Reflection where
 
 open import Prelude hiding (Type)
 open import PreludeMeta

@@ -5,10 +5,10 @@
 -- genErrors: match on a negated conjunction and return the string of that type
 --------------------------------------------------------------------------------
 
-module Tactic.GenError where
+module stdlib-meta.Tactic.GenError where
 
-open import MetaPrelude
-open import Meta
+open import Meta.Prelude
+open import Meta.Init
 
 open import Class.Functor
 open import Class.Monad
@@ -35,10 +35,6 @@ instance
 
 open ClauseExprM
 
-private
-  liftTC : {A : Set} → R.TC A → TC A
-  liftTC x = λ r → applyExtContext (r .TCEnv.localContext) x
-
 genError' : ITactic
 genError' = inDebugPath "genError" do
   t ← inferType (♯ 0)

@@ -1,6 +1,6 @@
 {-# OPTIONS --safe #-}
 -- {-# OPTIONS -v tactic.premises:100 #-}
-module Tactic.Premises where
+module stdlib-meta.Tactic.Premises where
 
 open import Prelude hiding (Type)
 open import PreludeMeta

@@ -2,7 +2,7 @@
 
 open import Agda.Primitive renaming (Set to Type)
 
-module Data.Rational.Ext where
+module stdlib.Data.Rational.Ext where
 
 open import Function using (_∘_; _$_)
 open import Data.Rational hiding (show)