Refactor documentation of properties #986

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged

williamdemeo merged 5 commits into master from 965-refactor-properties

Dec 9, 2025

+419 −207

build-tools/static/md/mkdocs/docs/Properties.md

This file was deleted.

build-tools/static/md/mkdocs/includes/links.md

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -11,23 +11,32 @@
  
    [CERT]: Ledger.Conway.Specification.Certs.md#sec:the-certs-transition-system

    [CERTS]: Ledger.Conway.Specification.Certs.md#sec:the-certs-transition-system

    [CERTS rules]: Ledger.Conway.Specification.Certs.md#sec:the-certs-transition-system

    [CERTS-PoV]: Ledger.Conway.Specification.Certs.Properties.PoV.md#thm:CERTS-PoV

    [CERT-PoV]: Ledger.Conway.Specification.Certs.Properties.PoVLemmas.md#thm:CERT-PoV

    [Certs.Properties.PoV]: Ledger.Conway.Specification.Certs.Properties.PoV.md

    [Certs.Properties.PoVLemmas]: Ledger.Conway.Specification.Certs.Properties.PoVLemmas.md

    [Certs.Properties.VoteDelegsVDeleg]: Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg.md

    [Certs-VoteDelegsVDeleg]: Ledger.Conway.Specification.Certs.Properties.VoteDelegsVDeleg.md#clm:VDelegsInRegDReps

    [CHAIN]: Ledger.Conway.Specification.Chain.md#sec:the-chain-transition-system

    [CIPs]: https://github.com/cardano-foundation/CIPs

    [CHAIN-GovDepsMatch]: Ledger.Conway.Specification.Chain.Properties.GovDepsMatch.md#thm:ChainGovDepsMatch

    [Chain.Properties.CredDepsEqualDomRwds]: Ledger.Conway.Specification.Chain.Properties.CredDepsEqualDomRwds.md

    [Chain.Properties.EpochStep]: Ledger.Conway.Specification.Chain.Properties.EpochStep.md

    [CHAIN-EpochStep]: Ledger.Conway.Specification.Chain.Properties.EpochStep.md#clm:EpochStep

    [CHAIN-CredDepsEqualDomRwds-inv]: Ledger.Conway.Specification.Chain.Properties.CredDepsEqualDomRwds.md#clm:CredDepsEqualDomRwds-inv

    [CHAIN-PParamsWellFormed-inv]: Ledger.Conway.Specification.Chain.Properties.PParamsWellFormed.md#clm:pp-wellFormed-inv

    [Chain.Properties.PParamsWellFormed]: Ledger.Conway.Specification.Chain.Properties.PParamsWellFormed.md

    [Chain.Properties.GovDepsMatch]: Ledger.Conway.Specification.Chain.Properties.GovDepsMatch.md

    [CIPs]: https://github.com/cardano-foundation/CIPs

    [DELEG]: Ledger.Conway.Specification.Certs.md#auxiliary-deleg-transition-system

    [ENACT]: Ledger.Conway.Specification.Enact.md#sec:the-enact-transition-system

    [EPOCH]: Ledger.Conway.Specification.Epoch.md#sec:the-epoch-transition-system

    [Epoch]: Ledger.Conway.Specification.Epoch.md

    [Epoch Boundary]: Ledger.Conway.Specification.Epoch.md#sec:epoch-boundary

    [Epoch.Properties.ConstRwds]: Ledger.Conway.Specification.Epoch.Properties.ConstRwds.md

    [Epoch.Properties.GovDepsMatch]: Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch.md

    [EPOCH-GovDepsMatch]: Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch.md#lem:EpochGovDepsMatch

    [Epoch.Properties.NoPropSameDReps]: Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps.md

    [Epoch-NoPropSameDReps]: Ledger.Conway.Specification.Epoch.Properties.NoPropSameDReps.md#clm:NoPropSameDReps

    [Essential Agda]: EssentialAgda.md

    [Fees]: Ledger.Conway.Specification.Fees.md

    [formal ledger specification]: https://github.com/IntersectMBO/formal-ledger-specifications

    @@ -38,16 +47,18 @@
  
    [Gov.Properties.ChangePPGroup]: Ledger.Conway.Specification.Gov.Properties.ChangePPGroup.md

    [GOVCERT]: Ledger.Conway.Specification.Certs.md#auxiliary-govcert-transition-system

    [Governance Functions]: Ledger.Conway.Specification.Gov.md#governance-functions

    [Gov-ChangePPHasGroup]: Ledger.Conway.Specification.Gov.Properties.ChangePPGroup.md#clm:ChangePPGroup

    [issues]: https://github.com/IntersectMBO/formal-ledger-specifications/issues

    [Introduction]: Ledger.Introduction.md

    [LEDGER]: Ledger.Conway.Specification.Ledger.md#ledger-transition-system

    [Ledger.Properties]: Ledger.Conway.Specification.Ledger.Properties.md

    [Ledger.Properties.GovDepsMatch]: Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch.md

    [Ledger.Properties.PoV]: Ledger.Conway.Specification.Ledger.Properties.PoV.md

    [LEDGERS]: Ledger.Conway.Specification.Ledger.md#ledgers-transition-system

    [lem:EpochGovDepsMatch]: Ledger.Conway.Specification.Epoch.Properties.GovDepsMatch.md#lem:EpochGovDepsMatch

    [lem:LedgerGovDepsMatch]: Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch.md#lem:LedgerGovDepsMatch

    [LEDGER-PoV]: Ledger.Conway.Specification.Ledger.Properties.PoV.md#thm:LEDGER-PoV

    [LEDGER-GovDepsMatch]: Ledger.Conway.Specification.Ledger.Properties.GovDepsMatch.md#lem:LedgerGovDepsMatch

    [NEWEPOCH]: Ledger.Conway.Specification.Epoch.md#sec:the-newepoch-transition-system

    [NEWEPOCH-ConstRwds]: Ledger.Conway.Specification.Epoch.Properties.ConstRwds.md#clm:NEWEPOCH-const-rwds

    [Notation]: Notation.md

    [Ouroboros Chronos blog post]: https://iohk.io/en/blog/posts/2021/10/27/ouroboros-chronos-provides-the-first-high-resilience-cryptographic-time-source-based-on-blockchain/

    [POOL]: Ledger.Conway.Specification.Certs.md#auxiliary-pool-transition-system

    @@ -65,13 +76,14 @@
  
    [STS Diagram]: Ledger.Introduction.md#fig:latest-sts-diagram

    [The GOV Transition System]: Ledger.Conway.Specification.Gov.md#the-gov-transition-system

    [The UTXOW Transition System]: Ledger.Conway.Specification.Utxow.md#sec:the-utxow-transition-system

    [thm:ChainGovDepsMatch]: Ledger.Conway.Specification.Chain.Properties.GovDepsMatch.md#thm:ChainGovDepsMatch

    [Time handling on Cardano]: https://docs.cardano.org/about-cardano/explore-more/time

    [Timing of Rewards Payout]: Ledger.Conway.Specification.Rewards.md#sec:timing-of-rewards-payout

    [Transaction Levels]: Ledger.Dijkstra.Specification.Transaction.md#sec:transaction-levels

    [Transaction Structure]: Ledger.Dijkstra.Specification.Transaction.md#sec:transaction-structure

    [Transactions]: Ledger.Dijkstra.Specification.Transaction.md#sec:transactions

    [UTXO]: Ledger.Conway.Specification.Utxo.md#sec:the-utxo-transition-system

    [UTXO-PoV]: Ledger.Conway.Specification.Utxo.Properties.PoV.md#thm:UTXO-PoV

    [UTXO-minspend]: Ledger.Conway.Specification.Utxo.Properties.MinSpend.md#thm:minspend

    [Utxo.Properties.MinSpend]: Ledger.Conway.Specification.Utxo.Properties.MinSpend.md

    [Utxo.Properties.PoV]: Ledger.Conway.Specification.Utxo.Properties.PoV.md

    [UTXOS]: Ledger.Conway.Specification.Utxo.md#sec:the-utxos-transition-rule

