[Dijkstra] Foreign step functions for new sub-rules

[williamdemeo]

Background

PR #1134 adds the Dijkstra Foreign modules. Top-level rules (LEDGER, LEDGERS, UTXO, UTXOW, CERT, CERTS, DELEG, POOL, GOVCERT, GOV, GOVS, ENACT, EPOCH, NEWEPOCH, RATIFY, RATIFIES, CHAIN) all have foreign step functions. The new Dijkstra SUB* rules (SUBLEDGER, SUBLEDGERS, SUBUTXO, SUBUTXOW) do not.

Why this matters

Per-rule conformance is how divergences between the Agda spec and the Haskell ledger get localized. End-to-end via ledgers-step exercises the sub-rules transitively, but a failure that originates inside, say, SUBUTXO will show up as a LEDGERS failure with no easy way to attribute it.

Scope

Add to Ledger/Dijkstra/Foreign/Ledger.lagda.md:

• subledger-step : HsType (SubLedgerEnv → LedgerState → Tx TxLevelSub → ComputationResult String LedgerState)
• subledgers-step : HsType (SubLedgerEnv → LedgerState → List (Tx TxLevelSub) → ComputationResult String LedgerState)

Add to Ledger/Dijkstra/Foreign/Utxo.lagda.md:

• subutxo-step : HsType (SubUTxOEnv → UTxOState → Tx TxLevelSub → ComputationResult String UTxOState)
• subutxow-step : HsType (SubUTxOEnv → UTxOState → Tx TxLevelSub → ComputationResult String UTxOState)

Re-export each from MAlonzo.Code.Ledger.Dijkstra.Foreign.API.

Notes

• The exact env/state/signal types should match Computational-SUBLEDGER/-SUBLEDGERS/-SUBUTXO/-SUBUTXOW in Ledger.Dijkstra.Specification.{Ledger,Utxo}.Properties.Computational.
• Verify that IsTopLevelValidFlagOf plumbing in SubUTxOEnv is exercisable from Haskell — the SUBUTXO rule branches on this flag and the conformance harness will need to set it.