Update Certs PoV proofs for direct-deposit application in POST-CERT (CIP-159)

williamdemeo · williamdemeo · commit 5e41b66073b0 · 2026-05-07T18:23:11.000-06:00
After direct-deposit application moved from LEDGER-V/SUBLEDGER-V into the POST-CERT rule, the Certs preservation-of-value proofs needed to account for the `getCoin (DirectDepositsOf Γ)` increase that POST-CERT now produces via `rewards ∪⁺ directDeposits`. Statement changes: - POST-CERT-pov: getCoin s ≡ getCoin s' → getCoin s + getCoin (DirectDepositsOf Γ) ≡ getCoin s' - sts-pov: gains a `+ getCoin (DirectDepositsOf Γ)` term on the LHS - CERTS-pov: becomes the symmetric "consumed = produced" form getCoin s₁ + getCoin (DirectDepositsOf Γ) ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ) Structural changes: - POST-CERT-pov and sts-pov move into the parameterized `Certs-Pov-lemmas` sub-module (alongside PRE-CERT-pov), since they now require a fourth module parameter: indexedSumᵛ'-∪⁺ : ∀ (m m' : Rewards) → getCoin (m ∪⁺ m') ≡ getCoin m + getCoin m' This is the natural ∪⁺ analogue of the existing `indexedSumᵛ'-∪` lemma for `∪ˡ` on disjoint domains, but unconditional because `∪⁺` adds (rather than drops) values at shared keys. TODO: upstream to agda-sets. - `Certs-PoV` (in PoV.lagda.md) gains the same parameter and forwards it. CERT-pov and PRE-CERT-pov are unchanged: the CERT and PRE-CERT rules did not change in this refactor. Closes part of #1185.
diff --git a/src/Ledger/Dijkstra/Specification/Account.lagda.md b/src/Ledger/Dijkstra/Specification/Account.lagda.md
@@ -33,6 +33,14 @@ DirectDeposits : Type
 DirectDeposits = Credential ⇀ Coin
 ```
 
+<!--
+```agda
+record HasDirectDeposits {a} (A : Type a) : Type a where
+  field DirectDepositsOf : A → DirectDeposits
+open HasDirectDeposits ⦃...⦄ public
+```
+-->
+
 ## Balance Intervals {#sec:balance-intervals}
 
 [CIP 159][] allows a transaction to assert that an account's balance falls within a
diff --git a/src/Ledger/Dijkstra/Specification/Certs.lagda.md b/src/Ledger/Dijkstra/Specification/Certs.lagda.md
@@ -181,6 +181,9 @@ instance
   HasWithdrawals-CertEnv : HasWithdrawals CertEnv
   HasWithdrawals-CertEnv .WithdrawalsOf = CertEnv.wdrls
 
+  HasDirectDeposits-CertEnv : HasDirectDeposits CertEnv
+  HasDirectDeposits-CertEnv .DirectDepositsOf = CertEnv.directDeposits
+
   HasVoteDelegs-DState : HasVoteDelegs DState
   HasVoteDelegs-DState .VoteDelegsOf = DState.voteDelegs
 
diff --git a/src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md
@@ -16,12 +16,13 @@ module Ledger.Dijkstra.Specification.Certs.Properties.PoV
 
 open import Ledger.Prelude
 
+open import Ledger.Dijkstra.Specification.Account gs
 open import Ledger.Dijkstra.Specification.Certs gs
 open import Ledger.Dijkstra.Specification.Certs.Properties.PoVLemmas gs
 open import Ledger.Dijkstra.Specification.Gov.Actions gs hiding (yes; no)
 open import Ledger.Prelude
 open import Data.List.Relation.Unary.Unique.Propositional using (Unique)
-open import Data.Nat.Properties using (+-0-monoid)
+open import Data.Nat.Properties using (+-0-monoid; +-comm; +-assoc)
 
 open CertState
 open RewardAddress
@@ -39,22 +40,59 @@ module Certs-PoV
   ( sum-map-proj₂≡getCoin : ∀ (m : Withdrawals) → sum (map proj₂ (setToList (m ˢ))) ≡ getCoin m )
 
   ( setToList-Unique : ∀ (m : Withdrawals) → Unique (map (stake ∘ proj₁) (setToList (m ˢ))) )
+
+  -- New CIP-159 assumption (forwarded to Certs-Pov-lemmas): see PoVLemmas.
+  ( indexedSumᵛ'-∪⁺ : ∀ (m m' : Rewards) → getCoin (m ∪⁺ m') ≡ getCoin m + getCoin m' )
+
   where
-    open Certs-Pov-lemmas ∪ˡ-res-lookup-preserve sum-map-proj₂≡getCoin setToList-Unique
+  open Certs-Pov-lemmas ∪ˡ-res-lookup-preserve sum-map-proj₂≡getCoin setToList-Unique
+                        indexedSumᵛ'-∪⁺
 ```
 -->
 
 ## Theorem: The `CERTS` rule preserves value {#thm:CERTS-PoV}
 
+In Dijkstra, the `CERTS`{.AgdaDatatype} rule processes withdrawals (via
+`PRE-CERT`{.AgdaDatatype}) and direct deposits (via `POST-CERT`{.AgdaDatatype})
+in addition to the certificate steps.  Withdrawals reduce the rewards balance;
+direct deposits increase it; the preservation-of-value equation is a symmetric
+"consumed equals produced" statement:
+
+`getCoin s₁ + getCoin (CertEnv.directDeposits Γ) ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)`.
+
+Equivalently, the *increase* in rewards balance from `s₁`{.AgdaBound} to
+`sₙ`{.AgdaBound} equals `directDeposits − withdrawals`.
+
 ```agda
-    CERTS-pov : {Γ : CertEnv} {s₁ sₙ : CertState}
-      → ∀[ a ∈ dom (WithdrawalsOf Γ) ] NetworkIdOf a ≡ NetworkId
-      → Γ ⊢ s₁ ⇀⦇ l ,CERTS⦈ sₙ
-      → getCoin s₁ ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)
+  CERTS-pov : {Γ : CertEnv} {s₁ sₙ : CertState}
+    → ∀[ a ∈ dom (WithdrawalsOf Γ) ] NetworkIdOf a ≡ NetworkId
+    → Γ ⊢ s₁ ⇀⦇ l ,CERTS⦈ sₙ
+    → getCoin s₁ + getCoin (DirectDepositsOf Γ) ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)
 ```
 
+The proof composes `PRE-CERT-pov`{.AgdaFunction} (which gives
+`getCoin s₁ ≡ getCoin s' + getCoin (WithdrawalsOf Γ)`) with `sts-pov`{.AgdaFunction}
+(which gives `getCoin s' + getCoin (DirectDepositsOf Γ) ≡ getCoin sₙ`),
+plus an arithmetic shuffle to interleave the two accounting terms.
+
+<!--
 ```agda
-    CERTS-pov {Γ = Γ} validNetId (run (pre-cert , certs)) =
-      trans  (PRE-CERT-pov validNetId pre-cert)
-             (cong (_+ getCoin (WithdrawalsOf Γ)) (sts-pov certs))
+  CERTS-pov {Γ = Γ} {s₁} {sₙ} validNetId (run {s' = s'} (pre-cert , certs)) =
+    begin
+      getCoin s₁ + cdd        ≡⟨ cong (_+ cdd) (PRE-CERT-pov validNetId pre-cert) ⟩
+      getCoin s' + cwd + cdd  ≡⟨ swap-right _ (cwd) (cdd) ⟩
+      getCoin s' + cdd + cwd  ≡⟨ cong (_+ cwd) (sts-pov certs) ⟩
+      getCoin sₙ + cwd ∎
+    where
+    open ≡-Reasoning
+    cdd cwd : Coin
+    cdd = getCoin (DirectDepositsOf Γ)
+    cwd = getCoin (WithdrawalsOf Γ)
+
+    swap-right : ∀ a b c → (a + b) + c ≡ (a + c) + b
+    swap-right a b c =
+      trans  (+-assoc a b c)
+             (trans  (cong (a +_) (+-comm b c))
+                     (sym (+-assoc a c b)))
 ```
+-->
diff --git a/src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md
@@ -8,11 +8,17 @@ source_path: src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.
 
 ## Key Differences from Conway
 
-+  **`PRE-CERT`**: Conway uses `constMap wdrlCreds 0 ∪ˡ rewards` (zeroing).
++  **`PRE-CERT`**.  Conway uses `constMap wdrlCreds 0 ∪ˡ rewards` (zeroing).
    Dijkstra (CIP-159) uses `applyWithdrawals wdrls rewards` (subtraction).
    The PoV equation still holds; the proof structure differs.
-+  **`CERT` / `DELEG`**: Same value-relevant structure as Conway.
-+  **No `CERT-vdel`**: Dijkstra has `CERT-deleg`, `CERT-pool`, `CERT-gov` only.
++  **`POST-CERT`**.  Conway only filters `voteDelegs` and preserves `getCoin`.
+   Dijkstra (CIP-159) additionally applies `rewards ∪⁺ directDeposits`, increasing
+   the value by `getCoin (DirectDepositsOf Γ)`.  The PoV equation
+   therefore changes: `POST-CERT-pov` and `sts-pov` now relate the pre- and
+   post-state by the direct-deposit total, and `CERTS-pov` becomes a symmetric
+   "consumed ≡ produced" equation balancing withdrawals against direct deposits.
++  **`CERT` / `DELEG`**.  Same value-relevant structure as Conway.
++  **No `CERT-vdel`**.  Dijkstra has `CERT-deleg`, `CERT-pool`, `CERT-gov` only.
 
 <!--
 ```agda
@@ -23,6 +29,7 @@ open import Ledger.Dijkstra.Specification.Gov.Base using (GovStructure)
 module Ledger.Dijkstra.Specification.Certs.Properties.PoVLemmas
   (gs : GovStructure) (open GovStructure gs) where
 
+open import Ledger.Dijkstra.Specification.Account gs
 open import Ledger.Dijkstra.Specification.Certs gs
 open import Ledger.Dijkstra.Specification.Certs.Properties.ApplyWithdrawalsPoV gs
 open import Ledger.Dijkstra.Specification.Gov.Actions gs hiding (yes; no)
@@ -56,6 +63,8 @@ CERT-pov : {Γ : CertEnv} {s s' : CertState}
   → Γ ⊢ s ⇀⦇ dCert ,CERT⦈ s' → getCoin s ≡ getCoin s'
 ```
 
+(The `CERT` rule is unchanged in Dijkstra, so this lemma matches the Conway version.)
+
 <!--
 ```agda
 CERT-pov (CERT-deleg (DELEG-delegate {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds)
@@ -88,26 +97,20 @@ CERT-pov (CERT-gov _) = refl
 ```
 -->
 
-## POST-CERT-pov and sts-pov
-
-```agda
-POST-CERT-pov : {Γ : CertEnv} {s s' : CertState}
-  → Γ ⊢ s ⇀⦇ _ ,POST-CERT⦈ s' → getCoin s ≡ getCoin s'
+## CIP-159 PoV lemmas (parameterized)
 
-POST-CERT-pov CERT-post = refl
-
-sts-pov : {Γ : CertEnv} {s₁ sₙ : CertState} {sigs : List DCert}
-  → RunTraceAndThen _⊢_⇀⦇_,CERT⦈_ _⊢_⇀⦇_,POST-CERT⦈_ Γ s₁ sigs sₙ
-  → getCoin s₁ ≡ getCoin sₙ
-sts-pov (run-[] x) = POST-CERT-pov x
-sts-pov (run-∷ x xs) = trans (CERT-pov x) (sts-pov xs)
-```
+The `POST-CERT-pov`, `sts-pov`, and `PRE-CERT-pov` proofs all live inside the
+parameterized `Certs-Pov-lemmas`{.AgdaModule} sub-module.
 
-## PRE-CERT-pov (CIP-159: partial withdrawals)
-
-The key new assumption `applyWithdrawals-pov` states that applying withdrawals
-decreases `rewardsBalance` by exactly the total withdrawn amount.  This replaces
-Conway's `constMap`/`res-decomp`/`sumConstZero` chain.
++  `PRE-CERT-pov`{.AgdaFunction} relies on `applyWithdrawals-pov`{.AgdaFunction}
+   from `Certs.Properties.ApplyWithdrawalsPoV`{.AgdaModule}, which itself takes
+   three module parameters bridging gaps in the `agda-sets` API.
++  `POST-CERT-pov`{.AgdaFunction} relies on a fourth parameter
+   `indexedSumᵛ'-∪⁺`{.AgdaFunction} stating that `getCoin` distributes over
+   `∪⁺`{.AgdaFunction} (union with addition).  This is the natural analogue of
+   the existing Conway `indexedSumᵛ'-∪`{.AgdaFunction} lemma for `∪ˡ`{.AgdaFunction}
+   on disjoint domains, but for `∪⁺`{.AgdaFunction} the equation holds
+   *unconditionally* — values at shared keys are added rather than dropped.
 
 <!--
 ```agda
@@ -124,11 +127,62 @@ module Certs-Pov-lemmas
   ( sum-map-proj₂≡getCoin : ∀ (m : Withdrawals) → sum (map proj₂ (setToList (m ˢ))) ≡ getCoin m )
 
   ( setToList-Unique : ∀ (m : Withdrawals) → Unique (map (stake ∘ proj₁) (setToList (m ˢ))) )
+
+  -- New CIP-159 assumption: getCoin distributes over ∪⁺.
+  -- `∪⁺` adds values of shared keys, so `getCoin (m ∪⁺ m') ≡ getCoin m + getCoin m'`
+  -- holds unconditionally.  TODO: Prove this in Ledger.Prelude or agda-sets.
+  ( indexedSumᵛ'-∪⁺ : ∀ (m m' : Rewards) → getCoin (m ∪⁺ m') ≡ getCoin m + getCoin m' )
   where
     open ApplyWithdrawals-PoV ∪ˡ-res-lookup-preserve sum-map-proj₂≡getCoin setToList-Unique
 ```
 -->
 
+### POST-CERT-pov (CIP-159: direct deposits)
+
+The `POST-CERT`{.AgdaDatatype} rule applies direct deposits via `rewards ∪⁺ dd`,
+*increasing* the rewards balance by `getCoin dd`.  The PoV equation therefore
+becomes "pre-balance plus direct deposits equals post-balance":
+
+```agda
+    POST-CERT-pov : {Γ : CertEnv} {s s' : CertState}
+      → Γ ⊢ s ⇀⦇ _ ,POST-CERT⦈ s'
+      → getCoin s + getCoin (DirectDepositsOf Γ) ≡ getCoin s'
+```
+
+<!--
+```agda
+    POST-CERT-pov (CERT-post {dd = dd} {rewards = rewards} _) =
+      sym (indexedSumᵛ'-∪⁺ rewards dd)
+```
+-->
+
+### sts-pov
+
+A trace of `CERT`{.AgdaDatatype} steps followed by `POST-CERT`{.AgdaDatatype}
+increases the rewards balance by exactly the direct-deposit total: each
+`CERT`{.AgdaDatatype} step preserves value (by `CERT-pov`{.AgdaFunction}), and the
+final `POST-CERT`{.AgdaDatatype} step adds `getCoin (DirectDepositsOf Γ)`.
+
+```agda
+    sts-pov : {Γ : CertEnv} {s₁ sₙ : CertState} {sigs : List DCert}
+      → 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)
+```
+-->
+
+### PRE-CERT-pov (CIP-159: partial withdrawals)
+
+The key new assumption `applyWithdrawals-pov` states that applying withdrawals
+decreases `rewardsBalance` by exactly the total withdrawn amount.  This replaces
+Conway's `constMap`/`res-decomp`/`sumConstZero` chain.
+
 ```agda
     PRE-CERT-pov : {Γ : CertEnv} {s s' : CertState}
       → ∀[ a ∈ dom (WithdrawalsOf Γ) ] NetworkIdOf a ≡ NetworkId
diff --git a/src/Ledger/Dijkstra/Specification/Transaction.lagda.md b/src/Ledger/Dijkstra/Specification/Transaction.lagda.md
@@ -412,10 +412,6 @@ could be either of them.
     field CurrentTreasuryOf : A → Maybe Coin
   open HasCurrentTreasury ⦃...⦄ public
 
-  record HasDirectDeposits {a} (A : Type a) : Type a where
-    field DirectDepositsOf : A → DirectDeposits
-  open HasDirectDeposits ⦃...⦄ public
-
   record HasBalanceIntervals {a} (A : Type a) : Type a where
     field BalanceIntervalsOf : A → AccountBalanceIntervals
   open HasBalanceIntervals ⦃...⦄ public
