[Dijkstra] Refactor ENTITIES and add SUBENTITIES

[carlostome]

Description

In particular closes #1251 and #1252.

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]

Nice work so far, Carlos!

Spinning SUBENTITIES out of ENTITIES, indexing both by the (sub-)transaction, and actually enforcing phantom-asset prevention is good progress.

That said, a number of things are still incomplete/need attention (some of which you're surely aware of, but I'll mention them anyway, just to be sure).

Computational instances and Foreign types

• src/Ledger/Dijkstra/Specification/Utxo/Properties/Computational.lagda.md

  UTXO lost 5 premises, so the 23-component premise tuples no longer parse; same for the 24-argument pattern UTXO-⋯ at src/Ledger/Dijkstra/Specification/Utxo.lagda.md:538, and the 17-component SUBUTXO tuples at lines 51--52 once the sub-level move is finished (see Question 1).

• src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md

  still instantiates Entities govStructure (lines 25--26), renames the deleted SubLedgerEnv.certState (line 109), builds the old six-field EntitiesEnv (lines 117, 226), and calls ENTITIES at List DCert (lines 133, 245). Computational-SUBLEDGER needs rewiring onto the new Computational-SUBENTITIES.

• src/Ledger/Dijkstra/Foreign/Entities.agda old module parameter (DummyGovStructure) and old EntitiesEnv mirror; entities-step becomes EntitiesEnv → CertState → Tx TxLevelTop → ....

Semantics to confirm

These are possibly intended, but I just want to be sure because the behavior changed.

• Balance intervals are now checked against the current threaded rewards (top-level: post-SUBLEDGERS; sub-level: at that sub-tx), not the pre-batch snapshot as before.

• withdrawalsCredentials ⊆ dom rewards₀ (Entities.lagda.md:156,196) forbids any withdrawal — including withdraw-0, the standard Plutus stake-script invocation pattern — from an account registered earlier in the same batch.

• There is no per-sub-transaction withdrawal amount check anymore; the top-level aggregate against rewards₀ is the only bound. I convinced myself this composes soundly — mid-batch balances can't drop below rewards₀ − withdrawnSoFar, because DELEG-dereg requires a zero balance and registration starts at 0, so applyWithdrawals's truncating _∸_ never actually truncates inside a valid LEDGER derivation — but that invariant deserves a sentence of prose, and standalone SUBENTITIES derivations do admit overdrawing.

• Several phase-1 checks became valid-path-only. The network-id / DD-registration / balance-interval checks previously lived in UTXO, which also runs (via UTXOW) in LEDGER-I; ENTITIES/SUBENTITIES run only on the valid path. So an isValid = false transaction with a wrong-network withdrawal address or a violated balance interval is now accepted (collateral consumed) where it was previously rejected, and the docs this PR deletes called the interval check "a Phase-1 validity condition". Is that intended? This applies to the whole #1251/#1252 move; the fixes branch follows the move, but we need an explicit decision.

Minor

• allWithdrawals (Transaction.lagda.md:724) is dead code now that NoPhantomWithdrawals is gone

• the phantom-asset rationale prose vanished entirely and should reappear in Entities.lagda.md next to the rewards₀ premises

• the SUBUTXO doc items 4-5 (Utxo.lagda.md:434-439) still say "pre-batch";

• dead renaming (filterˢ to filter) at Entities.lagda.md:17

• the CHANGELOG.md contains a leftover stale entry referencing #1117: "balance interval assertions will be checked per-(sub)transaction in UTXO/SUBUTXO rules" that we should delete.

[williamdemeo]

Excellent! LGTM!!