{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# 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 (Tracer (..))
import Data.Functor.Contravariant ((>$<))
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 qualified Ouroboros.Consensus.Storage.LedgerDB as LedgerDB
import Ouroboros.Consensus.Storage.LedgerDB.Snapshots
import Ouroboros.Consensus.Storage.LedgerDB.V1 as V1
import Ouroboros.Consensus.Storage.LedgerDB.V1.Args hiding
  ( LedgerDbBackendArgs
  )
import qualified Ouroboros.Consensus.Storage.LedgerDB.V1.BackingStore as V1
import qualified Ouroboros.Consensus.Storage.LedgerDB.V1.BackingStore.Impl.InMemory as V1.InMemory
import qualified Ouroboros.Consensus.Storage.LedgerDB.V1.BackingStore.Impl.LMDB as LMDB
import Ouroboros.Consensus.Storage.LedgerDB.V1.Snapshots as V1
import Ouroboros.Consensus.Storage.LedgerDB.V2 as V2
import Ouroboros.Consensus.Storage.LedgerDB.V2.Backend as V2
import qualified Ouroboros.Consensus.Storage.LedgerDB.V2.InMemory as V2.InMemory
import qualified Ouroboros.Consensus.Storage.LedgerDB.V2.LSM as LSM
import Ouroboros.Consensus.Util hiding (Some)
import Ouroboros.Consensus.Util.IOLike
import qualified Ouroboros.Network.AnchoredSeq as AS
import Ouroboros.Network.Protocol.LocalStateQuery.Type
import qualified System.Directory as Dir
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.FilePath as FilePath
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 qualified Test.QuickCheck.Monadic as QC
import Test.QuickCheck.StateModel
import Test.Tasty
import Test.Tasty.QuickCheck (frequency, tabulate, testProperty)
import Test.Util.TestBlock hiding
  ( TestBlock
  , TestBlockCodecConfig
  , TestBlockStorageConfig
  )

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

prop_sequential ::
  Int ->
  (SecurityParam -> LSM.Salt -> FilePath -> TestArguments IO) ->
  IO (FilePath, IO ()) ->
  IO (SomeHasFS IO, IO ()) ->
  Actions Model ->
  QC.Property
prop_sequential :: Int
-> (SecurityParam -> Word64 -> String -> TestArguments IO)
-> IO (String, IO ())
-> IO (SomeHasFS IO, IO ())
-> Actions Model
-> Property
prop_sequential Int
maxSuccess SecurityParam -> Word64 -> String -> TestArguments IO
mkTestArguments IO (String, IO ())
getDiskDir IO (SomeHasFS IO, IO ())
fsOps Actions Model
actions =
  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
$
    (StateT Environment IO Property -> Property)
-> PropertyM (StateT Environment IO) () -> Property
forall a (m :: * -> *).
(Testable a, Monad m) =>
(m Property -> Property) -> PropertyM m a -> Property
QC.monadic StateT Environment IO Property -> Property
runner (PropertyM (StateT Environment IO) () -> Property)
-> PropertyM (StateT Environment IO) () -> Property
forall a b. (a -> b) -> a -> b
$
      PropertyM (StateT Environment IO) (Annotated Model, Env)
-> PropertyM (StateT Environment IO) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
Monad.void (PropertyM (StateT Environment IO) (Annotated Model, Env)
 -> PropertyM (StateT Environment IO) ())
-> PropertyM (StateT Environment IO) (Annotated Model, Env)
-> PropertyM (StateT Environment IO) ()
forall a b. (a -> b) -> a -> b
$
        Actions Model
-> PropertyM (StateT Environment IO) (Annotated Model, Env)
forall state (m :: * -> *) e.
(StateModel state, RunModel state m, e ~ Error state m,
 forall a. IsPerformResult e a) =>
Actions state -> PropertyM m (Annotated state, Env)
runActions (Actions Model
 -> PropertyM (StateT Environment IO) (Annotated Model, Env))
-> Actions Model
-> PropertyM (StateT Environment IO) (Annotated Model, Env)
forall a b. (a -> b) -> a -> b
$
          Actions Model
actions
 where
  setup :: IO Environment
  setup :: IO Environment
setup = do
    cdb <- IO (ChainDB IO)
forall (m :: * -> *). (MonadIO m, IOLike m) => m (ChainDB m)
initChainDB
    rr <- unsafeNewRegistry
    initialEnvironment fsOps getDiskDir mkTestArguments cdb rr

  cleanup :: Environment -> IO ()
  cleanup :: Environment -> IO ()
cleanup (Environment LedgerDB' IO TestBlock
_ TestInternals' IO TestBlock
testInternals ChainDB IO
_ SecurityParam -> Word64 -> TestArguments IO
_ SomeHasFS IO
_ IO NumOpenHandles
_ IO ()
clean ResourceRegistry IO
registry) = do
    ResourceRegistry IO -> IO ()
forall (m :: * -> *).
(MonadMask m, MonadThread m, MonadSTM m, HasCallStack) =>
ResourceRegistry m -> m ()
closeRegistry ResourceRegistry IO
registry
    TestInternals' IO TestBlock -> IO ()
forall (m :: * -> *) (l :: LedgerStateKind) blk.
TestInternals m l blk -> m ()
closeLedgerDB TestInternals' IO TestBlock
testInternals
    IO ()
clean

  runner :: StateT Environment IO QC.Property -> QC.Property
  runner :: StateT Environment IO Property -> Property
runner StateT Environment IO Property
mprop =
    IO Property -> Property
forall prop. Testable prop => IO prop -> Property
QC.ioProperty (IO Property -> Property) -> IO Property -> Property
forall a b. (a -> b) -> a -> b
$
      IO Environment
-> (Environment -> IO ())
-> (Environment -> IO Property)
-> IO Property
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
forall (m :: * -> *) a b c.
MonadThrow m =>
m a -> (a -> m b) -> (a -> m c) -> m c
bracket IO Environment
setup Environment -> IO ()
cleanup ((Environment -> IO Property) -> IO Property)
-> (Environment -> IO Property) -> IO Property
forall a b. (a -> b) -> a -> b
$
        \Environment
env0 -> do
          (prop1, env1) <- StateT Environment IO Property
-> Environment -> IO (Property, Environment)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT Environment IO Property
mprop Environment
env0
          p2 <- checkNoLeakedHandles env1
          pure $ prop1 QC..&&. p2

-- | 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 -> LSM.Salt -> FilePath -> TestArguments IO) ->
  ChainDB IO ->
  ResourceRegistry IO ->
  IO Environment
