{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

#if !MIN_VERSION_QuickCheck(2,16,0)
{-# OPTIONS_GHC -Wno-dodgy-imports #-}
#endif

module Test.Ouroboros.Storage.PerasCertDB.StateMachine (tests) where

import Control.Monad.State
import Control.Tracer (nullTracer)
import Data.Function ((&))
import qualified Data.List.NonEmpty as NE
import qualified Data.Set as Set
import Ouroboros.Consensus.Block
import Ouroboros.Consensus.Peras.Weight (PerasWeightSnapshot)
import qualified Ouroboros.Consensus.Storage.PerasCertDB as PerasCertDB
import Ouroboros.Consensus.Storage.PerasCertDB.API (AddPerasCertResult (..), PerasCertDB)
import Ouroboros.Consensus.Util.IOLike
import Ouroboros.Consensus.Util.STM
import qualified Test.Ouroboros.Storage.PerasCertDB.Model as Model
import Test.QuickCheck hiding (Some (..))
import qualified Test.QuickCheck.Monadic as QC
import Test.QuickCheck.StateModel
import Test.Tasty
import Test.Tasty.QuickCheck hiding (Some (..))
import Test.Util.TestBlock (TestBlock, TestHash (..))
import Test.Util.TestEnv (adjustQuickCheckTests)

tests :: TestTree
tests :: TestTree
tests =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"PerasCertDB"
    [ (Int -> Int) -> TestTree -> TestTree
adjustQuickCheckTests (Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
100) (TestTree -> TestTree) -> TestTree -> TestTree
forall a b. (a -> b) -> a -> b
$ TestName -> (Actions Model -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"q-d" ((Actions Model -> Property) -> TestTree)
-> (Actions Model -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$ Actions Model -> Property
prop_qd
    ]

prop_qd :: Actions Model -> Property
prop_qd :: Actions Model -> Property
prop_qd Actions Model
actions = (StateT (PerasCertDB IO TestBlock) IO Property -> Property)
-> PropertyM (StateT (PerasCertDB IO TestBlock) IO) Property
-> Property
forall a (m :: * -> *).
(Testable a, Monad m) =>
(m Property -> Property) -> PropertyM m a -> Property
QC.monadic StateT (PerasCertDB IO TestBlock) IO Property -> Property
f (PropertyM (StateT (PerasCertDB IO TestBlock) IO) Property
 -> Property)
-> PropertyM (StateT (PerasCertDB IO TestBlock) IO) Property
-> Property
forall a b. (a -> b) -> a -> b
$ () -> Property
forall prop. Testable prop => prop -> Property
property () Property
-> PropertyM
     (StateT (PerasCertDB IO TestBlock) IO) (Annotated Model, Env)
-> PropertyM (StateT (PerasCertDB IO TestBlock) IO) Property
forall a b.
a
-> PropertyM (StateT (PerasCertDB IO TestBlock) IO) b
-> PropertyM (StateT (PerasCertDB IO TestBlock) IO) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Actions Model
-> PropertyM
     (StateT (PerasCertDB IO TestBlock) IO) (Annotated Model, Env)
forall state (m :: * -> *) e.
(StateModel state, RunModel state m, e ~ Error state m,
 forall a. IsPerformResult e a) =>
Actions state -> PropertyM m (Annotated state, Env)
runActions Actions Model
actions
 where
  f :: StateT (PerasCertDB IO TestBlock) IO Property -> Property
  f :: StateT (PerasCertDB IO TestBlock) IO Property -> Property
f = IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty (IO Property -> Property)
-> (StateT (PerasCertDB IO TestBlock) IO Property -> IO Property)
-> StateT (PerasCertDB IO TestBlock) IO Property
-> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StateT (PerasCertDB IO TestBlock) IO Property
 -> PerasCertDB IO TestBlock -> IO Property)
-> PerasCertDB IO TestBlock
-> StateT (PerasCertDB IO TestBlock) IO Property
-> IO Property
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (PerasCertDB IO TestBlock) IO Property
-> PerasCertDB IO TestBlock -> IO Property
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (TestName -> PerasCertDB IO TestBlock
forall a. HasCallStack => TestName -> a
error TestName
"unreachable")

newtype Model = Model (Model.Model TestBlock) deriving (Int -> Model -> ShowS
[Model] -> ShowS
Model -> TestName
(Int -> Model -> ShowS)
-> (Model -> TestName) -> ([Model] -> ShowS) -> Show Model
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Model -> ShowS
showsPrec :: Int -> Model -> ShowS
$cshow :: Model -> TestName
show :: Model -> TestName
$cshowList :: [Model] -> ShowS
showList :: [Model] -> ShowS
Show, (forall x. Model -> Rep Model x)
-> (forall x. Rep Model x -> Model) -> Generic Model
forall x. Rep Model x -> Model
forall x. Model -> Rep Model x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Model -> Rep Model x
from :: forall x. Model -> Rep Model x
$cto :: forall x. Rep Model x -> Model
to :: forall x. Rep Model x -> Model
Generic)

instance StateModel Model where
  data Action Model a where
    OpenDB :: Action Model ()
    CloseDB :: Action Model ()
    AddCert :: ValidatedPerasCert TestBlock -> Action Model AddPerasCertResult
    GetWeightSnapshot :: Action Model (PerasWeightSnapshot TestBlock)
    GarbageCollect :: SlotNo -> Action Model ()

  arbitraryAction :: VarContext -> Model -> Gen (Any (Action Model))
arbitraryAction VarContext
_ (Model Model TestBlock
model)
    | Model TestBlock
model.open =
        [(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model))
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
          [ (Int
1, Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> Any (Action Model) -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Action Model ()
CloseDB)
          , (Int
20, Action Model AddPerasCertResult -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model AddPerasCertResult -> Any (Action Model))
-> Gen (Action Model AddPerasCertResult)
-> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Action Model AddPerasCertResult)
genAddCert)
          , (Int
20, Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> Any (Action Model) -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action Model (PerasWeightSnapshot TestBlock) -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Action Model (PerasWeightSnapshot TestBlock)
GetWeightSnapshot)
          , (Int
5, Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model () -> Any (Action Model))
-> (Word64 -> Action Model ()) -> Word64 -> Any (Action Model)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SlotNo -> Action Model ()
GarbageCollect (SlotNo -> Action Model ())
-> (Word64 -> SlotNo) -> Word64 -> Action Model ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> SlotNo
SlotNo (Word64 -> Any (Action Model))
-> Gen Word64 -> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Word64
forall a. Arbitrary a => Gen a
arbitrary)
          ]
    | Bool
