fixup! ChainOrder: test laws

IntersectMBO · Apr 25, 2024 · 0796d29 · 0796d29
1 parent d1c1768
commit 0796d29
Show file tree

Hide file tree

Showing 3 changed files with 32 additions and 29 deletions.
diff --git a/ouroboros-consensus-protocol/test/protocol-test/Test/Consensus/Protocol/Praos/SelectView.hs b/ouroboros-consensus-protocol/test/protocol-test/Test/Consensus/Protocol/Praos/SelectView.hs
@@ -43,7 +43,7 @@ instance Crypto c => Arbitrary (PraosChainSelectView c) where
       csvChainLength <- BlockNo <$> choose (1, size)
       csvSlotNo      <- SlotNo  <$> choose (1, size)
       csvIssuer      <- elements knownIssuers
-      csvIssueNo     <- choose (1, size)
+      csvIssueNo     <- genIssueNo
       pure PraosChainSelectView {
           csvChainLength
         , csvSlotNo
@@ -61,18 +61,21 @@ instance Crypto c => Arbitrary (PraosChainSelectView c) where
          $ unGen (replicateM numIssuers (SL.VKey <$> arbitrary)) randomSeed 100
        where
          randomSeed = mkQCGen 4 -- chosen by fair dice roll
+         numIssuers = 10
 
-         -- TODO Increase this to a value like 10 once the issue number
-         -- tiebreaker has been fixed to be transitive. See the document in
-         -- https://github.com/IntersectMBO/ouroboros-consensus/pull/891 for
-         -- details.
-         --
-         -- TL;DR: In an edge case, the issue number tiebreaker prevents the
-         -- chain order to be transitive. This could be fixed relatively easily,
-         -- namely by swapping the issue number tiebreaker and the VRF
-         -- tiebreaker. However, this is technically not backwards-compatible,
-         -- impacting the current pre-Conway diffusion pipelining scheme.
-         numIssuers = 1
+     -- TODO Actually randomize this once the issue number tiebreaker has been
+     -- fixed to be transitive. See the document in
+     -- https://github.com/IntersectMBO/ouroboros-consensus/pull/891 for
+     -- details.
+     --
+     -- TL;DR: In an edge case, the issue number tiebreaker prevents the
+     -- chain order from being transitive. This could be fixed relatively
+     -- easily, namely by swapping the issue number tiebreaker and the VRF
+     -- tiebreaker. However, this is technically not backwards-compatible,
+     -- impacting the current pre-Conway diffusion pipelining scheme.
+     --
+     -- See https://github.com/IntersectMBO/ouroboros-consensus/issues/1075.
+     genIssueNo = pure 1
 
      -- The header VRF is a deterministic function of the issuer VRF key, the
      -- slot and the epoch nonce. Additionally, for any particular chain, the

diff --git a/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/Protocol.hs b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/Protocol.hs
@@ -12,7 +12,7 @@ import           Test.Tasty.QuickCheck
 import           Test.Util.QuickCheck
 
 -- | Test the laws of the 'ChainOrder' class (in particular, that 'Ord' is
--- lawful) /except/ of the high-level "Chain extension precedence" property.
+-- lawful) /except/ for the high-level "Chain extension precedence" property.
 tests_chainOrder ::
      forall a.
      ( ChainOrder a

diff --git a/ouroboros-consensus/src/unstable-consensus-testlib/Test/Util/QuickCheck.hs b/ouroboros-consensus/src/unstable-consensus-testlib/Test/Util/QuickCheck.hs
@@ -237,33 +237,33 @@ prop_lawfulEqAndTotalOrd ::
      forall a. (Show a, Ord a)
   => a -> a -> a -> Property
 prop_lawfulEqAndTotalOrd a b c = conjoin
-    [ counterexample "Not total: not (a <= b || b <= a)" $
-        (a `le` b) .||. (b `le` a)
-    , counterexample "Not transitive: not (a <= b && b <= c => a <= c)" $
+    [ counterexample "Not total: a <= b || b <= a VIOLATED" $
+        a <= b || b <= a
+    , counterexample "Not transitive: a <= b && b <= c => a <= c VIOLATED" $
         let antecedent = a <= b && b <= c in
         classify antecedent "Antecedent for transitivity" $
-        antecedent `implies` a `le` c
-    , counterexample "Not reflexive: not (a <= a)" $
+        antecedent `implies` a <= c
+    , counterexample "Not reflexive: a <= a VIOLATED" $
         a `le` a
-    , counterexample "Not antisymmetric: not (a <= b && b <= a => a == b)" $
+    , counterexample "Not antisymmetric: a <= b && b <= a => a == b VIOLATED" $
         let antecedent = a <= b && b <= a in
         classify antecedent "Antecedent for antisymmetry" $
-        antecedent `implies` a === b
+        antecedent `implies` a == b
     , -- compatibility laws
-      counterexample "not ((a <= b) == (b >= a))" $
+      counterexample "(a <= b) == (b >= a) VIOLATED" $
         (a <= b) === (b >= a)
-    , counterexample "not ((a < b) == (a <= b && a /= b))" $
+    , counterexample "(a < b) == (a <= b && a /= b) VIOLATED" $
         (a < b) === (a <= b && a /= b)
-    , counterexample "not ((a > b) = (b < a))" $
+    , counterexample "(a > b) = (b < a) VIOLATED" $
         (a > b) === (b < a)
-    , counterexample "not ((a < b) == (compare a b == LT))" $
+    , counterexample "(a < b) == (compare a b == LT) VIOLATED" $
         (a < b) === (compare a b == LT)
-    , counterexample "not ((a > b) == (compare a b == GT))" $
+    , counterexample "(a > b) == (compare a b == GT) VIOLATED" $
         (a > b) === (compare a b == GT)
-    , counterexample "not ((a == b) == (compare a b == EQ))" $
+    , counterexample "(a == b) == (compare a b == EQ) VIOLATED" $
         (a == b) === (compare a b == EQ)
-    , counterexample "not (min a b == if a <= b then a else b)" $
+    , counterexample "min a b == if a <= b then a else b VIOLATED" $
         min a b === if a <= b then a else b
-    , counterexample "not (max a b == if a >= b then a else b)" $
-        max a b == if a >= b then a else b
+    , counterexample "max a b == if a >= b then a else b VIOLATED" $
+        max a b === if a >= b then a else b
     ]