ChainOrder: test laws

ouroboros-consensus-protocol/ouroboros-consensus-protocol.cabal

@@ -43,6 +43,12 @@ common common-lib
   if flag(asserts)
     ghc-options: -fno-ignore-asserts
 
+common common-test
+  import: common-lib
+  ghc-options:
+    -threaded
+    -rtsopts
+
 library
   import: common-lib
   hs-source-dirs: src/ouroboros-consensus-protocol
@@ -90,3 +96,24 @@ library unstable-protocol-testlib
     cardano-protocol-tpraos,
     cardano-slotting,
     ouroboros-consensus-protocol,
+
+test-suite protocol-test
+  import: common-test
+  type: exitcode-stdio-1.0
+  hs-source-dirs: test/protocol-test
+  main-is: Main.hs
+  other-modules:
+    Test.Consensus.Protocol.Praos.SelectView
+
+  build-depends:
+    QuickCheck,
+    base,
+    cardano-crypto-class,
+    cardano-ledger-binary:testlib,
+    cardano-ledger-core,
+    containers,
+    ouroboros-consensus:{ouroboros-consensus, unstable-consensus-testlib},
+    ouroboros-consensus-protocol,
+    serialise,
+    tasty,
+    tasty-quickcheck,

ouroboros-consensus-protocol/test/protocol-test/Main.hs

@@ -0,0 +1,14 @@
+module Main (main) where
+
+import qualified Test.Consensus.Protocol.Praos.SelectView
+import           Test.Tasty
+import           Test.Util.TestEnv
+
+main :: IO ()
+main = defaultMainWithTestEnv defaultTestEnvConfig tests
+
+tests :: TestTree
+tests =
+    testGroup "protocol"
+      [ Test.Consensus.Protocol.Praos.SelectView.tests
+      ]

ouroboros-consensus-protocol/test/protocol-test/Test/Consensus/Protocol/Praos/SelectView.hs

@@ -0,0 +1,91 @@
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE FlexibleInstances   #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE NamedFieldPuns      #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
+
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Test.Consensus.Protocol.Praos.SelectView (tests) where
+
+import qualified Cardano.Crypto.Hash as Crypto
+import qualified Cardano.Crypto.Util as Crypto
+import           Cardano.Crypto.VRF (OutputVRF, mkTestOutputVRF)
+import           Cardano.Ledger.Crypto (Crypto (..), StandardCrypto)
+import qualified Cardano.Ledger.Keys as SL
+import           Codec.Serialise (encode)
+import           Control.Monad
+import           Data.Containers.ListUtils (nubOrdOn)
+import           Ouroboros.Consensus.Block
+import           Ouroboros.Consensus.Protocol.Praos.Common
+import           Test.Cardano.Ledger.Binary.Arbitrary ()
+import           Test.Ouroboros.Consensus.Protocol
+import           Test.QuickCheck.Gen (Gen (..))
+import           Test.QuickCheck.Random (mkQCGen)
+import           Test.Tasty
+import           Test.Tasty.QuickCheck hiding (elements)
+import           Test.Util.QuickCheck
+import           Test.Util.TestEnv
+
+tests :: TestTree
+tests = testGroup "PraosChainSelectView"
+    [   adjustQuickCheckTests (* 50)
+      -- Use a small max size by default in order to have a decent chance to
+      -- trigger the actual tiebreaker cases.
+      $ adjustQuickCheckMaxSize (`div` 10)
+      $ tests_chainOrder (Proxy @(PraosChainSelectView StandardCrypto))
+    ]
+
+instance Crypto c => Arbitrary (PraosChainSelectView c) where
+  arbitrary = do
+      size           <- fromIntegral <$> getSize
+      csvChainLength <- BlockNo <$> choose (1, size)
+      csvSlotNo      <- SlotNo  <$> choose (1, size)
+      csvIssuer      <- elements knownIssuers
+      csvIssueNo     <- genIssueNo
+      pure PraosChainSelectView {
+          csvChainLength
+        , csvSlotNo
+        , csvIssuer
+        , csvIssueNo
+        , csvTieBreakVRF = mkVRFFor csvIssuer csvSlotNo
+        }
+   where
+     -- We want to draw from the same small set of issuer identities in order to
+     -- have a chance to explore cases where the issuers of two 'SelectView's
+     -- are identical.
+     knownIssuers :: [SL.VKey SL.BlockIssuer c]
+     knownIssuers =
+           nubOrdOn SL.hashKey
+         $ unGen (replicateM numIssuers (SL.VKey <$> arbitrary)) randomSeed 100
+       where
+         randomSeed = mkQCGen 4 -- chosen by fair dice roll
+         numIssuers = 10
+
+     -- 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
+     -- slot determines the epoch nonce.
+     mkVRFFor :: SL.VKey SL.BlockIssuer c -> SlotNo -> OutputVRF (VRF c)
+     mkVRFFor issuer slot =
+           mkTestOutputVRF
+         $ Crypto.bytesToNatural
+         $ Crypto.hashToBytes
+         $ Crypto.xor (Crypto.castHash issuerHash)
+         $ Crypto.hashWithSerialiser encode slot
+       where
+         SL.KeyHash issuerHash = SL.hashKey issuer

