mkdocs.yml

# Project information
site_name: Formal Ledger Specification
site_url: https://intersectmbo.github.io/formal-ledger-specifications/
site_description: Formal ledger specification and documentation.
site_author: Formal Methods Ledger Team
repo_url: https://github.com/IntersectMBO/formal-ledger-specifications

# Use edit_uri_template to build file URLs (GitHub "blob" view)
edit_uri_template: blob/main/docs/{path}?plain=1

# Theme configuration (using mkdocs-material)
theme:
  name: material
  custom_dir: overrides
  favicon: img/Cardano-RGB_Logo-Icon-White.svg
  # Optional features - see mkdocs-material docs for many more
  features:
    - toc.follow      # <-- keeps the right toc aligned with your position
    - content.tooltips
    - content.code.copy
    - content.action.view  # Adds "View source" button (links to raw files)
    - navigation.footer
    - navigation.sections
    - navigation.tabs
  palette:
  - scheme: slate
    toggle:
      icon: material/weather-sunny
      name: Dark mode
    primary: black
  - scheme: default
    toggle:
      icon: material/weather-night
      name: Light mode
  icon:
    edit: fontawesome/brands/github    # <- octocat icon (link to file)
    view: fontawesome/brands/github    #
    repo: fontawesome/brands/git-alt   # <- git icon (link to repo)

  # Font configuration (optional)
  font:
    text: Open Sans        # Other options: Cambria, Lato, Roboto
    code: Source Code Pro  # Other options: Roboto Mono, StrippedJuliaMono (if available via CSS)d?
  logo: img/Cardano-RGB_Logo-Icon-Blue.svg

extra_css:
  # KaTeX CSS for math rendering
  - https://cdn.jsdelivr.net/npm/katex@0.16.9/dist/katex.min.css
  - css/custom.css
  - Agda.css
extra_javascript:
  # KaTeX JavaScript
  - https://cdn.jsdelivr.net/npm/katex@0.16.9/dist/katex.min.js
  - https://cdn.jsdelivr.net/npm/katex@0.16.9/dist/contrib/auto-render.min.js
  # mermaid JavaScript
  - https://unpkg.com/mermaid/dist/mermaid.min.js
  - js/katex-config.js
  - AgdaKaTeX.js
  - https://cdn.jsdelivr.net/npm/chart.js
  - js/custom.js
markdown_extensions:
  - admonition                # call-out boxes like !!! note
  - pymdownx.details
  - pymdownx.smartsymbols
  - toc:                      # table of contents generation
      permalink: true         # anchor links to headers
  - pymdownx.superfences:     # syntax highlighting in code blocks
      custom_fences:
      - name: mermaid
        class: mermaid
  - attr_list                 # inline attributes like `code`{.class}
  - pymdownx.tabbed:
      alternate_style: true
  - pymdownx.emoji
  - pymdownx.snippets:
      check_paths: true  # for debugging
      auto_append:
      - includes/links.md
  # Important: Use pymdownx.arithmatex with KaTeX
  - pymdownx.arithmatex:
      generic: true
  - footnotes
  - md_in_html
hooks:
- hooks/agda_hidden_code.py
- hooks/agda_source_link.py
extra:
  source_branch: master
  source_overrides:
    index.md: README.md
    Definitions.md: build-tools/static/md/common/src/Definitions.md
    Notation.md: build-tools/static/md/common/src/Notation.md
use_directory_urls: false

# Navigation structure
nav:
- Home: index.md
- Preliminaries:
  - Introduction: Ledger.Introduction.md
  - Notation: Notation.md
  - Earlier Eras: EarlierEras.md
- Core:
  - Introduction: Ledger.Core.Specification.md
  - Modules/:
    - Address: Ledger.Core.Specification.Address.md
    - Crypto: Ledger.Core.Specification.Crypto.md
    - Epoch: Ledger.Core.Specification.Epoch.md
    - ProtocolVersion: Ledger.Core.Specification.ProtocolVersion.md
