Apply CIP-159 direct deposits per-transaction, not batch-wide
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