simplifications

Author: williamdemeo

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

@@ -3,7 +3,7 @@ source_branch: master
 source_path: src/Ledger/Dijkstra/Specification/Entities/Properties/ApplyToRewardsPoV.lagda.md
 ---
 
-# `applyToRewards` Preservation of Value {#sec:apply-to-rewards-pov}
+## `applyToRewards` Preservation of Value {#sec:apply-to-rewards-pov}
 
 This module proves preservation of value for the two specializations of
 `applyToRewards`{.AgdaFunction} used inside the `ENTITIES`{.AgdaDatatype} rule.
@@ -38,12 +38,12 @@ open import Ledger.Dijkstra.Specification.Gov.Base using (GovStructure)
 module Ledger.Dijkstra.Specification.Entities.Properties.ApplyToRewardsPoV
   (gs : GovStructure) (open GovStructure gs) where
 
-open import Data.Nat.Properties using (+-identityʳ; +-comm; +-assoc; m∸n+n≡m; n≤0⇒n≡0)
-open import Data.Maybe.Properties using (just-injective)
 open import Data.List.Membership.Propositional.Properties using (∈-map⁺)
 open import Data.List.Relation.Unary.Any using (Any)
 open import Data.List.Relation.Unary.All using (lookup)
 open import Data.List.Relation.Unary.Unique.Propositional using (Unique) renaming (_∷_ to _::_)
+open import Data.Maybe.Properties using (just-injective)
+open import Data.Nat.Properties using (+-identityʳ; +-comm; +-assoc; m∸n+n≡m; n≤0⇒n≡0)
 open import Relation.Binary using (IsEquivalence)
 
 open import Ledger.Prelude hiding (lookup)
@@ -61,7 +61,7 @@ open ≡-Reasoning
 ```
 -->
 
-## Shared helpers
+### Shared helpers
 
 ```agda
 getCoin-∪ˡ-overwrite : (acc : Rewards) (c : Credential) (v : Coin)
@@ -70,9 +70,6 @@ getCoin-∪ˡ-overwrite : (acc : Rewards) (c : Credential) (v : Coin)
 
 <!--
 ```agda
--- The new applyToRewards writes to its accumulator via ❴ k , v ❵ ∪ˡ acc;
--- left-biasedness of ∪ˡ makes this extensionally equal to the older
--- ❴ k , v ❵ ∪ˡ (acc ∣ ❴ k ❵ ᶜ) form; the following proves this at the getCoin level.
 getCoin-∪ˡ-overwrite acc c v =
   begin
     getCoin (❴ c , v ❵ ∪ˡ acc)
@@ -143,7 +140,7 @@ split-by-lookup acc c bal lookup-eq =
 ```
 -->
 
-## The `ApplyToRewards-PoV` module
+### The `ApplyToRewards-PoV` module
 
 The three assumed identities below are the same set/map identities used by the Conway
 PoV proofs; they are stated as module parameters here, to be discharged in a
@@ -183,9 +180,9 @@ lambda body of `applyToRewards f`.
     maybe (λ bal → ❴ stake addr , f bal amt ❵ ∪ˡ acc) acc (lookupᵐ? acc (stake addr))
 ```
 
-## Withdrawal preservation of value
+### Withdrawal preservation of value
 
-### `applyOne-pov`: one withdrawal step decreases `getCoin` by `amt`
+#### `applyOne-pov`: one withdrawal step decreases `getCoin` by `amt`
 
 When `lookupᵐ? acc (stake addr) ≡ just bal` and `amt ≤ bal`, applying a single
 withdrawal reduces the total by exactly `amt`.
@@ -215,16 +212,16 @@ withdrawal reduces the total by exactly `amt`.
 ```
 -->
 
-### `foldl-applyOne-pov` (fold induction)
+#### `foldl-applyOne-pov` (fold induction)
 
-The fold invariant tracks three things through the induction:
+The fold invariant tracks three things through the induction.
 
-1.  every remaining withdrawal credential is in the current accumulator's domain;
+1.  Every remaining withdrawal credential is in the current accumulator's domain.
 
-2.  every remaining withdrawal amount is bounded by the current balance at that
-    credential;
+2.  Every remaining withdrawal amount is bounded by the current balance at that
+    credential.
 
