Cardano Updates

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`.
+  Clean up redundant code.

Add batch-wide withdrawal bound check to prevent phantom asset attacks
when nested transactions combine deposits and withdrawals.

`Transaction.lagda.md`:
+  Define allWithdrawals batch aggregation helper (mirrors
   allDirectDeposits)

`Utxo.lagda.md`:
+  Define NoPhantomWithdrawals predicate using allWithdrawals
+  Add NoPhantomWithdrawals premise to UTXO rule
+  Document phantom asset attack and spend-side safety analogy

`Utxo/Properties/Computational.lagda.md`:
+  Update Computational-UTXO for new premise tuple arity (21+h → 22+h)

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`.
+  Clean up redundant code.

CIP-159 changes the transaction balancing rules and introduces Phase-1
balance interval validation.  This commit updates the UTxO transition
system accordingly.

`Utxo.lagda.md`:
+  Add accountBalances : Rewards field to UTxOEnv and SubUTxOEnv for
   pre-batch account balance lookups;
+  Add HasAccountBalances type class and instances;
+  Update producedTx to include direct deposit amounts on the produced
   side of the preservation-of-value equation;
+  Add direct deposit registration premise to UTXO and SUBUTXO
   (`dom DirectDepositsOf ⊆ dom AccountBalancesOf`);
+  Add balance interval validation premise to UTXO and SUBUTXO
   (∀ (c,interval) ∈ BalanceIntervalsOf, InBalanceInterval using
   pre-batch account balances).

`Utxo/Properties/Computational.lagda.md`:
+  Update Computational-UTXO for new premise tuple arity (19+h → 21+h)

`Ledger.lagda.md`:
+  Add accountBalances field to SubLedgerEnv;
+  Populate accountBalances in SUBLEDGER-V, SUBLEDGER-I, LEDGER-V,
   LEDGER-I using RewardsOf certState₀ (pre-batch balances).

Added check: if a balance interval constraint is specified for a
credential, then that credential belongs to the domain of
`AccountBalancesOf Γ`; see Carlos' comment:

https://github.com/IntersectMBO/formal-ledger-specifications/pull/1160#discussion_r3110584513

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.

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`.
+  Clean up redundant code.

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`.

CIP-159 changes the transaction balancing rules and introduces Phase-1
balance interval validation.  This commit updates the UTxO transition
system accordingly.

`Utxo.lagda.md`:
+  Add accountBalances : Rewards field to UTxOEnv and SubUTxOEnv for
   pre-batch account balance lookups;
+  Add HasAccountBalances type class and instances;
+  Update producedTx to include direct deposit amounts on the produced
   side of the preservation-of-value equation;
+  Add direct deposit registration premise to UTXO and SUBUTXO
   (`dom DirectDepositsOf ⊆ dom AccountBalancesOf`);
+  Add balance interval validation premise to UTXO and SUBUTXO
   (∀ (c,interval) ∈ BalanceIntervalsOf, InBalanceInterval using
   pre-batch account balances).

`Utxo/Properties/Computational.lagda.md`:
+  Update Computational-UTXO for new premise tuple arity (19+h → 21+h)

`Ledger.lagda.md`:
+  Add accountBalances field to SubLedgerEnv;
+  Populate accountBalances in SUBLEDGER-V, SUBLEDGER-I, LEDGER-V,
   LEDGER-I using RewardsOf certState₀ (pre-batch balances).

See https://github.com/agda/agda/issues/8532