{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

-- | Tests for the volatile DB
--
-- The set of commands for the volatile DB is similar to the immutable DB,
-- commands such as:
--
-- * Get a block or information about a block
-- * Add a block
-- * Simulate disk corruption
--
-- in addition to a few commands that are supported only by the volatile DB,
-- such as "find all blocks with the given predecessor" (used by chain selection).
-- The model (defined in @Test.Ouroboros.Storage.VolatileDB.Model@) is a list
-- of "files", where every file is modelled simply as a list of blocks and some
-- block metadata. The reason that this is slightly more detailed than one might
-- hope (just a set of blocks) is that we need the additional detail to be able
-- to predict the effects of disk corruption.
module Test.Ouroboros.Storage.VolatileDB.StateMachine
  ( showLabelledExamples
  , tests
  ) where

import Control.Concurrent.Class.MonadSTM.Strict (newTMVar)
import Control.Monad (forM_, void)
import Control.ResourceRegistry
import Data.Bifunctor (first)
import Data.ByteString.Lazy (ByteString)
import Data.Functor.Classes
import Data.Functor.Identity (Identity)
import Data.Kind (Type)
import qualified Data.List.NonEmpty as NE
import qualified Data.Map.Strict as Map
import Data.Maybe (catMaybes, listToMaybe, mapMaybe)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.TreeDiff
import Data.Word
import GHC.Generics
import GHC.Stack
import qualified Generics.SOP as SOP
import Ouroboros.Consensus.Block
import Ouroboros.Consensus.Storage.Common
import Ouroboros.Consensus.Storage.VolatileDB
import Ouroboros.Consensus.Storage.VolatileDB.Impl.Types (FileId)
import Ouroboros.Consensus.Storage.VolatileDB.Impl.Util
import Ouroboros.Consensus.Util.IOLike
import Ouroboros.Network.Block (MaxSlotNo)
import System.FS.API.Lazy
import System.FS.Sim.Error
import qualified System.FS.Sim.MockFS as Mock
import System.Random (getStdRandom, randomR)
import Test.Ouroboros.Storage.Orphans ()
import Test.Ouroboros.Storage.TestBlock
import Test.Ouroboros.Storage.VolatileDB.Model
import Test.QuickCheck hiding (forAll)
import Test.QuickCheck.Monadic
import Test.QuickCheck.Random (mkQCGen)
import Test.StateMachine hiding
  ( showLabelledExamples
  , showLabelledExamples'
  )
import qualified Test.StateMachine.Labelling as C
import qualified Test.StateMachine.Sequential as QSM
import Test.StateMachine.Types
import qualified Test.StateMachine.Types.Rank2 as Rank2
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.QuickCheck (testProperty)
import Test.Util.Orphans.Arbitrary ()
import Test.Util.Orphans.ToExpr ()
import Test.Util.QuickCheck
import Test.Util.SOP
import Test.Util.ToExpr ()
import Test.Util.Tracer (recordingTracerIORef)
import Text.Show.Pretty (ppShow)
import Prelude hiding (elem)

type Block = TestBlock

newtype At t (r :: Type -> Type) = At {forall t (r :: * -> *). At t r -> t
unAt :: t}
  deriving (forall x. At t r -> Rep (At t r) x)
-> (forall x. Rep (At t r) x -> At t r) -> Generic (At t r)
forall x. Rep (At t r) x -> At t r
forall x. At t r -> Rep (At t r) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t (r :: * -> *) x. Rep (At t r) x -> At t r
forall t (r :: * -> *) x. At t r -> Rep (At t r) x
$cfrom :: forall t (r :: * -> *) x. At t r -> Rep (At t r) x
from :: forall x. At t r -> Rep (At t r) x
$cto :: forall t (r :: * -> *) x. Rep (At t r) x -> At t r
to :: forall x. Rep (At t r) x -> At t r
Generic

-- | Alias for 'At'
type (:@) t r = At t r

-- | Product of all 'BlockComponent's. As this is a GADT, generating random
-- values of it (and combinations!) is not so simple. Therefore, we just
-- always request all block components.
allComponents :: BlockComponent blk (AllComponents blk)
allComponents :: forall blk. BlockComponent blk (AllComponents blk)
allComponents =
  (,,,,,,,,,,)
    (blk
 -> blk
 -> ByteString
 -> Header blk
 -> ByteString
 -> HeaderHash blk
 -> SlotNo
 -> IsEBB
 -> SizeInBytes
 -> Word16
 -> SomeSecond (NestedCtxt Header) blk
 -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
     SlotNo, IsEBB, SizeInBytes, Word16,
     SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk blk
-> BlockComponent
     blk
     (blk
      -> ByteString
      -> Header blk
      -> ByteString
      -> HeaderHash blk
      -> SlotNo
      -> IsEBB
      -> SizeInBytes
      -> Word16
      -> SomeSecond (NestedCtxt Header) blk
      -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
          SlotNo, IsEBB, SizeInBytes, Word16,
          SomeSecond (NestedCtxt Header) blk))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BlockComponent blk blk
forall blk. BlockComponent blk blk
GetVerifiedBlock
    BlockComponent
  blk
  (blk
   -> ByteString
   -> Header blk
   -> ByteString
   -> HeaderHash blk
   -> SlotNo
   -> IsEBB
   -> SizeInBytes
   -> Word16
   -> SomeSecond (NestedCtxt Header) blk
   -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
       SlotNo, IsEBB, SizeInBytes, Word16,
       SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk blk
-> BlockComponent
     blk
     (ByteString
      -> Header blk
      -> ByteString
      -> HeaderHash blk
      -> SlotNo
      -> IsEBB
      -> SizeInBytes
      -> Word16
      -> SomeSecond (NestedCtxt Header) blk
      -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
          SlotNo, IsEBB, SizeInBytes, Word16,
          SomeSecond (NestedCtxt Header) blk))
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk blk
forall blk. BlockComponent blk blk
GetBlock
    BlockComponent
  blk
  (ByteString
   -> Header blk
   -> ByteString
   -> HeaderHash blk
   -> SlotNo
   -> IsEBB
   -> SizeInBytes
   -> Word16
   -> SomeSecond (NestedCtxt Header) blk
   -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
       SlotNo, IsEBB, SizeInBytes, Word16,
       SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk ByteString
-> BlockComponent
     blk
     (Header blk
      -> ByteString
      -> HeaderHash blk
      -> SlotNo
      -> IsEBB
      -> SizeInBytes
      -> Word16
      -> SomeSecond (NestedCtxt Header) blk
      -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
          SlotNo, IsEBB, SizeInBytes, Word16,
          SomeSecond (NestedCtxt Header) blk))
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk ByteString
forall blk. BlockComponent blk ByteString
GetRawBlock
    BlockComponent
  blk
  (Header blk
   -> ByteString
   -> HeaderHash blk
   -> SlotNo
   -> IsEBB
   -> SizeInBytes
   -> Word16
   -> SomeSecond (NestedCtxt Header) blk
   -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
       SlotNo, IsEBB, SizeInBytes, Word16,
       SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk (Header blk)
-> BlockComponent
     blk
     (ByteString
      -> HeaderHash blk
      -> SlotNo
      -> IsEBB
      -> SizeInBytes
      -> Word16
      -> SomeSecond (NestedCtxt Header) blk
      -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
          SlotNo, IsEBB, SizeInBytes, Word16,
          SomeSecond (NestedCtxt Header) blk))
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk (Header blk)
forall blk. BlockComponent blk (Header blk)
GetHeader
    BlockComponent
  blk
  (ByteString
   -> HeaderHash blk
   -> SlotNo
   -> IsEBB
   -> SizeInBytes
   -> Word16
   -> SomeSecond (NestedCtxt Header) blk
   -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
       SlotNo, IsEBB, SizeInBytes, Word16,
       SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk ByteString
-> BlockComponent
     blk
     (HeaderHash blk
      -> SlotNo
      -> IsEBB
      -> SizeInBytes
      -> Word16
      -> SomeSecond (NestedCtxt Header) blk
      -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
          SlotNo, IsEBB, SizeInBytes, Word16,
          SomeSecond (NestedCtxt Header) blk))
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk ByteString
forall blk. BlockComponent blk ByteString
GetRawHeader
    BlockComponent
  blk
  (HeaderHash blk
   -> SlotNo
   -> IsEBB
   -> SizeInBytes
   -> Word16
   -> SomeSecond (NestedCtxt Header) blk
   -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
       SlotNo, IsEBB, SizeInBytes, Word16,
       SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk (HeaderHash blk)
-> BlockComponent
     blk
     (SlotNo
      -> IsEBB
      -> SizeInBytes
      -> Word16
      -> SomeSecond (NestedCtxt Header) blk
      -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
          SlotNo, IsEBB, SizeInBytes, Word16,
          SomeSecond (NestedCtxt Header) blk))
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk (HeaderHash blk)
forall blk. BlockComponent blk (HeaderHash blk)
GetHash
    BlockComponent
  blk
  (SlotNo
   -> IsEBB
   -> SizeInBytes
   -> Word16
   -> SomeSecond (NestedCtxt Header) blk
   -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
       SlotNo, IsEBB, SizeInBytes, Word16,
       SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk SlotNo
-> BlockComponent
     blk
     (IsEBB
      -> SizeInBytes
      -> Word16
      -> SomeSecond (NestedCtxt Header) blk
      -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
          SlotNo, IsEBB, SizeInBytes, Word16,
          SomeSecond (NestedCtxt Header) blk))
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk SlotNo
forall blk. BlockComponent blk SlotNo
GetSlot
    BlockComponent
  blk
  (IsEBB
   -> SizeInBytes
   -> Word16
   -> SomeSecond (NestedCtxt Header) blk
   -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
       SlotNo, IsEBB, SizeInBytes, Word16,
       SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk IsEBB
-> BlockComponent
     blk
     (SizeInBytes
      -> Word16
      -> SomeSecond (NestedCtxt Header) blk
      -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
          SlotNo, IsEBB, SizeInBytes, Word16,
          SomeSecond (NestedCtxt Header) blk))
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk IsEBB
forall blk. BlockComponent blk IsEBB
GetIsEBB
    BlockComponent
  blk
  (SizeInBytes
   -> Word16
   -> SomeSecond (NestedCtxt Header) blk
   -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
       SlotNo, IsEBB, SizeInBytes, Word16,
       SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk SizeInBytes
-> BlockComponent
     blk
     (Word16
      -> SomeSecond (NestedCtxt Header) blk
      -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
          SlotNo, IsEBB, SizeInBytes, Word16,
          SomeSecond (NestedCtxt Header) blk))
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk SizeInBytes
forall blk. BlockComponent blk SizeInBytes
GetBlockSize
    BlockComponent
  blk
  (Word16
   -> SomeSecond (NestedCtxt Header) blk
   -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
       SlotNo, IsEBB, SizeInBytes, Word16,
       SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk Word16
-> BlockComponent
     blk
     (SomeSecond (NestedCtxt Header) blk
      -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
          SlotNo, IsEBB, SizeInBytes, Word16,
          SomeSecond (NestedCtxt Header) blk))
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk Word16
forall blk. BlockComponent blk Word16
GetHeaderSize
    BlockComponent
  blk
  (SomeSecond (NestedCtxt Header) blk
   -> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
       SlotNo, IsEBB, SizeInBytes, Word16,
       SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk (SomeSecond (NestedCtxt Header) blk)
-> BlockComponent
     blk
     (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
      SlotNo, IsEBB, SizeInBytes, Word16,
      SomeSecond (NestedCtxt Header) blk)
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk (SomeSecond (NestedCtxt Header) blk)
forall blk. BlockComponent blk (SomeSecond (NestedCtxt Header) blk)
GetNestedCtxt

-- | A list of all the 'BlockComponent' indices (@b@) we are interested in.
type AllComponents blk =
  ( blk
  , blk
  , ByteString
  , Header blk
  , ByteString
  , HeaderHash blk
  , SlotNo
  , IsEBB
  , SizeInBytes
  , Word16
  , SomeSecond (NestedCtxt Header) blk
  )

data Cmd
  = Close
  | ReOpen
  | GetBlockComponent (HeaderHash Block)
  | PutBlock Block
  | GarbageCollect SlotNo
  | FilterByPredecessor [ChainHash Block]
  | GetBlockInfo [HeaderHash Block]
  | GetMaxSlotNo
  | Corruption Corruptions
  | DuplicateBlock FileId Block
  deriving (Int -> Cmd -> ShowS
[Cmd] -> ShowS
Cmd -> String
(Int -> Cmd -> ShowS)
-> (Cmd -> String) -> ([Cmd] -> ShowS) -> Show Cmd
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Cmd -> ShowS
showsPrec :: Int -> Cmd -> ShowS
$cshow :: Cmd -> String
show :: Cmd -> String
$cshowList :: [Cmd] -> ShowS
showList :: [Cmd] -> ShowS
Show, (forall x. Cmd -> Rep Cmd x)
-> (forall x. Rep Cmd x -> Cmd) -> Generic Cmd
forall x. Rep Cmd x -> Cmd
forall x. Cmd -> Rep Cmd x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Cmd -> Rep Cmd x
from :: forall x. Cmd -> Rep Cmd x
$cto :: forall x. Rep Cmd x -> Cmd
to :: forall x. Rep Cmd x -> Cmd
Generic)

data CmdErr = CmdErr
  { CmdErr -> Cmd
cmd :: Cmd
  , CmdErr -> Maybe Errors
err :: Maybe Errors
  }
  deriving Int -> CmdErr -> ShowS
[CmdErr] -> ShowS
CmdErr -> String
(Int -> CmdErr -> ShowS)
-> (CmdErr -> String) -> ([CmdErr] -> ShowS) -> Show CmdErr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CmdErr -> ShowS
showsPrec :: Int -> CmdErr -> ShowS
$cshow :: CmdErr -> String
show :: CmdErr -> String
$cshowList :: [CmdErr] -> ShowS
showList :: [CmdErr] -> ShowS
Show

-- | We compare two functions based on their results on a list of inputs
-- (functional extensionality).
data Success
  = Unit ()
  | MbAllComponents (Maybe (AllComponents Block))
  | Bool Bool
  | Successors [Set (HeaderHash Block)]
  | BlockInfos [Maybe (BlockInfo Block)]
  | MaxSlot MaxSlotNo
  deriving (Int -> Success -> ShowS
[Success] -> ShowS
Success -> String
(Int -> Success -> ShowS)
-> (Success -> String) -> ([Success] -> ShowS) -> Show Success
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Success -> ShowS
showsPrec :: Int -> Success -> ShowS
$cshow :: Success -> String
show :: Success -> String
$cshowList :: [Success] -> ShowS
showList :: [Success] -> ShowS
Show, Success -> Success -> Bool
(Success -> Success -> Bool)
-> (Success -> Success -> Bool) -> Eq Success
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Success -> Success -> Bool
== :: Success -> Success -> Bool
$c/= :: Success -> Success -> Bool
/= :: Success -> Success -> Bool
Eq)

newtype Resp = Resp
  { Resp -> Either (VolatileDBError Block) Success
getResp :: Either (VolatileDBError Block) Success
  }
  deriving (Resp -> Resp -> Bool
(Resp -> Resp -> Bool) -> (Resp -> Resp -> Bool) -> Eq Resp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Resp -> Resp -> Bool
== :: Resp -> Resp -> Bool
$c/= :: Resp -> Resp -> Bool
/= :: Resp -> Resp -> Bool
Eq, Int -> Resp -> ShowS
[Resp] -> ShowS
Resp -> String
(Int -> Resp -> ShowS)
-> (Resp -> String) -> ([Resp] -> ShowS) -> Show Resp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Resp -> ShowS
showsPrec :: Int -> Resp -> ShowS
$cshow :: Resp -> String
show :: Resp -> String
$cshowList :: [Resp] -> ShowS
showList :: [Resp] -> ShowS
Show)

deriving instance Generic1 (At Cmd)
deriving instance Generic1 (At CmdErr)
deriving instance Rank2.Foldable (At Cmd)
deriving instance Rank2.Foldable (At CmdErr)
deriving instance Rank2.Functor (At Cmd)
deriving instance Rank2.Functor (At CmdErr)
deriving instance Rank2.Traversable (At CmdErr)
deriving instance Show1 r => Show (CmdErr :@ r)
deriving instance Show1 r => Show (Cmd :@ r)

deriving instance SOP.Generic Cmd
deriving instance SOP.HasDatatypeInfo Cmd

deriving instance Generic1 (At Resp)
deriving instance Rank2.Foldable (At Resp)
deriving instance Show1 r => Show (Resp :@ r)

deriving instance ToExpr (Model r)

instance CommandNames (At Cmd) where
  cmdName :: forall (r :: * -> *). At Cmd r -> String
cmdName (At Cmd
cmd) = Cmd -> String
forall a. HasDatatypeInfo a => a -> String
constrName Cmd
cmd
  cmdNames :: forall (r :: * -> *). Proxy (At Cmd r) -> [String]
cmdNames (Proxy (At Cmd r)
_ :: Proxy (At Cmd r)) = Proxy Cmd -> [String]
forall a (proxy :: * -> *).
HasDatatypeInfo a =>
proxy a -> [String]
constrNames (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Cmd)

instance CommandNames (At CmdErr) where
  cmdName :: forall (r :: * -> *). At CmdErr r -> String
cmdName (At (CmdErr{Cmd
cmd :: CmdErr -> Cmd
cmd :: Cmd
cmd})) = Cmd -> String
forall a. HasDatatypeInfo a => a -> String
constrName Cmd
cmd
  cmdNames :: forall (r :: * -> *). Proxy (At CmdErr r) -> [String]
cmdNames (Proxy (At CmdErr r)
_ :: Proxy (At CmdErr r)) = Proxy Cmd -> [String]
forall a (proxy :: * -> *).
HasDatatypeInfo a =>
proxy a -> [String]
constrNames (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Cmd)

newtype Model (r :: Type -> Type) = Model
  { forall (r :: * -> *). Model r -> DBModel Block
dbModel :: DBModel Block
  -- ^ A model of the database.
  }
  deriving ((forall x. Model r -> Rep (Model r) x)
-> (forall x. Rep (Model r) x -> Model r) -> Generic (Model r)
forall x. Rep (Model r) x -> Model r
forall x. Model r -> Rep (Model r) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (r :: * -> *) x. Rep (Model r) x -> Model r
forall (r :: * -> *) x. Model r -> Rep (Model r) x
$cfrom :: forall (r :: * -> *) x. Model r -> Rep (Model r) x
from :: forall x. Model r -> Rep (Model r) x
$cto :: forall (r :: * -> *) x. Rep (Model r) x -> Model r
to :: forall x. Rep (Model r) x -> Model r
Generic, Int -> Model r -> ShowS
[Model r] -> ShowS
Model r -> String
(Int -> Model r -> ShowS)
-> (Model r -> String) -> ([Model r] -> ShowS) -> Show (Model r)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (r :: * -> *). Int -> Model r -> ShowS
forall (r :: * -> *). [Model r] -> ShowS
forall (r :: * -> *). Model r -> String
$cshowsPrec :: forall (r :: * -> *). Int -> Model r -> ShowS
showsPrec :: Int -> Model r -> ShowS
$cshow :: forall (r :: * -> *). Model r -> String
show :: Model r -> String
$cshowList :: forall (r :: * -> *). [Model r] -> ShowS
showList :: [Model r] -> ShowS
Show)

-- | An event records the model before and after a command along with the
-- command itself, and a mocked version of the response.
data Event r = Event
  { forall (r :: * -> *). Event r -> Model r
eventBefore :: Model r
  , forall (r :: * -> *). Event r -> At CmdErr r
eventCmd :: At CmdErr r
  , forall (r :: * -> *). Event r -> Model r
eventAfter :: Model r
  , forall (r :: * -> *). Event r -> Resp
eventMockResp :: Resp
  }
  deriving Int -> Event r -> ShowS
[Event r] -> ShowS
Event r -> String
(Int -> Event r -> ShowS)
-> (Event r -> String) -> ([Event r] -> ShowS) -> Show (Event r)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (r :: * -> *). Show1 r => Int -> Event r -> ShowS
forall (r :: * -> *). Show1 r => [Event r] -> ShowS
forall (r :: * -> *). Show1 r => Event r -> String
$cshowsPrec :: forall (r :: * -> *). Show1 r => Int -> Event r -> ShowS
showsPrec :: Int -> Event r -> ShowS
$cshow :: forall (r :: * -> *). Show1 r => Event r -> String
show :: Event r -> String
$cshowList :: forall (r :: * -> *). Show1 r => [Event r] -> ShowS
showList :: [Event r] -> ShowS
Show

lockstep ::
  forall r.
  Model r ->
  At CmdErr r ->
  Event r
lockstep :: forall (r :: * -> *). Model r -> At CmdErr r -> Event r
lockstep Model r
model At CmdErr r
cmdErr =
  Event
    { eventBefore :: Model r
eventBefore = Model r
model
    , eventCmd :: At CmdErr r
eventCmd = At CmdErr r
cmdErr
    , eventAfter :: Model r
eventAfter = Model r
forall {r :: * -> *}. Model r
model'
    , eventMockResp :: Resp
eventMockResp = Resp
mockResp
    }
 where
  (Resp
mockResp, DBModel Block
dbModel') = Model r -> At CmdErr r -> (Resp, DBModel Block)
forall (r :: * -> *).
Model r -> At CmdErr r -> (Resp, DBModel Block)
step Model r
model At CmdErr r
cmdErr
  model' :: Model r
model' = DBModel Block -> Model r
forall (r :: * -> *). DBModel Block -> Model r
Model DBModel Block
dbModel'

-- | Key property of the model is that we can go from real to mock responses.
toMock :: Model r -> At t r -> t
toMock :: forall (r :: * -> *) t. Model r -> At t r -> t
toMock Model r
_ (At t
t) = t
t

step :: Model r -> At CmdErr r -> (Resp, DBModel Block)
step :: forall (r :: * -> *).
Model r -> At CmdErr r -> (Resp, DBModel Block)
step model :: Model r
model@Model{DBModel Block
dbModel :: forall (r :: * -> *). Model r -> DBModel Block
dbModel :: DBModel Block
..} At CmdErr r
cmderr = DBModel Block -> CmdErr -> (Resp, DBModel Block)
runPureErr DBModel Block
dbModel (Model r -> At CmdErr r -> CmdErr
forall (r :: * -> *) t. Model r -> At t r -> t
toMock Model r
model At CmdErr r
cmderr)

runPure :: Cmd -> DBModel Block -> (Resp, DBModel Block)
runPure :: Cmd -> DBModel Block -> (Resp, DBModel Block)
runPure = \case
  GetBlockComponent HeaderHash Block
h -> (Maybe
   (Block, Block, ByteString, Header Block, ByteString,
    TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
    SomeSecond (NestedCtxt Header) Block)
 -> Success)
-> (DBModel Block
    -> (Either
          (VolatileDBError Block)
          (Maybe
             (Block, Block, ByteString, Header Block, ByteString,
              TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
              SomeSecond (NestedCtxt Header) Block)),
        DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
    -> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok Maybe (AllComponents Block) -> Success
Maybe
  (Block, Block, ByteString, Header Block, ByteString,
   TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
   SomeSecond (NestedCtxt Header) Block)
-> Success
MbAllComponents ((DBModel Block
  -> (Either
        (VolatileDBError Block)
        (Maybe
           (Block, Block, ByteString, Header Block, ByteString,
            TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
            SomeSecond (NestedCtxt Header) Block)),
      DBModel Block))
 -> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
    -> (Either
          (VolatileDBError Block)
          (Maybe
             (Block, Block, ByteString, Header Block, ByteString,
              TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
              SomeSecond (NestedCtxt Header) Block)),
        DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block
 -> Either
      (VolatileDBError Block)
      (Maybe
         (Block, Block, ByteString, Header Block, ByteString,
          TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
          SomeSecond (NestedCtxt Header) Block)))
-> DBModel Block
-> (Either
      (VolatileDBError Block)
      (Maybe
         (Block, Block, ByteString, Header Block, ByteString,
          TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
          SomeSecond (NestedCtxt Header) Block)),
    DBModel Block)
forall {b} {a}. (b -> a) -> b -> (a, b)
queryE (BlockComponent
  Block
  (Block, Block, ByteString, Header Block, ByteString,
   TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
   SomeSecond (NestedCtxt Header) Block)
-> HeaderHash Block
-> DBModel Block
-> Either
     (VolatileDBError Block)
     (Maybe
        (Block, Block, ByteString, Header Block, ByteString,
         TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
         SomeSecond (NestedCtxt Header) Block))
forall blk b.
(HasHeader blk, GetHeader blk, HasBinaryBlockInfo blk,
 EncodeDisk blk blk, HasNestedContent Header blk) =>
BlockComponent blk b
-> HeaderHash blk
-> DBModel blk
-> Either (VolatileDBError blk) (Maybe b)
getBlockComponentModel BlockComponent Block (AllComponents Block)
BlockComponent
  Block
  (Block, Block, ByteString, Header Block, ByteString,
   TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
   SomeSecond (NestedCtxt Header) Block)
forall blk. BlockComponent blk (AllComponents blk)
allComponents HeaderHash Block
h)
  FilterByPredecessor [ChainHash Block]
hs -> ((ChainHash Block -> Set TestHeaderHash) -> Success)
-> (DBModel Block
    -> (Either
          (VolatileDBError Block) (ChainHash Block -> Set TestHeaderHash),
        DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
    -> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok ([Set (HeaderHash Block)] -> Success
[Set TestHeaderHash] -> Success
Successors ([Set TestHeaderHash] -> Success)
-> ((ChainHash Block -> Set TestHeaderHash)
    -> [Set TestHeaderHash])
-> (ChainHash Block -> Set TestHeaderHash)
-> Success
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ChainHash Block -> Set TestHeaderHash)
-> [ChainHash Block] -> [Set TestHeaderHash]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ChainHash Block]
hs)) ((DBModel Block
  -> (Either
        (VolatileDBError Block) (ChainHash Block -> Set TestHeaderHash),
      DBModel Block))
 -> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
    -> (Either
          (VolatileDBError Block) (ChainHash Block -> Set TestHeaderHash),
        DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block
 -> Either
      (VolatileDBError Block) (ChainHash Block -> Set TestHeaderHash))
-> DBModel Block
-> (Either
      (VolatileDBError Block) (ChainHash Block -> Set TestHeaderHash),
    DBModel Block)
forall {b} {a}. (b -> a) -> b -> (a, b)
queryE DBModel Block
-> Either
     (VolatileDBError Block) (ChainHash Block -> Set (HeaderHash Block))
DBModel Block
-> Either
     (VolatileDBError Block) (ChainHash Block -> Set TestHeaderHash)
forall blk.
GetPrevHash blk =>
DBModel blk
-> Either
     (VolatileDBError blk) (ChainHash blk -> Set (HeaderHash blk))
filterByPredecessorModel
  GetBlockInfo [HeaderHash Block]
hs -> ((TestHeaderHash -> Maybe (BlockInfo Block)) -> Success)
-> (DBModel Block
    -> (Either
          (VolatileDBError Block)
          (TestHeaderHash -> Maybe (BlockInfo Block)),
        DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
    -> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok ([Maybe (BlockInfo Block)] -> Success
BlockInfos ([Maybe (BlockInfo Block)] -> Success)
-> ((TestHeaderHash -> Maybe (BlockInfo Block))
    -> [Maybe (BlockInfo Block)])
-> (TestHeaderHash -> Maybe (BlockInfo Block))
-> Success
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((HeaderHash Block -> Maybe (BlockInfo Block))
-> [HeaderHash Block] -> [Maybe (BlockInfo Block)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [HeaderHash Block]
hs)) ((DBModel Block
  -> (Either
        (VolatileDBError Block)
        (TestHeaderHash -> Maybe (BlockInfo Block)),
      DBModel Block))
 -> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
    -> (Either
          (VolatileDBError Block)
          (TestHeaderHash -> Maybe (BlockInfo Block)),
        DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block
 -> Either
      (VolatileDBError Block)
      (TestHeaderHash -> Maybe (BlockInfo Block)))
-> DBModel Block
-> (Either
      (VolatileDBError Block)
      (TestHeaderHash -> Maybe (BlockInfo Block)),
    DBModel Block)
forall {b} {a}. (b -> a) -> b -> (a, b)
queryE DBModel Block
-> Either
     (VolatileDBError Block)
     (HeaderHash Block -> Maybe (BlockInfo Block))
DBModel Block
-> Either
     (VolatileDBError Block) (TestHeaderHash -> Maybe (BlockInfo Block))
forall blk.
(GetPrevHash blk, HasBinaryBlockInfo blk) =>
DBModel blk
-> Either
     (VolatileDBError blk) (HeaderHash blk -> Maybe (BlockInfo blk))
getBlockInfoModel
  GarbageCollect SlotNo
slot -> (() -> Success)
-> (DBModel Block
    -> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
    -> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok () -> Success
Unit ((DBModel Block
  -> (Either (VolatileDBError Block) (), DBModel Block))
 -> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
    -> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block -> Either (VolatileDBError Block) (DBModel Block))
-> DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block)
forall {b} {a}. (b -> Either a b) -> b -> (Either a (), b)
updateE_ (SlotNo
-> DBModel Block -> Either (VolatileDBError Block) (DBModel Block)
forall blk.
HasHeader blk =>
SlotNo -> DBModel blk -> Either (VolatileDBError blk) (DBModel blk)
garbageCollectModel SlotNo
slot)
  Cmd
Close -> (() -> Success)
-> (DBModel Block
    -> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
    -> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok () -> Success
Unit ((DBModel Block
  -> (Either (VolatileDBError Block) (), DBModel Block))
 -> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
    -> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block -> DBModel Block)
-> DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block)
forall {t} {b} {a}. (t -> b) -> t -> (Either a (), b)
update_ DBModel Block -> DBModel Block
forall blk. DBModel blk -> DBModel blk
closeModel
  Cmd
ReOpen -> (() -> Success)
-> (DBModel Block
    -> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
    -> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok () -> Success
Unit ((DBModel Block
  -> (Either (VolatileDBError Block) (), DBModel Block))
 -> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
    -> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block -> DBModel Block)
-> DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block)
forall {t} {b} {a}. (t -> b) -> t -> (Either a (), b)
update_ DBModel Block -> DBModel Block
forall blk. DBModel blk -> DBModel blk
reOpenModel
  Cmd
GetMaxSlotNo -> (MaxSlotNo -> Success)
-> (DBModel Block
    -> (Either (VolatileDBError Block) MaxSlotNo, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
    -> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok MaxSlotNo -> Success
MaxSlot ((DBModel Block
  -> (Either (VolatileDBError Block) MaxSlotNo, DBModel Block))
 -> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
    -> (Either (VolatileDBError Block) MaxSlotNo, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block -> Either (VolatileDBError Block) MaxSlotNo)
-> DBModel Block
-> (Either (VolatileDBError Block) MaxSlotNo, DBModel Block)
forall {b} {a}. (b -> a) -> b -> (a, b)
queryE DBModel Block -> Either (VolatileDBError Block) MaxSlotNo
forall blk.
HasHeader blk =>
DBModel blk -> Either (VolatileDBError blk) MaxSlotNo
getMaxSlotNoModel
  PutBlock Block
blk -> (() -> Success)
-> (DBModel Block
    -> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
    -> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok () -> Success
Unit ((DBModel Block
  -> (Either (VolatileDBError Block) (), DBModel Block))
 -> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
    -> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block -> Either (VolatileDBError Block) (DBModel Block))
-> DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block)
forall {b} {a}. (b -> Either a b) -> b -> (Either a (), b)
updateE_ (Block
-> DBModel Block -> Either (VolatileDBError Block) (DBModel Block)
forall blk.
HasHeader blk =>
blk -> DBModel blk -> Either (VolatileDBError blk) (DBModel blk)
putBlockModel Block
blk)
  Corruption Corruptions
cors -> (() -> Success)
-> (DBModel Block
    -> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
    -> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok () -> Success
Unit ((DBModel Block
  -> (Either (VolatileDBError Block) (), DBModel Block))
 -> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
    -> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block -> DBModel Block)
-> DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block)
forall {t} {b} {a}. (t -> b) -> t -> (Either a (), b)
update_ ((DBModel Block -> DBModel Block) -> DBModel Block -> DBModel Block
forall {blk} {blk}.
(DBModel blk -> DBModel blk) -> DBModel blk -> DBModel blk
withClosedDB (Corruptions -> DBModel Block -> DBModel Block
forall blk.
EncodeDisk blk blk =>
Corruptions -> DBModel blk -> DBModel blk
runCorruptionsModel Corruptions
cors))
  DuplicateBlock{} -> (() -> Success)
-> (DBModel Block
    -> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
    -> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok () -> Success
Unit ((DBModel Block
  -> (Either (VolatileDBError Block) (), DBModel Block))
 -> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
    -> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block -> DBModel Block)
-> DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block)
forall {t} {b} {a}. (t -> b) -> t -> (Either a (), b)
update_ ((DBModel Block -> DBModel Block) -> DBModel Block -> DBModel Block
forall {blk} {blk}.
(DBModel blk -> DBModel blk) -> DBModel blk -> DBModel blk
withClosedDB DBModel Block -> DBModel Block
forall {a}. a -> a
noop)
 where
  queryE :: (b -> a) -> b -> (a, b)
queryE b -> a
f b
m = (b -> a
f b
m, b
m)

  update_ :: (t -> b) -> t -> (Either a (), b)
update_ t -> b
f t
m = (() -> Either a ()
forall a b. b -> Either a b
Right (), t -> b
f t
m)
  updateE_ :: (b -> Either a b) -> b -> (Either a (), b)
updateE_ b -> Either a b
f b
m = case b -> Either a b
f b
m of
    Left a
e -> (a -> Either a ()
forall a b. a -> Either a b
Left a
e, b
m)
    Right b
m' -> (() -> Either a ()
forall a b. b -> Either a b
Right (), b
m')

  ok ::
    (a -> Success) ->
    (DBModel Block -> (Either (VolatileDBError Block) a, DBModel Block)) ->
    DBModel Block ->
    (Resp, DBModel Block)
  ok :: forall a.
(a -> Success)
-> (DBModel Block
    -> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok a -> Success
toSuccess DBModel Block -> (Either (VolatileDBError Block) a, DBModel Block)
f DBModel Block
m = (Either (VolatileDBError Block) a -> Resp)
-> (Either (VolatileDBError Block) a, DBModel Block)
-> (Resp, DBModel Block)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Either (VolatileDBError Block) Success -> Resp
Resp (Either (VolatileDBError Block) Success -> Resp)
-> (Either (VolatileDBError Block) a
    -> Either (VolatileDBError Block) Success)
-> Either (VolatileDBError Block) a
-> Resp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Success)
-> Either (VolatileDBError Block) a
-> Either (VolatileDBError Block) Success
forall a b.
(a -> b)
-> Either (VolatileDBError Block) a
-> Either (VolatileDBError Block) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Success
toSuccess) ((Either (VolatileDBError Block) a, DBModel Block)
 -> (Resp, DBModel Block))
-> (Either (VolatileDBError Block) a, DBModel Block)
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ DBModel Block -> (Either (VolatileDBError Block) a, DBModel Block)
f DBModel Block
m

  withClosedDB :: (DBModel blk -> DBModel blk) -> DBModel blk -> DBModel blk
withClosedDB DBModel blk -> DBModel blk
action = DBModel blk -> DBModel blk
forall blk. DBModel blk -> DBModel blk
reOpenModel (DBModel blk -> DBModel blk)
-> (DBModel blk -> DBModel blk) -> DBModel blk -> DBModel blk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DBModel blk -> DBModel blk
action (DBModel blk -> DBModel blk)
-> (DBModel blk -> DBModel blk) -> DBModel blk -> DBModel blk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DBModel blk -> DBModel blk
forall blk. DBModel blk -> DBModel blk
closeModel

  noop :: a -> a
noop = a -> a
forall {a}. a -> a
id

-- | When simulating an error in the real implementation, we reopen the
-- VolatileDB and run the command again, as each command is idempotent. In the
-- model, we can just run the command once.
runPureErr :: DBModel Block -> CmdErr -> (Resp, DBModel Block)
runPureErr :: DBModel Block -> CmdErr -> (Resp, DBModel Block)
runPureErr DBModel Block
dbm (CmdErr Cmd
cmd Maybe Errors
_mbErrors) = Cmd -> DBModel Block -> (Resp, DBModel Block)
runPure Cmd
cmd DBModel Block
dbm

sm ::
  VolatileDBEnv ->
  DBModel Block ->
  StateMachine Model (At CmdErr) IO (At Resp)
sm :: VolatileDBEnv
-> DBModel Block -> StateMachine Model (At CmdErr) IO (At Resp)
sm VolatileDBEnv
env DBModel Block
dbm =
  StateMachine
    { initModel :: forall {r :: * -> *}. Model r
initModel = DBModel Block -> Model r
forall (r :: * -> *). DBModel Block -> Model r
initModelImpl DBModel Block
dbm
    , transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
Model r -> At CmdErr r -> At Resp r -> Model r
transition = Model r -> At CmdErr r -> At Resp r -> Model r
forall (r :: * -> *).
(Show1 r, Ord1 r) =>
Model r -> At CmdErr r -> At Resp r -> Model r
forall (r :: * -> *).
Model r -> At CmdErr r -> At Resp r -> Model r
transitionImpl
    , precondition :: Model Symbolic -> At CmdErr Symbolic -> Logic
precondition = Model Symbolic -> At CmdErr Symbolic -> Logic
preconditionImpl
    , postcondition :: Model Concrete -> At CmdErr Concrete -> At Resp Concrete -> Logic
postcondition = Model Concrete -> At CmdErr Concrete -> At Resp Concrete -> Logic
postconditionImpl
    , generator :: Model Symbolic -> Maybe (Gen (At CmdErr Symbolic))
generator = Model Symbolic -> Maybe (Gen (At CmdErr Symbolic))
generatorImpl
    , shrinker :: Model Symbolic -> At CmdErr Symbolic -> [At CmdErr Symbolic]
shrinker = Model Symbolic -> At CmdErr Symbolic -> [At CmdErr Symbolic]
shrinkerImpl
    , semantics :: At CmdErr Concrete -> IO (At Resp Concrete)
semantics = VolatileDBEnv -> At CmdErr Concrete -> IO (At Resp Concrete)
semanticsImpl VolatileDBEnv
env
    , mock :: Model Symbolic -> At CmdErr Symbolic -> GenSym (At Resp Symbolic)
mock = Model Symbolic -> At CmdErr Symbolic -> GenSym (At Resp Symbolic)
mockImpl
    , invariant :: Maybe (Model Concrete -> Logic)
invariant = Maybe (Model Concrete -> Logic)
forall a. Maybe a
Nothing
    , cleanup :: Model Concrete -> IO ()
cleanup = Model Concrete -> IO ()
forall (m :: * -> *) (model :: (* -> *) -> *).
Monad m =>
model Concrete -> m ()
noCleanup
    }

initModelImpl :: DBModel Block -> Model r
initModelImpl :: forall (r :: * -> *). DBModel Block -> Model r
initModelImpl = DBModel Block -> Model r
forall (r :: * -> *). DBModel Block -> Model r
Model

transitionImpl :: Model r -> At CmdErr r -> At Resp r -> Model r
transitionImpl :: forall (r :: * -> *).
Model r -> At CmdErr r -> At Resp r -> Model r
transitionImpl Model r
model At CmdErr r
cmd At Resp r
_ = Event r -> Model r
forall (r :: * -> *). Event r -> Model r
eventAfter (Event r -> Model r) -> Event r -> Model r
forall a b. (a -> b) -> a -> b
$ Model r -> At CmdErr r -> Event r
forall (r :: * -> *). Model r -> At CmdErr r -> Event r
lockstep Model r
model At CmdErr r
cmd

preconditionImpl :: Model Symbolic -> At CmdErr Symbolic -> Logic
preconditionImpl :: Model Symbolic -> At CmdErr Symbolic -> Logic
preconditionImpl Model{DBModel Block
dbModel :: forall (r :: * -> *). Model r -> DBModel Block
dbModel :: DBModel Block
..} (At (CmdErr Cmd
cmd Maybe Errors
mbErrors)) =
  Logic
compatibleWithError Logic -> Logic -> Logic
.&& case Cmd
cmd of
    Corruption Corruptions
cors ->
      [FsPath] -> (FsPath -> Logic) -> Logic
forall a. Show a => [a] -> (a -> Logic) -> Logic
forAll (Corruptions -> [FsPath]
corruptionFiles Corruptions
cors) (FsPath -> [FsPath] -> Logic
forall (t :: * -> *) a.
(Foldable t, Eq a, Show a, Show (t a)) =>
a -> t a -> Logic
`member` DBModel Block -> [FsPath]
forall blk. DBModel blk -> [FsPath]
getDBFiles DBModel Block
dbModel)
    -- When duplicating a block by appending it to some other file, make
    -- sure that both the file and the block exists, and that we're adding
    -- it /after/ the original block, so that truncating that the duplicated
    -- block brings us back in the original state.
    DuplicateBlock Int
fileId Block
blk -> case HeaderHash Block -> Maybe Int
fileIdContainingBlock (Block -> HeaderHash Block
forall b. HasHeader b => b -> HeaderHash b
blockHash Block
blk) of
      Maybe Int
Nothing -> Logic
Bot
      Just Int
fileId' -> Int
fileId Int -> Int -> Logic
forall a. (Ord a, Show a) => a -> a -> Logic
.>= Int
fileId'
    Cmd
_ -> Logic
Top
 where
  -- \| Corruption commands are not allowed to have errors.
  compatibleWithError :: Logic
  compatibleWithError :: Logic
compatibleWithError
    | Bool -> Bool
not (Cmd -> Bool
allowErrorFor Cmd
cmd)
    , Just Errors
_ <- Maybe Errors
mbErrors =
        Logic
Bot
    | Bool
otherwise =
        Logic
Top

  fileIdContainingBlock :: HeaderHash Block -> Maybe FileId
  fileIdContainingBlock :: HeaderHash Block -> Maybe Int
fileIdContainingBlock HeaderHash Block
hash =
    [Int] -> Maybe Int
forall a. [a] -> Maybe a
listToMaybe
      [ Int
fileId
      | (Int
fileId, BlocksInFile [Block]
blocks) <- Map Int (BlocksInFile Block) -> [(Int, BlocksInFile Block)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Int (BlocksInFile Block) -> [(Int, BlocksInFile Block)])
-> Map Int (BlocksInFile Block) -> [(Int, BlocksInFile Block)]
forall a b. (a -> b) -> a -> b
$ DBModel Block -> Map Int (BlocksInFile Block)
forall blk. DBModel blk -> Map Int (BlocksInFile blk)
fileIndex DBModel Block
dbModel
      , Block
blk <- [Block]
blocks
      , Block -> HeaderHash Block
forall b. HasHeader b => b -> HeaderHash b
blockHash Block
blk TestHeaderHash -> TestHeaderHash -> Bool
forall a. Eq a => a -> a -> Bool
== HeaderHash Block
TestHeaderHash
hash
      ]

postconditionImpl ::
  Model Concrete ->
  At CmdErr Concrete ->
  At Resp Concrete ->
  Logic
postconditionImpl :: Model Concrete -> At CmdErr Concrete -> At Resp Concrete -> Logic
postconditionImpl Model Concrete
model At CmdErr Concrete
cmdErr At Resp Concrete
resp =
  Model Concrete -> At Resp Concrete -> Resp
forall (r :: * -> *) t. Model r -> At t r -> t
toMock (Event Concrete -> Model Concrete
forall (r :: * -> *). Event r -> Model r
eventAfter Event Concrete
ev) At Resp Concrete
resp Resp -> Resp -> Logic
forall a. (Eq a, Show a) => a -> a -> Logic
.== Event Concrete -> Resp
forall (r :: * -> *). Event r -> Resp
eventMockResp Event Concrete
ev
 where
  ev :: Event Concrete
ev = Model Concrete -> At CmdErr Concrete -> Event Concrete
forall (r :: * -> *). Model r -> At CmdErr r -> Event r
lockstep Model Concrete
model At CmdErr Concrete
cmdErr

generatorCmdImpl :: Model Symbolic -> Gen Cmd
generatorCmdImpl :: Model Symbolic -> Gen Cmd
generatorCmdImpl Model{DBModel Block
dbModel :: forall (r :: * -> *). Model r -> DBModel Block
dbModel :: DBModel Block
..} =
  [(Int, Gen Cmd)] -> Gen Cmd
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
    [ (Int
3, Block -> Cmd
PutBlock (Block -> Cmd) -> Gen Block -> Gen Cmd
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Block
genTestBlock)
    , (Int
1, Cmd -> Gen Cmd
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return Cmd
Close)
    , -- When the DB is closed, we try to reopen it ASAP.
      (if DBModel Block -> Bool
forall blk. DBModel blk -> Bool
open DBModel Block
dbModel then Int
1 else Int
5, Cmd -> Gen Cmd
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return Cmd
ReOpen)
    , (Int
2, HeaderHash Block -> Cmd
TestHeaderHash -> Cmd
GetBlockComponent (TestHeaderHash -> Cmd) -> Gen TestHeaderHash -> Gen Cmd
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (HeaderHash Block)
Gen TestHeaderHash
genHash)
    , (Int
2, SlotNo -> Cmd
GarbageCollect (SlotNo -> Cmd) -> Gen SlotNo -> Gen Cmd
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen SlotNo
genGCSlot)
    , (Int
2, [HeaderHash Block] -> Cmd
[TestHeaderHash] -> Cmd
GetBlockInfo ([TestHeaderHash] -> Cmd) -> Gen [TestHeaderHash] -> Gen Cmd
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen TestHeaderHash -> Gen [TestHeaderHash]
forall a. Gen a -> Gen [a]
listOf Gen (HeaderHash Block)
Gen TestHeaderHash
genHash)
    , (Int
2, [ChainHash Block] -> Cmd
FilterByPredecessor ([ChainHash Block] -> Cmd) -> Gen [ChainHash Block] -> Gen Cmd
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (ChainHash Block) -> Gen [ChainHash Block]
forall a. Gen a -> Gen [a]
listOf Gen (ChainHash Block)
genPrevHash)
    , (Int
2, Cmd -> Gen Cmd
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return Cmd
GetMaxSlotNo)
    ,
      ( if [FsPath] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FsPath]
dbFiles then Int
0 else Int
1
      , Corruptions -> Cmd
Corruption (Corruptions -> Cmd) -> Gen Corruptions -> Gen Cmd
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty FsPath -> Gen Corruptions
generateCorruptions ([FsPath] -> NonEmpty FsPath
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [FsPath]
dbFiles)
      )
    , (if Bool
isEmpty then Int
0 else Int
1, Gen Cmd
genDuplicateBlock)
    ]
 where
  blockIdx :: Map (HeaderHash Block) Block
blockIdx = DBModel Block -> Map (HeaderHash Block) Block
forall blk.
HasHeader blk =>
DBModel blk -> Map (HeaderHash blk) blk
blockIndex DBModel Block
dbModel
  dbFiles :: [FsPath]
dbFiles = DBModel Block -> [FsPath]
forall blk. DBModel blk -> [FsPath]
getDBFiles DBModel Block
dbModel
  isEmpty :: Bool
isEmpty = Map TestHeaderHash Block -> Bool
forall k a. Map k a -> Bool
Map.null Map TestHeaderHash Block
blockIdx
  canContainEBB :: b -> Bool
canContainEBB = Bool -> b -> Bool
forall a b. a -> b -> a
const Bool
True

  getSlot :: HeaderHash Block -> Maybe SlotNo
  getSlot :: HeaderHash Block -> Maybe SlotNo
getSlot HeaderHash Block
hash = Block -> SlotNo
forall b. HasHeader b => b -> SlotNo
blockSlot (Block -> SlotNo) -> Maybe Block -> Maybe SlotNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TestHeaderHash -> Map TestHeaderHash Block -> Maybe Block
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup HeaderHash Block
TestHeaderHash
hash Map TestHeaderHash Block
blockIdx

  genSlotStartingFrom :: SlotNo -> Gen SlotNo
  genSlotStartingFrom :: SlotNo -> Gen SlotNo
genSlotStartingFrom SlotNo
slot = SlotNo -> SlotNo -> Gen SlotNo
chooseSlot SlotNo
slot (SlotNo
slot SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
+ SlotNo
20)

  mbMinMaxSlotInModel :: Maybe (SlotNo, SlotNo)
  mbMinMaxSlotInModel :: Maybe (SlotNo, SlotNo)
mbMinMaxSlotInModel = do
    minSlot <- Block -> SlotNo
forall b. HasHeader b => b -> SlotNo
blockSlot (Block -> SlotNo)
-> ((Block, Map TestHeaderHash Block) -> Block)
-> (Block, Map TestHeaderHash Block)
-> SlotNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Block, Map TestHeaderHash Block) -> Block
forall a b. (a, b) -> a
fst ((Block, Map TestHeaderHash Block) -> SlotNo)
-> Maybe (Block, Map TestHeaderHash Block) -> Maybe SlotNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map TestHeaderHash Block -> Maybe (Block, Map TestHeaderHash Block)
forall k a. Map k a -> Maybe (a, Map k a)
Map.minView Map TestHeaderHash Block
blockIdx
    maxSlot <- blockSlot . fst <$> Map.maxView blockIdx
    return (minSlot, maxSlot)

  -- Blocks don't have to be valid, i.e., they don't have to satisfy the
  -- invariants checked in Mock.Chain and AnchoredFragment, etc. EBBs don't have
  -- to have a particular slot number, etc.
  genTestBlock :: Gen Block
  genTestBlock :: Gen Block
genTestBlock =
    [(Int, Gen Block)] -> Gen Block
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
      [ (Int
4, Gen (HeaderHash Block)
Gen TestHeaderHash
genHash Gen TestHeaderHash -> (TestHeaderHash -> Gen Block) -> Gen Block
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= HeaderHash Block -> Gen Block
TestHeaderHash -> Gen Block
genSuccessor)
      , (Int
1, Gen Block
genRandomBlock)
      ]

  genSuccessor :: HeaderHash Block -> Gen Block
  genSuccessor :: HeaderHash Block -> Gen Block
genSuccessor HeaderHash Block
prevHash = do
    b <- Gen Block
genRandomBlock
    slot <- genSlotStartingFrom $ maybe 0 succ (getSlot prevHash)
    let body = Block -> TestBody
testBody Block
b
        th = Block -> TestHeader
testHeader Block
b
        no = TestHeader -> BlockNo
thBlockNo TestHeader
th
        clen = TestHeader -> ChainLength
thChainLength TestHeader
th
        ebb = Block -> Maybe EpochNo
forall blk. GetHeader blk => blk -> Maybe EpochNo
blockIsEBB Block
b
    return $ mkBlock canContainEBB body (BlockHash prevHash) slot no clen ebb

  genRandomBlock :: Gen Block
  genRandomBlock :: Gen Block
genRandomBlock = do
    body <- Word -> Bool -> TestBody
TestBody (Word -> Bool -> TestBody) -> Gen Word -> Gen (Bool -> TestBody)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Word
forall a. Arbitrary a => Gen a
arbitrary Gen (Bool -> TestBody) -> Gen Bool -> Gen TestBody
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Bool
forall a. Arbitrary a => Gen a
arbitrary
    prevHash <-
      frequency
        [ (1, return GenesisHash)
        , (6, BlockHash . TestHeaderHash <$> arbitrary)
        ]
    slot <- genSlotStartingFrom 0
    -- We don't care about block numbers in the VolatileDB
    no <- BlockNo <$> arbitrary
    -- We don't care about epoch numbers in the VolatileDB
    ebb <- arbitrary
    -- We don't care about chain length in the VolatileDB
    let clen = Int -> ChainLength
ChainLength (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (BlockNo -> Word64
unBlockNo BlockNo
no))
    return $ mkBlock canContainEBB body prevHash slot no clen ebb

  genHash :: Gen (HeaderHash Block)
  genHash :: Gen (HeaderHash Block)
genHash =
    [(Int, Gen TestHeaderHash)] -> Gen TestHeaderHash
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
      [ (if Bool
isEmpty then Int
0 else Int
5, [TestHeaderHash] -> Gen TestHeaderHash
forall a. HasCallStack => [a] -> Gen a
elements ([TestHeaderHash] -> Gen TestHeaderHash)
-> [TestHeaderHash] -> Gen TestHeaderHash
forall a b. (a -> b) -> a -> b
$ Map TestHeaderHash Block -> [TestHeaderHash]
forall k a. Map k a -> [k]
Map.keys Map TestHeaderHash Block
blockIdx)
      , (Int
1, Int -> TestHeaderHash
TestHeaderHash (Int -> TestHeaderHash) -> Gen Int -> Gen TestHeaderHash
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int
forall a. Arbitrary a => Gen a
arbitrary)
      , (Int
4, Block -> HeaderHash Block
Block -> TestHeaderHash
forall b. HasHeader b => b -> HeaderHash b
blockHash (Block -> TestHeaderHash) -> Gen Block -> Gen TestHeaderHash
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Block
genTestBlock)
      ]

  genPrevHash :: Gen (ChainHash Block)
  genPrevHash :: Gen (ChainHash Block)
genPrevHash =
    [(Int, Gen (ChainHash Block))] -> Gen (ChainHash Block)
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
      [ (Int
1, ChainHash Block -> Gen (ChainHash Block)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return ChainHash Block
forall {k} (b :: k). ChainHash b
GenesisHash)
      , (Int
8, HeaderHash Block -> ChainHash Block
TestHeaderHash -> ChainHash Block
forall {k} (b :: k). HeaderHash b -> ChainHash b
BlockHash (TestHeaderHash -> ChainHash Block)
-> Gen TestHeaderHash -> Gen (ChainHash Block)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (HeaderHash Block)
Gen TestHeaderHash
genHash)
      ]

  -- In general, we only want to GC part of the blocks, not all of them
  genGCSlot :: Gen SlotNo
  genGCSlot :: Gen SlotNo
genGCSlot = case Maybe (SlotNo, SlotNo)
mbMinMaxSlotInModel of
    Maybe (SlotNo, SlotNo)
Nothing -> SlotNo -> SlotNo -> Gen SlotNo
chooseSlot SlotNo
0 SlotNo
10
    Just (SlotNo
minSlot, SlotNo
maxSlot) ->
      -- Sometimes GC a slot lower than @minSlot@ and GC a slot higher than
      -- @maxSlot@ (i.e., nothing and everything).
      SlotNo -> SlotNo -> Gen SlotNo
chooseSlot (SlotNo -> SlotNo -> SlotNo
forall a. (Num a, Ord a) => a -> a -> a
subtractNoUnderflow SlotNo
minSlot SlotNo
3) (SlotNo
maxSlot SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
+ SlotNo
3)

  subtractNoUnderflow :: (Num a, Ord a) => a -> a -> a
  subtractNoUnderflow :: forall a. (Num a, Ord a) => a -> a -> a
subtractNoUnderflow a
x a
y
    | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
y = a
x a -> a -> a
forall a. Num a => a -> a -> a
- a
y
    | Bool
otherwise = a
0

  chooseSlot :: SlotNo -> SlotNo -> Gen SlotNo
  chooseSlot :: SlotNo -> SlotNo -> Gen SlotNo
chooseSlot (SlotNo Word64
start) (SlotNo Word64
end) = Word64 -> SlotNo
SlotNo (Word64 -> SlotNo) -> Gen Word64 -> Gen SlotNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
choose (Word64
start, Word64
end)

  genDuplicateBlock :: Gen Cmd
genDuplicateBlock = do
    (originalFileId, blk) <-
      [(Int, Block)] -> Gen (Int, Block)
forall a. HasCallStack => [a] -> Gen a
elements
        [ (Int
fileId, Block
blk)
        | (Int
fileId, BlocksInFile [Block]
blks) <- Map Int (BlocksInFile Block) -> [(Int, BlocksInFile Block)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Int (BlocksInFile Block) -> [(Int, BlocksInFile Block)])
-> Map Int (BlocksInFile Block) -> [(Int, BlocksInFile Block)]
forall a b. (a -> b) -> a -> b
$ DBModel Block -> Map Int (BlocksInFile Block)
forall blk. DBModel blk -> Map Int (BlocksInFile blk)
fileIndex DBModel Block
dbModel
        , Block
blk <- [Block]
blks
        ]
    fileId <- elements (getDBFileIds dbModel) `suchThat` (>= originalFileId)
    return $ DuplicateBlock fileId blk

generatorImpl :: Model Symbolic -> Maybe (Gen (At CmdErr Symbolic))
generatorImpl :: Model Symbolic -> Maybe (Gen (At CmdErr Symbolic))
generatorImpl m :: Model Symbolic
m@Model{DBModel Block
dbModel :: forall (r :: * -> *). Model r -> DBModel Block
dbModel :: DBModel Block
..} = Gen (At CmdErr Symbolic) -> Maybe (Gen (At CmdErr Symbolic))
forall a. a -> Maybe a
Just (Gen (At CmdErr Symbolic) -> Maybe (Gen (At CmdErr Symbolic)))
-> Gen (At CmdErr Symbolic) -> Maybe (Gen (At CmdErr Symbolic))
forall a b. (a -> b) -> a -> b
$ do
  cmd <- Model Symbolic -> Gen Cmd
generatorCmdImpl Model Symbolic
m
  err <-
    frequency
      [ (9, return Nothing)
      ,
        ( if allowErrorFor cmd && open dbModel then 1 else 0
        , -- Don't simulate errors while closed, because they won't have any
          -- effect, but also because we would reopen, which would not be
          -- idempotent.
          Just <$> genErrors True True
        )
      ]
  return $ At $ CmdErr cmd err

allowErrorFor :: Cmd -> Bool
allowErrorFor :: Cmd -> Bool
allowErrorFor Corruption{} = Bool
False
allowErrorFor DuplicateBlock{} = Bool
False
allowErrorFor Cmd
_ = Bool
True

shrinkerImpl :: Model Symbolic -> At CmdErr Symbolic -> [At CmdErr Symbolic]
shrinkerImpl :: Model Symbolic -> At CmdErr Symbolic -> [At CmdErr Symbolic]
shrinkerImpl Model Symbolic
m (At (CmdErr Cmd
cmd Maybe Errors
mbErr)) =
  (CmdErr -> At CmdErr Symbolic) -> [CmdErr] -> [At CmdErr Symbolic]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CmdErr -> At CmdErr Symbolic
forall t (r :: * -> *). t -> At t r
At ([CmdErr] -> [At CmdErr Symbolic])
-> [CmdErr] -> [At CmdErr Symbolic]
forall a b. (a -> b) -> a -> b
$
    [Cmd -> Maybe Errors -> CmdErr
CmdErr Cmd
cmd Maybe Errors
mbErr' | Maybe Errors
mbErr' <- Maybe Errors -> [Maybe Errors]
forall a. Arbitrary a => a -> [a]
shrink Maybe Errors
mbErr]
      [CmdErr] -> [CmdErr] -> [CmdErr]
forall a. [a] -> [a] -> [a]
++ [Cmd -> Maybe Errors -> CmdErr
CmdErr Cmd
cmd' Maybe Errors
mbErr | Cmd
cmd' <- Model Symbolic -> Cmd -> [Cmd]
shrinkCmd Model Symbolic
m Cmd
cmd]

shrinkCmd :: Model Symbolic -> Cmd -> [Cmd]
shrinkCmd :: Model Symbolic -> Cmd -> [Cmd]
shrinkCmd Model Symbolic
_ Cmd
cmd = case Cmd
cmd of
  GetBlockInfo [HeaderHash Block]
bids -> [HeaderHash Block] -> Cmd
[TestHeaderHash] -> Cmd
GetBlockInfo ([TestHeaderHash] -> Cmd) -> [[TestHeaderHash]] -> [Cmd]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TestHeaderHash -> [TestHeaderHash])
-> [TestHeaderHash] -> [[TestHeaderHash]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList ([TestHeaderHash] -> TestHeaderHash -> [TestHeaderHash]
forall a b. a -> b -> a
const []) [HeaderHash Block]
[TestHeaderHash]
bids
  FilterByPredecessor [ChainHash Block]
preds -> [ChainHash Block] -> Cmd
FilterByPredecessor ([ChainHash Block] -> Cmd) -> [[ChainHash Block]] -> [Cmd]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ChainHash Block -> [ChainHash Block])
-> [ChainHash Block] -> [[ChainHash Block]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList ([ChainHash Block] -> ChainHash Block -> [ChainHash Block]
forall a b. a -> b -> a
const []) [ChainHash Block]
preds
  Corruption Corruptions
cors -> Corruptions -> Cmd
Corruption (Corruptions -> Cmd) -> [Corruptions] -> [Cmd]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Corruptions -> [Corruptions]
shrinkCorruptions Corruptions
cors
  Cmd
_ -> []

-- | Environment to run commands against the real VolatileDB implementation.
data VolatileDBEnv = VolatileDBEnv
  { VolatileDBEnv -> StrictTVar IO Errors
varErrors :: StrictTVar IO Errors
  , VolatileDBEnv -> StrictTVar IO (VolatileDB IO Block)
varDB :: StrictTVar IO (VolatileDB IO Block)
  , VolatileDBEnv -> VolatileDbArgs Identity IO Block
args :: VolatileDbArgs Identity IO Block
  }

-- | Opens a new VolatileDB and stores it in 'varDB'.
--
-- Does not close the current VolatileDB stored in 'varDB'.
reopenDB :: VolatileDBEnv -> IO ()
reopenDB :: VolatileDBEnv -> IO ()
reopenDB VolatileDBEnv{StrictTVar IO (VolatileDB IO Block)
varDB :: VolatileDBEnv -> StrictTVar IO (VolatileDB IO Block)
varDB :: StrictTVar IO (VolatileDB IO Block)
varDB, VolatileDbArgs Identity IO Block
args :: VolatileDBEnv -> VolatileDbArgs Identity IO Block
args :: VolatileDbArgs Identity IO Block
args} = do
  db <- VolatileDbArgs Identity IO Block
-> (forall st.
    WithTempRegistry st IO (VolatileDB IO Block, st)
    -> IO (VolatileDB IO Block))
-> IO (VolatileDB IO Block)
forall (m :: * -> *) blk ans.
(HasCallStack, IOLike m, GetPrevHash blk,
 VolatileDbSerialiseConstraints blk) =>
Complete VolatileDbArgs m blk
-> (forall st. WithTempRegistry st m (VolatileDB m blk, st) -> ans)
-> ans
openDB VolatileDbArgs Identity IO Block
args WithTempRegistry st IO (VolatileDB IO Block, st)
-> IO (VolatileDB IO Block)
forall st.
WithTempRegistry st IO (VolatileDB IO Block, st)
-> IO (VolatileDB IO Block)
forall (m :: * -> *) st a.
(MonadSTM m, MonadMask m, MonadThread m, HasCallStack) =>
WithTempRegistry st m (a, st) -> m a
runWithTempRegistry
  void $ atomically $ swapTVar varDB db

semanticsImpl :: VolatileDBEnv -> At CmdErr Concrete -> IO (At Resp Concrete)
semanticsImpl :: VolatileDBEnv -> At CmdErr Concrete -> IO (At Resp Concrete)
semanticsImpl env :: VolatileDBEnv
env@VolatileDBEnv{StrictTVar IO (VolatileDB IO Block)
varDB :: VolatileDBEnv -> StrictTVar IO (VolatileDB IO Block)
varDB :: StrictTVar IO (VolatileDB IO Block)
varDB, StrictTVar IO Errors
varErrors :: VolatileDBEnv -> StrictTVar IO Errors
varErrors :: StrictTVar IO Errors
varErrors} (At (CmdErr Cmd
cmd Maybe Errors
mbErrors)) =
  Resp -> At Resp Concrete
forall t (r :: * -> *). t -> At t r
At (Resp -> At Resp Concrete)
-> (Either (VolatileDBError Block) Success -> Resp)
-> Either (VolatileDBError Block) Success
-> At Resp Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either (VolatileDBError Block) Success -> Resp
Resp (Either (VolatileDBError Block) Success -> At Resp Concrete)
-> IO (Either (VolatileDBError Block) Success)
-> IO (At Resp Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case Maybe Errors
mbErrors of
    Maybe Errors
Nothing -> Proxy Block
-> IO Success -> IO (Either (VolatileDBError Block) Success)
forall (m :: * -> *) a blk.
(MonadCatch m, Typeable blk, StandardHash blk) =>
Proxy blk -> m a -> m (Either (VolatileDBError blk) a)
tryVolatileDB (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Block) (HasCallStack => VolatileDBEnv -> Cmd -> IO Success
VolatileDBEnv -> Cmd -> IO Success
runDB VolatileDBEnv
env Cmd
cmd)
    Just Errors
errors -> do
      _ <-
        StrictTVar IO Errors
-> Errors
-> IO (Either (VolatileDBError Block) Success)
-> IO (Either (VolatileDBError Block) Success)
forall (m :: * -> *) a.
MonadSTM m =>
StrictTVar m Errors -> Errors -> m a -> m a
withErrors (StrictTVar IO Errors -> StrictTVar IO Errors
forall (m :: * -> *) a. StrictTVar m a -> StrictTVar m a
unsafeToUncheckedStrictTVar StrictTVar IO Errors
varErrors) Errors
errors (IO (Either (VolatileDBError Block) Success)
 -> IO (Either (VolatileDBError Block) Success))
-> IO (Either (VolatileDBError Block) Success)
-> IO (Either (VolatileDBError Block) Success)
forall a b. (a -> b) -> a -> b
$
          Proxy Block
-> IO Success -> IO (Either (VolatileDBError Block) Success)
forall (m :: * -> *) a blk.
(MonadCatch m, Typeable blk, StandardHash blk) =>
Proxy blk -> m a -> m (Either (VolatileDBError blk) a)
tryVolatileDB (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Block) (HasCallStack => VolatileDBEnv -> Cmd -> IO Success
VolatileDBEnv -> Cmd -> IO Success
runDB VolatileDBEnv
env Cmd
cmd)
      -- As all operations on the VolatileDB are idempotent, close (not
      -- idempotent by default!), reopen it, and run the command again.
      readTVarIO varDB >>= idemPotentCloseDB
      reopenDB env
      tryVolatileDB (Proxy @Block) (runDB env cmd)

idemPotentCloseDB :: VolatileDB IO Block -> IO ()
idemPotentCloseDB :: VolatileDB IO Block -> IO ()
idemPotentCloseDB VolatileDB IO Block
db =
  (VolatileDBError Block -> Maybe ())
-> IO () -> (() -> IO ()) -> IO ()
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> (b -> IO a) -> IO a
forall (m :: * -> *) e b a.
(MonadCatch m, Exception e) =>
(e -> Maybe b) -> m a -> (b -> m a) -> m a
catchJust
    VolatileDBError Block -> Maybe ()
isClosedDBError
    (VolatileDB IO Block -> HasCallStack => IO ()
forall (m :: * -> *) blk. VolatileDB m blk -> HasCallStack => m ()
closeDB VolatileDB IO Block
db)
    (IO () -> () -> IO ()
forall a b. a -> b -> a
const (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()))
 where
  isClosedDBError :: VolatileDBError Block -> Maybe ()
  isClosedDBError :: VolatileDBError Block -> Maybe ()
isClosedDBError (ApiMisuse (ClosedDBError Maybe SomeException
_)) = () -> Maybe ()
forall a. a -> Maybe a
Just ()
  isClosedDBError VolatileDBError Block
_ = Maybe ()
forall a. Maybe a
Nothing

runDB :: HasCallStack => VolatileDBEnv -> Cmd -> IO Success
runDB :: HasCallStack => VolatileDBEnv -> Cmd -> IO Success
runDB env :: VolatileDBEnv
env@VolatileDBEnv{StrictTVar IO (VolatileDB IO Block)
varDB :: VolatileDBEnv -> StrictTVar IO (VolatileDB IO Block)
varDB :: StrictTVar IO (VolatileDB IO Block)
varDB, args :: VolatileDBEnv -> VolatileDbArgs Identity IO Block
args = VolatileDbArgs{volHasFS :: forall (f :: * -> *) (m :: * -> *) blk.
VolatileDbArgs f m blk -> HKD f (SomeHasFS m)
volHasFS = SomeHasFS HasFS IO h
hasFS}} Cmd
cmd =
  StrictTVar IO (VolatileDB IO Block) -> IO (VolatileDB IO Block)
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> m a
readTVarIO StrictTVar IO (VolatileDB IO Block)
varDB IO (VolatileDB IO Block)
-> (VolatileDB IO Block -> IO Success) -> IO Success
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \VolatileDB IO Block
db -> case Cmd
cmd of
    GetBlockComponent HeaderHash Block
hash -> Maybe (AllComponents Block) -> Success
Maybe
  (Block, Block, ByteString, Header Block, ByteString,
   TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
   SomeSecond (NestedCtxt Header) Block)
-> Success
MbAllComponents (Maybe
   (Block, Block, ByteString, Header Block, ByteString,
    TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
    SomeSecond (NestedCtxt Header) Block)
 -> Success)
-> IO
     (Maybe
        (Block, Block, ByteString, Header Block, ByteString,
         TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
         SomeSecond (NestedCtxt Header) Block))
-> IO Success
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VolatileDB IO Block
-> forall b.
   HasCallStack =>
   BlockComponent Block b -> HeaderHash Block -> IO (Maybe b)
forall (m :: * -> *) blk.
VolatileDB m blk
-> forall b.
   HasCallStack =>
   BlockComponent blk b -> HeaderHash blk -> m (Maybe b)
getBlockComponent VolatileDB IO Block
db BlockComponent Block (AllComponents Block)
BlockComponent
  Block
  (Block, Block, ByteString, Header Block, ByteString,
   TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
   SomeSecond (NestedCtxt Header) Block)
forall blk. BlockComponent blk (AllComponents blk)
allComponents HeaderHash Block
hash
    PutBlock Block
blk -> () -> Success
Unit (() -> Success) -> IO () -> IO Success
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VolatileDB IO Block -> HasCallStack => Block -> IO ()
forall (m :: * -> *) blk.
VolatileDB m blk -> HasCallStack => blk -> m ()
putBlock VolatileDB IO Block
db Block
blk
    FilterByPredecessor [ChainHash Block]
hashes -> [Set (HeaderHash Block)] -> Success
[Set TestHeaderHash] -> Success
Successors ([Set TestHeaderHash] -> Success)
-> ((ChainHash Block -> Set TestHeaderHash)
    -> [Set TestHeaderHash])
-> (ChainHash Block -> Set TestHeaderHash)
-> Success
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ChainHash Block -> Set TestHeaderHash)
-> [ChainHash Block] -> [Set TestHeaderHash]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ChainHash Block]
hashes) ((ChainHash Block -> Set TestHeaderHash) -> Success)
-> IO (ChainHash Block -> Set TestHeaderHash) -> IO Success
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STM IO (ChainHash Block -> Set TestHeaderHash)
-> IO (ChainHash Block -> Set TestHeaderHash)
forall a. HasCallStack => STM IO a -> IO a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (VolatileDB IO Block
-> HasCallStack =>
   STM IO (ChainHash Block -> Set (HeaderHash Block))
forall (m :: * -> *) blk.
VolatileDB m blk
-> HasCallStack => STM m (ChainHash blk -> Set (HeaderHash blk))
filterByPredecessor VolatileDB IO Block
db)
    GetBlockInfo [HeaderHash Block]
hashes -> [Maybe (BlockInfo Block)] -> Success
BlockInfos ([Maybe (BlockInfo Block)] -> Success)
-> ((TestHeaderHash -> Maybe (BlockInfo Block))
    -> [Maybe (BlockInfo Block)])
-> (TestHeaderHash -> Maybe (BlockInfo Block))
-> Success
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((HeaderHash Block -> Maybe (BlockInfo Block))
-> [HeaderHash Block] -> [Maybe (BlockInfo Block)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [HeaderHash Block]
hashes) ((TestHeaderHash -> Maybe (BlockInfo Block)) -> Success)
-> IO (TestHeaderHash -> Maybe (BlockInfo Block)) -> IO Success
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STM IO (TestHeaderHash -> Maybe (BlockInfo Block))
-> IO (TestHeaderHash -> Maybe (BlockInfo Block))
forall a. HasCallStack => STM IO a -> IO a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (VolatileDB IO Block
-> HasCallStack =>
   STM IO (HeaderHash Block -> Maybe (BlockInfo Block))
forall (m :: * -> *) blk.
VolatileDB m blk
-> HasCallStack => STM m (HeaderHash blk -> Maybe (BlockInfo blk))
getBlockInfo VolatileDB IO Block
db)
    GarbageCollect SlotNo
slot -> () -> Success
Unit (() -> Success) -> IO () -> IO Success
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VolatileDB IO Block -> HasCallStack => SlotNo -> IO ()
forall (m :: * -> *) blk.
VolatileDB m blk -> HasCallStack => SlotNo -> m ()
garbageCollect VolatileDB IO Block
db SlotNo
slot
    Cmd
GetMaxSlotNo -> MaxSlotNo -> Success
MaxSlot (MaxSlotNo -> Success) -> IO MaxSlotNo -> IO Success
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STM IO MaxSlotNo -> IO MaxSlotNo
forall a. HasCallStack => STM IO a -> IO a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (VolatileDB IO Block -> HasCallStack => STM IO MaxSlotNo
forall (m :: * -> *) blk.
VolatileDB m blk -> HasCallStack => STM m MaxSlotNo
getMaxSlotNo VolatileDB IO Block
db)
    Cmd
Close -> () -> Success
Unit (() -> Success) -> IO () -> IO Success
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VolatileDB IO Block -> HasCallStack => IO ()
forall (m :: * -> *) blk. VolatileDB m blk -> HasCallStack => m ()
closeDB VolatileDB IO Block
db
    Cmd
ReOpen -> do
      StrictTVar IO (VolatileDB IO Block) -> IO (VolatileDB IO Block)
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> m a
readTVarIO StrictTVar IO (VolatileDB IO Block)
varDB IO (VolatileDB IO Block) -> (VolatileDB IO Block -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= VolatileDB IO Block -> IO ()
idemPotentCloseDB
      () -> Success
Unit (() -> Success) -> IO () -> IO Success
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VolatileDBEnv -> IO ()
reopenDB VolatileDBEnv
env
    Corruption Corruptions
corrs ->
      IO () -> IO Success
withClosedDB (IO () -> IO Success) -> IO () -> IO Success
forall a b. (a -> b) -> a -> b
$
        Corruptions -> ((FileCorruption, FsPath) -> IO Bool) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Corruptions
corrs (((FileCorruption, FsPath) -> IO Bool) -> IO ())
-> ((FileCorruption, FsPath) -> IO Bool) -> IO ()
forall a b. (a -> b) -> a -> b
$
          \(FileCorruption
corr, FsPath
file) -> HasFS IO h -> FileCorruption -> FsPath -> IO Bool
forall (m :: * -> *) h.
MonadThrow m =>
HasFS m h -> FileCorruption -> FsPath -> m Bool
corruptFile HasFS IO h
hasFS FileCorruption
corr FsPath
file
    DuplicateBlock Int
fileId Block
blk -> do
      IO () -> IO Success
withClosedDB (IO () -> IO Success) -> IO () -> IO Success
forall a b. (a -> b) -> a -> b
$
        HasFS IO h -> FsPath -> OpenMode -> (Handle h -> IO ()) -> IO ()
forall (m :: * -> *) h a.
(HasCallStack, MonadThrow m) =>
HasFS m h -> FsPath -> OpenMode -> (Handle h -> m a) -> m a
withFile HasFS IO h
hasFS (Int -> FsPath
filePath Int
fileId) (AllowExisting -> OpenMode
AppendMode AllowExisting
AllowExisting) ((Handle h -> IO ()) -> IO ()) -> (Handle h -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Handle h
hndl ->
          IO Word64 -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO Word64 -> IO ()) -> IO Word64 -> IO ()
forall a b. (a -> b) -> a -> b
$ HasFS IO h -> Handle h -> ByteString -> IO Word64
forall (m :: * -> *) h.
(HasCallStack, Monad m) =>
HasFS m h -> Handle h -> ByteString -> m Word64
hPutAll HasFS IO h
hasFS Handle h
hndl (Block -> ByteString
testBlockToLazyByteString Block
blk)
 where
  withClosedDB :: IO () -> IO Success
  withClosedDB :: IO () -> IO Success
withClosedDB IO ()
action = do
    StrictTVar IO (VolatileDB IO Block) -> IO (VolatileDB IO Block)
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> m a
readTVarIO StrictTVar IO (VolatileDB IO Block)
varDB IO (VolatileDB IO Block) -> (VolatileDB IO Block -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= VolatileDB IO Block -> IO ()
VolatileDB IO Block -> HasCallStack => IO ()
forall (m :: * -> *) blk. VolatileDB m blk -> HasCallStack => m ()
closeDB
    IO ()
action
    VolatileDBEnv -> IO ()
reopenDB VolatileDBEnv
env
    Success -> IO Success
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Success -> IO Success) -> Success -> IO Success
forall a b. (a -> b) -> a -> b
$ () -> Success
Unit ()

mockImpl :: Model Symbolic -> At CmdErr Symbolic -> GenSym (At Resp Symbolic)
mockImpl :: Model Symbolic -> At CmdErr Symbolic -> GenSym (At Resp Symbolic)
mockImpl Model Symbolic
model At CmdErr Symbolic
cmdErr = Resp -> At Resp Symbolic
forall t (r :: * -> *). t -> At t r
At (Resp -> At Resp Symbolic)
-> GenSym Resp -> GenSym (At Resp Symbolic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Resp -> GenSym Resp
forall a. a -> GenSym a
forall (m :: * -> *) a. Monad m => a -> m a
return Resp
mockResp
 where
  (Resp
mockResp, DBModel Block
_dbModel') = Model Symbolic -> At CmdErr Symbolic -> (Resp, DBModel Block)
forall (r :: * -> *).
Model r -> At CmdErr r -> (Resp, DBModel Block)
step Model Symbolic
model At CmdErr Symbolic
cmdErr

prop_sequential :: Property
prop_sequential :: Property
prop_sequential = StateMachine Model (At CmdErr) IO (At Resp)
-> Maybe Int
-> (Commands (At CmdErr) (At Resp) -> Property)
-> Property
forall prop (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
       (model :: (* -> *) -> *) (m :: * -> *).
(Testable prop, Show (cmd Symbolic), Show (resp Symbolic),
 Show (model Symbolic), Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> Maybe Int -> (Commands cmd resp -> prop) -> Property
forAllCommands StateMachine Model (At CmdErr) IO (At Resp)
smUnused Maybe Int
forall a. Maybe a
Nothing ((Commands (At CmdErr) (At Resp) -> Property) -> Property)
-> (Commands (At CmdErr) (At Resp) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Commands (At CmdErr) (At Resp)
cmds -> PropertyM IO () -> Property
forall a. Testable a => PropertyM IO a -> Property
monadicIO (PropertyM IO () -> Property) -> PropertyM IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  (hist, prop) <- IO (History (At CmdErr) (At Resp), Property)
-> PropertyM IO (History (At CmdErr) (At Resp), Property)
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (IO (History (At CmdErr) (At Resp), Property)
 -> PropertyM IO (History (At CmdErr) (At Resp), Property))
-> IO (History (At CmdErr) (At Resp), Property)
-> PropertyM IO (History (At CmdErr) (At Resp), Property)
forall a b. (a -> b) -> a -> b
$ Commands (At CmdErr) (At Resp)
-> IO (History (At CmdErr) (At Resp), Property)
test Commands (At CmdErr) (At Resp)
cmds
  let events = Model Symbolic
-> Commands (At CmdErr) (At Resp) -> [Event Symbolic]
execCmds (StateMachine Model (At CmdErr) IO (At Resp)
-> forall {r :: * -> *}. Model r
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel StateMachine Model (At CmdErr) IO (At Resp)
smUnused) Commands (At CmdErr) (At Resp)
cmds
  prettyCommands smUnused hist
    $ tabulate
      "Tags"
      (map show $ tag events)
    $ tabulate
      "Commands"
      (cmdName . eventCmd <$> events)
    $ tabulate
      "Error Tags"
      (tagSimulatedErrors events)
    $ tabulate
      "GetBlockInfo: total number of Just's"
      [groupIsMember $ isMemberTrue events]
    $ tabulate
      "Successors"
      (tagFilterByPredecessor events)
    $ prop
 where
  dbm :: DBModel Block
dbm = BlocksPerFile -> CodecConfig Block -> DBModel Block
forall blk. BlocksPerFile -> CodecConfig blk -> DBModel blk
initDBModel BlocksPerFile
testMaxBlocksPerFile CodecConfig Block
TestBlockCodecConfig
  smUnused :: StateMachine Model (At CmdErr) IO (At Resp)
smUnused = VolatileDBEnv
-> DBModel Block -> StateMachine Model (At CmdErr) IO (At Resp)
sm VolatileDBEnv
unusedEnv DBModel Block
dbm

  groupIsMember :: a -> String
groupIsMember a
n
    | a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
5 = a -> String
forall a. Show a => a -> String
show a
n
    | a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
20 = String
"5-19"
    | a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
100 = String
"20-99"
    | Bool
otherwise = String
">=100"

test ::
  Commands (At CmdErr) (At Resp) ->
  IO (History (At CmdErr) (At Resp), Property)
test :: Commands (At CmdErr) (At Resp)
-> IO (History (At CmdErr) (At Resp), Property)
test Commands (At CmdErr) (At Resp)
cmds = do
  varErrors <- Errors -> IO (StrictTVar IO Errors)
forall (m :: * -> *) a. MonadSTM m => a -> m (StrictTVar m a)
uncheckedNewTVarM Errors
emptyErrors
  varFs <- atomically $ newTMVar Mock.empty
  (tracer, getTrace) <- recordingTracerIORef

  let hasFS = StrictTMVar IO MockFS
-> StrictTVar IO Errors -> HasFS IO HandleMock
forall (m :: * -> *).
(MonadSTM m, MonadThrow m, PrimMonad m) =>
StrictTMVar m MockFS -> StrictTVar m Errors -> HasFS m HandleMock
simErrorHasFS StrictTMVar IO MockFS
varFs (StrictTVar IO Errors -> StrictTVar IO Errors
forall (m :: * -> *) a. StrictTVar m a -> StrictTVar m a
unsafeToUncheckedStrictTVar StrictTVar IO Errors
varErrors)
      args =
        VolatileDbArgs
          { volCheckIntegrity :: HKD Identity (Block -> Bool)
volCheckIntegrity = HKD Identity (Block -> Bool)
Block -> Bool
testBlockIsValid
          , volCodecConfig :: HKD Identity (CodecConfig Block)
volCodecConfig = HKD Identity (CodecConfig Block)
CodecConfig Block
TestBlockCodecConfig
          , volHasFS :: HKD Identity (SomeHasFS IO)
volHasFS = HasFS IO HandleMock -> SomeHasFS IO
forall h (m :: * -> *). Eq h => HasFS m h -> SomeHasFS m
SomeHasFS HasFS IO HandleMock
hasFS
          , volMaxBlocksPerFile :: BlocksPerFile
volMaxBlocksPerFile = BlocksPerFile
testMaxBlocksPerFile
          , volTracer :: Tracer IO (TraceEvent Block)
volTracer = Tracer IO (TraceEvent Block)
tracer
          , volValidationPolicy :: BlockValidationPolicy
volValidationPolicy = BlockValidationPolicy
ValidateAll
          }

  (hist, res, trace) <- bracket
    (openDB args runWithTempRegistry >>= newTVarIO)
    -- Note: we might be closing a different VolatileDB than the one we
    -- opened, as we can reopen it the VolatileDB, swapping the VolatileDB
    -- in the TVar.
    (\StrictTVar IO (VolatileDB IO Block)
varDB -> StrictTVar IO (VolatileDB IO Block) -> IO (VolatileDB IO Block)
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> m a
readTVarIO StrictTVar IO (VolatileDB IO Block)
varDB IO (VolatileDB IO Block) -> (VolatileDB IO Block -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= VolatileDB IO Block -> IO ()
VolatileDB IO Block -> HasCallStack => IO ()
forall (m :: * -> *) blk. VolatileDB m blk -> HasCallStack => m ()
closeDB)
    $ \StrictTVar IO (VolatileDB IO Block)
varDB -> do
      let env :: VolatileDBEnv
env = VolatileDBEnv{StrictTVar IO Errors
varErrors :: StrictTVar IO Errors
varErrors :: StrictTVar IO Errors
varErrors, StrictTVar IO (VolatileDB IO Block)
varDB :: StrictTVar IO (VolatileDB IO Block)
varDB :: StrictTVar IO (VolatileDB IO Block)
varDB, VolatileDbArgs Identity IO Block
args :: VolatileDbArgs Identity IO Block
args :: VolatileDbArgs Identity IO Block
args}
          sm' :: StateMachine Model (At CmdErr) IO (At Resp)
sm' = VolatileDBEnv
-> DBModel Block -> StateMachine Model (At CmdErr) IO (At Resp)
sm VolatileDBEnv
env DBModel Block
dbm
      (hist, _model, res) <- StateMachine Model (At CmdErr) IO (At Resp)
-> Commands (At CmdErr) (At Resp)
-> IO (History (At CmdErr) (At Resp), Model Concrete, Reason)
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadIO m) =>
StateMachine model cmd m resp
-> Commands cmd resp
-> m (History cmd resp, model Concrete, Reason)
QSM.runCommands' StateMachine Model (At CmdErr) IO (At Resp)
sm' Commands (At CmdErr) (At Resp)
cmds
      trace <- getTrace
      return (hist, res, trace)

  fs <- atomically $ readTMVar varFs

  let prop =
        String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Trace: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> [String] -> String
unlines ((TraceEvent Block -> String) -> [TraceEvent Block] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TraceEvent Block -> String
forall a. Show a => a -> String
show [TraceEvent Block]
trace)) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"FS: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> MockFS -> String
Mock.pretty MockFS
fs) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
            Reason
res Reason -> Reason -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Reason
Ok
  return (hist, prop)
 where
  dbm :: DBModel Block
dbm = BlocksPerFile -> CodecConfig Block -> DBModel Block
forall blk. BlocksPerFile -> CodecConfig blk -> DBModel blk
initDBModel BlocksPerFile
testMaxBlocksPerFile CodecConfig Block
TestBlockCodecConfig

testMaxBlocksPerFile :: BlocksPerFile
testMaxBlocksPerFile :: BlocksPerFile
testMaxBlocksPerFile = Word32 -> BlocksPerFile
mkBlocksPerFile Word32
3

unusedEnv :: VolatileDBEnv
unusedEnv :: VolatileDBEnv
unusedEnv = String -> VolatileDBEnv
forall a. HasCallStack => String -> a
error String
"VolatileDBEnv used during command generation"

tests :: TestTree
tests :: TestTree
tests =
  String -> [TestTree] -> TestTree
testGroup
    String
"VolatileDB q-s-m"
    [ String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty String
"sequential" Property
prop_sequential
    ]

{-------------------------------------------------------------------------------
  Labelling
-------------------------------------------------------------------------------}

-- | Predicate on events
type EventPred = C.Predicate (Event Symbolic) Tag

-- | Convenience combinator for creating classifiers for successful commands
successful ::
  ( Event Symbolic ->
    Success ->
    Either Tag EventPred
  ) ->
  EventPred
successful :: (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
successful Event Symbolic -> Success -> Either Tag EventPred
f = (Event Symbolic -> Either Tag EventPred) -> EventPred
forall a b. (a -> Either b (Predicate a b)) -> Predicate a b
C.predicate ((Event Symbolic -> Either Tag EventPred) -> EventPred)
-> (Event Symbolic -> Either Tag EventPred) -> EventPred
forall a b. (a -> b) -> a -> b
$ \Event Symbolic
ev -> case (Event Symbolic -> Resp
forall (r :: * -> *). Event r -> Resp
eventMockResp Event Symbolic
ev, Event Symbolic -> At CmdErr Symbolic
forall (r :: * -> *). Event r -> At CmdErr r
eventCmd Event Symbolic
ev) of
  (Resp (Right Success
ok), At (CmdErr Cmd
_ Maybe Errors
Nothing)) -> Event Symbolic -> Success -> Either Tag EventPred
f Event Symbolic
ev Success
ok
  (Resp, At CmdErr Symbolic)
_ -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
successful Event Symbolic -> Success -> Either Tag EventPred
f

-- | Tag commands
--
-- Tagging works on symbolic events, so that we can tag without doing real IO.
tag :: [Event Symbolic] -> [Tag]
tag :: [Event Symbolic] -> [Tag]
tag [] = [Tag
TagEmpty]
tag [Event Symbolic]
ls =
  [EventPred] -> [Event Symbolic] -> [Tag]
forall a b. [Predicate a b] -> [a] -> [b]
C.classify
    [ EventPred
tagGetBlockComponentNothing
    , Either Tag EventPred -> EventPred
tagGetJust (Either Tag EventPred -> EventPred)
-> Either Tag EventPred -> EventPred
forall a b. (a -> b) -> a -> b
$ Tag -> Either Tag EventPred
forall a b. a -> Either a b
Left Tag
TagGetJust
    , EventPred
tagGetReOpenGet
    , EventPred
tagReOpenJust
    , Bool -> Set (HeaderHash Block) -> Maybe SlotNo -> EventPred
tagGarbageCollect Bool
True Set (HeaderHash Block)
Set TestHeaderHash
forall a. Set a
Set.empty Maybe SlotNo
forall a. Maybe a
Nothing
    , EventPred
tagCorruptWriteFile
    , EventPred
tagIsClosedError
    , EventPred
tagGarbageCollectThenReOpen
    ]
    [Event Symbolic]
ls
 where
  tagGetBlockComponentNothing :: EventPred
  tagGetBlockComponentNothing :: EventPred
tagGetBlockComponentNothing = (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
successful ((Event Symbolic -> Success -> Either Tag EventPred) -> EventPred)
-> (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
forall a b. (a -> b) -> a -> b
$ \Event Symbolic
ev Success
r -> case Success
r of
    MbAllComponents Maybe (AllComponents Block)
Nothing
      | GetBlockComponent{} <- Event Symbolic -> Cmd
forall (r :: * -> *). Event r -> Cmd
getCmd Event Symbolic
ev ->
          Tag -> Either Tag EventPred
forall a b. a -> Either a b
Left Tag
TagGetNothing
    Success
_ -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right EventPred
tagGetBlockComponentNothing

  tagReOpenJust :: EventPred
  tagReOpenJust :: EventPred
tagReOpenJust = Bool -> Either Tag EventPred -> EventPred
tagReOpen Bool
False (Either Tag EventPred -> EventPred)
-> Either Tag EventPred -> EventPred
forall a b. (a -> b) -> a -> b
$ EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Either Tag EventPred -> EventPred
tagGetJust (Either Tag EventPred -> EventPred)
-> Either Tag EventPred -> EventPred
forall a b. (a -> b) -> a -> b
$ Tag -> Either Tag EventPred
forall a b. a -> Either a b
Left Tag
TagReOpenGet

  tagGetReOpenGet :: EventPred
  tagGetReOpenGet :: EventPred
tagGetReOpenGet =
    Either Tag EventPred -> EventPred
tagGetJust (Either Tag EventPred -> EventPred)
-> Either Tag EventPred -> EventPred
forall a b. (a -> b) -> a -> b
$
      EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$
        Bool -> Either Tag EventPred -> EventPred
tagReOpen Bool
False (Either Tag EventPred -> EventPred)
-> Either Tag EventPred -> EventPred
forall a b. (a -> b) -> a -> b
$
          EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$
            Either Tag EventPred -> EventPred
tagGetJust (Either Tag EventPred -> EventPred)
-> Either Tag EventPred -> EventPred
forall a b. (a -> b) -> a -> b
$
              Tag -> Either Tag EventPred
forall a b. a -> Either a b
Left Tag
TagGetReOpenGet

  -- This rarely succeeds. I think this is because the last part
  -- (get -> Nothing) rarely succeeds. This happens because when a blockId is
  -- deleted is very unlikely to be requested.
  tagGarbageCollect ::
    Bool ->
    Set (HeaderHash Block) ->
    Maybe SlotNo ->
    EventPred
  tagGarbageCollect :: Bool -> Set (HeaderHash Block) -> Maybe SlotNo -> EventPred
tagGarbageCollect Bool
keep Set (HeaderHash Block)
bids Maybe SlotNo
mbGCed = (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
successful ((Event Symbolic -> Success -> Either Tag EventPred) -> EventPred)
-> (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
forall a b. (a -> b) -> a -> b
$ \Event Symbolic
ev Success
suc ->
    if Bool -> Bool
not Bool
keep
      then EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Bool -> Set (HeaderHash Block) -> Maybe SlotNo -> EventPred
tagGarbageCollect Bool
keep Set (HeaderHash Block)
bids Maybe SlotNo
mbGCed
      else case (Maybe SlotNo
mbGCed, Success
suc, Event Symbolic -> Cmd
forall (r :: * -> *). Event r -> Cmd
getCmd Event Symbolic
ev) of
        (Maybe SlotNo
Nothing, Success
_, PutBlock TestBlock{testHeader :: Block -> TestHeader
testHeader = TestHeader{BlockNo
SlotNo
ChainHash TestHeader
HeaderHash TestHeader
ChainLength
EBB
TestBodyHash
thBlockNo :: TestHeader -> BlockNo
thChainLength :: TestHeader -> ChainLength
thHash :: HeaderHash TestHeader
thPrevHash :: ChainHash TestHeader
thBodyHash :: TestBodyHash
thSlotNo :: SlotNo
thBlockNo :: BlockNo
thChainLength :: ChainLength
thIsEBB :: EBB
thIsEBB :: TestHeader -> EBB
thSlotNo :: TestHeader -> SlotNo
thBodyHash :: TestHeader -> TestBodyHash
thPrevHash :: TestHeader -> ChainHash TestHeader
thHash :: TestHeader -> HeaderHash TestHeader
..}}) ->
          EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$
            Bool -> Set (HeaderHash Block) -> Maybe SlotNo -> EventPred
tagGarbageCollect
              Bool
True
              (TestHeaderHash -> Set TestHeaderHash -> Set TestHeaderHash
forall a. Ord a => a -> Set a -> Set a
Set.insert HeaderHash TestHeader
TestHeaderHash
thHash Set (HeaderHash Block)
Set TestHeaderHash
bids)
              Maybe SlotNo
forall a. Maybe a
Nothing
        (Maybe SlotNo
Nothing, Success
_, GarbageCollect SlotNo
sl) ->
          EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Bool -> Set (HeaderHash Block) -> Maybe SlotNo -> EventPred
tagGarbageCollect Bool
True Set (HeaderHash Block)
bids (SlotNo -> Maybe SlotNo
forall a. a -> Maybe a
Just SlotNo
sl)
        (Just SlotNo
_gced, MbAllComponents Maybe (AllComponents Block)
Nothing, GetBlockComponent HeaderHash Block
bid)
          | (TestHeaderHash -> Set TestHeaderHash -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member HeaderHash Block
TestHeaderHash
bid Set (HeaderHash Block)
Set TestHeaderHash
bids) ->
              Tag -> Either Tag EventPred
forall a b. a -> Either a b
Left Tag
TagGarbageCollect
        (Maybe SlotNo
_, Success
_, Corruption Corruptions
_) ->
          EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Bool -> Set (HeaderHash Block) -> Maybe SlotNo -> EventPred
tagGarbageCollect Bool
False Set (HeaderHash Block)
bids Maybe SlotNo
mbGCed
        (Maybe SlotNo, Success, Cmd)
_ -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Bool -> Set (HeaderHash Block) -> Maybe SlotNo -> EventPred
tagGarbageCollect Bool
True Set (HeaderHash Block)
bids Maybe SlotNo
mbGCed

  tagGetJust :: Either Tag EventPred -> EventPred
  tagGetJust :: Either Tag EventPred -> EventPred
tagGetJust Either Tag EventPred
next = (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
successful ((Event Symbolic -> Success -> Either Tag EventPred) -> EventPred)
-> (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
forall a b. (a -> b) -> a -> b
$ \Event Symbolic
_ev Success
suc -> case Success
suc of
    MbAllComponents (Just AllComponents Block
_) -> Either Tag EventPred
next
    Success
_ -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Either Tag EventPred -> EventPred
tagGetJust Either Tag EventPred
next

  tagReOpen :: Bool -> Either Tag EventPred -> EventPred
  tagReOpen :: Bool -> Either Tag EventPred -> EventPred
tagReOpen Bool
hasClosed Either Tag EventPred
next = (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
successful ((Event Symbolic -> Success -> Either Tag EventPred) -> EventPred)
-> (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
forall a b. (a -> b) -> a -> b
$ \Event Symbolic
ev Success
_ ->
    case (Bool
hasClosed, Event Symbolic -> Cmd
forall (r :: * -> *). Event r -> Cmd
getCmd Event Symbolic
ev) of
      (Bool
True, Cmd
ReOpen) -> Either Tag EventPred
next
      (Bool
False, Cmd
Close) -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Bool -> Either Tag EventPred -> EventPred
tagReOpen Bool
True Either Tag EventPred
next
      (Bool
False, Corruption Corruptions
_) -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Bool -> Either Tag EventPred -> EventPred
tagReOpen Bool
True Either Tag EventPred
next
      (Bool, Cmd)
_ -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Bool -> Either Tag EventPred -> EventPred
tagReOpen Bool
hasClosed Either Tag EventPred
next

  tagCorruptWriteFile :: EventPred
  tagCorruptWriteFile :: EventPred
tagCorruptWriteFile = (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
successful ((Event Symbolic -> Success -> Either Tag EventPred) -> EventPred)
-> (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
forall a b. (a -> b) -> a -> b
$ \Event Symbolic
ev Success
_ -> case Event Symbolic -> Cmd
forall (r :: * -> *). Event r -> Cmd
getCmd Event Symbolic
ev of
    Corruption Corruptions
cors
      | let currentFile :: FsPath
currentFile = DBModel Block -> FsPath
forall blk. DBModel blk -> FsPath
getCurrentFile (DBModel Block -> FsPath) -> DBModel Block -> FsPath
forall a b. (a -> b) -> a -> b
$ Model Symbolic -> DBModel Block
forall (r :: * -> *). Model r -> DBModel Block
dbModel (Model Symbolic -> DBModel Block)
-> Model Symbolic -> DBModel Block
forall a b. (a -> b) -> a -> b
$ Event Symbolic -> Model Symbolic
forall (r :: * -> *). Event r -> Model r
eventBefore Event Symbolic
ev
      , ((FileCorruption, FsPath) -> Bool) -> Corruptions -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (FsPath -> (FileCorruption, FsPath) -> Bool
forall {a}. Eq a => a -> (FileCorruption, a) -> Bool
currentFileGotCorrupted FsPath
currentFile) Corruptions
cors ->
          Tag -> Either Tag EventPred
forall a b. a -> Either a b
Left Tag
TagCorruptWriteFile
    Cmd
_ -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right EventPred
tagCorruptWriteFile
   where
    currentFileGotCorrupted :: a -> (FileCorruption, a) -> Bool
currentFileGotCorrupted a
currentFile (FileCorruption
cor, a
file)
      | FileCorruption
DeleteFile <- FileCorruption
cor =
          a
file a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
currentFile
      | Bool
otherwise =
          Bool
False

  tagIsClosedError :: EventPred
  tagIsClosedError :: EventPred
tagIsClosedError = (Event Symbolic -> Either Tag EventPred) -> EventPred
forall a b. (a -> Either b (Predicate a b)) -> Predicate a b
C.predicate ((Event Symbolic -> Either Tag EventPred) -> EventPred)
-> (Event Symbolic -> Either Tag EventPred) -> EventPred
forall a b. (a -> b) -> a -> b
$ \Event Symbolic
ev -> case Event Symbolic -> Resp
forall (r :: * -> *). Event r -> Resp
eventMockResp Event Symbolic
ev of
    Resp (Left (ApiMisuse (ClosedDBError Maybe SomeException
_))) -> Tag -> Either Tag EventPred
forall a b. a -> Either a b
Left Tag
TagClosedError
    Resp
_ -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right EventPred
tagIsClosedError

  tagGarbageCollectThenReOpen :: EventPred
  tagGarbageCollectThenReOpen :: EventPred
tagGarbageCollectThenReOpen = (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
successful ((Event Symbolic -> Success -> Either Tag EventPred) -> EventPred)
-> (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
forall a b. (a -> b) -> a -> b
$ \Event Symbolic
ev Success
_ -> case Event Symbolic -> Cmd
forall (r :: * -> *). Event r -> Cmd
getCmd Event Symbolic
ev of
    GarbageCollect SlotNo
_ ->
      EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$
        Bool -> Either Tag EventPred -> EventPred
tagReOpen Bool
False (Either Tag EventPred -> EventPred)
-> Either Tag EventPred -> EventPred
forall a b. (a -> b) -> a -> b
$
          Tag -> Either Tag EventPred
forall a b. a -> Either a b
Left Tag
TagGarbageCollectThenReOpen
    Cmd
_ -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ EventPred
tagGarbageCollectThenReOpen

getCmd :: Event r -> Cmd
getCmd :: forall (r :: * -> *). Event r -> Cmd
getCmd Event r
ev = CmdErr -> Cmd
cmd (CmdErr -> Cmd) -> CmdErr -> Cmd
forall a b. (a -> b) -> a -> b
$ At CmdErr r -> CmdErr
forall t (r :: * -> *). At t r -> t
unAt (Event r -> At CmdErr r
forall (r :: * -> *). Event r -> At CmdErr r
eventCmd Event r
ev)

isMemberTrue :: [Event Symbolic] -> Int
isMemberTrue :: [Event Symbolic] -> Int
isMemberTrue [Event Symbolic]
events = [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ Event Symbolic -> Int
count (Event Symbolic -> Int) -> [Event Symbolic] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Event Symbolic]
events
 where
  count :: Event Symbolic -> Int
  count :: Event Symbolic -> Int
count Event Symbolic
e = case Event Symbolic -> Resp
forall (r :: * -> *). Event r -> Resp
eventMockResp Event Symbolic
e of
    Resp (Left VolatileDBError Block
_) -> Int
0
    Resp (Right (BlockInfos [Maybe (BlockInfo Block)]
ls)) -> [BlockInfo Block] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([BlockInfo Block] -> Int) -> [BlockInfo Block] -> Int
forall a b. (a -> b) -> a -> b
$ [Maybe (BlockInfo Block)] -> [BlockInfo Block]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (BlockInfo Block)]
ls
    Resp (Right Success
_) -> Int
0

data Tag
  = -- | Request a block successfully
    --
    -- > GetBlockComponent (returns Just)
    TagGetJust
  | -- | Try to get a non-existant block
    --
    -- > GetBlockComponent (returns Nothing)
    TagGetNothing
  | -- | Make a request, close, re-open and do another request.
    --
    -- > GetBlockComponent (returns Just)
    -- > CloseDB or Corrupt
    -- > ReOpen
    -- > GetBlockComponent (returns Just)
    TagGetReOpenGet
  | -- | Close, re-open and do a request.
    --
    -- > CloseDB or Corrupt
    -- > ReOpen
    -- > GetBlockComponent (returns Just)
    TagReOpenGet
  | -- | Test Garbage Collect.
    --
    -- > PutBlock
    -- > GarbageColect
    -- > GetBlockComponent (returns Nothing)
    TagGarbageCollect
  | -- | Try to delete the current active file.
    --
    -- > Corrupt Delete
    TagCorruptWriteFile
  | -- | A test with zero commands.
    TagEmpty
  | -- | Returns ClosedDBError (whatever Command)
    TagClosedError
  | -- | Gc then Close then Open
    --
    -- > GarbageCollect
    -- > CloseDB
    -- > ReOpen
    TagGarbageCollectThenReOpen
  deriving Int -> Tag -> ShowS
[Tag] -> ShowS
Tag -> String
(Int -> Tag -> ShowS)
-> (Tag -> String) -> ([Tag] -> ShowS) -> Show Tag
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Tag -> ShowS
showsPrec :: Int -> Tag -> ShowS
$cshow :: Tag -> String
show :: Tag -> String
$cshowList :: [Tag] -> ShowS
showList :: [Tag] -> ShowS
Show

tagSimulatedErrors :: [Event Symbolic] -> [String]
tagSimulatedErrors :: [Event Symbolic] -> [String]
tagSimulatedErrors [Event Symbolic]
events = (Event Symbolic -> String) -> [Event Symbolic] -> [String]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Event Symbolic -> String
tagError [Event Symbolic]
events
 where
  tagError :: Event Symbolic -> String
  tagError :: Event Symbolic -> String
tagError Event Symbolic
ev = case Event Symbolic -> At CmdErr Symbolic
forall (r :: * -> *). Event r -> At CmdErr r
eventCmd Event Symbolic
ev of
    At (CmdErr Cmd
_ Maybe Errors
Nothing) -> String
"NoError"
    At (CmdErr Cmd
cmd Maybe Errors
_) -> At Cmd Any -> String
forall k (cmd :: k -> *) (r :: k).
CommandNames cmd =>
cmd r -> String
forall (r :: * -> *). At Cmd r -> String
cmdName (Cmd -> At Cmd Any
forall t (r :: * -> *). t -> At t r
At Cmd
cmd) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Error"

tagFilterByPredecessor :: [Event Symbolic] -> [String]
tagFilterByPredecessor :: [Event Symbolic] -> [String]
tagFilterByPredecessor = (Event Symbolic -> Maybe String) -> [Event Symbolic] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Event Symbolic -> Maybe String
f
 where
  f :: Event Symbolic -> Maybe String
  f :: Event Symbolic -> Maybe String
f Event Symbolic
ev = case (Event Symbolic -> Cmd
forall (r :: * -> *). Event r -> Cmd
getCmd Event Symbolic
ev, Event Symbolic -> Resp
forall (r :: * -> *). Event r -> Resp
eventMockResp Event Symbolic
ev) of
    (FilterByPredecessor [ChainHash Block]
_pid, Resp (Right (Successors [Set (HeaderHash Block)]
st))) ->
      if (Set TestHeaderHash -> Bool) -> [Set TestHeaderHash] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Set TestHeaderHash -> Bool
forall a. Set a -> Bool
Set.null [Set (HeaderHash Block)]
[Set TestHeaderHash]
st
        then String -> Maybe String
forall a. a -> Maybe a
Just String
"Empty Successors"
        else String -> Maybe String
forall a. a -> Maybe a
Just String
"Non empty Successors"
    (Cmd, Resp)
_otherwise -> Maybe String
forall a. Maybe a
Nothing

execCmd ::
  Model Symbolic ->
  Command (At CmdErr) (At Resp) ->
  Event Symbolic
execCmd :: Model Symbolic -> Command (At CmdErr) (At Resp) -> Event Symbolic
execCmd Model Symbolic
model (Command At CmdErr Symbolic
cmdErr At Resp Symbolic
_resp [Var]
_vars) = Model Symbolic -> At CmdErr Symbolic -> Event Symbolic
forall (r :: * -> *). Model r -> At CmdErr r -> Event r
lockstep Model Symbolic
model At CmdErr Symbolic
cmdErr

execCmds :: Model Symbolic -> Commands (At CmdErr) (At Resp) -> [Event Symbolic]
execCmds :: Model Symbolic
-> Commands (At CmdErr) (At Resp) -> [Event Symbolic]
execCmds Model Symbolic
model (Commands [Command (At CmdErr) (At Resp)]
cs) = Model Symbolic
-> [Command (At CmdErr) (At Resp)] -> [Event Symbolic]
go Model Symbolic
model [Command (At CmdErr) (At Resp)]
cs
 where
  go :: Model Symbolic -> [Command (At CmdErr) (At Resp)] -> [Event Symbolic]
  go :: Model Symbolic
-> [Command (At CmdErr) (At Resp)] -> [Event Symbolic]
go Model Symbolic
_ [] = []
  go Model Symbolic
m (Command (At CmdErr) (At Resp)
c : [Command (At CmdErr) (At Resp)]
css) = let ev :: Event Symbolic
ev = Model Symbolic -> Command (At CmdErr) (At Resp) -> Event Symbolic
execCmd Model Symbolic
m Command (At CmdErr) (At Resp)
c in Event Symbolic
ev Event Symbolic -> [Event Symbolic] -> [Event Symbolic]
forall a. a -> [a] -> [a]
: Model Symbolic
-> [Command (At CmdErr) (At Resp)] -> [Event Symbolic]
go (Event Symbolic -> Model Symbolic
forall (r :: * -> *). Event r -> Model r
eventAfter Event Symbolic
ev) [Command (At CmdErr) (At Resp)]
css

showLabelledExamples :: IO ()
showLabelledExamples :: IO ()
showLabelledExamples = Maybe Int -> Int -> IO ()
showLabelledExamples' Maybe Int
forall a. Maybe a
Nothing Int
1000

showLabelledExamples' ::
  -- | Seed
  Maybe Int ->
  -- | Number of tests to run to find examples
  Int ->
  IO ()
showLabelledExamples' :: Maybe Int -> Int -> IO ()
showLabelledExamples' Maybe Int
mReplay Int
numTests = do
  replaySeed <- case Maybe Int
mReplay of
    Maybe Int
Nothing -> (StdGen -> (Int, StdGen)) -> IO Int
forall (m :: * -> *) a. MonadIO m => (StdGen -> (a, StdGen)) -> m a
getStdRandom ((Int, Int) -> StdGen -> (Int, StdGen)
forall g. RandomGen g => (Int, Int) -> g -> (Int, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Int
1, Int
999999))
    Just Int
seed -> Int -> IO Int
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
seed

  labelledExamplesWith
    ( stdArgs
        { replay = Just (mkQCGen replaySeed, 0)
        , maxSuccess = numTests
        }
    )
    $ forAllShrinkShow
      (QSM.generateCommands smUnused Nothing)
      (QSM.shrinkCommands smUnused)
      ppShow
    $ \Commands (At CmdErr) (At Resp)
cmds ->
      [Tag] -> Property -> Property
forall a. Show a => [a] -> Property -> Property
collects ([Event Symbolic] -> [Tag]
tag ([Event Symbolic] -> [Tag])
-> (Commands (At CmdErr) (At Resp) -> [Event Symbolic])
-> Commands (At CmdErr) (At Resp)
-> [Tag]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model Symbolic
-> Commands (At CmdErr) (At Resp) -> [Event Symbolic]
execCmds (StateMachine Model (At CmdErr) IO (At Resp)
-> forall {r :: * -> *}. Model r
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel StateMachine Model (At CmdErr) IO (At Resp)
smUnused) (Commands (At CmdErr) (At Resp) -> [Tag])
-> Commands (At CmdErr) (At Resp) -> [Tag]
forall a b. (a -> b) -> a -> b
$ Commands (At CmdErr) (At Resp)
cmds) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
        Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
 where
  dbm :: DBModel Block
dbm = BlocksPerFile -> CodecConfig Block -> DBModel Block
forall blk. BlocksPerFile -> CodecConfig blk -> DBModel blk
initDBModel BlocksPerFile
testMaxBlocksPerFile CodecConfig Block
TestBlockCodecConfig
  smUnused :: StateMachine Model (At CmdErr) IO (At Resp)
smUnused = VolatileDBEnv
-> DBModel Block -> StateMachine Model (At CmdErr) IO (At Resp)
sm VolatileDBEnv
unusedEnv DBModel Block
dbm