| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.ThreadNet.Ref.PBFT
Description
A reference simulator of the PBFT protocol under "ideal circumstances"
See step.
Synopsis
- data Outcome
- data Result
- = Forked !NumSlots !(Map CoreNodeId (Set SlotNo))
- | Nondeterministic
- | Outcomes ![Outcome]
- data State = State {}
- advanceUpTo ∷ PBftParams → NodeJoinPlan → State → SlotNo → State
- definitelyEnoughBlocks ∷ PBftParams → Result → Bool
- emptyState ∷ State
- mkLeaderOf ∷ PBftParams → SlotNo → CoreNodeId
- nullState ∷ State → Bool
- pbftLimit ∷ Integral a ⇒ PBftParams → a
- resultConstrName ∷ Result → String
- simulate ∷ HasCallStack ⇒ PBftParams → NodeJoinPlan → NumSlots → Result
- simulateShort ∷ HasCallStack ⇒ PBftParams → NodeJoinPlan → NumSlots → Either DetOrNondet ShortState
- step ∷ PBftParams → NodeJoinPlan → State → (Outcome, State)
- viable ∷ PBftParams → SlotNo → NodeJoinPlan → State → Bool
Documentation
Outcome of a node leading a slot
Constructors
| Absent | the leader hadn't yet joined |
| Nominal | the leader extended the networks' common chain with a valid block (We're using nominal in the engineer's sense of "according to plan".) |
| Unable | the leader could not forge a valid block |
| Wasted | the leader forged a valid-but-irrelevant block, because it forged before sufficiently synchronizing As of commit 4eb23cfe "Merge #1260", this only happens if a node leads in the slot it joins. In that slot, it forges before the mini protocols are able to pull in any of the existing nodes' chain, and so it re-forges the epoch 0 boundary block (EBB). |
The result of a reference simulation
There is only one way that multiple competing chains arise given the PBFT protocol under "ideal circumstances". When a node leads the slot in which it joins, it will forge before syncing. The fresh one-block chain it creates this way will be competitive if the other chains in the net are also only one block long. Once there is a two-block chain in the net, it will be the prefix of the net's one common chain going forward.
It is possible that the simulator is unable to statically determine which
one-block chain will be the prefix of the common prefix going forward. In
such a Nondeterministic scenario, the simulator inherently can not predict
up to that slot. Moreover, it cannot predict past that slot, since the
choice of chain affects who may be able to lead next. Therefore, the
simulator offers no information beyond identifying this case.
Constructors
| Forked !NumSlots !(Map CoreNodeId (Set SlotNo)) | All the chains in the net consist of 1 block. The map contains the deterministic block selections made by nodes, identifying each one-block chain by the slot in which its block was forged. |
| Nondeterministic | The outcomes cannot be determined statically. |
| Outcomes ![Outcome] | The expected outcomes of each slot. |
The state of a PBFT net with only one longest chain
Constructors
| State | |
advanceUpTo ∷ PBftParams → NodeJoinPlan → State → SlotNo → State Source #
definitelyEnoughBlocks ∷ PBftParams → Result → Bool Source #
Confirm that the simulated chain includes at least k blocks within every
2k-slot window
mkLeaderOf ∷ PBftParams → SlotNo → CoreNodeId Source #
pbftLimit ∷ Integral a ⇒ PBftParams → a Source #
How many blocks in the latest k-blocks that a single core node is
allowed to have signed
simulate ∷ HasCallStack ⇒ PBftParams → NodeJoinPlan → NumSlots → Result Source #
simulateShort ∷ HasCallStack ⇒ PBftParams → NodeJoinPlan → NumSlots → Either DetOrNondet ShortState Source #
step ∷ PBftParams → NodeJoinPlan → State → (Outcome, State) Source #
Advance the state by one slot
ASSUMPTION Any new valid block is immediately selected by all nodes.
This assumption seems mild because of PBFT's fixed round-robin schedule; it primarily constrains the network topology, network outages, node restarts, clock skew, etc to be trivial. In other words, "ideal circumstances".
The assumption is useful in this reference implementation because it lets us
maintain a single "global" State common to all nodes.
viable ∷ PBftParams → SlotNo → NodeJoinPlan → State → Bool Source #
True if there will be no necessary violations of "k-blocks in
2k-slots" before the given slot, assuming all remaining nodes join ASAP
PRE the given parameters and state are not already tooSparse params st
NOTE this function does not consider the competition between 1-block
multichains, so definitelyEnoughBlocks must still be checked to confirm