otherwise = Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> Any (Action Model) -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Action Model ()
OpenDB
   where
    genAddCert :: Gen (Action Model AddPerasCertResult)
genAddCert = do
      roundNo <- Gen PerasRoundNo
genRoundNo
      boostedBlock <- genPoint
      pure $
        AddCert
          ValidatedPerasCert
            { vpcCert =
                PerasCert
                  { pcCertRound = roundNo
                  , pcCertBoostedBlock = boostedBlock
                  }
            , vpcCertBoost = boostPerCert
            }

    -- Generators are heavily skewed toward collisions, to get equivocating certificates
    -- and certificates boosting the same block
    genPoint :: Gen (Point TestBlock)
    genPoint :: Gen (Point TestBlock)
genPoint =
      [Gen (Point TestBlock)] -> Gen (Point TestBlock)
forall a. HasCallStack => [Gen a] -> Gen a
oneof
        [ Point TestBlock -> Gen (Point TestBlock)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return Point TestBlock
forall {k} (block :: k). Point block
GenesisPoint
        , SlotNo -> HeaderHash TestBlock -> Point TestBlock
SlotNo -> TestHash -> Point TestBlock
forall {k} (block :: k). SlotNo -> HeaderHash block -> Point block
BlockPoint (SlotNo -> TestHash -> Point TestBlock)
-> Gen SlotNo -> Gen (TestHash -> Point TestBlock)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Word64 -> SlotNo
SlotNo (Word64 -> SlotNo) -> Gen Word64 -> Gen SlotNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Word64
forall a. Arbitrary a => Gen a
arbitrary) Gen (TestHash -> Point TestBlock)
-> Gen TestHash -> Gen (Point TestBlock)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen TestHash
genHash
        ]
    genRoundNo :: Gen (PerasRoundNo)
    genRoundNo :: Gen PerasRoundNo
