[Dijkstra] CIP-159: Update CERTS PoV proofs for new DirectDeposits type

williamdemeo · williamdemeo · commit 2a6a3dd11a18 · 2026-05-19T15:37:16.000-06:00
Following the merge of CIP-159 PR #1197 (DirectDeposits keyed by RewardAddress; applyDirectDeposits and applyWithdrawals refactored through a shared applyToRewards fold) and the agda-sets cleanup PR #1196 (Conway Equivalence.Map utilities moved into Ledger.Prelude), this commit updates the Dijkstra CERTS preservation-of-value proofs to compile against the new APIs. Main changes: + Rename `ApplyWithdrawals-PoV` sub-module to `ApplyToRewards-PoV`, since it now houses lemmas for both withdrawals and direct deposits. + Add `getCoin-∪ˡ-overwrite` bridge lemma: `getCoin (❴ c , v ❵ ∪ˡ acc) ≡ v + getCoin (acc ∣ ❴ c ❵ ᶜ)`. Encapsulates the listing-vs-replacement reconciliation between the new `❴ k , v ❵ ∪ˡ acc` form (used by `applyToRewards`) and the equivalent complement-restricted form used by the existing decomposition reasoning. + Factor `split-by-lookup` as a top-level lemma decomposing `getCoin acc` along a known lookup result. Used by both `applyOne-pov` (subtraction) and the new `applyOne-pov-add` (addition). + Add the additive parallel: `applyOne-pov-add`, `foldl-applyOne-pov-add`, and `applyDirectDeposits-pov`. Mirrors the existing withdrawal chain, sharing `getCoin-∪ˡ-overwrite` and `split-by-lookup`. + Strengthen the `setToList-Unique` module parameter with a `NetworkId` premise on the map's domain (the assumption no longer conflates withdrawals-specifically with general `RewardAddress ⇀ Coin` maps). + Replace the `∪ˡ-res-lookup-preserve` module parameter (which carried a no-longer-needed complement restriction on the right operand) with `∪ˡ-lookup-preserve`, stated against the new `❴ c , v ❵ ∪ˡ m` form. + Add a small top-level helper `∈-dom⇒¬lookup-nothing` to discharge the defensive `nothing` case of `foldl-applyOne-pov-add`. + Update `POST-CERT-pov` to use the new `applyDirectDeposits-pov`; the proof is `sym (applyDirectDeposits-pov ...)`. The CERT-post step's own `mapˢ stake (dom dd) ⊆ dom rewards` premise is extracted from the pattern rather than threaded as a separate parameter, since the pre-CERT* state's `dom rewards` is not preserved across `CERT` trace steps (in particular by `DELEG-dereg`). + Update `sts-pov` and `CERTS-pov` signatures accordingly: add the `DirectDeposits`-`NetworkId` premise, drop the membership-of-deposits premise. The proofs now typecheck on top of master.
diff --git a/src/Ledger/Dijkstra/Specification/Certs/Properties/ApplyWithdrawalsPoV.lagda.md b/src/Ledger/Dijkstra/Specification/Certs/Properties/ApplyWithdrawalsPoV.lagda.md
@@ -58,6 +58,7 @@ open import Relation.Binary using (IsEquivalence)
 open import Data.Nat.Properties using (n≤0⇒n≡0)
 open RewardAddress
 open Any
+open ≡-Reasoning
 
 private variable
   A : Type
@@ -98,7 +99,6 @@ getCoin-∪ˡ-overwrite acc c v =
     v + getCoin (acc ∣ ❴ c ❵ ᶜ)
       ∎
   where
-  open ≡-Reasoning
   open Equivalence
   module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
   -- `res-decomp ❴ c , v ❵ᵐ acc` proves
