{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

module Test.Ouroboros.Storage.PerasVoteDB.StateMachine
  ( tests

    -- * Reusable generators
  , genVoterId
  , genVoteStake
  ) where

import qualified Cardano.Crypto.DSIGN.Class as SL
import qualified Cardano.Crypto.Seed as SL
import qualified Cardano.Ledger.Keys as SL
import Control.Concurrent.Class.MonadSTM (MonadSTM (..))
import Control.Monad (join)
import Control.Monad.Class.MonadThrow (MonadCatch (..))
import Control.Monad.State
  ( MonadState (..)
  , MonadTrans (..)
  , StateT
  , evalStateT
  )
import Control.Tracer (nullTracer)
import Data.Char (chr)
import Data.Functor (($>))
import qualified Data.List.NonEmpty as NE
import qualified Data.Map as Map
import Data.Map.Strict (Map)
import Data.Ratio ((%))
import Data.Set (Set)
import qualified Data.Set as Set
import Data.String (IsString (..))
import Data.Word (Word64)
import GHC.Generics (Generic)
import Ouroboros.Consensus.Block.Abstract (Point (..), SlotNo (..))
import Ouroboros.Consensus.Block.SupportsPeras
  ( BlockSupportsPeras (..)
  , HasPerasVoteBlock (..)
  , HasPerasVoteRound (..)
  , PerasRoundNo (..)
  , PerasVote (..)
  , PerasVoteId
  , PerasVoteStake (..)
  , PerasVoteTarget (..)
  , PerasVoterId (..)
  , ValidatedPerasCert
  , ValidatedPerasVote (..)
  , mkPerasParams
  )
import Ouroboros.Consensus.BlockchainTime.WallClock.Types
  ( RelativeTime (..)
  , WithArrivalTime (..)
  )
import Ouroboros.Consensus.Storage.PerasVoteDB
  ( AddPerasVoteResult (..)
  , PerasVoteDB
  , PerasVoteDbError (..)
  , PerasVoteTicketNo
  )
import qualified Ouroboros.Consensus.Storage.PerasVoteDB as PerasVoteDB
import Ouroboros.Consensus.Util.Orphans ()
import Test.Cardano.Ledger.Binary.Arbitrary ()
import Test.Ouroboros.Storage.Orphans ()
import qualified Test.Ouroboros.Storage.PerasVoteDB.Model as Model
import Test.QuickCheck
  ( Arbitrary (..)
  , Gen
  , Property
  , choose
  , elements
  , frequency
  , ioProperty
  , tabulate
  )
import Test.QuickCheck.Monadic (PropertyM, monadic)
import Test.QuickCheck.StateModel
  ( Actions
  , Any (..)
  , HasVariables (..)
  , RunModel (..)
  , StateModel (..)
  , counterexamplePost
  , runActions
  )
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.QuickCheck (testProperty)
import Test.Util.TestBlock (TestBlock, TestHash (..))
import Test.Util.TestEnv (adjustQuickCheckMaxSize, adjustQuickCheckTests)

tests :: TestTree
tests :: TestTree
tests =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"PerasVoteDB"
    [ (Int -> Int) -> TestTree -> TestTree
adjustQuickCheckMaxSize (Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
5) (TestTree -> TestTree) -> TestTree -> TestTree
forall a b. (a -> b) -> a -> b
$
        (Int -> Int) -> TestTree -> TestTree
adjustQuickCheckTests (Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
10) (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
    ]

perasTestCfg :: PerasCfg TestBlock
perasTestCfg :: PerasCfg TestBlock
perasTestCfg = PerasParams
PerasCfg TestBlock
mkPerasParams

prop_qd :: Actions Model -> Property
prop_qd :: Actions Model -> Property
prop_qd Actions Model
actions = (StateT (PerasVoteDB IO TestBlock) IO Property -> Property)
-> PropertyM (StateT (PerasVoteDB IO TestBlock) IO) () -> Property
forall a (m :: * -> *).
(Testable a, Monad m) =>
(m Property -> Property) -> PropertyM m a -> Property
monadic StateT (PerasVoteDB IO TestBlock) IO Property -> Property
runActualImplemMonad PropertyM (StateT (PerasVoteDB IO TestBlock) IO) ()
resultAsPropertyM
 where
  -- This runs actions on the model and the actual implementation alongside,
  -- and checks the postconditions after each action.
  -- The `PropertyM` wrapper is keeping track of success/failure of the
  -- postconditions, so we don't care about the payload returned by `runActions`.
  resultAsPropertyM :: PropertyM (StateT (PerasVoteDB IO TestBlock) IO) ()
  resultAsPropertyM :: PropertyM (StateT (PerasVoteDB IO TestBlock) IO) ()
resultAsPropertyM = Actions Model
-> PropertyM
     (StateT (PerasVoteDB 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 PropertyM
  (StateT (PerasVoteDB IO TestBlock) IO) (Annotated Model, Env)
-> () -> PropertyM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ()

  -- This function is in charge of collapsing/running the different monadic
  -- layers on top of our property.
  runActualImplemMonad :: StateT (PerasVoteDB IO TestBlock) IO Property -> Property
  runActualImplemMonad :: StateT (PerasVoteDB IO TestBlock) IO Property -> Property
runActualImplemMonad StateT (PerasVoteDB IO TestBlock) IO Property
statefulIoProp =
    -- The _Model_ starts in `Model.open = False`, so `precondition` dictates
    -- that the first action must be `CreateDB`, and this `CreateDB` action will
    -- initialize the `StateT` state with a valid `PerasVoteDB` instance.
    -- The actual implementation state can only be read in `postcondition`, so
    -- we are sure that the `StateT` state will be properly initialized beforehand.
    let ioProp :: IO Property
ioProp = StateT (PerasVoteDB IO TestBlock) IO Property
-> PerasVoteDB IO TestBlock -> IO Property
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT (PerasVoteDB IO TestBlock) IO Property
statefulIoProp (TestName -> PerasVoteDB IO TestBlock
forall a. HasCallStack => TestName -> a
error TestName
"Trying to access uninitialized PerasVoteDB")
     in IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty IO Property
ioProp

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
    CreateDB ::
      Action Model ()
    AddVote ::
      WithArrivalTime (ValidatedPerasVote TestBlock) ->
      Action
        Model
        ( Either
            (PerasVoteDbError TestBlock)
            (AddPerasVoteResult TestBlock)
        )
    GetVoteIds ::
      Action Model (Set (PerasVoteId TestBlock))
    GetVotesAfter ::
      PerasVoteTicketNo ->
      Action
        Model
        ( Map
            PerasVoteTicketNo
            (WithArrivalTime (ValidatedPerasVote TestBlock))
        )
    GetForgedCertForRound ::
      PerasRoundNo ->
      Action Model (Maybe (ValidatedPerasCert TestBlock))
    GarbageCollect ::
      SlotNo ->
      Action Model ()

  arbitraryAction :: VarContext -> Model -> Gen (Any (Action Model))
arbitraryAction VarContext
_ (Model Model TestBlock
m)
    | Bool -> Bool
not (Model TestBlock -> Bool
forall blk. Model blk -> Bool
Model.open Model TestBlock
m) =
        Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model () -> Any (Action Model))
-> Gen (Action Model ()) -> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Action Model ())
genCreateDB
    | Bool
otherwise =
        [(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model))
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
          [ (Int
1000, Action
  Model
  (Either
     (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock))
-> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action
   Model
   (Either
      (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock))
 -> Any (Action Model))
-> Gen
     (Action
        Model
        (Either
           (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)))
-> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen
  (Action
     Model
     (Either
        (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)))
genAddVote)
          , (Int
10, Action Model (Set (PerasVoteId TestBlock)) -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model (Set (PerasVoteId TestBlock)) -> Any (Action Model))
-> Gen (Action Model (Set (PerasVoteId TestBlock)))
-> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Action Model (Set (PerasVoteId TestBlock)))
genGetVoteIds)
          , (Int
10, Action
  Model
  (Map
     PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock)))
-> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action
   Model
   (Map
      PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock)))
 -> Any (Action Model))
-> Gen
     (Action
        Model
        (Map
           PerasVoteTicketNo
           (WithArrivalTime (ValidatedPerasVote TestBlock))))
-> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen
  (Action
     Model
     (Map
        PerasVoteTicketNo
        (WithArrivalTime (ValidatedPerasVote TestBlock))))
genGetVotesAfter)
          , (Int
5, Action Model (Maybe (ValidatedPerasCert TestBlock))
-> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model (Maybe (ValidatedPerasCert TestBlock))
 -> Any (Action Model))
-> Gen (Action Model (Maybe (ValidatedPerasCert TestBlock)))
-> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Action Model (Maybe (ValidatedPerasCert TestBlock)))
genGetForgedCertForRound)
          , (Int
2, Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model () -> Any (Action Model))
-> Gen (Action Model ()) -> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Action Model ())
genGarbageCollect)
          ]
   where
    genCreateDB :: Gen (Action Model ())
genCreateDB = do
      Action Model () -> Gen (Action Model ())
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Action Model ()
CreateDB

    genAddVote :: Gen
  (Action
     Model
     (Either
        (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)))
genAddVote = do
      roundNo <- Gen PerasRoundNo
genRoundNo
      point <- genPoint
      voterId <- genVoterId
      stake <- genVoteStake
      now <- genRelativeTime
      let voteWithTime =
            RelativeTime
