Global state of the entire system.

The global state consists of a local state for each honest node.

StateMap : Type
StateMap = HonestVec LocalState

Other than that, it records the current epoch, in-flight messages, and the whole history of previous messages.

record GlobalState : Type where
  constructor mkGlobalState
  field
    e-now         : Epoch          -- The current epoch.
    stateMap      : StateMap       -- A map assigning each PID its local state.
    networkBuffer : List Envelope  -- Messages in transit on the network.
    history       : List Message   -- All messages seen so far.

The initial global state starts at epoch 1 with no messages and initial local states.

initStateMap : StateMap
initStateMap = V.replicate _ initLocalState

initGlobalState : GlobalState
initGlobalState = mkGlobalState 1 initStateMap [] []

_＠_ : GlobalState → ∀ p ⦃ _ : Honest p ⦄ → LocalState
s ＠ p = pLookup (s .stateMap) (p ,· it)