{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PackageImports #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wno-orphans #-}
#if __GLASGOW_HASKELL__ >= 908
{-# OPTIONS_GHC -Wno-x-partial #-}
#endif

-- | On-disk ledger DB tests.
--
-- This is a state-machine based test. The commands here are
--
-- * Get the current volatile and immutable tip
-- * Switch to a fork (possibly rolling back 0 blocks, so equivalent to a push)
-- * Write a snapshot to disk
-- * Restore the ledger DB from the snapshots on disk
-- * Model disk corruption (truncate or delete latest snapshot)
--
-- The model here is satisfyingly simple: just a map from blocks to their
-- corresponding ledger state modelling the whole block chain since genesis.
module Test.Ouroboros.Storage.LedgerDB.StateMachine (tests) where

import qualified Cardano.Ledger.BaseTypes as BT
import qualified Control.Monad as Monad
import           Control.Monad.Except
import           Control.Monad.State hiding (state)
import           Control.ResourceRegistry
import           Control.Tracer (nullTracer)
import qualified Data.List as L
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import qualified Data.SOP.Dict as Dict
import           Data.Word
import           Ouroboros.Consensus.Block
import           Ouroboros.Consensus.Config
import           Ouroboros.Consensus.Ledger.Abstract
import           Ouroboros.Consensus.Ledger.Extended
import           Ouroboros.Consensus.Ledger.Tables.Utils
import qualified Ouroboros.Consensus.Storage.ChainDB.Impl.BlockCache as BlockCache
import           Ouroboros.Consensus.Storage.ImmutableDB.Stream
import           Ouroboros.Consensus.Storage.LedgerDB
import           Ouroboros.Consensus.Storage.LedgerDB.Snapshots
import           Ouroboros.Consensus.Storage.LedgerDB.V1 as V1
import           Ouroboros.Consensus.Storage.LedgerDB.V1.Args hiding
                     (LedgerDbFlavorArgs)
import           Ouroboros.Consensus.Storage.LedgerDB.V2 as V2
import           Ouroboros.Consensus.Storage.LedgerDB.V2.Args hiding
                     (LedgerDbFlavorArgs)
import           Ouroboros.Consensus.Util hiding (Some)
import           Ouroboros.Consensus.Util.Args
import           Ouroboros.Consensus.Util.IOLike
import qualified Ouroboros.Network.AnchoredSeq as AS
import qualified System.Directory as Dir
import qualified System.FilePath as FilePath
import           System.FS.API
import qualified System.FS.IO as FSIO
import qualified System.FS.Sim.MockFS as MockFS
import           System.FS.Sim.STM
import qualified System.IO.Temp as Temp
import           Test.Ouroboros.Storage.LedgerDB.StateMachine.TestBlock
import           Test.Ouroboros.Storage.LedgerDB.V1.LMDB
import qualified Test.QuickCheck as QC
import           "quickcheck-dynamic" Test.QuickCheck.Extras
import qualified Test.QuickCheck.Monadic as QC
import           Test.QuickCheck.StateModel
import           Test.Tasty
import           Test.Tasty.QuickCheck
import           Test.Util.TestBlock hiding (TestBlock, TestBlockCodecConfig,
                     TestBlockStorageConfig)

tests :: TestTree
tests :: TestTree
tests = TestName -> [TestTree] -> TestTree
testGroup TestName
"StateMachine" [
      TestName -> (Actions Model -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"InMemV1" ((Actions Model -> Property) -> TestTree)
-> (Actions Model -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
          Int
-> (SecurityParam -> TestName -> TestArguments IO)
-> IO (TestName, IO ())
-> IO (SomeHasFS IO, IO ())
-> Actions Model
-> Property
prop_sequential Int
100000 SecurityParam -> TestName -> TestArguments IO
inMemV1TestArguments IO (TestName, IO ())
noFilePath IO (SomeHasFS IO, IO ())
simulatedFS
    , TestName -> (Actions Model -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"InMemV2" ((Actions Model -> Property) -> TestTree)
-> (Actions Model -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
          Int
-> (SecurityParam -> TestName -> TestArguments IO)
-> IO (TestName, IO ())
-> IO (SomeHasFS IO, IO ())
-> Actions Model
-> Property
prop_sequential Int
100000 SecurityParam -> TestName -> TestArguments IO
inMemV2TestArguments IO (TestName, IO ())
noFilePath IO (SomeHasFS IO, IO ())
simulatedFS
    , TestName -> (Actions Model -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"LMDB" ((Actions Model -> Property) -> TestTree)
-> (Actions Model -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
          Int
-> (SecurityParam -> TestName -> TestArguments IO)
-> IO (TestName, IO ())
-> IO (SomeHasFS IO, IO ())
-> Actions Model
-> Property
prop_sequential Int
1000 SecurityParam -> TestName -> TestArguments IO
lmdbTestArguments IO (TestName, IO ())
realFilePath IO (SomeHasFS IO, IO ())
realFS
    ]

prop_sequential ::
     Int
  -> (SecurityParam -> FilePath -> TestArguments IO)
  -> IO (FilePath, IO ())
  -> IO (SomeHasFS IO, IO ())
  -> Actions Model
  -> QC.Property
prop_sequential :: Int
-> (SecurityParam -> TestName -> TestArguments IO)
-> IO (TestName, IO ())
-> IO (SomeHasFS IO, IO ())
-> Actions Model
-> Property
prop_sequential Int
maxSuccess SecurityParam -> TestName -> TestArguments IO
mkTestArguments IO (TestName, IO ())
getLmdbDir IO (SomeHasFS IO, IO ())
fsOps Actions Model
as = Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
QC.withMaxSuccess Int
maxSuccess (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
  PropertyM IO () -> Property
forall a. Testable a => PropertyM IO a -> Property
QC.monadicIO (PropertyM IO () -> Property) -> PropertyM IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
    ref <- IO Environment -> PropertyM IO Environment
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Environment -> PropertyM IO Environment)
-> IO Environment -> PropertyM IO Environment
forall a b. (a -> b) -> a -> b
$ IO (SomeHasFS IO, IO ())
-> IO (TestName, IO ())
-> (SecurityParam -> TestName -> TestArguments IO)
-> ChainDB IO
-> IO Environment
initialEnvironment IO (SomeHasFS IO, IO ())
fsOps IO (TestName, IO ())
getLmdbDir SecurityParam -> TestName -> TestArguments IO
mkTestArguments (ChainDB IO -> IO Environment) -> IO (ChainDB IO) -> IO Environment
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO (ChainDB IO)
forall (m :: * -> *). (MonadIO m, IOLike m) => m (ChainDB m)
initChainDB
    (_, Environment _ testInternals _ _ _ clean) <- runPropertyStateT (runActions as) ref
    QC.run $ closeLedgerDB testInternals >> clean
    QC.assert True

-- | The initial environment is mostly undefined because it will be initialized
-- by the @Init@ command. We are forced to provide this dummy implementation
-- because some parts of it are static (which we can provide now) and also the
-- empty sequence of commands must still run the cleanup functions, which here
-- are trivial, but nevertheless they have to exist.
initialEnvironment ::
     IO (SomeHasFS IO, IO ())
  -> IO (FilePath, IO ())
  -> (SecurityParam ->  FilePath -> TestArguments IO)
  -> ChainDB IO
  -> IO Environment
initialEnvironment :: IO (SomeHasFS IO, IO ())
-> IO (TestName, IO ())
-> (SecurityParam -> TestName -> TestArguments IO)
-> ChainDB IO
-> IO Environment
initialEnvironment IO (SomeHasFS IO, IO ())
fsOps IO (TestName, IO ())
getLmdbDir SecurityParam -> TestName -> TestArguments IO
mkTestArguments ChainDB IO
cdb = do
  (sfs, cleanupFS) <- IO (SomeHasFS IO, IO ())
fsOps
  (lmdbDir, cleanupLMDB) <- getLmdbDir
  pure $ Environment
    undefined
    (TestInternals undefined undefined undefined undefined undefined (pure ()))
    cdb
    (flip mkTestArguments lmdbDir)
    sfs
    (cleanupFS >> cleanupLMDB)

{-------------------------------------------------------------------------------
  Arguments
-------------------------------------------------------------------------------}

data TestArguments m = TestArguments {
      forall (m :: * -> *).
TestArguments m -> Complete LedgerDbFlavorArgs m
argFlavorArgs  :: !(Complete LedgerDbFlavorArgs m)
    , forall (m :: * -> *).
TestArguments m -> LedgerDbCfg (ExtLedgerState TestBlock)
argLedgerDbCfg :: !(LedgerDbCfg (ExtLedgerState TestBlock))
    }

noFilePath :: IO (FilePath, IO ())
noFilePath :: IO (TestName, IO ())
noFilePath = (TestName, IO ()) -> IO (TestName, IO ())
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TestName
"Bogus", () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())

realFilePath :: IO (FilePath, IO ())
realFilePath :: IO (TestName, IO ())
realFilePath = IO (TestName, IO ()) -> IO (TestName, IO ())
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (TestName, IO ()) -> IO (TestName, IO ()))
-> IO (TestName, IO ()) -> IO (TestName, IO ())
forall a b. (a -> b) -> a -> b
$ do
  tmpdir <- (TestName -> TestName -> TestName
FilePath.</> TestName
"test_lmdb") (TestName -> TestName) -> IO TestName -> IO TestName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO TestName
Dir.getTemporaryDirectory
  pure (tmpdir, do
           exists <- Dir.doesDirectoryExist tmpdir
           Monad.when exists $ Dir.removeDirectoryRecursive tmpdir)

simulatedFS :: IO (SomeHasFS IO, IO ())
simulatedFS :: IO (SomeHasFS IO, IO ())
simulatedFS = do
  fs <- MockFS -> IO (HasFS IO HandleMock)
forall (m :: * -> *).
(MonadSTM m, MonadThrow m, PrimMonad m) =>
MockFS -> m (HasFS m HandleMock)
simHasFS' MockFS
MockFS.empty
  pure (SomeHasFS fs , pure ())

realFS :: IO (SomeHasFS IO, IO ())
realFS :: IO (SomeHasFS IO, IO ())
realFS = IO (SomeHasFS IO, IO ()) -> IO (SomeHasFS IO, IO ())
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SomeHasFS IO, IO ()) -> IO (SomeHasFS IO, IO ()))
-> IO (SomeHasFS IO, IO ()) -> IO (SomeHasFS IO, IO ())
forall a b. (a -> b) -> a -> b
$ do
  systmpdir <- IO TestName
Dir.getTemporaryDirectory
  tmpdir <- Temp.createTempDirectory systmpdir "init_standalone_db"
  pure (SomeHasFS $ FSIO.ioHasFS $ MountPoint tmpdir, Dir.removeDirectoryRecursive tmpdir)

inMemV1TestArguments ::
     SecurityParam
  -> FilePath
  -> TestArguments IO
inMemV1TestArguments :: SecurityParam -> TestName -> TestArguments IO
inMemV1TestArguments SecurityParam
secParam TestName
_ =
  TestArguments {
      argFlavorArgs :: Complete LedgerDbFlavorArgs IO
argFlavorArgs = LedgerDbFlavorArgs Identity IO -> Complete LedgerDbFlavorArgs IO
forall (f :: * -> *) (m :: * -> *).
LedgerDbFlavorArgs f m -> LedgerDbFlavorArgs f m
LedgerDbFlavorArgsV1 (LedgerDbFlavorArgs Identity IO -> Complete LedgerDbFlavorArgs IO)
-> LedgerDbFlavorArgs Identity IO -> Complete LedgerDbFlavorArgs IO
forall a b. (a -> b) -> a -> b
$ FlushFrequency
-> BackingStoreArgs Identity IO -> LedgerDbFlavorArgs Identity IO
forall (f :: * -> *) (m :: * -> *).
FlushFrequency -> BackingStoreArgs f m -> LedgerDbFlavorArgs f m
V1Args FlushFrequency
DisableFlushing BackingStoreArgs Identity IO
forall (f :: * -> *) (m :: * -> *). BackingStoreArgs f m
InMemoryBackingStoreArgs
    , argLedgerDbCfg :: LedgerDbCfg (ExtLedgerState TestBlock)
argLedgerDbCfg = SecurityParam -> LedgerDbCfg (ExtLedgerState TestBlock)
extLedgerDbConfig SecurityParam
secParam
    }

inMemV2TestArguments ::
     SecurityParam
  -> FilePath
  -> TestArguments IO
inMemV2TestArguments :: SecurityParam -> TestName -> TestArguments IO
inMemV2TestArguments SecurityParam
secParam TestName
_ =
  TestArguments {
      argFlavorArgs :: Complete LedgerDbFlavorArgs IO
argFlavorArgs = LedgerDbFlavorArgs Identity IO -> Complete LedgerDbFlavorArgs IO
forall (f :: * -> *) (m :: * -> *).
LedgerDbFlavorArgs f m -> LedgerDbFlavorArgs f m
LedgerDbFlavorArgsV2 (LedgerDbFlavorArgs Identity IO -> Complete LedgerDbFlavorArgs IO)
-> LedgerDbFlavorArgs Identity IO -> Complete LedgerDbFlavorArgs IO
forall a b. (a -> b) -> a -> b
$ HandleArgs -> LedgerDbFlavorArgs Identity IO
forall {k} {k1} (f :: k) (m :: k1).
HandleArgs -> LedgerDbFlavorArgs f m
V2Args HandleArgs
InMemoryHandleArgs
    , argLedgerDbCfg :: LedgerDbCfg (ExtLedgerState TestBlock)
argLedgerDbCfg = SecurityParam -> LedgerDbCfg (ExtLedgerState TestBlock)
extLedgerDbConfig SecurityParam
secParam
    }

lmdbTestArguments ::
     SecurityParam
  -> FilePath
  -> TestArguments IO
lmdbTestArguments :: SecurityParam -> TestName -> TestArguments IO
lmdbTestArguments SecurityParam
secParam TestName
fp =
  TestArguments {
      argFlavorArgs :: Complete LedgerDbFlavorArgs IO
argFlavorArgs = LedgerDbFlavorArgs Identity IO -> Complete LedgerDbFlavorArgs IO
forall (f :: * -> *) (m :: * -> *).
LedgerDbFlavorArgs f m -> LedgerDbFlavorArgs f m
LedgerDbFlavorArgsV1 (LedgerDbFlavorArgs Identity IO -> Complete LedgerDbFlavorArgs IO)
-> LedgerDbFlavorArgs Identity IO -> Complete LedgerDbFlavorArgs IO
forall a b. (a -> b) -> a -> b
$ FlushFrequency
-> BackingStoreArgs Identity IO -> LedgerDbFlavorArgs Identity IO
forall (f :: * -> *) (m :: * -> *).
FlushFrequency -> BackingStoreArgs f m -> LedgerDbFlavorArgs f m
V1Args FlushFrequency
DisableFlushing (BackingStoreArgs Identity IO -> LedgerDbFlavorArgs Identity IO)
-> BackingStoreArgs Identity IO -> LedgerDbFlavorArgs Identity IO
forall a b. (a -> b) -> a -> b
$ TestName
-> HKD Identity LMDBLimits
-> Dict MonadIOPrim IO
-> BackingStoreArgs Identity IO
forall (f :: * -> *) (m :: * -> *).
TestName
-> HKD f LMDBLimits -> Dict MonadIOPrim m -> BackingStoreArgs f m
LMDBBackingStoreArgs TestName
fp (Int -> LMDBLimits
testLMDBLimits Int
16) Dict MonadIOPrim IO
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict.Dict
    , argLedgerDbCfg :: LedgerDbCfg (ExtLedgerState TestBlock)
argLedgerDbCfg = SecurityParam -> LedgerDbCfg (ExtLedgerState TestBlock)
extLedgerDbConfig SecurityParam
secParam
    }

{-------------------------------------------------------------------------------
 Model
-------------------------------------------------------------------------------}

type TheBlockChain =
  AS.AnchoredSeq
    (WithOrigin SlotNo)
    (ExtLedgerState TestBlock ValuesMK)
    (TestBlock, ExtLedgerState TestBlock ValuesMK)

data Model =
    UnInit
  | Model
      TheBlockChain
      SecurityParam
  deriving ((forall x. Model -> Rep Model x)
-> (forall x. Rep Model x -> Model) -> Generic Model
forall x. Rep Model x -> Model
forall x. Model -> Rep Model x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Model -> Rep Model x
from :: forall x. Model -> Rep Model x
$cto :: forall x. Rep Model x -> Model
to :: forall x. Rep Model x -> Model
Generic, Int -> Model -> TestName -> TestName
[Model] -> TestName -> TestName
Model -> TestName
(Int -> Model -> TestName -> TestName)
-> (Model -> TestName)
-> ([Model] -> TestName -> TestName)
-> Show Model
forall a.
(Int -> a -> TestName -> TestName)
-> (a -> TestName) -> ([a] -> TestName -> TestName) -> Show a
$cshowsPrec :: Int -> Model -> TestName -> TestName
showsPrec :: Int -> Model -> TestName -> TestName
$cshow :: Model -> TestName
show :: Model -> TestName
$cshowList :: [Model] -> TestName -> TestName
showList :: [Model] -> TestName -> TestName
Show)

instance AS.Anchorable
           (WithOrigin SlotNo)
           (ExtLedgerState TestBlock ValuesMK)
           (TestBlock, ExtLedgerState TestBlock ValuesMK) where
  asAnchor :: (TestBlock, ExtLedgerState TestBlock ValuesMK)
-> ExtLedgerState TestBlock ValuesMK
asAnchor = (TestBlock, ExtLedgerState TestBlock ValuesMK)
-> ExtLedgerState TestBlock ValuesMK
forall a b. (a, b) -> b
snd
  getAnchorMeasure :: Proxy (TestBlock, ExtLedgerState TestBlock ValuesMK)
-> ExtLedgerState TestBlock ValuesMK -> WithOrigin SlotNo
getAnchorMeasure Proxy (TestBlock, ExtLedgerState TestBlock ValuesMK)
_ = ExtLedgerState TestBlock ValuesMK -> WithOrigin SlotNo
forall (l :: LedgerStateKind) (mk :: MapKind).
GetTip l =>
l mk -> WithOrigin SlotNo
getTipSlot

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

modelUpdateLedger ::
     StateT
       TheBlockChain
       (Except (ExtValidationError TestBlock)) a
  -> Model
  -> Model
modelUpdateLedger :: forall a.
StateT TheBlockChain (Except (ExtValidationError TestBlock)) a
-> Model -> Model
modelUpdateLedger StateT TheBlockChain (Except (ExtValidationError TestBlock)) a
f model :: Model
model@(Model TheBlockChain
chain SecurityParam
secParam) =
    case Except (ExtValidationError TestBlock) (a, TheBlockChain)
-> Either (ExtValidationError TestBlock) (a, TheBlockChain)
forall e a. Except e a -> Either e a
runExcept (StateT TheBlockChain (Except (ExtValidationError TestBlock)) a
-> TheBlockChain
-> Except (ExtValidationError TestBlock) (a, TheBlockChain)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT TheBlockChain (Except (ExtValidationError TestBlock)) a
f TheBlockChain
chain) of
      Left{}             -> Model
model
      Right (a
_, TheBlockChain
ledger') -> TheBlockChain -> SecurityParam -> Model
Model TheBlockChain
ledger' SecurityParam
secParam
modelUpdateLedger StateT TheBlockChain (Except (ExtValidationError TestBlock)) a
_ Model
_ = TestName -> Model
forall a. HasCallStack => TestName -> a
error TestName
"Uninitialized model tried to apply blocks!"

modelRollback :: Word64 -> Model -> Model
modelRollback :: Word64 -> Model -> Model
modelRollback Word64
n (Model TheBlockChain
chain SecurityParam
secParam) =
   TheBlockChain -> SecurityParam -> Model
Model (Int -> TheBlockChain -> TheBlockChain
forall v a b.
Anchorable v a b =>
Int -> AnchoredSeq v a b -> AnchoredSeq v a b
AS.dropNewest (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n) TheBlockChain
chain) SecurityParam
secParam
modelRollback Word64
_ Model
UnInit = TestName -> Model
forall a. HasCallStack => TestName -> a
error TestName
"Uninitialized model can't rollback!"

{-------------------------------------------------------------------------------
  StateModel
-------------------------------------------------------------------------------}

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

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

instance HasVariables (BT.NonZero Word64) where
  getAllVariables :: NonZero Word64 -> Set (Any Var)
getAllVariables NonZero Word64
_ = Set (Any Var)
forall a. Monoid a => a
mempty

instance StateModel Model where
  data Action Model a where
    WipeLedgerDB      :: Action Model ()
    TruncateSnapshots :: Action Model ()
    DropAndRestore    :: Word64 -> Action Model ()
    ForceTakeSnapshot :: Action Model ()
    GetState          :: Action Model (ExtLedgerState TestBlock EmptyMK, ExtLedgerState TestBlock EmptyMK)
    Init              :: SecurityParam -> Action Model ()
    ValidateAndCommit :: Word64 -> [TestBlock] -> Action Model ()

  actionName :: forall a. Action Model a -> TestName
actionName WipeLedgerDB{}      = TestName
"WipeLedgerDB"
  actionName TruncateSnapshots{} = TestName
"TruncateSnapshots"
  actionName DropAndRestore{}    = TestName
"DropAndRestore"
  actionName Action Model a
R:ActionModela a
ForceTakeSnapshot   = TestName
"TakeSnapshot"
  actionName GetState{}          = TestName
"GetState"
  actionName Init{}              = TestName
"Init"
  actionName ValidateAndCommit{} = TestName
"ValidateAndCommit"

  arbitraryAction :: VarContext -> Model -> Gen (Any (Action Model))
arbitraryAction VarContext
_ Model
UnInit = Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model () -> Any (Action Model))
-> (SecurityParam -> Action Model ())
-> SecurityParam
-> Any (Action Model)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SecurityParam -> Action Model ()
Init (SecurityParam -> Any (Action Model))
-> Gen SecurityParam -> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen SecurityParam
forall a. Arbitrary a => Gen a
QC.arbitrary
  arbitraryAction VarContext
_ model :: Model
model@(Model TheBlockChain
chain SecurityParam
secParam) =
    [(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model))
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency ([(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model)))
-> [(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ [ (Int
2, Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> Any (Action Model) -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action
  Model
  (ExtLedgerState TestBlock EmptyMK,
   ExtLedgerState TestBlock EmptyMK)
-> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Action
  Model
  (ExtLedgerState TestBlock EmptyMK,
   ExtLedgerState TestBlock EmptyMK)
GetState)
                , (Int
2, Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> Any (Action Model) -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Action Model ()
ForceTakeSnapshot)
                , (Int
1, Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model () -> Any (Action Model))
-> (Word64 -> Action Model ()) -> Word64 -> Any (Action Model)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> Action Model ()
DropAndRestore (Word64 -> Any (Action Model))
-> Gen Word64 -> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
QC.choose (Word64
0, Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word64) -> Int -> Word64
forall a b. (a -> b) -> a -> b
$ TheBlockChain -> Int
forall v a b. Anchorable v a b => AnchoredSeq v a b -> Int
AS.length TheBlockChain
chain))
                , (Int
4, Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model () -> Any (Action Model))
-> Gen (Action Model ()) -> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
                      let maxRollback :: Word64
maxRollback =
                            Word64 -> Word64 -> Word64
forall a. Ord a => a -> a -> a
min
                              (Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word64)
-> (TheBlockChain -> Int) -> TheBlockChain -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TheBlockChain -> Int
forall v a b. Anchorable v a b => AnchoredSeq v a b -> Int
AS.length (TheBlockChain -> Word64) -> TheBlockChain -> Word64
forall a b. (a -> b) -> a -> b
$ TheBlockChain
chain)
                              (NonZero Word64 -> Word64
forall a. NonZero a -> a
BT.unNonZero (NonZero Word64 -> Word64) -> NonZero Word64 -> Word64
forall a b. (a -> b) -> a -> b
$ SecurityParam -> NonZero Word64
maxRollbacks SecurityParam
secParam)
                      numRollback  <- (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
QC.choose (Word64
0, Word64
maxRollback)
                      numNewBlocks <- QC.choose (numRollback, numRollback + 2)
                      let
                        chain' = case Word64 -> Model -> Model
modelRollback Word64
numRollback Model
model of
                          Model
UnInit     -> TestName -> TheBlockChain
forall a. HasCallStack => TestName -> a
error TestName
"Impossible"
                          Model TheBlockChain
ch SecurityParam
_ -> TheBlockChain
ch
                        blocks = Word64 -> Point TestBlock -> [TestBlock]
genBlocks
                                 Word64
numNewBlocks
                                 (LedgerState TestBlock ValuesMK -> Point TestBlock
forall ptype (mk :: MapKind).
LedgerState (TestBlockWith ptype) mk -> Point (TestBlockWith ptype)
lastAppliedPoint (LedgerState TestBlock ValuesMK -> Point TestBlock)
-> (TheBlockChain -> LedgerState TestBlock ValuesMK)
-> TheBlockChain
-> Point TestBlock
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtLedgerState TestBlock ValuesMK -> LedgerState TestBlock ValuesMK
forall blk (mk :: MapKind).
ExtLedgerState blk mk -> LedgerState blk mk
ledgerState (ExtLedgerState TestBlock ValuesMK
 -> LedgerState TestBlock ValuesMK)
-> (TheBlockChain -> ExtLedgerState TestBlock ValuesMK)
-> TheBlockChain
-> LedgerState TestBlock ValuesMK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ExtLedgerState TestBlock ValuesMK
 -> ExtLedgerState TestBlock ValuesMK)
-> ((TestBlock, ExtLedgerState TestBlock ValuesMK)
    -> ExtLedgerState TestBlock ValuesMK)
-> Either
     (ExtLedgerState TestBlock ValuesMK)
     (TestBlock, ExtLedgerState TestBlock ValuesMK)
-> ExtLedgerState TestBlock ValuesMK
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ExtLedgerState TestBlock ValuesMK
-> ExtLedgerState TestBlock ValuesMK
forall a. a -> a
id (TestBlock, ExtLedgerState TestBlock ValuesMK)
-> ExtLedgerState TestBlock ValuesMK
forall a b. (a, b) -> b
snd (Either
   (ExtLedgerState TestBlock ValuesMK)
   (TestBlock, ExtLedgerState TestBlock ValuesMK)
 -> ExtLedgerState TestBlock ValuesMK)
-> (TheBlockChain
    -> Either
         (ExtLedgerState TestBlock ValuesMK)
         (TestBlock, ExtLedgerState TestBlock ValuesMK))
-> TheBlockChain
-> ExtLedgerState TestBlock ValuesMK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TheBlockChain
-> Either
     (ExtLedgerState TestBlock ValuesMK)
     (TestBlock, ExtLedgerState TestBlock ValuesMK)
forall v a b. Anchorable v a b => AnchoredSeq v a b -> Either a b
AS.head (TheBlockChain -> Point TestBlock)
-> TheBlockChain -> Point TestBlock
forall a b. (a -> b) -> a -> b
$ TheBlockChain
chain')
                      return $ ValidateAndCommit numRollback blocks)
                , (Int
1, Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> Any (Action Model) -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Action Model ()
WipeLedgerDB)
                , (Int
1, Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> Any (Action Model) -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Action Model ()
TruncateSnapshots)
                ]

  initialState :: Model
initialState = Model
UnInit

  nextState :: forall a. Typeable a => Model -> Action Model a -> Var a -> Model
nextState Model
_     (Init SecurityParam
secParam)            Var a
_var = TheBlockChain -> SecurityParam -> Model
Model (ExtLedgerState TestBlock ValuesMK -> TheBlockChain
forall v a b. Anchorable v a b => a -> AnchoredSeq v a b
AS.Empty ExtLedgerState TestBlock ValuesMK
genesis) SecurityParam
secParam
  nextState Model
state Action Model a
R:ActionModela a
GetState                   Var a
_var = Model
state
  nextState Model
state Action Model a
R:ActionModela a
ForceTakeSnapshot          Var a
_var = Model
state
  nextState state :: Model
state@(Model TheBlockChain
_ SecurityParam
secParam) (ValidateAndCommit Word64
n [TestBlock]
blks) Var a
_var =
      StateT TheBlockChain (Except (ExtValidationError TestBlock)) ()
-> Model -> Model
forall a.
StateT TheBlockChain (Except (ExtValidationError TestBlock)) a
-> Model -> Model
modelUpdateLedger StateT TheBlockChain (Except (ExtValidationError TestBlock)) ()
switch Model
state
    where
      push :: TestBlock -> StateT (AS.AnchoredSeq (WithOrigin SlotNo) (ExtLedgerState TestBlock ValuesMK) (TestBlock, ExtLedgerState TestBlock ValuesMK)) (Except (ExtValidationError TestBlock)) ()
      push :: TestBlock
-> StateT TheBlockChain (Except (ExtValidationError TestBlock)) ()
push TestBlock
b = do
        ls <- StateT
  TheBlockChain (Except (ExtValidationError TestBlock)) TheBlockChain
forall s (m :: * -> *). MonadState s m => m s
get
        let tip = (ExtLedgerState TestBlock ValuesMK
 -> ExtLedgerState TestBlock ValuesMK)
-> ((TestBlock, ExtLedgerState TestBlock ValuesMK)
    -> ExtLedgerState TestBlock ValuesMK)
-> Either
     (ExtLedgerState TestBlock ValuesMK)
     (TestBlock, ExtLedgerState TestBlock ValuesMK)
-> ExtLedgerState TestBlock ValuesMK
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ExtLedgerState TestBlock ValuesMK
-> ExtLedgerState TestBlock ValuesMK
forall a. a -> a
id (TestBlock, ExtLedgerState TestBlock ValuesMK)
-> ExtLedgerState TestBlock ValuesMK
forall a b. (a, b) -> b
snd (Either
   (ExtLedgerState TestBlock ValuesMK)
   (TestBlock, ExtLedgerState TestBlock ValuesMK)
 -> ExtLedgerState TestBlock ValuesMK)
-> Either
     (ExtLedgerState TestBlock ValuesMK)
     (TestBlock, ExtLedgerState TestBlock ValuesMK)
-> ExtLedgerState TestBlock ValuesMK
forall a b. (a -> b) -> a -> b
$ TheBlockChain
-> Either
     (ExtLedgerState TestBlock ValuesMK)
     (TestBlock, ExtLedgerState TestBlock ValuesMK)
forall v a b. Anchorable v a b => AnchoredSeq v a b -> Either a b
AS.head TheBlockChain
ls
        l' <- lift $ tickThenApply OmitLedgerEvents (ledgerDbCfg $ extLedgerDbConfig secParam) b tip
        put (ls AS.:> (b, applyDiffs tip l'))

      switch :: StateT (AS.AnchoredSeq (WithOrigin SlotNo) (ExtLedgerState TestBlock ValuesMK) (TestBlock, ExtLedgerState TestBlock ValuesMK)) (Except (ExtValidationError TestBlock)) ()
      switch :: StateT TheBlockChain (Except (ExtValidationError TestBlock)) ()
switch = do
          (TheBlockChain -> TheBlockChain)
-> StateT TheBlockChain (Except (ExtValidationError TestBlock)) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TheBlockChain -> TheBlockChain)
 -> StateT TheBlockChain (Except (ExtValidationError TestBlock)) ())
-> (TheBlockChain -> TheBlockChain)
-> StateT TheBlockChain (Except (ExtValidationError TestBlock)) ()
forall a b. (a -> b) -> a -> b
$ Int -> TheBlockChain -> TheBlockChain
forall v a b.
Anchorable v a b =>
Int -> AnchoredSeq v a b -> AnchoredSeq v a b
AS.dropNewest (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n)
          (TestBlock
 -> StateT TheBlockChain (Except (ExtValidationError TestBlock)) ())
-> [TestBlock]
-> StateT TheBlockChain (Except (ExtValidationError TestBlock)) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TestBlock
-> StateT TheBlockChain (Except (ExtValidationError TestBlock)) ()
push [TestBlock]
blks

  nextState Model
state Action Model a
R:ActionModela a
WipeLedgerDB Var a
_var = Model
state
  nextState Model
state Action Model a
R:ActionModela a
TruncateSnapshots Var a
_var = Model
state
  nextState Model
state (DropAndRestore Word64
n)         Var a
_var = Word64 -> Model -> Model
modelRollback Word64
n Model
state
  nextState Model
UnInit Action Model a
_ Var a
_ = TestName -> Model
forall a. HasCallStack => TestName -> a
error TestName
"Uninitialized model created a command different than Init"

  precondition :: forall a. Model -> Action Model a -> Bool
precondition Model
UnInit               Init{}                  = Bool
True
  precondition Model
UnInit Action Model a
_                                     = Bool
False
  precondition (Model TheBlockChain
chain SecurityParam
secParam) (ValidateAndCommit Word64
n [TestBlock]
blks) =
       Word64
n Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
<= Word64 -> Word64 -> Word64
forall a. Ord a => a -> a -> a
min (NonZero Word64 -> Word64
forall a. NonZero a -> a
BT.unNonZero (NonZero Word64 -> Word64) -> NonZero Word64 -> Word64
forall a b. (a -> b) -> a -> b
$ SecurityParam -> NonZero Word64
maxRollbacks SecurityParam
secParam) (Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word64) -> Int -> Word64
forall a b. (a -> b) -> a -> b
$ TheBlockChain -> Int
forall v a b. Anchorable v a b => AnchoredSeq v a b -> Int
AS.length TheBlockChain
chain)
    Bool -> Bool -> Bool
&& case [TestBlock]
blks of
        [] -> Bool
True
        (TestBlock
b:[TestBlock]
_) -> TestBlock -> SlotNo
forall ptype. TestBlockWith ptype -> SlotNo
tbSlot TestBlock
b SlotNo -> SlotNo -> Bool
forall a. Eq a => a -> a -> Bool
== SlotNo
1 SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
+ SlotNo -> (SlotNo -> SlotNo) -> WithOrigin SlotNo -> SlotNo
forall b t. b -> (t -> b) -> WithOrigin t -> b
withOrigin SlotNo
0 SlotNo -> SlotNo
forall a. a -> a
id (ExtLedgerState TestBlock ValuesMK -> WithOrigin SlotNo
forall (l :: LedgerStateKind) (mk :: MapKind).
GetTip l =>
l mk -> WithOrigin SlotNo
getTipSlot (TheBlockChain -> ExtLedgerState TestBlock ValuesMK
forall v a b. Anchorable v a b => AnchoredSeq v a b -> a
AS.headAnchor TheBlockChain
chain))
  precondition Model
_                    Init{}                  = Bool
False
  precondition Model
_ Action Model a
_                                          = Bool
True

{-------------------------------------------------------------------------------
  Mocked ChainDB
-------------------------------------------------------------------------------}

-- | Mocked chain db
data ChainDB m = ChainDB {
      -- | Block storage
      forall (m :: * -> *).
ChainDB m -> StrictTVar m (Map (RealPoint TestBlock) TestBlock)
dbBlocks :: StrictTVar m (Map (RealPoint TestBlock) TestBlock)

      -- | Current chain and corresponding ledger state
    , forall (m :: * -> *).
ChainDB m -> StrictTVar m [RealPoint TestBlock]
dbChain  :: StrictTVar m [RealPoint TestBlock]
    }

initChainDB ::
     forall m. (MonadIO m, IOLike m)
  => m (ChainDB m)
initChainDB :: forall (m :: * -> *). (MonadIO m, IOLike m) => m (ChainDB m)
initChainDB = do
    dbBlocks <- Map (RealPoint TestBlock) TestBlock
-> m (StrictTVar m (Map (RealPoint TestBlock) TestBlock))
forall (m :: * -> *) a. MonadSTM m => a -> m (StrictTVar m a)
uncheckedNewTVarM Map (RealPoint TestBlock) TestBlock
forall k a. Map k a
Map.empty
    dbChain  <- uncheckedNewTVarM []
    return $ ChainDB dbBlocks dbChain

dbStreamAPI ::
     forall m. IOLike m
  => SecurityParam
  -> ChainDB m
  -> m (StreamAPI m TestBlock TestBlock, [TestBlock])
dbStreamAPI :: forall (m :: * -> *).
IOLike m =>
SecurityParam
-> ChainDB m -> m (StreamAPI m TestBlock TestBlock, [TestBlock])
dbStreamAPI SecurityParam
secParam ChainDB m
chainDb =
    STM m (StreamAPI m TestBlock TestBlock, [TestBlock])
-> m (StreamAPI m TestBlock TestBlock, [TestBlock])
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m (StreamAPI m TestBlock TestBlock, [TestBlock])
 -> m (StreamAPI m TestBlock TestBlock, [TestBlock]))
-> STM m (StreamAPI m TestBlock TestBlock, [TestBlock])
-> m (StreamAPI m TestBlock TestBlock, [TestBlock])
forall a b. (a -> b) -> a -> b
$ do
      points <- [RealPoint TestBlock] -> [RealPoint TestBlock]
forall a. [a] -> [a]
reverse ([RealPoint TestBlock] -> [RealPoint TestBlock])
-> ([RealPoint TestBlock] -> [RealPoint TestBlock])
-> [RealPoint TestBlock]
-> [RealPoint TestBlock]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [RealPoint TestBlock] -> [RealPoint TestBlock]
forall a. Int -> [a] -> [a]
take (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64 -> Int) -> Word64 -> Int
forall a b. (a -> b) -> a -> b
$ NonZero Word64 -> Word64
forall a. NonZero a -> a
BT.unNonZero (NonZero Word64 -> Word64) -> NonZero Word64 -> Word64
forall a b. (a -> b) -> a -> b
$ SecurityParam -> NonZero Word64
maxRollbacks SecurityParam
secParam) ([RealPoint TestBlock] -> [RealPoint TestBlock])
-> STM m [RealPoint TestBlock] -> STM m [RealPoint TestBlock]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictTVar m [RealPoint TestBlock] -> STM m [RealPoint TestBlock]
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m [RealPoint TestBlock]
dbChain
      blks <- readTVar dbBlocks
      pure $ (StreamAPI streamAfter, map (blks Map.!) points)
  where
    ChainDB {
        StrictTVar m (Map (RealPoint TestBlock) TestBlock)
dbBlocks :: forall (m :: * -> *).
ChainDB m -> StrictTVar m (Map (RealPoint TestBlock) TestBlock)
dbBlocks :: StrictTVar m (Map (RealPoint TestBlock) TestBlock)
dbBlocks
      , StrictTVar m [RealPoint TestBlock]
dbChain :: forall (m :: * -> *).
ChainDB m -> StrictTVar m [RealPoint TestBlock]
dbChain :: StrictTVar m [RealPoint TestBlock]
dbChain
      } = ChainDB m