- Conway:
  - Introduction: Ledger.Conway.Specification.md
  - Modules/:
    - Abstract: Ledger.Conway.Specification.Abstract.md
    - BlockBody: Ledger.Conway.Specification.BlockBody.md
    - BlockBody/:
      - Properties: Ledger.Conway.Specification.BlockBody.Properties.md
      - Properties/:
        - Computational: Ledger.Conway.Specification.BlockBody.Properties.Computational.md
    - Certs: Ledger.Conway.Specification.Certs.md
    - Certs/:
      - Properties: Ledger.Conway.Specification.Certs.Properties.md
      - Properties/:
        - Computational: Ledger.Conway.Specification.Certs.Properties.Computational.md
        - PoV: Ledger.Conway.Specification.Certs.Properties.PoV.md
        - PoVLemmas: Ledger.Conway.Specification.Certs.Properties.PoVLemmas.md
        - VoteDelegsVDeleg: Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg.md
    - Chain: Ledger.Conway.Specification.Chain.md
    - Chain/:
      - Properties: Ledger.Conway.Specification.Chain.Properties.md
      - Properties/:
        - Computational: Ledger.Conway.Specification.Chain.Properties.Computational.md
        - CredDepsEqualDomRwds: Ledger.Conway.Specification.Chain.Properties.CredDepsEqualDomRwds.md
        - EpochStep: Ledger.Conway.Specification.Chain.Properties.EpochStep.md
        - GovDepsMatch: Ledger.Conway.Specification.Chain.Properties.GovDepsMatch.md
        - PParamsWellFormed: Ledger.Conway.Specification.Chain.Properties.PParamsWellFormed.md
    - Enact: Ledger.Conway.Specification.Enact.md
    - Enact/:
      - Properties: Ledger.Conway.Specification.Enact.Properties.md
      - Properties/:
        - Computational: Ledger.Conway.Specification.Enact.Properties.Computational.md
    - Epoch: Ledger.Conway.Specification.Epoch.md
    - Epoch/:
      - Properties: Ledger.Conway.Specification.Epoch.Properties.md
      - Properties/:
        - Computational: Ledger.Conway.Specification.Epoch.Properties.Computational.md
        - ConstRwds: Ledger.Conway.Specification.Epoch.Properties.ConstRwds.md
        - ExpiredDReps: Ledger.Conway.Specification.Epoch.Properties.ExpiredDReps.md
        - GovDepsMatch: Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch.md
        - NoPropSameDReps: Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps.md
    - Fees: Ledger.Conway.Specification.Fees.md
    - Gov: Ledger.Conway.Specification.Gov.md
    - Gov/:
      - Base: Ledger.Conway.Specification.Gov.Base.md
      - Actions: Ledger.Conway.Specification.Gov.Actions.md
      - Properties: Ledger.Conway.Specification.Gov.Properties.md
      - Properties/:
        - Computational: Ledger.Conway.Specification.Gov.Properties.Computational.md
        - ChangePPGroup: Ledger.Conway.Specification.Gov.Properties.ChangePPGroup.md
    - Ledger: Ledger.Conway.Specification.Ledger.md
    - Ledger/:
      - Properties: Ledger.Conway.Specification.Ledger.Properties.md
      - Properties/:
        - Base: Ledger.Conway.Specification.Ledger.Properties.Base.md
        - ChangePPGroup: Ledger.Conway.Specification.Ledger.Properties.ChangePPGroup.md
        - Computational: Ledger.Conway.Specification.Ledger.Properties.Computational.md
        - GovDepsMatch: Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch.md
        - PoV: Ledger.Conway.Specification.Ledger.Properties.PoV.md
    - PoolReap: Ledger.Conway.Specification.PoolReap.md
    - PoolReap/:
      - Properties/:
        - Computational: Ledger.Conway.Specification.PoolReap.Properties.Computational.md
    - PParams: Ledger.Conway.Specification.PParams.md
    - Properties: Ledger.Conway.Specification.Properties.md
    - Ratify: Ledger.Conway.Specification.Ratify.md
    - Ratify/:
      - Properties: Ledger.Conway.Specification.Ratify.Properties.md
      - Properties/:
        - Computational: Ledger.Conway.Specification.Ratify.Properties.Computational.md
    - Rewards: Ledger.Conway.Specification.Rewards.md
    - Rewards/:
      - Properties: Ledger.Conway.Specification.Rewards.Properties.md
      - Properties/:
        - Computational: Ledger.Conway.Specification.Rewards.Properties.Computational.md
    - RewardUpdate: Ledger.Conway.Specification.RewardUpdate.md
    - RewardUpdate/:
      - Properties: Ledger.Conway.Specification.RewardUpdate.Properties.md
      - Properties/:
        - Computational: Ledger.Conway.Specification.RewardUpdate.Properties.Computational.md
    - Script: Ledger.Conway.Specification.Script.md
    - Script/:
      - Base: Ledger.Conway.Specification.Script.Base.md
      - ScriptPurpose: Ledger.Conway.Specification.Script.ScriptPurpose.md
      - Timelock: Ledger.Conway.Specification.Script.Timelock.md
      - Validation: Ledger.Conway.Specification.Script.Validation.md
    - TokenAlgebra/:
      - Base: Ledger.Conway.Specification.TokenAlgebra.Base.md
      - Coin: Ledger.Conway.Specification.TokenAlgebra.Coin.md
      - ValueSet: Ledger.Conway.Specification.TokenAlgebra.ValueSet.md
      - ValueVector: Ledger.Conway.Specification.TokenAlgebra.ValueVector.md
    - Transaction: Ledger.Conway.Specification.Transaction.md
    - Utxo: Ledger.Conway.Specification.Utxo.md
    - Utxo/:
      - Properties: Ledger.Conway.Specification.Utxo.Properties.md
      - Properties/:
        - Base: Ledger.Conway.Specification.Utxo.Properties.Base.md
        - Computational: Ledger.Conway.Specification.Utxo.Properties.Computational.md
        - GenMinspend: Ledger.Conway.Specification.Utxo.Properties.GenMinSpend.md
        - MinSpend: Ledger.Conway.Specification.Utxo.Properties.MinSpend.md
        - PoV: Ledger.Conway.Specification.Utxo.Properties.PoV.md
    - Utxow: Ledger.Conway.Specification.Utxow.md
    - Utxow/:
      - Properties: Ledger.Conway.Specification.Utxow.Properties.md
      - Properties/:
        - Computational: Ledger.Conway.Specification.Utxow.Properties.Computational.md
    - Types/:
      - GovStructure: Ledger.Conway.Specification.Types.GovStructure.md
