Cardano Updates

Co-Authored-By: Claude Sonnet 4.6 <[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`.

Address Carlos's review: `allowedLanguagesLegacyMode` is intended for use
*within* legacy mode to select among V1–V3 versions, not to gate entry
into legacy mode.

`Utxow.lagda.md`:
+  Revert allowedLanguagesLegacyMode to its original form (remove
   UsesV4Features check)
+  Add explicit `Is-∅ (dom txDirectDeposits)` and
   `Is-∅ (dom txBalanceIntervals)` premises to UTXOW-legacy
+  Update `UTXOW-legacy-⋯` pattern synonym for 13 premises
+  Revise documentation to describe the premise-based approach

`Utxow/Properties/Computational.lagda.md`:
+  Update computeProof and completeness for the new legacy tuple arity.

Test hangs in the nix build sandbox: a Python multiprocessing.Pool
deadlock (`_help_stuff_finish` acquires `inqueue._rlock` without
releasing) combined with a leaked signal mask that leaves SIGTERM
blocked in the worker means `pool.terminate()` can't kill it.
nix-shell builds complete fine; only nix-build hangs.

Address Carlos's review: `allowedLanguagesLegacyMode` is intended for use
*within* legacy mode to select among V1–V3 versions, not to gate entry
into legacy mode.

`Utxow.lagda.md`:
+  Revert allowedLanguagesLegacyMode to its original form (remove
   UsesV4Features check)
+  Add explicit `Is-∅ (dom txDirectDeposits)` and
   `Is-∅ (dom txBalanceIntervals)` premises to UTXOW-legacy
+  Update `UTXOW-legacy-⋯` pattern synonym for 13 premises
+  Revise documentation to describe the premise-based approach

`Utxow/Properties/Computational.lagda.md`:
+  Update computeProof and completeness for the new legacy tuple arity.

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

Much simpler and maintains the correct/intended semantics.

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.

Update roadmap.md

Signed-off-by: Ales Verbic <[email protected]>

* fix(ledger): emit LedgerErrorEvent when rollback tx undo decode fails

Signed-off-by: cryptodj413 <[email protected]>

* fix(ledger): address ai review

Signed-off-by: cryptodj413 <[email protected]>

---------

Signed-off-by: cryptodj413 <[email protected]>

Signed-off-by: dependabot[bot] <[email protected]>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>