Generate security parameter for ChainDB q-s-m test on the fly

After analysing the effect of varying the security parameter (`k`) of
the ChainDB state machine tests (currently hardcoded with 2), we have
observed a tension between:

1) generating enough tests exercising the new Peras behavior where the
   chain selection mechanism switches to a shorter but heavier chain
   (cert boost is derived from k and must be large enough to overcome
   the weight of a longer chain), and

2) generating enough tests exercising the ImmutableDB logic (the chain
   must have at least k blocks)

Here are some empirical results:

k   -> P(switch to shorter chain), P(generate a chain with >= k blocks)
k=2 -> ~1.3%, ~40%
k=3 -> ~1.9%, ~20%
k=4 -> ~2.4%, ~9%
k=5 -> ~2.5%, ~3%
k=10 -> ~3%,  ~0.05%

We believe that the sweet spot between both desiderata appears to be
around `k=2` and `k=4`.

This commit introduces a random generator for `k` using a geometric
distribution to bias the randomly generated `k`s to be relatively small,
while still allowing larger ones to appear from time to time.

Under the current parameters, roughly 87.5% of the tests use `k<=4`;

```
Security Parameter (k) (10000 in total):
  50.82% 2
  23.83% 3
  12.62% 4
   6.69% 5
   3.08% 6
   1.54% 7
   0.74% 8
   0.37% 9
   0.16% 10
   0.06% 11
   0.05% 12
   0.02% 13
   0.01% 14
   0.01% 17
```

Yielding the following distributions for 1) and 2), respectively:

```
Tags (5161 in total):
  39.35% TagGetIsValidJust
  29.22% TagChainSelReprocessKeptSelection
  25.91% TagGetIsValidNothing
   3.88% TagChainSelReprocessChangedSelection
   1.65% TagSwitchedToShorterChain  <- HERE
```

```
Chain length >= k (10000 in total):
  73.25% False
  26.75% True  <- HERE
```

Author: agustinmista

ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/ChainDB/StateMachine.hs

@@ -73,7 +73,7 @@ module Test.Ouroboros.Storage.ChainDB.StateMachine
   , tests
   ) where
 
-import Cardano.Ledger.BaseTypes (NonZero (..), knownNonZeroBounded)
+import Cardano.Ledger.BaseTypes (NonZero (..), unsafeNonZero)
 import Codec.Serialise (Serialise)
 import Control.Monad (replicateM, void)
 import Control.ResourceRegistry
@@ -151,6 +151,7 @@ import qualified Test.Ouroboros.Storage.ChainDB.Model as Model
 import Test.Ouroboros.Storage.Orphans ()
 import Test.Ouroboros.Storage.TestBlock
 import Test.QuickCheck hiding (forAll)
+import qualified Test.QuickCheck as QC
 import qualified Test.QuickCheck.Monadic as QC
 import Test.StateMachine
 import qualified Test.StateMachine.Labelling as C
@@ -1720,56 +1721,75 @@ genBlk chunkInfo Model{..} =
         )
       ]
 
+genSecurityParam :: Gen SecurityParam
+genSecurityParam =
+  SecurityParam
+    . unsafeNonZero
+    . fromIntegral
+    . (+ 2) -- shift to the right to avoid degenerate cases
+    <$> geometric 0.5 -- range in [0, +inf); mean = 1/p = 2
+ where
+  geometric :: Double -> Gen Int
+  geometric p
+    | p <= 0 || p > 1 = error "p must be in (0,1]"
+    | otherwise = do
+        u <- choose (0.0, 1.0)
+        let k = floor (log u / log (1 - p))
+        return k
+
 {-------------------------------------------------------------------------------
   Top-level tests
 -------------------------------------------------------------------------------}
 
-mkTestCfg :: ImmutableDB.ChunkInfo -> TopLevelConfig TestBlock
-mkTestCfg (ImmutableDB.UniformChunkSize chunkSize) =
-  mkTestConfig (SecurityParam $ knownNonZeroBounded @2) chunkSize
+mkTestCfg :: SecurityParam -> ImmutableDB.ChunkInfo -> TopLevelConfig TestBlock
+mkTestCfg k (ImmutableDB.UniformChunkSize chunkSize) =
+  mkTestConfig k chunkSize
 
 envUnused :: ChainDBEnv m blk
 envUnused = error "ChainDBEnv used during command generation"
 
 smUnused ::
   LoE () ->
