{-# 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 qualified Generics.SOP as SOP
import           GHC.Generics
import           GHC.Stack
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           Prelude hiding (elem)
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)


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' :: Maybe Int
                      -- ^ Seed
                      -> Int
                      -- ^ Number of tests to run to find examples
                      -> 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