[Dijkstra] Move normal/legacy mode decision to LEDGER

[williamdemeo]

Description

Closes #1258.

Previously the normal-vs-legacy decision lived in two places that could disagree: UTXOW chose a mode nondeterministically via its two rules (feeding false/true into UTXO's self-balance premise), while LEDGER-V passed a hardcoded true to ENTITIES — making the legacyMode ≡ false branch of ENTITIES (partial top-level withdrawals) unreachable and letting an all-V4 transaction get normal-mode UTxO accounting but legacy-mode withdrawal treatment.

This PR makes the decision once, in LEDGER, and threads the result through the rules' environments.

Changes

• Utxow: new neededP2Scripts and isLegacyMode : UTxO → ℙ Script → TopLevelTx → Bool — legacy exactly when some needed phase-2 script uses a pre-V4 Plutus language (the same criterion Computational-UTXOW already used to dispatch). UTXOW-normal/UTXOW-legacy gain a first premise LegacyModeOf Γ ≡ false/≡ true and pass Γ to UTXO unchanged. Their language premises remain as checks, so the environment flag is validated rather than trusted, and each rule keeps its standalone meaning.

• Utxo: UTxOEnv gains a named legacyMode : Bool field (mirroring how isTopLevelValid is threaded via SubUTxOEnv), with a HasLegacyMode/LegacyModeOf accessor. UTXO's environment is plain UTxOEnv again instead of UTxOEnv × Bool.

• Ledger: LEDGER-V/LEDGER-I compute legacyMode = isLegacyMode utxo₀ allScripts tx and thread it to UTXOW/UTXO via UTxOEnv and to ENTITIES via EntitiesEnv, replacing the hardcoded true. All three rules now see one consistent flag.

• Computational: Computational-UTXOW dispatches on the flag premises, which removes the DecV3 decision and the V1,V2,V3∩V4⊆∅ disjointness lemma; Computational-UTXO loses the product-env plumbing; Computational-LEDGER mirrors the new rule environments.

• Foreign/Utxo: utxo-step is now UTxOEnv → UTxOState → Tx TxLevelTop → … (the flag moved into the auto-derived MkUTxOEnv; no Haskell consumers exist yet).

Verification

The full Ledger.Dijkstra aggregate typechecks (Agda 2.8.0 via the Nix flake), as does Specification/Computational.lagda.md, which sits outside the aggregate's import graph. No modules outside src/Ledger/Dijkstra import the changed ones.

Out of scope

The legacy-mode withdrawal gap is not fixed here: the ENTITIES legacy branch still requires the top-level withdrawal to equal the current (post-SUBLEDGERS) balance with no rewards₀ bound, and UsesV4Features only inspects top-level fields, so a legacy batch can still carry sub-transactions with direct deposits and drain them. This is now tracked in Issue #1261.

🤖 Generated with Claude Code

Checked/revised by @williamdemeo

Checklist

• Commit sequence broadly makes sense and commits have useful messages
• Any semantic changes to the specifications are documented in CHANGELOG.md
• Code is formatted according to CONTRIBUTING.md
• Self-reviewed the diff

[williamdemeo]

replace with isLegacymode = false check.

[williamdemeo]

replace with isLegacymode = true

[carlostome]

LGTM! (modulo the comments we discussed)