Move vote delegation removal to GovCert

[carlostome]

Description

This PR changes the Conway (and Dijkstra) specification to match the implementation.
In particular, in the implementation a DRep deregistering certificate makes the DRep delegated stake be reset to empty, even if the same DRep is reregistered in the same transaction.

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]

Here's something Claude found that I'm not sure about, but I'll post it in case it helps you.

Generated Haskell no longer compiles.

CertState moved modules

• src/Ledger/Conway/Foreign/Certs.agda:83-84
• src/Ledger/Dijkstra/Foreign/Certs.agda:62-63

Moving HsTy-CertState/Conv-CertState out of Foreign/Cert.agda moves the generated Haskell datatype with it.

In this PR's hs artifact, data CertState = MkCertState… appears only in MAlonzo/Code/Ledger/{Conway,Dijkstra}/Foreign/Certs.hs and is gone from Foreign/Cert.hs. But the static re-export modules still import it from the old location:

• build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Conway/Foreign/API.hs:14-15
• build-tools/static/hs-src/src/MAlonzo/Code/Ledger/Dijkstra/Foreign/API.hs:19-20

MAlonzo emits modules without export lists, so the Agda-level public on the import does not re-export the Haskell type and GHC will reject import …Foreign.Cert (…, CertState(..)).

CI will not flag it: the hs target only assembles the tree, and build-tools/nix/hs-src.nix checks nothing beyond the presence of the .cabal file. Both API.hs files need CertState(..) imported from Foreign.Certs.

[williamdemeo]

Another Claude find seems useful:

The GOVCERT step is now resolved by an ambiguous instance search

src/Ledger/Conway/Specification/Certs/Properties/Computational.lagda.md:106,
src/Ledger/Conway/Conformance/Certs/Properties.lagda.md:121,
src/Ledger/Dijkstra/Specification/Certs/Properties/Computational.lagda.md:103

Computational-GOVCERT and Computational-CERT now have the same index type CertEnv → CertState → DCert → CertState → Type, so both are candidates for the bare computeProof ce cs dCert, and it only lands on GOVCERT because the metavariable is pinned later by CERT-vdel h on the right-hand side.

Please make it explicit: computeProof {STS = _⊢_⇀⦇_,GOVCERT⦈_} ce cs dCert.

I suspect this is also why the CERT-vdel completeness clauses had to be rewritten to re-inline each GOVCERT decision procedure; with the annotation the old with computeProof… | completeness _ _ _ _ h form should work again, and the ¿ … ¿ predicates would not be duplicated across three sites.

[williamdemeo]

Suggested change

	`DRep`{.AgdaInductiveConstructor}, and every vote delegation to that `DRep`{.AgdaInductiveConstructor} is dropped.

[williamdemeo]

This was meant to suggest replacing the period with a comma and adding the phrase that begins, "and every vote..."

[williamdemeo]

This is a pre-existing flaw, not something this PR introduced, but we might as well fix it here, since it sits in the middle of what the PR touches.

In GOVCERTFromConf the right-hand sides are C.GOVCERT-… where I think L.GOVCERT-… is meant (cf. DELEGFromConf above).

[williamdemeo]

Confirmed the two fixes: SUBENTITIES no longer applies the filter, and the API.hs re-exports resolve again. (Claude cross-checked every re-exported name in the three API.hs files against the generated modules in the latest hs artifact; all 194 resolve, and the same check on the previous artifact flags exactly the two CertState misses.)

Remaining items, none of them blocking:

Docs. src/Ledger/Conway/Specification/Certs.lagda.md:430-431 still says only that GOVCERT-deregdrep deregisters a DRep; it should also say that vote delegations to that DRep are dropped, and the section could use a sentence on why GOVCERT takes a whole CertState while DELEG and POOL stay on their own component.

Small things.

• stᵍ' is declared but unused in all three Certs modules (Specification/Certs.lagda.md:362, Conformance/Certs.lagda.md:106, Dijkstra/Specification/Certs.lagda.md:322).
• src/Ledger/Dijkstra/Specification/Certs/Properties/Computational.lagda.md:74-97 still calls the GOVCERT state gs although it is a CertState; Conway's copy was renamed to cs.
• src/Ledger/Dijkstra/Specification/Certs.lagda.md:463: deposits for the GState field and deposits' for the DState field reads like a post-state; depositsᵈ/depositsᵍ as in Entities would be clearer.

Maybe worth recording. Pruning at deregistration makes range voteDelegs ⊆ mapˢ vDelegCredential (dom dReps) ∪ {vDelegAbstain, vDelegNoConfidence} an inductive invariant of CERT rather than something re-imposed at the end of CERTS: DELEG-delegate admits only registered delegatees, dom dReps shrinks only at deregdrep, and the epoch boundary only bumps the epoch values (Epoch.lagda.md:688-691). That is a better basis for #1233 than POST-CERT was, and it invalidates #1290 as written, which states the property in terms of POST-CERT's activeVDelegs.

[williamdemeo]

Nice work, Carlos! Approving, but see the (non-blocking) comments I added in case you want to address any of them here before merging.