GasperBeaconChain
Core
AtomicDef
State: Votes and states

Votes and states

A vote (attestation) is a five-tuple (v,\, s,\, t,\, h_s,\, h_t) recording that validator v supports a link from source checkpoint s at height h_s to target checkpoint t at height h_t. A protocol state \sigma is a finite set of such votes.

The central predicate of this file is vote_msg, which asserts membership of a vote in a state: \sigma \ni (v, s, t, h_s, h_t). This predicate is the foundation for all quorum and slashing definitions in subsequent files.

Representation choice

A state is represented extensionally as a Finset of votes (State unfolds to Finset (Vote Validator Hash)). Three consequences follow from this choice:

duplicate identical votes collapse — a vote is either present or absent, never present "twice";
the state records only extensional membership, not the order in which votes were inserted;
no temporal or network metadata (timestamps, rounds, delivery order) is stored at this layer.

This file therefore models the logical content of a vote state, not its network history. The representation is a design choice, not a mathematical necessity.

Coq source: State.v. Coq represents a vote as a nested tuple; Lean uses a structure with named fields. The two types Validator : Type u and Hash : Type v live in separate universes, avoiding an unnecessary restriction.

A vote as a link

Each vote is a directed link from a source checkpoint (s, h_s) to a target checkpoint (t, h_t), labelled by the attesting validator v (top row). Bundled with v and the two heights, that link is a Vote, and the predicate vote_msg asserts that the Vote belongs to the state \sigma, a State (bottom row). The identifier nodes Vote, vote_msg, and State are the real declarations: hover for the signature and click to jump to the definition.

%%mermaid
graph LR
  source["source (s, hₛ)"] -->|"validator v"| target["target (t, hₜ)"]
  target -->|"bundled with v, hₛ, hₜ"| Vote
  Vote -->|"vote_msg"| State

A Casper FFG vote — the atomic element of a protocol state. A vote pairs an attesting validator v with a source checkpoint (s, h_s) and a target checkpoint (t, h_t), where \mathsf{Validator} and \mathsf{Hash} are the validator and block-identifier types respectively:

(v,\; s,\; t,\; h_s,\; h_t) \;\in\; \mathsf{Validator} \times \mathsf{Hash} \times \mathsf{Hash} \times \mathbb{N} \times \mathbb{N}

The five fields correspond to:

validator — v, the attesting validator,
source — s, the source block identifier,
target — t, the target block identifier,
sourceHeight — h_s, the source height,
targetHeight — h_t, the target height.

The presence or absence of a vote in a state \sigma is queried via vote_msg and forms the basis of quorum and slashing predicates in subsequent files.

structure Vote (Validator : Type u) (Hash : Type v) where
  validator : Validator
  source : Hash
  target : Hash
  sourceHeight : Nat
  targetHeight : Nat
deriving DecidableEq, Repr

A protocol state is a finite set of votes: \sigma \in \mathcal{P}_{\mathrm{fin}}(\mathsf{Vote}).

This corresponds to Coq's {fset Vote}.

abbrev State
    (Validator : Type u)
    (Hash : Type v)
    [DecidableEq Validator]
    [DecidableEq Hash] :=
  Finset (Vote Validator Hash)

The membership predicate for votes in a state. Writing \sigma \ni (v, s, t, h_s, h_t) for vote_msg st v s t s_h t_h, this asserts that the vote \langle v, s, t, h_s, h_t \rangle belongs to the finite set \sigma:

\operatorname{vote\_msg}(\sigma, v, s, t, h_s, h_t) \;\;\coloneqq\;\; \langle v,\, s,\, t,\, h_s,\, h_t \rangle \in \sigma

This is the foundational predicate from which link_supporters, slashed_double_vote, and slashed_surround_vote are built.

def vote_msg
    {Validator : Type u}
    {Hash : Type v}
    [DecidableEq Validator]
    [DecidableEq Hash]
    (st : State Validator Hash)
    (v : Validator)
    (s t : Hash)
    (s_h t_h : Nat) : Prop :=
  ({ validator := v
     source := s
     target := t
     sourceHeight := s_h
     targetHeight := t_h } : Vote Validator Hash) ∈ st

vote_msg is decidable: the underlying Vote type derives DecidableEq, so membership in the finite set \sigma is decided by Finset.decidableMem.

instance vote_msg_decidable
    {Validator : Type u}
    {Hash : Type v}
    [DecidableEq Validator]
    [DecidableEq Hash]
    (st : State Validator Hash)
    (v : Validator)
    (s t : Hash)
    (s_h t_h : Nat) :
    Decidable (vote_msg st v s t s_h t_h) :=
  Finset.decidableMem _ st

Projection of the validator component.