chainDb

    streamAfter ::
         Point TestBlock
      -> (Either (RealPoint TestBlock) (m (NextItem TestBlock)) -> m a)
      -> m a
    streamAfter :: forall a.
Point TestBlock
-> (Either (RealPoint TestBlock) (m (NextItem TestBlock)) -> m a)
-> m a
streamAfter Point TestBlock
tip Either (RealPoint TestBlock) (m (NextItem TestBlock)) -> m a
k = do
        pts <- STM m [RealPoint TestBlock] -> m [RealPoint TestBlock]
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m [RealPoint TestBlock] -> m [RealPoint TestBlock])
-> STM m [RealPoint TestBlock] -> m [RealPoint TestBlock]
forall a b. (a -> b) -> a -> b
$ [RealPoint TestBlock] -> [RealPoint TestBlock]
forall a. [a] -> [a]
reverse ([RealPoint TestBlock] -> [RealPoint TestBlock])
-> ([RealPoint TestBlock] -> [RealPoint TestBlock])
-> [RealPoint TestBlock]
-> [RealPoint TestBlock]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [RealPoint TestBlock] -> [RealPoint TestBlock]
forall a. Int -> [a] -> [a]
drop (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64 -> Int) -> Word64 -> Int
forall a b. (a -> b) -> a -> b
$ NonZero Word64 -> Word64
forall a. NonZero a -> a
BT.unNonZero (NonZero Word64 -> Word64) -> NonZero Word64 -> Word64
forall a b. (a -> b) -> a -> b
$ SecurityParam -> NonZero Word64
maxRollbacks SecurityParam
secParam) ([RealPoint TestBlock] -> [RealPoint TestBlock])
-> STM m [RealPoint TestBlock] -> STM m [RealPoint TestBlock]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictTVar m [RealPoint TestBlock] -> STM m [RealPoint TestBlock]
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m [RealPoint TestBlock]
dbChain
        case tip' of
          NotOrigin RealPoint TestBlock