+  SecurityParam ->
   ImmutableDB.ChunkInfo ->
   StateMachine (Model Blk IO) (At Cmd Blk IO) IO (At Resp Blk IO)
-smUnused loe chunkInfo =
+smUnused loe k chunkInfo =
   sm
     loe
     envUnused
     (genBlk chunkInfo)
-    (mkTestCfg chunkInfo)
+    (mkTestCfg k chunkInfo)
     testInitExtLedger
 
 prop_sequential :: LoE () -> SmallChunkInfo -> Property
 prop_sequential loe smallChunkInfo@(SmallChunkInfo chunkInfo) =
-  forAllCommands (smUnused loe chunkInfo) Nothing $
-    runCmdsLockstep loe smallChunkInfo
+  QC.forAll genSecurityParam $ \k ->
+    forAllCommands (smUnused loe k chunkInfo) Nothing $
+      runCmdsLockstep loe k smallChunkInfo
 
 runCmdsLockstep ::
   LoE () ->
+  SecurityParam ->
   SmallChunkInfo ->
   QSM.Commands (At Cmd Blk IO) (At Resp Blk IO) ->
   Property
-runCmdsLockstep loe (SmallChunkInfo chunkInfo) cmds =
+runCmdsLockstep loe k (SmallChunkInfo chunkInfo) cmds =
   QC.monadicIO $ do
     let
       -- Current test case command names.
       ctcCmdNames :: [String]
       ctcCmdNames = fmap (show . cmdName . QSM.getCommand) $ QSM.unCommands cmds
 
     (hist, prop) <- QC.run $ test cmds
-    prettyCommands (smUnused loe chunkInfo) hist
+    prettyCommands (smUnused loe k chunkInfo) hist
       $ tabulate
         "Tags"
-        (map show $ tag (execCmds (QSM.initModel (smUnused loe chunkInfo)) cmds))
+        (map show $ tag (execCmds (QSM.initModel (smUnused loe k chunkInfo)) cmds))
       $ tabulate "Command sequence length" [show $ length ctcCmdNames]
       $ tabulate "Commands" ctcCmdNames
       $ prop
  where
-  testCfg = mkTestCfg chunkInfo
+  testCfg = mkTestCfg k chunkInfo
 
   test ::
     QSM.Commands (At Cmd Blk IO) (At Resp Blk IO) ->
@@ -1832,26 +1852,30 @@ runCmdsLockstep loe (SmallChunkInfo chunkInfo) cmds =
     fses <- atomically $ traverse readTMVar nodeDBs
     let
       modelChain = Model.currentChain $ dbModel model
+      secParam = unNonZero (maxRollbacks (configSecurityParam testCfg))
       prop =
         counterexample (show (configSecurityParam testCfg)) $
           counterexample ("Model chain: " <> condense modelChain) $
             counterexample ("TraceEvents: " <> unlines (map show trace)) $
               tabulate "Chain length" [show (Chain.length modelChain)] $