initialEnvironment :: IO (SomeHasFS IO, IO ())
-> IO (String, IO ())
-> (SecurityParam -> Word64 -> String -> TestArguments IO)
-> ChainDB IO
-> ResourceRegistry IO
-> IO Environment
initialEnvironment IO (SomeHasFS IO, IO ())
fsOps IO (String, IO ())
getDiskDir SecurityParam -> Word64 -> String -> TestArguments IO
mkTestArguments ChainDB IO
cdb ResourceRegistry IO
rr = do
  (sfs, cleanupFS) <- IO (SomeHasFS IO, IO ())
fsOps
  (diskDir, cleanupDisk) <- getDiskDir
  pure $
    Environment
      undefined
      (TestInternals undefined undefined undefined undefined undefined (pure ()) (pure 0))
      cdb
      (\SecurityParam
sp Word64
st -> SecurityParam -> Word64 -> String -> TestArguments IO
mkTestArguments SecurityParam
sp Word64
st String
diskDir)
      sfs
      (pure $ NumOpenHandles 0)
      (cleanupFS >> cleanupDisk)
      rr

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

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

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

realFilePath :: String -> IO (FilePath, IO ())
realFilePath :: String -> IO (String, IO ())
realFilePath String
l = IO (String, IO ()) -> IO (String, IO ())
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (String, IO ()) -> IO (String, IO ()))
-> IO (String, IO ()) -> IO (String, IO ())
forall a b. (a -> b) -> a -> b
$ do
  tmpdir <- (String -> String -> String
FilePath.</> (String
"test_" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
l)) (String -> String) -> IO String -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO String
Dir.getTemporaryDirectory
  Dir.createDirectoryIfMissing False tmpdir
  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 String
Dir.getTemporaryDirectory
  tmpdir <- Temp.createTempDirectory systmpdir "init_standalone_db"
  pure (SomeHasFS $ FSIO.ioHasFS $ MountPoint tmpdir, Dir.removeDirectoryRecursive tmpdir)

inMemV1TestArguments ::
  SecurityParam ->
  LSM.Salt ->
  FilePath ->
  TestArguments IO
inMemV1TestArguments :: SecurityParam -> Word64 -> String -> TestArguments IO
inMemV1TestArguments SecurityParam
secParam Word64
_ String
_ =
  TestArguments
    { argFlavorArgs :: LedgerDbBackendArgs IO TestBlock
argFlavorArgs =
        LedgerDbBackendArgs IO (ExtLedgerState TestBlock)
-> LedgerDbBackendArgs IO TestBlock
forall (m :: * -> *) blk.
LedgerDbBackendArgs m (ExtLedgerState blk)
-> LedgerDbBackendArgs m blk
LedgerDbBackendArgsV1 (LedgerDbBackendArgs IO (ExtLedgerState TestBlock)
 -> LedgerDbBackendArgs IO TestBlock)
-> LedgerDbBackendArgs IO (ExtLedgerState TestBlock)
-> LedgerDbBackendArgs IO TestBlock
forall a b. (a -> b) -> a -> b
$ FlushFrequency
-> SomeBackendArgs IO (ExtLedgerState TestBlock)
-> LedgerDbBackendArgs IO (ExtLedgerState TestBlock)
forall (m :: * -> *) (l :: LedgerStateKind).
FlushFrequency -> SomeBackendArgs m l -> LedgerDbBackendArgs m l
V1Args FlushFrequency
DisableFlushing (SomeBackendArgs IO (ExtLedgerState TestBlock)
 -> LedgerDbBackendArgs IO (ExtLedgerState TestBlock))
-> SomeBackendArgs IO (ExtLedgerState TestBlock)
-> LedgerDbBackendArgs IO (ExtLedgerState TestBlock)
forall a b. (a -> b) -> a -> b
$ Args IO Mem -> SomeBackendArgs IO (ExtLedgerState TestBlock)
forall (m :: * -> *) backend (l :: LedgerStateKind).
Backend m backend l =>
Args m backend -> SomeBackendArgs m l
V1.SomeBackendArgs Args IO Mem
forall (m :: * -> *). Args m Mem
V1.InMemory.InMemArgs
    , argLedgerDbCfg :: LedgerDbCfg (ExtLedgerState TestBlock)
argLedgerDbCfg = SecurityParam -> LedgerDbCfg (ExtLedgerState TestBlock)
extLedgerDbConfig SecurityParam
secParam
    }

inMemV2TestArguments ::
  SecurityParam ->
  LSM.Salt ->
  FilePath ->
  TestArguments IO
inMemV2TestArguments :: SecurityParam -> Word64 -> String -> TestArguments IO
inMemV2TestArguments SecurityParam
secParam Word64
_ String
_ =
  TestArguments
    { argFlavorArgs :: LedgerDbBackendArgs IO TestBlock
argFlavorArgs = SomeBackendArgs IO TestBlock -> LedgerDbBackendArgs IO TestBlock
forall (m :: * -> *) blk.
SomeBackendArgs m blk -> LedgerDbBackendArgs m blk
LedgerDbBackendArgsV2 (SomeBackendArgs IO TestBlock -> LedgerDbBackendArgs IO TestBlock)
-> SomeBackendArgs IO TestBlock -> LedgerDbBackendArgs IO TestBlock
forall a b. (a -> b) -> a -> b
$ Args IO Mem -> SomeBackendArgs IO TestBlock
forall (m :: * -> *) backend blk.
Backend m backend blk =>
Args m backend -> SomeBackendArgs m blk
SomeBackendArgs Args IO Mem
forall (m :: * -> *). Args m Mem
V2.InMemory.InMemArgs
    , argLedgerDbCfg :: LedgerDbCfg (ExtLedgerState TestBlock)
argLedgerDbCfg = SecurityParam -> LedgerDbCfg (ExtLedgerState TestBlock)
extLedgerDbConfig SecurityParam
secParam
    }

lsmTestArguments ::
  SecurityParam ->
  LSM.Salt ->
  FilePath ->
  TestArguments IO
