Gov property #417: state that a voter's last vote is applied to the GA#1218
Open
williamdemeo wants to merge 8 commits into
Open
Gov property #417: state that a voter's last vote is applied to the GA#1218williamdemeo wants to merge 8 commits into
williamdemeo wants to merge 8 commits into
Conversation
Contributor
There was a problem hiding this comment.
Pull request overview
Adds a new governance-spec property statement (no proof yet) capturing that when a voter casts multiple votes on the same governance action within a block, the last such vote is the one recorded in the resulting GovState.
Changes:
- Introduces
Ledger.Conway.Specification.Gov.Properties.LastVoteApplied, including helper definitions to read recorded votes and compute the last vote over aGOVSsignal list, plus statement stubs for the single-step and block-lifted claims. - Wires the new module into the
Gov.Propertiesaggregator and lists the claim in the global properties index. - Documents the addition in
CHANGELOG.md.
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| src/Ledger/Conway/Specification/Properties.lagda.md | Adds the new governance claim to the properties index. |
| src/Ledger/Conway/Specification/Gov/Properties/LastVoteApplied.lagda.md | New module stating (and scaffolding) the “last vote is applied” governance property. |
| src/Ledger/Conway/Specification/Gov/Properties.lagda.md | Exports the new property module via the Gov properties aggregator. |
| CHANGELOG.md | Notes the newly stated (unproven) governance claim. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Member
Author
|
Machine-checked this branch with Agda 2.8.0 (via the project's Nix flake): Small follow-up to the Statement only; proof to follow. Part of #417. Generated by Claude Code |
williamdemeo
changed the title
Add the statement stub for issue #417 in a new module Ledger.Conway.Specification.Gov.Properties.LastVoteApplied: - votedOn / lookupGAState / recordedVote: read back the vote a voter has recorded on a governance action in a GovState - lastVoteOn: the last vote a voter casts on an action in a block - vote-applied-to-GA: a single GOV vote step records the cast vote (base case) - last-vote-applied-to-GA: over a block (GOVS), the last vote a voter casts on an action is the one recorded in the resulting state The proof is left as future work ("coming soon"). Wire the module into the Gov.Properties aggregator, list the claim in the properties index, and note it in the changelog.
Follow-up to "update link": the index entry rendered as malformed markdown (`[Gov-LastVoteApplied]][]`` `) and the link target pointed at the module page rather than the claim. Make it a clean reference (`[Gov-LastVoteApplied][]`) and point the link at the `#clm:LastVoteApplied` anchor, matching the sibling `[Gov-ChangePPHasGroup]`. Also add the `[Gov.Properties.LastVoteApplied]` module link for completeness. Part of #417 (statement only; proof to follow). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RP1jARAhD3898yZhVnPHZ4
williamdemeo
force-pushed
the
claude/417-property-last-vote-applied-to-GA
branch
from
d641c55 to
7c6304b
Compare
Add `applyVP` and `runGOVS` (the GovState update that a block of GOV signals performs) together with `GOVS→run≡`, which shows that a GOVS derivation computes exactly `runGOVS`. Mirrors `STS→updateGovSt≡` in Ledger.Conway.Specification.Ledger.Properties.Base. Stepping stone toward proving vote-applied-to-GA and last-vote-applied-to-GA.
…tion
`GovEnv.txid Γ ≢ proj₁ aid` (the voted action was not created by the current
transaction). Without it the claim is false: a same-block GOVPropose can mint a
fresh action id that collides with a pre-existing `aid` and, being inserted by
priority, shadows the voted entry. The condition holds for every reachable
ledger state, so it only excludes voting on an action proposed in the same tx.
What's proved:
- GOVS→run≡ a GOVS derivation computes the pure fold runGOVS
- vote-applied-to-GA base case (single GOV-Vote step); unconditional
- recordedVote-addVote voting on a present action records exactly that vote
- lookupᵐ?-insert lookup of a freshly inserted key
- ∈-insert-≢ / ∈-insert-≢⁻ insert at a different key preserves membership
- lookupGAState-addVote-≢ / recordedVote-addVote-≢gid
a vote on a different action leaves the lookup unchanged
- foldl-stepVote-nothing the stepVote fold is independent of its start accumulator
Remaining for the lifted proof:
- lookupᵐ?-insert-≢ (different-voter case)
- the proposal per-step fact (lookup invariance through insertGovAction),
- the derivation induction
- the final assembly.
williamdemeo
changed the title
williamdemeo
force-pushed
the
claude/417-property-last-vote-applied-to-GA
branch
from
2c84eac to
96ac313
Compare
Gov/Properties/LastVoteApplied:
- last-vote-applied-to-GA: across a block (the GOVS closure of GOV), the last
vote a voter casts on an action is the one recorded in the resulting
GovState, provided the action was not created by the current transaction
(Γ.txid ≢ proj₁ aid).
- vote-applied-to-GA: the single-GOV-step companion.
The proof is an induction on the GOVS derivation, chaining the per-step facts
(recordedVote-addVote / -≢gid / -≢voter / -addAction-≢) into the foldl that
lastVoteOn computes. Inducting on the derivation rather than a pure fold over
the signals is essential: the GOV-Vote rule supplies the proof that the voted
action is present. Without the freshness precondition the statement is false
(a same-block re-proposal can shadow the voted entry); discharging it for all
ledger-reachable states is left as a TODO noted in the source.
Axiom.Set.Map.Extras: adds four general, non-Gov-specific finite-map lemmas the
proof relies on — lookupᵐ?-insert, ∈-insert-≢, ∈-insert-≢⁻, and lookupᵐ?-insert-≢
(lookup commutes with insert at a distinct key). Candidates for upstreaming to
agda-sets.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Rz41G9j463RqCCpUpFTGc4
williamdemeo
force-pushed
the
claude/417-property-last-vote-applied-to-GA
branch
from
96ac313 to
0f70d5c
Compare
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
williamdemeo
commented
Jul 1, 2026
| set `updateGroups`{.AgdaField} `pu`{.AgdaBound} is nonempty. | ||
|
|
||
|
|
||
| + **Claim** [Gov-LastVoteApplied][]. A voter's vote is applied to the governance action. |
Member
Author
There was a problem hiding this comment.
Actually, this should be a Theorem, not a claim.
Also, the original purpose of the "top-level" Conway.Specification.Properties module was simply to collect in one place all of the properties we have claimed and/or proved. Once we have the properties tracker we can probably retire this module.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
A voter's last vote is applied to the governance action
Closes #417
#417 asks only for the statement of this property; this PR also proves it.
Result (
Gov/Properties/LastVoteApplied)last-vote-applied-to-GA— across a block (theGOVSclosure ofGOV), the last vote a voter casts on an action is the one recorded in the resultingGovState, provided that action was not created by the current transaction (Γ.txid ≢ proj₁ aid).vote-applied-to-GA— the single-step companion.Why the precondition is needed. Without it the claim is genuinely false: a same-block proposal can mint an action whose id collides with
aidand, being priority-inserted ahead of the voted entry, shadows it. The condition holds for every ledger-reachable state (existing actions carry earlier transactions' ids); proving that in general is left as a TODO, flagged in the source.Proof. Induction on the
GOVSderivation, chaining four per-steprecordedVote-*facts into the fold thatlastVoteOncomputes.Also. Four general lookup-after-insert lemmas were added to
Axiom.Set.Map.Extras(candidates for upstreaming to agda-sets).Checklist
CHANGELOG.md