def vote_val
    {Validator : Type u}
    {Hash : Type v}
    (vote : Vote Validator Hash) : Validator :=
  vote.validator

Projection of the source block.

def vote_source
    {Validator : Type u}
    {Hash : Type v}
    (vote : Vote Validator Hash) : Hash :=
  vote.source

Projection of the target block.

def vote_target
    {Validator : Type u}
    {Hash : Type v}
    (vote : Vote Validator Hash) : Hash :=
  vote.target

Projection of the source height.

def vote_source_height
    {Validator : Type u}
    {Hash : Type v}
    (vote : Vote Validator Hash) : Nat :=
  vote.sourceHeight

Projection of the target height.

def vote_target_height
    {Validator : Type u}
    {Hash : Type v}
    (vote : Vote Validator Hash) : Nat :=
  vote.targetHeight

\eta-expansion for votes: every vote \mathbf{w} equals the structure reconstructed from its five projections:

\begin{gathered} \mathbf{w} \;=\; \bigl\langle\, \operatorname{vote\_val}(\mathbf{w}),\;\; \operatorname{vote\_source}(\mathbf{w}),\;\; \operatorname{vote\_target}(\mathbf{w}), \\ \qquad\qquad \operatorname{vote\_source\_height}(\mathbf{w}),\;\; \operatorname{vote\_target\_height}(\mathbf{w}) \,\bigr\rangle \end{gathered}

The five projections are vote_val, vote_source, vote_target, vote_source_height, vote_target_height. The equality is definitional: by \eta-expansion for structures, with the projections unfolded, the two sides are the same term.

Coq: vote_unfold.

theorem vote_unfold
    {Validator : Type u}
    {Hash : Type v}
    (vote : Vote Validator Hash) :
    vote =
      { validator := vote_val vote
        source := vote_source vote
        target := vote_target vote
        sourceHeight := vote_source_height vote
        targetHeight := vote_target_height vote } :=
  match vote with | ⟨_, _, _, _, _⟩ => rfl

Forward direction of the vote_msg unfolding: given \mathbf{w} \in \sigma with \mathbf{w} = \langle v, s, t, h_s, h_t \rangle,

\operatorname{vote\_msg}(\sigma,\; v,\; s,\; t,\; h_s,\; h_t)

holds. That is, membership of a Vote structure in a state implies the membership predicate with the vote's field values as arguments.

theorem vote_msg_of_mem
    {Validator : Type u}
    {Hash : Type v}
    [DecidableEq Validator]
    [DecidableEq Hash]
    {st : State Validator Hash}
    {vote : Vote Validator Hash}
    (h : vote ∈ st) :
    vote_msg st
      vote.validator
      vote.source
      vote.target
      vote.sourceHeight
      vote.targetHeight :=
  match vote, h with | ⟨_, _, _, _, _⟩, h => h

Reverse direction of the vote_msg unfolding:

\operatorname{vote\_msg}(\sigma, v, s, t, h_s, h_t) \;\;\implies\;\; \langle v, s, t, h_s, h_t \rangle \in \sigma

Together with vote_msg_of_mem, this makes explicit that vote_msg is definitionally equal to set membership \langle v, s, t, h_s, h_t \rangle \in \sigma.

theorem mem_of_vote_msg
    {Validator : Type u}
    {Hash : Type v}
    [DecidableEq Validator]
    [DecidableEq Hash]
    {st : State Validator Hash}
    {v : Validator}
    {s t : Hash}
    {s_h t_h : Nat}
    (h : vote_msg st v s t s_h t_h) :
    ({ validator := v
       source := s
       target := t
       sourceHeight := s_h
       targetHeight := t_h } : Vote Validator Hash) ∈ st :=
  h

Transfers a uniform upper bound on target heights to a specific vote:

\bigl(\forall\, \mathbf{w} \in \sigma,\; \mathbf{w}.\mathit{targetHeight} \le H\bigr) \;\wedge\; \sigma \ni (v, s, t, h_s, h_t) \;\;\implies\;\; h_t \le H

The proof constructs the Vote structure from the vote_msg arguments and applies the bound hypothesis.

theorem target_height_le_of_vote_msg
    {Validator : Type u}
    {Hash : Type v}
    [DecidableEq Validator]
    [DecidableEq Hash]
    {st : State Validator Hash}
    {v : Validator} {s t : Hash} {s_h t_h : Nat}
    {H : Nat}
    (hbound : ∀ vote : Vote Validator Hash, vote ∈ st → vote.targetHeight ≤ H)
    (hvm : vote_msg st v s t s_h t_h) :
    t_h ≤ H :=
  hbound ⟨v, s, t, s_h, t_h⟩ hvm