-3.  no credential is revisited (the `Unique`{.AgdaDatatype} witness on the
+3.  No credential is revisited (the `Unique`{.AgdaDatatype} witness on the
     stake-projected list).
 
 Uniqueness is essential here precisely because `applyOne _∸_` *modifies* the balance
@@ -235,8 +232,7 @@ holds.
 ```agda
   foldl-applyOne-pov : (acc : Rewards) (entries : List (RewardAddress × Coin))
     → ( ∀ {addr amt} → (addr , amt) ∈ˡ entries
-        → stake addr ∈ dom acc
-        × amt ≤ maybe id 0 (lookupᵐ? acc (stake addr)) )
+        →  stake addr ∈ dom acc × amt ≤ maybe id 0 (lookupᵐ? acc (stake addr)) )
     → Unique (map (stake ∘ proj₁) entries)
     → getCoin acc ≡ getCoin (foldl (applyOne _∸_) acc entries) + sum (map proj₂ entries)
 ```
@@ -246,15 +242,13 @@ holds.
   foldl-applyOne-pov acc [] _ _ = sym (+-identityʳ (indexedSumᵛ' id acc))
   foldl-applyOne-pov acc ((addr , amt) ∷ xs) h (c∉xs :: uniq-xs)
     with lookupᵐ? acc (stake addr) in eq
-  -- Nothing case: applyOne is the identity; the bound `h (here refl) .proj₂`
-  -- forces `amt ≡ 0`, which makes the recursive call's right-hand side equal
-  -- to ours.
+  -- Nothing case: applyOne is the identity; the bound `h (here refl) .proj₂` forces
+  -- `amt ≡ 0`, which makes the recursive call's right-hand side equal to ours.
   ... | nothing =
     let amt≤0 = subst (amt ≤_) (cong (maybe id 0) eq) (h (here refl) .proj₂)
-        amt≡0 = n≤0⇒n≡0 amt≤0
     in
     subst (λ a → getCoin acc ≡ getCoin (foldl (applyOne _∸_) acc xs) + (a + sum (map proj₂ xs)))
-          (sym amt≡0)
+          (sym (n≤0⇒n≡0 amt≤0))
           (foldl-applyOne-pov acc xs (λ mem → h (there mem)) uniq-xs)
   -- Just case: per-step decrease via `applyOne-pov`, then chain with the IH.
   ... | just bal = begin
@@ -270,7 +264,9 @@ holds.
         getCoin (foldl (applyOne _∸_) acc' xs) + (amt + sum (map proj₂ xs))
           ∎
     where
+    c : Credential
     c = stake addr
+
     acc' : Rewards
     acc' = ❴ c , bal ∸ amt ❵ ∪ˡ acc
 
@@ -302,8 +298,7 @@ holds.
   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))
+    → ∀[ (addr , amt) ∈ wdrls ˢ ] amt ≤ maybe id 0 (lookupᵐ? rwds (stake addr))
     → getCoin rwds ≡ getCoin (applyWithdrawals wdrls rwds) + getCoin wdrls
 ```
 
@@ -429,7 +424,7 @@ Note the slimmed-down signature relative to `applyWithdrawals-pov`: no
   applyDirectDeposits-pov dd rwds creds∈ =
     begin
       getCoin (applyDirectDeposits dd rwds)
-        ≡⟨ refl ⟩  -- by definition of `applyDirectDeposits = applyToRewards _+_`
+        ≡⟨ refl ⟩
       getCoin (foldl (applyOne _+_) rwds (setToList (dd ˢ)))
         ≡⟨ foldl-applyOne-pov-add rwds (setToList (dd ˢ)) inv ⟩
       getCoin rwds + sum (map proj₂ (setToList (dd ˢ)))
@@ -438,8 +433,7 @@ Note the slimmed-down signature relative to `applyWithdrawals-pov`: no
         ∎
     where
     open Equivalence
-    inv : ∀ {addr amt} → (addr , amt) ∈ˡ setToList (dd ˢ)
-        → stake addr ∈ dom rwds
+    inv : ∀ {addr amt} → (addr , amt) ∈ˡ setToList (dd ˢ) → stake addr ∈ dom rwds
     inv {addr} {amt} mem = creds∈ c∈dom-dd
       where
       addr-amt∈dd : (addr , amt) ∈ dd ˢ

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

@@ -3,40 +3,16 @@ source_branch: master
 source_path: src/Ledger/Dijkstra/Specification/Entities/Properties/PoV.lagda.md
 ---
 
-# Properties of `ENTITIES`: Preservation of Value {#thm:ENTITIES-PoV}
+## Properties of `ENTITIES`: Preservation of Value {#thm:ENTITIES-PoV}
 
-This module proves preservation of value for the `ENTITIES`{.AgdaDatatype} rule
-introduced in [CIP-159-11d][PR-1201].  In the Dijkstra era, `ENTITIES`{.AgdaDatatype}
-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 the cert-state rewards balance
-(`coinFromRewards`{.AgdaFunction}; the deposit pots are accounted separately):
+This module proves preservation of value for the `ENTITIES`{.AgdaDatatype} rule.
 
-    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.
-
-## Proof Strategy
-
-Case-split on the single `ENTITIES`{.AgdaInductiveConstructor} constructor to expose
-the three internal phases.  Letting `r₀`{.AgdaBound} denote the initial rewards map
-and `r₁`{.AgdaBound} the rewards map after `CERTS`{.AgdaDatatype}, the equational
-chain is
-
-+  `applyWithdrawals-pov`{.AgdaFunction} on `(wdrls, r₀)` rewrites `getCoin r₀` as
-   `getCoin (applyWithdrawals wdrls r₀) + getCoin wdrls`.
-+  `CERTS-pov`{.AgdaFunction} on the inner step rewrites
-   `getCoin (applyWithdrawals wdrls r₀)` as `getCoin r₁` (the rewards balance is
-   preserved by the closure of `CERT`{.AgdaDatatype}).
-+  `applyDirectDeposits-pov`{.AgdaFunction} on `(dd, r₁)` rewrites
-   `getCoin (applyDirectDeposits dd r₁)` as `getCoin r₁ + getCoin dd`.
-
-The three rewrites compose into the desired equation modulo associativity and
-commutativity of `+` on `Coin`.
-
-[PR-1201]: https://github.com/IntersectMBO/formal-ledger-specifications/pull/1201
+In the Dijkstra era, `ENTITIES`{.AgdaDatatype} wraps the inner `CERTS`{.AgdaDatatype}
+step with per-transaction withdrawal and direct-deposit handling.  Withdrawals and
+deposits are applied to the rewards balance before and after `CERTS`{.AgdaDatatype},
+respectively.  The "value-flow" equation proved below captures the net effect of all
+three components on the cert-state rewards balance (`coinFromRewards`{.AgdaFunction};
+the deposits are accounted separately).
 
 <!--
 ```agda
@@ -48,11 +24,12 @@ module Ledger.Dijkstra.Specification.Entities.Properties.PoV
   (gs : GovStructure) (open GovStructure gs) where
 
 open import Data.List.Relation.Unary.Unique.Propositional using (Unique)
-open import Data.Nat.Properties using (+-comm; +-assoc; +-0-monoid)
+open import Data.Nat.Properties using (+-comm; +-assoc)
 
 open import Ledger.Prelude
 
-open import Ledger.Dijkstra.Specification.Account gs using (DirectDeposits; DirectDepositsOf)
+open import Ledger.Dijkstra.Specification.Account gs
+  using (DirectDeposits; DirectDepositsOf)
 open import Ledger.Dijkstra.Specification.Certs gs
 open import Ledger.Dijkstra.Specification.Entities gs
 open import Ledger.Dijkstra.Specification.Entities.Properties.ApplyToRewardsPoV gs
@@ -62,20 +39,17 @@ open RewardAddress
 open ≡-Reasoning
 
 private variable
-  A      : Type
-  dCerts : List DCert
+  A       : Type
+  dCerts  : List DCert
 
-instance
-  _ = +-0-monoid
 ```
 -->
 
 ## The `ENTITIES-pov` module
 
-`ENTITIES-pov`{.AgdaFunction} inherits the three set/map module parameters of
-`ApplyToRewards-PoV`{.AgdaModule} — they are needed by
-`applyWithdrawals-pov`{.AgdaFunction} and `applyDirectDeposits-pov`{.AgdaFunction} —
-and threads them through unchanged.
+`ENTITIES-pov`{.AgdaFunction} inherits the three module parameters of
+`ApplyToRewards-PoV`{.AgdaModule} (which are "obvious" facts which probably ought to
+be proved upstream in the `agda-sets` library).
 
 ```agda
 module ENTITIES-PoV
@@ -84,18 +58,14 @@ module ENTITIES-PoV
       → c' ≢ c → lookupᵐ? (❴ c , v ❵ ∪ˡ m) c' ≡ lookupᵐ? m c' )
 
   ( sum-map-proj₂≡getCoin :
-      (m : RewardAddress ⇀ Coin)
-      → sum (map proj₂ (setToList (m ˢ))) ≡ getCoin m )
+    (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 ˢ))) )
 