pt
            | RealPoint TestBlock
pt RealPoint TestBlock -> [RealPoint TestBlock] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`L.notElem` [RealPoint TestBlock]
pts
            -> Either (RealPoint TestBlock) (m (NextItem TestBlock)) -> m a
k (Either (RealPoint TestBlock) (m (NextItem TestBlock)) -> m a)
-> Either (RealPoint TestBlock) (m (NextItem TestBlock)) -> m a
forall a b. (a -> b) -> a -> b
$ RealPoint TestBlock
-> Either (RealPoint TestBlock) (m (NextItem TestBlock))
forall a b. a -> Either a b
Left RealPoint TestBlock
pt
          WithOrigin (RealPoint TestBlock)
_otherwise
            -> do toStream <- [RealPoint TestBlock] -> m (StrictTVar m [RealPoint TestBlock])
forall (m :: * -> *) a. MonadSTM m => a -> m (StrictTVar m a)
uncheckedNewTVarM (WithOrigin (RealPoint TestBlock)
-> [RealPoint TestBlock] -> [RealPoint TestBlock]
blocksToStream WithOrigin (RealPoint TestBlock)
tip' [RealPoint TestBlock]
pts)
                  k (Right (getNext toStream))
     where
       tip' :: WithOrigin (RealPoint TestBlock)
