Implement missing parts from StakePoolParams specification

[carlostome]

Description

• Add minPoolCost protocol parameter and enforce cost constraint of pool registration
• Add VRF to StakePoolParams. Enforce VRF uniqueness wrt registered pools
• Change StakePoolParams reward account from Credential to RewardAddress, and enforce NetworkId coincides during pool registration
• Add pool retirement conditions wrt pp Emax

Closes #1272
Addresses part of #1259

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

[Copilot]

Pull request overview

Implements missing Dijkstra stake-pool parameters and registration/retirement constraints.

Changes:

• Adds minimum pool cost, VRF uniqueness, reward-address network validation, and retirement bounds.
• Updates reward-account consumers and computational proofs.
• Extends foreign representations and pool-step environment.

Reviewed changes

Copilot reviewed 9 out of 9 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
src/Ledger/Dijkstra/Specification/Rewards.lagda.md	Extracts reward credentials.
src/Ledger/Dijkstra/Specification/Ratify.lagda.md	Uses reward-address credentials for delegation.
src/Ledger/Dijkstra/Specification/PParams.lagda.md	Adds minPoolCost.
src/Ledger/Dijkstra/Specification/PoolReap.lagda.md	Extracts credentials for refunds.
src/Ledger/Dijkstra/Specification/Certs/Properties/Computational.lagda.md	Implements and proves new validations.
src/Ledger/Dijkstra/Specification/Certs.lagda.md	Extends pool parameters and transition rules.
src/Ledger/Dijkstra/Foreign/Certs.agda	Exposes the new pool environment.
src/Ledger/Core/Specification/Crypto.lagda.md	Adds the VRF type.
src/Ledger/Core/Foreign/Crypto/Structure.agda	Instantiates VRF for Haskell.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[williamdemeo]

Nice, focused PR, and the commit sequence is clean; one concern per commit.

Two things are blocking, and there is one conformance question that should be settled before merging.

1. formal-ledger-test no longer builds. This is what the two red Hydra checks are telling us. The cause is the new VRF field of CryptoStructure. Test.LedgerImplementation builds its crypto structure from a module,

     SVCrypto = record
       { Implementation
       ; pkk = SVPKKScheme
       }

   and Implementation has no VRF, so VRF and the DecEq-VRF instance are both left as metas. (nix build .#formal-ledger-test reproduces it.)

   The fix. One line beside ScriptHash = ℕ in formal-ledger-test/src/Test/LedgerImplementation.lagda.md (line 63) clears it, and the build then goes through:

      ScriptHash = ℕ
      VRF = ℕ

2. PoolEnv is missing from the Dijkstra Haskell API

   build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Dijkstra/Foreign/API.hs:24-25

   re-exports poolStep but not PoolEnv(..). Now that pool-step takes a PoolEnv rather than a PParams, a downstream consumer cannot call it; neither the argument type nor the MkPoolEnv constructor is nameable. Every other environment record in that export list is there, so this is probably an oversight.

   The fix. Adding PoolEnv(..) on line 24.

The conformance question. POOL-rereg's VRF premise is more permissive than the implementation.

Certs.lagda.md:441 puts the condition as "the new VRF is not used by any other pool":

∙ ¬ (poolParams .vrf ∈ mapˢ vrf (range (pools ∣ ❴ kh ❵ ᶜ) ∪ range (fPools ∣ ❴ kh ❵ ᶜ)))

The implementation states it differently:

-- re-register Pool
Just stakePoolState -> do
  when (hardforkConwayDisallowDuplicatedVRFKeys pv) $ do
    sppVrf == stakePoolState ^. spsVrfL
      || Map.notMember sppVrf psVRFKeyHashes
        ?! injectFailure (VRFKeyHashAlreadyRegistered sppId sppVrf)

stakePoolState comes from psStakePools, so the equality escape hatch covers only the pool's active VRF; psVRFKeyHashes, by contrast, does hold the VRF recorded by a pending re-registration. The two agree everywhere but one case. Pool kh is active with vrf₀; in epoch E it re-registers with a fresh vrf₁, then re-registers again in the same epoch with vrf₁, say to correct cost. The implementation rejects that second certificate, since vrf₁ ≠ vrf₀ and vrf₁ is already in psVRFKeyHashes. Our rule accepts it, since fPools ∣ ❴ kh ❵ ᶜ drops the pending entry.

I prefer your formulation, and deriving the in-use set from pools and fPools rather than maintaining it incrementally avoids the bookkeeping the implementation has to do by hand. Since conformance is the point of the PR, though, I would rather see the divergence decided than inherited: either match the implementation here, or raise it upstream as an unintended bar on re-registering twice in one epoch after a VRF change.

Non-blocking

1. Alignment messed up in Certs.lagda.md around lines 428, 445 and 461.

2. The premise block is repeated a few times. The conjunction of the VRF, network-id and minPoolCost conditions is spelled out twice in Certs.lagda.md and four more times in Computational.lagda.md; the retirement triple appears twice more. A name for each, say

   ValidPoolParams : PParams → Pools → Pools → StakePoolParams → Type

   would shorten the rules and, more importantly, keep the rule and its decision procedure from drifting apart the next time a premise moves.

[carlostome]

1. **formal-ledger-test no longer builds**.  This is what the two red Hydra checks are telling us.  The cause is the new VRF field of CryptoStructure.

Fixed.

2. PoolEnv is missing from the Dijkstra Haskell API

Fixed.

The conformance question. POOL-rereg's VRF premise is more permissive than the implementation.

This has already been reported in cardano-ledger: IntersectMBO/cardano-ledger#6003

Non-blocking

1. Alignment messed up in `Certs.lagda.md` around lines 428, 445 and 461.

Fixed.

2. The premise block is repeated a few times.  

The premise is repeated exactly twice, so I think it does not merit its own definition (would be less straightforward).

[Copilot]

Pull request overview

Copilot reviewed 11 out of 11 changed files in this pull request and generated no new comments.

Suppressed comments (1)

Previously missed (1) — in code that hasn't changed since the last review.

src/Ledger/Dijkstra/Specification/PParams.lagda.md:121

• The PR checklist requires semantic specification changes to be documented in CHANGELOG.md, but the Dijkstra WIP section has no entry for this work. Please add a changelog entry covering minPoolCost, the reward-address/VRF registration checks, and the retirement bounds.

    minPoolCost                   : Coin

[williamdemeo]

Nice work, Carlos! LGTM!