@@ -115,7 +115,10 @@ getCoin-∪ˡ-overwrite acc c v =
   -- (`Map.agda`: `(x , _) ≡ᵐ (y , _) = x ≡ᵉ y`), so `res-comp-cong`
   -- (from `Axiom.Set.Rel`) lifts straight to the Map level.
   restrict-cong' : (❴ c , v ❵ᵐ ∪ˡ (acc ∣ dom (❴ c , v ❵ᵐ ˢ) ᶜ)) ˢ ≡ᵉ (❴ c , v ❵ᵐ ∪ˡ (acc ∣ ❴ c ❵ ᶜ)) ˢ
-  restrict-cong' = ∪ˡ-cong (≡ᵉ.refl {x = ❴ c , v ❵ᵐ ˢ}) (res-comp-cong dom-single≡single)
+  restrict-cong' =
+    ∪ˡ-cong {m = ❴ c , v ❵ᵐ} {m' = (acc ∣ dom (❴ c , v ❵ᵐ ˢ) ᶜ)}{m'' = ❴ c , v ❵ᵐ} {m''' = (acc ∣ ❴ c ❵ ᶜ)}
+      (≡ᵉ.refl {x = ❴ c , v ❵ᵐ ˢ}) (res-comp-cong dom-single≡single)
+--  ∪ˡ-cong : ∀ {m m' m'' m''' : Map A B} → m ≡ᵐ m'' → m' ≡ᵐ m''' → (m ∪ˡ m') ≡ᵐ (m'' ∪ˡ m''')
 
   bridge : (❴ c , v ❵ ∪ˡ acc) ˢ ≡ᵉ (❴ c , v ❵ ∪ˡ (acc ∣ ❴ c ❵ ᶜ)) ˢ
   bridge = ≡ᵉ.trans (res-decomp ❴ c , v ❵ᵐ acc) restrict-cong'
@@ -125,63 +128,80 @@ getCoin-∪ˡ-overwrite acc c v =
 ```
 -->
 
-### Single-step Lemma: `applyOne` decreases `getCoin` by `amt`
+### `split-by-lookup`: decompose `getCoin acc` along a known lookup result
 
-When `stake addr ∈ dom acc` and `amt ≤ bal` (where `bal` is the current balance),
-applying a single withdrawal decreases the total by exactly `amt`.
+When `lookupᵐ? acc c ≡ just bal`, we can split `getCoin acc` into the
+contribution of `c` (which is `bal`) plus the contribution of everything
+else (`acc ∣ ❴ c ❵ ᶜ`).  This is the prefix shared by both `applyOne-pov`
+and `applyOne-pov-add`; factoring it out avoids duplicating the proof.
 
 ```agda
-applyOne-pov :
-  (acc : Rewards) (addr : RewardAddress) (amt bal : Coin)
-  → lookupᵐ? acc (stake addr) ≡ just bal
-  → amt ≤ bal
-  → getCoin acc ≡ getCoin (❴ stake addr , bal ∸ amt ❵ ∪ˡ acc) + amt
+split-by-lookup : (acc : Rewards) (c : Credential) (bal : Coin)
+  → lookupᵐ? acc c ≡ just bal
+  → getCoin acc ≡ getCoin (acc ∣ ❴ c ❵ ᶜ) + bal
 ```
 
 <!--
 ```agda
-applyOne-pov acc addr amt bal lookup-eq amt≤bal =
+split-by-lookup acc c bal lookup-eq =
   begin
     getCoin acc
       ≡˘⟨ ≡ᵉ-getCoin decomp acc
-      ( ≡ᵉ.trans (disjoint-∪ˡ-∪ (disjoint-sym res-ex-disjoint))
-                 ( ≡ᵉ.trans ∪-sym (res-ex-∪ Dec-∈-singleton)) ) ⟩
+            ( ≡ᵉ.trans (disjoint-∪ˡ-∪ (disjoint-sym res-ex-disjoint))
+                       ( ≡ᵉ.trans ∪-sym (res-ex-∪ Dec-∈-singleton)) ) ⟩
     getCoin decomp
       ≡⟨ indexedSumᵛ'-∪ (acc ∣ ❴ c ❵ ᶜ) (acc ∣ ❴ c ❵) (disjoint-sym res-ex-disjoint) ⟩
     getCoin (acc ∣ ❴ c ❵ ᶜ) + getCoin (acc ∣ ❴ c ❵)
       ≡⟨ cong (getCoin (acc ∣ ❴ c ❵ ᶜ) +_) acc∣c≡bal ⟩
     getCoin (acc ∣ ❴ c ❵ ᶜ) + bal