-> ValidatedPerasVote TestBlock
-> WithArrivalTime (ValidatedPerasVote TestBlock)
forall a. RelativeTime -> a -> WithArrivalTime a
WithArrivalTime RelativeTime
now (ValidatedPerasVote TestBlock
 -> WithArrivalTime (ValidatedPerasVote TestBlock))
-> ValidatedPerasVote TestBlock
-> WithArrivalTime (ValidatedPerasVote TestBlock)
forall a b. (a -> b) -> a -> b
$
              ValidatedPerasVote
                { vpvVote :: PerasVote TestBlock
vpvVote =
                    PerasVote
                      { pvVoteRound :: PerasRoundNo
pvVoteRound = PerasRoundNo
roundNo
                      , pvVoteBlock :: Point TestBlock
pvVoteBlock = Point TestBlock
point
                      , pvVoteVoterId :: PerasVoterId
pvVoteVoterId = PerasVoterId
voterId
                      }
                , vpvVoteStake :: PerasVoteStake
vpvVoteStake = PerasVoteStake
stake
                }
      return (AddVote voteWithTime)

    genGetVoteIds :: Gen (Action Model (Set (PerasVoteId TestBlock)))
genGetVoteIds = do
      Action Model (Set (PerasVoteId TestBlock))
-> Gen (Action Model (Set (PerasVoteId TestBlock)))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Action Model (Set (PerasVoteId TestBlock))
GetVoteIds

    genGetVotesAfter :: Gen
  (Action
     Model
     (Map
        PerasVoteTicketNo
        (WithArrivalTime (ValidatedPerasVote TestBlock))))
genGetVotesAfter = do
      ticketNo <- Int -> PerasVoteTicketNo
forall a. Enum a => Int -> a
toEnum (Int -> PerasVoteTicketNo) -> Gen Int -> Gen PerasVoteTicketNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0, PerasVoteTicketNo -> Int
forall a. Enum a => a -> Int
fromEnum (Model TestBlock -> PerasVoteTicketNo
forall blk. Model blk -> PerasVoteTicketNo
Model.lastTicketNo Model TestBlock
m) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
      pure (GetVotesAfter ticketNo)

    genGetForgedCertForRound :: Gen (Action Model (Maybe (ValidatedPerasCert TestBlock)))
genGetForgedCertForRound = do
      roundNo <- Gen PerasRoundNo
genRoundNo
      pure (GetForgedCertForRound roundNo)

    genGarbageCollect :: Gen (Action Model ())
genGarbageCollect = do
      slotNo <- Word64 -> SlotNo
SlotNo (Word64 -> SlotNo) -> Gen Word64 -> Gen SlotNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose @Word64 (Word64
0, Word64
9)
      pure (GarbageCollect slotNo)

    genPoint :: Gen (Point TestBlock)
genPoint = do
      [(Int, Gen (Point TestBlock))] -> Gen (Point TestBlock)
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
        [
          ( Int
1
          , 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
          )
        ,
          ( Int
50
          , do
              slotNo <- Word64 -> SlotNo
SlotNo (Word64 -> SlotNo) -> Gen Word64 -> Gen SlotNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose @Word64 (Word64
0, Word64
9)
              hash <- TestHash <$> NE.fromList . pure <$> choose (0, 9)
              return (BlockPoint slotNo hash)
          )
        ]

    genRoundNo :: Gen PerasRoundNo
genRoundNo = do
      n <- forall a. Random a => (a, a) -> Gen a
choose @Word64 (Word64
0, Word64
9)
      pure (PerasRoundNo n)

    genRelativeTime :: Gen RelativeTime
genRelativeTime = do
      time <- Word64 -> NominalDiffTime
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64 -> NominalDiffTime) -> Gen Word64 -> Gen NominalDiffTime
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary @Word64
      pure (RelativeTime time)

  initialState :: Model
initialState =
    Model TestBlock -> Model
Model (PerasCfg TestBlock -> Model TestBlock
forall blk. PerasCfg blk -> Model blk
Model.initModel PerasCfg TestBlock
perasTestCfg)

  nextState :: forall a. Typeable a => Model -> Action Model a -> Var a -> Model
nextState (Model Model TestBlock
m) Action Model a
action Var a
_ =
    case Action Model a
action of
      Action Model a
R:ActionModela a
CreateDB -> Model TestBlock -> Model
Model (Model TestBlock -> Model) -> Model TestBlock -> Model
forall a b. (a -> b) -> a -> b
$ Model TestBlock -> Model TestBlock
forall blk. Model blk -> Model blk
Model.openDB Model TestBlock
m
      AddVote WithArrivalTime (ValidatedPerasVote TestBlock)
vote -> Model TestBlock -> Model
Model (Model TestBlock -> Model) -> Model TestBlock -> Model
forall a b. (a -> b) -> a -> b
$ (Either PerasVoteDbModelError (AddPerasVoteResult TestBlock),
 Model TestBlock)
