Make getCoin on CertState total (rewards + deposits)

`HasCoin-CertState.getCoin` previously returned only the rewards balance
(`rewardsBalance ∘ DStateOf`), a misleading partial notion that needed a
paragraph of prose to explain why the deposit pots had to be re-added at the
`LedgerState` level.

Introduce `coinFromRewards = rewardsBalance ∘ DStateOf` and redefine
`getCoin (CertState) = coinFromRewards cs + coinFromDeposits cs` — the honest
total coin a cert state accounts for (rewards plus the three deposit pots).

The cert-level PoV lemmas that genuinely track only the rewards flow now say
`coinFromRewards` explicitly:
- `CERTS-pov` / `ENTITIES-pov` — these preserve/move the rewards balance, not
  the deposits (`CERTS` changes the deposit pots), so the old getCoin-
  preservation statements are false under the new instance and must be
  restated;
- `SUBLEDGERS-certs-pov`, `combined-certs`, and the `R₀`/`R₂` bindings.
Their proof bodies are unchanged: `coinFromRewards` is definitionally the old
instance, so these are mechanical renames.

The `LedgerState` total keeps its explicit four-summand form (UTxO +
`coinFromRewards` + `coinFromDeposits` + gov); the two middle summands are now
exactly `getCoin (CertStateOf s)`.  The obsolete N.B. prose is rewritten.

Typechecks under --safe (Certs, Ledger, Entities/Ledger PoV).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r

Author: claude

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

@@ -356,6 +356,9 @@ doesn't balance.
 coinFromDeposits : CertState → Coin
 coinFromDeposits cs = coinFromDepositTriple (depositTripleOf cs)
 
+coinFromRewards : CertState → Coin
+coinFromRewards = rewardsBalance ∘ DStateOf
+
 module _ (pp : PParams) (certState : CertState) where
 
   updateCertDeposits : List DCert → CertState
@@ -376,7 +379,8 @@ module _ (pp : PParams) (certState : CertState) where
 ```agda
 instance
   HasCoin-CertState : HasCoin CertState
-  HasCoin-CertState .getCoin = rewardsBalance ∘ DStateOf
+  -- Total coin held in a CertState: the rewards balance plus the deposit pots.
+  HasCoin-CertState .getCoin = λ cs → coinFromRewards cs + coinFromDeposits cs
 
   unquoteDecl DecEq-StakePoolParams = derive-DecEq
     ((quote StakePoolParams , DecEq-StakePoolParams) ∷ [])

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

@@ -10,9 +10,10 @@ introduced in [CIP-159-11d][PR-1201].  In the Dijkstra era, `ENTITIES`{.AgdaData
 wraps the inner `CERTS`{.AgdaDatatype} step with per-transaction withdrawal- and
 direct-deposit-handling: withdrawals are applied to the rewards balance *before*
 `CERTS`{.AgdaDatatype}, direct deposits *after*.  The value-flow equation captures
-the net effect of all three components on `getCoin (CertState)`:
+the net effect of all three components on the cert-state rewards balance
+(`coinFromRewards`{.AgdaFunction}; the deposit pots are accounted separately):
 
-    getCoin s + getCoin (DirectDepositsOf Γ) ≡ getCoin s' + getCoin (WithdrawalsOf Γ)
+    coinFromRewards s + getCoin (DirectDepositsOf Γ) ≡ coinFromRewards s' + getCoin (WithdrawalsOf Γ)
 
 Intuitively, the deposits added on the right are matched by the withdrawals removed
 on the left — they "pass through" the rule.
@@ -96,7 +97,7 @@ module ENTITIES-PoV
   -- `Certs.Properties.PoV`; lifted to a module parameter so this PR proves only
   -- the `ENTITIES`/`LEDGER` layer (top-down strategy).
   ( CERTS-pov : ∀ {Γ : CertEnv} {s s' : CertState} {dCerts : List DCert}
-      → Γ ⊢ s ⇀⦇ dCerts ,CERTS⦈ s' → getCoin s ≡ getCoin s' )
+      → Γ ⊢ s ⇀⦇ dCerts ,CERTS⦈ s' → coinFromRewards s ≡ coinFromRewards s' )
   where
   open ApplyToRewards-PoV ∪ˡ-lookup-preserve sum-map-proj₂≡getCoin setToList-Unique public
 ```
