From c347554662b4187e1aac31b44675a1fdf82523ad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Mon, 19 Aug 2024 12:03:33 +0000 Subject: [PATCH] Test FetchModeGenesis in BlockFetch tests --- .../Test/Ouroboros/Network/BlockFetch.hs | 163 ++++++++++++++++-- 1 file changed, 151 insertions(+), 12 deletions(-) diff --git a/ouroboros-network/sim-tests-lib/Test/Ouroboros/Network/BlockFetch.hs b/ouroboros-network/sim-tests-lib/Test/Ouroboros/Network/BlockFetch.hs index 0d6f0c32ff1..3c7eec8baaa 100644 --- a/ouroboros-network/sim-tests-lib/Test/Ouroboros/Network/BlockFetch.hs +++ b/ouroboros-network/sim-tests-lib/Test/Ouroboros/Network/BlockFetch.hs @@ -75,6 +75,16 @@ tests = testGroup "BlockFetch" , testProperty "termination" $ prop_terminate (PraosFetchMode FetchModeBulkSync) ] + , testGroup "Genesis" + [ testProperty "static chains without overlap" $ + prop_blockFetchStaticNoOverlap FetchModeGenesis + + , testProperty "static chains with overlap" $ + prop_blockFetchStaticWithOverlap FetchModeGenesis + + , testProperty "termination" $ + prop_terminate FetchModeGenesis + ] , testCaseSteps "bracketSyncWithFetchClient" unit_bracketSyncWithFetchClient , testProperty "compare comparePeerGSV" prop_comparePeerGSV @@ -88,8 +98,14 @@ tests = testGroup "BlockFetch" -- | In this test we have two candidates chains that are static throughout the -- run. The two chains share some common prefix (genesis in the degenerate --- case). The test runs the block fetch logic to download all of both chain --- candidates. +-- case). +-- +-- With a Praos fetch mode, the test runs the block fetch logic to download all +-- blocks of both chain candidates. +-- +-- With GenesisFetchMode, the test runs the block fetch logic to download all +-- blocks of the longest candidate chain (either of them if they are of equal +-- length). -- -- In this variant we set up the common prefix of the two candidates as the -- \"current\" chain. This means the block fetch only has to download the @@ -100,7 +116,7 @@ tests = testGroup "BlockFetch" -- This runs the block fetch and then checks that the trace of the events in -- that run satisfy the trace properties: -- --- * 'tracePropertyBlocksRequestedAndRecievedPerPeer' +-- * 'tracePropertyBlocksRequestedAndReceivedPerPeerPraos' -- * 'tracePropertyClientStateSanity' -- * 'tracePropertyInFlight' -- @@ -112,7 +128,11 @@ prop_blockFetchStaticNoOverlap fetchMode (TestChainFork common fork1 fork2) = -- For fetch reqs added and received, we observe exactly the sequence -- of blocks we expect, which is the whole fork suffix. - tracePropertyBlocksRequestedAndRecievedPerPeer fork1'' fork2'' trace + case fetchMode of + FetchModeGenesis -> + tracePropertyBlocksRequestedAndReceivedPerPeerGenesis fork1'' fork2'' trace + PraosFetchMode{} -> + tracePropertyBlocksRequestedAndReceivedPerPeerPraos fork1'' fork2'' trace -- state sanity check .&&. property (tracePropertyClientStateSanity trace) @@ -155,7 +175,7 @@ prop_blockFetchStaticNoOverlap fetchMode (TestChainFork common fork1 fork2) = -- This runs the block fetch and then checks that the trace of the events in -- that run satisfy the trace properties: -- --- * 'tracePropertyBlocksRequestedAndRecievedAllPeers' +-- * 'tracePropertyBlocksRequestedAndReceivedAllPeersPraos' -- * 'tracePropertyNoDuplicateBlocksBetweenPeers' -- * 'tracePropertyClientStateSanity' -- * 'tracePropertyInFlight' @@ -170,7 +190,11 @@ prop_blockFetchStaticWithOverlap fetchMode (TestChainFork _common fork1 fork2) = -- For fetch reqs added and received, between the two peers we observe -- the set of blocks we expect, which is the union of the two chains. - tracePropertyBlocksRequestedAndRecievedAllPeers fork1' fork2' trace + case fetchMode of + FetchModeGenesis -> + tracePropertyBlocksRequestedAndReceivedAllPeersGenesis fork1' fork2' trace + PraosFetchMode{} -> + tracePropertyBlocksRequestedAndReceivedAllPeersPraos fork1' fork2' trace -- For fetch reqs added, the set of blocks added for the two peers -- should not intersect @@ -229,7 +253,7 @@ instance Show Example1TraceEvent where -- requested and completed by both fetch clients is exactly the sequence -- expected. The expected sequence is exactly the chain suffixes in order. -- --- This property is stronger than 'tracePropertyBlocksRequestedAndRecievedAllPeers' +-- This property is stronger than 'tracePropertyBlocksRequestedAndReceivedAllPeersPraos' -- since it works with sequences rather than sets and for each chain -- individually rather than both chains together. It only holds for the -- situation where the suffixes of the chains that need to be fetched are @@ -238,12 +262,12 @@ instance Show Example1TraceEvent where -- It turns out that no duplicates part is not trivial. Earlier versions of the -- block fetch logic did not satisfy this in all cases. -- -tracePropertyBlocksRequestedAndRecievedPerPeer +tracePropertyBlocksRequestedAndReceivedPerPeerPraos :: AnchoredFragment Block -> AnchoredFragment Block -> [Example1TraceEvent] -> Property -tracePropertyBlocksRequestedAndRecievedPerPeer fork1 fork2 es = +tracePropertyBlocksRequestedAndReceivedPerPeerPraos fork1 fork2 es = requestedFetchPoints === requiredFetchPoints .&&. receivedFetchPoints === requiredFetchPoints where @@ -273,6 +297,65 @@ tracePropertyBlocksRequestedAndRecievedPerPeer fork1 fork2 es = (TraceLabelPeer peer (CompletedBlockFetch pt _ _ _ _ _)) <- es ] +-- | Check the execution trace for a particular property: we observe all the +-- blocks in the 'FetchRequest's added by the decision logic and the blocks +-- received by the fetch clients; check that the ordered sequence of blocks +-- requested and completed by both fetch clients is exactly the sequence +-- expected. The expected sequence is exactly the longest chain suffix, or +-- either of them if they are of equal length. +-- +-- This property is stronger than 'tracePropertyBlocksRequestedAndReceivedAllPeersGenesis' +-- since it works with sequences rather than sets and for each chain +-- individually rather than both chains together. It only holds for the +-- situation where the suffixes of the chains that need to be fetched are +-- disjoint, sharing no common prefix. +-- +-- It turns out that no duplicates part is not trivial. Earlier versions of the +-- block fetch logic did not satisfy this in all cases. +-- +tracePropertyBlocksRequestedAndReceivedPerPeerGenesis + :: AnchoredFragment Block + -> AnchoredFragment Block + -> [Example1TraceEvent] + -> Property +tracePropertyBlocksRequestedAndReceivedPerPeerGenesis fork1 fork2 es = + counterexample "should request the expected blocks" + (disjoin $ map (requestedFetchPoints ===) requiredFetchPoints) + .&&. counterexample "should receive the expected blocks" + (disjoin $ map (receivedFetchPoints ===) requiredFetchPoints) + where + requiredFetchPoints = + if AnchoredFragment.length fork1 == AnchoredFragment.length fork2 + then [ requiredFetchPointsFor 1 fork1 + , requiredFetchPointsFor 2 fork2 + , Map.union (requiredFetchPointsFor 1 fork1) (requiredFetchPointsFor 2 fork2) + ] + else if AnchoredFragment.length fork1 < AnchoredFragment.length fork2 + then [requiredFetchPointsFor 2 fork2] + else [requiredFetchPointsFor 1 fork1] + + requiredFetchPointsFor peer fork = + Map.filter (not . Prelude.null) $ + Map.fromList [ (peer, chainPoints fork) ] + + requestedFetchPoints :: Map Int [Point BlockHeader] + requestedFetchPoints = + Map.fromListWith (flip (++)) + [ (peer, map blockPoint (AnchoredFragment.toOldestFirst fragment)) + | TraceFetchClientState + (TraceLabelPeer peer + (AddedFetchRequest + (FetchRequest fragments) _ _ _)) <- es + , fragment <- fragments + ] + + receivedFetchPoints :: Map Int [Point BlockHeader] + receivedFetchPoints = + Map.fromListWith (flip (++)) + [ (peer, [pt]) + | TraceFetchClientState + (TraceLabelPeer peer (CompletedBlockFetch pt _ _ _ _ _)) <- es + ] -- | Check the execution trace for a particular property: we observe all the -- blocks in the 'FetchRequest's added by the decision logic and the blocks @@ -281,16 +364,16 @@ tracePropertyBlocksRequestedAndRecievedPerPeer fork1 fork2 es = -- set of all blocks received. The expected set of blocks is the union of the -- blocks on the two candidate chains. -- --- This property is weaker than 'tracePropertyBlocksRequestedAndRecievedPerPeer' +-- This property is weaker than 'tracePropertyBlocksRequestedAndReceivedPerPeerPraos' -- since it does not involve order or frequency, but it holds for the general -- case of multiple chains with common prefixes. -- -tracePropertyBlocksRequestedAndRecievedAllPeers +tracePropertyBlocksRequestedAndReceivedAllPeersPraos :: AnchoredFragment Block -> AnchoredFragment Block -> [Example1TraceEvent] -> Property -tracePropertyBlocksRequestedAndRecievedAllPeers fork1 fork2 es = +tracePropertyBlocksRequestedAndReceivedAllPeersPraos fork1 fork2 es = requestedFetchPoints === requiredFetchPoints .&&. receivedFetchPoints === requiredFetchPoints where @@ -318,6 +401,62 @@ tracePropertyBlocksRequestedAndRecievedAllPeers fork1 fork2 es = ] +-- | Check the execution trace for a particular property: we observe all the +-- blocks in the 'FetchRequest's added by the decision logic and the blocks +-- received by the fetch clients; check that the set of all blocks requested +-- across the two peers is the set of blocks we expect, and similarly for the +-- set of all blocks received. The expected set of blocks is the block of the +-- longest candidate chain, or either of them if they have the same size. +-- +-- This property is weaker than 'tracePropertyBlocksRequestedAndReceivedPerPeerGenesis' +-- since it does not involve order or frequency, but it holds for the general +-- case of multiple chains with common prefixes. +-- +tracePropertyBlocksRequestedAndReceivedAllPeersGenesis + :: AnchoredFragment Block + -> AnchoredFragment Block + -> [Example1TraceEvent] + -> Property +tracePropertyBlocksRequestedAndReceivedAllPeersGenesis fork1 fork2 es = + counterexample "should request the expected blocks" + (disjoin $ map (requestedFetchPoints ===) requiredFetchPoints) + .&&. counterexample "should receive the expected blocks" + (disjoin $ map (receivedFetchPoints ===) requiredFetchPoints) + where + requiredFetchPoints = + if AnchoredFragment.length fork1 == AnchoredFragment.length fork2 + then [ requiredFetchPointsFor fork1 + , requiredFetchPointsFor fork2 + , Set.union (requiredFetchPointsFor fork1) (requiredFetchPointsFor fork2) + ] + else if AnchoredFragment.length fork1 < AnchoredFragment.length fork2 + then [requiredFetchPointsFor fork2] + else [requiredFetchPointsFor fork1] + + requiredFetchPointsFor fork = + Set.fromList $ chainPoints fork + + requestedFetchPoints :: Set (Point BlockHeader) + requestedFetchPoints = + Set.fromList + [ blockPoint block + | TraceFetchClientState + (TraceLabelPeer _ + (AddedFetchRequest + (FetchRequest fragments) _ _ _)) <- es + , fragment <- fragments + , block <- AnchoredFragment.toOldestFirst fragment + ] + + receivedFetchPoints :: Set (Point BlockHeader) + receivedFetchPoints = + Set.fromList + [ pt + | TraceFetchClientState + (TraceLabelPeer _ (CompletedBlockFetch pt _ _ _ _ _)) <- es + ] + + -- | Check the execution trace for a particular property: we observe all the -- blocks in the 'FetchRequest's added by the decision logic; check that the -- set blocks requested for one peer and for the other do not intersect.