Cardano Updates

Thanks @carlostome for point out this oversight.

CIP-159 changes withdrawal semantics from "all-or-nothing" (withdrawal
amount must equal the full account balance) to "partial" (any amount up
to the current balance may be withdrawn).

`Certs.lagda.md`:
+  Define _≤ᵐ_ relation and Dec-≤ᵐ decision procedure for comparing a
   Coin value against a Maybe Coin (just bal → amt ≤ bal; nothing → ⊥).
+  Define applyWithdrawals helper (fold-based pointwise subtraction of
   withdrawal amounts from account balances).
+  Relax PRE-CERT precondition to three premises: credential is a
   registered key hash, credential is in dom rewards, and withdrawal
   amount ≤ balance (via ≤ᵐ with lookupᵐ?).
+  Update PRE-CERT effect from zeroing withdrawn credentials to pointwise
   subtraction via applyWithdrawals.
+  Document partial withdrawal semantics and version restriction deferral.

`Certs/Properties/Computational.lagda.md`:
+  Add scoped ⁇-≤ᵐ instance (positioned after DELEG/POOL/GOVCERT/CERT
   proofs to avoid instance pollution).
+  Update Computational-PRE-CERT for the new three-premise precondition.

Per feedback from @carlostome: balance interval assertions should be
checked per-(sub)transaction in the UTXO and SUBUTXO rules, analogously
to how slot validity intervals are already checked.  This eliminates the
need for batch-level aggregation of balance intervals and the associated
domain-disjointness constraint.

Removed:
+  "Account Balance Intervals" prose subsection
+  `allBalanceIntervals : TopLevelTx → AccountBalanceIntervals` helper
+  Footnote [^2] referencing Issue #1117

The `txBalanceIntervals` field on `TxBody` and the `BalanceIntervalsOf`
type class accessor (both introduced in #1114) are unchanged; they
provide per-(sub)transaction access, which is exactly what the UTXO and
SUBUTXO rules need.

Direct deposits (`allDirectDeposits`) still require batch-level
aggregation because they are an additive state update; balance intervals,
being pure precondition checks, do not.

See Issue #1117 for the per-transaction checking design.

CIP-159 changes withdrawal semantics from "all-or-nothing" (withdrawal
amount must equal the full account balance) to "partial" (any amount up
to the current balance may be withdrawn).

`Certs.lagda.md`:
+  Define _≤ᵐ_ relation and Dec-≤ᵐ decision procedure for comparing a
   Coin value against a Maybe Coin (just bal → amt ≤ bal; nothing → ⊥).
+  Define applyWithdrawals helper (fold-based pointwise subtraction of
   withdrawal amounts from account balances).
+  Relax PRE-CERT precondition to three premises: credential is a
   registered key hash, credential is in dom rewards, and withdrawal
   amount ≤ balance (via ≤ᵐ with lookupᵐ?).
+  Update PRE-CERT effect from zeroing withdrawn credentials to pointwise
   subtraction via applyWithdrawals.
+  Document partial withdrawal semantics and version restriction deferral.

`Certs/Properties/Computational.lagda.md`:
+  Add scoped ⁇-≤ᵐ instance (positioned after DELEG/POOL/GOVCERT/CERT
   proofs to avoid instance pollution).
+  Update Computational-PRE-CERT for the new three-premise precondition.

Co-authored-by: Copilot <[email protected]>

Extend `UsesV4Features` to detect CIP-159 transaction fields and update
`allowedLanguagesLegacyMode` to forbid them in legacy mode.

+  Add hasDirectDeposits and hasBalanceIntervals constructors to
   `UsesV4Features`, detecting non-empty
   `txDirectDeposits`/`txBalanceIntervals`.
+  Prepend `UsesV4Features` check to `allowedLanguagesLegacyMode`,
   returning ∅ when V4 features are present (making legacy rule unsatisfiable).
+  Update `Dec-UsesV4Features` instance for the two new constructors.
+  Document the CIP-159/CIP-118 interaction for version gating.

No changes to `Utxow/Properties/Computational.lagda.md`; premise shapes are
unchanged since no new fields are added to `UTXOW-legacy` or `UTXOW-normal`.

Extend the Plutus script context (TxInfo) with the two new CIP-159
transaction fields and document that credsNeeded requires no changes.

+  `ScriptPurpose.lagda.md`
   + Add txDirectDeposits : DirectDeposits to TxInfo.
   + Add txBalanceIntervals : AccountBalanceIntervals to TxInfo.
   + Document pre-emptive upgrade rationale and absence of new ScriptPurpose values.

+  `Validation.lagda.md`
   +  Populate new TxInfo fields in both txInfo TxLevelTop and txInfo
      TxLevelSub using DirectDepositsOf/BalanceIntervalsOf accessors.
   +  Document that credsNeeded does not need changes for CIP-159.