CIP-159-11: applyWithdrawals-pov and new library lemmas (#1123)

Add the applyWithdrawals preservation-of-value proof machinery and
prove several lemmas that were previously assumed as module parameters
in Conway.

New proofs in Ledger.Prelude (previously Conway module parameters):
- indexedSumᵛ'-∪: getCoin distributes over disjoint ∪ˡ
- sumConstZero: getCoin (constMap X 0) ≡ 0
- getCoin-cong: indexedSum' proj₂ respects set equality
- res-decomp: (m ∪ˡ m') ≡ᵉ (m ∪ˡ (m' ∣ dom m ᶜ))
- getCoin-singleton, ≡ᵉ-getCoin, ∪ˡsingleton∈dom, ∪ˡsingleton∉dom,
  ∪ˡsingleton0≡: singleton map getCoin lemmas
- indexedSumL-proj₂-zero: sum of zero-valued entries is zero
- setToList-∈: opaque bridge from list membership to set membership

New module Certs.Properties.ApplyWithdrawalsPoV:
- applyOne-pov: single withdrawal step decreases getCoin by amt
- foldl-applyOne-pov: fold induction with Unique invariant
- applyWithdrawals-pov: top-level lemma for PRE-CERT-pov
- ∪ˡ-res-dom-preserve: ∪ˡ with complement restriction preserves
  domain membership for other credentials

Remaining assumptions (deferred to agda-sets library):
- ∪ˡ-res-lookup-preserve: lookupᵐ? stability under ∪ˡ for other keys
- sum-map-proj₂≡getCoin: relates list-level sum to indexedSumᵛ'
- setToList-Unique: credential uniqueness of withdrawal list
- ≡ᵉ-getCoinˢ: getCoin invariance under injective key renaming

Author: williamdemeo

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

@@ -47,15 +47,11 @@ instance
   _ = +-0-monoid
 
 module Certs-PoV
