feat(dijkstra): discharge coin-of-{consumed,produced}Batch in UTXO PoV

Replace the two `coin-of-consumedBatch` / `coin-of-producedBatch` module
parameters of `Utxo/Properties/PoV` with direct proofs.  The proofs are
organised as three layers:

+  Layer 1 — single-transaction coin equations

   `coin-producedTx : coin (producedTx t) ≡ cbalance (outs t) + DonationsOf t + getCoin (DirectDepositsOf t)`

   `coin-consumedTx : coin (MintedValueOf t) ≡ 0 → coin (consumedTx t utxo₀) ≡ cbalance (utxo₀ ∣ SpendInputsOf t) + getCoin (WithdrawalsOf t)`

   Each is a direct unfolding: repeated `∙-homo-Coin` to distribute `coin`
   across `+`, followed by `coin∘inject≗id` to strip each `inject`.  The
   consumed version additionally uses `coin (MintedValueOf t) ≡ 0` to cancel
   the mint term (from UTXO premise p₆ / SUBUTXO premise).

+  Layer 2 — sum-over-sub-transactions coin equations

   `coin-∑-producedTx-sub` : pushes `coin` through the `∑ˡ`-indexed sum over
   `SubTransactionsOf tx` using the new `coin-∑ˡ` lemma (from
   `Utxo/Properties/Base`), then applies Layer 1 pointwise by list induction.

   `coin-∑-consumedTx-sub` : same shape, threading a `noMintingSubTxs tx`
   hypothesis (`∀ stx → stx ∈ˡ SubTransactionsOf tx → coin (MintedValueOf stx) ≡ 0`)
   through the induction so each element's Layer-1 application has its
   `noMint` premise available.

+  Layer 3 — the two batch-level coin equations

   `coin-of-consumedBatch` and `coin-of-producedBatch`: unfold the outer
   `+ inject _` / `+ ∑ˡ _` structure of `consumedBatch` / `producedBatch` by
   repeated `∙-homo-Coin` and `coin∘inject≗id`, substitute the Layer-1
   top-level equation for the top-level summand, and substitute the Layer-2
   equation for the sub-transaction sum.

   The produced-side proof ends with a small associative-commutative shuffle
   (`reshape-top`) that reorders the top-level fields from
   `(outs + Donations + DirectDeposits) + TxFees` to the stated
   `outs + TxFees + Donations + DirectDeposits`.  The shuffle uses the same
   `swap-right` helper already used in `UTXO-V-mechanical`.

+  Supporting change

   Adds a small helper alias `noMintingSubTxs` at the top of the file to keep
   the sub-level mint-conservation hypothesis readable in the theorem
   statements.