-> Model TestBlock
forall a b. (a, b) -> b
snd ((Either PerasVoteDbModelError (AddPerasVoteResult TestBlock),
  Model TestBlock)
 -> Model TestBlock)
-> (Either PerasVoteDbModelError (AddPerasVoteResult TestBlock),
    Model TestBlock)
-> Model TestBlock
forall a b. (a -> b) -> a -> b
$ WithArrivalTime (ValidatedPerasVote TestBlock)
-> Model TestBlock
-> (Either PerasVoteDbModelError (AddPerasVoteResult TestBlock),
    Model TestBlock)
forall blk.
StandardHash blk =>
WithArrivalTime (ValidatedPerasVote blk)
-> Model blk
-> (Either PerasVoteDbModelError (AddPerasVoteResult blk),
    Model blk)
Model.addVote WithArrivalTime (ValidatedPerasVote TestBlock)
vote Model TestBlock
m
      Action Model a
R:ActionModela a
GetVoteIds -> Model TestBlock -> Model
Model (Model TestBlock -> Model) -> Model TestBlock -> Model
forall a b. (a -> b) -> a -> b
$ Model TestBlock
m
      GetVotesAfter PerasVoteTicketNo
_ -> Model TestBlock -> Model
Model (Model TestBlock -> Model) -> Model TestBlock -> Model
forall a b. (a -> b) -> a -> b
$ Model TestBlock
m
      GetForgedCertForRound PerasRoundNo
_ -> Model TestBlock -> Model
Model (Model TestBlock -> Model) -> Model TestBlock -> Model
forall a b. (a -> b) -> a -> b
$ Model TestBlock
m
      GarbageCollect SlotNo
slotNo -> Model TestBlock -> Model
Model (Model TestBlock -> Model) -> Model TestBlock -> Model
forall a b. (a -> b) -> a -> b
$ SlotNo -> Model TestBlock -> Model TestBlock
forall blk. SlotNo -> Model blk -> Model blk
Model.garbageCollect SlotNo
slotNo Model TestBlock
m

  precondition :: forall a. Model -> Action Model a -> Bool
precondition (Model Model TestBlock
m) Action Model a
action =
    case Action Model a
action of
      Action Model a
R:ActionModela a
CreateDB -> Bool -> Bool
not (Model TestBlock -> Bool
forall blk. Model blk -> Bool
Model.open Model TestBlock
m)
      AddVote WithArrivalTime (ValidatedPerasVote TestBlock)
_ -> Model TestBlock -> Bool
forall blk. Model blk -> Bool
Model.open Model TestBlock
m
      Action Model a
R:ActionModela a
GetVoteIds -> Model TestBlock -> Bool
forall blk. Model blk -> Bool
Model.open Model TestBlock
m
      GetVotesAfter PerasVoteTicketNo
_ -> Model TestBlock -> Bool
forall blk. Model blk -> Bool
Model.open Model TestBlock
m
      GetForgedCertForRound PerasRoundNo
_ -> Model TestBlock -> Bool
forall blk. Model blk -> Bool
Model.open Model TestBlock
m
      GarbageCollect SlotNo
_ -> Model TestBlock -> Bool
forall blk. Model blk -> Bool
Model.open Model TestBlock
m

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 (PerasVoteDB IO TestBlock) IO) where
  perform :: forall a.
Typeable a =>
Model
-> Action Model a
-> LookUp
-> StateT
     (PerasVoteDB IO TestBlock)
     IO
     (PerformResult Model (StateT (PerasVoteDB IO TestBlock) IO) a)
perform Model
_ Action Model a
action LookUp
_ =
    case Action Model a
action of
      Action Model a
R:ActionModela a
CreateDB -> do
        let args :: PerasVoteDbArgs Identity IO blk
args = Tracer IO (TraceEvent blk)
-> HKD Identity (PerasCfg blk) -> PerasVoteDbArgs Identity IO blk
forall (f :: * -> *) (m :: * -> *) blk.
Tracer m (TraceEvent blk)
-> HKD f (PerasCfg blk) -> PerasVoteDbArgs f m blk
PerasVoteDB.PerasVoteDbArgs Tracer IO (TraceEvent blk)
forall (m :: * -> *) a. Applicative m => Tracer m a
nullTracer HKD Identity (PerasCfg blk)
PerasCfg TestBlock
perasTestCfg
        voteDB <- IO (PerasVoteDB IO TestBlock)
-> StateT (PerasVoteDB IO TestBlock) IO (PerasVoteDB IO TestBlock)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (PerasVoteDB IO TestBlock) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (PerasVoteDB IO TestBlock)
 -> StateT (PerasVoteDB IO TestBlock) IO (PerasVoteDB IO TestBlock))
