Local state from the view of a single node.

Each node records whether it can proposed or voted in the current epoch:

data Phase : Type where
  Ready Voted : 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 phase : Phase
        db    : List Message
        inbox : List Message
        final : Chain

The initial local state is the empty one:

initLocalState : LocalState
initLocalState = ⦅ Ready , [] , [] , genesisChain ⦆

Chains contained within messages

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

Chain membership

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

data _chain-∈_ : Chain → List Message → Type where
  [] :
      ───────────────────────
      genesisChain chain-∈ ms

  _∷_⊣_ :
    ∀ (m∈ : Any ((b ≡_) ∘ _∙block) ms) →
    ∙ ch chain-∈ ms
    ∙ b -connects-to- ch
      ────────────────────────────────
      (b ∷ ch) chain-∈ ms

Notarized Chains

A block is notarized when it has been voted by the majority.

module _ (ms : List Message) where
  module _ (b : Block) where
    votes : List Message
    votes = filter ((b ≟_) ∘ _∙block) ms

    voteIds : List Pid
    voteIds = map _∙pid votes

    voteRightBlock : All ((b ≡_) ∘ _∙block) votes
    voteRightBlock = L.All.all-filter ((b ≟_) ∘ _∙block) ms

    seenVotes : votes ⊆ˢ ms
    seenVotes = L.SubS.filter-⊆ ((b ≟_) ∘ _∙block) ms

    record NotarizedBlock : Type where

      field enoughVotes : IsMajority votes


      enoughVoteIds : IsMajority voteIds
      enoughVoteIds rewrite L.length-map _∙pid votes = enoughVotes

      votesNonempty : length votes > 0
      votesNonempty with votes in eq
      ... | [] = ⊥-elim (majority⁺ (subst IsMajority eq enoughVotes))
      ... | x ∷ xs = Nat.s≤s Nat.z≤n

    open NotarizedBlock public
      -- NB: Proposals count as votes

  NotarizedChain : Chain → Type
  NotarizedChain = All NotarizedBlock

  data FinalizedChain : Chain → Block → Type where
    Finalize : ∀ {ch b₁ b₂ b₃} →
      ∙ NotarizedChain (b₃ ∷ b₂ ∷ b₁ ∷ ch)
      ∙ b₃ .epoch ≡ suc (b₂ .epoch)
      ∙ b₂ .epoch ≡ suc (b₁ .epoch)
        ───────────────────────────────────
        FinalizedChain (b₂ ∷ b₁ ∷ ch) b₃

_notarized-chain-∈_ : Chain → List Message → Type
ch notarized-chain-∈ ms
  = (ch chain-∈ ms)
  × NotarizedChain ms ch

Often we will need to talk about the longest notarized chain seen so far.

_≤ᶜʰ_ _≼_ : Chain → Chain → Type
_≤ᶜʰ_ = _≤_ on length
_≼_   = Suffix≡

data Longest∈ (ch : Chain) (ms : List Message) : Type where
  mkLongest∈ :
    (∀ {ch′} → ch′ notarized-chain-∈ ms → ch′ ≤ᶜʰ ch)
    ─────────────────────────────────────────────────
    Longest∈ ch ms

_longest-notarized-chain-∈_ : Chain → List Message → Type
ch longest-notarized-chain-∈ ms
  = ch notarized-chain-∈ ms
  × Longest∈ ch ms