@@ -110,7 +111,7 @@ per-batch `NetworkId`{.AgdaFunction} witnesses for `WithdrawalsOf Γ`{.AgdaBound
 `DirectDepositsOf Γ`{.AgdaBound} (produced at the call site by the
 `SUBUTXOW`{.AgdaDatatype} or `UTXOW`{.AgdaDatatype} step).  Then,
 
-    getCoin s + getCoin (DirectDepositsOf Γ) ≡ getCoin s' + getCoin (WithdrawalsOf Γ)
+    coinFromRewards s + getCoin (DirectDepositsOf Γ) ≡ coinFromRewards s' + getCoin (WithdrawalsOf Γ)
 
 **Formally**.
 
@@ -119,7 +120,7 @@ per-batch `NetworkId`{.AgdaFunction} witnesses for `WithdrawalsOf Γ`{.AgdaBound
     → ∀[ a ∈ dom (WithdrawalsOf Γ)    ] NetworkIdOf a ≡ NetworkId
     → ∀[ a ∈ dom (DirectDepositsOf Γ) ] NetworkIdOf a ≡ NetworkId
     → Γ ⊢ s ⇀⦇ dCerts ,ENTITIES⦈ s'
-    → getCoin s + getCoin (DirectDepositsOf Γ) ≡ getCoin s' + getCoin (WithdrawalsOf Γ)
+    → coinFromRewards s + getCoin (DirectDepositsOf Γ) ≡ coinFromRewards s' + getCoin (WithdrawalsOf Γ)
 ```
 
 **Proof**.  Case-split on the single `ENTITIES`{.AgdaInductiveConstructor}
@@ -166,10 +167,9 @@ step then preserves `getCoin`{.AgdaFunction} through the inner closure;
 and the final rewrite folds `applyDirectDeposits`{.AgdaFunction} back
 into the LHS of the goal.
 
-Equivalences used implicitly: under
-`HasCoin-CertState`{.AgdaFunction}, `getCoin (CertState) ≡ getCoin (rewards ∘ DStateOf)`,
-which is why `G r₀`, `G aw`, `G r₁`, and `G (applyDirectDeposits dd r₁)`
-are interchangeable with `getCoin s`, `getCoin <intermediate>`,
-`getCoin <post-CERTS>`, and `getCoin s'` respectively — both sides
-project to the `rewards`{.AgdaField} field, which is exactly what the
-chain manipulates.
+Equivalences used implicitly: `coinFromRewards`{.AgdaFunction} is
+`rewardsBalance ∘ DStateOf`{.AgdaFunction} by definition, which is why `G r₀`, `G aw`,
+`G r₁`, and `G (applyDirectDeposits dd r₁)` are interchangeable with
+`coinFromRewards s`, `coinFromRewards <intermediate>`, `coinFromRewards <post-CERTS>`,
+and `coinFromRewards s'` respectively — both sides project to the `rewards`{.AgdaField}
+field, which is exactly what the chain manipulates.

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

@@ -185,9 +185,10 @@ allColdCreds govSt es =
 4. the governance-action deposits, summed by `coinFromGovDeposit`{.AgdaFunction} over
    `GovActionState.deposit`{.AgdaField} for each action in the current `GovState`{.AgdaRecord}.
 
-N.B. `HasCoin-CertState` counts only the rewards balance (component 2) — its `getCoin` is
-`rewardsBalance ∘ DStateOf`{.AgdaFunction} — so components 3 and 4 must be added at the
-`LedgerState`{.AgdaRecord} level to make the `LEDGER-pov` equation balance against the
+`HasCoin-CertState` sums components 2 and 3 — its `getCoin` is `coinFromRewards cs +
+coinFromDeposits cs`{.AgdaFunction} (the rewards balance plus the three deposit pots) — so
+the `LedgerState`{.AgdaRecord} total adds only component 1 (UTxO coin) and component 4
+(governance-action deposits).  This balances the `LEDGER-pov` equation against the
 `UTXO`{.AgdaDatatype} batch-balance equation, which charges `newCertDeposits`{.AgdaFunction}
 and `govProposalsDeposits`{.AgdaFunction} on the *produced* side.  Cert deposits flow into
 the `DState`/`PState` pots tracked by `coinFromDeposits`{.AgdaFunction}; governance-action
@@ -205,7 +206,7 @@ coinFromGovDeposit = foldr (λ (_ , gaSt) acc → GovActionState.deposit gaSt +
 instance
   HasCoin-LedgerState : HasCoin LedgerState
   HasCoin-LedgerState .getCoin s =  getCoin (UTxOStateOf s)
-                                    + rewardsBalance (DStateOf (CertStateOf s))
+                                    + coinFromRewards (CertStateOf s)
                                     + coinFromDeposits (CertStateOf s)
                                     + coinFromGovDeposit (GovStateOf s)
 ```

src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md

@@ -18,13 +18,16 @@ then `getCoin s ≡ getCoin s'`.
 Recall (from `Ledger.lagda.md`) that `getCoin (LedgerState)` is
 
     getCoin (UTxOStateOf s)
-    + rewardsBalance (DStateOf (CertStateOf s))
+    + coinFromRewards (CertStateOf s)
     + coinFromDeposits (CertStateOf s)
     + coinFromGovDeposit (GovStateOf s)
 
-This is the sum of UTxO coin, rewards balance, the deposits from `DState`, `PState`,
-and `GState` (`coinFromDeposits`{.AgdaFunction}), and the governance-action deposits
-(`coinFromGovDeposit`{.AgdaFunction}).
+This is the sum of UTxO coin, the cert-state rewards balance
+(`coinFromRewards`{.AgdaFunction}), the deposits from `DState`, `PState`, and `GState`
+(`coinFromDeposits`{.AgdaFunction}), and the governance-action deposits
+(`coinFromGovDeposit`{.AgdaFunction}).  Note `getCoin (CertState)` itself now sums the
+rewards balance *and* the deposit pots (`coinFromRewards + coinFromDeposits`), so the
+two middle summands are exactly `getCoin (CertStateOf s)`.
 
 > **Status — complete.** `LEDGER-pov` typechecks end-to-end under `--safe` (no
 > postulates or holes).  Following the top-down plan, this module proves only the
@@ -206,7 +209,7 @@ module LEDGER-PoV
   -- Certs-PoV stubs (discharged later by #1210).  These were the `Certs.Properties.PoV`
   -- provider lemmas; under the top-down plan they are module parameters here.
   ( CERTS-pov : ∀ {Γ : CertEnv} {s s' : CertState} {dCerts : List DCert}
-      → Γ ⊢ s ⇀⦇ dCerts ,CERTS⦈ s' → getCoin s ≡ getCoin s' )
+      → Γ ⊢ s ⇀⦇ dCerts ,CERTS⦈ s' → coinFromRewards s ≡ coinFromRewards s' )
   -- Closed-form cert-deposit coin equation: the post-`CERTS` `CertState` has the same
   -- `coinFromDeposits` as the closed-form `updateCertDeposits` applied to the initial
   -- state and the cert list.  (#1210 discharges this using the ledger-level
@@ -422,8 +425,8 @@ deposits.
   SUBLEDGERS-certs-pov : ∀ {Γ : SubLedgerEnv} {s₀ s₁ : LedgerState} {stxs : List SubLevelTx}
     → SubLedgerEnv.isTopLevelValid Γ ≡ true
     → Γ ⊢ s₀ ⇀⦇ stxs ,SUBLEDGERS⦈ s₁
-    → getCoin (CertStateOf s₀) + sum (map ddwl stxs)
-      ≡ getCoin (CertStateOf s₁) + sum (map wdrwl stxs)
+    → coinFromRewards (CertStateOf s₀) + sum (map ddwl stxs)
+      ≡ coinFromRewards (CertStateOf s₁) + sum (map wdrwl stxs)
 
   SUBLEDGERS-certs-pov _ (BS-base Id-nop) = refl
 
@@ -433,28 +436,28 @@ deposits.
   SUBLEDGERS-certs-pov {Γ} isV (BS-ind {s = s₀} {s' = s₁} {sigs} {s'' = sₙ}
     (SUBLEDGER-V {stx = stx} (isV' , subutxowStep , entitiesStep , _)) rest) =
     begin
-      getCoin (CertStateOf s₀) + (getCoin (DirectDepositsOf stx) + sum (map ddwl sigs))
-        ≡⟨ sym (+-assoc (getCoin (CertStateOf s₀))
+      coinFromRewards (CertStateOf s₀) + (getCoin (DirectDepositsOf stx) + sum (map ddwl sigs))
+        ≡⟨ sym (+-assoc (coinFromRewards (CertStateOf s₀))
                         (getCoin (DirectDepositsOf stx))
                         (sum (map ddwl sigs))) ⟩
-      (getCoin (CertStateOf s₀) + getCoin (DirectDepositsOf stx)) + sum (map ddwl sigs)
+      (coinFromRewards (CertStateOf s₀) + getCoin (DirectDepositsOf stx)) + sum (map ddwl sigs)
         ≡⟨ cong (_+ sum (map ddwl sigs))
                 (ENTITIES-pov wd-netId dd-netId entitiesStep) ⟩
-      (getCoin (CertStateOf s₁) + getCoin (WithdrawalsOf stx)) + sum (map ddwl sigs)
-        ≡⟨ swap-right (getCoin (CertStateOf s₁))
+      (coinFromRewards (CertStateOf s₁) + getCoin (WithdrawalsOf stx)) + sum (map ddwl sigs)
+        ≡⟨ swap-right (coinFromRewards (CertStateOf s₁))
                       (getCoin (WithdrawalsOf stx))
                       (sum (map ddwl sigs)) ⟩
-      (getCoin (CertStateOf s₁) + sum (map ddwl sigs)) + getCoin (WithdrawalsOf stx)
+      (coinFromRewards (CertStateOf s₁) + sum (map ddwl sigs)) + getCoin (WithdrawalsOf stx)
         ≡⟨ cong (_+ getCoin (WithdrawalsOf stx)) ih ⟩
-      (getCoin (CertStateOf sₙ) + sum (map wdrwl sigs)) + getCoin (WithdrawalsOf stx)
-        ≡⟨ swap-right (getCoin (CertStateOf sₙ))
+      (coinFromRewards (CertStateOf sₙ) + sum (map wdrwl sigs)) + getCoin (WithdrawalsOf stx)
+        ≡⟨ swap-right (coinFromRewards (CertStateOf sₙ))
                       (sum (map wdrwl sigs))
                       (getCoin (WithdrawalsOf stx)) ⟩
-      (getCoin (CertStateOf sₙ) + getCoin (WithdrawalsOf stx)) + sum (map wdrwl sigs)
-        ≡⟨ +-assoc (getCoin (CertStateOf sₙ))
+      (coinFromRewards (CertStateOf sₙ) + getCoin (WithdrawalsOf stx)) + sum (map wdrwl sigs)
+        ≡⟨ +-assoc (coinFromRewards (CertStateOf sₙ))
                    (getCoin (WithdrawalsOf stx))
                    (sum (map wdrwl sigs)) ⟩
-      getCoin (CertStateOf sₙ) + (getCoin (WithdrawalsOf stx) + sum (map wdrwl sigs))
+      coinFromRewards (CertStateOf sₙ) + (getCoin (WithdrawalsOf stx) + sum (map wdrwl sigs))
         ∎
     where
     -- The two NetworkId witnesses, extracted from the SUBUTXOW step.
@@ -477,8 +480,8 @@ deposits.
     wd-netId = proj₁ netIds
     dd-netId = proj₂ netIds
 
-    ih : getCoin (CertStateOf s₁) + sum (map ddwl sigs)
-         ≡ getCoin (CertStateOf sₙ) + sum (map wdrwl sigs)
+    ih : coinFromRewards (CertStateOf s₁) + sum (map ddwl sigs)
+         ≡ coinFromRewards (CertStateOf sₙ) + sum (map wdrwl sigs)
     ih = SUBLEDGERS-certs-pov isV rest
 ```
 
@@ -557,15 +560,15 @@ are unchanged.  Only the `UTXOW` step affects `getCoin`, and it preserves it via
 
 ```agda
   LEDGER-pov {Γ} {s} (LEDGER-I (invalid , _ , utxoStep)) =
-    cong (λ u → u + getCoin (CertStateOf s) + coinFromDeposits (CertStateOf s)
+    cong (λ u → u + coinFromRewards (CertStateOf s) + coinFromDeposits (CertStateOf s)
                   + coinFromGovDeposit (GovStateOf s))
          (utxow-pov-invalid utxoStep invalid)
 ```
 
 ### `LEDGER-V` case (valid transaction)
 
 The proof is a single equational chain over `LedgerState` coin totals.  Setting
-`U = getCoin (UTxOState)`, `R = rewardsBalance`, `D = coinFromDeposits`,
+`U = getCoin (UTxOState)`, `R = coinFromRewards`, `D = coinFromDeposits`,
 `G = coinFromGovDeposit`, and `allDirectDeps` / `allWdrls` for the top-level and
 sub-level totals of direct deposits and withdrawals respectively, the goal
 `getCoin s ≡ getCoin s'` is
@@ -626,8 +629,8 @@ are stated explicitly to keep the chain readable.
       D₂ = coinFromDeposits cs₂
 
       R₀ R₂ : Coin
-      R₀ = rewardsBalance (DStateOf (CertStateOf s))
-      R₂ = rewardsBalance (DStateOf cs₂)
+      R₀ = coinFromRewards (CertStateOf s)
+      R₂ = coinFromRewards cs₂
 
       -- Governance-deposit summands of the LedgerState totals.  G₀ is the initial
       -- GovState's deposit; G' is the final state's (`rmOrphanDRepVotes cs₂ govSt₂`),
@@ -708,27 +711,27 @@ The "combined" `ENTITIES-pov` invocation: pre-batch `certState` + all direct dep
 key step where direct deposits cancel between the UTxO and CertState sides of the ledger.
 
 ```agda
-      combined-certs : getCoin (CertStateOf s) + allDirectDeps
-                     ≡ getCoin cs₂ + allWdrls
+      combined-certs : coinFromRewards (CertStateOf s) + allDirectDeps
+                     ≡ coinFromRewards cs₂ + allWdrls
       combined-certs =
         begin
-          getCoin (CertStateOf s) + allDirectDeps
-            ≡⟨ cong (getCoin (CertStateOf s) +_)
+          coinFromRewards (CertStateOf s) + allDirectDeps
+            ≡⟨ cong (coinFromRewards (CertStateOf s) +_)
                     (+-comm (getCoin (DirectDepositsOf tx)) subDirectDepsCoin) ⟩
-          getCoin (CertStateOf s) + (subDirectDepsCoin + getCoin (DirectDepositsOf tx))
-            ≡⟨ sym (+-assoc (getCoin (CertStateOf s))
+          coinFromRewards (CertStateOf s) + (subDirectDepsCoin + getCoin (DirectDepositsOf tx))
+            ≡⟨ sym (+-assoc (coinFromRewards (CertStateOf s))
                             subDirectDepsCoin
                             (getCoin (DirectDepositsOf tx))) ⟩
-          getCoin (CertStateOf s) + subDirectDepsCoin + getCoin (DirectDepositsOf tx)
+          coinFromRewards (CertStateOf s) + subDirectDepsCoin + getCoin (DirectDepositsOf tx)
             ≡⟨ cong (_+ getCoin (DirectDepositsOf tx))
                     (SUBLEDGERS-certs-pov valid subStep) ⟩
-          getCoin cs₁ + subWdrlsCoin + getCoin (DirectDepositsOf tx)
-            ≡⟨ swap-right (getCoin cs₁) subWdrlsCoin (getCoin (DirectDepositsOf tx)) ⟩
-          getCoin cs₁ + getCoin (DirectDepositsOf tx) + subWdrlsCoin
+          coinFromRewards cs₁ + subWdrlsCoin + getCoin (DirectDepositsOf tx)
+            ≡⟨ swap-right (coinFromRewards cs₁) subWdrlsCoin (getCoin (DirectDepositsOf tx)) ⟩
+          coinFromRewards cs₁ + getCoin (DirectDepositsOf tx) + subWdrlsCoin
             ≡⟨ cong (_+ subWdrlsCoin) (ENTITIES-pov top-wd-netId top-dd-netId entitiesStep) ⟩
-          getCoin cs₂ + getCoin (WithdrawalsOf tx) + subWdrlsCoin
-            ≡⟨ +-assoc (getCoin cs₂) (getCoin (WithdrawalsOf tx)) subWdrlsCoin ⟩
-          getCoin cs₂ + (getCoin (WithdrawalsOf tx) + subWdrlsCoin)
+          coinFromRewards cs₂ + getCoin (WithdrawalsOf tx) + subWdrlsCoin
+            ≡⟨ +-assoc (coinFromRewards cs₂) (getCoin (WithdrawalsOf tx)) subWdrlsCoin ⟩
+          coinFromRewards cs₂ + (getCoin (WithdrawalsOf tx) + subWdrlsCoin)
             ∎
 ```