-> IO (PerasVoteDB IO TestBlock)
-> StateT (PerasVoteDB IO TestBlock) IO (PerasVoteDB IO TestBlock)
forall a b. (a -> b) -> a -> b
$ Complete PerasVoteDbArgs IO TestBlock
-> IO (PerasVoteDB IO TestBlock)
forall (m :: * -> *) blk.
(IOLike m, StandardHash blk, Typeable blk) =>
Complete PerasVoteDbArgs m blk -> m (PerasVoteDB m blk)
PerasVoteDB.createDB Complete PerasVoteDbArgs IO TestBlock
forall {blk}. PerasVoteDbArgs Identity IO blk
args
        put voteDB
      AddVote WithArrivalTime (ValidatedPerasVote TestBlock)
vote -> do
        voteDB <- StateT (PerasVoteDB IO TestBlock) IO (PerasVoteDB IO TestBlock)
forall s (m :: * -> *). MonadState s m => m s
get
        lift $ try $ join $ atomically $ PerasVoteDB.addVote voteDB vote
      Action Model a
R:ActionModela a
GetVoteIds -> do
        voteDB <- StateT (PerasVoteDB IO TestBlock) IO (PerasVoteDB IO TestBlock)
forall s (m :: * -> *). MonadState s m => m s
get
        lift $ atomically $ PerasVoteDB.getVoteIds voteDB
      GetVotesAfter PerasVoteTicketNo
ticketNo -> do
        voteDB <- StateT (PerasVoteDB IO TestBlock) IO (PerasVoteDB IO TestBlock)
forall s (m :: * -> *). MonadState s m => m s
get
        lift $ atomically $ PerasVoteDB.getVotesAfter voteDB ticketNo
      GetForgedCertForRound PerasRoundNo
roundNo -> do
        voteDB <- StateT (PerasVoteDB IO TestBlock) IO (PerasVoteDB IO TestBlock)
forall s (m :: * -> *). MonadState s m => m s
get
        lift $ atomically $ PerasVoteDB.getForgedCertForRound voteDB roundNo
      GarbageCollect SlotNo
slotNo -> do
        voteDB <- StateT (PerasVoteDB IO TestBlock) IO (PerasVoteDB IO TestBlock)
forall s (m :: * -> *). MonadState s m => m s
get
        lift $ join $ atomically $ PerasVoteDB.garbageCollect voteDB slotNo

  postcondition :: forall a.
(Model, Model)
-> Action Model a
-> LookUp
-> a
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
postcondition (Model Model TestBlock
model, Model
_) (AddVote WithArrivalTime (ValidatedPerasVote TestBlock)
vote) LookUp
_ a
actual = do
    let (Either PerasVoteDbModelError (AddPerasVoteResult TestBlock)
expected, Model TestBlock
_) = WithArrivalTime (ValidatedPerasVote TestBlock)
-> Model TestBlock
-> (Either PerasVoteDbModelError (AddPerasVoteResult TestBlock),
    Model TestBlock)
forall blk.
StandardHash blk =>
WithArrivalTime (ValidatedPerasVote blk)
-> Model blk
-> (Either PerasVoteDbModelError (AddPerasVoteResult blk),
    Model blk)
Model.addVote WithArrivalTime (ValidatedPerasVote TestBlock)
vote Model TestBlock
model
    case (Either PerasVoteDbModelError (AddPerasVoteResult TestBlock)
expected, a
actual) of
      (Right AddPerasVoteResult TestBlock
expectedRes, Right AddPerasVoteResult TestBlock
actualRes) -> do
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Mismatched success results:"
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Model: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> AddPerasVoteResult TestBlock -> TestName
forall a. Show a => a -> TestName
show AddPerasVoteResult TestBlock
expectedRes
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"SUT: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> AddPerasVoteResult TestBlock -> TestName
forall a. Show a => a -> TestName
show AddPerasVoteResult TestBlock
actualRes
        Bool -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool)
-> Bool
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a b. (a -> b) -> a -> b
$ AddPerasVoteResult TestBlock
expectedRes AddPerasVoteResult TestBlock
-> AddPerasVoteResult TestBlock -> Bool
forall a. Eq a => a -> a -> Bool
== AddPerasVoteResult TestBlock
actualRes
      (Left PerasVoteDbModelError
expectedErr, Left PerasVoteDbError TestBlock
actualErr) -> do
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Mismatched failure results:"
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Model: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasVoteDbModelError -> TestName
forall a. Show a => a -> TestName
show PerasVoteDbModelError
expectedErr
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"SUT: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasVoteDbError TestBlock -> TestName
forall a. Show a => a -> TestName
show PerasVoteDbError TestBlock
actualErr
        case (PerasVoteDbModelError
expectedErr, PerasVoteDbError TestBlock
actualErr) of
          ( Model.MultipleWinnersInRound PerasRoundNo
roundNo
            , MultipleWinnersInRound PerasRoundNo
roundNo' ExistingPerasRoundWinner TestBlock
_ BlockedPerasRoundWinner TestBlock
_
            ) ->
              Bool -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool)
