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
• validityCheckTime: the time it takes to validate a given EB (in slots)

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-IB 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 }
 
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) π
          ──────────────────────────────────────────────────────
          s ↝ (addUpkeep s EB-Role , Send (ebHeader eb) nothing)

        
      

  VT-Role : ∀ {ebHash slot'}
          → let open LeiosState s
          in
          ∙ getCurrentEBHash s ≡ just ebHash
          ∙ find (λ (s , 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 + validityCheckTime eb
          ∙ validityCheckTime eb ≤  * Lhdr + Lvote
          ∙ EndorserBlockOSig.txs eb ≢ []
          ∙ needsUpkeep VT-Role
          ∙ canProduceV (slotNumber eb) sk-VT (stake s)
          ───────────────────────────────────────────────────────
          s ↝ ( rememberVote (addUpkeep s VT-Role) eb
              , Send (vtHeader [ vote sk-VT (hash eb) ]) nothing)

        
      

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

allDone : LeiosState → Type
allDone record { Upkeep = u } = fromList u ≡ᵉ fromList (EB-Role ∷ VT-Role ∷ Base ∷ [])

        
      

Linear Leios transitions

The relation describing the transition given input and state #### Initialization

open Types params
 
data _⊢_ : VTy → LeiosState → Type where
  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'
       ────────────────────────────────────────────────────────────────
       V ⊢ initLeiosState V SD pks

        
      

data _-⟦_/_⟧⇀_ : MachineType (FFD ⊗ BaseC) (IO ⊗ Adv) LeiosState where

        
      

Network and Ledger

  Slot₁ : let open LeiosState s in
        ∙ allDone s
        ───────────────────────────────────────────────────────────────────────────────────
        s -⟦ honestOutputI (rcvˡ (-, FFD-OUT msgs)) / honestInputO' (sndʳ (-, FTCH-LDG)) ⟧⇀
          record s { slot         = suc slot
                   ; Upkeep       = []
                   } ↑ L.filter (isValid? s) msgs
 
  Slot₂ : let open LeiosState s in
        ──────────────────────────────────────────────────────────────────────────────
        s -⟦ honestOutputI (rcvʳ (-, BASE-LDG rbs)) / nothing ⟧⇀ record s { RBs = rbs }

        
      

  Ftch : let open LeiosState s in
       ────────────────────────────────────────────────────────────────────────────
       s -⟦ honestInputI (-, FetchLdgI) / honestOutputO' (-, 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₁   :
          ──────────────────────────────────────────────────────────────────────────────
          s -⟦ honestInputI (-, 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 fzero)
                rb = record
                       { txs = proj₁ (splitTxs ToPropose)
                       ; announcedEB = hash <$> toProposeEB s π
                       ; ebCert = proj₂ <$> currentCertEB }
          in
          ∙ needsUpkeep Base
          ────────────────────────────────────────────────────────────────────────────
          s -⟦ honestOutputI (rcvˡ (-, SLOT)) / honestInputO' (sndʳ (-, SUBMIT rb)) ⟧⇀
            addUpkeep s Base

        
      

Protocol rules

  Roles₁ :
         ∙ s ↝ (s' , i)
         ──────────────────────────────────────────────────────────────────────────────
         s -⟦ honestOutputI (rcvˡ (-, SLOT)) / honestInputO' (sndˡ (-, FFD-IN i)) ⟧⇀ s'
 
  Roles₂ : ∀ {x u s'} → let open LeiosState s in
         ∙ ¬ (s ↝ (s' , x))
         ∙ needsUpkeep u
         ∙ u ≢ Base
         ──────────────────────────────────────────────────────────────
         s -⟦ honestOutputI (rcvˡ (-, SLOT)) / nothing ⟧⇀ addUpkeep s u