build-tools/static/md/mkdocs/mkdocs.yml

-Original file line number
+Diff line change
@@ Expand Up / @@ -118,4 +118,3 @@ extra: @@
         index.md: README.md
         Definitions.md: build-tools/static/md/common/src/Definitions.md
         Notation.md: build-tools/static/md/common/src/Notation.md
-        Properties.md: build-tools/static/md/common/src/Properties.md

build-tools/static/md/nav.yml

-Original file line number
+Diff line change
@@ -1,7 +1,6 @@
     - Home: index.md
     - Preliminaries:
       - Introduction: Ledger.Introduction.md
-      - Properties: Properties.md
       - Notation: Notation.md
     - Core:
       - Introduction: Ledger.Core.Specification.md
@@ Expand Down @@

src/Ledger/Conway/Specification/Certs/Properties.lagda.md

-Original file line number
+Diff line change
@@ Expand Up / @@ -3,11 +3,17 @@ source_branch: master @@
     source_path: src/Ledger/Conway/Specification/Certs/Properties.lagda.md
     ---
+    # Properties Of Certificates {#sec:properties-of-certificates}
+    <!--
     ```agda
     {-# OPTIONS --safe #-}
     module Ledger.Conway.Specification.Certs.Properties where
+    ```
+    -->
+    ```agda
     open import Ledger.Conway.Specification.Certs.Properties.Computational
     open import Ledger.Conway.Specification.Certs.Properties.PoV
     open import Ledger.Conway.Specification.Certs.Properties.PoVLemmas
@@ Expand Down @@

src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md

-Original file line number
+Diff line change
@@ -1,3 +1,10 @@
+    ---
+    source_branch: master
+    source_path: src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md
+    ---
+    ## Theorem: The <span class="AgdaDatatype">CERTS</span> rule preserves value {#thm:CERTS-PoV}
     <!--
     ```agda
