Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- chainCommonPrefix ∷ HasHeader b ⇒ Chain b → Chain b → Chain b
- prop_all_common_prefix ∷ (HasHeader b, Condense (HeaderHash b), Eq b) ⇒ Word64 → [Chain b] → Property
- shortestLength ∷ Map NodeId (Chain b) → Natural
- consensusExpected ∷ SecurityParam → NodeJoinPlan → LeaderSchedule → Bool
- emptyLeaderSchedule ∷ NumSlots → LeaderSchedule
- roundRobinLeaderSchedule ∷ NumCoreNodes → NumSlots → LeaderSchedule
- tracesToDot ∷ ∀ b. (GetPrevHash b, HasCreator b) ⇒ Map NodeId (NodeOutput b) → String
- newtype NumBlocks = NumBlocks Word64
- determineForkLength ∷ SecurityParam → NodeJoinPlan → LeaderSchedule → NumBlocks
Chain properties
chainCommonPrefix ∷ HasHeader b ⇒ Chain b → Chain b → Chain b Source #
Find the common prefix of two chains
prop_all_common_prefix ∷ (HasHeader b, Condense (HeaderHash b), Eq b) ⇒ Word64 → [Chain b] → Property Source #
LeaderSchedule
GraphViz Dot
tracesToDot ∷ ∀ b. (GetPrevHash b, HasCreator b) ⇒ Map NodeId (NodeOutput b) → String Source #
Re-exports
determineForkLength ∷ SecurityParam → NodeJoinPlan → LeaderSchedule → NumBlocks Source #
Compute a bound for the length of the final forks
At the end of the test, the nodes' final chains will share a common prefix ("intersection"), though it may be empty. Each node's current chain is a fork off that prefix. No such fork will be longer than the result of this function.
ASSUMPTION: The network connectivity is such that -- barring other non-network considerations -- any block forged at the start of a slot will be fetched and possibly selected by every other node before the end of the slot.
How LeaderSchedule
affects this function
A round-robin LeaderSchedule
will always reach consensus, so the fork
length will be 0
. For other LeaderSchedule
s -- whether known a priori
(see Test.ThreadNet.LeaderSchedule) or a posteriori (see
Test.ThreadNet.Praos) -- we often will not expect consensus. The key
difference is that a round-robin schedule always has exactly one leader per
slot. Arbitrary schedules instead may have 0 or multiple leaders.
A sequence of slots in which no slot has exactly one leader can drive a
network away from consensus. This function bounds how far from consensus the
network could be after the last simulated slot. It determines a conservative
upper bound on the length of the contended suffix of the nodes' final
chains. The bound may be less than, equal, or greater than k
; regardless
of which, it should be used to test the nodes' final chains.
If such a sequence is long enough, it might even prevent the network from
every reaching consensus again: the nodes at the end of the sequence may
have chains that disagree by more than k
blocks, thereby exceeding the
security parameter k
. In particular, if the bound determined by a
LeaderSchedule
is greater than k
, then no extension of that
LeaderSchedule
can determine a lesser bound.
Multiple leaders create divergent chains as follows. Assume that every
leader of s + 1
begins the slot with a chain of length n
, and that no
chain in the network has a greater length. Each leader forges a unique
block. A race condition between ChainSync/BlockFetch and forging makes it
possible, though relatively unlikely, that a leader would have received
another leader's new block before it forges its own. In that case, the new
leader will forged a block but then not select it, since it already selected
the other leader's new block. This function assumes the "worst-case" in
which both leaders make separate chains, thereby breaking consensus. Hence
it computes an upper bound. Each leader thus selects a new n+1
-length
chain, and each non-leader will adopt one of them because they previously
had a chain of length <= n
. Thus the network is likely not in consensus at
the end of a multi-leader slot.
The network will reestablish consensus at the end of a single-leader slot,
because the leader creates the only chain of length n+1
and all other
nodes thus select it.
In a slot with no leaders, all nodes will simply retain their current chains.
How NodeJoinPlan
affects this function
Because the race condition between forging and ChainSync/BlockFetch is consistently won by forging, a node that leads in the same slot it joins always attempts to make a chain of length 1 (ASSUMPTION: new nodes start with an empty chain). Except for the edge cases when the longest chains in the network are of length 0 or 1, this means that leaders who are joining can be disregarded.