-> Bool
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a b. (a -> b) -> a -> b
$ PerasRoundNo
roundNo PerasRoundNo -> PerasRoundNo -> Bool
forall a. Eq a => a -> a -> Bool
== PerasRoundNo
roundNo'
          (PerasVoteDbModelError, PerasVoteDbError TestBlock)
_ ->
            Bool -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
      (Right AddPerasVoteResult TestBlock
expectedRes, Left PerasVoteDbError TestBlock
actualErr) -> do
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Expected success, but got error"
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Model: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> AddPerasVoteResult TestBlock -> TestName
forall a. Show a => a -> TestName
show AddPerasVoteResult TestBlock
expectedRes
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"SUT: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasVoteDbError TestBlock -> TestName
forall a. Show a => a -> TestName
show PerasVoteDbError TestBlock
actualErr
        Bool -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
      (Left PerasVoteDbModelError
expectedErr, Right AddPerasVoteResult TestBlock
actualRes) -> do
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Expected error, but got success:"
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Model: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasVoteDbModelError -> TestName
forall a. Show a => a -> TestName
show PerasVoteDbModelError
expectedErr
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"SUT: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> AddPerasVoteResult TestBlock -> TestName
forall a. Show a => a -> TestName
show AddPerasVoteResult TestBlock
actualRes
        Bool -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
  postcondition (Model Model TestBlock
model, Model
_) (Action Model a
R:ActionModela a
GetVoteIds) LookUp
_ a
actual = do
    let expected :: Set (PerasVoteId TestBlock)
expected = Model TestBlock -> Set (PerasVoteId TestBlock)
forall blk. Model blk -> Set (PerasVoteId blk)
Model.getVoteIds Model TestBlock
model
    TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Mismatched result:"
    TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Model: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Set (PerasVoteId TestBlock) -> TestName
forall a. Show a => a -> TestName
show Set (PerasVoteId TestBlock)
expected
    TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB 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 (PerasVoteDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool)
-> Bool
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a b. (a -> b) -> a -> b
$ Set (PerasVoteId TestBlock)
expected Set (PerasVoteId TestBlock) -> Set (PerasVoteId TestBlock) -> Bool
forall a. Eq a => a -> a -> Bool
== a
Set (PerasVoteId TestBlock)
actual
  postcondition (Model Model TestBlock
model, Model
_) (GetVotesAfter PerasVoteTicketNo
ticketNo) LookUp
_ a
actual = do
    let expected :: Map
  PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
expected = PerasVoteTicketNo
-> Model TestBlock
-> Map
     PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
forall blk.
PerasVoteTicketNo
-> Model blk
-> Map PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote blk))
Model.getVotesAfter PerasVoteTicketNo
ticketNo Model TestBlock
model
    TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Mismatched result:"
    TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Model: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Map
  PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
-> TestName
forall a. Show a => a -> TestName
show Map
  PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
expected
    TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB 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 (PerasVoteDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool)
-> Bool
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a b. (a -> b) -> a -> b
$ Map
  PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
expected Map
  PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
-> Map
     PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
-> Bool
forall a. Eq a => a -> a -> Bool
== a
Map
  PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
actual
  postcondition (Model Model TestBlock
model, Model
_) (GetForgedCertForRound PerasRoundNo
roundNo) LookUp
_ a
actual = do
    let expected :: Maybe (ValidatedPerasCert TestBlock)
expected = PerasRoundNo
-> Map PerasRoundNo (ValidatedPerasCert TestBlock)
-> Maybe (ValidatedPerasCert TestBlock)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup PerasRoundNo
roundNo (Model TestBlock -> Map PerasRoundNo (ValidatedPerasCert TestBlock)
forall blk. Model blk -> Map PerasRoundNo (ValidatedPerasCert blk)
Model.certs Model TestBlock
model)
    TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Mismatched result:"
    TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Model: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Maybe (ValidatedPerasCert TestBlock) -> TestName
forall a. Show a => a -> TestName
show Maybe (ValidatedPerasCert TestBlock)
expected
    TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB 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 (PerasVoteDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool)
-> Bool
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a b. (a -> b) -> a -> b
$ Maybe (ValidatedPerasCert TestBlock)
expected Maybe (ValidatedPerasCert TestBlock)
-> Maybe (ValidatedPerasCert TestBlock) -> Bool
forall a. Eq a => a -> a -> Bool
== a
Maybe (ValidatedPerasCert TestBlock)
actual
  postcondition (Model, Model)
