[Conway] Property : voteDelegs range lies in VDelegs of registered DReps (#1233)

[williamdemeo]

Every value of voteDelegs is a VDeleg of a registered DRep, vDelegAbstain, or vDelegNoConfidence, and CERTS preserves that.

CERTS-voteDelegsVDeleg : LedgerInvariant _⊢_⇀⦇_,CERTS⦈_ voteDelegsVDeleg

The original statement was corrected. It said

range (VoteDelegsOf d) ⊆ mapˢ vDelegCredential (dom (VoteDelegsOf d))

which is well typed (mapˢ vDelegCredential lifts the domain into ℙ VDeleg) but false, for two independent reasons: vDelegAbstain and vDelegNoConfidence are legal voteDelegs values and neither is vDelegCredential c for any c; and the range wraps DRep credentials, while regdrep never adds a key to voteDelegs, so a delegatee need not lie in dom voteDelegs.

It is now an invariant rather than a postcondition, because master removed POST-CERT in the meantime. That rule used to corestrict voteDelegs to the active VDelegs at the end of every batch, which made the containment unconditional on the output of CERTS. With the final sweep gone, an input state may already violate it and no CERTS step would repair it, so the property is stated and proved as preservation instead.

The containment is now maintained incrementally by the two rules that could break it: DELEG-delegate may install only a VDeleg that is already active for the current delegatees, and GOVCERT-deregdrep, the one rule that shrinks the registered DReps, deletes every delegation to the credential it deregisters in the same step. The proof establishes invariance for DELEG, GOVCERT, CERT and PRE-CERT, then lifts the CERT lemma along RTC-preserves-inv.

Four small lemmas go to Axiom.Set.Map.Extra: coex-∈⁻, and dom-∪ˡ-⊇ʳ with its corollaries dom-insert-⊇ and dom-mapValueRestricted-⊇.

Closes #1233

[Copilot]

Pull request overview

Note

Copilot was unable to run its full agentic suite in this review.

This PR upgrades the “vote delegation targets are valid” statement from an informal claim to a formally proved theorem, ensuring post-CERTS states only contain vote delegations to registered DReps (or the two special constants).

Changes:

• Replaces an informal claim with a theorem statement in the Conway spec properties overview.
• Adds a full formalization and proof that CERTS steps leave only “active” VDeleg values in voteDelegs.
• Introduces a supporting set-theory lemma about corestriction range containment and records the change in the changelog.

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 3 comments.

File	Description
src/Ledger/Conway/Specification/Properties.lagda.md	Updates the high-level spec statement from “Claim” to “Theorem” with a refined description.
src/Ledger/Conway/Specification/Certs/Properties/VoteDelegsVDeleg.lagda.md	Defines activeVDelegs, restates the property over CertState, and adds a proof for the CERTS step.
src-lib-exts/abstract-set-theory/Axiom/Set/Map/Extra.agda	Adds lemma cores-range-⊆ used by the new proof.
CHANGELOG.md	Documents the newly stated/proved voteDelegs property.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[williamdemeo]

Keeping these, because the pluralization is a repo-wide prose convention rather than something local to this entry. It occurs 19 times under src/, including the two neighbouring bullets in this same file and the modules this bullet links to (Certs/Properties/PoV.lagda.md L61-62, Certs/Properties/PoVLemmas.lagda.md L50 and L215-218). Aligning only this entry would make it the odd one out.

You are right on the underlying point, though: CertStates and DCerts are not identifiers, so tagging them {.AgdaRecord} / {.AgdaDatatype} applies Agda-identifier styling to non-identifiers. That is pre-existing and repo-wide, so it belongs in its own pass over the prose rather than here.

[williamdemeo]

Deliberately keeping the anchor:

1. It is referenced from build-tools/static/mkdocs/includes/links.md and is a published-docs URL fragment, so renaming breaks existing external links to #clm:VDelegsInRegDReps.
2. There is already in-repo precedent for a proved theorem retaining a clm: anchor: src/Ledger/Conway/Specification/Gov/Properties/LastVoteApplied.lagda.md L6 is ## Theorem: ... {#clm:LastVoteApplied}.
3. Preserving this anchor was an explicit requirement for this change.

Your point stands that the clm: / thm: prefixes are no longer a reliable classification signal. With two files now in this state, the fix is one pass over every anchor plus links.md (and ideally redirects for the published fragments), not a one-off rename here.

[williamdemeo]

Two separate points here; the first rests on a misreading.

cores-range-⊆ is not inside the module _ {A B : Type} ... block that opens at L64. It starts at column 0, which closes that block, so the ∀ {A B : Type} is required rather than redundant. It also must stay: that module's parameters include ⦃ CommutativeMonoid _ _ B ⦄ and ⦃ IsCommutativeSemigroup _◇_ ⦄, and a corestriction lemma has no business carrying a commutative-monoid constraint. The form used matches the adjacent top-level lemmas (lookupᵐ?-insert, ∈-insert-≢, lookupᵐ?-insert-≢), which are all ∀ {A B : Type} ⦃ _ : DecEq _ ⦄.

The naming nit is fair, and is fixed in 9dd24fb: cores-range-⊆ _ b∈range is now cores-range-⊆ m b∈range. m stays unused in the body (the proof only inspects the membership proof), but naming it saves the reader a trip to the signature to recover the argument order.

[williamdemeo]

Rebased onto master (8f3bb1173) and reworked, because master removed POST-CERT while this sat open.

That rule was load-bearing here. It corestricted voteDelegs to the active VDelegs at the end of every batch, so the containment held unconditionally of the output of CERTS and the proof was a one-liner off CERT-post. With the final sweep gone, an input state may already violate the containment and no CERTS step repairs it, so the property is now stated and proved as preservation:

CERTS-voteDelegsVDeleg : LedgerInvariant _⊢_⇀⦇_,CERTS⦈_ voteDelegsVDeleg

This is the honest correction rather than a simplification: the statement is the more useful one (a real invariant), but the proof grew, since the containment is now maintained incrementally by DELEG-delegate and GOVCERT-deregdrep instead of being re-established wholesale at the end.

Two notes for anyone re-reading the earlier review threads:

• cores-range-⊆, the subject of the third Copilot comment and my reply, is gone. Nothing corestricts any more, so it would have been dead code. The complement form coex-∈⁻ replaced it, and the naming point from that thread carries over to it and to the three new domain lemmas.
• The correction to the original issue statement is unaffected by any of this, and both reasons it was false still hold.

Verified with agda on each edited module and a full nix build before pushing.