Cardano Updates

* Improve `(SUB)UTXOW` `Computational` instance type checking speed

* Improve type checking speed of some equalities

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.

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.

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.

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.

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.

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.

After all sub-rule transitions (`SUBLEDGERS`, `CERTS`, `GOVS`, `UTXOW`),
apply batch-wide direct deposits to the final CertState via
`applyDirectDeposits` and `allDirectDeposits`.

`Ledger.lagda.md`:
+  Update `LEDGER-V` output: compute `certStateFinal` by applying
   `allDirectDeposits` to `certState₂`, use `certStateFinal` in the
   output `LedgerState` and in `rmOrphanDRepVotes`;
+  `LEDGER-I` unchanged (invalid batches don't apply deposits);
+  Document direct deposit application ordering and phantom asset
   prevention rationale.

`Ledger/Properties/Computational.lagda.md`:
+  Update `computeProof` valid branch to compute `certStateFinal` and use
   it in the output `LedgerState`.