lsmTestArguments :: SecurityParam -> Word64 -> String -> TestArguments IO
lsmTestArguments SecurityParam
secParam Word64
salt String
fp =
  TestArguments
    { argFlavorArgs :: LedgerDbBackendArgs IO TestBlock
argFlavorArgs =
        SomeBackendArgs IO TestBlock -> LedgerDbBackendArgs IO TestBlock
forall (m :: * -> *) blk.
SomeBackendArgs m blk -> LedgerDbBackendArgs m blk
LedgerDbBackendArgsV2 (SomeBackendArgs IO TestBlock -> LedgerDbBackendArgs IO TestBlock)
-> SomeBackendArgs IO TestBlock -> LedgerDbBackendArgs IO TestBlock
forall a b. (a -> b) -> a -> b
$
          Args IO LSM -> SomeBackendArgs IO TestBlock
forall (m :: * -> *) backend blk.
Backend m backend blk =>
Args m backend -> SomeBackendArgs m blk
SomeBackendArgs (Args IO LSM -> SomeBackendArgs IO TestBlock)
-> Args IO LSM -> SomeBackendArgs IO TestBlock
forall a b. (a -> b) -> a -> b
$
            FsPath
-> Word64
-> (ResourceRegistry IO
    -> IO (ResourceKey IO, SomeHasFSAndBlockIO IO))
-> Args IO LSM
forall (m :: * -> *).
FsPath
-> Word64
-> (ResourceRegistry m -> m (ResourceKey m, SomeHasFSAndBlockIO m))
-> Args m LSM
LSM.LSMArgs ([String] -> FsPath
mkFsPath ([String] -> FsPath) -> [String] -> FsPath
forall a b. (a -> b) -> a -> b
$ String -> [String]
FilePath.splitDirectories String
fp) Word64
salt (String
-> ResourceRegistry IO
-> IO (ResourceKey IO, SomeHasFSAndBlockIO IO)
LSM.stdMkBlockIOFS String
fp)
    , argLedgerDbCfg :: LedgerDbCfg (ExtLedgerState TestBlock)
argLedgerDbCfg = SecurityParam -> LedgerDbCfg (ExtLedgerState TestBlock)
extLedgerDbConfig SecurityParam
secParam
    }

lmdbTestArguments ::
  SecurityParam ->
  LSM.Salt ->
  FilePath ->
  TestArguments IO
lmdbTestArguments :: SecurityParam -> Word64 -> String -> TestArguments IO
lmdbTestArguments SecurityParam
secParam Word64
_ String
fp =
  TestArguments
    { argFlavorArgs :: LedgerDbBackendArgs IO TestBlock
argFlavorArgs =
        LedgerDbBackendArgs IO (ExtLedgerState TestBlock)
-> LedgerDbBackendArgs IO TestBlock
forall (m :: * -> *) blk.
LedgerDbBackendArgs m (ExtLedgerState blk)
-> LedgerDbBackendArgs m blk
LedgerDbBackendArgsV1 (LedgerDbBackendArgs IO (ExtLedgerState TestBlock)
 -> LedgerDbBackendArgs IO TestBlock)
-> LedgerDbBackendArgs IO (ExtLedgerState TestBlock)
-> LedgerDbBackendArgs IO TestBlock
forall a b. (a -> b) -> a -> b
$
          FlushFrequency
-> SomeBackendArgs IO (ExtLedgerState TestBlock)
-> LedgerDbBackendArgs IO (ExtLedgerState TestBlock)
forall (m :: * -> *) (l :: LedgerStateKind).
FlushFrequency -> SomeBackendArgs m l -> LedgerDbBackendArgs m l
V1Args FlushFrequency
DisableFlushing (SomeBackendArgs IO (ExtLedgerState TestBlock)
 -> LedgerDbBackendArgs IO (ExtLedgerState TestBlock))
-> SomeBackendArgs IO (ExtLedgerState TestBlock)
-> LedgerDbBackendArgs IO (ExtLedgerState TestBlock)
forall a b. (a -> b) -> a -> b
$
            Args IO LMDB -> SomeBackendArgs IO (ExtLedgerState TestBlock)
forall (m :: * -> *) backend (l :: LedgerStateKind).
Backend m backend l =>
Args m backend -> SomeBackendArgs m l
V1.SomeBackendArgs (Args IO LMDB -> SomeBackendArgs IO (ExtLedgerState TestBlock))
-> Args IO LMDB -> SomeBackendArgs IO (ExtLedgerState TestBlock)
forall a b. (a -> b) -> a -> b
$
              String -> LMDBLimits -> Dict MonadIOPrim IO -> Args IO LMDB
forall (m :: * -> *).
String -> LMDBLimits -> Dict MonadIOPrim m -> Args m LMDB
LMDB.LMDBBackingStoreArgs String
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 -> String -> String
[Model] -> String -> String
Model -> String
(Int -> Model -> String -> String)
-> (Model -> String) -> ([Model] -> String -> String) -> Show Model
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Model -> String -> String
showsPrec :: Int -> Model -> String -> String
$cshow :: Model -> String
show :: Model -> String
$cshowList :: [Model] -> String -> String
showList :: [Model] -> String -> String
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
_ = String -> Model
forall a. HasCallStack => String -> a
error String
"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 = String -> Model
forall a. HasCallStack => String -> a
error String
"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 -> LSM.Salt -> Action Model ()
    ForceTakeSnapshot :: Action Model ()
    GetState ::
      Action Model (ExtLedgerState TestBlock EmptyMK, ExtLedgerState TestBlock EmptyMK)
    Init :: SecurityParam -> LSM.Salt -> Action Model ()
    ValidateAndCommit :: Word64 -> [TestBlock] -> Action Model ()
    -- \| This action is used only to observe the side effects of closing an
    -- uncommitted forker, to ensure all handles are properly deallocated.
    OpenAndCloseForker :: Action Model ()

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

  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))
