Test FetchModeGenesis in BlockFetch tests

IntersectMBO · Aug 19, 2024 · c347554 · c347554
1 parent 2e89bfc
commit c347554
Showing 1 changed file with 151 additions and 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
@@ -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.