Cardano Updates

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

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.

+  reduce WitnessData record type to just two fields---the fields that
   differ depending on normal/legacy mode.
+  remove duplicate collectWitnessDataLegacy function, by adding
   branching (normal vs legacy) logic to collectWitnessData
+  add support for normal vs legacy mode to LEDGER rule