tip' = Point TestBlock -> WithOrigin (RealPoint TestBlock)
forall blk. Point blk -> WithOrigin (RealPoint blk)
pointToWithOriginRealPoint Point TestBlock
tip

    -- Blocks to stream
    --
    -- Precondition: tip must be on the current chain
    blocksToStream ::
         WithOrigin (RealPoint TestBlock)
      -> [RealPoint TestBlock] -> [RealPoint TestBlock]
    blocksToStream :: WithOrigin (RealPoint TestBlock)
-> [RealPoint TestBlock] -> [RealPoint TestBlock]
blocksToStream WithOrigin (RealPoint TestBlock)
Origin        = [RealPoint TestBlock] -> [RealPoint TestBlock]
forall a. a -> a
id
    blocksToStream (NotOrigin RealPoint TestBlock
r) = [RealPoint TestBlock] -> [RealPoint TestBlock]
forall a. HasCallStack => [a] -> [a]
tail ([RealPoint TestBlock] -> [RealPoint TestBlock])
-> ([RealPoint TestBlock] -> [RealPoint TestBlock])
-> [RealPoint TestBlock]
-> [RealPoint TestBlock]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RealPoint TestBlock -> Bool)
-> [RealPoint TestBlock] -> [RealPoint TestBlock]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (RealPoint TestBlock -> RealPoint TestBlock -> Bool
forall a. Eq a => a -> a -> Bool
/= RealPoint TestBlock
r)

    getNext :: StrictTVar m [RealPoint TestBlock] -> m (NextItem TestBlock)
    getNext :: StrictTVar m [RealPoint TestBlock] -> m (NextItem TestBlock)
