improvements

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.
@@ -60,7 +60,7 @@ open ≡-Reasoning
 ```
 -->
 
-### Shared helpers
+## Shared helpers
 
 ```agda
 getCoin-∪ˡ-overwrite : (acc : Rewards) (c : Credential) (v : Coin)
@@ -139,7 +139,7 @@ split-by-lookup acc c bal lookup-eq =
 ```
 -->
 
-### The `ApplyToRewards-PoV` module
+## The <span class="AgdaModule">ApplyToRewards-PoV</span> 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.
@@ -290,7 +290,7 @@ holds.
 ```
 -->
 
-### `applyWithdrawals-pov`
+#### `applyWithdrawals-pov`
 
 ```agda
   applyWithdrawals-pov : (wdrls : Withdrawals) (rwds : Rewards)
@@ -327,9 +327,9 @@ holds.
 ```
 -->
 
-## Direct-deposit preservation of value
+### Direct-deposit preservation of value
 
-### `applyOne-pov-add` (one direct-deposit step increases `getCoin` by `amt`)
+#### `applyOne-pov-add` (one direct-deposit step increases `getCoin` by `amt`)
 
 For addition, no `amt ≤ bal` premise is needed (the operation is total),
 and the per-step equation is `getCoin (...) ≡ getCoin acc + amt`
@@ -360,7 +360,7 @@ balance.
 ```
 -->
 
-### `foldl-applyOne-pov-add` (fold induction, no `Unique` needed)
+#### `foldl-applyOne-pov-add` (fold induction, no `Unique` needed)
 
 Unlike the withdrawal version, the additive fold induction needs only
 domain preservation — the `Unique`{.AgdaDatatype} witness drops out.
@@ -405,7 +405,7 @@ the same credential simply accumulates additions correctly.
 ```
 -->
 
-### `applyDirectDeposits-pov`
+#### `applyDirectDeposits-pov`
 
 Note the slimmed-down signature relative to `applyWithdrawals-pov`: no
 `NetworkId`{.AgdaFunction} premise (none is needed), no

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

@@ -6,20 +6,21 @@ source_path: src/Ledger/Dijkstra/Specification/Entities/Properties/PoV.lagda.md
 ## Properties of `ENTITIES`: Preservation of Value {#thm:ENTITIES-PoV}
 
 This module proves preservation of value for the `ENTITIES`{.AgdaDatatype} and
-`SUBENTITIES`{.AgdaDatatype} rules.  Each rule wraps the inner `CERTS`{.AgdaDatatype}
-step with the withdrawal and direct-deposit handling of the transaction given as the
-signal, and its value accounting splits into the two components of
-`getCoin`{.AgdaFunction} on a `CertState`{.AgdaRecord}:
+`SUBENTITIES`{.AgdaDatatype} rules.
+
+Each rule wraps the inner `CERTS`{.AgdaDatatype} step with the withdrawal and
+direct-deposit handling of the transaction.  Each rule's value accounting splits into
+the following two components of `getCoin`{.AgdaFunction} on a `CertState`{.AgdaRecord}:
 
 +  **rewards flow** (`SUBENTITIES-pov`{.AgdaFunction}, `ENTITIES-pov`{.AgdaFunction}):
    the rewards balance grows by the transaction's direct deposits and shrinks by its
-   withdrawals — `CERTS`{.AgdaDatatype} itself preserves it;
+   withdrawals, whereas `CERTS`{.AgdaDatatype} preserves rewards balance;
 
 +  **deposit flow** (`SUBENTITIES-deposits-pov`{.AgdaFunction},
    `ENTITIES-deposits-pov`{.AgdaFunction}): the deposit pots change by exactly the
    new deposits minus the refunds of the transaction's certificates, in the closed
    form (`newCertDeposits`{.AgdaFunction}/`refundCertDeposits`{.AgdaFunction}) used
-   by the `UTXO`{.AgdaDatatype} batch-balance equation.
+   by the batch-balance equation of `UTXO`{.AgdaDatatype}.
 
 `SUBENTITIES-pov-total`{.AgdaFunction} and `ENTITIES-pov-total`{.AgdaFunction}
 combine the two into a single equation for the full `CertState`{.AgdaRecord} coin.