genRoundNo =
      [(Int, Gen PerasRoundNo)] -> Gen PerasRoundNo
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
        [ (Int
1, PerasRoundNo -> Gen PerasRoundNo
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PerasRoundNo -> Gen PerasRoundNo)
-> PerasRoundNo -> Gen PerasRoundNo
forall a b. (a -> b) -> a -> b
$ Word64 -> PerasRoundNo
PerasRoundNo Word64
1)
        , (Int
1, PerasRoundNo -> Gen PerasRoundNo
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PerasRoundNo -> Gen PerasRoundNo)
-> PerasRoundNo -> Gen PerasRoundNo
forall a b. (a -> b) -> a -> b
$ Word64 -> PerasRoundNo
PerasRoundNo Word64
2)
        , (Int
8, Word64 -> PerasRoundNo
PerasRoundNo (Word64 -> PerasRoundNo) -> Gen Word64 -> Gen PerasRoundNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Word64
forall a. Arbitrary a => Gen a
arbitrary)
        ]
    genHash :: Gen TestHash
genHash = NonEmpty Word64 -> TestHash
TestHash (NonEmpty Word64 -> TestHash)
-> (NonEmptyList Word64 -> NonEmpty Word64)
-> NonEmptyList Word64
-> TestHash
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word64] -> NonEmpty Word64
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList ([Word64] -> NonEmpty Word64)
-> (NonEmptyList Word64 -> [Word64])
-> NonEmptyList Word64
-> NonEmpty Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyList Word64 -> [Word64]
forall a. NonEmptyList a -> [a]
getNonEmpty (NonEmptyList Word64 -> TestHash)
-> Gen (NonEmptyList Word64) -> Gen TestHash
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (NonEmptyList Word64)
forall a. Arbitrary a => Gen a
arbitrary

  initialState :: Model
initialState = Model TestBlock -> Model
Model Model TestBlock
forall blk. Model blk
Model.initModel

  nextState :: forall a. Typeable a => Model -> Action Model a -> Var a -> Model
nextState (Model Model TestBlock
model) Action Model a
action Var a
_ = Model TestBlock -> Model
Model (Model TestBlock -> Model) -> Model TestBlock -> Model
forall a b. (a -> b) -> a -> b
$ case Action Model a
action of
    Action Model a
R:ActionModela a
OpenDB -> Model TestBlock -> Model TestBlock
forall blk. Model blk -> Model blk
Model.openDB Model TestBlock
model
    Action Model a
R:ActionModela a
CloseDB -> Model TestBlock -> Model TestBlock
forall blk. Model blk -> Model blk
Model.closeDB Model TestBlock
model
    AddCert ValidatedPerasCert TestBlock
cert -> Model TestBlock -> ValidatedPerasCert TestBlock -> Model TestBlock
forall blk.
StandardHash blk =>
Model blk -> ValidatedPerasCert blk -> Model blk
Model.addCert Model TestBlock
model ValidatedPerasCert TestBlock
cert
    Action Model a
R:ActionModela a
GetWeightSnapshot -> Model TestBlock
model
    GarbageCollect SlotNo
slot -> SlotNo -> Model TestBlock -> Model TestBlock
forall blk. StandardHash blk => SlotNo -> Model blk -> Model blk
Model.garbageCollect SlotNo
slot Model TestBlock
model

  precondition :: forall a. Model -> Action Model a -> Bool
precondition (Model Model TestBlock
model) = \case
    Action Model a
R:ActionModela a
OpenDB -> Bool -> Bool
not Model TestBlock
model.open
    Action Model a
_ -> Model TestBlock
model.open

deriving stock instance Show (Action Model a)
deriving stock instance Eq (Action Model a)

instance HasVariables (Action Model a) where
  getAllVariables :: Action Model a -> Set (Any Var)
getAllVariables Action Model a
_ = Set (Any Var)
forall a. Monoid a => a
mempty