getNext StrictTVar m [RealPoint TestBlock]
toStream = do
        mr <- STM m (Maybe (RealPoint TestBlock))
-> m (Maybe (RealPoint TestBlock))
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m (Maybe (RealPoint TestBlock))
 -> m (Maybe (RealPoint TestBlock)))
-> STM m (Maybe (RealPoint TestBlock))
-> m (Maybe (RealPoint TestBlock))
forall a b. (a -> b) -> a -> b
$ do
                rs <- StrictTVar m [RealPoint TestBlock] -> STM m [RealPoint TestBlock]
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m [RealPoint TestBlock]
toStream
                case rs of
                  []    -> Maybe (RealPoint TestBlock) -> STM m (Maybe (RealPoint TestBlock))
forall a. a -> STM m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (RealPoint TestBlock)
forall a. Maybe a
Nothing
                  RealPoint TestBlock
r:[RealPoint TestBlock]
rs' -> StrictTVar m [RealPoint TestBlock]
-> [RealPoint TestBlock] -> STM m ()
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
StrictTVar m a -> a -> STM m ()
writeTVar StrictTVar m [RealPoint TestBlock]
toStream [RealPoint TestBlock]
rs' STM m ()
-> STM m (Maybe (RealPoint TestBlock))
-> STM m (Maybe (RealPoint TestBlock))
forall a b. STM m a -> STM m b -> STM m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe (RealPoint TestBlock) -> STM m (Maybe (RealPoint TestBlock))
forall a. a -> STM m a
forall (m :: * -> *) a. Monad m => a -> m a
return (RealPoint TestBlock -> Maybe (RealPoint TestBlock)
forall a. a -> Maybe a
Just RealPoint TestBlock
r)
        case mr of
          Maybe (RealPoint TestBlock)
Nothing -> NextItem TestBlock -> m (NextItem TestBlock)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return NextItem TestBlock
forall blk. NextItem blk
NoMoreItems
          Just RealPoint TestBlock
