Cardano Updates

Signed-off-by: Ritesh Pandit <[email protected]>

Signed-off-by: Ritesh Pandit <[email protected]>

Signed-off-by: Ritesh Pandit <[email protected]>

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

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

Add build-raw reference script spending test

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

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