instance RunModel Model (StateT (PerasCertDB IO TestBlock) IO) where
  perform :: forall a.
Typeable a =>
Model
-> Action Model a
-> LookUp
-> StateT
     (PerasCertDB IO TestBlock)
     IO
     (PerformResult Model (StateT (PerasCertDB IO TestBlock) IO) a)
perform Model
_ Action Model a
action LookUp
_ = case Action Model a
action of
    Action Model a
R:ActionModela a
OpenDB -> do
      perasCertDB <- IO (PerasCertDB IO TestBlock)
-> StateT (PerasCertDB IO TestBlock) IO (PerasCertDB IO TestBlock)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (PerasCertDB IO TestBlock) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (PerasCertDB IO TestBlock)
 -> StateT (PerasCertDB IO TestBlock) IO (PerasCertDB IO TestBlock))
-> IO (PerasCertDB IO TestBlock)
-> StateT (PerasCertDB IO TestBlock) IO (PerasCertDB IO TestBlock)
forall a b. (a -> b) -> a -> b
$ Complete PerasCertDbArgs IO TestBlock
-> IO (PerasCertDB IO TestBlock)
forall (m :: * -> *) blk.
(IOLike m, StandardHash blk) =>
Complete PerasCertDbArgs m blk -> m (PerasCertDB m blk)
PerasCertDB.openDB (Tracer IO (TraceEvent TestBlock)
-> Complete PerasCertDbArgs IO TestBlock
forall (f :: * -> *) (m :: * -> *) blk.
Tracer m (TraceEvent blk) -> PerasCertDbArgs f m blk
PerasCertDB.PerasCertDbArgs Tracer IO (TraceEvent TestBlock)
forall (m :: * -> *) a. Applicative m => Tracer m a
nullTracer)
      put perasCertDB
    Action Model a
R:ActionModela a
CloseDB -> do
      perasCertDB <- StateT (PerasCertDB IO TestBlock) IO (PerasCertDB IO TestBlock)
forall s (m :: * -> *). MonadState s m => m s
get
      lift $ PerasCertDB.closeDB perasCertDB
    AddCert ValidatedPerasCert TestBlock
cert -> do
      perasCertDB <- StateT (PerasCertDB IO TestBlock) IO (PerasCertDB IO TestBlock)
forall s (m :: * -> *). MonadState s m => m s
get
      lift $ PerasCertDB.addCert perasCertDB cert
    Action Model a
R:ActionModela a
GetWeightSnapshot -> do
      perasCertDB <- StateT (PerasCertDB IO TestBlock) IO (PerasCertDB IO TestBlock)
forall s (m :: * -> *). MonadState s m => m s
get
      lift $ atomically $ forgetFingerprint <$> PerasCertDB.getWeightSnapshot perasCertDB
    GarbageCollect SlotNo
slot -> do
      perasCertDB <- StateT (PerasCertDB IO TestBlock) IO (PerasCertDB IO TestBlock)
forall s (m :: * -> *). MonadState s m => m s
get
      lift $ PerasCertDB.garbageCollect perasCertDB slot

  postcondition :: forall a.
(Model, Model)
-> Action Model a
-> LookUp
-> a
-> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) Bool
postcondition (Model Model TestBlock
model, Model
_) (AddCert ValidatedPerasCert TestBlock
cert) LookUp
_ a
actual = do
    let expected :: AddPerasCertResult
expected
          | Model TestBlock
model.certs Set (ValidatedPerasCert TestBlock)
-> ValidatedPerasCert TestBlock -> Bool
forall blk.
StandardHash blk =>
Set (ValidatedPerasCert blk) -> ValidatedPerasCert blk -> Bool
`Model.hasRoundNo` ValidatedPerasCert TestBlock
cert = AddPerasCertResult
PerasCertAlreadyInDB
          | Bool
otherwise = AddPerasCertResult
AddedPerasCertToDB
    TestName
-> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ AddPerasCertResult -> TestName
forall a. Show a => a -> TestName
show AddPerasCertResult
expected TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> TestName
" /= " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> a -> TestName
forall a. Show a => a -> TestName
show a
actual
    Bool -> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
 -> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) Bool)