-> Gen (Action Model ()) -> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SecurityParam -> Word64 -> Action Model ()
Init (SecurityParam -> Word64 -> Action Model ())
-> Gen SecurityParam -> Gen (Word64 -> Action Model ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen SecurityParam
forall a. Arbitrary a => Gen a
QC.arbitrary Gen (Word64 -> Action Model ())
-> Gen Word64 -> Gen (Action Model ())
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Word64
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))
-> Gen (Action Model ()) -> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Word64 -> Word64 -> Action Model ()
DropAndRestore (Word64 -> Word64 -> Action Model ())
-> Gen Word64 -> Gen (Word64 -> 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) Gen (Word64 -> Action Model ())
-> Gen Word64 -> Gen (Action Model ())
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Word64
forall a. Arbitrary a => Gen a
QC.arbitrary))
      ,
        ( 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 <-
              [(Int, Gen Word64)] -> Gen Word64
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
                [ (Int
10, (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
QC.choose (Word64
0, Word64
maxRollback))
                , -- Sometimes generate invalid 'ValidateAndCommit's for
                  -- negative testing.
                  (Int
1, (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
QC.choose (Word64
maxRollback Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1, Word64
maxRollback Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
5))
                ]
            numNewBlocks <- QC.choose (numRollback, numRollback + 2)
            let
              chain' = case Word64 -> Model -> Model
modelRollback Word64
numRollback Model
model of
                Model
UnInit -> String -> TheBlockChain
forall a. HasCallStack => String -> a
error String
"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)
      , (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 ()
OpenAndCloseForker)
      ]

  initialState :: Model
initialState = Model
UnInit

  nextState :: forall a. Typeable a => Model -> Action Model a -> Var a -> Model
nextState Model
_ (Init SecurityParam
secParam Word64
_) 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 Word64
_) Var a
_var = Word64 -> Model -> Model
modelRollback Word64
n Model
state
  nextState Model
state Action Model a
R:ActionModela a
OpenAndCloseForker Var a
_var = Model
state
  nextState Model
UnInit Action Model a
_ Var a
_ = String -> Model
forall a. HasCallStack => String -> a
error String
"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 -> WithOrigin SlotNo -> SlotNo
forall t. t -> WithOrigin t -> t
fromWithOrigin SlotNo
0 (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'))
         where
          chain' :: TheBlockChain
chain' = 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
  precondition Model
_ Init{} = Bool
False
  precondition Model
_ Action Model a
_ = Bool
True

  validFailingAction :: forall a. Model -> Action Model a -> Bool
validFailingAction Model{} ValidateAndCommit{} = Bool
True
  validFailingAction Model
_ Action Model a
_ = Bool
False

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

-- | Mocked chain db
data ChainDB m = ChainDB
  { forall (m :: * -> *).
ChainDB m -> StrictTVar m (Map (RealPoint TestBlock) TestBlock)
dbBlocks :: StrictTVar m (Map (RealPoint TestBlock) TestBlock)
  -- ^ Block storage
  , forall (m :: * -> *).
ChainDB m -> StrictTVar m [RealPoint TestBlock]
dbChain :: StrictTVar m [RealPoint TestBlock]
  -- ^ Current chain and corresponding ledger state
  }

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 -> String -> m (NextItem TestBlock)
forall a. HasCallStack => String -> a
error String
blockNotFound

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

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

openLedgerDB ::
  LedgerDbBackendArgs IO TestBlock ->
  ChainDB IO ->
  LedgerDbCfg (ExtLedgerState TestBlock) ->
  SomeHasFS IO ->
  ResourceRegistry IO ->
  IO (LedgerDB' IO TestBlock, TestInternals' IO TestBlock, IO NumOpenHandles)
openLedgerDB :: LedgerDbBackendArgs IO TestBlock
-> ChainDB IO
-> LedgerDbCfg (ExtLedgerState TestBlock)
-> SomeHasFS IO
-> ResourceRegistry IO
-> IO
     (LedgerDB' IO TestBlock, TestInternals' IO TestBlock,
      IO NumOpenHandles)
openLedgerDB LedgerDbBackendArgs IO TestBlock
flavArgs ChainDB IO
env LedgerDbCfg (ExtLedgerState TestBlock)
cfg SomeHasFS IO
fs ResourceRegistry IO
rr = 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 (String -> TestBlock
forall a. HasCallStack => String -> a
error String
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)
  (tracer, getNumOpenHandles) <- mkTrackOpenHandles
  let args =
        SnapshotPolicyArgs
-> HKD Identity (IO (ExtLedgerState TestBlock ValuesMK))
-> HKD Identity (SomeHasFS IO)
-> LedgerDbCfg (ExtLedgerState TestBlock)
-> Tracer IO (TraceEvent TestBlock)
-> LedgerDbBackendArgs IO TestBlock
-> 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)
-> LedgerDbBackendArgs m blk
-> 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)
tracer
          LedgerDbBackendArgs IO TestBlock
flavArgs
          HKD Identity (ResourceRegistry IO)
ResourceRegistry IO
rr
          QueryBatchSize
DefaultQueryBatchSize
          Maybe DiskSnapshot
forall a. Maybe a
Nothing
  (ldb, _, od) <- case lgrBackendArgs args of
    LedgerDbBackendArgsV1 LedgerDbBackendArgs IO (ExtLedgerState TestBlock)