- Dijkstra:
  - Introduction: Ledger.Dijkstra.Specification.md
  - Modules/:
    - Abstract: Ledger.Dijkstra.Specification.Abstract.md
    - Account: Ledger.Dijkstra.Specification.Account.md
    - BlockBody: Ledger.Dijkstra.Specification.BlockBody.md
    - BlockBody/:
      - Properties: Ledger.Dijkstra.Specification.BlockBody.Properties.md
      - Properties/:
        - Computational: Ledger.Dijkstra.Specification.BlockBody.Properties.Computational.md
    - Certs: Ledger.Dijkstra.Specification.Certs.md
    - Certs/:
      - Properties: Ledger.Dijkstra.Specification.Certs.Properties.md
      - Properties/:
        - Computational: Ledger.Dijkstra.Specification.Certs.Properties.Computational.md
    - Chain: Ledger.Dijkstra.Specification.Chain.md
    - Chain/:
      - Properties: Ledger.Dijkstra.Specification.Chain.Properties.md
      - Properties/:
        - Computational: Ledger.Dijkstra.Specification.Chain.Properties.Computational.md
    - Enact: Ledger.Dijkstra.Specification.Enact.md
    - Enact/:
      - Properties: Ledger.Dijkstra.Specification.Enact.Properties.md
      - Properties/:
        - Computational: Ledger.Dijkstra.Specification.Enact.Properties.Computational.md
    - Entities: Ledger.Dijkstra.Specification.Entities.md
    - Entities/:
      - Properties: Ledger.Dijkstra.Specification.Entities.Properties.md
      - Properties/:
        - Computational: Ledger.Dijkstra.Specification.Entities.Properties.Computational.md
    - Epoch: Ledger.Dijkstra.Specification.Epoch.md
    - Epoch/:
      - Properties: Ledger.Dijkstra.Specification.Epoch.Properties.md
      - Properties/:
        - Computational: Ledger.Dijkstra.Specification.Epoch.Properties.Computational.md
    - Fees: Ledger.Dijkstra.Specification.Fees.md
    - Gov: Ledger.Dijkstra.Specification.Gov.md
    - Gov/:
      - Actions: Ledger.Dijkstra.Specification.Gov.Actions.md
      - Base: Ledger.Dijkstra.Specification.Gov.Base.md
      - Properties: Ledger.Dijkstra.Specification.Gov.Properties.md
      - Properties/:
        - Computational: Ledger.Dijkstra.Specification.Gov.Properties.Computational.md
    - Ledger: Ledger.Dijkstra.Specification.Ledger.md
    - Ledger/:
      - Properties: Ledger.Dijkstra.Specification.Ledger.Properties.md
      - Properties/:
        - Computational: Ledger.Dijkstra.Specification.Ledger.Properties.Computational.md
    - PoolReap: Ledger.Dijkstra.Specification.PoolReap.md
    - PoolReap/:
      - Properties: Ledger.Dijkstra.Specification.PoolReap.Properties.md
      - Properties/:
        - Computational: Ledger.Dijkstra.Specification.PoolReap.Properties.Computational.md
    - PParams: Ledger.Dijkstra.Specification.PParams.md
    - Ratify: Ledger.Dijkstra.Specification.Ratify.md
    - Ratify/:
      - Properties: Ledger.Dijkstra.Specification.Ratify.Properties.md
      - Properties/:
        - Computational: Ledger.Dijkstra.Specification.Ratify.Properties.Computational.md

    - Rewards: Ledger.Dijkstra.Specification.Rewards.md
    - Rewards/:
      - Properties: Ledger.Dijkstra.Specification.Rewards.Properties.md
      - Properties/:
        - Computational: Ledger.Dijkstra.Specification.Rewards.Properties.Computational.md
    - RewardUpdate: Ledger.Dijkstra.Specification.RewardUpdate.md
    - RewardUpdate/:
      - Properties: Ledger.Dijkstra.Specification.RewardUpdate.Properties.md
      - Properties/:
        - Computational: Ledger.Dijkstra.Specification.RewardUpdate.Properties.Computational.md
    - Script: Ledger.Dijkstra.Specification.Script.md
    - Script/:
      - Base: Ledger.Dijkstra.Specification.Script.Base.md
      - Native: Ledger.Dijkstra.Specification.Script.Native.md
      - ScriptPurpose: Ledger.Dijkstra.Specification.Script.ScriptPurpose.md
      - Validation: Ledger.Dijkstra.Specification.Script.Validation.md
    - TokenAlgebra: Ledger.Dijkstra.Specification.TokenAlgebra.Base.md
    - Transaction: Ledger.Dijkstra.Specification.Transaction.md
    - Utxo: Ledger.Dijkstra.Specification.Utxo.md
    - Utxo/:
      - Properties: Ledger.Dijkstra.Specification.Utxo.Properties.md
      - Properties/:
        - Computational: Ledger.Dijkstra.Specification.Utxo.Properties.Computational.md
    - Utxow: Ledger.Dijkstra.Specification.Utxow.md
    - Utxow/:
      - Properties: Ledger.Dijkstra.Specification.Utxow.Properties.md
      - Properties/:
        - Computational: Ledger.Dijkstra.Specification.Utxow.Properties.Computational.md