ouroboros-consensus/ouroboros-consensus.cabal

@@ -331,6 +331,7 @@ library unstable-consensus-testlib
     Test.Ouroboros.Consensus.ChainGenerator.Slot
     Test.Ouroboros.Consensus.ChainGenerator.Some
     Test.Ouroboros.Consensus.DiffusionPipelining
+    Test.Ouroboros.Consensus.Protocol
     Test.QuickCheck.Extras
     Test.Util.BoolProps
     Test.Util.ChainDB

ouroboros-consensus/src/unstable-consensus-testlib/Test/Ouroboros/Consensus/Protocol.hs

@@ -0,0 +1,31 @@
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
+
+module Test.Ouroboros.Consensus.Protocol (tests_chainOrder) where
+
+import           Data.Proxy
+import           Data.Typeable (Typeable, typeRep)
+import           Ouroboros.Consensus.Protocol.Abstract
+import           Test.Tasty
+import           Test.Tasty.QuickCheck
+import           Test.Util.QuickCheck
+
+-- | Test the laws of the 'ChainOrder' class (in particular, that 'Ord' is
+-- lawful) /except/ for the high-level "Chain extension precedence" property.
+tests_chainOrder ::
+     forall a.
+     ( ChainOrder a
+     , Typeable a
+     , Arbitrary a
+     , Show a
+     , Arbitrary (ChainOrderConfig a)
+     , Show (ChainOrderConfig a)
+     )
+  => Proxy a
+  -> TestTree
+tests_chainOrder aPrx = testGroup ("ChainOrder " <> show (typeRep aPrx))
+    [ testProperty "Eq & Ord" (prop_lawfulEqAndTotalOrd @a)
+    , testProperty "Consistency with Ord" $ \cfg (a :: a) b ->
+        preferCandidate cfg a b ==> a `lt` b
+    ]

ouroboros-consensus/src/unstable-consensus-testlib/Test/Util/QuickCheck.hs

@@ -29,6 +29,8 @@ module Test.Util.QuickCheck (
   , collects
   , forAllGenRunShrinkCheck
   , implies
+    -- * Typeclass laws
+  , prop_lawfulEqAndTotalOrd
   ) where
 
 import           Control.Monad.Except
@@ -226,3 +228,42 @@ collects = repeatedly collect
 implies :: Testable prop => Bool -> prop -> Property
 implies p1 p2 = not p1 .||. p2
 infixr 0 `implies`
+
+{-------------------------------------------------------------------------------
+  Typeclass laws
+-------------------------------------------------------------------------------}
+
+prop_lawfulEqAndTotalOrd ::
+     forall a. (Show a, Ord a)
+  => a -> a -> a -> Property
+prop_lawfulEqAndTotalOrd a b c = conjoin
+    [ 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 <= c
+    , counterexample "Not reflexive: a <= a VIOLATED" $
+        a `le` a
+    , 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
+    , -- compatibility laws
+      counterexample "(a <= b) == (b >= a) VIOLATED" $
+        (a <= b) === (b >= a)
+    , counterexample "(a < b) == (a <= b && a /= b) VIOLATED" $
+        (a < b) === (a <= b && a /= b)
+    , counterexample "(a > b) = (b < a) VIOLATED" $
+        (a > b) === (b < a)
+    , counterexample "(a < b) == (compare a b == LT) VIOLATED" $
+        (a < b) === (compare a b == LT)
+    , counterexample "(a > b) == (compare a b == GT) VIOLATED" $
+        (a > b) === (compare a b == GT)
+    , counterexample "(a == b) == (compare a b == EQ) VIOLATED" $
+        (a == b) === (compare a b == EQ)
+    , counterexample "min a b == if a <= b then a else b VIOLATED" $
+        min 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
+    ]