feat(Dijkstra/Ledger/PoV): prove SUBLEDGERS-utxo-coin

Proves by induction on the SUBLEDGERS transition that the UTxO-state
coin total at the start of a sub-tx batch plus all outs + donations
equals the UTxO coin total at the end plus all consumed spend inputs
(compared against the batch-start snapshot `utxo₀`):

```agda
getCoin (UTxOStateOf s₀) + Σ (cbalance (outs stx) + DonationsOf stx)
≡ getCoin (UTxOStateOf s₁) + Σ cbalance (utxo₀ ∣ SpendInputsOf stx)
```

Base case (`BS-base Id-nop`): both sides reduce to `x + 0`, so `refl`.
Inductive case: `SUBLEDGER-I` is impossible under `isTopLevelValid ≡
true`; `SUBLEDGER-V` combines the per-step SUBUTXOW balance with the
IH via an eight-step +-commutative-monoid rearrangement.

Introduces `subutxow-step-coin` as a new module parameter:

```agda
getCoin s₀ + cbalance (outs stx) + DonationsOf stx
≡ getCoin s₁ + cbalance (UTxOOf Γ ∣ SpendInputsOf stx)
```

+  Rationale for keeping this as a parameter at the SUBLEDGERS level:
   proving it locally requires, beyond `balance-∪` and `split-balance`,
   two batch-wide invariants:

   1. the running UTxO agrees with `utxo₀` on every sub-tx's spend
      inputs, and
   2. freshness of each sub-tx's TxId relative to the running UTxO

   neither of which is a local SUBUTXO premise; both follow from
   batch-wide disjointness exposed by the outer UTXO rule and will be
   discharged in a follow-up PR dedicated to general Dijkstra PoV
   infrastructure.

Statement parallels the existing `SUBLEDGERS-certs-pov`, uses
`SubLedgerEnv.utxo₀ Γ` uniformly on the RHS (matching the shape of
`batch-balance-coin`), and is the key lemma needed to derive
`batch-utxo-accounting` internally in the next step of this PR.

Author: williamdemeo

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

@@ -206,6 +206,20 @@ module _
 
   ( setToList-Unique : ∀ (m : Withdrawals) → Unique (map (stake ∘ proj₁) (setToList (m ˢ))) )
 