r  -> do mb <- STM m (Maybe TestBlock) -> m (Maybe TestBlock)
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m (Maybe TestBlock) -> m (Maybe TestBlock))
-> STM m (Maybe TestBlock) -> m (Maybe TestBlock)
forall a b. (a -> b) -> a -> b
$ RealPoint TestBlock
-> Map (RealPoint TestBlock) TestBlock -> Maybe TestBlock
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup RealPoint TestBlock
r (Map (RealPoint TestBlock) TestBlock -> Maybe TestBlock)
-> STM m (Map (RealPoint TestBlock) TestBlock)
-> STM m (Maybe TestBlock)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictTVar m (Map (RealPoint TestBlock) TestBlock)
-> STM m (Map (RealPoint TestBlock) TestBlock)
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m (Map (RealPoint TestBlock) TestBlock)
dbBlocks
                        case mb of
                          Just TestBlock
b  -> NextItem TestBlock -> m (NextItem TestBlock)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (NextItem TestBlock -> m (NextItem TestBlock))
-> NextItem TestBlock -> m (NextItem TestBlock)
forall a b. (a -> b) -> a -> b
$ TestBlock -> NextItem TestBlock
forall blk. blk -> NextItem blk
NextItem TestBlock
b
                          Maybe TestBlock
Nothing -> TestName -> m (NextItem TestBlock)
forall a. HasCallStack => TestName -> a
error TestName
blockNotFound

blockNotFound :: String
blockNotFound :: TestName
blockNotFound = [TestName] -> TestName
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
          TestName
"dbStreamAPI: "
        , TestName
"invariant violation: "
        , TestName
"block in dbChain not present in dbBlocks"
        ]

{-------------------------------------------------------------------------------
  New SUT
-------------------------------------------------------------------------------}

openLedgerDB ::
     Complete LedgerDbFlavorArgs IO
  -> ChainDB IO
  -> LedgerDbCfg (ExtLedgerState TestBlock)
  -> SomeHasFS IO
  -> IO (LedgerDB' IO TestBlock, TestInternals' IO TestBlock)
openLedgerDB :: Complete LedgerDbFlavorArgs IO
-> ChainDB IO
-> LedgerDbCfg (ExtLedgerState TestBlock)
-> SomeHasFS IO
-> IO (LedgerDB' IO TestBlock, TestInternals' IO TestBlock)
openLedgerDB Complete LedgerDbFlavorArgs IO
flavArgs ChainDB IO
env LedgerDbCfg (ExtLedgerState TestBlock)
cfg SomeHasFS IO
fs = do
  (stream, volBlocks) <- SecurityParam
-> ChainDB IO -> IO (StreamAPI IO TestBlock TestBlock, [TestBlock])
forall (m :: * -> *).
IOLike m =>
SecurityParam
-> ChainDB m -> m (StreamAPI m TestBlock TestBlock, [TestBlock])
dbStreamAPI (LedgerDbCfg (ExtLedgerState TestBlock)
-> HKD Identity SecurityParam
forall (f :: * -> *) (l :: LedgerStateKind).
LedgerDbCfgF f l -> HKD f SecurityParam
ledgerDbCfgSecParam LedgerDbCfg (ExtLedgerState TestBlock)
cfg) ChainDB IO
env
  let getBlock RealPoint TestBlock
f = TestBlock
-> RealPoint TestBlock
-> Map (RealPoint TestBlock) TestBlock
-> TestBlock
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (TestName -> TestBlock
forall a. HasCallStack => TestName -> a
error TestName
blockNotFound) RealPoint TestBlock
f (Map (RealPoint TestBlock) TestBlock -> TestBlock)
-> IO (Map (RealPoint TestBlock) TestBlock) -> IO TestBlock
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictTVar IO (Map (RealPoint TestBlock) TestBlock)
-> IO (Map (RealPoint TestBlock) TestBlock)
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> m a
readTVarIO (ChainDB IO -> StrictTVar IO (Map (RealPoint TestBlock) TestBlock)
forall (m :: * -> *).
ChainDB m -> StrictTVar m (Map (RealPoint TestBlock) TestBlock)
dbBlocks ChainDB IO
env)
  replayGoal <- fmap (realPointToPoint . last . Map.keys) . atomically $ readTVar (dbBlocks env)
  rr <- unsafeNewRegistry
  let args = SnapshotPolicyArgs
-> HKD Identity (IO (ExtLedgerState TestBlock ValuesMK))
-> HKD Identity (SomeHasFS IO)
-> LedgerDbCfg (ExtLedgerState TestBlock)
-> Tracer IO (TraceEvent TestBlock)
-> Complete LedgerDbFlavorArgs IO
-> HKD Identity (ResourceRegistry IO)
-> QueryBatchSize
-> Maybe DiskSnapshot
-> LedgerDbArgs Identity IO TestBlock
forall (f :: * -> *) (m :: * -> *) blk.
SnapshotPolicyArgs
-> HKD f (m (ExtLedgerState blk ValuesMK))
-> HKD f (SomeHasFS m)
-> LedgerDbCfgF f (ExtLedgerState blk)
-> Tracer m (TraceEvent blk)
-> LedgerDbFlavorArgs f m
-> HKD f (ResourceRegistry m)
-> QueryBatchSize
-> Maybe DiskSnapshot
-> LedgerDbArgs f m blk
LedgerDbArgs
               (SnapshotInterval -> NumOfDiskSnapshots -> SnapshotPolicyArgs
SnapshotPolicyArgs SnapshotInterval
DisableSnapshots NumOfDiskSnapshots
DefaultNumOfDiskSnapshots)
               (ExtLedgerState TestBlock ValuesMK
-> IO (ExtLedgerState TestBlock ValuesMK)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ExtLedgerState TestBlock ValuesMK
genesis)
               SomeHasFS IO
HKD Identity (SomeHasFS IO)
fs
               LedgerDbCfg (ExtLedgerState TestBlock)
cfg
               Tracer IO (TraceEvent TestBlock)
forall (m :: * -> *) a. Applicative m => Tracer m a
nullTracer
               Complete LedgerDbFlavorArgs IO
flavArgs
               HKD Identity (ResourceRegistry IO)
ResourceRegistry IO
rr
               QueryBatchSize
DefaultQueryBatchSize
               Maybe DiskSnapshot
forall a. Maybe a
Nothing
  (ldb, _, od) <- case flavArgs of
    LedgerDbFlavorArgsV1 LedgerDbFlavorArgs Identity IO
bss ->
      let initDb :: InitDB
  (DbChangelog' TestBlock, BackingStore' IO TestBlock) IO TestBlock
initDb = LedgerDbArgs Identity IO TestBlock
-> LedgerDbFlavorArgs Identity IO
-> (RealPoint TestBlock -> IO TestBlock)
-> InitDB
     (DbChangelog' TestBlock, BackingStore' IO TestBlock) IO TestBlock
forall (m :: * -> *) blk.
(LedgerSupportsProtocol blk, IOLike m,
 LedgerDbSerialiseConstraints blk, HasHardForkHistory blk,
 LedgerSupportsLedgerDB blk) =>
Complete LedgerDbArgs m blk
-> Complete LedgerDbFlavorArgs m
-> ResolveBlock m blk
-> InitDB (DbChangelog' blk, BackingStore' m blk) m blk
V1.mkInitDb
                       LedgerDbArgs Identity IO TestBlock
args
                       LedgerDbFlavorArgs Identity IO
bss
                       RealPoint TestBlock -> IO TestBlock
getBlock
        in
          LedgerDbArgs Identity IO TestBlock
-> InitDB
     (DbChangelog' TestBlock, BackingStore' IO TestBlock) IO TestBlock
-> StreamAPI IO TestBlock TestBlock
-> Point TestBlock
-> IO (LedgerDB' IO TestBlock, Word64, TestInternals' IO TestBlock)
forall (m :: * -> *) blk db.
(IOLike m, LedgerSupportsProtocol blk, InspectLedger blk,
 HasCallStack) =>
Complete LedgerDbArgs m blk
-> InitDB db m blk
-> StreamAPI m blk blk
-> Point blk
-> m (LedgerDB' m blk, Word64, TestInternals' m blk)
openDBInternal LedgerDbArgs Identity IO TestBlock
args InitDB
  (DbChangelog' TestBlock, BackingStore' IO TestBlock) IO TestBlock
initDb StreamAPI IO TestBlock TestBlock
stream Point TestBlock
replayGoal
    LedgerDbFlavorArgsV2 LedgerDbFlavorArgs Identity IO
