Local state from the view of a single node.

data Phase : Type where
  EnteringRound Proposing Receiving AdvancingRound Locking Committing Voting : Phase

Furthermore, the local state stores a database of blocks and votes, an inbox for unread messages, and the current finalized chain.

record LocalState : Type where
  constructor ⦅_,_,_,_,_,_,_,_,_,_,_⦆
  field
    r-vote    : Round     -- highest voted round
    -- r-lock    : Round     -- highest locked round
    r-cur     : Round     -- current round
    qc-high   : QC        -- highest quorum certificate
    tc-last   : Maybe TC  -- last round timeout certificate

    phase      : Phase     -- current phase
    db         : Messages  -- list of processed messages
    inbox      : Messages  -- messages received, but not yet processed
    finalChain : Chain     -- the most recent committed chain

    timer      : Maybe Time -- (optional) timer to fire
    timedOut?  : Bool       -- whether the timer has fired

    roundAdvanced? : Bool -- whether the round has advanced

  currentLeader = roundLeader r-cur
  nextLeader    = roundLeader ( + r-cur)

  timedOut : Time → Type
  timedOut t = Any (_≤ t) timer

initLocalState : LocalState
initLocalState = record
  { r-vote = 
  -- ; r-lock = 0
  ; r-cur = 
  ; qc-high = qc₀
  ; tc-last = nothing
  ; phase = EnteringRound
  ; db = []
  ; inbox = []
  ; finalChain = []
  ; timer =  nothing
  ; timedOut? = false
  ; roundAdvanced? = true
  }

Blocks and Chains contained within messages

Membership class

record Has∈ (A : Type) : Type₁ where
  field _∙∈_ : A → Messages → Type
  _∙∉_ = ¬_ ∘₂ _∙∈_
  infix  _∙∈_

  module _ ⦃ _ : _∙∈_ ⁇² ⦄ where
    _∙∈?_ : Decidable² _∙∈_
    _∙∈?_ = dec²
open Has∈ ⦃...⦄ public

data AllMs {A} ⦃ _ : Has∈ A ⦄ (P : A → Type) (ms : Messages) : Type where
  mk : (∀ {a} → a ∙∈ ms → P a) → AllMs P ms

Block Membership

{-
data _-block-∈-_ : Block → Messages → Type where
  initialBlock :
    b ∙blockId ≡ genesisId
    ──────────────────────
    b -block-∈- ms

  proposedBlock :
    b ∈ allBlocks ms
    ────────────────
    b -block-∈- ms

  -- In the paper there's no other way of learning about a block.
  -- inQC :
  --     ∙ Any (qc qc∈-Message_) ms
  --     ∙ qc ∙blockId ≡ b ∙blockId
  --     ───────────────────────────
  --     b block-∈ ms

instance Has∈-Block = Has∈ Block ∋ λ where ._∙∈_ → _-block-∈-_
-}

instance Has∈-Block = Has∈ Block ∋ λ where ._∙∈_ b ms → b ∈ allBlocks ms

We define different Predicates on chains wrt to lists of messages.

QC membership

qcVoteShares : QC → VoteShares
qcVoteShares qc = map (qc .payload signed-by_) (qc .shares)

instance Has∈-VS = Has∈ VoteShare ∋ λ where ._∙∈_ vs ms → Vote vs ∈ ms

FormedVS : VoteShares → Messages → Type
FormedVS vss ms = All (_∙∈ ms) vss

FormedQC : QC → Messages → Type
FormedQC qc = FormedVS (qcVoteShares qc)

data _-qc-∈-_ (qc : QC) (ms : Messages) : Type where
  initialQC :
    qc ≡ qc₀
    ────────────
    qc -qc-∈- ms

  formedQC :
    FormedQC qc ms -- all voteshares come from ms
    ──────────────
    qc -qc-∈- ms

  receivedQC :
    Any (qc qc∈-Message_) ms
    ────────────────────────
    qc -qc-∈- ms

TC Membership

_-te-∈-_ : TimeoutEvidence → Messages → Type
te -te-∈- ms = ∃ λ mtc → Timeout (te , mtc) ∈ ms