All proofs typecheck under `--safe`.  The `UTXO-pov` placeholder remains;
this commit delivers the coin-balance infrastructure that the eventual
full proof (and the LEDGER-pov's `BatchUtxoAccounting` consumer) will
depend on.

Author: williamdemeo

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

@@ -141,6 +141,14 @@ record HasDepositsChange {a} (A : Type a) : Type a where
   field DepositsChangeOf : A → DepositsChange
 open HasDepositsChange ⦃...⦄ public
 
+record HasDepositsChangeTop {a} (A : Type a) : Type a where
+  field DepositsChangeTopOf : A → ℤ
+open HasDepositsChangeTop ⦃...⦄ public
+
+record HasDepositsChangeSub {a} (A : Type a) : Type a where
+  field DepositsChangeSubOf : A → ℤ
+open HasDepositsChangeSub ⦃...⦄ public
+
 record HasScriptPool {a} (A : Type a) : Type a where
   field ScriptPoolOf : A → ℙ Script
 open HasScriptPool ⦃...⦄ public
@@ -209,6 +217,12 @@ instance
   HasDonations-UTxOState : HasDonations UTxOState
   HasDonations-UTxOState .DonationsOf = UTxOState.donations
 
+  HasDepositsChangeTop-DepositsChange : HasDepositsChangeTop DepositsChange
+  HasDepositsChangeTop-DepositsChange .DepositsChangeTopOf = DepositsChange.depositsChangeTop
+
+  HasDepositsChangeSub-DepositsChange : HasDepositsChangeSub DepositsChange
+  HasDepositsChangeSub-DepositsChange .DepositsChangeSubOf = DepositsChange.depositsChangeSub
+
   unquoteDecl HasCast-DepositsChange
               HasCast-UTxOEnv
               HasCast-SubUTxOEnv
@@ -303,6 +317,16 @@ collateralCheck pp txTop utxo =
   × coin (balance (utxo ∣ CollateralInputsOf txTop)) * 100 ≥ (TxFeesOf txTop) * pp .collateralPercentage
   × (CollateralInputsOf txTop) ≢ ∅
 
+producedTx : Tx ℓ → Value
+producedTx tx = balance (outs tx)
+                + inject (DonationsOf tx)
+                + inject (getCoin (DirectDepositsOf tx))
+
+consumedTx : Tx ℓ → UTxO → Value
+consumedTx tx utxo = balance (utxo ∣ SpendInputsOf tx)
+                     + MintedValueOf tx
+                     + inject (getCoin (WithdrawalsOf tx))
+
 module _ (depositsChange : DepositsChange) where
 
   open DepositsChange depositsChange
@@ -319,11 +343,6 @@ module _ (depositsChange : DepositsChange) where
   depositRefundsTop : Coin
   depositRefundsTop = negPart depositsChangeTop
 
-  consumedTx : Tx ℓ → UTxO → Value
-  consumedTx tx utxo = balance (utxo ∣ SpendInputsOf tx)
-                       + MintedValueOf tx
-                       + inject (getCoin (WithdrawalsOf tx))
-
   consumed : TopLevelTx → UTxO → Value
   consumed txTop utxo = consumedTx txTop utxo
                         + inject depositRefundsTop
@@ -340,11 +359,6 @@ In the preservation-of-value equation, direct deposits appear on the
 the transaction and that amount is deposited into accounts.
 
 ```agda
-  producedTx : Tx ℓ → Value
-  producedTx tx = balance (outs tx)
-                  + inject (DonationsOf tx)
-                  + inject (getCoin (DirectDepositsOf tx))
-
   produced : TopLevelTx → Value
   produced txTop = producedTx txTop
                    + inject (TxFeesOf txTop)

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

@@ -14,4 +14,6 @@ module Ledger.Dijkstra.Specification.Utxo.Properties where
 
 ```agda
 open import Ledger.Dijkstra.Specification.Utxo.Properties.Computational
+open import Ledger.Dijkstra.Specification.Utxo.Properties.Base
+open import Ledger.Dijkstra.Specification.Utxo.Properties.PoV
 ```

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

@@ -58,6 +58,22 @@ private variable
 ∙-homo-Coin = IsMagmaHomomorphism.homo (isMagmaHomomorphism coinIsMonoidHomomorphism)
 ```
 
+## `coin-∑ˡ`
+
+`coin`{.AgdaField} is a monoid homomorphism from `Value`{.AgdaField} (under `+ᵛ`/`ε`) to
+`ℕ`{.AgdaDatatype} (under `+`/`0`), so it distributes over a list-indexed sum.  This
+is the "coin version" of the generic fact that a monoid homomorphism commutes with
+`foldr _∙_ ε`.
+
+```agda
+coin-∑ˡ : ∀ {A : Type} (f : A → Value) (xs : List A)
+        → coin (∑ˡ[ x ← xs ] f x) ≡ sum (map (coin ∘ f) xs)
+coin-∑ˡ f []       = ε-homo coinIsMonoidHomomorphism
+coin-∑ˡ f (x ∷ xs) = trans  (∙-homo-Coin (f x) (∑ˡ[ z ← xs ] f z))
+                            (cong (coin (f x) +_) (coin-∑ˡ f xs))
+```
+
+
 ## Freshness ⇒ disjointness
 
 ```agda