Cardano Updates

For consistency with SUBUTXOW

After direct-deposit application moved from LEDGER-V/SUBLEDGER-V into the
POST-CERT rule, the Certs preservation-of-value proofs needed to account for
the `getCoin (DirectDepositsOf Γ)` increase that POST-CERT now produces via
`rewards ∪⁺ directDeposits`.

Statement changes:
- POST-CERT-pov:  getCoin s ≡ getCoin s'
              →  getCoin s + getCoin (DirectDepositsOf Γ) ≡ getCoin s'
- sts-pov:        gains a `+ getCoin (DirectDepositsOf Γ)` term on the LHS
- CERTS-pov:      becomes the symmetric "consumed = produced" form
                  getCoin s₁ + getCoin (DirectDepositsOf Γ)
                  ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)

Structural changes:
- POST-CERT-pov and sts-pov move into the parameterized `Certs-Pov-lemmas`
  sub-module (alongside PRE-CERT-pov), since they now require a fourth
  module parameter:
    indexedSumᵛ'-∪⁺ : ∀ (m m' : Rewards) → getCoin (m ∪⁺ m') ≡ getCoin m + getCoin m'
  This is the natural ∪⁺ analogue of the existing `indexedSumᵛ'-∪` lemma for
  `∪ˡ` on disjoint domains, but unconditional because `∪⁺` adds (rather than
  drops) values at shared keys.  TODO: upstream to agda-sets.
- `Certs-PoV` (in PoV.lagda.md) gains the same parameter and forwards it.

CERT-pov and PRE-CERT-pov are unchanged: the CERT and PRE-CERT rules did
not change in this refactor.

Closes part of #1185.

Per @carlostome's review of #1161, move CIP-159 direct-deposit
application out of the LEDGER/SUBLEDGER orchestration rules and into
the POST-CERT sub-rule of CERTS, alongside the existing voteDelegs
filtering.

CertEnv gains a sixth field, directDeposits, populated by LEDGER-V
(DirectDepositsOf tx) and SUBLEDGER-V (DirectDepositsOf stx) when
constructing each CERTS invocation's environment.  POST-CERT (CERT-post)
gains a premise dom directDeposits ⊆ dom rewards and updates its
post-state's rewards to rewards ∪⁺ directDeposits.

SUBLEDGER-V and LEDGER-V revert to threading-only: certStateWithDDeps,
the certStateFinal let-binding, and the dom-check premises are removed.
Computational instances are updated correspondingly.

Per-transaction semantics are preserved (POST-CERT runs at the end of
each transaction's CERTS invocation).  Phantom-asset prevention via
NoPhantomWithdrawals is unaffected (accountBalances is fixed at the
pre-batch snapshot).  depositsChange remains orthogonal
(applyDirectDeposits touches rewards only; calculateDepositsChange
reads deposits only).

Direct-deposit documentation moves from Ledger.lagda.md to the POST-CERT
section of Certs.lagda.md.

`applyDirectDeposits` uses `∪⁺` (union-with-addition) on the `rewards`
map, so a credential not present in `RewardsOf certState₂` is added as a
new entry rather than rejected.  The pre-existing SUBUTXO/UTXO premise
`dom (DirectDepositsOf tx) ⊆ dom (AccountBalancesOf Γ)` only checks
against the pre-batch balances `RewardsOf certState₀`, so it does not
catch the case where a credential is registered pre-batch, deregistered
during `CERTS`, and direct-deposited to in the same batch.  Without the
new premise, the resulting `certStateFinal` is internally inconsistent:
the credential has a positive `rewards` entry but no corresponding
`voteDelegs`, `stakeDelegs`, or `deposits` entry — effectively re-
registering the credential without a key deposit.

Add the phase-1 premise

    dom (allDirectDeposits tx) ⊆ dom (RewardsOf certState₂)

to `LEDGER-V` to rule this out.  Filtering `allDirectDeposits tx` by
`dom (RewardsOf certState₂)` would be an alternative, but it would
silently destroy user funds when a deposit and a deregistration race in
the same batch.  The premise is symmetric to (and complements) the
existing pre-batch SUBUTXO/UTXO check.

Update `Ledger/Properties/Computational.lagda.md` for the new premise,
and pass `UTxOStateOf s₁` explicitly to `computeUtxow` in the LEDGER
valid branch (the previous `_` resolved by chained unification through
the LEDGER-V constructor, which was fragile and obscured intent).

TODO: fix `Ledger/Properties/Computational.lagda.md`; it's choking on
the new premise.

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.

Each transaction's `txDirectDeposits` are now applied to the threaded
`CertState` immediately after that transaction's `CERTS` step, replacing
the batch-wide application introduced earlier on this branch.

  * `SUBLEDGER-V` applies `DirectDepositsOf stx` to `certState₁` after
    `CERTS` and emits the result.
  * `LEDGER-V` still applies the top-level transaction's deposits to
    `certState₂` after the top-level `CERTS`, but the premise now bounds
    `dom (DirectDepositsOf tx)` rather than the batch aggregate
    `dom (allDirectDeposits tx)`.
  * `certStateWithDDeps` is generalised to
    `∀ {ℓ} → Tx ℓ → CertState → CertState` so both rules can invoke it
    with the local `DirectDepositsOf`.

The original draft of this branch argued that batch-wide application
made CIP-159's phantom-asset prohibition manifest in the rule
structure.  Per-transaction application is equally safe: the prohibition
is enforced separately by `NoPhantomWithdrawals` in the `Utxo` module,
which bounds batch-wide withdrawal totals against the `accountBalances`
field of `UTxOEnv`/`SubUTxOEnv` — fixed at the pre-batch snapshot
`RewardsOf certState₀` regardless of when (or how) deposits are applied
to the threaded `CertState`.  Per-transaction application also mirrors
the Haskell ledger executor's sequential per-transaction processing,
which simplifies the conformance proof and avoids a structural gap
between the spec and the implementation.

A direct-deposit registration premise is added to each rule to prevent
`applyDirectDeposits` from silently re-introducing a credential into
`rewards` after deregistration earlier in the same transaction:

  * `SUBLEDGER-V` requires
    `dom (DirectDepositsOf stx) ⊆ dom (RewardsOf certState₁)`.
  * `LEDGER-V` requires
    `dom (DirectDepositsOf tx)  ⊆ dom (RewardsOf certState₂)`.

The check is local to each transaction's post-`CERTS` state, so a
sub-transaction whose deposit targets a credential deregistered by an
earlier sub-transaction in the same batch will fail the premise.

`Computational-SUBLEDGER` and `Computational-LEDGER` are updated to
dispatch on these decidable premises in `computeProof` and
`completeness`.  `depositsChange` is unaffected: it reads only the
protocol-deposit fields of `DState`/`PState`/`GState`, which
`applyDirectDeposits` does not touch.

Refs: #1122

Per @carlostome's review of #1161, move CIP-159 direct-deposit
application out of the LEDGER/SUBLEDGER orchestration rules and into
the POST-CERT sub-rule of CERTS, alongside the existing voteDelegs
filtering.

CertEnv gains a sixth field, directDeposits, populated by LEDGER-V
(DirectDepositsOf tx) and SUBLEDGER-V (DirectDepositsOf stx) when
constructing each CERTS invocation's environment.  POST-CERT (CERT-post)
gains a premise dom directDeposits ⊆ dom rewards and updates its
post-state's rewards to rewards ∪⁺ directDeposits.

SUBLEDGER-V and LEDGER-V revert to threading-only: certStateWithDDeps,
the certStateFinal let-binding, and the dom-check premises are removed.
Computational instances are updated correspondingly.

Per-transaction semantics are preserved (POST-CERT runs at the end of
each transaction's CERTS invocation).  Phantom-asset prevention via
NoPhantomWithdrawals is unaffected (accountBalances is fixed at the
pre-batch snapshot).  depositsChange remains orthogonal
(applyDirectDeposits touches rewards only; calculateDepositsChange
reads deposits only).

Direct-deposit documentation moves from Ledger.lagda.md to the POST-CERT
section of Certs.lagda.md.