_ Action Model a
_ LookUp
_ a
_ = Bool -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasVoteDB 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 (PerasVoteDB IO TestBlock) IO)) a
-> Property
-> Property
monitoring (Model
_, Model Model TestBlock
model') (AddVote WithArrivalTime (ValidatedPerasVote TestBlock)
vote) LookUp
_ (Right a
res) = do
    TestName -> [TestName] -> Property -> Property
forall prop.
Testable prop =>
TestName -> [TestName] -> prop -> Property
tabulate TestName
"AddVote" [(PerasVoteDbError TestBlock -> TestName)
-> (AddPerasVoteResult TestBlock -> TestName)
-> Either
     (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)
-> TestName
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either PerasVoteDbError TestBlock -> TestName
perasVoteDBErrorTag AddPerasVoteResult TestBlock -> TestName
addVoteResultTag a
Either (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)
res]
      -- In addition to the result of the command, we also tabulate how many
      -- votes were needed to reach quorum (if quorum was reached).
      (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestName -> [TestName] -> Property -> Property
forall prop.
Testable prop =>
TestName -> [TestName] -> prop -> Property
tabulate TestName
"Votes until quorum" (Model TestBlock
-> WithArrivalTime (ValidatedPerasVote TestBlock)
-> Either
     (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)
-> [TestName]
votesToReachQuorum Model TestBlock
model' WithArrivalTime (ValidatedPerasVote TestBlock)
vote a
Either (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)
res)
  monitoring (Model, Model)
_ (Action Model a
R:ActionModela a
GetVoteIds) LookUp
_ (Right a
res) = do
    let tag :: TestName
tag = if Set (PerasVoteId TestBlock) -> Bool
forall a. Set a -> Bool
Set.null a
Set (PerasVoteId TestBlock)
res then TestName
"NoVoteIds" else TestName
"HasVoteIds"
    TestName -> [TestName] -> Property -> Property
forall prop.
Testable prop =>
TestName -> [TestName] -> prop -> Property
tabulate TestName
"GetVoteIds" [TestName
tag]
  monitoring (Model, Model)
_ (GetVotesAfter PerasVoteTicketNo
_) LookUp
_ (Right a
res) = do
    let tag :: TestName
tag = if Map
  PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
-> Bool
forall k a. Map k a -> Bool
Map.null a
Map
  PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
res then TestName
"NoVotesAfter" else TestName
"HasVotesAfter"
    TestName -> [TestName] -> Property -> Property
forall prop.
Testable prop =>
TestName -> [TestName] -> prop -> Property
tabulate TestName
"GetVotesAfter" [TestName
tag]
  monitoring (Model, Model)
_ (GetForgedCertForRound{}) LookUp
_ (Right a
res) = do
    let tag :: TestName
tag = TestName
-> (ValidatedPerasCert TestBlock -> TestName)
-> Maybe (ValidatedPerasCert TestBlock)
-> TestName
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TestName
"NoCert" (TestName -> ValidatedPerasCert TestBlock -> TestName
forall a b. a -> b -> a
const TestName
"FoundCert") a
Maybe (ValidatedPerasCert TestBlock)
res
    TestName -> [TestName] -> Property -> Property
forall prop.
Testable prop =>
TestName -> [TestName] -> prop -> Property
tabulate TestName
"GetForgedCertForRound" [TestName
tag]
  monitoring (Model, Model)
_ Action Model a
_ LookUp
_ Either (Error Model (StateT (PerasVoteDB IO TestBlock) IO)) a
_ =
    Property -> Property
forall a. a -> a
id

-- * Reusable generators

-- | Generate a random 'PerasVoterId'.
--
-- We want to force collisions when adding votes, so we need to restrict
-- the key space a lot here. Otherwise we might never hit the case where
-- the same voter casts two votes for the same round/block.
genVoterId :: Gen PerasVoterId
genVoterId :: Gen PerasVoterId
genVoterId = do
  let mkVoterKey :: Char -> ByteString
mkVoterKey = TestName -> ByteString
forall a. IsString a => TestName -> a
fromString (TestName -> ByteString)
-> (Char -> TestName) -> Char -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Char -> TestName
forall a. Int -> a -> [a]
replicate Int
32
  bytes <- Char -> ByteString
mkVoterKey (Char -> ByteString) -> Gen Char -> Gen ByteString
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TestName -> Gen Char
forall a. HasCallStack => [a] -> Gen a
elements [Int -> Char
chr Int
c | Int
c <- [Int
0 .. Int
99]]
  let signKey = Seed -> SignKeyDSIGN DSIGN
forall v. DSIGNAlgorithm v => Seed -> SignKeyDSIGN v
SL.genKeyDSIGN (ByteString -> Seed
SL.mkSeedFromBytes ByteString
bytes)
  let verKey = SignKeyDSIGN DSIGN -> VerKeyDSIGN DSIGN
forall v. DSIGNAlgorithm v => SignKeyDSIGN v -> VerKeyDSIGN v
SL.deriveVerKeyDSIGN SignKeyDSIGN DSIGN
signKey
  let keyHash = VKey StakePool -> KeyHash StakePool
forall (kd :: KeyRole). VKey kd -> KeyHash kd
SL.hashKey (VerKeyDSIGN DSIGN -> VKey StakePool
forall (kd :: KeyRole). VerKeyDSIGN DSIGN -> VKey kd
SL.VKey VerKeyDSIGN DSIGN
verKey)
  pure (PerasVoterId keyHash)

-- | Generate a random 'PerasVoteStake'.
--
-- Make it so that we always require multiple votes to reach a quorum.
-- This is assuming a quorum threshold strictly larger than 50%, which is
-- a very conservative assumption for Peras.
genVoteStake :: Gen PerasVoteStake
genVoteStake :: Gen PerasVoteStake
genVoteStake = do
  stake <- (Integer
1 Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
%) (Integer -> Rational) -> Gen Integer -> Gen Rational
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> Gen Integer
forall a. Random a => (a, a) -> Gen a
choose (Integer
2, Integer
10) -- stake between 1/2 and 1/10
  pure (PerasVoteStake stake)

-- * Helpers

perasVoteDBErrorTag :: PerasVoteDbError TestBlock -> String
perasVoteDBErrorTag :: PerasVoteDbError TestBlock -> TestName
perasVoteDBErrorTag PerasVoteDbError TestBlock
err =
  case PerasVoteDbError TestBlock
err of
    MultipleWinnersInRound{} ->
      TestName
"MultipleWinnersInRound"
    ForgingCertError{} ->
      TestName
"ForgingCertError"

addVoteResultTag :: AddPerasVoteResult TestBlock -> String
addVoteResultTag :: AddPerasVoteResult TestBlock -> TestName
addVoteResultTag AddPerasVoteResult TestBlock
res =
  case AddPerasVoteResult TestBlock
res of
    AddPerasVoteResult TestBlock
PerasVoteAlreadyInDB ->
      TestName
"PerasVoteAlreadyInDB"
    AddedPerasVoteAndGeneratedNewCert{} ->
      TestName
"AddedPerasVoteAndGeneratedNewCert"
    AddPerasVoteResult TestBlock
AddedPerasVoteButDidntGenerateNewCert ->
      TestName
"AddedPerasVoteButDidntGenerateNewCert"

votesToReachQuorum ::
  Model.Model TestBlock ->
  WithArrivalTime (ValidatedPerasVote TestBlock) ->
  Either (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock) ->
  [String]
votesToReachQuorum :: Model TestBlock
-> WithArrivalTime (ValidatedPerasVote TestBlock)
-> Either
     (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)
-> [TestName]
votesToReachQuorum Model TestBlock
model WithArrivalTime (ValidatedPerasVote TestBlock)
vote Either (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)
res =
  case Either (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)
res of
    Right AddedPerasVoteAndGeneratedNewCert{} ->
      [Int -> TestName
forall a. Show a => a -> TestName
show (Set (VoteEntry TestBlock) -> Int
forall a. Set a -> Int
Set.size Set (VoteEntry TestBlock)
votesInRound)]
    Either (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)
_ ->
      []
 where
  votesInRound :: Set (VoteEntry TestBlock)
votesInRound =
    Set (VoteEntry TestBlock)
-> PerasVoteTarget TestBlock
-> Map (PerasVoteTarget TestBlock) (Set (VoteEntry TestBlock))
-> Set (VoteEntry TestBlock)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
      Set (VoteEntry TestBlock)
forall a. Set a
Set.empty
      PerasVoteTarget
        { pvtRoundNo :: PerasRoundNo
pvtRoundNo = WithArrivalTime (ValidatedPerasVote TestBlock) -> PerasRoundNo
forall vote. HasPerasVoteRound vote => vote -> PerasRoundNo
getPerasVoteRound WithArrivalTime (ValidatedPerasVote TestBlock)
vote
        , pvtBlock :: Point TestBlock
pvtBlock = WithArrivalTime (ValidatedPerasVote TestBlock) -> Point TestBlock
forall vote blk. HasPerasVoteBlock vote blk => vote -> Point blk
getPerasVoteBlock WithArrivalTime (ValidatedPerasVote TestBlock)
vote
        }
      (Model TestBlock
-> Map (PerasVoteTarget TestBlock) (Set (VoteEntry TestBlock))
forall blk.
Model blk -> Map (PerasVoteTarget blk) (Set (VoteEntry blk))
Model.votes Model TestBlock
model)