Gov property #417: state that a voter's last vote is applied to the GA by williamdemeo · Pull Request #1218 · IntersectMBO/formal-ledger-specifications

williamdemeo · 2026-06-09T13:55:15Z

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.

GOVS-level result (`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 that action was not created by the current transaction (Γ.txid ≢ proj₁ aid).
vote-applied-to-GA: the single-step companion.

The precondition is needed at this level because the signal list is an arbitrary List (GovVote ⊎ GovProposal) — proposals and votes can be interleaved, and a proposal after a vote can shadow it via priority insertion.

The proof is by induction on the GOVS derivation, chaining four per-step recordedVote-* facts into the fold that lastVoteOn computes.

LEDGER-level result (`Ledger/Properties/LastVoteApplied`)

LEDGER-last-vote-applied — the same property lifted to the LEDGER rule, without the freshness premise Γ.txid ≢ proj₁ aid.

The key insight is that txgov places all proposals before all votes (map inj₂ txGovProposals ++ map inj₁ txGovVotes). During the proposals phase, lastVoteOn is unaffected (proposals are no-ops for stepVote). During the votes phase, no proposals occur, so recordedVote-addAction-≢ — the only lemma that consumes the freshness assumption — is never invoked.

Three helper lemmas support this:

stepVote-proposals: proposals don't change the vote-fold accumulator
split-GOVS: decompose a GOVS derivation at a ++ boundary
lift-GOVS-votes: votes-only lift needs no freshness (GOV-Propose is ruled out by pattern matching on inj₁)

Also. Four general lookup-after-insert lemmas were added to Axiom.Set.Map.Extras (candidates for upstreaming to agda-sets).

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

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 a GOVS signal list, plus statement stubs for the single-step and block-lifted claims.
Wires the new module into the Gov.Properties aggregator 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.

williamdemeo · 2026-06-23T06:12:43Z

Machine-checked this branch with Agda 2.8.0 (via the project's Nix flake): LastVoteApplied.lagda.md and the Ledger.Conway.Specification.Properties index both typecheck under --safe with no errors or warnings. The lookupᵐ? lookups, the GovVoter (⟦_,_⟧ᵍᵛ) pattern match, and the GOV/GOVS statements all elaborate as written — no proof yet.

Small follow-up to the update link commit: the index entry had rendered as malformed markdown ([Gov-LastVoteApplied]][]`` ``) and the link pointed at the module page. Fixed it to a clean [Gov-LastVoteApplied][]reference pointing at the#clm:LastVoteAppliedanchor (matching[Gov-ChangePPHasGroup]), and added the [Gov.Properties.LastVoteApplied]` module link.

Statement only; proof to follow. Part of #417.

Generated by Claude Code

Copilot

Pull request overview

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

carlostome · 2026-07-01T11:51:49Z

+recordedVote : GovState → GovActionID → GovVoter → Maybe Vote
+recordedVote s aid voter = case lookupGAState s aid of λ where
+  nothing     → nothing
+  (just gaSt) → votedOn gaSt voter


Suggested change

recordedVote : GovState → GovActionID → GovVoter → Maybe Vote

recordedVote s aid voter = case lookupGAState s aid of λ where

nothing → nothing

(just gaSt) → votedOn gaSt voter

recordedVote : GovState → GovActionID → GovVoter → Maybe Vote

recordedVote s aid voter = lookupGAState s aid >>= \gaSt -> votedOn gaSt voter

I (and Claude) tried this... resulting in some unresolved metas (specifically, the Monad instance for Maybe blocks reduction during rewrite) I think it's fine the way it is.

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

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.

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

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

- Fix title: "A voter's vote" → "A voter's last vote" (Carlos's suggestion) - Properties index: "Claim" → "Theorem" (proved, not just stated) - Add Ledger.Properties.LastVoteApplied: lift the GOVS-level theorem to the LEDGER rule, taking TxId freshness as a premise

Exploit the txgov structure (proposals before votes) to prove LEDGER-last-vote-applied without the Γ.txid ≢ proj₁ aid premise. Three helper lemmas: + stepVote-proposals: proposals are no-ops for the vote fold + split-GOVS: decompose a GOVS derivation at a ++ boundary + lift-GOVS-votes: votes-only lift needs no freshness (GOV-Propose is ruled out by pattern matching on inj₁)

Copilot

Pull request overview

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

Comments suppressed due to low confidence (1)

build-tools/static/mkdocs/includes/links.md:61

A new LEDGER properties page was added (...Ledger.Properties.LastVoteApplied), but there are no corresponding link definitions here like the other Ledger.Properties.* pages/anchors. Adding these entries will make it easy to reference the theorem consistently from other docs.

[Gov-LastVoteApplied]: Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.md#clm:LastVoteApplied
[issues]: https://github.com/IntersectMBO/formal-ledger-specifications/issues
[Introduction]: Ledger.Introduction.md
[LEDGER]: Ledger.Conway.Specification.Ledger.md#ledger-transition-system
[Ledger.Properties]: Ledger.Conway.Specification.Ledger.Properties.md

williamdemeo · 2026-07-09T05:59:01Z

+module Ledger.Conway.Specification.Ledger.Properties.LastVoteApplied
+  (txs : _) (open TransactionStructure txs)
+  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
+  where


williamdemeo requested a review from Copilot June 23, 2026 03:07

williamdemeo marked this pull request as ready for review June 23, 2026 03:07

Copilot started reviewing on behalf of williamdemeo June 23, 2026 03:08 View session

Copilot AI reviewed Jun 23, 2026

View reviewed changes

Comment thread src/Ledger/Conway/Specification/Properties.lagda.md Outdated

williamdemeo self-assigned this Jun 23, 2026

williamdemeo requested a review from carlostome June 23, 2026 06:02

williamdemeo marked this pull request as draft June 24, 2026 14:39

williamdemeo changed the title ~~Gov property #417: state that a voter's last vote is applied to the GA~~ WIP -- Gov property #417: state that a voter's last vote is applied to the GA Jun 25, 2026

williamdemeo force-pushed the claude/417-property-last-vote-applied-to-GA branch from d641c55 to 7c6304b Compare June 30, 2026 01:50

williamdemeo changed the title ~~WIP -- Gov property #417: state that a voter's last vote is applied to the GA~~ Gov property #417: state that a voter's last vote is applied to the GA Jun 30, 2026

williamdemeo marked this pull request as ready for review June 30, 2026 22:47

williamdemeo force-pushed the claude/417-property-last-vote-applied-to-GA branch 2 times, most recently from 96ac313 to 0f70d5c Compare June 30, 2026 22:50

williamdemeo requested a review from Copilot June 30, 2026 22:50

Copilot started reviewing on behalf of williamdemeo June 30, 2026 22:50 View session

Copilot AI reviewed Jun 30, 2026

View reviewed changes

Comment thread src/Ledger/Conway/Specification/Gov/Properties/LastVoteApplied.lagda.md

Comment thread src/Ledger/Conway/Specification/Gov/Properties/LastVoteApplied.lagda.md Outdated

Comment thread CHANGELOG.md Outdated

williamdemeo commented Jul 1, 2026

View reviewed changes

Comment thread src/Ledger/Conway/Specification/Properties.lagda.md Outdated

carlostome reviewed Jul 1, 2026

View reviewed changes

claude and others added 9 commits July 7, 2026 08:11

minor polish

c581245

update link

d0e098a

Apply suggestions from code review

449e4a4

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

williamdemeo force-pushed the claude/417-property-last-vote-applied-to-GA branch from 9edccbd to fe57eac Compare July 7, 2026 14:12

williamdemeo marked this pull request as draft July 7, 2026 14:15

williamdemeo force-pushed the claude/417-property-last-vote-applied-to-GA branch from cf9884a to d86cb92 Compare July 8, 2026 04:42

williamdemeo marked this pull request as ready for review July 8, 2026 04:52

williamdemeo requested a review from Copilot July 8, 2026 04:52

Copilot started reviewing on behalf of williamdemeo July 8, 2026 04:52 View session

Copilot AI reviewed Jul 8, 2026

View reviewed changes

address Copilot PR review comment

8a82965

williamdemeo requested a review from carlostome July 9, 2026 05:59

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Gov property #417: state that a voter's last vote is applied to the GA#1218

Gov property #417: state that a voter's last vote is applied to the GA#1218
williamdemeo wants to merge 11 commits into
masterfrom
claude/417-property-last-vote-applied-to-GA

williamdemeo commented Jun 9, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

williamdemeo commented Jun 23, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

carlostome Jul 1, 2026

Uh oh!

williamdemeo Jul 7, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

williamdemeo Jul 9, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Uh oh!

Conversation

williamdemeo commented Jun 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description

A voter's last vote is applied to the governance action

GOVS-level result (Gov/Properties/LastVoteApplied)

LEDGER-level result (Ledger/Properties/LastVoteApplied)

Checklist

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

williamdemeo commented Jun 23, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

carlostome Jul 1, 2026

Choose a reason for hiding this comment

Uh oh!

williamdemeo Jul 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

williamdemeo Jul 9, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

williamdemeo commented Jun 9, 2026 •

edited

Loading

GOVS-level result (`Gov/Properties/LastVoteApplied`)

LEDGER-level result (`Ledger/Properties/LastVoteApplied`)

williamdemeo Jul 7, 2026 •

edited

Loading