[Dijkstra] Add EntitiesEnv and GovCertEnv

[carlostome]

Description

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]

Overview

This PR splits the previously monolithic Dijkstra CertEnv into three purpose-fitted environments — EntitiesEnv (epoch, pp, votes, coldCredentials, withdrawals, directDeposits) for ENTITIES, a slimmed CertEnv (e, pp, coldCredentials) for CERT/CERTS, and a new GovCertEnv for GOVCERT — adds a HasColdCredentials class, threads the Computational proofs through the new envs, and reworks the FFI layer accordingly.

This is a genuine improvement: GOVCERT/CERT no longer drag around votes/wdrls/directDeposits they never used, and the env shapes now say what each rule actually depends on. All CI checks pass. Most of my comments are inline; the two below concern files not touched by this diff.

🔴 entitiesStep FFI export deleted, but the static Haskell API still re-exports it

This PR removes the entities-step function and its {-# COMPILE GHC entities-step as entitiesStep #-} pragma from Foreign/Entities.agda, but the static re-export module still imports it:

formal-ledger-specifications/build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Dijkstra/Foreign/API.hs

Lines 26 to 27 in fc2fa0b

	import MAlonzo.Code.Ledger.Dijkstra.Foreign.Entities as X
	(entitiesStep)

Without the pragma, MAlonzo emits only mangled internal names, so this import will not compile. CI doesn't catch it because the hs shake target runs Agda with --ghc-dont-call-ghc and only assembles the package (build-tools/shake/src/Main.hs:110) — GHC never compiles the generated code in this repo. The break surfaces downstream when cardano-ledger's conformance tests build cardano-ledger-executable-spec.

Given the commit is titled "Fix foreign interface for ENTITIES" and the EntitiesEnv' wrapper exists precisely to make EntitiesEnv FFI-convertible, I assume this was an accidental deletion — see the inline suggestion in Foreign/Entities.agda for restoring it with the new env type. (If dropping entitiesStep is intentional, the right fix is instead to remove it from API.hs.)

🟡 API.hs is out of sync with the new interface

Even with entitiesStep restored, build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Dijkstra/Foreign/API.hs needs updating:

• govCertStep now takes GovCertEnv, but GovCertEnv(..) is not in the export list — downstream users can call the function but can't name or construct its argument without reaching into internal MAlonzo modules. EntitiesEnv(..) is likewise missing.
• Heads-up rather than a defect: the exported CertEnv(..) keeps its name but its Haskell fields change from ceEpoch/cePp/ceVotes/ceWdrls/ceColdCreds/ceDirectDeposits to ceE/cePp/ceColdCredentials — breaking for any conformance-test code constructing it. Expected for in-flight Dijkstra work, but worth coordinating with the consumers.

🟡 CHANGELOG

CHANGELOG.md has a "Dijkstra spec / WIP" section that records exactly this kind of change — this PR should add an entry (it's also an unchecked box on the PR checklist).

Verdict

Requesting changes for the entitiesStep break, since it's invisible to this repo's CI and would land as a compile failure on the cardano-ledger side. Everything else inline is naming/style-level and mostly comes with suggested fixes.

🤖 Generated with Claude Code

[williamdemeo]

Optional: ⟦ EpochOf ce , PParamsOf ce , ColdCredentialsOf ce ⟧ is now spelled out at five call sites in this module (plus the CERT-gov rule itself). A small helper next to the record definitions, e.g.

govCertEnvOf : CertEnv → GovCertEnv
govCertEnvOf Γ = ⟦ EpochOf Γ , PParamsOf Γ , ColdCredentialsOf Γ ⟧

would DRY these up and make the CertEnv → GovCertEnv projection a named, documented thing.

[williamdemeo]

Nice work Carlos! The restored entities-step and the applied suggestions all look good.

Approving with one remaining loose end from the first review (could be a follow-up commit or PR if/as you see fit):

API.hs doesn't export the new env types

In build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Dijkstra/Foreign/API.hs, govCertStep now takes GovCertEnv and entitiesStep takes EntitiesEnv, but neither type is in the export list, so downstream consumers (e.g. the cardano-ledger conformance tests) can call the step functions but can't name or construct their env arguments without reaching into the internal MAlonzo modules directly. The old code didn't have this gap because both steps took CertEnv, which is exported.

The fix suggested by Claude:

import MAlonzo.Code.Ledger.Dijkstra.Foreign.Certs as X
  ( StakePoolParams(..), PState(..), DelegEnv(..), CertEnv(..), GovCertEnv(..), DState(..), DCert(..), GState(..) , delegStep, govCertStep, poolStep)
import MAlonzo.Code.Ledger.Dijkstra.Foreign.Entities as X (EntitiesEnv(..), entitiesStep)

GovCertEnv/MkGovCertEnv is generated into Foreign.Certs by the new HsTy-GovCertEnv, and EntitiesEnv/MkEntitiesEnv into Foreign.Entities by HsTy-EntitiesEnv' (same pattern as the old CertEnv' re-export, so both names exist to be re-exported).