Linear Leios

This document is a specification of Linear Leios. It removes concurrency at the transaction level by producing one (large) EB for every Praos block.

In addition to the expected paramaters, we assume a two functions:

• splitTxs: produces a pair of a list of transactions that can be included in an RB and a list of transactions that can be included in an EB
• isValidityChecked: whether validation of a given EB has completed by a given slot

Upkeep

A node that never produces a block even though it could is not supposed to be an honest node, and we prevent that by tracking whether a node has checked if it can make a block in a particular slot. LeiosState contains a set of SlotUpkeep and we ensure that this set contains all elements before we can advance to the next slot, resetting this field to the empty set.

data SlotUpkeep : Type where
  Base EB-Role VT-Role : SlotUpkeep

        
      

Block/Vote production

We now define the rules for block production given by the relation _↝_. These are split in two:

1. Positive rules, when we do need to create a block.
2. Negative rules, when we cannot create a block.

The purpose of the negative rules is to properly adjust the upkeep if we cannot make a block.

Note that _↝_, starting with an empty upkeep can always make exactly three steps corresponding to the three types of Leios specific blocks.

toProposeEB : LeiosState → VrfPf → Maybe EndorserBlock
toProposeEB s π = let open LeiosState s in case proj₂ (splitTxs ToPropose) of λ where
  [] → nothing
  _ → just $ mkEB slot id π sk-EB ToPropose
 
getCurrentEBHash : LeiosState → Maybe EBRef
getCurrentEBHash s = let open LeiosState s in
  RankingBlock.announcedEB currentRB
 
isEquivocated : LeiosState → EndorserBlock → Type
isEquivocated s eb = Any (areEquivocated eb) (toSet (LeiosState.EBs s))
 
rememberVote : LeiosState → EndorserBlock → LeiosState
rememberVote s@(record { VotedEBs = vebs }) eb = record s { VotedEBs = hash eb ∷ vebs }
 
-- Record the EB this party is diffusing, so that `Base₂` announces the block
-- that actually went out rather than recomputing a candidate from `ToPropose`.
rememberProposal : LeiosState → EndorserBlock → LeiosState
rememberProposal s eb = record s { proposedEB = just (hash eb) }
 
data _↝_ : LeiosState → LeiosState × FFDAbstract.Input ffdAbstract → Type where

        
      

Positive rules

