[Dijkstra] CIP-159-11a: Prove Certs preservation of value (#1185)

Author: williamdemeo

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

@@ -40,35 +40,12 @@ private variable
 instance
   _ = +-0-monoid
 
-getCoin-singleton : ⦃ _ : DecEq A ⦄ {(a , c) : A × Coin} → indexedSumᵛ' id ❴ (a , c) ❵ ≡ c
-getCoin-singleton = indexedSum-singleton' {M = Coin} (finiteness _)
-
-∪ˡsingleton∈dom :  ⦃ _ : DecEq A ⦄ (m : A ⇀ Coin) {(a , c) : A × Coin}
-                → a ∈ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m
-∪ˡsingleton∈dom m {(a , c)} a∈dom = ≡ᵉ-getCoin (m ∪ˡ ❴ (a , c) ❵) m (singleton-∈-∪ˡ {m = m} a∈dom)
-
 module _  ( indexedSumᵛ'-∪ :  {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
                               → disjoint (dom m) (dom m')
                               → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' )
   where
   open ≡-Reasoning
   open Equivalence
-
-  ∪ˡsingleton∉dom :  ⦃ _ : DecEq A ⦄ (m : A ⇀ Coin) {(a , c) : A × Coin}
-                   → a ∉ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m + c
-  ∪ˡsingleton∉dom m {(a , c)} a∉dom = begin
-    getCoin (m ∪ˡ ❴ a , c ❵ᵐ)
-      ≡⟨ indexedSumᵛ'-∪ m ❴ a , c ❵ᵐ
-         ( λ x y → a∉dom (subst (_∈ dom m) (from ∈-dom-singleton-pair y) x) ) ⟩
-    getCoin m + getCoin ❴ a , c ❵ᵐ
-      ≡⟨ cong (getCoin m +_) getCoin-singleton ⟩
-    getCoin m + c
-      ∎
-
-  ∪ˡsingleton0≡ : ⦃ _ : DecEq A ⦄ → (m : A ⇀ Coin) {a : A} → getCoin (m ∪ˡ ❴ (a , 0) ❵ᵐ) ≡ getCoin m
-  ∪ˡsingleton0≡ m {a} with a ∈? dom m
-  ... | yes a∈dom = ∪ˡsingleton∈dom m a∈dom
-  ... | no a∉dom = trans (∪ˡsingleton∉dom m a∉dom) (+-identityʳ (getCoin m))
 ```
 -->
 

src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md

@@ -51,9 +51,6 @@ coin∅ = begin
   0 ∎
   where open Prelude.≡-Reasoning
 
-getCoin-singleton : ((dp , c) : DepositPurpose × Coin) → indexedSumᵛ' id ❴ (dp , c) ❵ ≡ c
-getCoin-singleton _ = indexedSum-singleton' {A = DepositPurpose × Coin} {f = proj₂} (finiteness _)
-
 module _ -- ASSUMPTION --
          (gc-hom : (d₁ d₂ : Deposits) → getCoin (d₁ ∪⁺ d₂) ≡ getCoin d₁ + getCoin d₂)
   where
@@ -63,7 +60,7 @@ module _ -- ASSUMPTION --
     getCoin (deps ∪⁺ ❴ (dp , c) ❵)
       ≡⟨ gc-hom deps ❴ (dp , c) ❵ ⟩
     getCoin deps + getCoin{A = Deposits} ❴ (dp , c) ❵
-      ≡⟨ cong (getCoin deps +_) (getCoin-singleton (dp , c)) ⟩
+      ≡⟨ cong (getCoin deps +_) getCoin-singleton ⟩
     getCoin deps + c
       ∎
     where open Prelude.≡-Reasoning

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

@@ -104,14 +104,14 @@ record PState : Type where
   field
     pools     : Pools
     fPools    : Pools
-    retiring  : KeyHash ⇀ Epoch
+    retiring  : Retiring
     deposits  : KeyHash ⇀ Coin
 
 record GState : Type where
   constructor ⟦_,_,_⟧ᵛ
   field
     dreps      : DReps
-    ccHotKeys  : Credential ⇀ Maybe Credential
+    ccHotKeys  : CCHotKeys
     deposits   : Credential ⇀ Coin
 
 record CertState : Type where
@@ -297,22 +297,23 @@ credit each transaction's direct deposits to its account balances after certific
 processing.  See *Direct Deposit Application (CIP-159)* below for details.
 
 ```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
 ```