-                tabulate "TraceEvents" (map traceEventName trace) $
-                  res === Ok
-                    .&&. prop_trace testCfg (dbModel model) trace
-                    .&&. counterexample
-                      "ImmutableDB is leaking file handles"
-                      (Mock.numOpenHandles (nodeDBsImm fses) === 0)
-                    .&&. counterexample
-                      "VolatileDB is leaking file handles"
-                      (Mock.numOpenHandles (nodeDBsVol fses) === 0)
-                    .&&. counterexample
-                      "LedgerDB is leaking file handles"
-                      (Mock.numOpenHandles (nodeDBsLgr fses) === 0)
-                    .&&. counterexample
-                      "There were registered clean-up actions"
-                      (remainingCleanups === 0)
+                tabulate "Security Parameter (k)" [show secParam] $
+                  tabulate "Chain length >= k" [show (Chain.length modelChain >= fromIntegral secParam)] $
+                    tabulate "TraceEvents" (map traceEventName trace) $
+                      res
+                        === Ok
+                        .&&. prop_trace testCfg (dbModel model) trace
+                        .&&. counterexample
+                          "ImmutableDB is leaking file handles"
+                          (Mock.numOpenHandles (nodeDBsImm fses) === 0)
+                        .&&. counterexample
+                          "VolatileDB is leaking file handles"
+                          (Mock.numOpenHandles (nodeDBsVol fses) === 0)
+                        .&&. counterexample
+                          "LedgerDB is leaking file handles"
+                          (Mock.numOpenHandles (nodeDBsLgr fses) === 0)
+                        .&&. counterexample
+                          "There were registered clean-up actions"
+                          (remainingCleanups === 0)
     return (hist, prop)
 
 prop_trace :: TopLevelConfig Blk -> DBModel Blk -> [TraceEvent Blk] -> Property

ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/ChainDB/StateMachine/Utils/RunOnRepl.hs

@@ -87,6 +87,7 @@ import Ouroboros.Consensus.Block
   , EpochNo (EpochNo)
   , SlotNo (SlotNo)
   )
+import Ouroboros.Consensus.Config (SecurityParam)
 import Ouroboros.Consensus.Storage.ChainDB
   ( ChainType (TentativeChain)
   , LoE
@@ -142,8 +143,9 @@ pattern Command cmd rsp xs =
 
 quickCheckCmdsLockStep ::
   LoE () ->
+  SecurityParam ->
   SmallChunkInfo ->
   Commands (StateMachine.At Cmd TestBlock IO) (StateMachine.At Resp TestBlock IO) ->
   IO ()
-quickCheckCmdsLockStep loe chunkInfo cmds =
-  quickCheck $ runCmdsLockstep loe chunkInfo cmds
+quickCheckCmdsLockStep loe k chunkInfo cmds =
+  quickCheck $ runCmdsLockstep loe k chunkInfo cmds

ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/ChainDB/Unit.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -7,12 +8,14 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module Test.Ouroboros.Storage.ChainDB.Unit (tests) where
 
+import Cardano.Ledger.BaseTypes (knownNonZeroBounded)
 import Cardano.Slotting.Slot (WithOrigin (..))
 import Control.Monad (replicateM, unless, void)
 import Control.Monad.Except
@@ -35,6 +38,7 @@ import Ouroboros.Consensus.Config
   ( TopLevelConfig
   , configSecurityParam
   )
+import Ouroboros.Consensus.Config.SecurityParam (SecurityParam (..))
 import Ouroboros.Consensus.Ledger.Basics
 import Ouroboros.Consensus.Ledger.Extended (ExtLedgerState)
 import Ouroboros.Consensus.Ledger.SupportsProtocol
@@ -243,16 +247,18 @@ runModelIO :: API.LoE () -> ModelM TestBlock a -> IO ()
 runModelIO loe expr = toAssertion (runModel newModel topLevelConfig expr)
  where
   chunkInfo = ImmutableDB.simpleChunkInfo 100
+  k = SecurityParam (knownNonZeroBounded @2)
   newModel = Model.empty loe testInitExtLedger
-  topLevelConfig = mkTestCfg chunkInfo
+  topLevelConfig = mkTestCfg k chunkInfo
 
 -- | Helper function to run the test against the actual chain database and
 -- translate to something that HUnit likes.
 runSystemIO :: SystemM TestBlock IO a -> IO ()
 runSystemIO expr = runSystem withChainDbEnv expr >>= toAssertion
  where
   chunkInfo = ImmutableDB.simpleChunkInfo 100
-  topLevelConfig = mkTestCfg chunkInfo
+  k = SecurityParam (knownNonZeroBounded @2)
+  topLevelConfig = mkTestCfg k chunkInfo
   withChainDbEnv = withTestChainDbEnv topLevelConfig chunkInfo $ convertMapKind testInitExtLedger
 
 newtype TestFailure = TestFailure String deriving Show