+  ( balance-∪ : ∀ {u u' : UTxO} → disjoint (dom u) (dom u') → cbalance (u ∪ˡ u') ≡ cbalance u + cbalance u' )
+
+  ( split-balance : ∀ (u : UTxO) (keys : ℙ TxIn) → cbalance u ≡ cbalance (u ∣ keys ᶜ) + cbalance (u ∣ keys) )
+
+  -- Per-step SUBUTXOW coin equation.  Assumed for now; a local proof
+  -- would require, in addition to `balance-∪` and `split-balance`, a
+  -- batch-wide "spend inputs preserved" invariant (the running UTxO
+  -- agrees with the snapshot on every sub-tx's spend inputs) and
+  -- freshness of each sub-tx's TxId relative to the running UTxO.
+  -- See the follow-up PR plan.
+  ( subutxow-step-coin : ∀ {Γ : SubUTxOEnv} {s₀ s₁ : UTxOState} {stx : SubLevelTx}
+      → IsTopLevelValidFlagOf Γ ≡ true → Γ ⊢ s₀ ⇀⦇ stx ,SUBUTXOW⦈ s₁
+      → getCoin s₀ + cbalance (outs stx) + DonationsOf stx ≡ getCoin s₁ + cbalance (UTxOOf Γ ∣ SpendInputsOf stx) )
+
   -- Sub-lemmas (assumptions for now) --
 
   -- CIP-159–specific assumption: ∪⁺ adds getCoin values
@@ -228,9 +242,59 @@ module _
     open Certs-PoV ∪ˡ-res-lookup-preserve sum-map-proj₂≡getCoin setToList-Unique
     open ≡-Reasoning
 
-
-    SUBLEDGERS-certs-pov :
-      ∀ {Γ : SubLedgerEnv} {s₀ s₁ : LedgerState} {stxs : List SubLevelTx}
+    SUBLEDGERS-utxo-coin : ∀ {Γ : SubLedgerEnv} {s₀ s₁ : LedgerState} {stxs : List SubLevelTx}
+      → SubLedgerEnv.isTopLevelValid Γ ≡ true
+      → Γ ⊢ s₀ ⇀⦇ stxs ,SUBLEDGERS⦈ s₁
+      → getCoin (UTxOStateOf s₀) + sum (map (λ stx → cbalance (outs stx) + DonationsOf stx) stxs)
+        ≡ getCoin (UTxOStateOf s₁) + sum (map (λ stx → cbalance (SubLedgerEnv.utxo₀ Γ ∣ SpendInputsOf stx)) stxs)
+
+    -- Base case: empty list.  `Id-nop` unifies s₀ ≡ s₁, and
+    -- `sum (map _ []) = 0` on both sides, giving `refl`.
+    SUBLEDGERS-utxo-coin isV (BS-base Id-nop) = refl
+    -- Inductive step: one SUBLEDGER step + rest.
+    -- SUBLEDGER-I is ruled out by `isV : isTopLevelValid ≡ true`.
+    -- In the SUBLEDGER-V case, combine the per-step SUBUTXOW balance
+    -- (via `subutxow-step-coin`) with the IH using a small +-monoid shuffle.
+    SUBLEDGERS-utxo-coin {Γ} isV
+      (BS-ind {s = s₀} {s' = s₁} {sigs} {s'' = sₙ} step rest) with step
+    ... | SUBLEDGER-I (isI , _) =
+      ⊥-elim (case trans (sym isV) isI of λ ())
+    ... | SUBLEDGER-V {stx = stx} (isV' , subutxowStep , _ , _) =
+      begin
+        U₀ + (p-stx + p-sum)    ≡⟨ sym (+-assoc U₀ p-stx p-sum) ⟩
+        (U₀ + p-stx) + p-sum    ≡⟨ cong (_+ p-sum) step-P-C ⟩
+        (U₁ + c-stx) + p-sum    ≡⟨ +-assoc U₁ c-stx p-sum ⟩
+        U₁ + (c-stx + p-sum)    ≡⟨ cong (U₁ +_) (+-comm c-stx p-sum) ⟩
+        U₁ + (p-sum + c-stx)    ≡⟨ sym (+-assoc U₁ p-sum c-stx) ⟩
+        (U₁ + p-sum) + c-stx    ≡⟨ cong (_+ c-stx) ih ⟩
+        (Uₙ + c-sum) + c-stx    ≡⟨ +-assoc Uₙ c-sum c-stx ⟩
+        Uₙ + (c-sum + c-stx)    ≡⟨ cong (Uₙ +_) (+-comm c-sum c-stx) ⟩
+        Uₙ + (c-stx + c-sum)    ∎
+      where
+      -- Abbreviations for the three utxo-state coin totals.
+      U₀ = getCoin (UTxOStateOf s₀)
+      U₁ = getCoin (UTxOStateOf s₁)
+      Uₙ = getCoin (UTxOStateOf sₙ)
+      -- Per-element summands, split into "head" (stx) and "tail" (sigs).
+      p-stx = cbalance (outs stx) + DonationsOf stx
+      c-stx = cbalance (SubLedgerEnv.utxo₀ Γ ∣ SpendInputsOf stx)
+      p-sum = sum (map (λ stx → cbalance (outs stx) + DonationsOf stx) sigs)
+      c-sum = sum (map (λ stx → cbalance (SubLedgerEnv.utxo₀ Γ ∣ SpendInputsOf stx)) sigs)
+      -- Single-step coin equation from the SUBUTXOW step assumption.
+      -- (Left-associated: `U₀ + cbalance outs + donations`.)
+      step-eq : U₀ + cbalance (outs stx) + DonationsOf stx
+              ≡ U₁ + c-stx
+      step-eq = subutxow-step-coin isV' subutxowStep
+      -- Re-associate so the (cbalance outs + donations) summand is a
+      -- single term on the LHS, matching the shape of the goal.
+      step-P-C : U₀ + p-stx ≡ U₁ + c-stx
+      step-P-C = trans (sym (+-assoc U₀ (cbalance (outs stx)) (DonationsOf stx)))
+                       step-eq
+      -- Inductive hypothesis for the tail `sigs`.
+      ih : U₁ + p-sum ≡ Uₙ + c-sum
+      ih = SUBLEDGERS-utxo-coin isV rest
+
+    SUBLEDGERS-certs-pov : ∀ {Γ : SubLedgerEnv} {s₀ s₁ : LedgerState} {stxs : List SubLevelTx}
       → SubLedgerEnv.isTopLevelValid Γ ≡ true
       → Γ ⊢ s₀ ⇀⦇ stxs ,SUBLEDGERS⦈ s₁
       → getCoin (CertStateOf s₀)

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

@@ -232,6 +232,12 @@ instance
   HasDepositsChangeSub-DepositsChange : HasDepositsChangeSub DepositsChange
   HasDepositsChangeSub-DepositsChange .DepositsChangeSubOf = DepositsChange.depositsChangeSub
 
+  HasDepositsChangeTop-UTxOEnv : HasDepositsChangeTop UTxOEnv
+  HasDepositsChangeTop-UTxOEnv .DepositsChangeTopOf = DepositsChangeTopOf ∘ DepositsChangeOf
+
+  HasDepositsChangeSub-UTxOEnv : HasDepositsChangeSub UTxOEnv
+  HasDepositsChangeSub-UTxOEnv .DepositsChangeSubOf = DepositsChangeSubOf ∘ DepositsChangeOf
+
   unquoteDecl HasCast-DepositsChange
               HasCast-UTxOEnv
               HasCast-SubUTxOEnv

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

@@ -403,7 +403,7 @@ coin-of-producedBatch tx dc = begin
     swap-right a b c = trans (+-assoc a b c) (trans (cong (a +_) (+-comm b c)) (sym (+-assoc a c b)))
 
 
-module _
+module UTxO-PoV
   (tx : TopLevelTx) (let open Tx tx; open TxBody txBody)
 
   -- ASSUMPTIONS --
@@ -528,25 +528,25 @@ proof actually consumes.  We expose it as a separate lemma here.
 ```agda
   batch-balance-coin : (Γ , legacyMode) ⊢ s₀ ⇀⦇ tx ,UTXO⦈ s₁
     → cbalance (UTxOOf Γ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx)
-      + negPart (DepositsChangeTopOf (DepositsChangeOf Γ))
+      + negPart (DepositsChangeTopOf Γ)
       + sum ( map  (λ stx → cbalance (UTxOOf Γ ∣ SpendInputsOf stx) + getCoin (WithdrawalsOf stx))
                    (SubTransactionsOf tx) )
-      + negPart (DepositsChangeSubOf (DepositsChangeOf Γ))
+      + negPart (DepositsChangeSubOf Γ)
       ≡ cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + getCoin (DirectDepositsOf tx)
-        + posPart (DepositsChangeTopOf (DepositsChangeOf Γ))
+        + posPart (DepositsChangeTopOf Γ)
         + sum ( map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx))
                     (SubTransactionsOf tx))
-        + posPart (DepositsChangeSubOf (DepositsChangeOf Γ))
+        + posPart (DepositsChangeSubOf Γ)
 
   batch-balance-coin {Γ = Γ} (UTXO-⋯ _ _ _ _ _ _ _ batchBal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
     begin
-    cbalance (UTxOOf Γ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) + negPart (DepositsChangeTopOf (DepositsChangeOf Γ)) + _ + _
+    cbalance (UTxOOf Γ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) + negPart (DepositsChangeTopOf Γ) + _ + _
       ≡˘⟨ coin-of-consumedBatch tx (DepositsChangeOf Γ) (UTxOOf Γ) noMintTx noMintSubTx ⟩
     coin (consumedBatch (DepositsChangeOf Γ) tx (UTxOOf Γ))
       ≡⟨ cong coin batchBal ⟩
     coin (producedBatch (DepositsChangeOf Γ) tx)
       ≡⟨ coin-of-producedBatch tx (DepositsChangeOf Γ) ⟩
-    cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + getCoin (DirectDepositsOf tx) + posPart (DepositsChangeTopOf (DepositsChangeOf Γ)) + _ + _
+    cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + getCoin (DirectDepositsOf tx) + posPart (DepositsChangeTopOf Γ) + _ + _
       ∎
 ```
 
@@ -574,8 +574,7 @@ when combined with the `SUBLEDGERS-pov`{.AgdaFunction} lemma.
 
 ```agda
 {--
-  UTXO-pov :
-    ∀ {Γ : UTxOEnv} {legacyMode : Bool} {s₀ s₁ : UTxOState}
+  UTXO-pov : ∀ {Γ : UTxOEnv} {legacyMode : Bool} {s₀ s₁ : UTxOState}
     → TxIdOf tx ∉ mapˢ proj₁ (dom (UTxOOf s₀))
     → (Γ , legacyMode) ⊢ s₀ ⇀⦇ tx ,UTXO⦈ s₁
     → getCoin s₀

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

@@ -48,10 +48,9 @@ and `UTXOW-legacy`{.AgdaInductiveConstructor} embed a `UTXO`{.AgdaDatatype}
 derivation as their final premise.  We factor out an extractor:
 
 ```agda
-UTXOW⇒UTXO :
-  ∀ {Γ : UTxOEnv} {s s' : UTxOState} {tx : TopLevelTx}
-  → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s'
-  → ∃[ legacyMode ] ((Γ , legacyMode) ⊢ s ⇀⦇ tx ,UTXO⦈ s')
+UTXOW⇒UTXO : ∀ {Γ : UTxOEnv} {s s' : UTxOState} {tx : TopLevelTx}
+  → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' → ∃[ legacyMode ] ((Γ , legacyMode) ⊢ s ⇀⦇ tx ,UTXO⦈ s')
+
 UTXOW⇒UTXO (UTXOW-normal-⋯ _ _ _ _ _ _ _ _ _ _ utxo) = false , utxo
 UTXOW⇒UTXO (UTXOW-legacy-⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ utxo) = true , utxo
 ```
@@ -66,113 +65,51 @@ counted in `getCoin`{.AgdaField}):
 module _ (tx : TopLevelTx) (let open Tx tx; open TxBody txBody)
 
   -- Same assumptions as the UTXO-pov module.
-  ( balance-∪ : ∀ {u u' : UTxO} → disjoint (dom u) (dom u')
-              → cbalance (u ∪ˡ u') ≡ cbalance u + cbalance u' )
-
-  ( split-balance : ∀ (u : UTxO) (keys : ℙ TxIn)
-                  → cbalance u ≡ cbalance (u ∣ keys ᶜ) + cbalance (u ∣ keys) )
+  ( balance-∪ : ∀ {u u' : UTxO} → disjoint (dom u) (dom u') → cbalance (u ∪ˡ u') ≡ cbalance u + cbalance u' )
 
-  ( outs-disjoint : ∀ {u : UTxO}
-                  → TxIdOf tx ∉ mapˢ proj₁ (dom u)
-                  → disjoint (dom (u ∣ SpendInputsOf tx ᶜ)) (dom (outs tx)) )
+  ( split-balance : ∀ (u : UTxO) (keys : ℙ TxIn) → cbalance u ≡ cbalance (u ∣ keys ᶜ) + cbalance (u ∣ keys) )
 
-  ( coin-of-consumedBatch :
-      ∀ (dc : DepositsChange) (utxo₀ : UTxO)
-      → let open DepositsChange dc in
-        coin (consumedBatch dc tx utxo₀) ≡ _ )
+  ( noMintTx : coin (MintedValueOf tx) ≡ 0 )
 
-  ( coin-of-producedBatch :
-      ∀ (dc : DepositsChange)
-      → let open DepositsChange dc in
-        coin (producedBatch dc tx) ≡ _ )
+  ( noMintSubTx : noMintingSubTxs tx )
 
+  ( outs-disjoint : ∀ {u : UTxO} → TxIdOf tx ∉ mapˢ proj₁ (dom u) → disjoint (dom (u ∣ SpendInputsOf tx ᶜ)) (dom (outs tx)) )
   where
+  -- Instantiate the inner `module UTxO-PoV` of `Utxo.Properties.PoV`.
+  open UTxO-PoV tx balance-∪ split-balance noMintTx noMintSubTx
 
-  -- Instantiate the inner `module _` of `Utxo.Properties.PoV`.
-  private
-    module U =
-      Ledger.Dijkstra.Specification.Utxo.Properties.PoV
-        txs abs
-    -- `utxo-pov-mod` refers to the parameterized inner module of `U`
-    -- (the one that takes `tx` and the arithmetic assumptions).
-```
-
-```agda
-  UTXOW-I-getCoin :
-    ∀ {Γ : UTxOEnv} {s s' : UTxOState}
-    → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s'
-    → IsValidFlagOf tx ≡ false
-    → getCoin s ≡ getCoin s'
-  UTXOW-I-getCoin utxow invalid =
-    let (_ , utxo) = UTXOW⇒UTXO utxow
-    in  U-pov.UTXO-I-getCoin utxo invalid
-    where
-    -- Re-instantiate the inner module with our assumption lemmas.
-    module U-pov =
-      U tx balance-∪ split-balance outs-disjoint
-        coin-of-consumedBatch coin-of-producedBatch
+  UTXOW-I-getCoin : ∀ {Γ : UTxOEnv} {s s' : UTxOState}
+    → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' → IsValidFlagOf tx ≡ false → getCoin s ≡ getCoin s'
+  UTXOW-I-getCoin {Γ} utxow invalid = UTXO-I-getCoin (proj₂ (UTXOW⇒UTXO utxow)) invalid
 ```
 
-(The inner module instantiation is a bit boilerplate-heavy; in practice this
-should be simplified once the final module structure of `Utxo.Properties.PoV`
-is settled.)
-
 ## `UTXOW-V-mechanical`: mechanical rearrangement
 
 The valid case simply reuses the UTXO-level mechanical rearrangement:
 
 ```agda
-  UTXOW-V-mechanical :
-    ∀ {Γ : UTxOEnv} {s s' : UTxOState}
-    → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s'
-    → IsValidFlagOf tx ≡ true
-    → TxIdOf tx ∉ mapˢ proj₁ (dom (UTxOOf s))
+  UTXOW-V-mechanical : ∀ {Γ : UTxOEnv} {s s' : UTxOState}
+    → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' → IsValidFlagOf tx ≡ true → TxIdOf tx ∉ mapˢ proj₁ (dom (UTxOOf s))
     → getCoin s + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx
       ≡ getCoin s' + cbalance (UTxOOf s ∣ SpendInputsOf tx)
-  UTXOW-V-mechanical utxow valid fresh =
-    let (_ , utxo) = UTXOW⇒UTXO utxow
-    in  U-pov.UTXO-V-mechanical utxo valid fresh
-    where
-    module U-pov =
-      U tx balance-∪ split-balance outs-disjoint
-        coin-of-consumedBatch coin-of-producedBatch
+
+  UTXOW-V-mechanical utxow valid fresh = UTXO-V-mechanical (proj₂ (UTXOW⇒UTXO utxow)) valid fresh
 ```
 
 ## `UTXOW-batch-balance-coin`
 
 ```agda
-  UTXOW-batch-balance-coin :
-    ∀ {Γ : UTxOEnv} {s s' : UTxOState}
+  UTXOW-batch-balance-coin : ∀ {Γ : UTxOEnv} {s s' : UTxOState}
     → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s'
-    → let dc = DepositsChangeOf Γ
-          utxo₀ = UTxOOf Γ
-          open DepositsChange dc
-      in  cbalance (utxo₀ ∣ SpendInputsOf tx)
-        + getCoin (WithdrawalsOf tx)
-        + negPart depositsChangeTop
-        + sum (map (λ (stx : SubLevelTx) →
-                       cbalance (utxo₀ ∣ SpendInputsOf stx)
-                       + getCoin (WithdrawalsOf stx))
-                    (SubTransactionsOf tx))
-        + negPart depositsChangeSub
-        ≡ cbalance (outs tx)
-        + TxFeesOf tx
-        + DonationsOf tx
-        + getCoin (DirectDepositsOf tx)
-        + posPart depositsChangeTop
-        + sum (map (λ (stx : SubLevelTx) →
-                       cbalance (outs stx)
-                       + DonationsOf stx
-                       + getCoin (DirectDepositsOf stx))
-                    (SubTransactionsOf tx))
-        + posPart depositsChangeSub
-  UTXOW-batch-balance-coin utxow =
-    let (_ , utxo) = UTXOW⇒UTXO utxow
-    in  U-pov.batch-balance-coin utxo
-    where
-    module U-pov =
-      U tx balance-∪ split-balance outs-disjoint
-        coin-of-consumedBatch coin-of-producedBatch
+    → cbalance (UTxOOf Γ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx)
+      + negPart (DepositsChangeTopOf Γ)
+      + sum (map (λ stx → cbalance (UTxOOf Γ ∣ SpendInputsOf stx) + getCoin (WithdrawalsOf stx)) (SubTransactionsOf tx))
+      + negPart (DepositsChangeSubOf Γ)
+      ≡ cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + getCoin (DirectDepositsOf tx)
+        + posPart (DepositsChangeTopOf Γ)
+        + sum ( map (λ (stx : SubLevelTx) → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) (SubTransactionsOf tx) )
+        + posPart (DepositsChangeSubOf Γ)
+  UTXOW-batch-balance-coin utxow = batch-balance-coin (proj₂ (UTXOW⇒UTXO utxow))
 ```
 
 ## `utxow-pov-invalid` for use in `LEDGER-pov`
@@ -182,11 +119,8 @@ The following is the *specific* form needed by `Ledger.Properties.PoV`
 identical to `UTXOW-I-getCoin`{.AgdaFunction} above, retagged for clarity:
 
 ```agda
-  utxow-pov-invalid :
-    ∀ {Γ : UTxOEnv} {s s' : UTxOState}
-    → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s'
-    → IsValidFlagOf tx ≡ false
-    → getCoin s ≡ getCoin s'
+  utxow-pov-invalid : ∀ {Γ : UTxOEnv} {s s' : UTxOState}
+    → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' → IsValidFlagOf tx ≡ false → getCoin s ≡ getCoin s'
   utxow-pov-invalid = UTXOW-I-getCoin
 ```