instance Has∈-TimeoutEvidence = Has∈ TimeoutEvidence ∋ λ where ._∙∈_ → _-te-∈-_

FormedTE : List TimeoutEvidence → Messages → Type
FormedTE tes ms = All (_∙∈ ms) tes

FormedTC : TC → Messages → Type
FormedTC tc = FormedTE (tc .tes)

data _-tc-∈-_ (tc : TC) (ms : Messages) : Type where
  formedTC :
    FormedTC tc ms
    ──────────────────────
    tc -tc-∈- ms

  receivedTC :
    Any (tc tc∈-Message_) ms
    ────────────────────────
    tc -tc-∈- ms

Highest QC

data _-highest-qc-∈-_ : QC → Messages → Type where
  isHighest :
    ∙ qc ∙∈ ms
    ∙ (∀ qc′ → qc′ ∙∈ ms → qc′ ≤qc qc)
      ────────────────────────────────
      qc -highest-qc-∈- ms

Chain membership

The following predicate indicates that the chain has been “seen” (i. e. it is in the database).

data _-chain-∈-_ : Chain → Messages → Type where
  [] :
    ────────────────────
    genesis -chain-∈- ms

  _∷_⊣_ :
    ∙ b ∙∈ ms
    ∙ ch -chain-∈- ms
    ∙ b -connects-to- ch
      ─────────────────────
      (b ∷ ch) -chain-∈- ms

-- TODO: refactor to this definition instead
-- _-chain-∈-_ : Chain → Messages → Type
-- ch -chain-∈- ms = All (_∙∈ ms) ch × ValidChain ch

Certified blocks

A block is certified if there exists a qc for that block.

data _-certified-∈-_ (b : Block) (ms : Messages) : Type where
  certified :
    -- ∙ b ∙∈ ms
    ∙ qc ∙∈ ms
    ∙ qc ∙blockId ≡ b ∙blockId
    ∙ qc ∙round   ≡ b ∙round
      ────────────────────────
      b -certified-∈- ms

Final Chain

data _∶_final-∈_ : Block → Chain → Messages → Type where
  final∈ :
    ∙ b  -certified-∈- ms
    ∙ b′ -certified-∈- ms
    ∙ (b′ ∷ b ∷ ch) ∙∈ ms
    ∙ b′ ∙round ≡  + b ∙round
      ────────────────────────
      b′ ∶ (b ∷ ch) final-∈ ms

_∶_longer-final-∈_ : Block → Chain → LocalState → Type
b ∶ ch longer-final-∈ ls
  = b ∶ ch final-∈ ls .db
  × length ch > length (ls .finalChain)

data _longer-final-∈_ : Block → LocalState → Type where
  mk : ∀ {ch} →
    (b ∶ ch longer-final-∈ ls)
    ──────────────────────────
    b longer-final-∈ ls

Voting conditions

ShouldVote : LocalState → Block → Type
ShouldVote ls ⟨ qc , mtc , r , _ {-⊣ _-} ⟩
  = r ≡ ls .r-cur
  × r > ls .r-vote
  × ( {-(1)-} r ≡  + qc ∙round
    ⊎ {-(2)-} Any (λ tc → r ≡  + tc ∙round × qc ∙round ≥ highestQC tc ∙round) mtc
    )

Proposal conditions

data _-connects-∈-_ (b : Block) (ms : Messages) : Type where
  mk : ∀ {ch : Chain} →
    ∙ ch -chain-∈- ms
    ∙ b -connects-to- ch
      ──────────────────
      b -connects-∈- ms

ValidProposal : Messages → Block → Type
ValidProposal ms b
  = AllBlock (λ b′ → b ∙round ≢ b′ ∙round) ms
  × b -connects-∈- ms -- this is also checked by Commit (longer-final-∈)


ValidProposal⇒ValidBlock : ValidProposal ms b → ValidBlock b
ValidProposal⇒ValidBlock (_ , mk _ (connects∶ _ _ vb)) = vb