-    -- TODO: prove some or all of the following assumptions, used in roof of `CERTBASE-pov`.
-    ( res-decomp'      :  {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
-                         → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ )
-    ( getCoin-cong'    :  {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s'
-                         → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' )
-    ( ≡ᵉ-getCoinˢ'     :  {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
-                         → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
+    -- TODO: prove the following assumption, used in roof of `CERTBASE-pov`.
+    ( ≡ᵉ-getCoinˢ' :  {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
+                      → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
     where
-    open Certs-Pov-lemmas res-decomp' getCoin-cong' ≡ᵉ-getCoinˢ'
+    open Certs-Pov-lemmas ≡ᵉ-getCoinˢ'
 ```
 -->
 

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

@@ -23,7 +23,7 @@ open import Axiom.Set.Properties th
 open import Algebra using (CommutativeMonoid)
 open import Data.Maybe.Properties
 open import Data.Nat.Properties using (+-0-monoid; +-0-commutativeMonoid; +-identityʳ; +-identityˡ)
-open import Relation.Binary using (IsEquivalence)
+import Relation.Binary as Eq using (IsEquivalence)
 open import Relation.Nullary.Decidable
 open import Tactic.ReduceDec
 
@@ -77,7 +77,7 @@ CERT-pov {s = ⟦ _ , stᵖ , stᵍ ⟧ᶜˢ}{⟦ _ , stᵖ' , stᵍ' ⟧ᶜˢ}
   getCoin ⟦ ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ , stᵖ' , stᵍ' ⟧
     ∎
   where
-  module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
+  module ≡ᵉ = Eq.IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
   rwds-∪ˡ-decomp = (rwds ∣ ❴ c ❵ ᶜ) ∪ˡ (rwds ∣ ❴ c ❵ )
 
   rwds-∪ˡ-∪ : rwds-∪ˡ-decomp ˢ ≡ᵉ (rwds ∣ ❴ c ❵ ᶜ)ˢ ∪ (rwds ∣ ❴ c ❵)ˢ
@@ -100,13 +100,9 @@ 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
-  -- TODO: prove some or all of the following assumptions, used in roof of `CERTBASE-pov`.
-  ( res-decomp      :  {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
-                       → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ )
-  ( getCoin-cong    :  {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s'
-                       → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' )
-  ( ≡ᵉ-getCoinˢ     :  {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
-                       → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
+  -- TODO: prove the following assumption, used in roof of `CERTBASE-pov`.
+  ( ≡ᵉ-getCoinˢ :  {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
+                   → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
   where
 ```
 -->
@@ -145,7 +141,7 @@ value of the withdrawals in `Γ`{.AgdaBound}.  In other terms,
       let
         open DState (dState cs )
         open DState (dState cs') renaming (rewards to rewards')
-        module ≡ᵉ       = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
+        module ≡ᵉ       = Eq.IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
         wdrlsCC         = mapˢ (map₁ RewardAddress.stake) (wdrls ˢ)
         zeroMap         = constMap (mapˢ RewardAddress.stake (dom wdrls)) 0
         rwds-∪ˡ-decomp  = (rewards ∣ dom wdrlsCC ᶜ) ∪ˡ (rewards ∣ dom wdrlsCC)

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

@@ -38,12 +38,9 @@ instance
 
 module _
   (tx : Tx) (let open Tx tx; open TxBody body)
-  ( res-decomp      :  {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
-                       → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ )
-  ( getCoin-cong    :  {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s'
-                       → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' )
-  ( ≡ᵉ-getCoinˢ     :  {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
-                       → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
+  -- TODO: prove the following assumption, used in roof of `CERTBASE-pov`.
+  ( ≡ᵉ-getCoinˢ :  {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
+                   → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
   where
 
   pattern UTXO-induction r = UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ r _ _ _
@@ -81,8 +78,8 @@ then the coin values of `s`{.AgdaBound} and `s'`{.AgdaBound} are equal, that is,
       open LState s' renaming (utxoSt to utxoSt'; govSt to govSt'; certState to certState')
       open CertState certState'
       open ≡-Reasoning
-      open Certs-PoV res-decomp  getCoin-cong ≡ᵉ-getCoinˢ
-      zeroMap    = constMap (mapˢ RewardAddress.stake (dom txWithdrawals)) 0
+      open Certs-PoV ≡ᵉ-getCoinˢ
+      zeroMap = constMap (mapˢ RewardAddress.stake (dom txWithdrawals)) 0
     in
     begin
       getCoin utxoSt + getCoin certState

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

@@ -294,22 +294,23 @@ The `LEDGER`{.AgdaDatatype} rule will call `applyDirectDeposits`{.AgdaFunction}
 credit direct deposits to account balances as part of processing a transaction batch.
 
 ```agda
+-- For each withdrawal entry `(addr, amt)`, look up `stake addr` in the acc,
+-- compute `bal ∸ amt`, create a singleton map with the new balance, and
+-- merge it with the rest (complement-restricted, to remove the old entry).
+applyOne : Rewards → RewardAddress × Coin → Rewards
+applyOne acc (addr , amt) =
+  case lookupᵐ? acc (stake addr) of λ where
+    (just bal) → ❴ stake addr , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ stake addr ❵ ᶜ)
+    nothing    → acc
+    -- `nothing` case is defensive; the PRE-CERT precondition guarantees the
+    -- credential is registered, but handling it makes the function total.
+
 applyWithdrawals : Withdrawals → Rewards → Rewards
-applyWithdrawals wdrls rwds =
-  foldl applyOne rwds (setToList (wdrls ˢ))
-  where
-    -- For each withdrawal entry `(addr, amt)`, look up `stake addr` in the acc,
-    -- compute `bal ∸ amt`, create a singleton map with the new balance, and
-    -- merge it with the rest (complement-restricted, to remove the old entry).
-    applyOne : Rewards → RewardAddress × Coin → Rewards
-    applyOne acc (addr , amt) =
-      case lookupᵐ? acc (stake addr) of λ where
-        (just bal) → ❴ stake addr , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ stake addr ❵ ᶜ)
-        nothing    → acc
-        -- `nothing` case is defensive; the PRE-CERT precondition guarantees the
-        -- credential is registered, but handling it makes the function total.
+applyWithdrawals wdrls rwds = foldl applyOne rwds (setToList (wdrls ˢ))
 ```
 
+
+
 In the Dijkstra era, CIP-159 allows **partial withdrawals**: a transaction may
 withdraw any amount up to the current account balance.
 `applyWithdrawals`{.AgdaFunction} subtracts each withdrawal amount from the

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

@@ -13,5 +13,8 @@ module Ledger.Dijkstra.Specification.Certs.Properties where
 -->
 
 ```agda
+open import Ledger.Dijkstra.Specification.Certs.Properties.ApplyWithdrawalsPoV
 open import Ledger.Dijkstra.Specification.Certs.Properties.Computational
+open import Ledger.Dijkstra.Specification.Certs.Properties.PoV
+open import Ledger.Dijkstra.Specification.Certs.Properties.PoVLemmas
 ```