fixup! Add tests for PerasWeightSnapshot

Author: amesgen

ouroboros-consensus/test/consensus-test/Test/Consensus/Peras/WeightSnapshot.hs

@@ -51,8 +51,12 @@ prop_perasWeightSnapshot testSetup =
           | pt <- tsPoints
           ]
       , conjoin
-          [ counterexample ("Incorrect weight for " <> condense frag) $
-              weightBoostOfFragmentReference frag =:= weightBoostOfFragment snap frag
+          [ conjoin
+              [ counterexample ("Incorrect weight for " <> condense frag) $
+                  weightBoostOfFragmentReference frag =:= weightBoostOfFragment snap frag
+              , counterexample ("Weight not inductively consistent for " <> condense frag) $
+                  prop_fragmentInduction snap frag
+              ]
           | frag <- tsFragments
           ]
       ]
@@ -74,6 +78,31 @@ prop_perasWeightSnapshot testSetup =
       (weightBoostOfPointReference . blockPoint)
       (AF.toOldestFirst frag)
 
+-- | Test that the weight of a fragment is equal to the weight of its
+-- first\/last point plus the weight of the remaining suffix\/infix.
+prop_fragmentInduction ::
+  PerasWeightSnapshot TestBlock ->
+  AnchoredFragment TestBlock ->
+  Property
+prop_fragmentInduction snap =
+  \frag -> fromLeft frag .&&. fromRight frag
+ where
+  fromLeft :: AnchoredFragment TestBlock -> Property
+  fromLeft frag = case frag of
+    AF.Empty _ ->
+      weightBoostOfFragment snap frag === mempty
+    b AF.:< frag' ->
+      weightBoostOfFragment snap frag
+        === weightBoostOfPoint snap (blockPoint b) <> weightBoostOfFragment snap frag'
+
+  fromRight :: AnchoredFragment TestBlock -> Property
+  fromRight frag = case frag of
+    AF.Empty _ ->
+      weightBoostOfFragment snap frag === mempty
+    frag' AF.:> b ->
+      weightBoostOfFragment snap frag
+        === weightBoostOfPoint snap (blockPoint b) <> weightBoostOfFragment snap frag'
+
 data TestSetup = TestSetup
   { tsWeights :: Map (Point TestBlock) PerasWeight
   , tsPoints :: [Point TestBlock]