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.

Traces

We consider traces of the (global) step relation, defined as its reflexive-transitive closure, and use these to prove invariants as state predicates:

open import Prelude.Closures _—→_ public
  using ( begin_; _∎
        ; _↞—_; _⟨_⟩←—_; _⟨_∣_⟩←—_
        ; _—↠_; _—→⟨_⟩_
        ; Reachable; Invariant; StepPreserved; Step⇒Invariant
        ; Trace; TraceProperty; TraceInvariant
        )

StateProperty = GlobalState → Type

Now, we can consider a specific local step occurring within a sequence of global transitions:

record Step : Type where
  constructor _⊢_
  field
    stepArgs : _ × _ × _ × _ × _
    step : let p , e , ls , mm , ls' = stepArgs in
           p ▷ e ⊢ ls —[ mm ]→ ls'

LocalStepProperty = Step → Type

allLocalSteps : (s′ ↞— s) → List Step
allLocalSteps = λ where
  (_ ∎) → []
  (_ ⟨ LocalStep st ⟩←— tr) → (_ ⊢ st) ∷ allLocalSteps tr
  (_ ⟨ _ ⟩←— tr) → allLocalSteps tr

_∋⋯_ : Trace → LocalStepProperty → Type
(_ , _ , _ , tr) ∋⋯ P = Any P (allLocalSteps tr)