-  -- Certs-PoV stub (discharged later by PR #1210): preservation of value across
-  -- the reflexive-transitive `CERTS` closure.  Formerly proved in
-  -- `Certs.Properties.PoV`; lifted to a module parameter so this PR proves only
-  -- the `ENTITIES`/`LEDGER` layer (top-down strategy).
+  -- Value preservation of the `CERTS` rule to be proved in `Certs.Properties.PoV`.
   ( CERTS-pov : ∀ {Γ : CertEnv} {s s' : CertState} {dCerts : List DCert}
       → Γ ⊢ s ⇀⦇ dCerts ,CERTS⦈ s' → coinFromRewards s ≡ coinFromRewards s' )
   where
@@ -123,53 +93,31 @@ per-batch `NetworkId`{.AgdaFunction} witnesses for `WithdrawalsOf Γ`{.AgdaBound
     → coinFromRewards s + getCoin (DirectDepositsOf Γ) ≡ coinFromRewards s' + getCoin (WithdrawalsOf Γ)
 ```
 
-**Proof**.  Case-split on the single `ENTITIES`{.AgdaInductiveConstructor}
-constructor to expose the inner `CERTS`{.AgdaDatatype} step and the threaded states.
+**Proof**.
 
-<!--
 ```agda
   ENTITIES-pov {Γ = Γ}
     {s  = ⟦ ⟦ _ , _ , r₀ , _ ⟧ᵈ , _ , _ ⟧ᶜˢ} {s' = ⟦ ⟦ _ , _ , _  , _ ⟧ᵈ , _ , _ ⟧ᶜˢ}
     wd-netId dd-netId (ENTITIES { rewards₁ = r₁ } (fst , wdrls⊆ , amts≤ , certsStep , ddCreds⊆ )) =
     begin
-      G r₀ + DD
-        ≡⟨ cong (_+ DD) (applyWithdrawals-pov wdrls r₀ wdrls⊆ wd-netId amts≤) ⟩
-      (G aw + W) + DD
-        ≡⟨ +-assoc (G aw) W DD ⟩
-      G aw + (W + DD)
-        ≡⟨ cong (G aw +_) (+-comm W DD) ⟩
-      G aw + (DD + W)
-        ≡˘⟨ +-assoc (G aw) DD W ⟩
-      (G aw + DD) + W
-        ≡⟨ cong (λ x → (x + DD) + W) (CERTS-pov certsStep) ⟩
-      (G r₁ + DD) + W
-        ≡˘⟨ cong (_+ W) (applyDirectDeposits-pov dd r₁ ddCreds⊆) ⟩
-      G (applyDirectDeposits dd r₁) + W
+      getCoin r₀ + dd
+        ≡⟨ cong (_+ dd) (applyWithdrawals-pov (WithdrawalsOf Γ) r₀ wdrls⊆ wd-netId amts≤) ⟩
+      getCoin aw + wdrls + dd
+        ≡⟨ +-assoc (getCoin aw) wdrls dd ⟩
+      getCoin aw + (wdrls + dd)
+        ≡⟨ cong (getCoin aw +_) (+-comm wdrls dd) ⟩
+      getCoin aw + (dd + wdrls)
+        ≡˘⟨ +-assoc (getCoin  aw) dd wdrls ⟩
+      getCoin aw + dd + wdrls
+        ≡⟨ cong (λ x → (x + dd) + wdrls) (CERTS-pov certsStep) ⟩
+      (getCoin r₁ + dd) + wdrls
+        ≡˘⟨ cong (_+ wdrls) (applyDirectDeposits-pov (DirectDepositsOf Γ) r₁ ddCreds⊆) ⟩
+      getCoin (applyDirectDeposits (DirectDepositsOf Γ) r₁) + wdrls
         ∎
     where
-    wdrls : Withdrawals
-    wdrls = WithdrawalsOf Γ
-    dd : DirectDeposits
-    dd = CertEnv.directDeposits Γ
+    dd  wdrls : Coin
+    dd = getCoin (DirectDepositsOf Γ)
+    wdrls = getCoin (WithdrawalsOf Γ)
     aw : Rewards
-    aw = applyWithdrawals wdrls r₀
-    G : Rewards → Coin
-    G = getCoin
-    W DD : Coin
-    W  = getCoin wdrls
-    DD = getCoin dd
+    aw = applyWithdrawals (WithdrawalsOf Γ) r₀
 ```
--->
-
-The first three rewrites move `W` past `DD` to set up the
-`CERTS-pov`{.AgdaFunction} application; the `CERTS-pov`{.AgdaFunction}
-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: `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.