-> Bool
-> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) Bool
forall a b. (a -> b) -> a -> b
$ AddPerasCertResult
expected AddPerasCertResult -> AddPerasCertResult -> Bool
forall a. Eq a => a -> a -> Bool
== a
AddPerasCertResult
actual
  postcondition (Model Model TestBlock
model, Model
_) Action Model a
R:ActionModela a
GetWeightSnapshot LookUp
_ a
actual = do
    let expected :: PerasWeightSnapshot TestBlock
expected = Model TestBlock -> PerasWeightSnapshot TestBlock
forall blk.
StandardHash blk =>
Model blk -> PerasWeightSnapshot blk
Model.getWeightSnapshot Model TestBlock
model
    TestName
-> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Model: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasWeightSnapshot TestBlock -> TestName
forall a. Show a => a -> TestName
show PerasWeightSnapshot TestBlock
expected
    TestName
-> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"SUT: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> a -> TestName
forall a. Show a => a -> TestName
show a
actual
    Bool -> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
 -> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) Bool)
-> Bool
-> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) Bool
forall a b. (a -> b) -> a -> b
$ PerasWeightSnapshot TestBlock
expected PerasWeightSnapshot TestBlock
-> PerasWeightSnapshot TestBlock -> Bool
forall a. Eq a => a -> a -> Bool
== a
PerasWeightSnapshot TestBlock
actual
  postcondition (Model, Model)
_ Action Model a
_ LookUp
_ a
_ = Bool -> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasCertDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True

  monitoring :: forall a.
(Model, Model)
-> Action Model a
-> LookUp
-> Either (Error Model (StateT (PerasCertDB IO TestBlock) IO)) a
-> Property
-> Property
monitoring (Model Model TestBlock
model, Model
_) (AddCert ValidatedPerasCert TestBlock
cert) LookUp
_ Either (Error Model (StateT (PerasCertDB IO TestBlock) IO)) a
_ Property
prop =
    Property
prop
      Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& TestName -> [TestName] -> Property -> Property
forall prop.
Testable prop =>
TestName -> [TestName] -> prop -> Property
tabulate
        TestName
"Certificate round collision"
        [Bool -> TestName
forall a. Show a => a -> TestName
show (Bool -> TestName) -> Bool -> TestName
forall a b. (a -> b) -> a -> b
$ Model TestBlock
model.certs Set (ValidatedPerasCert TestBlock)
-> ValidatedPerasCert TestBlock -> Bool
forall blk.
StandardHash blk =>
Set (ValidatedPerasCert blk) -> ValidatedPerasCert blk -> Bool
`Model.hasRoundNo` ValidatedPerasCert TestBlock
cert]
      Property -> (Property -> Property) -> Property
forall a b. a -> (a -> b) -> b
& TestName -> [TestName] -> Property -> Property
forall prop.
Testable prop =>
TestName -> [TestName] -> prop -> Property
tabulate
        TestName
"Certificate block collision"
        [ Bool -> TestName
forall a. Show a => a -> TestName
show (Bool -> TestName) -> Bool -> TestName
forall a b. (a -> b) -> a -> b
$
            Point TestBlock -> Set (Point TestBlock) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member
              (ValidatedPerasCert TestBlock -> Point TestBlock
forall (cert :: * -> *) blk.
HasPerasCert cert blk =>
cert blk -> Point blk
getPerasCertBoostedBlock ValidatedPerasCert TestBlock
cert)
              ((ValidatedPerasCert TestBlock -> Point TestBlock)
-> Set (ValidatedPerasCert TestBlock) -> Set (Point TestBlock)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ValidatedPerasCert TestBlock -> Point TestBlock
forall (cert :: * -> *) blk.
HasPerasCert cert blk =>
cert blk -> Point blk
getPerasCertBoostedBlock Model TestBlock
model.certs)
        ]
  monitoring (Model, Model)
_ Action Model a
_ LookUp
_ Either (Error Model (StateT (PerasCertDB IO TestBlock) IO)) a
_ Property
prop = Property
prop