bss ->
        let initDb :: InitDB (LedgerSeq' IO TestBlock) IO TestBlock
initDb = LedgerDbArgs Identity IO TestBlock
-> LedgerDbFlavorArgs Identity IO
-> (RealPoint TestBlock -> IO TestBlock)
-> InitDB (LedgerSeq' IO TestBlock) IO TestBlock
forall (m :: * -> *) blk.
(LedgerSupportsProtocol blk, IOLike m,
 LedgerDbSerialiseConstraints blk, HasHardForkHistory blk,
 LedgerSupportsInMemoryLedgerDB blk) =>
Complete LedgerDbArgs m blk
-> Complete LedgerDbFlavorArgs m
-> ResolveBlock m blk
-> InitDB (LedgerSeq' m blk) m blk
V2.mkInitDb
                       LedgerDbArgs Identity IO TestBlock
args
                       LedgerDbFlavorArgs Identity IO
bss
                       RealPoint TestBlock -> IO TestBlock
getBlock
        in
          LedgerDbArgs Identity IO TestBlock
-> InitDB (LedgerSeq' IO TestBlock) IO TestBlock
-> StreamAPI IO TestBlock TestBlock
-> Point TestBlock
-> IO (LedgerDB' IO TestBlock, Word64, TestInternals' IO TestBlock)
forall (m :: * -> *) blk db.
(IOLike m, LedgerSupportsProtocol blk, InspectLedger blk,
 HasCallStack) =>
Complete LedgerDbArgs m blk
-> InitDB db m blk
-> StreamAPI m blk blk
-> Point blk
-> m (LedgerDB' m blk, Word64, TestInternals' m blk)
openDBInternal LedgerDbArgs Identity IO TestBlock
args InitDB (LedgerSeq' IO TestBlock) IO TestBlock
initDb StreamAPI IO TestBlock TestBlock
stream Point TestBlock
replayGoal
  withRegistry $ \ResourceRegistry IO
reg -> do
    vr <- LedgerDB' IO TestBlock
-> (ExtLedgerState TestBlock ~ ExtLedgerState TestBlock) =>
   ResourceRegistry IO
   -> (TraceValidateEvent TestBlock -> IO ())
   -> BlockCache TestBlock
   -> Word64
   -> [Header TestBlock]
   -> IO (ValidateResult IO (ExtLedgerState TestBlock) TestBlock)
forall (m :: * -> *) (l :: LedgerStateKind) blk.
LedgerDB m l blk
-> (l ~ ExtLedgerState blk) =>
   ResourceRegistry m
   -> (TraceValidateEvent blk -> m ())
   -> BlockCache blk
   -> Word64
   -> [Header blk]
   -> m (ValidateResult m l blk)
validateFork LedgerDB' IO TestBlock
ldb ResourceRegistry IO
reg (IO () -> TraceValidateEvent TestBlock -> IO ()
forall a b. a -> b -> a
const (IO () -> TraceValidateEvent TestBlock -> IO ())
-> IO () -> TraceValidateEvent TestBlock -> IO ()
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) BlockCache TestBlock
forall blk. BlockCache blk
BlockCache.empty Word64
0 ((TestBlock -> Header TestBlock)
-> [TestBlock] -> [Header TestBlock]
forall a b. (a -> b) -> [a] -> [b]
map TestBlock -> Header TestBlock
forall blk. GetHeader blk => blk -> Header blk
getHeader [TestBlock]
volBlocks)
    case vr of
      ValidateSuccessful Forker IO (ExtLedgerState TestBlock) TestBlock
forker -> do
        STM IO () -> IO ()
forall a. HasCallStack => STM IO a -> IO a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (Forker IO (ExtLedgerState TestBlock) TestBlock -> STM IO ()
forall (m :: * -> *) (l :: LedgerStateKind) blk.
Forker m l blk -> STM m ()
forkerCommit Forker IO (ExtLedgerState TestBlock) TestBlock
forker)
        Forker IO (ExtLedgerState TestBlock) TestBlock -> IO ()
forall (m :: * -> *) (l :: LedgerStateKind) blk.
Forker m l blk -> m ()
forkerClose Forker IO (ExtLedgerState TestBlock) TestBlock
forker
      ValidateResult IO (ExtLedgerState TestBlock) TestBlock
_ -> TestName -> IO ()
forall a. HasCallStack => TestName -> a
error TestName
"Couldn't restart the chain, failed to apply volatile blocks!"
  pure (ldb, od)

{-------------------------------------------------------------------------------
  RunModel
-------------------------------------------------------------------------------}

-- | The environment for the monad in which we will run the test
data Environment =
  Environment
    (LedgerDB' IO TestBlock)
    (TestInternals' IO TestBlock)
    (ChainDB IO)
    (SecurityParam -> TestArguments IO)
    (SomeHasFS IO)
    (IO ())

instance RunModel Model (StateT Environment IO) where

  perform :: forall a.
Typeable a =>
Model
-> Action Model a
-> LookUp (StateT Environment IO)
-> StateT
     Environment
     IO
     (PerformResult (Error Model) (Realized (StateT Environment IO) a))
perform Model
_ (Init SecurityParam
secParam) LookUp (StateT Environment IO)
_ = do
    Environment _ _ chainDb mkArgs fs cleanup <- StateT Environment IO Environment
forall s (m :: * -> *). MonadState s m => m s
get
    (ldb, testInternals) <- lift $ do
      let args = SecurityParam -> TestArguments IO
mkArgs SecurityParam
secParam
      openLedgerDB (argFlavorArgs args) chainDb (argLedgerDbCfg args) fs
    put (Environment ldb testInternals chainDb mkArgs fs cleanup)

  perform Model
_ Action Model a
R:ActionModela a
WipeLedgerDB LookUp (StateT Environment IO)
_ = do
    Environment _ testInternals _ _ _ _ <- StateT Environment IO Environment
forall s (m :: * -> *). MonadState s m => m s
get
    lift $ wipeLedgerDB testInternals

  perform Model
_ Action Model a
R:ActionModela a
GetState LookUp (StateT Environment IO)
_ = do
    Environment ldb _ _ _ _ _ <- StateT Environment IO Environment
forall s (m :: * -> *). MonadState s m => m s
get
    lift $ atomically $ (,) <$> getImmutableTip ldb <*> getVolatileTip ldb

  perform Model
_ Action Model a
R:ActionModela a
ForceTakeSnapshot LookUp (StateT Environment IO)
_ = do
    Environment _ testInternals _ _ _ _ <- StateT Environment IO Environment
forall s (m :: * -> *). MonadState s m => m s
get
    lift $ takeSnapshotNOW testInternals TakeAtImmutableTip Nothing

  perform Model
_ (ValidateAndCommit Word64
n [TestBlock]
blks) LookUp (StateT Environment IO)
_ = do
      Environment ldb _ chainDb _ _ _ <- StateT Environment IO Environment
forall s (m :: * -> *). MonadState s m => m s
get
      lift $ do
        atomically $ modifyTVar (dbBlocks chainDb) $
           repeatedly (uncurry Map.insert) (map (\TestBlock
b -> (TestBlock -> RealPoint TestBlock
forall blk. HasHeader blk => blk -> RealPoint blk
blockRealPoint TestBlock
b, TestBlock
b)) blks)
        withRegistry $ \ResourceRegistry IO
rr -> do
          vr <- LedgerDB' IO TestBlock
-> (ExtLedgerState TestBlock ~ ExtLedgerState TestBlock) =>
   ResourceRegistry IO
   -> (TraceValidateEvent TestBlock -> IO ())
   -> BlockCache TestBlock
   -> Word64
   -> [Header TestBlock]
   -> IO (ValidateResult IO (ExtLedgerState TestBlock) TestBlock)
forall (m :: * -> *) (l :: LedgerStateKind) blk.
LedgerDB m l blk
-> (l ~ ExtLedgerState blk) =>
   ResourceRegistry m
   -> (TraceValidateEvent blk -> m ())
   -> BlockCache blk
   -> Word64
   -> [Header blk]
   -> m (ValidateResult m l blk)
validateFork LedgerDB' IO TestBlock
ldb ResourceRegistry IO
rr (IO () -> TraceValidateEvent TestBlock -> IO ()
forall a b. a -> b -> a
const (IO () -> TraceValidateEvent TestBlock -> IO ())
-> IO () -> TraceValidateEvent TestBlock -> IO ()
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) BlockCache TestBlock
forall blk. BlockCache blk
BlockCache.empty Word64
n ((TestBlock -> Header TestBlock)
-> [TestBlock] -> [Header TestBlock]
forall a b. (a -> b) -> [a] -> [b]
map TestBlock -> Header TestBlock
forall blk. GetHeader blk => blk -> Header blk
getHeader [TestBlock]
blks)
          case vr of
            ValidateSuccessful Forker IO (ExtLedgerState TestBlock) TestBlock
forker -> do
              STM IO () -> IO ()
forall a. HasCallStack => STM IO a -> IO a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM IO () -> IO ()) -> STM IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ StrictTVar IO [RealPoint TestBlock]
-> ([RealPoint TestBlock] -> [RealPoint TestBlock]) -> STM IO ()
forall (m :: * -> *) a.
MonadSTM m =>
StrictTVar m a -> (a -> a) -> STM m ()
modifyTVar (ChainDB IO -> StrictTVar IO [RealPoint TestBlock]
forall (m :: * -> *).
ChainDB m -> StrictTVar m [RealPoint TestBlock]
dbChain ChainDB IO
chainDb) ([RealPoint TestBlock] -> [RealPoint TestBlock]
forall a. [a] -> [a]
reverse ((TestBlock -> RealPoint TestBlock)
-> [TestBlock] -> [RealPoint TestBlock]
forall a b. (a -> b) -> [a] -> [b]
map TestBlock -> RealPoint TestBlock
forall blk. HasHeader blk => blk -> RealPoint blk
blockRealPoint [TestBlock]
blks) [RealPoint TestBlock]
-> [RealPoint TestBlock] -> [RealPoint TestBlock]
forall a. [a] -> [a] -> [a]
++)
              STM IO () -> IO ()
forall a. HasCallStack => STM IO a -> IO a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (Forker IO (ExtLedgerState TestBlock) TestBlock -> STM IO ()
forall (m :: * -> *) (l :: LedgerStateKind) blk.
Forker m l blk -> STM m ()
forkerCommit Forker IO (ExtLedgerState TestBlock) TestBlock
forker)
              Forker IO (ExtLedgerState TestBlock) TestBlock -> IO ()
forall (m :: * -> *) (l :: LedgerStateKind) blk.
Forker m l blk -> m ()
forkerClose Forker IO (ExtLedgerState TestBlock) TestBlock
forker
            ValidateExceededRollBack{} -> TestName -> IO ()
forall a. HasCallStack => TestName -> a
error TestName
"Unexpected Rollback"
            ValidateLedgerError (AnnLedgerError Forker IO (ExtLedgerState TestBlock) TestBlock
forker RealPoint TestBlock
_ LedgerErr (ExtLedgerState TestBlock)
_) -> Forker IO (ExtLedgerState TestBlock) TestBlock -> IO ()
forall (m :: * -> *) (l :: LedgerStateKind) blk.
Forker m l blk -> m ()
forkerClose Forker IO (ExtLedgerState TestBlock) TestBlock
forker IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TestName -> IO ()
forall a. HasCallStack => TestName -> a
error TestName
"Unexpected ledger error"

  perform state :: Model
state@(Model TheBlockChain
_ SecurityParam
secParam) (DropAndRestore Word64
n) LookUp (StateT Environment IO)
lk = do
    Environment _ testInternals chainDb _ _ _ <- StateT Environment IO Environment
forall s (m :: * -> *). MonadState s m => m s
get
    lift $ do
      atomically $ modifyTVar (dbChain chainDb) (drop (fromIntegral n))
      closeLedgerDB testInternals
    perform state (Init secParam) lk

  perform Model
_ Action Model a
R:ActionModela a
TruncateSnapshots LookUp (StateT Environment IO)
_ = do
    Environment _ testInternals _ _ _ _ <- StateT Environment IO Environment
forall s (m :: * -> *). MonadState s m => m s
get
    lift $ truncateSnapshots testInternals

  perform Model
UnInit Action Model a
_ LookUp (StateT Environment IO)
_ = TestName -> StateT Environment IO a
forall a. HasCallStack => TestName -> a
error TestName
"Uninitialized model created a command different than Init"


  -- NOTE
  --
  -- In terms of postcondition, we only need to check that the immutable and
  -- volatile tip are the right ones. By the blocks validating one on top of
  -- each other it already implies that having the right volatile tip means that
  -- we have the right whole chain.
  postcondition :: forall a.
(Model, Model)
-> Action Model a
-> LookUp (StateT Environment IO)
-> Realized (StateT Environment IO) a
-> PostconditionM (StateT Environment IO) Bool
postcondition (Model TheBlockChain
chain SecurityParam
secParam, Model
_) Action Model a
R:ActionModela a
GetState LookUp (StateT Environment IO)
_ (ExtLedgerState TestBlock EmptyMK
imm, ExtLedgerState TestBlock EmptyMK
vol) =
    let volSt :: ExtLedgerState TestBlock EmptyMK
volSt = (ExtLedgerState TestBlock ValuesMK
 -> ExtLedgerState TestBlock EmptyMK)
-> ((TestBlock, ExtLedgerState TestBlock ValuesMK)
    -> ExtLedgerState TestBlock EmptyMK)
-> Either
     (ExtLedgerState TestBlock ValuesMK)
     (TestBlock, ExtLedgerState TestBlock ValuesMK)
-> ExtLedgerState TestBlock EmptyMK
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ExtLedgerState TestBlock ValuesMK
-> ExtLedgerState TestBlock EmptyMK
forall (l :: LedgerStateKind) (mk :: MapKind).
HasLedgerTables l =>
l mk -> l EmptyMK
forgetLedgerTables (ExtLedgerState TestBlock ValuesMK
-> ExtLedgerState TestBlock EmptyMK
forall (l :: LedgerStateKind) (mk :: MapKind).
HasLedgerTables l =>
l mk -> l EmptyMK
forgetLedgerTables (ExtLedgerState TestBlock ValuesMK
 -> ExtLedgerState TestBlock EmptyMK)
-> ((TestBlock, ExtLedgerState TestBlock ValuesMK)
    -> ExtLedgerState TestBlock ValuesMK)
-> (TestBlock, ExtLedgerState TestBlock ValuesMK)
-> ExtLedgerState TestBlock EmptyMK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TestBlock, ExtLedgerState TestBlock ValuesMK)
-> ExtLedgerState TestBlock ValuesMK
forall a b. (a, b) -> b
snd) (TheBlockChain
-> Either
     (ExtLedgerState TestBlock ValuesMK)
     (TestBlock, ExtLedgerState TestBlock ValuesMK)
forall v a b. Anchorable v a b => AnchoredSeq v a b -> Either a b
AS.head TheBlockChain
chain)
        immSt :: ExtLedgerState TestBlock EmptyMK
immSt = (ExtLedgerState TestBlock ValuesMK
 -> ExtLedgerState TestBlock EmptyMK)
-> ((TestBlock, ExtLedgerState TestBlock ValuesMK)
    -> ExtLedgerState TestBlock EmptyMK)
-> Either
     (ExtLedgerState TestBlock ValuesMK)
     (TestBlock, ExtLedgerState TestBlock ValuesMK)
-> ExtLedgerState TestBlock EmptyMK
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ExtLedgerState TestBlock ValuesMK
-> ExtLedgerState TestBlock EmptyMK
forall (l :: LedgerStateKind) (mk :: MapKind).
HasLedgerTables l =>
l mk -> l EmptyMK
forgetLedgerTables (ExtLedgerState TestBlock ValuesMK
-> ExtLedgerState TestBlock EmptyMK
forall (l :: LedgerStateKind) (mk :: MapKind).
HasLedgerTables l =>
l mk -> l EmptyMK
forgetLedgerTables (ExtLedgerState TestBlock ValuesMK
 -> ExtLedgerState TestBlock EmptyMK)
-> ((TestBlock, ExtLedgerState TestBlock ValuesMK)
    -> ExtLedgerState TestBlock ValuesMK)
-> (TestBlock, ExtLedgerState TestBlock ValuesMK)
-> ExtLedgerState TestBlock EmptyMK
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TestBlock, ExtLedgerState TestBlock ValuesMK)
-> ExtLedgerState TestBlock ValuesMK
forall a b. (a, b) -> b
snd) (TheBlockChain
-> Either
     (ExtLedgerState TestBlock ValuesMK)
     (TestBlock, ExtLedgerState TestBlock ValuesMK)
forall v a b. Anchorable v a b => AnchoredSeq v a b -> Either a b
AS.head (Int -> TheBlockChain -> TheBlockChain
forall v a b.
Anchorable v a b =>
Int -> AnchoredSeq v a b -> AnchoredSeq v a b
AS.dropNewest (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64 -> Int) -> Word64 -> Int
forall a b. (a -> b) -> a -> b
$ NonZero Word64 -> Word64
forall a. NonZero a -> a
BT.unNonZero (NonZero Word64 -> Word64) -> NonZero Word64 -> Word64
forall a b. (a -> b) -> a -> b
$ SecurityParam -> NonZero Word64
maxRollbacks SecurityParam
secParam) TheBlockChain
chain))
    in do
       TestName -> PostconditionM (StateT Environment IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName -> PostconditionM (StateT Environment IO) ())
-> TestName -> PostconditionM (StateT Environment IO) ()
forall a b. (a -> b) -> a -> b
$ [TestName] -> TestName
unlines [ TestName
"VolSt: ", ExtLedgerState TestBlock EmptyMK -> TestName
forall a. Show a => a -> TestName
show ExtLedgerState TestBlock EmptyMK
volSt
                                    , TestName
"VolSut: ", ExtLedgerState TestBlock EmptyMK -> TestName
forall a. Show a => a -> TestName
show ExtLedgerState TestBlock EmptyMK
vol
                                    , TestName
"ImmSt: ", ExtLedgerState TestBlock EmptyMK -> TestName
forall a. Show a => a -> TestName
show ExtLedgerState TestBlock EmptyMK
immSt
                                    , TestName
"ImmSut: ", ExtLedgerState TestBlock EmptyMK -> TestName
forall a. Show a => a -> TestName
show ExtLedgerState TestBlock EmptyMK
imm
                                    ]
       Bool -> PostconditionM (StateT Environment IO) Bool
forall a. a -> PostconditionM (StateT Environment IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> PostconditionM (StateT Environment IO) Bool)
-> Bool -> PostconditionM (StateT Environment IO) Bool
forall a b. (a -> b) -> a -> b
$ ExtLedgerState TestBlock EmptyMK
volSt ExtLedgerState TestBlock EmptyMK
-> ExtLedgerState TestBlock EmptyMK -> Bool
forall a. Eq a => a -> a -> Bool
== ExtLedgerState TestBlock EmptyMK
vol Bool -> Bool -> Bool
&& ExtLedgerState TestBlock EmptyMK
immSt ExtLedgerState TestBlock EmptyMK
-> ExtLedgerState TestBlock EmptyMK -> Bool
forall a. Eq a => a -> a -> Bool
== ExtLedgerState TestBlock EmptyMK
imm
  postcondition (Model, Model)
_ Action Model a
_ LookUp (StateT Environment IO)
_ Realized (StateT Environment IO) a
_ = Bool -> PostconditionM (StateT Environment IO) Bool
forall a. a -> PostconditionM (StateT Environment IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True