Ledger.Conway.Specification.Gov.Properties.LastVoteApplied

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

{-# OPTIONS --safe #-}

open import Ledger.Conway.Specification.Gov.Base

module Ledger.Conway.Specification.Gov.Properties.LastVoteApplied
  (gs : GovStructure) (open GovStructure gs)
  where

open import Ledger.Prelude
open import Ledger.Conway.Specification.Gov.Actions gs hiding (yes; no)
open import Ledger.Conway.Specification.Gov gs
open import Data.List.Relation.Unary.Any using (here; there)

open GovActionState using (votes)
open GovVotes using (gvCC ; gvDRep ; gvSPO)
open GovVote using (gid)
open GovEnv using (txid ; epoch)
open PParams using (govActionLifetime)

Informally.

Theorem (last-vote-applied). When a voter casts one or more votes on a governance action within a single block (the GOVS closure of GOV steps), the last vote they cast is the one recorded in the resulting GovState.

Formally.

We first define what it means to read back the vote a voter recorded on an action, and the last vote a voter casts in a list of GOV signals.

-- The vote (if any) that `voter` recorded on a single GovActionState.
votedOn : GovActionState → GovVoter → Maybe Vote
votedOn gaSt $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1024}{\htmlId{1407}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#1414}{\htmlId{1414}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ = lookupᵐ? (gaSt .votes .gvCC) c
votedOn gaSt $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1027}{\htmlId{1469}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#1476}{\htmlId{1476}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ = lookupᵐ? (gaSt .votes .gvDRep) c
votedOn gaSt $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1032}{\htmlId{1533}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#1540}{\htmlId{1540}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix}$ = lookupᵐ? (gaSt .votes .gvSPO) kh

-- Find the GovActionState associated with an action id in a GovState.
lookupGAState : GovState → GovActionID → Maybe GovActionState
lookupGAState [] aid = nothing
lookupGAState ((aid' , gaSt) ∷ s) aid = case aid ≟ aid' of λ where
  (yes _) → just gaSt
  (no  _) → lookupGAState s aid

-- The vote (if any) recorded for `voter` on action `aid` in `s`.
recordedVote : GovState → GovActionID → GovVoter → Maybe Vote
recordedVote s aid voter = case lookupGAState s aid of λ where
  nothing     → nothing
  (just gaSt) → votedOn gaSt voter

-- Fold step keeping the most recent vote that `voter` cast on action `aid`.
stepVote : GovVoter → GovActionID → Maybe Vote → GovVote ⊎ GovProposal → Maybe Vote
stepVote voter aid acc (inj₁ gv) with GovVoterOf gv ≟ voter | gv .gid ≟ aid
... | yes _ | yes _ = just (VoteOf gv)
... | _     | _     = acc
stepVote voter aid acc (inj₂ _)  = acc

-- The last vote `voter` cast on action `aid` in a list of GOV signals.
lastVoteOn : GovVoter → GovActionID → List (GovVote ⊎ GovProposal) → Maybe Vote
lastVoteOn voter aid = foldl (stepVote voter aid) nothing

The following is the type that codifies the property we wish to prove.

last-vote-applied-to-GA : Type
last-vote-applied-to-GA =
  {Γ      : GovEnv}
  {s s'   : GovState}
  {vps    : List (GovVote ⊎ GovProposal) }
  {aid    : GovActionID}
  {voter  : GovVoter}
  {v      : Vote}
  → Γ .txid ≢ proj₁ aid
  → Γ ⊢ s ⇀⦇ vps ,GOVS⦈ s'
  → lastVoteOn voter aid vps ≡ just v
  → recordedVote s' aid voter ≡ just v

Proof.

The proof (that last-vote-applied-to-GA is inhabited) has three main ingredients.

Four per-step lemmas. A handful of per-step facts describing how a single GOV signal changes the vote that recordedVote reads back: a vote on the targeted action and voter records it; any other vote, or a proposal, leaves it untouched.
A fold lemma (foldl-stepVote-nothing). Once a matching vote appears in the signal list, foldl stepVote produces that vote regardless of the starting accumulator. This lets us replace the nothing seed of lastVoteOn with recordedVote s aid voter (the initial state's recorded vote).
Induction on the GOVS derivation (lift-GOVS). At each step, the appropriate per-step lemma rewrites the accumulator. The induction chains these per-step facts into the foldl that lastVoteOn computes. Crucially, inducting on the derivation (not the bare list) provides the GOV-Vote membership proof that recordedVote-addVote requires.

Four per-step lemmas¶

Four per-step lemmas describe how a single GOV step changes the recorded vote.

1. recordedVote-addVote¶

Voting for (aid , voter) on an action that is present records exactly v.

opaque
  unfolding addVote

  recordedVote-addVote :
    {s     : GovState}
    {aid   : GovActionID}
    {ast   : GovActionState}
    {voter : GovVoter}
    {v     : Vote}
    → (aid , ast) ∈ fromList s → recordedVote (addVote s aid voter v) aid voter ≡ just v

  recordedVote-addVote {s} {aid} {ast} {voter} {v} p = go voter s (Equivalence.from ∈-fromList p)
    where
    go : (w : GovVoter) (t : GovState) → (aid , ast) ∈ˡ t
       → recordedVote (addVote t aid w v) aid w ≡ just v
    go w ((aid' , g') ∷ t) mem with aid ≟ aid'
    ... | yes refl rewrite dec-yes (aid ≟ aid) refl .proj₂ with w
    ...   | $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1024}{\htmlId{5073}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#5080}{\htmlId{5080}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ = lookupᵐ?-insert (gvCC   (votes g')) c  v
    ...   | $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1027}{\htmlId{5144}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#5151}{\htmlId{5151}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ = lookupᵐ?-insert (gvDRep (votes g')) c  v
    ...   | $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1032}{\htmlId{5215}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#5222}{\htmlId{5222}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix}$ = lookupᵐ?-insert (gvSPO  (votes g')) kh v
    go w ((aid' , g') ∷ t) mem | no aid≢ with mem
    ...   | here refl = ⊥-elim (aid≢ refl)
    ...   | there m   = go w t m

The next two per-step facts say a GOV step that does not match (aid , voter) leaves its recorded vote unchanged.

2. recordedVote-addVote-≢gid¶

Voting on a different action leaves the recorded vote unchanged.

opaque
  unfolding addVote

  lookupGAState-addVote-≢ :
    {s : GovState}
    {aid₀ aid : GovActionID}
    {voter₀ : GovVoter}
    {v₀ : Vote}
    → aid₀ ≢ aid
    → lookupGAState (addVote s aid₀ voter₀ v₀) aid ≡ lookupGAState s aid
  lookupGAState-addVote-≢ {s = []} _ = refl
  lookupGAState-addVote-≢ {s = ((aid'' , g'') ∷ s)} {aid₀} {aid} {voter₀} {v₀} ne
    with aid ≟ aid''
  ... | no  _    = lookupGAState-addVote-≢ {s} {voter₀ = voter₀} {v₀} ne
  ... | yes refl with aid ≟ aid₀
  ...   | yes refl = ⊥-elim (ne refl)
  ...   | no  _    = refl

  recordedVote-addVote-≢gid :
    {s : GovState}
    {aid₀ aid : GovActionID}
    {voter₀ voter : GovVoter}
    {v₀ : Vote}
    → aid₀ ≢ aid
    → recordedVote (addVote s aid₀ voter₀ v₀) aid voter ≡ recordedVote s aid voter
  recordedVote-addVote-≢gid {s} {voter₀ = voter₀} {v₀ = v₀} ne
    rewrite lookupGAState-addVote-≢ {s = s} {voter₀ = voter₀} {v₀} ne = refl

3. recordedVote-addVote-≢voter¶

A vote on the same action by a different voter, leaves the recorded vote unchanged.

Once the voted entry is located, the recorded vote for voter reads the credential map. A vote by voter₀ ≢ voter either touches a different role's map or the same role at a different credential (lookupᵐ?-insert-≢, the credentials differing because the voters differ).

  recordedVote-addVote-≢voter :
    {s : GovState}
    {aid : GovActionID}
    {voter₀ voter : GovVoter}
    {v₀ : Vote}
    → voter₀ ≢ voter
    → recordedVote (addVote s aid voter₀ v₀) aid voter ≡ recordedVote s aid voter
  recordedVote-addVote-≢voter {s} {aid} {voter₀} {voter} {v₀} ne = go voter₀ voter s ne
    where
    go : (w₀ w : GovVoter) (t : GovState) → w₀ ≢ w
       → recordedVote (addVote t aid w₀ v₀) aid w ≡ recordedVote t aid w
    go w₀ w [] ne′ = refl
    go w₀ w ((aid' , g') ∷ t) ne′ with aid ≟ aid'
    ... | no  _    = go w₀ w t ne′
    ... | yes refl rewrite dec-yes (aid ≟ aid) refl .proj₂ with w₀ | w
    ...   | $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1024}{\htmlId{7728}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#7735}{\htmlId{7735}{\htmlClass{Bound}{\text{c₀}}}}\,  \end{pmatrix}$ | $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1027}{\htmlId{7747}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#7754}{\htmlId{7754}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ = refl
    ...   | $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1024}{\htmlId{7782}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#7789}{\htmlId{7789}{\htmlClass{Bound}{\text{c₀}}}}\,  \end{pmatrix}$ | $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1032}{\htmlId{7801}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#7808}{\htmlId{7808}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix}$ = refl
    ...   | $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1027}{\htmlId{7836}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#7843}{\htmlId{7843}{\htmlClass{Bound}{\text{c₀}}}}\,  \end{pmatrix}$ | $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1024}{\htmlId{7855}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#7862}{\htmlId{7862}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ = refl
    ...   | $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1027}{\htmlId{7890}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#7897}{\htmlId{7897}{\htmlClass{Bound}{\text{c₀}}}}\,  \end{pmatrix}$ | $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1032}{\htmlId{7909}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#7916}{\htmlId{7916}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix}$ = refl
    ...   | $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1032}{\htmlId{7944}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#7951}{\htmlId{7951}{\htmlClass{Bound}{\text{kh₀}}}}\, \end{pmatrix}$ | $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1024}{\htmlId{7963}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#7970}{\htmlId{7970}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ = refl
    ...   | $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1032}{\htmlId{7998}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#8005}{\htmlId{8005}{\htmlClass{Bound}{\text{kh₀}}}}\, \end{pmatrix}$ | $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1027}{\htmlId{8017}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#8024}{\htmlId{8024}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ = refl
    ...   | $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1024}{\htmlId{8052}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#8059}{\htmlId{8059}{\htmlClass{Bound}{\text{c₀}}}}\,  \end{pmatrix}$ | $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1024}{\htmlId{8071}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#8078}{\htmlId{8078}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix}$ =
      lookupᵐ?-insert-≢ (gvCC (votes g')) λ c₀≡c → ne′ (cong $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1024}{\htmlId{8150}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#8131}{\htmlId{8161}{\htmlClass{Bound}{\text{c₀≡c}}}}\,\,\htmlId{8165}{\htmlClass{Symbol}{\text{)}}}\,
    \,\htmlId{8171}{\htmlClass{Symbol}{\text{...}}}\,   \,\htmlId{8177}{\htmlClass{Symbol}{\text{|}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1027}{\htmlId{8181}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#8188}{\htmlId{8188}{\htmlClass{Bound}{\text{c₀}}}}\,  \end{pmatrix} \,\htmlId{8196}{\htmlClass{Symbol}{\text{|}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1027}{\htmlId{8200}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#8207}{\htmlId{8207}{\htmlClass{Bound}{\text{c}}}}\,  \end{pmatrix} \,\htmlId{8214}{\htmlClass{Symbol}{\text{=}}}\,
      \,\href{abstract-set-theory.Axiom.Set.Map.Extra.html#32684}{\htmlId{8222}{\htmlClass{Function}{\text{lookupᵐ?-insert-≢}}}}\, \,\htmlId{8240}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#8001}{\htmlId{8241}{\htmlClass{Field}{\text{gvDRep}}}}\, \,\htmlId{8248}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#12574}{\htmlId{8249}{\htmlClass{Field}{\text{votes}}}}\, \,\htmlId{8255}{\htmlClass{Bound}{\text{g'}}}\,\,\htmlId{8257}{\htmlClass{Symbol}{\text{))}}}\, \,\htmlId{8260}{\htmlClass{Symbol}{\text{λ}}}\, \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#8262}{\htmlId{8262}{\htmlClass{Bound}{\text{c₀≡c}}}}\, \,\htmlId{8267}{\htmlClass{Symbol}{\text{→}}}\, \,\htmlId{8269}{\htmlClass{Bound}{\text{ne′}}}\, \,\htmlId{8273}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{8274}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1027}{\htmlId{8281}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#8262}{\htmlId{8292}{\htmlClass{Bound}{\text{c₀≡c}}}}\,\,\htmlId{8296}{\htmlClass{Symbol}{\text{)}}}\,
    \,\htmlId{8302}{\htmlClass{Symbol}{\text{...}}}\,   \,\htmlId{8308}{\htmlClass{Symbol}{\text{|}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1032}{\htmlId{8312}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#8319}{\htmlId{8319}{\htmlClass{Bound}{\text{kh₀}}}}\, \end{pmatrix} \,\htmlId{8327}{\htmlClass{Symbol}{\text{|}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1032}{\htmlId{8331}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  \\ \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#8338}{\htmlId{8338}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix} \,\htmlId{8345}{\htmlClass{Symbol}{\text{=}}}\,
      \,\href{abstract-set-theory.Axiom.Set.Map.Extra.html#32684}{\htmlId{8353}{\htmlClass{Function}{\text{lookupᵐ?-insert-≢}}}}\, \,\htmlId{8371}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#8032}{\htmlId{8372}{\htmlClass{Field}{\text{gvSPO}}}}\, \,\htmlId{8378}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#12574}{\htmlId{8379}{\htmlClass{Field}{\text{votes}}}}\, \,\htmlId{8385}{\htmlClass{Bound}{\text{g'}}}\,\,\htmlId{8387}{\htmlClass{Symbol}{\text{))}}}\, \,\htmlId{8390}{\htmlClass{Symbol}{\text{λ}}}\, \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#8392}{\htmlId{8392}{\htmlClass{Bound}{\text{kh₀≡kh}}}}\, \,\htmlId{8399}{\htmlClass{Symbol}{\text{→}}}\, \,\htmlId{8401}{\htmlClass{Bound}{\text{ne′}}}\, \,\htmlId{8405}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{8406}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1032}{\htmlId{8413}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Properties.LastVoteApplied.html#8392}{\htmlId{8424}{\htmlClass{Bound}{\text{kh₀≡kh}}}}\,\,\htmlId{8430}{\htmlClass{Symbol}{\text{)}}}\,

4. recordedVote-addAction-≢¶

Proposing a new action with a different id leaves the recorded vote unchanged.

This concerns a GOV-Propose step. Proposing adds a fresh action via insertGovAction, a priority-ordered insert. Looking up any other id is unaffected, since the new entry carries the fresh id and insertGovAction preserves the relative order of the existing entries. This is where the freshness hypothesis is consumed: the proposed id (txid , k) differs from aid.

lookupGAState-insertGovAction-≢ : ∀ s (p : GovActionID × GovActionState) {aid}
  → proj₁ p ≢ aid → lookupGAState (insertGovAction s p) aid ≡ lookupGAState s aid
lookupGAState-insertGovAction-≢ []                 (aid₀ , ast₀) {aid} ne with aid ≟ aid₀
... | yes refl = ⊥-elim (ne refl)
... | no  _    = refl
lookupGAState-insertGovAction-≢ ((gaID , astH) ∷ s) (aid₀ , ast₀) {aid} ne
  with govActionPriority (GovActionTypeOf astH) ≤? govActionPriority (GovActionTypeOf ast₀)
lookupGAState-insertGovAction-≢ ((gaID , astH) ∷ s) (aid₀ , ast₀) {aid} ne | yes _
  with aid ≟ gaID
... | yes refl = refl
... | no  _    = lookupGAState-insertGovAction-≢ s (aid₀ , ast₀) ne
lookupGAState-insertGovAction-≢ ((gaID , astH) ∷ s) (aid₀ , ast₀) {aid} ne | no  _
  with aid ≟ aid₀
... | yes refl = ⊥-elim (ne refl)
... | no  _    = refl

recordedVote-addAction-≢ :
  {s : GovState }
  {e : Epoch }
  {aid₀ aid : GovActionID }
  {addr : RewardAddress }
  {a : GovAction }
  {prev : NeedsHash (gaType a) }
  {voter : GovVoter}
  → aid₀ ≢ aid
  → recordedVote (addAction s e aid₀ addr a prev) aid voter ≡ recordedVote s aid voter
recordedVote-addAction-≢ {s} {e} {aid₀} {aid} {addr} {a} {prev} ne
  rewrite lookupGAState-insertGovAction-≢ s (mkGovStatePair e aid₀ addr a prev) {aid} ne = refl

The fold lemma¶

Once a matching vote appears, foldl stepVote produces that vote regardless of the starting accumulator (a later matching vote overrides, a non-match keeps the accumulator). In particular, starting from nothing (as lastVoteOn does) can be replaced by starting from any accumulator.

foldl-stepVote-nothing :
  {aid : GovActionID}
  {voter : GovVoter}
  (vps : List (GovVote ⊎ GovProposal))
  (acc : Maybe Vote)
  {v : Vote}
  → foldl (stepVote voter aid) nothing  vps ≡ just v
  → foldl (stepVote voter aid) acc      vps ≡ just v
foldl-stepVote-nothing [] acc ()
foldl-stepVote-nothing (inj₂ p ∷ vps) acc h = foldl-stepVote-nothing vps acc h
foldl-stepVote-nothing {aid} {voter} (inj₁ gv ∷ vps) acc h
  with GovVote.voter gv ≟ voter | gv .gid ≟ aid
... | yes _ | yes _ = h
... | yes _ | no  _ = foldl-stepVote-nothing vps acc h
... | no  _ | yes _ = foldl-stepVote-nothing vps acc h
... | no  _ | no  _ = foldl-stepVote-nothing vps acc h

Induction on the GOVS derivation¶

The base case is a single GOV vote step: the cast vote is recorded on the targeted action.

vote-applied-to-GA : Type
vote-applied-to-GA = ∀ {Γ k s s'} {gv : GovVote}
  → (Γ , k) ⊢ s ⇀⦇ inj₁ gv ,GOV⦈ s'
  → recordedVote s' (gv .gid) (GovVoterOf gv) ≡ just (VoteOf gv)

The base case follows immediately: a GOV-Vote step exists only when the voted action is present, which is the premise recordedVote-addVote needs.

vote-applied : vote-applied-to-GA
vote-applied (GOV-Vote (aid∈s , _)) = recordedVote-addVote aid∈s

Lifting to a whole block (the GOVS closure of GOV), the last vote a voter casts on an action is the one recorded in the resulting state.

This needs one precondition: the action aid being voted on must not have been created by the current transaction, i.e. Γ .txid ≢ proj₁ aid. Without it the claim is false. Indeed, suppose a GOV-Propose in the same block yields a fresh action with id (txid , k); if that collides with a pre-existing aid it is inserted (by priority) ahead of the voted entry and shadows it, so recordedVote no longer sees the vote.

Fortunately, Γ .txid ≢ proj₁ aid holds for every state reachable in the ledger (actions already in s carry the ids of earlier transactions), so the condition only rules out voting on an action proposed within the very same transaction.¹

The lifting is a direct induction on the GOVS derivation. At each step one of the per-step facts above rewrites the accumulator — a vote splits (via voter ≟/gid ≟) into the three recordedVote-addVote* facts, and a proposal uses recordedVote-addAction-≢ (where the freshness hypothesis is consumed); cong threads the equation through the remaining fold while the induction hypothesis supplies the tail.

Inducting on the derivation — rather than on the bare list of signals divorced from the state — is what makes the matching-vote case provable: the GOV-Vote rule carries the proof that the voted action is present, which recordedVote-addVote requires. (A pure fold over the signals could not know this, and indeed the claim is false without it: a matching vote on an action absent from the state would be reported by stepVote yet not recorded.)

lift-GOVS :
  {Γ      : GovEnv}
  {n      : ℕ}
  {s s'   : GovState}
  {vps    : List (GovVote ⊎ GovProposal)}
  {aid    : GovActionID}
  {voter  : GovVoter}
  → Γ .txid ≢ proj₁ aid
  → _⊢_⇀⟦_⟧ᵢ*'_ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS} {_⊢_⇀⦇_,GOV⦈_} (Γ , n) s vps s'
  → recordedVote s' aid voter ≡ foldl (stepVote voter aid) (recordedVote s aid voter) vps
lift-GOVS _ (BS-base Id-nop) = refl
lift-GOVS {aid = aid} {voter} fresh
  (BS-ind {sigs = sigs} (GOV-Vote {aid = aid₁} {voter = voter₁} (m∈ , _)) rest)
  with voter₁ ≟ voter | aid₁ ≟ aid

... | yes refl | yes refl =
  trans  (lift-GOVS fresh rest)
         (cong  (λ acc → foldl (stepVote voter aid) acc sigs)
                (recordedVote-addVote m∈))

... | no  v≢   | yes refl =
  trans  (lift-GOVS fresh rest)
         (cong  (λ acc → foldl (stepVote voter aid) acc sigs)
                (recordedVote-addVote-≢voter v≢))

... | yes _    | no  a≢   =
  trans  (lift-GOVS fresh rest)
         (cong  (λ acc → foldl (stepVote voter aid) acc sigs)
                (recordedVote-addVote-≢gid a≢))

... | no  _    | no  a≢   =
  trans  (lift-GOVS fresh rest)
         (cong  (λ acc → foldl (stepVote voter aid) acc sigs)
                (recordedVote-addVote-≢gid a≢))

lift-GOVS {s = s} {aid = aid} {voter} fresh
  (BS-ind {sigs = sigs} (GOV-Propose _) rest) =
    trans  (lift-GOVS fresh rest)
           (cong  (λ acc → foldl (stepVote voter aid) acc sigs)
                  (recordedVote-addAction-≢ {s} λ eq → fresh (cong proj₁ eq)) )

Finally, both claims follow. The lifted statement combines lift-GOVS with foldl-stepVote-nothing (the last vote in the block survives folding from any starting accumulator).

last-vote-applied : last-vote-applied-to-GA
last-vote-applied {s = s} {vps = vps} {aid} {voter} fresh govs lvo =
  trans (lift-GOVS fresh govs) (foldl-stepVote-nothing vps (recordedVote s aid voter) lvo)

This is a potential TODO item: formally prove the claim, "GovEnv.txid Γ ≢ proj₁ aid holds for every state reachable in the ledger." ↩