[Dijkstra] Add starting account balance intervals

[carlostome]

Description

Following the changes in cardano-ledger (IntersectMBO/cardano-ledger#6001) and the amendments to the CIP (cardano-foundation/CIPs#1243)

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]

Approved with some minor, non-blocking comments.

Question (not a change request). A non-empty txBalanceIntervals makes UsesV4Features tx hold (hasBalanceIntervals in Utxow), which makes allowedLanguagesLegacy exclude V1--V3 scripts, so a transaction carrying a non-empty txBalanceIntervals cannot run V1--V3 scripts. Otoh, a non-empty txStartingBalanceIntervals has no such restriction, since it is not a UsesV4Features constructor.

Is that intentional? The restriction to V4 for non-empty txBalanceIntervals seems reasonable. But I don't see why the same restriction shouldn't hold for a non-empty txStartingBalanceIntervals.

Follow-up suggestion. This PR shows once again how brittle the sts rule patterns are. In this case, in ENTITIES, one premise insertion touched five pattern sites across Computational and PoV, and the eleven-tuple is mostly underscores.

(In my recent properties PRs, I battled with the same issue again.)

Utxow solves this with genPremises and a ⋯ pattern synonym (see Utxow.lagda.md:539-542). A follow-up doing the same for ENTITIES and SUBENTITIES would let the PoV proofs name certsStep and ddCreds⊆ instead of counting positions. I think you mentioned you planned to tackle the genPremises problems soon. Maybe this can be part of that work.

[carlostome]

Follow-up suggestion. This PR shows once again how brittle the sts rule patterns are. In this case, in ENTITIES, one premise insertion touched five pattern sites across Computational and PoV, and the eleven-tuple is mostly underscores.

(In my recent properties PRs, I battled with the same issue again.)

Utxow solves this with genPremises and a ⋯ pattern synonym (see Utxow.lagda.md:539-542). A follow-up doing the same for ENTITIES and SUBENTITIES would let the PoV proofs name certsStep and ddCreds⊆ instead of counting positions. I think you mentioned you planned to tackle the genPremises problems soon. Maybe this can be part of that work.

I agree but atm genPremises doesn't work for ENTITIES.