-      ≡⟨ cong (getCoin (acc ∣ ❴ c ❵ ᶜ) +_) (sym (m∸n+n≡m amt≤bal)) ⟩
-    getCoin (acc ∣ ❴ c ❵ ᶜ) + (bal ∸ amt + amt)
-      ≡⟨ trans (sym (+-assoc (getCoin (acc ∣ ❴ c ❵ ᶜ)) (bal ∸ amt) amt))
-               (cong (_+ amt) (+-comm (getCoin (acc ∣ ❴ c ❵ ᶜ)) (bal ∸ amt))) ⟩
-    (bal ∸ amt) + getCoin (acc ∣ ❴ c ❵ ᶜ) + amt
-      ≡˘⟨ cong (_+ amt) (getCoin-∪ˡ-overwrite acc c (bal ∸ amt)) ⟩
-    getCoin (❴ c , bal ∸ amt ❵ ∪ˡ acc) + amt
       ∎
   where
   module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
-  open ≡-Reasoning
   open Equivalence
-
-  c : Credential
-  c = stake addr
-
   decomp : Credential ⇀ Coin
   decomp = (acc ∣ ❴ c ❵ ᶜ) ∪ˡ (acc ∣ ❴ c ❵)
-
   c∈acc : (c , bal) ∈ acc ˢ
   c∈acc with c ∈? dom (acc ˢ)
   ... | yes c∈dom =
     subst (λ v → (c , v) ∈ acc ˢ) (just-injective lookup-eq) (lookupᵐ-∈ acc c c∈dom)
   ... | no c∉dom = case lookup-eq of λ ()