@@ Expand Down Expand Up @@
     -->
-    <a id="thm:CERTS-PoV"></a>
-    **Theorem (The `CERTS`{.AgdaOperator} rule preserves value).**
     *Informally*.
     Let `l`{.AgdaBound} be a list of `DCerts`{.AgdaDatatype}, and let `s₁`{.AgdaBound},
@@ Expand Down @@

src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -1,3 +1,10 @@
  
    ---

    source_branch: master

    source_path: src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md

    ---

    ## Theorem: The <span class="AgdaDatatype">CERT</span> rule preserves value {#thm:CERT-PoV}

    <!--

    ```agda

    @@ -66,8 +73,6 @@ module _  ( indexedSumᵛ'-∪ :  {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ C
  
    -->

    **Lemma (The `CERT`{.AgdaOperator} rule preserves value).**

    *Informally*.

    Let `s`{.AgdaBound}, `s'`{.AgdaBound} be `CertStates`{.AgdaRecord} such that

    @@ -83,8 +88,9 @@ some `dcert`{.AgdaBound} : `DCert`{.AgdaDatatype}. Then,
  
        → getCoin s ≡ getCoin s'

    ```

    *Proof*.

    *Proof*.  (Click the "Show more Agda" button to reveal the proof.)

    <!--

    ```agda

      CERT-pov (CERT-deleg (DELEG-delegate {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds)

      CERT-pov (CERT-deleg (DELEG-reg {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds)

    @@ -133,7 +139,7 @@ some `dcert`{.AgdaBound} : `DCert`{.AgdaDatatype}. Then,
  
                             → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )

        where

    ```

    -->

    **Lemma (`PRE-CERT`{.AgdaOperator} rule preserves value).**

    @@ -156,8 +162,9 @@ value of the withdrawals in `Γ`{.AgdaBound}.  In other terms,
  
          → getCoin s ≡ getCoin s' + getCoin (CertEnv.wdrls Γ)

    ```

    *Proof*.

    *Proof*.  (Click the "Show more Agda" button to reveal the proof.)

    <!--

    ```agda

        PRE-CERT-pov  {Γ   = Γ}

    @@ -209,7 +216,7 @@ value of the withdrawals in `Γ`{.AgdaBound}.  In other terms,
  
              getCoin (zeroMap ∪ˡ rewards) + getCoin wdrls

                ∎

    ```

    -->

    **Lemma (`POST-CERT`{.AgdaOperator} rule preserves value).**

src/Ledger/Conway/Specification/Certs/Properties/VoteDelegsVDeleg.lagda.md

-Original file line number
+Diff line change
@@ -1,3 +1,10 @@
+    ---
+    source_branch: master
+    source_path: src/Ledger/Conway/Specification/Certs/Properties/VoteDelegsVDeleg.lagda.md
+    ---
+    ## Claim: <span class="AgdaField">voteDelegs</span> field values are <span class="AgdaDatatype">VDelegs</span> constructed from their keys {#clm:VDelegsInRegDReps}
     <!--
     ```agda
@@ Expand All / @@ -13,9 +20,6 @@ open import Ledger.Conway.Specification.Gov.Actions gs @@
     ```
     -->
-    <a id="thm:VDelegsInRegDReps"></a>
-    **Claim (`voteDelegs`{.AgdaField} by `credVoter`{.AgdaInductiveConstructor} constructor).**
     *Informally*.
     A `CertState`{.AgdaRecord} has a `DState`{.AgdaDatatype}, a `PState`{.AgdaDatatype}, and a
@@ Expand Down @@

src/Ledger/Conway/Specification/Chain/Properties/CredDepsEqualDomRwds.lagda.md

-Original file line number
+Diff line change
@@ -1,3 +1,10 @@
+    ---
+    source_branch: master
+    source_path: src/Ledger/Conway/Specification/Chain/Properties/CredDepsEqualDomRwds.lagda.md
+    ---
+    # Claim: Equality of credential deposits is a <span class="AgdaDatatype">CHAIN</span> invariant {#clm:CredDepsEqualDomRwds-inv}
     <!--
     ```agda
@@ Expand All / @@ -18,8 +25,6 @@ open import Ledger.Conway.Specification.Properties txs abs @@
     ```
     -->
-    **Claim (Equality of credential depsoits is a `CHAIN`{.AgdaOperator} invariant).**
     *Informally*.
     This property concerns two quantities associated with a given
@@ Expand Down @@

src/Ledger/Conway/Specification/Chain/Properties/EpochStep.lagda.md

-Original file line number
+Diff line change
@@ -1,3 +1,10 @@
+    ---
+    source_branch: master
+    source_path: src/Ledger/Conway/Specification/Chain/Properties/EpochStep.lagda.md
+    ---
+    ## Claim: New enact state only if new epoch {#clm:EpochStep}
     <!--
     ```agda
@@ Expand All / @@ -19,8 +26,6 @@ open Block @@
     ```
     -->
-    **Claim (New enact state only if new epoch).**
     *Informally*.
     Let `cs`{.AgdaBound} and `cs'`{.AgdaBound} be `ChainStates`{.AgdaRecord}
@@ Expand Down @@

src/Ledger/Conway/Specification/Chain/Properties/GovDepsMatch.lagda.md

-Original file line number
+Diff line change
@@ -1,3 +1,11 @@
+    ---
+    source_branch: master
+    source_path: src/Ledger/Conway/Specification/Chain/Properties/GovDepsMatch.lagda.md
+    ---
+    ## Theorem: <span class="AgdaFunction">govDepsMatch</span> is a <span class="AgdaDatatype">CHAIN</span> invariant {#thm:ChainGovDepsMatch}
     <!--
     ```agda
@@ Expand Down Expand Up / @@ -36,9 +44,6 @@ module _ @@
     ```
     -->
-    <a id="thm:ChainGovDepsMatch"></a>
-    **Theorem (`govDepsMatch`{.AgdaFunction} is invariant of `CHAIN`{.AgdaOperator} rule)**.
     *Informally*.
     Fix a `Block`{.AgdaRecord} `b`{.AgdaBound}, a `ChainState`{.AgdaRecord} `cs`{.AgdaBound},
@@ Expand Down @@

src/Ledger/Conway/Specification/Chain/Properties/PParamsWellFormed.lagda.md

-Original file line number
+Diff line change
@@ -1,3 +1,10 @@
+    ---
+    source_branch: master
+    source_path: src/Ledger/Conway/Specification/Chain/Properties/PParamsWellFormed.lagda.md
+    ---
+    ## Claim: Well-formedness of <span class="AgdaRecord">PParams</span> is a <span class="AgdaOperator">CHAIN</span> invariant {#clm:pp-wellFormed-inv}
     <!--
     ```agda
@@ Expand All / @@ -16,8 +23,6 @@ open import Ledger.Prelude @@
     ```
     -->
-    **Claim (Well-formedness of `PParams`{.AgdaRecord} is a `CHAIN`{.AgdaOperator} invariant).**
     *Informally*.
     We say the `PParams`{.AgdaRecord} of a chain state are
@@ Expand Down @@

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Refactor documentation of properties #986

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Uh oh!