[Dijkstra] Restate CERTS PoV contract at full accounting; derive the batch bridge

Per review: the Certs-level parameters now state the complete value
accounting of a CERTS run, and the ENTITIES PoV module surfaces it
per transaction:

- CERTS-rewards-pov (rewards preserved), CERTS-deposits-pov (closed-form
  deposit accounting D + new ≡ D' + refunds), CERTS-deposits-registered
  (invariant preservation), CERTS-new-thread (newCertDeposits split at a
  run boundary), refundCertDeposits-++ (fold algebra).
- Entities.Properties.PoV adds SUBENTITIES/ENTITIES-deposits-pov,
  -deposits-registered, SUBENTITIES-new-thread (all definitional
  transports of the CERTS facts), and the combined full-CertState-coin
  identities SUBENTITIES/ENTITIES-pov-total:
  coin in + direct deposits + new deposits ≡
  coin out + withdrawals + refunds.
- Ledger.Properties.PoV now *derives* the batch-wide deposit accounting
  (SUBLEDGERS-deposits, telescoping per-step closed forms across the
  batch, with SUBLEDGERS-registered threading the invariant and
  refund-concatMap recombining refunds); the batch-cert-deposits-bridge
  parameter is gone.  Its premises mentioned SUBLEDGERS, so it was not
  statable at the Certs level anyway.

Restating the per-run accounting exposed a genuine soundness condition:
POOL-reg adds its deposit with a left-biased union, so at a state with a
stale pot entry for an unregistered pool, registering that pool destroys
the deposit the batch balance charges, and value preservation is false.
New PoolDepositsRegistered invariant in Certs (every pool-deposit entry
belongs to a registered pool; preserved by CERTS, holds on-chain by
construction); LEDGER-pov now takes it as a hypothesis on the initial
state.  The old bridge parameter silently baked in the same assumption
and would have been undischargeable as stated.

Also apply the review's prose policy: status/roadmap/issue-number prose
moved from module documentation to the PR description; explanations
deduplicated across modules (stated once, referenced elsewhere).

Final touches:

+ general improvements
+ remove unnecessary CHANGELOG entry
+ add mkdocs nav entries

AI-assisted: Claude Fable 5 (Anthropic)

Author: williamdemeo

CHANGELOG.md

@@ -4,12 +4,9 @@
 
 ### WIP
 
-- Prove preservation of value for the `LEDGER` rule (`LEDGER-pov`, #1187), in new module
-  `Ledger.Properties.PoV`.  Supporting modules: `Entities.Properties.PoV`
-  (`ENTITIES-pov`, `SUBENTITIES-pov`) and `Entities.Properties.ApplyToRewardsPoV`
-  (`applyWithdrawals-pov`, `applyDirectDeposits-pov`).  The supporting UTxO, Certs, and
-  Gov facts are module parameters, to be discharged by #1186, #1210, and a future
-  `Gov.Properties.PoV`.
+- Add `PoolDepositsRegistered` (every pool-deposit entry belongs to a registered
+  pool) to `Certs`; the deposit accounting genuinely fails without it, since
+  `POOL-reg` adds its deposit with a left-biased union.
 - Count governance-action deposits in `getCoin LedgerState` via a new
   `coinFromGovDeposit : GovState → Coin` (sum of `GovActionState.deposit`).  These
   deposits live in `GovActionState.deposit`, not `GState.deposits`, so the three

build-tools/static/mkdocs/mkdocs.yml

@@ -241,7 +241,9 @@ nav:
     - Entities/:
       - Properties: Ledger.Dijkstra.Specification.Entities.Properties.md
       - Properties/:
+        - ApplyToRewardsPoV: Ledger.Dijkstra.Specification.Entities.Properties.ApplyToRewardsPoV.md
         - Computational: Ledger.Dijkstra.Specification.Entities.Properties.Computational.md
+        - PoV: Ledger.Dijkstra.Specification.Entities.Properties.PoV.md
     - Epoch: Ledger.Dijkstra.Specification.Epoch.md
     - Epoch/:
       - Properties: Ledger.Dijkstra.Specification.Epoch.Properties.md
@@ -260,6 +262,7 @@ nav:
       - Properties: Ledger.Dijkstra.Specification.Ledger.Properties.md
       - Properties/:
         - Computational: Ledger.Dijkstra.Specification.Ledger.Properties.Computational.md
+        - PoV: Ledger.Dijkstra.Specification.Ledger.Properties.PoV.md
     - PoolReap: Ledger.Dijkstra.Specification.PoolReap.md
     - PoolReap/:
       - Properties: Ledger.Dijkstra.Specification.PoolReap.Properties.md

src/Ledger/Dijkstra/Specification/Certs.lagda.md

@@ -380,6 +380,18 @@ coinFromDeposits cs =
   getCoin (DepositsOf (DStateOf cs)) + getCoin (DepositsOf (PStateOf cs)) + getCoin (DepositsOf (GStateOf cs))
 ```
 
+A `CertState`{.AgdaRecord} is *pool-deposit registered* when every entry of the pool
+deposit pot belongs to a registered pool.  Deposit accounting relies on this:
+`POOL-reg`{.AgdaInductiveConstructor} adds the pool deposit with a left-biased union,
+so a stale pot entry for an unregistered pool would silently swallow the added
+deposit.  The property is preserved by `CERTS`{.AgdaDatatype} (both maps gain exactly
+the new pool's key, and no rule removes a pool without its deposit).
+
+```agda
+PoolDepositsRegistered : CertState → Type
+PoolDepositsRegistered cs = dom (DepositsOf (PStateOf cs)) ⊆ dom (PoolsOf cs)
+```
+
 <!--
 ```agda
 instance

src/Ledger/Dijkstra/Specification/Entities.lagda.md

@@ -22,7 +22,7 @@ open PParams
 ```
 -->
 
-# Auxiliary Types and Functions
+## Auxiliary Types and Functions
 
 ```agda
 record EntitiesEnv : Type where
@@ -89,7 +89,7 @@ applyWithdrawals : Withdrawals → Rewards → Rewards
 applyWithdrawals = applyToRewards _∸_
 ```
 
-# `ENTITIES`{.AgdaDatatype} Transition System
+## `ENTITIES`{.AgdaDatatype} Transition System
 
 In Dijkstra, the new `ENTITIES`{.AgdaDatatype} rule subsumes the
 pre-Dijkstra `CERTS`{.AgdaDatatype} rule. This rule in addition to
@@ -101,7 +101,7 @@ and `balanceIntervals`. Direct deposits represent value that flows
 from the transaction into account addresses. Balance intervals enable
 transactions to assert predicates about account balances.
 
-## Withdrawals 
+### Withdrawals
 
 The `ENTITIES`{.AgdaDatatype} rule applies withdrawals, via
 `applyWithdrawals`{.AgdaFunction} before certificate evaluation.  In
@@ -111,7 +111,7 @@ rule (via `isLegacyMode`{.AgdaFunction}, defined in the
 `Utxow`{.AgdaModule} module) and provided here through the
 `legacyMode`{.AgdaField} field of `EntitiesEnv`{.AgdaRecord}.
 
-## Direct Deposits
+### Direct Deposits
 
 The `ENTITIES`{.AgdaDatatype} rule applies direct deposits to the
 `CertState`{.AgdaRecord} after  `CERTS`{.AgdaDatatype}.
@@ -168,9 +168,7 @@ data _⊢_⇀⦇_,SUBENTITIES⦈_ : SubEntitiesEnv → CertState → SubLevelTx
     ∙ directDepositsCredentials ⊆ dom rewards'
       ────────────────────────────────
       ⟦ e , pp , cc , rewards₀ ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , rewards , depositsᵈ ⟧ , pState , ⟦ dReps , ccHotKeys , depositsᵍ ⟧ ⟧ ⇀⦇ txSub ,SUBENTITIES⦈ ⟦ ⟦ voteDelegs' , stakeDelegs' , applyDirectDeposits directDeposits rewards' , depositsᵈ' ⟧ , pState' , gState' ⟧
-```
 
-```agda
 data _⊢_⇀⦇_,ENTITIES⦈_ : EntitiesEnv → CertState → TopLevelTx → CertState → Type where
 
   ENTITIES :

src/Ledger/Dijkstra/Specification/Entities/Properties/ApplyToRewardsPoV.lagda.md

@@ -3,22 +3,22 @@ source_branch: master
 source_path: src/Ledger/Dijkstra/Specification/Entities/Properties/ApplyToRewardsPoV.lagda.md
 ---
 
-## `applyToRewards` Preservation of Value {#sec:apply-to-rewards-pov}
+# <span class="AgdaFunction">applyToRewards</span> Preservation of Value {#sec:apply-to-rewards-pov}
 
 This module proves preservation of value for the two specializations of
 `applyToRewards`{.AgdaFunction} used inside the `ENTITIES`{.AgdaDatatype} rule.
 
 +  `applyWithdrawals-pov`{.AgdaFunction}.
 
-   `applyWithdrawals`{.AgdaFunction} *decreases* the total rewards balance by exactly
+   `applyWithdrawals`{.AgdaFunction} decreases the total rewards balance by exactly
    the sum of withdrawal amounts.  Truncating subtraction (`_∸_`) means the per-step
    lemma requires `amt ≤ bal`, and the fold induction requires a
    `Unique`{.AgdaDatatype} witness on the stake-projected withdrawal list so that no
    already-reduced balance is revisited.
 
 +  `applyDirectDeposits-pov`{.AgdaFunction}.
 
-   `applyDirectDeposits`{.AgdaFunction} *increases* the total rewards balance by
+   `applyDirectDeposits`{.AgdaFunction} increases the total rewards balance by
    exactly the sum of direct-deposit amounts.  Because `_+_` is total and
    commutative, revisiting a credential is harmless, so neither the
    `NetworkId`{.AgdaFunction} witness nor the `Unique`{.AgdaDatatype} premise is
@@ -27,7 +27,7 @@ This module proves preservation of value for the two specializations of
 Both lemmas share a common backbone: a per-step result about
 `applyOne`{.AgdaFunction} (the lambda body of `applyToRewards`{.AgdaFunction})
 together with a `foldl`-induction lemma over `setToList (m ˢ)`.  They are consumed
-directly by `ENTITIES-pov`{.AgdaFunction} in `Entities.Properties.PoV`.
+directly by `ENTITIES-pov`{.AgdaFunction} in `Entities.Properties.PoV`{.AgdaModule}.
 
 <!--
 ```agda
@@ -60,7 +60,7 @@ open ≡-Reasoning
 ```
 -->
 
-### Shared helpers
+## Shared helpers
 
 ```agda
 getCoin-∪ˡ-overwrite : (acc : Rewards) (c : Credential) (v : Coin)
@@ -139,11 +139,10 @@ split-by-lookup acc c bal lookup-eq =
 ```
 -->
 
-### The `ApplyToRewards-PoV` module
+## The <span class="AgdaModule">ApplyToRewards-PoV</span> module
 
 The three assumed identities below are the same set/map identities used by the Conway
-PoV proofs; they are stated as module parameters here, to be discharged in a
-follow-up against the `agda-sets` library.
+PoV proofs; they are stated as module parameters here.
 
 +  `∪ˡ-lookup-preserve`: lookup in a left-biased union with a singleton at `c` agrees
    with lookup in the right map for any key `c' ≠ c`.
@@ -223,8 +222,8 @@ The fold invariant tracks three things through the induction.
 3.  No credential is revisited (the `Unique`{.AgdaDatatype} witness on the
     stake-projected list).
 
-Uniqueness is essential here precisely because `applyOne _∸_` *modifies* the balance
-at the targeted credential — without it, a re-visit could attempt to subtract from an
+Uniqueness is essential here precisely because `applyOne _∸_` modifies the balance
+at the targeted credential; without it, a re-visit could attempt to subtract from an
 already-reduced balance for which the caller's original `amt ≤ bal` bound no longer
 holds.
 
@@ -291,7 +290,7 @@ holds.
 ```
 -->
 
-### `applyWithdrawals-pov`
+#### `applyWithdrawals-pov`
 
 ```agda
   applyWithdrawals-pov : (wdrls : Withdrawals) (rwds : Rewards)
@@ -328,9 +327,9 @@ holds.
 ```
 -->
 
-## Direct-deposit preservation of value
+### Direct-deposit preservation of value
 
-### `applyOne-pov-add` (one direct-deposit step increases `getCoin` by `amt`)
+#### `applyOne-pov-add` (one direct-deposit step increases `getCoin` by `amt`)
 
 For addition, no `amt ≤ bal` premise is needed (the operation is total),
 and the per-step equation is `getCoin (...) ≡ getCoin acc + amt`
@@ -361,10 +360,10 @@ balance.
 ```
 -->
 
-### `foldl-applyOne-pov-add` (fold induction, no `Unique` needed)
+#### `foldl-applyOne-pov-add` (fold induction, no `Unique` needed)
 
 Unlike the withdrawal version, the additive fold induction needs only
-domain preservation — the `Unique`{.AgdaDatatype} witness drops out.
+domain preservation; the `Unique`{.AgdaDatatype} witness drops out.
 The reason: `applyOne _+_` modifies the balance at the targeted
 credential, but since the per-step lemma `applyOne-pov-add` is
 unconditional on the prior balance and `_+_` is commutative, revisiting
@@ -406,7 +405,7 @@ the same credential simply accumulates additions correctly.
 ```
 -->
 
-### `applyDirectDeposits-pov`
+#### `applyDirectDeposits-pov`
 
 Note the slimmed-down signature relative to `applyWithdrawals-pov`: no
 `NetworkId`{.AgdaFunction} premise (none is needed), no