In this specification, we don’t want to peek behind the base chain abstraction. This means that we assume instead that the canProduceEB predicate is satisfied if and only if we can make an RB. In that case, we send out an EB with the transactions currently stored in the mempool.

  EB-Role : let open LeiosState s in
          ∙ toProposeEB s π ≡ just eb
          ∙ canProduceEB slot sk-EB (stake s) π
          ∙ needsUpkeep EB-Role
          ───────────────────────────────────────────────────────
          s ↝ (rememberProposal (addUpkeep s EB-Role) eb , Send (ebHeader eb) nothing)

        
      

  VT-Role : ∀ {ebHash slot'}
          → let open LeiosState s
          in
          ∙ getCurrentEBHash s ≡ just ebHash
          ∙ find (λ (_ , eb') → hash eb' ≟ ebHash) EBs' ≡ just (slot' , eb)
          ∙ hash eb ∉ VotedEBs
          ∙ ¬ isEquivocated s eb
          ∙ isValid s (inj₁ (ebHeader eb))
          ∙ slot' ≤ slotNumber eb + Lhdr
          ∙ slotNumber eb +  * Lhdr ≤ slot
          ∙ slot ≤ slotNumber eb +  * Lhdr + Lvote
          ∙ isValidityChecked slot eb
          ∙ EndorserBlockOSig.txs eb ≢ []
          ∙ needsUpkeep VT-Role
          ∙ inVotingCommittee params (stake s)
          -- Only a pool with a registered voting key may sign
          ∙ id ∈ˡ L.map poolID PubKeys
          ───────────────────────────────────────────────────────
          s ↝ ( rememberVote (addUpkeep s VT-Role) eb
              , Send (vtHeader [ vote sk-VT (hash currentRB) ]) nothing)

        
      

Predicate needed for slot transition. Special care needs to be taken when starting from genesis.

allDone : LeiosState → Type
allDone record { Upkeep = u } = VT-Role ∈ˡ u × EB-Role ∈ˡ u × Base ∈ˡ u

        
      

Voting happens within a window: it opens 3 * Lhdr slots after the announcing RB’s slot (the equivocation-detection period) and closes Lvote slots later. voteDeadline is the last slot at which the current EB may still be voted on; when there is no current EB (or it has not been received yet) the deadline is 0, so the deferral rule Roles₃ below is vacuously inapplicable and abstention is governed solely by Roles₂.

voteDeadline : LeiosState → ℕ
voteDeadline s = let open LeiosState s in
  case getCurrentEBHash s of λ where
    nothing       → 
    (just ebHash) → case find (λ (_ , eb') → hash eb' ≟ ebHash) EBs' of λ where
      nothing         → 
      (just (_ , eb)) → slotNumber eb +  * Lhdr + Lvote

        
      

Linear Leios transitions

The relation describing the transition given input and state

open Types params
open BaseAbstract B'
 
data _-⟦_/_⟧⇀_ : MachineType (FFD ⊗₀ BaseIO) (IO ⊗₀ Adv) LeiosState where

        
      

Network and Ledger

  Slot₁ : let open LeiosState s in
        ∙ allDone s
        ──────────────────────────────────────────────────────────────────
        s -⟦ (ϵ ⊗R) ⊗R ↑ᵢ FFD-OUT msgs / just $ (L⊗ ϵ) ⊗R ↑ₒ FTCH-LDG ⟧⇀
          let s' = s ↑ L.filter (isValid? s) msgs
          in record s'
               { slot       = suc slot
               ; Upkeep     = []
               ; proposedEB = nothing
               }
 
  Slot₂ : let open LeiosState s in
        ───────────────────────────────────────────────────────────────────
        s -⟦ (L⊗ ϵ) ⊗R ↑ᵢ BASE-LDG rbs / nothing ⟧⇀ record s { RBs = rbs }

        
      

  Ftch : let open LeiosState s in
       ───────────────────────────────────────────────────────────────────────────
       s -⟦ L⊗ (ϵ ⊗R) ᵗ¹ ↑ₒ FetchLdgI / just $ L⊗ (ϵ ⊗R) ᵗ¹ ↑ᵢ FetchLdgO Ledger ⟧⇀ s

        
      

Base chain

Note: Submitted data to the base chain is only taken into account if the party submitting is the block producer on the base chain for the given slot

Base₂ announces the EB recorded by EB-Role, not a candidate recomputed from ToPropose. The premise hasUpkeep EB-Role makes the party settle its EB role for the slot first, either by producing (which sets proposedEB) or by declining through Roles₂; without it a Base₂ step scheduled early in the slot would announce nothing and strand the EB the party goes on to diffuse.

  Base₁   :
          ───────────────────────────────────────────────────────────────────────────
          s -⟦ L⊗ (ϵ ᵗ¹ ⊗R) ᵗ¹ ↑ᵢ SubmitTxs txs / nothing ⟧⇀ record s { ToPropose = txs }
 
  Base₂   : let open LeiosState s
                currentCertEB = find (λ (eb , _) →
                  ¿ just (hash eb) ≡ getCurrentEBHash s
                  × slotNumber eb +  * Lhdr + Lvote + Ldiff ≤ slot ¿) ebsWithCert
                rb = record
                       { announcedEB = proposedEB
                       ; txsOrEbCert = case currentCertEB of λ where
                           (just (_ , cert)) → inj₂ cert
                           nothing → inj₁ (proj₁ (splitTxs ToPropose))
                       }
          in
          ∙ needsUpkeep Base
          ∙ hasUpkeep EB-Role
          ───────────────────────────────────────────────────────────────────────────
          s -⟦ (ϵ ⊗R) ⊗R ↑ᵢ SLOT / just $ (L⊗ ϵ) ⊗R ↑ₒ SUBMIT rb ⟧⇀ addUpkeep s Base

        
      

Protocol rules

  Roles₁ :
         ∙ s ↝ (s' , i)
         ────────────────────────────────────────────────────────────
         s -⟦ (ϵ ⊗R) ⊗R ↑ᵢ SLOT / just $ (ϵ ⊗R) ⊗R ↑ₒ FFD-IN i ⟧⇀ s'
 
  Roles₂ : ∀ {u} → let open LeiosState in
         ∙ ¬ (∃[ s'×i ] (s ↝ s'×i × Upkeep (addUpkeep s u) ≡ Upkeep (proj₁ s'×i)))
         ∙ needsUpkeep s u
         ∙ u ≢ Base
         ──────────────────────────────────────────────────
         s -⟦ (ϵ ⊗R) ⊗R ↑ᵢ SLOT / nothing ⟧⇀ addUpkeep s u

        
      

Deferral of the VT-Role: abstaining from voting is permitted while the current EB’s voting window is still open, even when a positive VT-Role step could fire. Together with Roles₂ this yields bounded liveness: at the deadline slot neither Roles₃ (window closes) nor Roles₂ (a vote can still fire) applies, so a vote must be cast by then.

  Roles₃ : let open LeiosState s in
         ∙ slot < voteDeadline s
         ∙ needsUpkeep VT-Role
         ──────────────────────────────────────────────────
         s -⟦ (ϵ ⊗R) ⊗R ↑ᵢ SLOT / nothing ⟧⇀ addUpkeep s VT-Role