@@ -30,9 +31,10 @@ Two hypotheses appear, both about the rule's *input* state:
    the account's balance.  `applyWithdrawals`{.AgdaFunction} uses truncating
    subtraction (`_∸_`), so without this bound a withdrawal could claim more coin than
    actually leaves the rewards pot.  The rules' own premises bound withdrawals
-   against the *pre-batch* snapshot `rewards₀`{.AgdaField} (exactly, per account, in
-   top-level legacy mode), which does not by itself bound them against the input
-   state of a later step in the batch, so the bound is taken as a hypothesis here.
+   against the *pre-batch* snapshot `rewards₀`{.AgdaField}, which does not by itself
+   bound them against the input state of a later step in the batch, so the bound is
+   taken as a hypothesis here.  In legacy mode, however, the equality premise checks
+   against the rule's current input rewards, not `rewards₀`{.AgdaField}.
 
 +  `PoolDepositsRegistered`{.AgdaFunction}: every pool-deposit entry belongs to a
    registered pool (see `Certs`{.AgdaModule}).  Without it,
@@ -77,11 +79,10 @@ private variable
 +  `CERTS-deposits-pov`: over a `CERTS` run, the deposit pots satisfy the closed-form
    accounting *pre + new ≡ post + refunds*, with `newCertDeposits`{.AgdaFunction}
    threading the run's initial registered-pool set;
-+  `CERTS-deposits-registered`: `CERTS` preserves
-   `PoolDepositsRegistered`{.AgdaFunction};
++  `CERTS-deposits-registered`: `CERTS` preserves `PoolDepositsRegistered`{.AgdaFunction};
 +  `CERTS-new-thread`: `newCertDeposits`{.AgdaFunction} over an appended certificate
    list splits at a `CERTS` run boundary, the second half against the run's *final*
-   pool set — this is what lets per-step accounting compose across a batch.
+   pool set; this is what lets per-step accounting compose across a batch.
 
 ```agda
 module ENTITIES-PoV
@@ -132,10 +133,10 @@ account balance in `s`{.AgdaBound} (the `amts≤`{.AgdaBound} no-truncation
 hypothesis).  Then,
 
     coinFromRewards s + getCoin (DirectDepositsOf txSub)
-      ≡ coinFromRewards s' + getCoin (WithdrawalsOf txSub)
+    ≡ coinFromRewards s' + getCoin (WithdrawalsOf txSub)
 
-All other ingredients — the `NetworkId`{.AgdaFunction} witnesses and the two domain
-conditions — are premises of the rule itself.
+All other ingredients (the `NetworkId`{.AgdaFunction} witnesses and the two domain
+conditions) are premises of the rule itself.
 
 **Formally**.
 
@@ -173,6 +174,7 @@ conditions — are premises of the rule itself.
     dd  wdrls : Coin
     dd = getCoin (DirectDepositsOf txSub)
     wdrls = getCoin (WithdrawalsOf txSub)
+
     aw : Rewards
     aw = applyWithdrawals (WithdrawalsOf txSub) r₀
 ```

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

@@ -35,10 +35,10 @@ the direct-deposit trick (see *Proof Strategy*), and the gov-deposit growth
 
 The `PoolDepositsRegistered`{.AgdaFunction} hypothesis is necessary, not an artifact
 of the proof: the batch balance charges `newCertDeposits`{.AgdaFunction} against the
-registered-pool set, while `POOL-reg`{.AgdaInductiveConstructor}'s left-biased pot
-update silently keeps a stale entry for an unregistered pool — at a state with such
-an entry, a pool registration destroys the charged deposit and the theorem is false.
-On-chain states satisfy the hypothesis by construction.
+registered-pool set, while `POOL-reg`{.AgdaInductiveConstructor}'s left-biased update
+silently keeps a stale entry for an unregistered pool; at a state with such an entry,
+a pool registration destroys the charged deposit and the theorem is false.  On-chain
+states satisfy the hypothesis by construction.
 
 ## Proof Strategy
 
@@ -49,25 +49,24 @@ The Dijkstra `LEDGER-pov`{.AgdaFunction} does not decompose into independent
 may individually transfer value between UTxO and CertState without local balancing.
 
 Instead, the `LEDGER-V` proof is a single equational chain at the