bss ->
      let snapManager :: SnapshotManager
  IO
  (ReadLocked IO)
  TestBlock
  (StrictTVar IO (DbChangelog' TestBlock),
   BackingStore' IO TestBlock)
snapManager = LedgerDbArgs Identity IO TestBlock
-> SnapshotManager
     IO
     (ReadLocked IO)
     TestBlock
     (StrictTVar IO (DbChangelog' TestBlock),
      BackingStore' IO TestBlock)
forall (m :: * -> *) blk.
(IOLike m, LedgerDbSerialiseConstraints blk,
 LedgerSupportsProtocol blk) =>
Complete LedgerDbArgs m blk
-> SnapshotManager
     m
     (ReadLocked m)
     blk
     (StrictTVar m (DbChangelog' blk), BackingStore' m blk)
V1.snapshotManager LedgerDbArgs Identity IO TestBlock
args
          initDb :: InitDB
  (DbChangelog' TestBlock, ResourceKey IO,
   BackingStore' IO TestBlock)
  IO
  TestBlock
initDb =
            LedgerDbArgs Identity IO TestBlock
-> LedgerDbBackendArgs IO (ExtLedgerState TestBlock)
-> (RealPoint TestBlock -> IO TestBlock)
-> SnapshotManager
     IO
     (ReadLocked IO)
     TestBlock
     (StrictTVar IO (DbChangelog' TestBlock),
      BackingStore' IO TestBlock)
-> GetVolatileSuffix IO TestBlock
-> InitDB
     (DbChangelog' TestBlock, ResourceKey IO,
      BackingStore' IO TestBlock)
     IO
     TestBlock
forall (m :: * -> *) blk.
(LedgerSupportsProtocol blk, IOLike m, HasHardForkHistory blk,
 LedgerSupportsLedgerDB blk) =>
Complete LedgerDbArgs m blk
-> LedgerDbBackendArgs m (ExtLedgerState blk)
-> ResolveBlock m blk
-> SnapshotManagerV1 m blk
-> GetVolatileSuffix m blk
-> InitDB
     (DbChangelog' blk, ResourceKey m, BackingStore' m blk) m blk
V1.mkInitDb
              LedgerDbArgs Identity IO TestBlock
args
              LedgerDbBackendArgs IO (ExtLedgerState TestBlock)
bss
              RealPoint TestBlock -> IO TestBlock
getBlock
              SnapshotManager
  IO
  (ReadLocked IO)
  TestBlock
  (StrictTVar IO (DbChangelog' TestBlock),
   BackingStore' IO TestBlock)
snapManager
              (SecurityParam -> GetVolatileSuffix IO TestBlock
forall (m :: * -> *) blk.
IOLike m =>
SecurityParam -> GetVolatileSuffix m blk
praosGetVolatileSuffix (SecurityParam -> GetVolatileSuffix IO TestBlock)
-> SecurityParam -> GetVolatileSuffix IO TestBlock
forall a b. (a -> b) -> a -> b
$ LedgerDbCfg (ExtLedgerState TestBlock)
-> HKD Identity SecurityParam
forall (f :: * -> *) (l :: LedgerStateKind).
LedgerDbCfgF f l -> HKD f SecurityParam
ledgerDbCfgSecParam LedgerDbCfg (ExtLedgerState TestBlock)
cfg)
       in LedgerDbArgs Identity IO TestBlock
-> InitDB
     (DbChangelog' TestBlock, ResourceKey IO,
      BackingStore
        IO
        (LedgerTables (ExtLedgerState TestBlock) KeysMK)
        Token
        (LedgerTables (ExtLedgerState TestBlock) ValuesMK)
        (LedgerTables (ExtLedgerState TestBlock) DiffMK))
     IO
     TestBlock
-> SnapshotManager
     IO
     (ReadLocked IO)
     TestBlock
     (StrictTVar IO (DbChangelog' TestBlock),
      BackingStore
        IO
        (LedgerTables (ExtLedgerState TestBlock) KeysMK)
        Token
        (LedgerTables (ExtLedgerState TestBlock) ValuesMK)
        (LedgerTables (ExtLedgerState TestBlock) DiffMK))
-> StreamAPI IO TestBlock TestBlock
-> Point TestBlock
-> IO (LedgerDB' IO TestBlock, Word64, TestInternals' IO TestBlock)
forall (m :: * -> *) blk db (n :: * -> *) st.
(IOLike m, LedgerSupportsProtocol blk, InspectLedger blk,
 HasCallStack) =>
Complete LedgerDbArgs m blk
-> InitDB db m blk
-> SnapshotManager m n blk st
-> StreamAPI m blk blk
-> Point blk
-> m (LedgerDB' m blk, Word64, TestInternals' m blk)
openDBInternal LedgerDbArgs Identity IO TestBlock
args InitDB
  (DbChangelog' TestBlock, ResourceKey IO,
   BackingStore' IO TestBlock)
  IO
  TestBlock
InitDB
  (DbChangelog' TestBlock, ResourceKey IO,
   BackingStore
     IO
     (LedgerTables (ExtLedgerState TestBlock) KeysMK)
     Token
     (LedgerTables (ExtLedgerState TestBlock) ValuesMK)
     (LedgerTables (ExtLedgerState TestBlock) DiffMK))
  IO
  TestBlock
initDb SnapshotManager
  IO
  (ReadLocked IO)
  TestBlock
  (StrictTVar IO (DbChangelog' TestBlock),
   BackingStore' IO TestBlock)
SnapshotManager
  IO
  (ReadLocked IO)
  TestBlock
  (StrictTVar IO (DbChangelog' TestBlock),
   BackingStore
     IO
     (LedgerTables (ExtLedgerState TestBlock) KeysMK)
     Token
     (LedgerTables (ExtLedgerState TestBlock) ValuesMK)
     (LedgerTables (ExtLedgerState TestBlock) DiffMK))
snapManager StreamAPI IO TestBlock TestBlock
stream Point TestBlock
replayGoal
    LedgerDbBackendArgsV2 (V2.SomeBackendArgs Args IO backend
bArgs) -> do
      res <-
        Proxy TestBlock
-> Tracer IO LedgerDBV2Trace
-> Args IO backend
-> ResourceRegistry IO
-> SomeHasFS IO
-> IO (Resources IO backend)
forall (m :: * -> *) backend blk.
Backend m backend blk =>
Proxy blk
-> Tracer m LedgerDBV2Trace
-> Args m backend
-> ResourceRegistry m
-> SomeHasFS m
-> m (Resources m backend)
mkResources
          (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @TestBlock)
          (FlavorImplSpecificTrace -> TraceEvent TestBlock
forall blk. FlavorImplSpecificTrace -> TraceEvent blk
LedgerDBFlavorImplEvent (FlavorImplSpecificTrace -> TraceEvent TestBlock)
-> (LedgerDBV2Trace -> FlavorImplSpecificTrace)
-> LedgerDBV2Trace
-> TraceEvent TestBlock
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LedgerDBV2Trace -> FlavorImplSpecificTrace
FlavorImplSpecificTraceV2 (LedgerDBV2Trace -> TraceEvent TestBlock)
-> Tracer IO (TraceEvent TestBlock) -> Tracer IO LedgerDBV2Trace
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
>$< LedgerDbArgs Identity IO TestBlock
-> Tracer IO (TraceEvent TestBlock)
forall (f :: * -> *) (m :: * -> *) blk.
LedgerDbArgs f m blk -> Tracer m (TraceEvent blk)
lgrTracer LedgerDbArgs Identity IO TestBlock
args)
          Args IO backend
bArgs
          (LedgerDbArgs Identity IO TestBlock
-> HKD Identity (ResourceRegistry IO)
forall (f :: * -> *) (m :: * -> *) blk.
LedgerDbArgs f m blk -> HKD f (ResourceRegistry m)
lgrRegistry LedgerDbArgs Identity IO TestBlock
args)
          (LedgerDbArgs Identity IO TestBlock -> HKD Identity (SomeHasFS IO)
forall (f :: * -> *) (m :: * -> *) blk.
LedgerDbArgs f m blk -> HKD f (SomeHasFS m)
lgrHasFS LedgerDbArgs Identity IO TestBlock
args)
      let snapManager =
            Proxy TestBlock
-> Resources IO backend
-> CodecConfig TestBlock
-> Tracer IO (TraceSnapshotEvent TestBlock)
-> SomeHasFS IO
-> SnapshotManager
     IO IO TestBlock (StateRef IO (ExtLedgerState TestBlock))
forall (m :: * -> *) backend blk.
Backend m backend blk =>
Proxy blk
-> Resources m backend
-> CodecConfig blk
-> Tracer m (TraceSnapshotEvent blk)
-> SomeHasFS m
-> SnapshotManager m m blk (StateRef m (ExtLedgerState blk))
V2.snapshotManager
              (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @TestBlock)
              Resources IO backend
res
              (TopLevelConfig TestBlock -> CodecConfig TestBlock
forall blk. TopLevelConfig blk -> CodecConfig blk
configCodec (TopLevelConfig TestBlock -> CodecConfig TestBlock)
-> (LedgerDbCfg (ExtLedgerState TestBlock)
    -> TopLevelConfig TestBlock)
-> LedgerDbCfg (ExtLedgerState TestBlock)
-> CodecConfig TestBlock
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtLedgerCfg TestBlock -> TopLevelConfig TestBlock
forall blk. ExtLedgerCfg blk -> TopLevelConfig blk
getExtLedgerCfg (ExtLedgerCfg TestBlock -> TopLevelConfig TestBlock)
-> (LedgerDbCfg (ExtLedgerState TestBlock)
    -> ExtLedgerCfg TestBlock)
-> LedgerDbCfg (ExtLedgerState TestBlock)
-> TopLevelConfig TestBlock
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LedgerDbCfg (ExtLedgerState TestBlock)
-> HKD Identity (LedgerCfg (ExtLedgerState TestBlock))
LedgerDbCfg (ExtLedgerState TestBlock) -> ExtLedgerCfg TestBlock
forall (f :: * -> *) (l :: LedgerStateKind).
LedgerDbCfgF f l -> HKD f (LedgerCfg l)
ledgerDbCfg (LedgerDbCfg (ExtLedgerState TestBlock) -> CodecConfig TestBlock)
-> LedgerDbCfg (ExtLedgerState TestBlock) -> CodecConfig TestBlock
forall a b. (a -> b) -> a -> b
$ LedgerDbArgs Identity IO TestBlock
-> LedgerDbCfg (ExtLedgerState TestBlock)
forall (f :: * -> *) (m :: * -> *) blk.
LedgerDbArgs f m blk -> LedgerDbCfgF f (ExtLedgerState blk)
lgrConfig LedgerDbArgs Identity IO TestBlock
args)
              (TraceSnapshotEvent TestBlock -> TraceEvent TestBlock
forall blk. TraceSnapshotEvent blk -> TraceEvent blk
LedgerDBSnapshotEvent (TraceSnapshotEvent TestBlock -> TraceEvent TestBlock)
-> Tracer IO (TraceEvent TestBlock)
-> Tracer IO (TraceSnapshotEvent TestBlock)
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
>$< LedgerDbArgs Identity IO TestBlock
-> Tracer IO (TraceEvent TestBlock)
forall (f :: * -> *) (m :: * -> *) blk.
LedgerDbArgs f m blk -> Tracer m (TraceEvent blk)
lgrTracer LedgerDbArgs Identity IO TestBlock
args)
              (LedgerDbArgs Identity IO TestBlock -> HKD Identity (SomeHasFS IO)
forall (f :: * -> *) (m :: * -> *) blk.
LedgerDbArgs f m blk -> HKD f (SomeHasFS m)
lgrHasFS LedgerDbArgs Identity IO TestBlock
args)
      let initDb = LedgerDbArgs Identity IO TestBlock
-> (RealPoint TestBlock -> IO TestBlock)
-> SnapshotManager
     IO IO TestBlock (StateRef IO (ExtLedgerState TestBlock))
-> GetVolatileSuffix IO TestBlock
-> Resources IO backend
-> InitDB (LedgerSeq' IO TestBlock) IO TestBlock
forall (m :: * -> *) blk backend.
(LedgerSupportsProtocol blk, LedgerDbSerialiseConstraints blk,
 HasHardForkHistory blk, Backend m backend blk, IOLike m) =>
Complete LedgerDbArgs m blk
-> ResolveBlock m blk
-> SnapshotManagerV2 m blk
-> GetVolatileSuffix m blk
-> Resources m backend
-> InitDB (LedgerSeq' m blk) m blk
V2.mkInitDb LedgerDbArgs Identity IO TestBlock
args RealPoint TestBlock -> IO TestBlock
getBlock SnapshotManager
  IO IO TestBlock (StateRef IO (ExtLedgerState TestBlock))
snapManager (SecurityParam -> GetVolatileSuffix IO TestBlock
forall (m :: * -> *) blk.
IOLike m =>
SecurityParam -> GetVolatileSuffix m blk
praosGetVolatileSuffix (SecurityParam -> GetVolatileSuffix IO TestBlock)
-> SecurityParam -> GetVolatileSuffix IO TestBlock
forall a b. (a -> b) -> a -> b
$ LedgerDbCfg (ExtLedgerState TestBlock)
-> HKD Identity SecurityParam
forall (f :: * -> *) (l :: LedgerStateKind).
LedgerDbCfgF f l -> HKD f SecurityParam
ledgerDbCfgSecParam LedgerDbCfg (ExtLedgerState TestBlock)
cfg) Resources IO backend
res
      openDBInternal args initDb snapManager stream 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
_ -> String -> IO ()
forall a. HasCallStack => String -> a
error String
"Couldn't restart the chain, failed to apply volatile blocks!"
  pure (ldb, od, getNumOpenHandles)

{-------------------------------------------------------------------------------
  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 -> LSM.Salt -> TestArguments IO)
      (SomeHasFS IO)
      !(IO NumOpenHandles)
      !(IO ())
      !(ResourceRegistry IO)

data LedgerDBError = ErrorValidateExceededRollback

instance RunModel Model (StateT Environment IO) where
  type Error Model (StateT Environment IO) = LedgerDBError

  perform :: forall a.
Typeable a =>
Model
-> Action Model a
-> LookUp
-> StateT
     Environment IO (PerformResult Model (StateT Environment IO) a)
perform Model
_ (Init SecurityParam
secParam Word64
salt) LookUp
_ = do
    Environment _ _ chainDb mkArgs fs _ cleanup rr <- StateT Environment IO Environment
forall s (m :: * -> *). MonadState s m => m s
get
    (ldb, testInternals, getNumOpenHandles) <- lift $ do
      let args = SecurityParam -> Word64 -> TestArguments IO
mkArgs SecurityParam
secParam Word64
salt
      -- TODO after a drop and restore we restart the db but the session has been closed below where I wrote blahblahblah
      openLedgerDB (argFlavorArgs args) chainDb (argLedgerDbCfg args) fs rr
    put (Environment ldb testInternals chainDb mkArgs fs getNumOpenHandles cleanup rr)
    pure $ pure ()
  perform Model
_ Action Model a
R:ActionModela a
WipeLedgerDB LookUp
_ = do
    Environment _ testInternals _ _ _ _ _ _ <- StateT Environment IO Environment
forall s (m :: * -> *). MonadState s m => m s
get
    lift $ wipeLedgerDB testInternals
    pure $ pure ()
  perform Model
_ Action Model a
R:ActionModela a
GetState LookUp
_ = do
    Environment ldb _ _ _ _ _ _ _ <- StateT Environment IO Environment
forall s (m :: * -> *). MonadState s m => m s
get
    lift $ fmap pure $ atomically $ (,) <$> getImmutableTip ldb <*> getVolatileTip ldb
  perform Model
_ Action Model a
R:ActionModela a
ForceTakeSnapshot LookUp
_ = do
    Environment _ testInternals _ _ _ _ _ _ <- StateT Environment IO Environment
forall s (m :: * -> *). MonadState s m => m s
get
    lift $ takeSnapshotNOW testInternals TakeAtImmutableTip Nothing
    pure $ pure ()
  perform Model
_ (ValidateAndCommit Word64
n [TestBlock]
blks) LookUp
_ = 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]) -> STM IO ())
-> ([RealPoint TestBlock] -> [RealPoint TestBlock]) -> STM IO ()
forall a b. (a -> b) -> a -> b
$
                ([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]
++) ([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
n)
            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
            Either LedgerDBError () -> IO (Either LedgerDBError ())
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either LedgerDBError () -> IO (Either LedgerDBError ()))
-> Either LedgerDBError () -> IO (Either LedgerDBError ())
forall a b. (a -> b) -> a -> b
$ () -> Either LedgerDBError ()
forall a. a -> Either LedgerDBError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          ValidateExceededRollBack{} -> Either LedgerDBError () -> IO (Either LedgerDBError ())
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either LedgerDBError () -> IO (Either LedgerDBError ()))
-> Either LedgerDBError () -> IO (Either LedgerDBError ())
forall a b. (a -> b) -> a -> b
$ LedgerDBError -> Either LedgerDBError ()
forall a b. a -> Either a b
Left LedgerDBError
ErrorValidateExceededRollback
          ValidateLedgerError (AnnLedgerError Forker IO (ExtLedgerState TestBlock) TestBlock
forker RealPoint TestBlock
_ LedgerErr (ExtLedgerState TestBlock)
err) -> 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 (Either LedgerDBError ()) -> IO (Either LedgerDBError ())
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> IO (Either LedgerDBError ())
forall a. HasCallStack => String -> a
error (String
"Unexpected ledger error" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> ExtValidationError TestBlock -> String
forall a. Show a => a -> String
show LedgerErr (ExtLedgerState TestBlock)
ExtValidationError TestBlock
err)
  perform state :: Model
state@(Model TheBlockChain
_ SecurityParam
secParam) (DropAndRestore Word64
n Word64
salt) LookUp
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))
      -- blahblahblah
      closeLedgerDB testInternals
    perform state (Init secParam salt) lk
  perform Model
_ Action Model a
R:ActionModela a
OpenAndCloseForker LookUp
_ = do
    Environment ldb _ _ _ _ _ _ _ <- StateT Environment IO Environment
forall s (m :: * -> *). MonadState s m => m s
get
    lift $ withRegistry $ \ResourceRegistry IO
rr -> do
      eFrk <- LedgerDB' IO TestBlock
-> ResourceRegistry IO
-> Target (Point TestBlock)
-> IO
     (Either
        GetForkerError (Forker IO (ExtLedgerState TestBlock) TestBlock))
forall (m :: * -> *) (l :: LedgerStateKind) blk.
LedgerDB m l blk
-> ResourceRegistry m
-> Target (Point blk)
-> m (Either GetForkerError (Forker m l blk))
LedgerDB.getForkerAtTarget LedgerDB' IO TestBlock
ldb ResourceRegistry IO
rr Target (Point TestBlock)
forall point. Target point
VolatileTip
      case eFrk of
        Left GetForkerError
err -> String -> IO ()
forall a. HasCallStack => String -> a
error (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Impossible: can't acquire forker at tip: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> GetForkerError -> String
forall a. Show a => a -> String
show GetForkerError
err
        Right Forker IO (ExtLedgerState TestBlock) TestBlock
frk -> Forker IO (ExtLedgerState TestBlock) TestBlock -> IO ()
forall (m :: * -> *) (l :: LedgerStateKind) blk.
Forker m l blk -> m ()
forkerClose Forker IO (ExtLedgerState TestBlock) TestBlock
frk
    pure $ pure ()
  perform Model
_ Action Model a
R:ActionModela a
TruncateSnapshots LookUp
_ = do
    Environment _ testInternals _ _ _ _ _ _ <- StateT Environment IO Environment
forall s (m :: * -> *). MonadState s m => m s
get
    lift $ truncateSnapshots testInternals
    pure $ pure ()
  perform Model
UnInit Action Model a
_ LookUp
_ = String -> StateT Environment IO (Either LedgerDBError a)
forall a. HasCallStack => String -> a
error String
"Uninitialized model created a command different than Init"

  monitoring :: forall a.
(Model, Model)
-> Action Model a
-> LookUp
-> Either (Error Model (StateT Environment IO)) a
-> Property
-> Property
monitoring (Model, Model)
_ (ValidateAndCommit Word64
n [TestBlock]
_) LookUp
_ Either (Error Model (StateT Environment IO)) a
_ = String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Rollback depths" [Word64 -> String
forall a. Show a => a -> String
show Word64
n]
  monitoring (Model, Model)
_ Action Model a
_ LookUp
_ Either (Error Model (StateT Environment IO)) a
_ = Property -> Property
forall a. a -> a
id

  -- 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
-> a
-> PostconditionM (StateT Environment IO) Bool
postcondition (Model TheBlockChain
chain SecurityParam
secParam, Model
_) Action Model a
R:ActionModela a
GetState LookUp
_ (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
          String -> PostconditionM (StateT Environment IO) ()
forall (m :: * -> *). Monad m => String -> PostconditionM m ()
counterexamplePost (String -> PostconditionM (StateT Environment IO) ())
-> String -> PostconditionM (StateT Environment IO) ()
forall a b. (a -> b) -> a -> b
$
            [String] -> String
unlines
              [ String
"VolSt: "
              , ExtLedgerState TestBlock EmptyMK -> String
forall a. Show a => a -> String
show ExtLedgerState TestBlock EmptyMK
volSt
              , String
"VolSut: "
              , ExtLedgerState TestBlock EmptyMK -> String
forall a. Show a => a -> String
show ExtLedgerState TestBlock EmptyMK
vol
              , String
"ImmSt: "
              , ExtLedgerState TestBlock EmptyMK -> String
forall a. Show a => a -> String
show ExtLedgerState TestBlock EmptyMK
immSt
              , String
"ImmSut: "
              , ExtLedgerState TestBlock EmptyMK -> String
forall a. Show a => a -> String
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
_ 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

  postconditionOnFailure :: forall a.
(Model, Model)
-> Action Model a
-> LookUp
-> Either (Error Model (StateT Environment IO)) a
-> PostconditionM (StateT Environment IO) Bool
postconditionOnFailure (Model, Model)
_ ValidateAndCommit{} LookUp
_ Either (Error Model (StateT Environment IO)) a
res = case Either (Error Model (StateT Environment IO)) a
res of
    Right () -> Bool
False Bool
-> PostconditionM (StateT Environment IO) ()
-> PostconditionM (StateT Environment IO) Bool
forall a b.
a
-> PostconditionM (StateT Environment IO) b
-> PostconditionM (StateT Environment IO) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> PostconditionM (StateT Environment IO) ()
forall (m :: * -> *). Monad m => String -> PostconditionM m ()
counterexamplePost String
"Unexpected success on invalid ValidateAndCommit"
    Left Error Model (StateT Environment IO)
LedgerDBError
ErrorValidateExceededRollback -> 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
  postconditionOnFailure (Model, Model)
_ Action Model a
_ LookUp
_ Either (Error Model (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

{-------------------------------------------------------------------------------
  Additional checks
-------------------------------------------------------------------------------}

newtype NumOpenHandles = NumOpenHandles Word64
  deriving newtype (Int -> NumOpenHandles -> String -> String
[NumOpenHandles] -> String -> String
NumOpenHandles -> String
(Int -> NumOpenHandles -> String -> String)
-> (NumOpenHandles -> String)
-> ([NumOpenHandles] -> String -> String)
-> Show NumOpenHandles
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> NumOpenHandles -> String -> String
showsPrec :: Int -> NumOpenHandles -> String -> String
$cshow :: NumOpenHandles -> String
show :: NumOpenHandles -> String
$cshowList :: [NumOpenHandles] -> String -> String
showList :: [NumOpenHandles] -> String -> String
Show, NumOpenHandles -> NumOpenHandles -> Bool
(NumOpenHandles -> NumOpenHandles -> Bool)
-> (NumOpenHandles -> NumOpenHandles -> Bool) -> Eq NumOpenHandles
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NumOpenHandles -> NumOpenHandles -> Bool
== :: NumOpenHandles -> NumOpenHandles -> Bool
$c/= :: NumOpenHandles -> NumOpenHandles -> Bool
/= :: NumOpenHandles -> NumOpenHandles -> Bool
Eq, Int -> NumOpenHandles
NumOpenHandles -> Int
NumOpenHandles -> [NumOpenHandles]
NumOpenHandles -> NumOpenHandles
NumOpenHandles -> NumOpenHandles -> [NumOpenHandles]
NumOpenHandles
-> NumOpenHandles -> NumOpenHandles -> [NumOpenHandles]
(NumOpenHandles -> NumOpenHandles)
-> (NumOpenHandles -> NumOpenHandles)
-> (Int -> NumOpenHandles)
-> (NumOpenHandles -> Int)
-> (NumOpenHandles -> [NumOpenHandles])
-> (NumOpenHandles -> NumOpenHandles -> [NumOpenHandles])
-> (NumOpenHandles -> NumOpenHandles -> [NumOpenHandles])
-> (NumOpenHandles
    -> NumOpenHandles -> NumOpenHandles -> [NumOpenHandles])
-> Enum NumOpenHandles
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: NumOpenHandles -> NumOpenHandles
succ :: NumOpenHandles -> NumOpenHandles
$cpred :: NumOpenHandles -> NumOpenHandles
pred :: NumOpenHandles -> NumOpenHandles
$ctoEnum :: Int -> NumOpenHandles
toEnum :: Int -> NumOpenHandles
$cfromEnum :: NumOpenHandles -> Int
fromEnum :: NumOpenHandles -> Int
$cenumFrom :: NumOpenHandles -> [NumOpenHandles]
enumFrom :: NumOpenHandles -> [NumOpenHandles]
$cenumFromThen :: NumOpenHandles -> NumOpenHandles -> [NumOpenHandles]
enumFromThen :: NumOpenHandles -> NumOpenHandles -> [NumOpenHandles]
$cenumFromTo :: NumOpenHandles -> NumOpenHandles -> [NumOpenHandles]
enumFromTo :: NumOpenHandles -> NumOpenHandles -> [NumOpenHandles]
$cenumFromThenTo :: NumOpenHandles
-> NumOpenHandles -> NumOpenHandles -> [NumOpenHandles]
enumFromThenTo :: NumOpenHandles
-> NumOpenHandles -> NumOpenHandles -> [NumOpenHandles]
Enum)

mkTrackOpenHandles :: IO (Tracer IO (TraceEvent TestBlock), IO NumOpenHandles)
mkTrackOpenHandles :: IO (Tracer IO (TraceEvent TestBlock), IO NumOpenHandles)
mkTrackOpenHandles = do
  varOpen <- NumOpenHandles -> IO (StrictTVar IO NumOpenHandles)
forall (m :: * -> *) a. MonadSTM m => a -> m (StrictTVar m a)
uncheckedNewTVarM (Word64 -> NumOpenHandles
NumOpenHandles Word64
0)
  let tracer = (TraceEvent TestBlock -> IO ()) -> Tracer IO (TraceEvent TestBlock)
forall (m :: * -> *) a. (a -> m ()) -> Tracer m a
Tracer ((TraceEvent TestBlock -> IO ())
 -> Tracer IO (TraceEvent TestBlock))
-> (TraceEvent TestBlock -> IO ())
-> Tracer IO (TraceEvent TestBlock)
forall a b. (a -> b) -> a -> b
$ \case
        LedgerDBFlavorImplEvent (FlavorImplSpecificTraceV2 LedgerDBV2Trace
ev) ->
          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 NumOpenHandles
-> (NumOpenHandles -> NumOpenHandles) -> STM IO ()
forall (m :: * -> *) a.
MonadSTM m =>
StrictTVar m a -> (a -> a) -> STM m ()
modifyTVar StrictTVar IO NumOpenHandles
varOpen ((NumOpenHandles -> NumOpenHandles) -> STM IO ())
-> (NumOpenHandles -> NumOpenHandles) -> STM IO ()
forall a b. (a -> b) -> a -> b
$ case LedgerDBV2Trace
ev of
            LedgerDBV2Trace
V2.TraceLedgerTablesHandleCreate -> NumOpenHandles -> NumOpenHandles
forall a. Enum a => a -> a
succ
            LedgerDBV2Trace
V2.TraceLedgerTablesHandleClose -> NumOpenHandles -> NumOpenHandles
forall a. Enum a => a -> a
pred
            LedgerDBV2Trace
_ -> NumOpenHandles -> NumOpenHandles
forall a. a -> a
id
        TraceEvent TestBlock
_ -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  pure (tracer, readTVarIO varOpen)

-- | Check that we didn't leak any 'LedgerTablesHandle's (with V2 only).
checkNoLeakedHandles :: Environment -> IO QC.Property
checkNoLeakedHandles :: Environment -> IO Property
checkNoLeakedHandles (Environment LedgerDB' IO TestBlock
_ TestInternals' IO TestBlock
testInternals ChainDB IO
_ SecurityParam -> Word64 -> TestArguments IO
_ SomeHasFS IO
_ IO NumOpenHandles
getNumOpenHandles IO ()
_ ResourceRegistry IO
_) = do
  expected <- Word64 -> NumOpenHandles
NumOpenHandles (Word64 -> NumOpenHandles) -> IO Word64 -> IO NumOpenHandles
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TestInternals' IO TestBlock -> IO Word64
forall (m :: * -> *) (l :: LedgerStateKind) blk.
TestInternals m l blk -> m Word64
LedgerDB.getNumLedgerTablesHandles TestInternals' IO TestBlock
testInternals
  actual <- getNumOpenHandles
  pure $
    QC.counterexample
      ("leaked handles, expected " <> show expected <> ", but actual " <> show actual)
      (actual == expected)