- Appendix:
  - Background:
    - Definitions: Definitions.md
    - Essential Agda: EssentialAgda.md
    - Bootstrapping:
      - Bootstrapping Governance: ConwayBootstrap.md
      - Bootstrapping EnactState: ConwayBootstrapEnact.md
  - Era-independent Modules:
    - Prelude: Prelude.md
    - Ledger: Ledger.md
    - Ledger.Core: Ledger.Core.md
    - Ledger.Prelude: Ledger.Prelude.md
    - Ledger.Prelude/:
      - Base: Ledger.Prelude.Base.md
      - Foreign/:
        - HSTypes: Ledger.Prelude.Foreign.HSTypes.md
        - Util: Ledger.Prelude.Foreign.Util.md
      - HasCoin: Ledger.Prelude.HasCoin.md
      - Instances: Ledger.Prelude.Instances.md
      - Numeric: Ledger.Prelude.Numeric.md
      - Numeric/:
        - PositiveNat: Ledger.Prelude.Numeric.PositiveNat.md
        - UnitInterval: Ledger.Prelude.Numeric.UnitInterval.md
    - Interface:
      - STS: Interface.STS.md
      - ComputationalRelation: Interface.ComputationalRelation.md
      - TypeClasses: Interface.TypeClasses.Hashable.md
      - TypeClasses/:
        - Hashable: Interface.TypeClasses.Hashable.md
        - HasSubset: Interface.TypeClasses.HasSubset.md
        - HasSubtract: Interface.TypeClasses.HasSubtract.md
        - HasSubtract/:
          - Instance: Interface.TypeClasses.HasSubtract.Instances.md
    - MyDebugOptions: MyDebugOptions.md
  - Era-dependent Modules:
    - Dijkstra:
      - Ledger.Dijkstra: Ledger.Dijkstra.md
    - PreConway:
      - Ledger.PreConway: Ledger.PreConway.md
      - Ledger.PreConway/:
        - Conformance:
          - NewPP: Ledger.PreConway.Conformance.NewPP.md
          - NewPP/:
            - Properties: Ledger.PreConway.Conformance.NewPP.Properties.md
          - PPUp: Ledger.PreConway.Conformance.PPUp.md
          - PPUp/:
            - Properties: Ledger.PreConway.Conformance.PPUp.Properties.md
        - NewPP: Ledger.PreConway.NewPP.md
        - NewPP/:
          - Properties: Ledger.PreConway.NewPP.Properties.md
        - PPUp: Ledger.PreConway.PPUp.md
        - PPUp/:
          - Properties: Ledger.PreConway.PPUp.Properties.md
    - Conway:
      - Ledger.Conway: Ledger.Conway.md
      - Conformance: Ledger.Conway.Conformance.md
      - Conformance/:
        - Certs: Ledger.Conway.Conformance.Certs.md
        - Certs/:
          - Properties: Ledger.Conway.Conformance.Certs.Properties.md
        - Epoch: Ledger.Conway.Conformance.Epoch.md
        - Equivalence: Ledger.Conway.Conformance.Equivalence.md
        - Equivalence/:
          - Bisimilarity: Ledger.Conway.Conformance.Equivalence.Bisimilarity.md
          - Certs: Ledger.Conway.Conformance.Equivalence.Certs.md
          - Convert: Ledger.Conway.Conformance.Equivalence.Convert.md
          - Deposits: Ledger.Conway.Conformance.Equivalence.Deposits.md
          - Utxo: Ledger.Conway.Conformance.Equivalence.Utxo.md
        - Gov: Ledger.Conway.Conformance.Gov.md
        - Ledger: Ledger.Conway.Conformance.Ledger.md
        - Ledger/:
          - Properties: Ledger.Conway.Conformance.Ledger.Properties.md
        - Properties: Ledger.Conway.Conformance.Properties.md
        - Rewards: Ledger.Conway.Conformance.Rewards.md
        - Utxo: Ledger.Conway.Conformance.Utxo.md
        - Utxo/:
          - Properties: Ledger.Conway.Conformance.Utxo.Properties.md
        - Utxow: Ledger.Conway.Conformance.Utxow.md
        - Utxow/:
          - Properties: Ledger.Conway.Conformance.Utxow.Properties.md