-`LedgerState`{.AgdaRecord} level, with the cancellation of total direct deposits as
-the central trick — direct-deposit value appears both on the UTxO side (via
+`LedgerState`{.AgdaRecord} level, and cancellation of the *total* direct deposits is
+the key to the proof.  Direct-deposit value appears both on the UTxO side (via
 `producedBatch`) and on the CertState side (via `applyDirectDeposits` inside
 `ENTITIES`) and cancels in the total.
 
 Concretely, the proof composes four inductions over the `SUBLEDGERS`{.AgdaDatatype}
 reflexive-transitive closure, plus one arithmetic identity.
 
-+  **`SUBLEDGERS-utxo-coin`{.AgdaFunction}** threads the per-`SUBUTXOW` coin equation
-   (`subutxow-step-coin`).
-+  **`SUBLEDGERS-certs-pov`{.AgdaFunction}** composes per-sub-transaction
++  **`SUBLEDGERS-utxo-coin`{.AgdaFunction}** inducts over the subtransaction list,
+   applying the per-`SUBUTXOW` coin equation (`subutxow-step-coin`) at each step.
++  **`SUBLEDGERS-rewards-pov`{.AgdaFunction}** composes per-sub-transaction
    `SUBENTITIES-pov`{.AgdaFunction} invocations (the rewards flow).
 +  **`SUBLEDGERS-deposits`{.AgdaFunction}** (with `SUBLEDGERS-registered`{.AgdaFunction})
    telescopes the per-step closed-form deposit accounting into the batch-wide
    equation consumed by `bat'`.
-+  **`SUBLEDGERS-gov-coin`{.AgdaFunction}** accumulates the per-`GOVS` gov-deposit
-   growth.
-+  **`posNeg-deposits`{.AgdaFunction}** equationally relates the pre-/post-batch deposit
-   totals to the `posPart`/`negPart` of `calculateDepositsChange`.
++  **`SUBLEDGERS-gov-coin`{.AgdaFunction}** accumulates the per-`GOVS` gov-deposit growth.
++  **`posNeg-deposits`{.AgdaFunction}** relates the pre-/post-batch deposit totals to
+   the `posPart`/`negPart` of `calculateDepositsChange`.
 
 The `LEDGER-I` case is straightforward; `certState` and `govSt` are unchanged,
 `SUBLEDGERS` is a no-op, and only the `UTXOW` step affects `getCoin`, which it
@@ -106,10 +105,6 @@ open import Ledger.Dijkstra.Specification.Utxow txs abs
 
 open import Ledger.Dijkstra.Specification.Entities.Properties.PoV txs
 
--- We will import the following once the UTXO/UTXOW PoV proofs land:
--- open import Ledger.Dijkstra.Specification.Utxo.Properties.PoV txs abs
--- open import Ledger.Dijkstra.Specification.Utxow.Properties.PoV txs abs
-
 open import Interface.STS
 
 open RewardAddress
@@ -394,8 +389,8 @@ same quantity (the sum of deposits across the batch), just rephrased to expose
 
 ## `SUBLEDGERS-utxo-coin`
 
-Induct over the `SUBLEDGERS` reflexive-transitive closure, threading the
-per-`SUBUTXOW` coin equation:
+Induct over the `SUBLEDGERS` reflexive-transitive closure, applying the
+per-`SUBUTXOW` coin equation at each step:
 
 ```agda
   SUBLEDGERS-utxo-coin :
@@ -450,7 +445,7 @@ per-`SUBUTXOW` coin equation:
     ih = SUBLEDGERS-utxo-coin isV rest
 ```
 
-## `SUBLEDGERS-certs-pov`
+## `SUBLEDGERS-rewards-pov`
 
 Parallel induction over `SUBLEDGERS`, composing per-sub-transaction `SUBENTITIES-pov`
 invocations.  The `NetworkId` witnesses and domain conditions are premises of the
@@ -460,7 +455,7 @@ invocations.  The `NetworkId` witnesses and domain conditions are premises of th
 ```agda
   open SubLedgerEnv
 
-  SUBLEDGERS-certs-pov :
+  SUBLEDGERS-rewards-pov :
     {Γ : SubLedgerEnv}
     {s₀ s₁ : LedgerState}
     {stxs : List SubLevelTx}
@@ -469,12 +464,12 @@ invocations.  The `NetworkId` witnesses and domain conditions are premises of th
     →  coinFromRewards (CertStateOf s₀) + sum (map ddwl stxs)
        ≡ coinFromRewards (CertStateOf s₁) + sum (map wdrwl stxs)
 
-  SUBLEDGERS-certs-pov _ (BS-base Id-nop) = refl
+  SUBLEDGERS-rewards-pov _ (BS-base Id-nop) = refl
 
-  SUBLEDGERS-certs-pov isV (BS-ind (SUBLEDGER-I (isI , _)) _) =
+  SUBLEDGERS-rewards-pov isV (BS-ind (SUBLEDGER-I (isI , _)) _) =
     ⊥-elim (case trans (sym isV) isI of λ ())
 
-  SUBLEDGERS-certs-pov {Γ} isV (BS-ind {s = s₀} {s' = s₁} {sigs} {s'' = sₙ}
+  SUBLEDGERS-rewards-pov {Γ} isV (BS-ind {s = s₀} {s' = s₁} {sigs} {s'' = sₙ}
     (SUBLEDGER-V {stx = stx} (_ , _ , entitiesStep , _)) rest) =
     begin
       coinFromRewards (CertStateOf s₀) + (getCoin (DirectDepositsOf stx) + sum (map ddwl sigs))
@@ -495,7 +490,7 @@ invocations.  The `NetworkId` witnesses and domain conditions are premises of th
     where
     ih : coinFromRewards (CertStateOf s₁) + sum (map ddwl sigs)
          ≡ coinFromRewards (CertStateOf sₙ) + sum (map wdrwl sigs)
-    ih = SUBLEDGERS-certs-pov isV rest
+    ih = SUBLEDGERS-rewards-pov isV rest
 ```
 
 ## `SUBLEDGERS-deposits`
@@ -814,7 +809,7 @@ itself; the no-truncation bound comes from `ENTITIES-wdrls-bounded`.)
           coinFromRewards (CertStateOf s) + (subDirectDepsCoin + getCoin (DirectDepositsOf tx))
             ≡˘⟨ +-assoc (coinFromRewards (CertStateOf s)) subDirectDepsCoin (getCoin (DirectDepositsOf tx)) ⟩
           coinFromRewards (CertStateOf s) + subDirectDepsCoin + getCoin (DirectDepositsOf tx)