-
   acc∣c≡bal : getCoin (acc ∣ ❴ c ❵) ≡ bal
   acc∣c≡bal =
     trans (getCoin-cong (acc ∣ ❴ c ❵) ❴ (c , bal) ❵ (res-singleton' {m = acc} c∈acc))
           getCoin-singleton
+```
+-->
 
-  -- `c∉dom-compl` and `disj-doms` removed: the bridge lemma encapsulates them.
+
+
+### Single-step Lemma: `applyOne` decreases `getCoin` by `amt`
+
+When `stake addr ∈ dom acc` and `amt ≤ bal` (where `bal` is the current balance),
+applying a single withdrawal decreases the total by exactly `amt`.
+
+```agda
+applyOne-pov :
+  (acc : Rewards) (addr : RewardAddress) (amt bal : Coin)
+  → lookupᵐ? acc (stake addr) ≡ just bal
+  → amt ≤ bal
+  → getCoin acc ≡ getCoin (❴ stake addr , bal ∸ amt ❵ ∪ˡ acc) + amt
+```
+
+<!--
+```agda
+applyOne-pov acc addr amt bal lookup-eq amt≤bal = let c = stake addr in
+  begin
+    getCoin acc
+      ≡⟨ split-by-lookup acc c bal lookup-eq ⟩
+    getCoin (acc ∣ ❴ c ❵ ᶜ) + bal
+      ≡⟨ cong (getCoin (acc ∣ ❴ c ❵ ᶜ) +_) (sym (m∸n+n≡m amt≤bal)) ⟩
+    getCoin (acc ∣ ❴ c ❵ ᶜ) + (bal ∸ amt + amt)
+      ≡⟨ trans (sym (+-assoc (getCoin (acc ∣ ❴ c ❵ ᶜ)) (bal ∸ amt) amt))
+               (cong (_+ amt) (+-comm (getCoin (acc ∣ ❴ c ❵ ᶜ)) (bal ∸ amt))) ⟩
+    (bal ∸ amt) + getCoin (acc ∣ ❴ c ❵ ᶜ) + amt
+      ≡˘⟨ cong (_+ amt) (getCoin-∪ˡ-overwrite acc c (bal ∸ amt)) ⟩
+    getCoin (❴ c , bal ∸ amt ❵ ∪ˡ acc) + amt
+      ∎
 ```
 -->
 
@@ -218,9 +238,9 @@ module ApplyToRewards-PoV
 
   -- TODO: ask that these be proved in the `agda-sets` library.
 
-  -- 1. For any credential `c'` other than `c`, lookupᵐ? (❴ c , v ❵ ∪ˡ (m ∣ ❴ c ❵ ᶜ)) c' ≡ lookupᵐ? m c'
-  ( ∪ˡ-res-lookup-preserve : (m : Rewards) (c : Credential) (v : Coin) (c' : Credential)
-      → c' ≢ c → lookupᵐ? (❴ c , v ❵ ∪ˡ (m ∣ ❴ c ❵ ᶜ)) c' ≡ lookupᵐ? m c' )
+  -- 1. For any credential `c'` other than `c`, lookupᵐ? (❴ c , v ❵ ∪ˡ m) c' ≡ lookupᵐ? m c'
+  ( ∪ˡ-lookup-preserve : (m : Rewards) (c : Credential) (v : Coin) (c' : Credential)
+      → c' ≢ c → lookupᵐ? (❴ c , v ❵ ∪ˡ m) c' ≡ lookupᵐ? m c' )
     -- It's hard because the `agda-sets` API requires instance resolution for
     -- `lookupᵐ?`, but the semantic content is clear (lookup in a left-biased union
     -- for a key not in the left map equals lookup in the right map, and complement
@@ -255,22 +275,22 @@ This is the form needed by `PRE-CERT-pov`.
 ```agda
   applyWithdrawals-pov : (wdrls : Withdrawals) (rwds : Rewards)
     → mapˢ stake (dom wdrls) ⊆ dom rwds
+    → ∀[ a ∈ dom wdrls ] NetworkIdOf a ≡ NetworkId
     → ∀[ (addr , amt) ∈ wdrls ˢ ] amt ≤ maybe id 0 (lookupᵐ? rwds (stake addr))
     → getCoin rwds ≡ getCoin (applyWithdrawals wdrls rwds) + getCoin wdrls
 ```
 
 <!--
 ```agda
-  applyWithdrawals-pov wdrls rwds creds∈ amts≤ =
+  applyWithdrawals-pov wdrls rwds creds∈ netIds amts≤ =
     begin
       getCoin rwds
-        ≡⟨ foldl-applyOne-pov rwds (setToList (wdrls ˢ)) inv (setToList-Unique wdrls) ⟩
+        ≡⟨ foldl-applyOne-pov rwds (setToList (wdrls ˢ)) inv (setToList-Unique wdrls netIds) ⟩
       getCoin (foldl (applyOne _∸_) rwds (setToList (wdrls ˢ))) + sum (map proj₂ (setToList (wdrls ˢ)))
         ≡⟨ cong (getCoin (foldl (applyOne _∸_) rwds (setToList (wdrls ˢ))) +_) (sum-map-proj₂≡getCoin wdrls) ⟩
       getCoin (applyWithdrawals wdrls rwds) + getCoin wdrls
         ∎
     where
-    open ≡-Reasoning
     open Equivalence
 
     inv : ∀ {addr amt} → (addr , amt) ∈ˡ setToList (wdrls ˢ)
@@ -357,9 +377,9 @@ This is the form needed by `PRE-CERT-pov`.
             c'≢c : stake addr' ≢ c
             c'≢c = ≢-sym (All.lookup c∉xs (∈-map⁺ (stake ∘ proj₁) mem))
             dom' : stake addr' ∈ dom acc'
-            dom' = ∪ˡ-res-dom-preserve acc c (bal ∸ amt) (stake addr') c'∈dom c'≢c
+            dom' = dom∪ˡʳ {m = ❴ c , bal ∸ amt ❵} {m' = acc} c'∈dom
             bal' : lookupᵐ? acc' (stake addr') ≡ lookupᵐ? acc (stake addr')
-            bal' = ∪ˡ-res-lookup-preserve acc c (bal ∸ amt) (stake addr') c'≢c
+            bal' = ∪ˡ-lookup-preserve acc c (bal ∸ amt) (stake addr') c'≢c
         in  dom' , subst (amt' ≤_) (cong (maybe id 0) (sym bal')) amt'≤
 ```
 -->
@@ -396,15 +416,6 @@ directly from `getCoin-∪ˡ-overwrite`.
         ≡˘⟨ cong (_+ amt) (split-by-lookup acc c bal lookup-eq) ⟩
       getCoin acc + amt
         ∎
-    where
-    open ≡-Reasoning
-    -- Same decomposition `acc ≡ (acc ∣ ❴ c ❵ ᶜ) ∪ˡ (acc ∣ ❴ c ❵)` used in
-    -- `applyOne-pov`; factor it out if both proofs are kept in this module.
-    split-by-lookup : (acc : Rewards) (c : Credential) (bal : Coin)
-      → lookupᵐ? acc c ≡ just bal
-      → getCoin acc ≡ getCoin (acc ∣ ❴ c ❵ ᶜ) + bal
-    split-by-lookup acc c bal lookup-eq = {!!}
-      -- Same proof as the first three steps of `applyOne-pov`; factor it out.
 ```
 -->
 
@@ -421,13 +432,6 @@ directly from `getCoin-∪ˡ-overwrite`.
     sym (+-identityʳ (indexedSumᵛ' id acc))
   foldl-applyOne-pov-add acc ((addr , amt) ∷ xs) h (c∉xs :: uniq-xs)
     with lookupᵐ? acc (stake addr) in eq
-  -- Defensive `nothing` case ruled out by the membership precondition.
-  ... | nothing = ⊥-elim (case lookup-just (h (here refl)) of λ where
-                            (_ , p) → case trans (sym eq) p of λ ())
-    where
-    -- A small helper: membership in domain implies `lookupᵐ?` is `just`.
-    lookup-just : ∀ {a} → a ∈ dom acc → Σ Coin λ v → lookupᵐ? acc a ≡ just v
-    lookup-just = {!!}  -- standard agda-sets bridge; provable from `dom∈`.
   ... | just bal = begin
       getCoin (foldl (applyOne _+_) acc' xs)
         ≡⟨ foldl-applyOne-pov-add acc' xs h' uniq-xs ⟩
@@ -438,17 +442,20 @@ directly from `getCoin-∪ˡ-overwrite`.
       getCoin acc + (amt + sum (map proj₂ xs))
         ∎
     where
-    open ≡-Reasoning
     c = stake addr
     acc' = ❴ c , bal + amt ❵ ∪ˡ acc
     -- `h'` is the same invariant-transfer argument as in `foldl-applyOne-pov`,
-    -- but with no `amt ≤ maybe id 0 (lookupᵐ? _ _)` bound to thread —
-    -- only domain membership has to be preserved.  Use the bridge lemma
-    -- to convert `acc' = ❴ c , bal + amt ❵ ∪ˡ acc` into the equivalent
-    -- `❴ c , bal + amt ❵ ∪ˡ (acc ∣ ❴ c ❵ ᶜ)` form, then reuse
-    -- `∪ˡ-res-dom-preserve` from `Certs/Properties/ApplyWithdrawalsPoV`.
+    -- but with no `amt ≤ maybe id 0 (lookupᵐ? _ _)` bound to thread — only
+    -- domain membership has to be preserved.
+    -- Since `acc' = ❴ c , bal + amt ❵ ∪ˡ acc` (no complement restriction),
+    -- we use `dom∪ˡʳ` directly; membership in `dom acc` lifts to membership
+    -- in `dom acc'` without needing the `c'≢c` witness.
     h' : ∀ {addr' amt'} → (addr' , amt') ∈ˡ xs → stake addr' ∈ dom acc'
-    h' = {!!}  -- mechanical mirror of the original `h'`; see comment above.
+    h' mem = dom∪ˡʳ {m = ❴ c , bal + amt ❵} {m' = acc} (h (there mem))
+  -- Defensive `nothing` case ruled out by the membership precondition.
+  ... | nothing with (stake addr ∈? dom (acc ˢ))
+  ... | yes c∈ = case eq of λ ()
+  ... | no a∉ = ⊥-elim (a∉ (h (here refl)))
 ```
 -->
 
@@ -468,14 +475,13 @@ directly from `getCoin-∪ˡ-overwrite`.
       getCoin (applyDirectDeposits dd rwds)
         ≡⟨ refl ⟩  -- by definition of `applyDirectDeposits = applyToRewards _+_`
       getCoin (foldl (applyOne _+_) rwds (setToList (dd ˢ)))
-        ≡⟨ sym (foldl-applyOne-pov-add rwds (setToList (dd ˢ)) inv
-                                       (setToList-Unique dd netIds)) ⟩
+        ≡⟨ foldl-applyOne-pov-add rwds (setToList (dd ˢ)) inv
+                                       (setToList-Unique dd netIds) ⟩
       getCoin rwds + sum (map proj₂ (setToList (dd ˢ)))
         ≡⟨ cong (getCoin rwds +_) (sum-map-proj₂≡getCoin dd) ⟩
       getCoin rwds + getCoin dd
         ∎
     where
-    open ≡-Reasoning
     open Equivalence
     inv : ∀ {addr amt} → (addr , amt) ∈ˡ setToList (dd ˢ) → stake addr ∈ dom rwds
     inv {addr} {amt} mem =
diff --git a/src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md
@@ -34,16 +34,16 @@ instance
   _ = +-0-monoid
 
 module Certs-PoV
-  ( ∪ˡ-res-lookup-preserve : ∀ (m : Rewards) (c : Credential) (v : Coin) (c' : Credential)
-      → c' ≢ c → lookupᵐ? (❴ c , v ❵ ∪ˡ (m ∣ ❴ c ❵ ᶜ)) c' ≡ lookupᵐ? m c' )
+  ( ∪ˡ-lookup-preserve : ∀ (m : Rewards) (c : Credential) (v : Coin) (c' : Credential)
+      → c' ≢ c → lookupᵐ? (❴ c , v ❵ ∪ˡ m) c' ≡ lookupᵐ? m c' )
 
   ( sum-map-proj₂≡getCoin : ∀ (m : RewardAddress ⇀ Coin) → sum (map proj₂ (setToList (m ˢ))) ≡ getCoin m )
 
   ( setToList-Unique : ∀ (m : RewardAddress ⇀ Coin) → ∀[ a ∈ dom (m ˢ) ] NetworkIdOf a ≡ NetworkId
       → Unique (map (stake ∘ proj₁) (setToList (m ˢ))) )
 
   where
-  open Certs-Pov-lemmas ∪ˡ-res-lookup-preserve sum-map-proj₂≡getCoin setToList-Unique
+  open Certs-Pov-lemmas ∪ˡ-lookup-preserve sum-map-proj₂≡getCoin setToList-Unique
 ```
 -->
 
@@ -64,7 +64,6 @@ Equivalently, the *increase* in rewards balance from `s₁`{.AgdaBound} to
   CERTS-pov : {Γ : CertEnv} {s₁ sₙ : CertState}
     → ∀[ a ∈ dom (WithdrawalsOf Γ) ] NetworkIdOf a ≡ NetworkId
     → ∀[ a ∈ dom (DirectDepositsOf Γ) ] NetworkIdOf a ≡ NetworkId
-    → mapˢ stake (dom (DirectDepositsOf Γ)) ⊆ dom (RewardsOf (DStateOf s₁))
     → Γ ⊢ s₁ ⇀⦇ l ,CERTS⦈ sₙ
     → getCoin s₁ + getCoin (DirectDepositsOf Γ) ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)
 ```
@@ -76,11 +75,11 @@ plus an arithmetic shuffle to interleave the two accounting terms.
 
 <!--
 ```agda
-  CERTS-pov {Γ = Γ} {s₁} {sₙ} validNetIdW validNetIdDD creds∈ (run {s' = s'} (pre-cert , certs)) =
+  CERTS-pov {Γ = Γ} {s₁} {sₙ} validNetIdW validNetIdDD (run {s' = s'} (pre-cert , certs)) =
     begin
-      getCoin s₁ + cdd        ≡⟨ cong (_+ cdd) (PRE-CERT-pov validNetId pre-cert) ⟩
+      getCoin s₁ + cdd        ≡⟨ cong (_+ cdd) (PRE-CERT-pov validNetIdW pre-cert) ⟩
       getCoin s' + cwd + cdd  ≡⟨ swap-right _ (cwd) (cdd) ⟩
-      getCoin s' + cdd + cwd  ≡⟨ cong (_+ cwd) (sts-pov creds∈' validNetIdDD certs) ⟩
+      getCoin s' + cdd + cwd  ≡⟨ cong (_+ cwd) (sts-pov validNetIdDD certs) ⟩
       getCoin sₙ + cwd ∎
     where
     open ≡-Reasoning
@@ -93,7 +92,5 @@ plus an arithmetic shuffle to interleave the two accounting terms.
       trans  (+-assoc a b c)
              (trans  (cong (a +_) (+-comm b c))
                      (sym (+-assoc a c b)))
-    creds∈' : mapˢ stake (dom (DirectDepositsOf Γ)) ⊆ dom (RewardsOf (DStateOf s'))
-    creds∈' = {!!}  -- preserve-dom across PRE-CERT
 ```
 -->
diff --git a/src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md
@@ -121,15 +121,15 @@ injOn _ h {record { stake = stakex }} {record { stake = stakey }} x∈ y∈ refl
   cong (λ u → record { net = u ; stake = stakex }) (trans (h x∈) (sym (h y∈)))
 
 module Certs-Pov-lemmas
-  ( ∪ˡ-res-lookup-preserve : ∀ (m : Rewards) (c : Credential) (v : Coin) (c' : Credential)
-      → c' ≢ c → lookupᵐ? (❴ c , v ❵ ∪ˡ (m ∣ ❴ c ❵ ᶜ)) c' ≡ lookupᵐ? m c' )
+  ( ∪ˡ-lookup-preserve : ∀ (m : Rewards) (c : Credential) (v : Coin) (c' : Credential)
+      → c' ≢ c → lookupᵐ? (❴ c , v ❵ ∪ˡ m ) c' ≡ lookupᵐ? m c' )
 
   ( sum-map-proj₂≡getCoin : ∀ (m : RewardAddress ⇀ Coin) → sum (map proj₂ (setToList (m ˢ))) ≡ getCoin m )
 
   ( setToList-Unique : ∀ (m : RewardAddress ⇀ Coin) → ∀[ a ∈ dom (m ˢ) ] NetworkIdOf a ≡ NetworkId
       → Unique (map (stake ∘ proj₁) (setToList (m ˢ))) )
   where
-    open ApplyToRewards-PoV ∪ˡ-res-lookup-preserve sum-map-proj₂≡getCoin setToList-Unique
+    open ApplyToRewards-PoV ∪ˡ-lookup-preserve sum-map-proj₂≡getCoin setToList-Unique
 ```
 -->
 
@@ -141,16 +141,20 @@ becomes "pre-balance plus direct deposits equals post-balance":
 
 ```agda
     POST-CERT-pov : {Γ : CertEnv} {s s' : CertState}
-      → mapˢ stake (dom (DirectDepositsOf Γ)) ⊆ dom (RewardsOf (DStateOf s))
       → ∀[ a ∈ dom (DirectDepositsOf Γ) ] NetworkIdOf a ≡ NetworkId
       → Γ ⊢ s ⇀⦇ _ ,POST-CERT⦈ s'
       → getCoin s + getCoin (DirectDepositsOf Γ) ≡ getCoin s'
 ```
 
 <!--
 ```agda
-    POST-CERT-pov {Γ} {s} creds∈ netIds (CERT-post {dd = dd} {rewards = rewards} _) =
-      applyDirectDeposits-pov dd rewards creds∈ netIds
+    -- `CERT-post`'s own premise `creds∈ : mapˢ stake (dom dd) ⊆ dom rewards`
+    -- is exactly what `applyDirectDeposits-pov` needs.  We extract it from
+    -- the step rather than threading it from outside, because CERTs *do*
+    -- generally change `dom rewards` (e.g. `DELEG-dereg`), so the premise
+    -- can't be propagated from the pre-CERT* state.
+    POST-CERT-pov netIds (CERT-post {dd = dd} {rewards = rewards} creds∈) =
+      sym (applyDirectDeposits-pov dd rewards creds∈ netIds)
 ```
 -->
 
@@ -163,17 +167,22 @@ final `POST-CERT`{.AgdaDatatype} step adds `getCoin (DirectDepositsOf Γ)`.
 
 ```agda
     sts-pov : {Γ : CertEnv} {s₁ sₙ : CertState} {sigs : List DCert}
-      → mapˢ stake (dom (DirectDepositsOf Γ)) ⊆ dom (RewardsOf (DStateOf s₁))
       → ∀[ a ∈ dom (DirectDepositsOf Γ) ] NetworkIdOf a ≡ NetworkId
       → RunTraceAndThen _⊢_⇀⦇_,CERT⦈_ _⊢_⇀⦇_,POST-CERT⦈_ Γ s₁ sigs sₙ
       → getCoin s₁ + getCoin (DirectDepositsOf Γ) ≡ getCoin sₙ
 ```
 
 <!--
 ```agda
-    sts-pov (run-[] x) = POST-CERT-pov x
-    sts-pov {Γ = Γ} (run-∷ x xs) =
-      trans (cong (_+ getCoin (DirectDepositsOf Γ)) (CERT-pov x)) (sts-pov xs)
+    sts-pov nid (run-[] x) = POST-CERT-pov nid x
+    sts-pov {Γ} {s₁} {sₙ} nid (run-∷ {s' = s'} x xs) =
+      begin
+      rewardsBalance (dState s₁) + getCoin (DirectDepositsOf Γ)
+      ≡⟨ cong (_+ getCoin (DirectDepositsOf Γ)) (CERT-pov x) ⟩
+      rewardsBalance (dState s') + getCoin (DirectDepositsOf Γ)
+        ≡⟨ sts-pov nid xs ⟩
+      rewardsBalance (dState sₙ)
+      ∎
 ```
 -->
 
@@ -194,6 +203,6 @@ Conway's `constMap`/`res-decomp`/`sumConstZero` chain.
 ```agda
     PRE-CERT-pov {Γ = Γ} {s = cs} validNetId
       (CERT-pre {wdrls = wdrls} (_ , wdrlCreds⊆rwds , wdrlBounded)) =
-        applyWithdrawals-pov wdrls (RewardsOf (dState cs)) wdrlCreds⊆rwds wdrlBounded
+        applyWithdrawals-pov wdrls (RewardsOf (dState cs)) wdrlCreds⊆rwds validNetId wdrlBounded
 ```
 -->
