ouroboros-consensus-test-0.1.0.0: Tests of the consensus layer
Safe HaskellNone
LanguageHaskell2010

Test.ThreadNet.Util

Synopsis

Chain properties

chainCommonPrefixHasHeader 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

Re-exports

newtype NumBlocks Source #

Constructors

NumBlocks Word64 

Instances

Instances details
Eq NumBlocks Source # 
Instance details

Defined in Test.ThreadNet.Util.Expectations

Show NumBlocks Source # 
Instance details

Defined in Test.ThreadNet.Util.Expectations

determineForkLengthSecurityParamNodeJoinPlanLeaderScheduleNumBlocks 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.

A round-robin LeaderSchedule will always reach consensus, so the fork length will be 0. For other LeaderSchedules -- 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.

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.