Short-Pipeline Leios

This document is a specification of Short-Pipeline Leios, usually abbreviated as Short Leios. On a high level, the pipeline looks like this:

1. If elected, propose IB
2. Wait
3. Wait
4. If elected, propose EB
5. If elected, vote If elected, propose RB

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 IB-Role EB-Role VT-Role : SlotUpkeep

        
      

Block/Vote production rules

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.

data _↝_ : LeiosState → LeiosState → Type where

        
      

Positive rules

  IB-Role : let open LeiosState s renaming (FFDState to ffds)
                b = ibBody (record { txs = ToPropose })
                h = ibHeader (mkIBHeader slot id π sk-IB ToPropose)
          in
          ∙ needsUpkeep IB-Role
          ∙ canProduceIB slot sk-IB (stake s) π
          ∙ ffds FFD.-⟦ Send h (just b) / SendRes ⟧⇀ ffds'
          ─────────────────────────────────────────────────────────────────────────
          s ↝ addUpkeep record s { FFDState = ffds' } IB-Role

        
      

  EB-Role : let open LeiosState s renaming (FFDState to ffds)
                LI = map getIBRef $ filter (_∈ᴮ slice L slot ) IBs
                h = mkEB slot id π sk-EB LI []
          in
          ∙ needsUpkeep EB-Role
          ∙ canProduceEB slot sk-EB (stake s) π
          ∙ ffds FFD.-⟦ Send (ebHeader h) nothing / SendRes ⟧⇀ ffds'
          ─────────────────────────────────────────────────────────────────────────
          s ↝ addUpkeep record s { FFDState = ffds' } EB-Role

        
      

  VT-Role : let open LeiosState s renaming (FFDState to ffds)
                EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot ) EBs
                votes = map (vote sk-VT ∘ hash) EBs'
          in
          ∙ needsUpkeep VT-Role
          ∙ canProduceV slot sk-VT (stake s)
          ∙ ffds FFD.-⟦ Send (vtHeader votes) nothing / SendRes ⟧⇀ ffds'
          ─────────────────────────────────────────────────────────────────────────
          s ↝ addUpkeep record s { FFDState = ffds' } VT-Role

        
      

Negative rules

  No-IB-Role : let open LeiosState s in
             ∙ needsUpkeep IB-Role
             ∙ (∀ π → ¬ canProduceIB slot sk-IB (stake s) π)
             ─────────────────────────────────────────────
             s ↝ addUpkeep s IB-Role

        
      

  No-EB-Role : let open LeiosState s in
             ∙ needsUpkeep EB-Role
             ∙ (∀ π → ¬ canProduceEB slot sk-EB (stake s) π)
             ─────────────────────────────────────────────
             s ↝ addUpkeep s EB-Role

        
      

  No-VT-Role : let open LeiosState s in
             ∙ needsUpkeep VT-Role
             ∙ ¬ canProduceV slot sk-VT (stake s)
             ─────────────────────────────────────────────
             s ↝ addUpkeep s VT-Role

        
      

Uniform short-pipeline

stage : ℕ → ⦃ _ : NonZero L ⦄ → ℕ
stage s = s / L
 
beginningOfStage : ℕ → Type
beginningOfStage s = stage s * L ≡ s
 
allDone : LeiosState → Type
allDone record { slot = slot ; Upkeep = Upkeep } =
      (beginningOfStage slot × Upkeep ≡ᵉ fromList (IB-Role ∷ EB-Role ∷ VT-Role ∷ Base ∷ []))
  ⊎ (¬ beginningOfStage slot × Upkeep ≡ᵉ fromList (IB-Role ∷ VT-Role ∷ Base ∷ []))
  ⊎ (slot ≡ zero × Upkeep ≡ᵉ fromList (Base ∷ []))
 
data _-⟦_/_⟧⇀_ : Maybe LeiosState → LeiosInput → LeiosOutput → LeiosState → Type where

        
      

Initialization

  Init :
       ∙ ks K.-⟦ K.INIT pk-IB pk-EB pk-VT / K.PUBKEYS pks ⟧⇀ ks'
       ∙ initBaseState B.-⟦ B.INIT (V-chkCerts pks) / B.STAKE SD ⟧⇀ bs'
       ────────────────────────────────────────────────────────────────
       nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD bs' pks

        
      

Network and Ledger

  Slot : let open LeiosState s renaming (FFDState to ffds; BaseState to bs) in
       ∙ allDone s
       ∙ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG rbs ⟧⇀ bs'
       ∙ ffds FFD.-⟦ Fetch / FetchRes msgs ⟧⇀ ffds'
       ───────────────────────────────────────────────────────────────────────
       just s -⟦ SLOT / EMPTY ⟧⇀ record s
           { FFDState  = ffds'
           ; BaseState = bs'
           ; Ledger    = constructLedger rbs
           ; slot      = suc slot
           ; Upkeep    = ∅
           } ↑ L.filter (isValid? s) msgs

        
      

  Ftch :
       ────────────────────────────────────────────────────────
       just s -⟦ FTCH-LDG / FTCH-LDG (LeiosState.Ledger s) ⟧⇀ 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₁   :
          ───────────────────────────────────────────────────────────────────
          just s -⟦ SUBMIT (inj₂ txs) / EMPTY ⟧⇀ record s { ToPropose = txs }

        
      

  Base₂a  : let open LeiosState s renaming (BaseState to bs) in
          ∙ needsUpkeep Base
          ∙ eb ∈ filter (λ eb → isVoteCertified s eb × eb ∈ᴮ slice L slot ) EBs
          ∙ bs B.-⟦ B.SUBMIT (this eb) / B.EMPTY ⟧⇀ bs'
          ───────────────────────────────────────────────────────────────────────
          just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base
 
  Base₂b  : let open LeiosState s renaming (BaseState to bs) in
          ∙ needsUpkeep Base
          ∙ [] ≡ filter (λ eb → isVoteCertified s eb × eb ∈ᴮ slice L slot ) EBs
          ∙ bs B.-⟦ B.SUBMIT (that ToPropose) / B.EMPTY ⟧⇀ bs'
          ───────────────────────────────────────────────────────────────────────
          just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base

        
      

Protocol rules

  Roles :
        ∙ s ↝ s'
        ─────────────────────────────
        just s -⟦ SLOT / EMPTY ⟧⇀ s'