-            ≡⟨ cong (_+ getCoin (DirectDepositsOf tx)) (SUBLEDGERS-certs-pov valid subStep) ⟩
+            ≡⟨ cong (_+ getCoin (DirectDepositsOf tx)) (SUBLEDGERS-rewards-pov valid subStep) ⟩
           coinFromRewards cs₁ + subWdrlsCoin + getCoin (DirectDepositsOf tx)
             ≡⟨ swap-right (coinFromRewards cs₁) subWdrlsCoin (getCoin (DirectDepositsOf tx)) ⟩
           coinFromRewards cs₁ + getCoin (DirectDepositsOf tx) + subWdrlsCoin
@@ -1038,10 +1033,7 @@ The main inner chain, showing LHS + E ≡ RHS + E:
           ≡⟨ arithmetic-2 U₀ allWdrls D₀ ⟩
         U₀ + Psub + allWdrls + (D₀ + posPart dct + posPart dcs) + Ctop
           ≡⟨ cong  (λ x → x + allWdrls + (D₀ + posPart dct + posPart dcs) + Ctop)
-                   (subst  (λ u → U₀ + Psub ≡ U₁ + sum (map  (λ stx → cbalance (u ∣ SpendInputsOf stx))
-                                                             (SubTransactionsOf tx)))
-                           (refl {x = UTxOOf (UTxOStateOf s)})
-                           (SUBLEDGERS-utxo-coin valid subStep)) ⟩
+                           (SUBLEDGERS-utxo-coin valid subStep) ⟩
         U₁ + Csub + allWdrls + (D₀ + posPart dct + posPart dcs) + Ctop
           ≡⟨ cong (λ x → (U₁ + Csub) + allWdrls + x + Ctop) posneg ⟩
         U₁ + Csub + allWdrls + (D₂ + negPart dct + negPart dcs) + Ctop