Streamlet Protocol Description

Sending messages

updateLocal : ∀ p ⦃ _ : Honest p ⦄ → LocalState → Op₁ GlobalState
updateLocal p ls s = record s
  { stateMap = s .stateMap [ p ,· it ]≔ ls }

module _
  (s : GlobalState) {env : Envelope}
  (let [ p ∣ m ⟩ = env)
  (env∈ : env ∈ s .networkBuffer) (let envⁱ = L.Any.index env∈) where

  deliverMsg dropMsg : GlobalState
  deliverMsg = record s
    { stateMap      = s .stateMap [ p ]%= receiveMessage m
    ; networkBuffer = L.removeAt (s .networkBuffer) envⁱ
    }
  dropMsg = record s
    { networkBuffer = L.removeAt (s .networkBuffer) envⁱ }

broadcast : Pid → Maybe Message → Op₁ GlobalState
broadcast _   nothing  s = s
broadcast pid (just m) s = record s
  { networkBuffer = s .networkBuffer ++ msgs
  ; history       = m ∷ s .history
  }
  where msgs = L.map [_∣ m ⟩ (filter (pid ≢?_) allPids)

advanceEpoch : Op₁ GlobalState
advanceEpoch s = record s
  { e-now    = suc (s .e-now)
  ; stateMap = V.map epochChange (s .stateMap)
  }

The (global) step relation

data _—→_ (s : GlobalState) : GlobalState → Type where

   -- An *honest* node performs a local step.
  LocalStep : ⦃ _ : Honest p ⦄ →
    (p ▷ s .e-now ⊢ s ＠ p —[ mm ]→ ls′)
    ─────────────────────────────────────────
    s —→ broadcast p mm (updateLocal p ls′ s)

  -- A *dishonest* node can:
  --   - Replay a message sent previously by an honest participant.
  --   - Broadcast any message signed by a dishonest participant.
  --   - Update their local database arbitrarily.
  DishonestLocalStep :
    ∙ Dishonest p
    ∙ (Honest (m ∙pid) → m ∈ s .history)
      ───────────────────────────────────────────────
      s —→ broadcast p (just m) s

  -- * Deliver a message in the network.
  -- Since we may deliver any message on the network, this models
  -- non-determinism in the order that messages may arrive.
  Deliver :
    (env∈ : env ∈ s .networkBuffer) →
    ─────────────────────────────────
    s —→ deliverMsg s env∈

  -- * Advancing to the next epoch.
  AdvanceEpoch :
    ───────────────────
    s —→ advanceEpoch s

  -- * A message is lost in the network.
  Drop :
    (env∈ : env ∈ s .networkBuffer) →
    ─────────────────────────────────
    s —→ dropMsg s env∈

Note : We have system epoch but not local epochs. In a synchronous network (like the one assumed in Streamlet) only the system epoch is needed. If we were to assume a partially-synchronous network then we need the epoch in each local state.