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

[williamdemeo]

For every CERTS step Γ ⊢ s ⇀⦇ certs ,CERTS⦈ s', the range of voteDelegs in s' is contained in the VDelegs of the DReps registered in s', together with vDelegNoConfidence and vDelegAbstain.

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:

1. vDelegAbstain and vDelegNoConfidence are legal voteDelegs values. DELEG-delegate admits them and POST-CERT deliberately keeps them, and neither is vDelegCredential c for any c.
2. The range wraps DRep credentials, and regdrep never adds a key to voteDelegs, so a delegatee need not lie in dom voteDelegs.

A single delegate certificate already carries ⟦ ∅ , ∅ , ∅ ⟧ᵈ, which satisfies the original statement, to a state that refutes it (checked in Agda while preparing this PR).

The corrected statement uses the domain of the registered DReps and adds the two constants, so it matches the set POST-CERT corestricts to and the intent recorded in the anchor {#clm:VDelegsInRegDReps}. Nothing is assumed about the initial state, since POST-CERT enforces the property on the output of every batch.

The proof inverts the CERTS step, inducts over the CERT trace, and closes the run-[] case with a new lemma cores-range-⊆ : range (m ∣^ X) ⊆ X in Axiom.Set.Map.Extra.

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.