Cardano Updates

Co-authored-by: Carlos Tomé Cortiñas <[email protected]>

Co-authored-by: Carlos Tomé Cortiñas <[email protected]>

Co-authored-by: Carlos Tomé Cortiñas <[email protected]>

Co-authored-by: Carlos Tomé Cortiñas <[email protected]>

Closes #1114 by adding the two new transaction body fields required by [CIP-159](https://github.com/cardano-foundation/CIPs/tree/master/CIP-0159) (Account Address Enhancement) to the Dijkstra-era `TxBody` record, along with type class accessors and batch-wide aggregation helpers.

Closes #1113

This PR completes the formalization of the computational instance for the `UTXOW` transition rule in the Dijkstra era.

+  **Record-Based Premises**.
   Refactored the transition rules to use named record types for premises (`UTXOW-Normal-Premises`, `UTXOW-Legacy-Premises`, `SUBUTXOW-Premises`). This significantly improves type-checking performance and scannability compared to the previous nested-tuple approach.
+  **WitnessData Consolidation**.
   Centralized the logic for collecting vKey hashes, scripts, and data hashes into a `WitnessData` record to avoid redundant lookups and simplify the decider logic.
+  **Era Toggle Logic**.
   Introduced a boolean `v1-v3-allowed` flag to the `UTXOW` mode
   records; this provides a simpler decidable mechanism to distinguish between Dijkstra-native (Normal/V4) and compatibility (Legacy/V1-V3) modes (but we should be able to prove it using other premises instead (TODO)).
+  **Completeness Proof**. (TODO: finish implementing completeness proof for `UTXOW`.)

+  Finalize `normal-legacy-exclusive` lemma logic, removing temporary boolean toggle if an intrinsic proof based on script pool contents is possible.
+  Expand the `failure` strings into more descriptive error messages using a structured error type.