{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralisedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep
  ( BackingStoreState (..)
  , RealEnv (..)
  , RealMonad
  , maxOpenValueHandles
  ) where

import Cardano.Slotting.Slot
import Control.Concurrent.Class.MonadMVar.Strict
import Control.Monad
import Control.Monad.Class.MonadThrow
import Control.Monad.Reader
import Data.Bifunctor
import Data.Constraint
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Typeable
import Ouroboros.Consensus.Ledger.Tables
import qualified Ouroboros.Consensus.Storage.LedgerDB.V1.BackingStore as BS
import qualified Ouroboros.Consensus.Storage.LedgerDB.V1.BackingStore.Impl.InMemory as BS
import Ouroboros.Consensus.Storage.LedgerDB.V1.BackingStore.Impl.LMDB as LMDB
  ( LMDBErr (..)
  )
import Ouroboros.Consensus.Util.IOLike hiding
  ( MonadMask (..)
  , StrictMVar
  , handle
  , readMVar
  , swapMVar
  )
import System.FS.API hiding (Handle)
import qualified System.FS.API.Types as FS
import Test.Cardano.Ledger.Binary.Arbitrary ()
import Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Mock
  ( Err (..)
  , Mock (..)
  , ValueHandle (..)
  , runMockMonad
  )
import qualified Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Mock as Mock
import Test.QuickCheck (Gen)
import qualified Test.QuickCheck as QC
import Test.QuickCheck.StateModel
import Test.QuickCheck.StateModel.Lockstep as Lockstep
import Test.QuickCheck.StateModel.Lockstep.Defaults as Lockstep
import Test.QuickCheck.StateModel.Lockstep.Op.SumProd as Lockstep
import Test.Util.Orphans.Arbitrary ()
import Test.Util.Orphans.ToExpr ()

{-------------------------------------------------------------------------------
  @'Values'@ wrapper
-------------------------------------------------------------------------------}

-- | Wrapper to prevent ambiguity in pattern matches.
newtype Values vs = Values {forall vs. Values vs -> vs
unValues :: vs}
  deriving stock (Int -> Values vs -> ShowS
[Values vs] -> ShowS
Values vs -> String
(Int -> Values vs -> ShowS)
-> (Values vs -> String)
-> ([Values vs] -> ShowS)
-> Show (Values vs)
forall vs. Show vs => Int -> Values vs -> ShowS
forall vs. Show vs => [Values vs] -> ShowS
forall vs. Show vs => Values vs -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall vs. Show vs => Int -> Values vs -> ShowS
showsPrec :: Int -> Values vs -> ShowS
$cshow :: forall vs. Show vs => Values vs -> String
show :: Values vs -> String
$cshowList :: forall vs. Show vs => [Values vs] -> ShowS
showList :: [Values vs] -> ShowS
Show, Values vs -> Values vs -> Bool
(Values vs -> Values vs -> Bool)
-> (Values vs -> Values vs -> Bool) -> Eq (Values vs)
forall vs. Eq vs => Values vs -> Values vs -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall vs. Eq vs => Values vs -> Values vs -> Bool
== :: Values vs -> Values vs -> Bool
$c/= :: forall vs. Eq vs => Values vs -> Values vs -> Bool
/= :: Values vs -> Values vs -> Bool
Eq, Eq (Values vs)
Eq (Values vs) =>
(Values vs -> Values vs -> Ordering)
-> (Values vs -> Values vs -> Bool)
-> (Values vs -> Values vs -> Bool)
-> (Values vs -> Values vs -> Bool)
-> (Values vs -> Values vs -> Bool)
-> (Values vs -> Values vs -> Values vs)
-> (Values vs -> Values vs -> Values vs)
-> Ord (Values vs)
Values vs -> Values vs -> Bool
Values vs -> Values vs -> Ordering
Values vs -> Values vs -> Values vs
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall vs. Ord vs => Eq (Values vs)
forall vs. Ord vs => Values vs -> Values vs -> Bool
forall vs. Ord vs => Values vs -> Values vs -> Ordering
forall vs. Ord vs => Values vs -> Values vs -> Values vs
$ccompare :: forall vs. Ord vs => Values vs -> Values vs -> Ordering
compare :: Values vs -> Values vs -> Ordering
$c< :: forall vs. Ord vs => Values vs -> Values vs -> Bool
< :: Values vs -> Values vs -> Bool
$c<= :: forall vs. Ord vs => Values vs -> Values vs -> Bool
<= :: Values vs -> Values vs -> Bool
$c> :: forall vs. Ord vs => Values vs -> Values vs -> Bool
> :: Values vs -> Values vs -> Bool
$c>= :: forall vs. Ord vs => Values vs -> Values vs -> Bool
>= :: Values vs -> Values vs -> Bool
$cmax :: forall vs. Ord vs => Values vs -> Values vs -> Values vs
max :: Values vs -> Values vs -> Values vs
$cmin :: forall vs. Ord vs => Values vs -> Values vs -> Values vs
min :: Values vs -> Values vs -> Values vs
Ord)
  deriving newtype Gen (Values vs)
Gen (Values vs)
-> (Values vs -> [Values vs]) -> Arbitrary (Values vs)
Values vs -> [Values vs]
forall a. Gen a -> (a -> [a]) -> Arbitrary a
forall vs. Arbitrary vs => Gen (Values vs)
forall vs. Arbitrary vs => Values vs -> [Values vs]
$carbitrary :: forall vs. Arbitrary vs => Gen (Values vs)
arbitrary :: Gen (Values vs)
$cshrink :: forall vs. Arbitrary vs => Values vs -> [Values vs]
shrink :: Values vs -> [Values vs]
QC.Arbitrary

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

data BackingStoreState ks k vs d = BackingStoreState
  { forall ks k vs d. BackingStoreState ks k vs d -> Mock vs
bssMock :: Mock vs
  , forall ks k vs d. BackingStoreState ks k vs d -> Stats ks k vs d
bssStats :: Stats ks k vs d
  }
  deriving (Int -> BackingStoreState ks k vs d -> ShowS
[BackingStoreState ks k vs d] -> ShowS
BackingStoreState ks k vs d -> String
(Int -> BackingStoreState ks k vs d -> ShowS)
-> (BackingStoreState ks k vs d -> String)
-> ([BackingStoreState ks k vs d] -> ShowS)
-> Show (BackingStoreState ks k vs d)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall ks k vs d.
Show vs =>
Int -> BackingStoreState ks k vs d -> ShowS
forall ks k vs d. Show vs => [BackingStoreState ks k vs d] -> ShowS
forall ks k vs d. Show vs => BackingStoreState ks k vs d -> String
$cshowsPrec :: forall ks k vs d.
Show vs =>
Int -> BackingStoreState ks k vs d -> ShowS
showsPrec :: Int -> BackingStoreState ks k vs d -> ShowS
$cshow :: forall ks k vs d. Show vs => BackingStoreState ks k vs d -> String
show :: BackingStoreState ks k vs d -> String
$cshowList :: forall ks k vs d. Show vs => [BackingStoreState ks k vs d] -> ShowS
showList :: [BackingStoreState ks k vs d] -> ShowS
Show, BackingStoreState ks k vs d -> BackingStoreState ks k vs d -> Bool
(BackingStoreState ks k vs d
 -> BackingStoreState ks k vs d -> Bool)
-> (BackingStoreState ks k vs d
    -> BackingStoreState ks k vs d -> Bool)
-> Eq (BackingStoreState ks k vs d)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall ks k vs d.
Eq vs =>
BackingStoreState ks k vs d -> BackingStoreState ks k vs d -> Bool
$c== :: forall ks k vs d.
Eq vs =>
BackingStoreState ks k vs d -> BackingStoreState ks k vs d -> Bool
== :: BackingStoreState ks k vs d -> BackingStoreState ks k vs d -> Bool
$c/= :: forall ks k vs d.
Eq vs =>
BackingStoreState ks k vs d -> BackingStoreState ks k vs d -> Bool
/= :: BackingStoreState ks k vs d -> BackingStoreState ks k vs d -> Bool
Eq)

initState :: Mock.EmptyValues vs => BackingStoreState ks k vs d
initState :: forall vs ks k d. EmptyValues vs => BackingStoreState ks k vs d
initState =
  BackingStoreState
    { bssMock :: Mock vs
bssMock = Mock vs
forall vs. EmptyValues vs => Mock vs
Mock.emptyMock
    , bssStats :: Stats ks k vs d
bssStats = Stats ks k vs d
forall ks k vs d. Stats ks k vs d
initStats
    }

-- | Maximum number of LMDB readers that can be active at a time.
--
-- 32 is an arbitrary number of readers. We can increase or decrease this at
-- will.
maxOpenValueHandles :: Int
maxOpenValueHandles :: Int
maxOpenValueHandles = Int
32

{-------------------------------------------------------------------------------
  @'StateModel'@ and @'RunModel'@ instances
-------------------------------------------------------------------------------}

type BackingStoreInitializer m ks k vs d =
  BS.InitFrom vs ->
  m (BS.BackingStore m ks k vs d)

data RealEnv m ks k vs d = RealEnv
  { forall (m :: * -> *) ks k vs d.
RealEnv m ks k vs d -> BackingStoreInitializer m ks k vs d
reBackingStoreInit :: BackingStoreInitializer m ks k vs d
  , forall (m :: * -> *) ks k vs d.
RealEnv m ks k vs d -> StrictMVar m (BackingStore m ks k vs d)
reBackingStore :: StrictMVar m (BS.BackingStore m ks k vs d)
  }

type RealMonad m ks k vs d = ReaderT (RealEnv m ks k vs d) m

type BSAct ks k vs d a =
  Action
    (Lockstep (BackingStoreState ks k vs d))
    (Either Err a)
type BSVar ks k vs d a =
  ModelVar (BackingStoreState ks k vs d) a

instance
  ( Show ks
  , Show vs
  , Show k
  , Show d
  , Show (BS.InitHint vs)
  , Show (BS.WriteHint d)
  , Show (BS.ReadHint vs)
  , Eq ks
  , Eq k
  , Eq vs
  , Eq d
  , Eq (BS.InitHint vs)
  , Eq (BS.WriteHint d)
  , Eq (BS.ReadHint vs)
  , Typeable ks
  , Typeable k
  , Typeable vs
  , Typeable d
  , Typeable (BS.WriteHint d)
  , QC.Arbitrary ks
  , QC.Arbitrary k
  , QC.Arbitrary vs
  , QC.Arbitrary d
  , QC.Arbitrary (BS.RangeQuery ks)
  , Mock.HasOps ks k vs d
  ) =>
  StateModel (Lockstep (BackingStoreState ks k vs d))
  where
  data Action (Lockstep (BackingStoreState ks k vs d)) a where
    -- Reopen a backing store by intialising from values.
    BSInitFromValues ::
      WithOrigin SlotNo ->
      BS.InitHint vs ->
      Values vs ->
      BSAct ks k vs d ()
    -- Reopen a backing store by initialising from a copy.
    BSInitFromCopy ::
      BS.InitHint vs ->
      FS.FsPath ->
      BSAct ks k vs d ()
    BSClose :: BSAct ks k vs d ()
    BSCopy ::
      SerializeTablesHint vs ->
      FS.FsPath ->
      BSAct ks k vs d ()
    BSValueHandle :: BSAct ks k vs d (BS.BackingStoreValueHandle IO ks k vs)
    BSWrite ::
      SlotNo ->
      BS.WriteHint d ->
      d ->
      BSAct ks k vs d ()
    BSVHClose ::
      BSVar ks k vs d (BS.BackingStoreValueHandle IO ks k vs) ->
      BSAct ks k vs d ()
    BSVHRangeRead ::
      BSVar ks k vs d (BS.BackingStoreValueHandle IO ks k vs) ->
      BS.ReadHint vs ->
      BS.RangeQuery ks ->
      BSAct ks k vs d (Values vs, Maybe k)
    BSVHRead ::
      BSVar ks k vs d (BS.BackingStoreValueHandle IO ks k vs) ->
      BS.ReadHint vs ->
      ks ->
      BSAct ks k vs d (Values vs)
    BSVHAtSlot ::
      BSVar ks k vs d (BS.BackingStoreValueHandle IO ks k vs) ->
      BSAct ks k vs d (WithOrigin SlotNo)
    -- \| Corresponds to 'bsvhStat'
    BSVHStat ::
      BSVar ks k vs d (BS.BackingStoreValueHandle IO ks k vs) ->
      BSAct ks k vs d BS.Statistics

  initialState :: Lockstep (BackingStoreState ks k vs d)
initialState = BackingStoreState ks k vs d
-> Lockstep (BackingStoreState ks k vs d)
forall state. state -> Lockstep state
Lockstep.initialState BackingStoreState ks k vs d
forall vs ks k d. EmptyValues vs => BackingStoreState ks k vs d
initState
  nextState :: forall a.
Typeable a =>
Lockstep (BackingStoreState ks k vs d)
-> Action (Lockstep (BackingStoreState ks k vs d)) a
-> Var a
-> Lockstep (BackingStoreState ks k vs d)
nextState = Lockstep (BackingStoreState ks k vs d)
-> LockstepAction (BackingStoreState ks k vs d) a
-> Var a
-> Lockstep (BackingStoreState ks k vs d)
forall state a.
(InLockstep state, Typeable a) =>
Lockstep state -> LockstepAction state a -> Var a -> Lockstep state
Lockstep.nextState
  precondition :: forall a.
Lockstep (BackingStoreState ks k vs d)
-> Action (Lockstep (BackingStoreState ks k vs d)) a -> Bool
precondition Lockstep (BackingStoreState ks k vs d)
st Action (Lockstep (BackingStoreState ks k vs d)) a
act =
    Lockstep (BackingStoreState ks k vs d)
-> Action (Lockstep (BackingStoreState ks k vs d)) a -> Bool
forall state a.
InLockstep state =>
Lockstep state -> LockstepAction state a -> Bool
Lockstep.precondition Lockstep (BackingStoreState ks k vs d)
st Action (Lockstep (BackingStoreState ks k vs d)) a
act
      Bool -> Bool -> Bool
&& BackingStoreState ks k vs d
-> Action (Lockstep (BackingStoreState ks k vs d)) a -> Bool
forall ks k vs d a.
BackingStoreState ks k vs d
-> LockstepAction (BackingStoreState ks k vs d) a -> Bool
modelPrecondition (Lockstep (BackingStoreState ks k vs d)
-> BackingStoreState ks k vs d
forall state. Lockstep state -> state
getModel Lockstep (BackingStoreState ks k vs d)
st) Action (Lockstep (BackingStoreState ks k vs d)) a
act
  arbitraryAction :: VarContext
-> Lockstep (BackingStoreState ks k vs d)
-> Gen (Any (Action (Lockstep (BackingStoreState ks k vs d))))
arbitraryAction = VarContext
-> Lockstep (BackingStoreState ks k vs d)
-> Gen (Any (Action (Lockstep (BackingStoreState ks k vs d))))
forall state.
InLockstep state =>
VarContext -> Lockstep state -> Gen (Any (LockstepAction state))
Lockstep.arbitraryAction
  shrinkAction :: forall a.
Typeable a =>
VarContext
-> Lockstep (BackingStoreState ks k vs d)
-> Action (Lockstep (BackingStoreState ks k vs d)) a
-> [Any (Action (Lockstep (BackingStoreState ks k vs d)))]
shrinkAction = VarContext
-> Lockstep (BackingStoreState ks k vs d)
-> LockstepAction (BackingStoreState ks k vs d) a
-> [Any (Action (Lockstep (BackingStoreState ks k vs d)))]
forall state a.
InLockstep state =>
VarContext
-> Lockstep state
-> LockstepAction state a
-> [Any (LockstepAction state)]
Lockstep.shrinkAction

deriving stock instance
  ( Show ks
  , Show vs
  , Show d
  , Show (BS.InitHint vs)
  , Show (BS.WriteHint d)
  , Show (BS.ReadHint vs)
  , Show (SerializeTablesHint vs)
  ) =>
  Show (LockstepAction (BackingStoreState ks k vs d) a)
deriving stock instance
  ( Eq ks
  , Eq vs
  , Eq d
  , Eq (BS.InitHint vs)
  , Eq (BS.WriteHint d)
  , Eq (BS.ReadHint vs)
  , Eq (SerializeTablesHint vs)
  ) =>
  Eq (LockstepAction (BackingStoreState ks k vs d) a)

instance
  ( Show ks
  , Show vs
  , Show k
  , Show d
  , Show (BS.InitHint vs)
  , Show (BS.WriteHint d)
  , Show (BS.ReadHint vs)
  , Eq ks
  , Eq vs
  , Eq k
  , Eq d
  , Eq (BS.InitHint vs)
  , Eq (BS.WriteHint d)
  , Eq (BS.ReadHint vs)
  , Typeable ks
  , Typeable k
  , Typeable vs
  , Typeable d
  , Typeable (BS.WriteHint d)
  , QC.Arbitrary ks
  , QC.Arbitrary k
  , QC.Arbitrary vs
  , QC.Arbitrary d
  , QC.Arbitrary (BS.RangeQuery ks)
  , Mock.HasOps ks k vs d
  ) =>
  RunModel
    (Lockstep (BackingStoreState ks k vs d))
    (RealMonad IO ks k vs d)
  where
  perform :: forall a.
Typeable a =>
Lockstep (BackingStoreState ks k vs d)
-> Action (Lockstep (BackingStoreState ks k vs d)) a
-> LookUp
-> RealMonad
     IO
     ks
     k
     vs
     d
     (PerformResult
        (Lockstep (BackingStoreState ks k vs d))
        (RealMonad IO ks k vs d)
        a)
perform = \Lockstep (BackingStoreState ks k vs d)
_st -> Action (Lockstep (BackingStoreState ks k vs d)) a
-> LookUp -> RealMonad IO ks k vs d a
Action (Lockstep (BackingStoreState ks k vs d)) a
-> LookUp
-> RealMonad
     IO
     ks
     k
     vs
     d
     (PerformResult
        (Lockstep (BackingStoreState ks k vs d))
        (RealMonad IO ks k vs d)
        a)
forall ks k vs d a.
LockstepAction (BackingStoreState ks k vs d) a
-> LookUp -> RealMonad IO ks k vs d a
runIO
  postcondition :: forall a.
(Lockstep (BackingStoreState ks k vs d),
 Lockstep (BackingStoreState ks k vs d))
-> Action (Lockstep (BackingStoreState ks k vs d)) a
-> LookUp
-> a
-> PostconditionM (RealMonad IO ks k vs d) Bool
postcondition = (Lockstep (BackingStoreState ks k vs d),
 Lockstep (BackingStoreState ks k vs d))
-> LockstepAction (BackingStoreState ks k vs d) a
-> LookUp
-> a
-> PostconditionM (RealMonad IO ks k vs d) Bool
forall (m :: * -> *) state a.
RunLockstep state m =>
(Lockstep state, Lockstep state)
-> LockstepAction state a -> LookUp -> a -> PostconditionM m Bool
Lockstep.postcondition
  monitoring :: forall a.
(Lockstep (BackingStoreState ks k vs d),
 Lockstep (BackingStoreState ks k vs d))
-> Action (Lockstep (BackingStoreState ks k vs d)) a
-> LookUp
-> Either
     (Error
        (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d))
     a
-> Property
-> Property
monitoring = Proxy (RealMonad IO ks k vs d)
-> (Lockstep (BackingStoreState ks k vs d),
    Lockstep (BackingStoreState ks k vs d))
-> Action (Lockstep (BackingStoreState ks k vs d)) a
-> LookUp
-> Either
     (Error
        (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d))
     a
-> Property
-> Property
forall (m :: * -> *) state a.
RunLockstep state m =>
Proxy m
-> (Lockstep state, Lockstep state)
-> LockstepAction state a
-> LookUp
-> Either (Error (Lockstep state) m) a
-> Property
-> Property
Lockstep.monitoring (forall {k} (t :: k). Proxy t
forall (t :: * -> *). Proxy t
Proxy @(RealMonad IO ks k vs d))

-- | Custom precondition that prevents errors in the @'LMDB'@ backing store due
-- to exceeding the maximum number of LMDB readers.
--
-- See @'maxOpenValueHandles'@.
modelPrecondition ::
  BackingStoreState ks k vs d ->
  LockstepAction (BackingStoreState ks k vs d) a ->
  Bool
modelPrecondition :: forall ks k vs d a.
BackingStoreState ks k vs d
-> LockstepAction (BackingStoreState ks k vs d) a -> Bool
modelPrecondition (BackingStoreState Mock vs
mock Stats ks k vs d
_stats) LockstepAction (BackingStoreState ks k vs d) a
action = case LockstepAction (BackingStoreState ks k vs d) a
action of
  BSInitFromValues WithOrigin SlotNo
_ InitHint vs
_ Values vs
_ -> Mock vs -> Bool
forall vs. Mock vs -> Bool
isClosed Mock vs
mock
  BSInitFromCopy InitHint vs
_ FsPath
_ -> Mock vs -> Bool
forall vs. Mock vs -> Bool
isClosed Mock vs
mock
  BSCopy SerializeTablesHint vs
_ FsPath
_ -> Bool
canOpenReader
  LockstepAction (BackingStoreState ks k vs d) a
R:ActionLockstepa ks k vs d a
BSValueHandle -> Bool
canOpenReader
  LockstepAction (BackingStoreState ks k vs d) a
_ -> Bool
True
 where
  canOpenReader :: Bool
canOpenReader = Map ID ValueHandleStatus -> Int
forall k a. Map k a -> Int
Map.size Map ID ValueHandleStatus
openValueHandles Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
maxOpenValueHandles
  openValueHandles :: Map ID ValueHandleStatus
openValueHandles = (ValueHandleStatus -> Bool)
-> Map ID ValueHandleStatus -> Map ID ValueHandleStatus
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (ValueHandleStatus -> ValueHandleStatus -> Bool
forall a. Eq a => a -> a -> Bool
== ValueHandleStatus
Mock.Open) (Mock vs -> Map ID ValueHandleStatus
forall vs. Mock vs -> Map ID ValueHandleStatus
valueHandles Mock vs
mock)

{-------------------------------------------------------------------------------
  @'InLockstep'@ instance
-------------------------------------------------------------------------------}

type BSVal ks k vs d a = ModelValue (BackingStoreState ks k vs d) a
type BSObs ks k vs d a = Observable (BackingStoreState ks k vs d) a

instance
  ( Show ks
  , Show vs
  , Show d
  , Show k
  , Show (BS.InitHint vs)
  , Show (BS.WriteHint d)
  , Show (BS.ReadHint vs)
  , Eq ks
  , Eq vs
  , Eq k
  , Eq d
  , Eq (BS.InitHint vs)
  , Eq (BS.WriteHint d)
  , Eq (BS.ReadHint vs)
  , Typeable ks
  , Typeable k
  , Typeable vs
  , Typeable d
  , Typeable (BS.WriteHint d)
  , QC.Arbitrary ks
  , QC.Arbitrary k
  , QC.Arbitrary vs
  , QC.Arbitrary d
  , QC.Arbitrary (BS.RangeQuery ks)
  , Mock.HasOps ks k vs d
  ) =>
  InLockstep (BackingStoreState ks k vs d)
  where
  data ModelValue (BackingStoreState ks k vs d) a where
    MValueHandle :: ValueHandle vs -> BSVal ks k vs d (BS.BackingStoreValueHandle IO ks k vs)
    MErr ::
      Err ->
      BSVal ks k vs d Err
    MSlotNo ::
      WithOrigin SlotNo ->
      BSVal ks k vs d (WithOrigin SlotNo)
    MValues ::
      vs ->
      BSVal ks k vs d (Values vs)
    MValuesAndLast ::
      (vs, Maybe k) ->
      BSVal ks k vs d (Values vs, Maybe k)
    MUnit ::
      () ->
      BSVal ks k vs d ()
    MStatistics ::
      BS.Statistics ->
      BSVal ks k vs d BS.Statistics
    MEither ::
      Either (BSVal ks k vs d a) (BSVal ks k vs d b) ->
      BSVal ks k vs d (Either a b)
    MPair ::
      (BSVal ks k vs d a, BSVal ks k vs d b) ->
      BSVal ks k vs d (a, b)

  data Observable (BackingStoreState ks k vs d) a where
    OValueHandle :: BSObs ks k vs d (BS.BackingStoreValueHandle IO ks k vs)
    OValues :: (Show a, Eq a, Typeable a) => a -> BSObs ks k vs d (Values a)
    OValuesAndLast :: (Show a, Eq a, Typeable a) => (a, Maybe k) -> BSObs ks k vs d (Values a, Maybe k)
    OId :: (Show a, Eq a, Typeable a) => a -> BSObs ks k vs d a
    OEither ::
      Either (BSObs ks k vs d a) (BSObs ks k vs d b) ->
      BSObs ks k vs d (Either a b)
    OPair :: (BSObs ks k vs d a, BSObs ks k vs d b) -> BSObs ks k vs d (a, b)

  observeModel :: BSVal ks k vs d a -> BSObs ks k vs d a
  observeModel :: forall a.
ModelValue (BackingStoreState ks k vs d) a
-> Observable (BackingStoreState ks k vs d) a
observeModel = \case
    MValueHandle ValueHandle vs
_ -> BSObs ks k vs d a
BSObs ks k vs d (BackingStoreValueHandle IO ks k vs)
forall ks k vs d.
BSObs ks k vs d (BackingStoreValueHandle IO ks k vs)
OValueHandle
    MErr Err
x -> a -> BSObs ks k vs d a
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId a
Err
x
    MSlotNo WithOrigin SlotNo
x -> a -> BSObs ks k vs d a
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId a
WithOrigin SlotNo
x
    MValues vs
x -> vs -> BSObs ks k vs d (Values vs)
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d (Values a)
OValues vs
x
    MValuesAndLast (vs, Maybe k)
x -> (vs, Maybe k) -> BSObs ks k vs d (Values vs, Maybe k)
forall a k ks vs d.
(Show a, Eq a, Typeable a) =>
(a, Maybe k) -> BSObs ks k vs d (Values a, Maybe k)
OValuesAndLast (vs, Maybe k)
x
    MUnit ()
x -> a -> BSObs ks k vs d a
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId a
()
x
    MStatistics Statistics
x -> a -> BSObs ks k vs d a
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId a
Statistics
x
    MEither Either (BSVal ks k vs d a) (BSVal ks k vs d b)
x -> Either (BSObs ks k vs d a) (BSObs ks k vs d b)
-> BSObs ks k vs d (Either a b)
forall ks k vs d a b.
Either (BSObs ks k vs d a) (BSObs ks k vs d b)
-> BSObs ks k vs d (Either a b)
OEither (Either (BSObs ks k vs d a) (BSObs ks k vs d b)
 -> BSObs ks k vs d (Either a b))
-> Either (BSObs ks k vs d a) (BSObs ks k vs d b)
-> BSObs ks k vs d (Either a b)
forall a b. (a -> b) -> a -> b
$ (BSVal ks k vs d a -> BSObs ks k vs d a)
-> (BSVal ks k vs d b -> BSObs ks k vs d b)
-> Either (BSVal ks k vs d a) (BSVal ks k vs d b)
-> Either (BSObs ks k vs d a) (BSObs ks k vs d b)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap BSVal ks k vs d a -> BSObs ks k vs d a
forall state a.
InLockstep state =>
ModelValue state a -> Observable state a
forall a.
ModelValue (BackingStoreState ks k vs d) a
-> Observable (BackingStoreState ks k vs d) a
observeModel BSVal ks k vs d b -> BSObs ks k vs d b
forall state a.
InLockstep state =>
ModelValue state a -> Observable state a
forall a.
ModelValue (BackingStoreState ks k vs d) a
-> Observable (BackingStoreState ks k vs d) a
observeModel Either (BSVal ks k vs d a) (BSVal ks k vs d b)
x
    MPair (BSVal ks k vs d a, BSVal ks k vs d b)
x -> (BSObs ks k vs d a, BSObs ks k vs d b) -> BSObs ks k vs d (a, b)
forall ks k vs d a b.
(BSObs ks k vs d a, BSObs ks k vs d b) -> BSObs ks k vs d (a, b)
OPair ((BSObs ks k vs d a, BSObs ks k vs d b) -> BSObs ks k vs d (a, b))
-> (BSObs ks k vs d a, BSObs ks k vs d b) -> BSObs ks k vs d (a, b)
forall a b. (a -> b) -> a -> b
$ (BSVal ks k vs d a -> BSObs ks k vs d a)
-> (BSVal ks k vs d b -> BSObs ks k vs d b)
-> (BSVal ks k vs d a, BSVal ks k vs d b)
-> (BSObs ks k vs d a, BSObs ks k vs d b)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap BSVal ks k vs d a -> BSObs ks k vs d a
forall state a.
InLockstep state =>
ModelValue state a -> Observable state a
forall a.
ModelValue (BackingStoreState ks k vs d) a
-> Observable (BackingStoreState ks k vs d) a
observeModel BSVal ks k vs d b -> BSObs ks k vs d b
forall state a.
InLockstep state =>
ModelValue state a -> Observable state a
forall a.
ModelValue (BackingStoreState ks k vs d) a
-> Observable (BackingStoreState ks k vs d) a
observeModel (BSVal ks k vs d a, BSVal ks k vs d b)
x

  modelNextState ::
    forall a.
    LockstepAction (BackingStoreState ks k vs d) a ->
    ModelVarContext (BackingStoreState ks k vs d) ->
    BackingStoreState ks k vs d ->
    (BSVal ks k vs d a, BackingStoreState ks k vs d)
  modelNextState :: forall a.
LockstepAction (BackingStoreState ks k vs d) a
-> ModelVarContext (BackingStoreState ks k vs d)
-> BackingStoreState ks k vs d
-> (ModelValue (BackingStoreState ks k vs d) a,
    BackingStoreState ks k vs d)
modelNextState LockstepAction (BackingStoreState ks k vs d) a
action ModelVarContext (BackingStoreState ks k vs d)
lookUp (BackingStoreState Mock vs
mock Stats ks k vs d
stats) =
    (BSVal ks k vs d a, Mock vs)
-> (BSVal ks k vs d a, BackingStoreState ks k vs d)
auxStats ((BSVal ks k vs d a, Mock vs)
 -> (BSVal ks k vs d a, BackingStoreState ks k vs d))
-> (BSVal ks k vs d a, Mock vs)
-> (BSVal ks k vs d a, BackingStoreState ks k vs d)
forall a b. (a -> b) -> a -> b
$ ModelVarContext (BackingStoreState ks k vs d)
-> LockstepAction (BackingStoreState ks k vs d) a
-> Mock vs
-> (BSVal ks k vs d a, Mock vs)
forall ks k vs d a.
(HasOps ks k vs d, Arbitrary ks, Arbitrary vs, Arbitrary k,
 Arbitrary d, Arbitrary (RangeQuery ks)) =>
ModelVarContext (BackingStoreState ks k vs d)
-> Action (Lockstep (BackingStoreState ks k vs d)) a
-> Mock vs
-> (BSVal ks k vs d a, Mock vs)
runMock ModelVarContext (BackingStoreState ks k vs d)
lookUp LockstepAction (BackingStoreState ks k vs d) a
action Mock vs
mock
   where
    auxStats ::
      (BSVal ks k vs d a, Mock vs) ->
      (BSVal ks k vs d a, BackingStoreState ks k vs d)
    auxStats :: (BSVal ks k vs d a, Mock vs)
-> (BSVal ks k vs d a, BackingStoreState ks k vs d)
auxStats (BSVal ks k vs d a
result, Mock vs
state') =
      ( BSVal ks k vs d a
result
      , Mock vs -> Stats ks k vs d -> BackingStoreState ks k vs d
forall ks k vs d.
Mock vs -> Stats ks k vs d -> BackingStoreState ks k vs d
BackingStoreState Mock vs
state' (Stats ks k vs d -> BackingStoreState ks k vs d)
-> Stats ks k vs d -> BackingStoreState ks k vs d
forall a b. (a -> b) -> a -> b
$ LockstepAction (BackingStoreState ks k vs d) a
-> ModelVarContext (BackingStoreState ks k vs d)
-> BSVal ks k vs d a
-> Stats ks k vs d
-> Stats ks k vs d
forall ks k vs d a.
(HasOps ks k vs d, Arbitrary ks, Arbitrary vs, Arbitrary k,
 Arbitrary d, Arbitrary (RangeQuery ks)) =>
LockstepAction (BackingStoreState ks k vs d) a
-> ModelVarContext (BackingStoreState ks k vs d)
-> BSVal ks k vs d a
-> Stats ks k vs d
-> Stats ks k vs d
updateStats LockstepAction (BackingStoreState ks k vs d) a
action ModelVarContext (BackingStoreState ks k vs d)
lookUp BSVal ks k vs d a
result Stats ks k vs d
stats
      )

  type ModelOp (BackingStoreState ks k vs d) = Op

  usedVars ::
    LockstepAction (BackingStoreState ks k vs d) a ->
    [AnyGVar (ModelOp (BackingStoreState ks k vs d))]
  usedVars :: forall a.
LockstepAction (BackingStoreState ks k vs d) a
-> [AnyGVar (ModelOp (BackingStoreState ks k vs d))]
usedVars = \case
    BSInitFromValues WithOrigin SlotNo
_ InitHint vs
_ Values vs
_ -> []
    BSInitFromCopy InitHint vs
_ FsPath
_ -> []
    LockstepAction (BackingStoreState ks k vs d) a
R:ActionLockstepa ks k vs d a
BSClose -> []
    BSCopy SerializeTablesHint vs
_ FsPath
_ -> []
    LockstepAction (BackingStoreState ks k vs d) a
R:ActionLockstepa ks k vs d a
BSValueHandle -> []
    BSWrite SlotNo
_ WriteHint d
_ d
_ -> []
    BSVHClose BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h -> [GVar Op (BackingStoreValueHandle IO ks k vs) -> AnyGVar Op
forall {k} (op :: * -> k -> *) (y :: k). GVar op y -> AnyGVar op
SomeGVar BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
GVar Op (BackingStoreValueHandle IO ks k vs)
h]
    BSVHRangeRead BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h ReadHint vs
_ RangeQuery ks
_ -> [GVar Op (BackingStoreValueHandle IO ks k vs) -> AnyGVar Op
forall {k} (op :: * -> k -> *) (y :: k). GVar op y -> AnyGVar op
SomeGVar BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
GVar Op (BackingStoreValueHandle IO ks k vs)
h]
    BSVHRead BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h ReadHint vs
_ ks
_ -> [GVar Op (BackingStoreValueHandle IO ks k vs) -> AnyGVar Op
forall {k} (op :: * -> k -> *) (y :: k). GVar op y -> AnyGVar op
SomeGVar BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
GVar Op (BackingStoreValueHandle IO ks k vs)
h]
    BSVHAtSlot BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h -> [GVar Op (BackingStoreValueHandle IO ks k vs) -> AnyGVar Op
forall {k} (op :: * -> k -> *) (y :: k). GVar op y -> AnyGVar op
SomeGVar BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
GVar Op (BackingStoreValueHandle IO ks k vs)
h]
    BSVHStat BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h -> [GVar Op (BackingStoreValueHandle IO ks k vs) -> AnyGVar Op
forall {k} (op :: * -> k -> *) (y :: k). GVar op y -> AnyGVar op
SomeGVar BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
GVar Op (BackingStoreValueHandle IO ks k vs)
h]

  arbitraryWithVars ::
    ModelVarContext (BackingStoreState ks k vs d) ->
    BackingStoreState ks k vs d ->
    Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
  arbitraryWithVars :: ModelVarContext (BackingStoreState ks k vs d)
-> BackingStoreState ks k vs d
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
arbitraryWithVars = ModelVarContext (BackingStoreState ks k vs d)
-> BackingStoreState ks k vs d
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall ks k vs d.
(HasOps ks k vs d, Arbitrary ks, Arbitrary vs, Arbitrary k,
 Arbitrary d, Arbitrary (RangeQuery ks)) =>
ModelVarContext (BackingStoreState ks k vs d)
-> BackingStoreState ks k vs d
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
arbitraryBackingStoreAction

  shrinkWithVars ::
    ModelVarContext (BackingStoreState ks k vs d) ->
    BackingStoreState ks k vs d ->
    LockstepAction (BackingStoreState ks k vs d) a ->
    [Any (LockstepAction (BackingStoreState ks k vs d))]
  shrinkWithVars :: forall a.
ModelVarContext (BackingStoreState ks k vs d)
-> BackingStoreState ks k vs d
-> LockstepAction (BackingStoreState ks k vs d) a
-> [Any (LockstepAction (BackingStoreState ks k vs d))]
shrinkWithVars = ModelVarContext (BackingStoreState ks k vs d)
-> BackingStoreState ks k vs d
-> LockstepAction (BackingStoreState ks k vs d) a
-> [Any (LockstepAction (BackingStoreState ks k vs d))]
forall ks k vs d a.
(Typeable vs, Typeable k, Eq ks, Eq vs, Eq d, Eq (InitHint vs),
 Eq (WriteHint d), Eq (ReadHint vs), Eq (SerializeTablesHint vs),
 Arbitrary d, Arbitrary (RangeQuery ks), Arbitrary ks) =>
ModelVarContext (BackingStoreState ks k vs d)
-> BackingStoreState ks k vs d
-> LockstepAction (BackingStoreState ks k vs d) a
-> [Any (LockstepAction (BackingStoreState ks k vs d))]
shrinkBackingStoreAction

  tagStep ::
    (BackingStoreState ks k vs d, BackingStoreState ks k vs d) ->
    LockstepAction (BackingStoreState ks k vs d) a ->
    BSVal ks k vs d a ->
    [String]
  tagStep :: forall a.
(BackingStoreState ks k vs d, BackingStoreState ks k vs d)
-> LockstepAction (BackingStoreState ks k vs d) a
-> ModelValue (BackingStoreState ks k vs d) a
-> [String]
tagStep (BackingStoreState Mock vs
_ Stats ks k vs d
before, BackingStoreState Mock vs
_ Stats ks k vs d
after) LockstepAction (BackingStoreState ks k vs d) a
action BSVal ks k vs d a
val =
    (Tag -> String) -> [Tag] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Tag -> String
forall a. Show a => a -> String
show ([Tag] -> [String]) -> [Tag] -> [String]
forall a b. (a -> b) -> a -> b
$ Stats ks k vs d
-> Stats ks k vs d
-> LockstepAction (BackingStoreState ks k vs d) a
-> BSVal ks k vs d a
-> [Tag]
forall ks k vs d a.
Stats ks k vs d
-> Stats ks k vs d
-> LockstepAction (BackingStoreState ks k vs d) a
-> BSVal ks k vs d a
-> [Tag]
tagBSAction Stats ks k vs d
before Stats ks k vs d
after LockstepAction (BackingStoreState ks k vs d) a
action BSVal ks k vs d a
val

deriving stock instance
  ( Show ks
  , Show vs
  , Show k
  , Show d
  , Show (BS.WriteHint d)
  , Show (BS.ReadHint vs)
  ) =>
  Show (BSVal ks k vs d a)

deriving stock instance
  ( Show ks
  , Show vs
  , Show k
  , Show d
  , Show (BS.WriteHint d)
  , Show (BS.ReadHint vs)
  ) =>
  Show (BSObs ks k vs d a)

deriving stock instance
  ( Eq ks
  , Eq vs
  , Eq k
  , Eq d
  , Eq (BS.WriteHint d)
  , Eq (BS.ReadHint vs)
  ) =>
  Eq (BSObs ks k vs d a)

{-------------------------------------------------------------------------------
  @'RunLockstep'@ instance
-------------------------------------------------------------------------------}

instance
  ( Show ks
  , Show vs
  , Show k
  , Show d
  , Show (BS.InitHint vs)
  , Show (BS.WriteHint d)
  , Show (BS.ReadHint vs)
  , Eq ks
  , Eq vs
  , Eq k
  , Eq d
  , Eq (BS.InitHint vs)
  , Eq (BS.WriteHint d)
  , Eq (BS.ReadHint vs)
  , Typeable ks
  , Typeable vs
  , Typeable k
  , Typeable d
  , Typeable (BS.WriteHint d)
  , QC.Arbitrary ks
  , QC.Arbitrary vs
  , QC.Arbitrary k
  , QC.Arbitrary d
  , QC.Arbitrary (BS.RangeQuery ks)
  , Mock.HasOps ks k vs d
  ) =>
  RunLockstep (BackingStoreState ks k vs d) (RealMonad IO ks k vs d)
  where
  observeReal ::
    Proxy (RealMonad IO ks k vs d) ->
    LockstepAction (BackingStoreState ks k vs d) a ->
    a ->
    BSObs ks k vs d a
  observeReal :: forall a.
Proxy (RealMonad IO ks k vs d)
-> LockstepAction (BackingStoreState ks k vs d) a
-> a
-> Observable (BackingStoreState ks k vs d) a
observeReal Proxy (RealMonad IO ks k vs d)
_proxy = \case
    BSInitFromValues WithOrigin SlotNo
_ InitHint vs
_ Values vs
_ -> Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
-> BSObs ks k vs d a
Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
-> BSObs ks k vs d (Either Err ())
forall ks k vs d a b.
Either (BSObs ks k vs d a) (BSObs ks k vs d b)
-> BSObs ks k vs d (Either a b)
OEither (Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
 -> BSObs ks k vs d a)
-> (a -> Either (BSObs ks k vs d Err) (BSObs ks k vs d ()))
-> a
-> BSObs ks k vs d a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Err -> BSObs ks k vs d Err)
-> (() -> BSObs ks k vs d ())
-> Either Err ()
-> Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Err -> BSObs ks k vs d Err
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId () -> BSObs ks k vs d ()
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId
    BSInitFromCopy InitHint vs
_ FsPath
_ -> Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
-> BSObs ks k vs d a
Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
-> BSObs ks k vs d (Either Err ())
forall ks k vs d a b.
Either (BSObs ks k vs d a) (BSObs ks k vs d b)
-> BSObs ks k vs d (Either a b)
OEither (Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
 -> BSObs ks k vs d a)
-> (a -> Either (BSObs ks k vs d Err) (BSObs ks k vs d ()))
-> a
-> BSObs ks k vs d a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Err -> BSObs ks k vs d Err)
-> (() -> BSObs ks k vs d ())
-> Either Err ()
-> Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Err -> BSObs ks k vs d Err
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId () -> BSObs ks k vs d ()
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId
    LockstepAction (BackingStoreState ks k vs d) a
R:ActionLockstepa ks k vs d a
BSClose -> Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
-> BSObs ks k vs d a
Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
-> BSObs ks k vs d (Either Err ())
forall ks k vs d a b.
Either (BSObs ks k vs d a) (BSObs ks k vs d b)
-> BSObs ks k vs d (Either a b)
OEither (Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
 -> BSObs ks k vs d a)
-> (a -> Either (BSObs ks k vs d Err) (BSObs ks k vs d ()))
-> a
-> BSObs ks k vs d a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Err -> BSObs ks k vs d Err)
-> (() -> BSObs ks k vs d ())
-> Either Err ()
-> Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Err -> BSObs ks k vs d Err
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId () -> BSObs ks k vs d ()
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId
    BSCopy SerializeTablesHint vs
_ FsPath
_ -> Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
-> BSObs ks k vs d a
Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
-> BSObs ks k vs d (Either Err ())
forall ks k vs d a b.
Either (BSObs ks k vs d a) (BSObs ks k vs d b)
-> BSObs ks k vs d (Either a b)
OEither (Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
 -> BSObs ks k vs d a)
-> (a -> Either (BSObs ks k vs d Err) (BSObs ks k vs d ()))
-> a
-> BSObs ks k vs d a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Err -> BSObs ks k vs d Err)
-> (() -> BSObs ks k vs d ())
-> Either Err ()
-> Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Err -> BSObs ks k vs d Err
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId () -> BSObs ks k vs d ()
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId
    LockstepAction (BackingStoreState ks k vs d) a
R:ActionLockstepa ks k vs d a
BSValueHandle -> Either
  (BSObs ks k vs d Err)
  (BSObs ks k vs d (BackingStoreValueHandle IO ks k vs))
-> BSObs ks k vs d a
Either
  (BSObs ks k vs d Err)
  (BSObs ks k vs d (BackingStoreValueHandle IO ks k vs))
-> BSObs
     ks k vs d (Either Err (BackingStoreValueHandle IO ks k vs))
forall ks k vs d a b.
Either (BSObs ks k vs d a) (BSObs ks k vs d b)
-> BSObs ks k vs d (Either a b)
OEither (Either
   (BSObs ks k vs d Err)
   (BSObs ks k vs d (BackingStoreValueHandle IO ks k vs))
 -> BSObs ks k vs d a)
-> (a
    -> Either
         (BSObs ks k vs d Err)
         (BSObs ks k vs d (BackingStoreValueHandle IO ks k vs)))
-> a
-> BSObs ks k vs d a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Err -> BSObs ks k vs d Err)
-> (BackingStoreValueHandle IO ks k vs
    -> BSObs ks k vs d (BackingStoreValueHandle IO ks k vs))
-> Either Err (BackingStoreValueHandle IO ks k vs)
-> Either
     (BSObs ks k vs d Err)
     (BSObs ks k vs d (BackingStoreValueHandle IO ks k vs))
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Err -> BSObs ks k vs d Err
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId (BSObs ks k vs d (BackingStoreValueHandle IO ks k vs)
-> BackingStoreValueHandle IO ks k vs
-> BSObs ks k vs d (BackingStoreValueHandle IO ks k vs)
forall a b. a -> b -> a
const BSObs ks k vs d (BackingStoreValueHandle IO ks k vs)
forall ks k vs d.
BSObs ks k vs d (BackingStoreValueHandle IO ks k vs)
OValueHandle)
    BSWrite SlotNo
_ WriteHint d
_ d
_ -> Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
-> BSObs ks k vs d a
Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
-> BSObs ks k vs d (Either Err ())
forall ks k vs d a b.
Either (BSObs ks k vs d a) (BSObs ks k vs d b)
-> BSObs ks k vs d (Either a b)
OEither (Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
 -> BSObs ks k vs d a)
-> (a -> Either (BSObs ks k vs d Err) (BSObs ks k vs d ()))
-> a
-> BSObs ks k vs d a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Err -> BSObs ks k vs d Err)
-> (() -> BSObs ks k vs d ())
-> Either Err ()
-> Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Err -> BSObs ks k vs d Err
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId () -> BSObs ks k vs d ()
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId
    BSVHClose BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
_ -> Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
-> BSObs ks k vs d a
Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
-> BSObs ks k vs d (Either Err ())
forall ks k vs d a b.
Either (BSObs ks k vs d a) (BSObs ks k vs d b)
-> BSObs ks k vs d (Either a b)
OEither (Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
 -> BSObs ks k vs d a)
-> (a -> Either (BSObs ks k vs d Err) (BSObs ks k vs d ()))
-> a
-> BSObs ks k vs d a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Err -> BSObs ks k vs d Err)
-> (() -> BSObs ks k vs d ())
-> Either Err ()
-> Either (BSObs ks k vs d Err) (BSObs ks k vs d ())
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Err -> BSObs ks k vs d Err
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId () -> BSObs ks k vs d ()
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId
    BSVHRangeRead BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
_ ReadHint vs
_ RangeQuery ks
_ -> Either (BSObs ks k vs d Err) (BSObs ks k vs d (Values vs, Maybe k))
-> BSObs ks k vs d a
Either (BSObs ks k vs d Err) (BSObs ks k vs d (Values vs, Maybe k))
-> BSObs ks k vs d (Either Err (Values vs, Maybe k))
forall ks k vs d a b.
Either (BSObs ks k vs d a) (BSObs ks k vs d b)
-> BSObs ks k vs d (Either a b)
OEither (Either
   (BSObs ks k vs d Err) (BSObs ks k vs d (Values vs, Maybe k))
 -> BSObs ks k vs d a)
-> (a
    -> Either
         (BSObs ks k vs d Err) (BSObs ks k vs d (Values vs, Maybe k)))
-> a
-> BSObs ks k vs d a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Err -> BSObs ks k vs d Err)
-> ((Values vs, Maybe k) -> BSObs ks k vs d (Values vs, Maybe k))
-> Either Err (Values vs, Maybe k)
-> Either
     (BSObs ks k vs d Err) (BSObs ks k vs d (Values vs, Maybe k))
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Err -> BSObs ks k vs d Err
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId ((vs, Maybe k) -> BSObs ks k vs d (Values vs, Maybe k)
forall a k ks vs d.
(Show a, Eq a, Typeable a) =>
(a, Maybe k) -> BSObs ks k vs d (Values a, Maybe k)
OValuesAndLast ((vs, Maybe k) -> BSObs ks k vs d (Values vs, Maybe k))
-> ((Values vs, Maybe k) -> (vs, Maybe k))
-> (Values vs, Maybe k)
-> BSObs ks k vs d (Values vs, Maybe k)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Values vs -> vs) -> (Values vs, Maybe k) -> (vs, Maybe k)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Values vs -> vs
forall vs. Values vs -> vs
unValues)
    BSVHRead BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
_ ReadHint vs
_ ks
_ -> Either (BSObs ks k vs d Err) (BSObs ks k vs d (Values vs))
-> BSObs ks k vs d a
Either (BSObs ks k vs d Err) (BSObs ks k vs d (Values vs))
-> BSObs ks k vs d (Either Err (Values vs))
forall ks k vs d a b.
Either (BSObs ks k vs d a) (BSObs ks k vs d b)
-> BSObs ks k vs d (Either a b)
OEither (Either (BSObs ks k vs d Err) (BSObs ks k vs d (Values vs))
 -> BSObs ks k vs d a)
-> (a
    -> Either (BSObs ks k vs d Err) (BSObs ks k vs d (Values vs)))
-> a
-> BSObs ks k vs d a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Err -> BSObs ks k vs d Err)
-> (Values vs -> BSObs ks k vs d (Values vs))
-> Either Err (Values vs)
-> Either (BSObs ks k vs d Err) (BSObs ks k vs d (Values vs))
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Err -> BSObs ks k vs d Err
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId (vs -> BSObs ks k vs d (Values vs)
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d (Values a)
OValues (vs -> BSObs ks k vs d (Values vs))
-> (Values vs -> vs) -> Values vs -> BSObs ks k vs d (Values vs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Values vs -> vs
forall vs. Values vs -> vs
unValues)
    BSVHAtSlot BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
_ -> Either (BSObs ks k vs d Err) (BSObs ks k vs d (WithOrigin SlotNo))
-> BSObs ks k vs d a
Either (BSObs ks k vs d Err) (BSObs ks k vs d (WithOrigin SlotNo))
-> BSObs ks k vs d (Either Err (WithOrigin SlotNo))
forall ks k vs d a b.
Either (BSObs ks k vs d a) (BSObs ks k vs d b)
-> BSObs ks k vs d (Either a b)
OEither (Either (BSObs ks k vs d Err) (BSObs ks k vs d (WithOrigin SlotNo))
 -> BSObs ks k vs d a)
-> (a
    -> Either
         (BSObs ks k vs d Err) (BSObs ks k vs d (WithOrigin SlotNo)))
-> a
-> BSObs ks k vs d a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Err -> BSObs ks k vs d Err)
-> (WithOrigin SlotNo -> BSObs ks k vs d (WithOrigin SlotNo))
-> Either Err (WithOrigin SlotNo)
-> Either
     (BSObs ks k vs d Err) (BSObs ks k vs d (WithOrigin SlotNo))
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Err -> BSObs ks k vs d Err
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId WithOrigin SlotNo -> BSObs ks k vs d (WithOrigin SlotNo)
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId
    BSVHStat BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
_ -> Either (BSObs ks k vs d Err) (BSObs ks k vs d Statistics)
-> BSObs ks k vs d a
Either (BSObs ks k vs d Err) (BSObs ks k vs d Statistics)
-> BSObs ks k vs d (Either Err Statistics)
forall ks k vs d a b.
Either (BSObs ks k vs d a) (BSObs ks k vs d b)
-> BSObs ks k vs d (Either a b)
OEither (Either (BSObs ks k vs d Err) (BSObs ks k vs d Statistics)
 -> BSObs ks k vs d a)
-> (a -> Either (BSObs ks k vs d Err) (BSObs ks k vs d Statistics))
-> a
-> BSObs ks k vs d a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Err -> BSObs ks k vs d Err)
-> (Statistics -> BSObs ks k vs d Statistics)
-> Either Err Statistics
-> Either (BSObs ks k vs d Err) (BSObs ks k vs d Statistics)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Err -> BSObs ks k vs d Err
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId Statistics -> BSObs ks k vs d Statistics
forall a ks k vs d.
(Show a, Eq a, Typeable a) =>
a -> BSObs ks k vs d a
OId

  showRealResponse ::
    Proxy (RealMonad IO ks k vs d) ->
    LockstepAction (BackingStoreState ks k vs d) a ->
    Maybe (Dict (Show a))
  showRealResponse :: forall a.
Proxy (RealMonad IO ks k vs d)
-> LockstepAction (BackingStoreState ks k vs d) a
-> Maybe (Dict (Show a))
showRealResponse Proxy (RealMonad IO ks k vs d)
_proxy = \case
    BSInitFromValues WithOrigin SlotNo
_ InitHint vs
_ Values vs
_ -> Dict (Show a) -> Maybe (Dict (Show a))
forall a. a -> Maybe a
Just Dict (Show a)
forall (a :: Constraint). a => Dict a
Dict
    BSInitFromCopy InitHint vs
_ FsPath
_ -> Dict (Show a) -> Maybe (Dict (Show a))
forall a. a -> Maybe a
Just Dict (Show a)
forall (a :: Constraint). a => Dict a
Dict
    LockstepAction (BackingStoreState ks k vs d) a
R:ActionLockstepa ks k vs d a
BSClose -> Dict (Show a) -> Maybe (Dict (Show a))
forall a. a -> Maybe a
Just Dict (Show a)
forall (a :: Constraint). a => Dict a
Dict
    BSCopy SerializeTablesHint vs
_ FsPath
_ -> Dict (Show a) -> Maybe (Dict (Show a))
forall a. a -> Maybe a
Just Dict (Show a)
forall (a :: Constraint). a => Dict a
Dict
    LockstepAction (BackingStoreState ks k vs d) a
R:ActionLockstepa ks k vs d a
BSValueHandle -> Maybe (Dict (Show a))
forall a. Maybe a
Nothing
    BSWrite SlotNo
_ WriteHint d
_ d
_ -> Dict (Show a) -> Maybe (Dict (Show a))
forall a. a -> Maybe a
Just Dict (Show a)
forall (a :: Constraint). a => Dict a
Dict
    BSVHClose BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
_ -> Dict (Show a) -> Maybe (Dict (Show a))
forall a. a -> Maybe a
Just Dict (Show a)
forall (a :: Constraint). a => Dict a
Dict
    BSVHRangeRead BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
_ ReadHint vs
_ RangeQuery ks
_ -> Dict (Show a) -> Maybe (Dict (Show a))
forall a. a -> Maybe a
Just Dict (Show a)
forall (a :: Constraint). a => Dict a
Dict
    BSVHRead BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
_ ReadHint vs
_ ks
_ -> Dict (Show a) -> Maybe (Dict (Show a))
forall a. a -> Maybe a
Just Dict (Show a)
forall (a :: Constraint). a => Dict a
Dict
    BSVHAtSlot BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
_ -> Dict (Show a) -> Maybe (Dict (Show a))
forall a. a -> Maybe a
Just Dict (Show a)
forall (a :: Constraint). a => Dict a
Dict
    BSVHStat BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
_ -> Dict (Show a) -> Maybe (Dict (Show a))
forall a. a -> Maybe a
Just Dict (Show a)
forall (a :: Constraint). a => Dict a
Dict

{-------------------------------------------------------------------------------
  Interpreter against the model
-------------------------------------------------------------------------------}

runMock ::
  forall ks k vs d a.
  ( Mock.HasOps ks k vs d
  , QC.Arbitrary ks
  , QC.Arbitrary vs
  , QC.Arbitrary k
  , QC.Arbitrary d
  , QC.Arbitrary (BS.RangeQuery ks)
  ) =>
  ModelVarContext (BackingStoreState ks k vs d) ->
  Action (Lockstep (BackingStoreState ks k vs d)) a ->
  Mock vs ->
  ( BSVal ks k vs d a
  , Mock vs
  )
runMock :: forall ks k vs d a.
(HasOps ks k vs d, Arbitrary ks, Arbitrary vs, Arbitrary k,
 Arbitrary d, Arbitrary (RangeQuery ks)) =>
ModelVarContext (BackingStoreState ks k vs d)
-> Action (Lockstep (BackingStoreState ks k vs d)) a
-> Mock vs
-> (BSVal ks k vs d a, Mock vs)
runMock ModelVarContext (BackingStoreState ks k vs d)
lookUp = \case
  BSInitFromValues WithOrigin SlotNo
sl InitHint vs
h (Values vs
vs) ->
    (() -> BSVal ks k vs d ())
-> (Either Err (), Mock vs)
-> (BSVal ks k vs d (Either Err ()), Mock vs)
forall {p :: * -> * -> *} {c} {ks} {k} {vs} {d} {b} {c}.
Bifunctor p =>
(c -> BSVal ks k vs d b)
-> p (Either Err c) c -> p (BSVal ks k vs d (Either Err b)) c
wrap () -> BSVal ks k vs d ()
forall ks k vs d. () -> BSVal ks k vs d ()
MUnit ((Either Err (), Mock vs) -> (BSVal ks k vs d a, Mock vs))
-> (Mock vs -> (Either Err (), Mock vs))
-> Mock vs
-> (BSVal ks k vs d a, Mock vs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MockMonad (ZonkAny 0) (ZonkAny 1) vs (ZonkAny 2) ()
-> Mock vs -> (Either Err (), Mock vs)
forall ks k vs d a.
MockMonad ks k vs d a -> Mock vs -> (Either Err a, Mock vs)
runMockMonad (WithOrigin SlotNo
-> InitHint vs
-> vs
-> MockMonad (ZonkAny 0) (ZonkAny 1) vs (ZonkAny 2) ()
forall vs (m :: * -> *).
MonadState (Mock vs) m =>
WithOrigin SlotNo -> InitHint vs -> vs -> m ()
Mock.mBSInitFromValues WithOrigin SlotNo
sl InitHint vs
h vs
vs)
  BSInitFromCopy InitHint vs
h FsPath
bsp ->
    (() -> BSVal ks k vs d ())
-> (Either Err (), Mock vs)
-> (BSVal ks k vs d (Either Err ()), Mock vs)
forall {p :: * -> * -> *} {c} {ks} {k} {vs} {d} {b} {c}.
Bifunctor p =>
(c -> BSVal ks k vs d b)
-> p (Either Err c) c -> p (BSVal ks k vs d (Either Err b)) c
wrap () -> BSVal ks k vs d ()
forall ks k vs d. () -> BSVal ks k vs d ()
MUnit ((Either Err (), Mock vs) -> (BSVal ks k vs d a, Mock vs))
-> (Mock vs -> (Either Err (), Mock vs))
-> Mock vs
-> (BSVal ks k vs d a, Mock vs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MockMonad (ZonkAny 3) (ZonkAny 4) vs (ZonkAny 5) ()
-> Mock vs -> (Either Err (), Mock vs)
forall ks k vs d a.
MockMonad ks k vs d a -> Mock vs -> (Either Err a, Mock vs)
runMockMonad (InitHint vs
-> FsPath -> MockMonad (ZonkAny 3) (ZonkAny 4) vs (ZonkAny 5) ()
forall vs (m :: * -> *).
(MonadState (Mock vs) m, MonadError Err m) =>
InitHint vs -> FsPath -> m ()
Mock.mBSInitFromCopy InitHint vs
h FsPath
bsp)
  Action (Lockstep (BackingStoreState ks k vs d)) a
R:ActionLockstepa ks k vs d a
BSClose ->
    (() -> BSVal ks k vs d ())
-> (Either Err (), Mock vs)
-> (BSVal ks k vs d (Either Err ()), Mock vs)
forall {p :: * -> * -> *} {c} {ks} {k} {vs} {d} {b} {c}.
Bifunctor p =>
(c -> BSVal ks k vs d b)
-> p (Either Err c) c -> p (BSVal ks k vs d (Either Err b)) c
wrap () -> BSVal ks k vs d ()
forall ks k vs d. () -> BSVal ks k vs d ()
MUnit ((Either Err (), Mock vs) -> (BSVal ks k vs d a, Mock vs))
-> (Mock vs -> (Either Err (), Mock vs))
-> Mock vs
-> (BSVal ks k vs d a, Mock vs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MockMonad (ZonkAny 6) (ZonkAny 7) vs (ZonkAny 8) ()
-> Mock vs -> (Either Err (), Mock vs)
forall ks k vs d a.
MockMonad ks k vs d a -> Mock vs -> (Either Err a, Mock vs)
runMockMonad MockMonad (ZonkAny 6) (ZonkAny 7) vs (ZonkAny 8) ()
forall vs (m :: * -> *). MonadState (Mock vs) m => m ()
Mock.mBSClose
  BSCopy SerializeTablesHint vs
h FsPath
bsp ->
    (() -> BSVal ks k vs d ())
-> (Either Err (), Mock vs)
-> (BSVal ks k vs d (Either Err ()), Mock vs)
forall {p :: * -> * -> *} {c} {ks} {k} {vs} {d} {b} {c}.
Bifunctor p =>
(c -> BSVal ks k vs d b)
-> p (Either Err c) c -> p (BSVal ks k vs d (Either Err b)) c
wrap () -> BSVal ks k vs d ()
forall ks k vs d. () -> BSVal ks k vs d ()
MUnit ((Either Err (), Mock vs) -> (BSVal ks k vs d a, Mock vs))
-> (Mock vs -> (Either Err (), Mock vs))
-> Mock vs
-> (BSVal ks k vs d a, Mock vs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MockMonad (ZonkAny 9) (ZonkAny 10) vs (ZonkAny 11) ()
-> Mock vs -> (Either Err (), Mock vs)
forall ks k vs d a.
MockMonad ks k vs d a -> Mock vs -> (Either Err a, Mock vs)
runMockMonad (SerializeTablesHint vs
-> FsPath -> MockMonad (ZonkAny 9) (ZonkAny 10) vs (ZonkAny 11) ()
forall vs (m :: * -> *).
(MonadState (Mock vs) m, MonadError Err m) =>
SerializeTablesHint vs -> FsPath -> m ()
Mock.mBSCopy SerializeTablesHint vs
h FsPath
bsp)
  Action (Lockstep (BackingStoreState ks k vs d)) a
R:ActionLockstepa ks k vs d a
BSValueHandle ->
    (ValueHandle vs
 -> BSVal ks k vs d (BackingStoreValueHandle IO ks k vs))
-> (Either Err (ValueHandle vs), Mock vs)
-> (BSVal
      ks k vs d (Either Err (BackingStoreValueHandle IO ks k vs)),
    Mock vs)
forall {p :: * -> * -> *} {c} {ks} {k} {vs} {d} {b} {c}.
Bifunctor p =>
(c -> BSVal ks k vs d b)
-> p (Either Err c) c -> p (BSVal ks k vs d (Either Err b)) c
wrap ValueHandle vs
-> BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
forall vs ks k d.
ValueHandle vs
-> BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
MValueHandle ((Either Err (ValueHandle vs), Mock vs)
 -> (BSVal ks k vs d a, Mock vs))
-> (Mock vs -> (Either Err (ValueHandle vs), Mock vs))
-> Mock vs
-> (BSVal ks k vs d a, Mock vs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MockMonad
  (ZonkAny 12) (ZonkAny 13) vs (ZonkAny 14) (ValueHandle vs)
-> Mock vs -> (Either Err (ValueHandle vs), Mock vs)
forall ks k vs d a.
MockMonad ks k vs d a -> Mock vs -> (Either Err a, Mock vs)
runMockMonad MockMonad
  (ZonkAny 12) (ZonkAny 13) vs (ZonkAny 14) (ValueHandle vs)
forall vs (m :: * -> *).
(MonadState (Mock vs) m, MonadError Err m) =>
m (ValueHandle vs)
Mock.mBSValueHandle
  BSWrite SlotNo
sl WriteHint d
whint d
d ->
    (() -> BSVal ks k vs d ())
-> (Either Err (), Mock vs)
-> (BSVal ks k vs d (Either Err ()), Mock vs)
forall {p :: * -> * -> *} {c} {ks} {k} {vs} {d} {b} {c}.
Bifunctor p =>
(c -> BSVal ks k vs d b)
-> p (Either Err c) c -> p (BSVal ks k vs d (Either Err b)) c
wrap () -> BSVal ks k vs d ()
forall ks k vs d. () -> BSVal ks k vs d ()
MUnit ((Either Err (), Mock vs) -> (BSVal ks k vs d a, Mock vs))
-> (Mock vs -> (Either Err (), Mock vs))
-> Mock vs
-> (BSVal ks k vs d a, Mock vs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MockMonad (ZonkAny 15) (ZonkAny 16) vs (ZonkAny 17) ()
-> Mock vs -> (Either Err (), Mock vs)
forall ks k vs d a.
MockMonad ks k vs d a -> Mock vs -> (Either Err a, Mock vs)
runMockMonad (SlotNo
-> WriteHint d
-> d
-> MockMonad (ZonkAny 15) (ZonkAny 16) vs (ZonkAny 17) ()
forall vs (m :: * -> *) d.
(MonadState (Mock vs) m, MonadError Err m, ApplyDiff vs d) =>
SlotNo -> WriteHint d -> d -> m ()
Mock.mBSWrite SlotNo
sl WriteHint d
whint d
d)
  BSVHClose BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h ->
    (() -> BSVal ks k vs d ())
-> (Either Err (), Mock vs)
-> (BSVal ks k vs d (Either Err ()), Mock vs)
forall {p :: * -> * -> *} {c} {ks} {k} {vs} {d} {b} {c}.
Bifunctor p =>
(c -> BSVal ks k vs d b)
-> p (Either Err c) c -> p (BSVal ks k vs d (Either Err b)) c
wrap () -> BSVal ks k vs d ()
forall ks k vs d. () -> BSVal ks k vs d ()
MUnit ((Either Err (), Mock vs) -> (BSVal ks k vs d a, Mock vs))
-> (Mock vs -> (Either Err (), Mock vs))
-> Mock vs
-> (BSVal ks k vs d a, Mock vs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MockMonad (ZonkAny 18) (ZonkAny 19) vs (ZonkAny 20) ()
-> Mock vs -> (Either Err (), Mock vs)
forall ks k vs d a.
MockMonad ks k vs d a -> Mock vs -> (Either Err a, Mock vs)
runMockMonad (ValueHandle vs
-> MockMonad (ZonkAny 18) (ZonkAny 19) vs (ZonkAny 20) ()
forall vs (m :: * -> *).
MonadState (Mock vs) m =>
ValueHandle vs -> m ()
Mock.mBSVHClose (BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ValueHandle vs
getHandle (BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
 -> ValueHandle vs)
-> BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ValueHandle vs
forall a b. (a -> b) -> a -> b
$ ModelVarContext (BackingStoreState ks k vs d)
-> ModelLookUp (BackingStoreState ks k vs d)
forall state.
InLockstep state =>
ModelVarContext state -> ModelLookUp state
lookupVar ModelVarContext (BackingStoreState ks k vs d)
lookUp BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h))
  BSVHRangeRead BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h ReadHint vs
rhint RangeQuery ks
rq ->
    ((vs, Maybe k) -> BSVal ks k vs d (Values vs, Maybe k))
-> (Either Err (vs, Maybe k), Mock vs)
-> (BSVal ks k vs d (Either Err (Values vs, Maybe k)), Mock vs)
forall {p :: * -> * -> *} {c} {ks} {k} {vs} {d} {b} {c}.
Bifunctor p =>
(c -> BSVal ks k vs d b)
-> p (Either Err c) c -> p (BSVal ks k vs d (Either Err b)) c
wrap (vs, Maybe k) -> BSVal ks k vs d (Values vs, Maybe k)
forall vs k ks d.
(vs, Maybe k) -> BSVal ks k vs d (Values vs, Maybe k)
MValuesAndLast ((Either Err (vs, Maybe k), Mock vs)
 -> (BSVal ks k vs d a, Mock vs))
-> (Mock vs -> (Either Err (vs, Maybe k), Mock vs))
-> Mock vs
-> (BSVal ks k vs d a, Mock vs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MockMonad (ZonkAny 21) (ZonkAny 22) vs (ZonkAny 23) (vs, Maybe k)
-> Mock vs -> (Either Err (vs, Maybe k), Mock vs)
forall ks k vs d a.
MockMonad ks k vs d a -> Mock vs -> (Either Err a, Mock vs)
runMockMonad (ValueHandle vs
-> ReadHint vs
-> RangeQuery ks
-> MockMonad
     (ZonkAny 21) (ZonkAny 22) vs (ZonkAny 23) (vs, Maybe k)
forall vs (m :: * -> *) ks k.
(MonadState (Mock vs) m, MonadError Err m,
 LookupKeysRange ks k vs) =>
ValueHandle vs -> ReadHint vs -> RangeQuery ks -> m (vs, Maybe k)
Mock.mBSVHRangeRead (BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ValueHandle vs
getHandle (BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
 -> ValueHandle vs)
-> BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ValueHandle vs
forall a b. (a -> b) -> a -> b
$ ModelVarContext (BackingStoreState ks k vs d)
-> ModelLookUp (BackingStoreState ks k vs d)
forall state.
InLockstep state =>
ModelVarContext state -> ModelLookUp state
lookupVar ModelVarContext (BackingStoreState ks k vs d)
lookUp BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h) ReadHint vs
rhint RangeQuery ks
rq)
  BSVHRead BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h ReadHint vs
rhint ks
ks ->
    (vs -> BSVal ks k vs d (Values vs))
-> (Either Err vs, Mock vs)
-> (BSVal ks k vs d (Either Err (Values vs)), Mock vs)
forall {p :: * -> * -> *} {c} {ks} {k} {vs} {d} {b} {c}.
Bifunctor p =>
(c -> BSVal ks k vs d b)
-> p (Either Err c) c -> p (BSVal ks k vs d (Either Err b)) c
wrap vs -> BSVal ks k vs d (Values vs)
forall vs ks k d. vs -> BSVal ks k vs d (Values vs)
MValues ((Either Err vs, Mock vs) -> (BSVal ks k vs d a, Mock vs))
-> (Mock vs -> (Either Err vs, Mock vs))
-> Mock vs
-> (BSVal ks k vs d a, Mock vs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MockMonad (ZonkAny 24) (ZonkAny 25) vs (ZonkAny 26) vs
-> Mock vs -> (Either Err vs, Mock vs)
forall ks k vs d a.
MockMonad ks k vs d a -> Mock vs -> (Either Err a, Mock vs)
runMockMonad (ValueHandle vs
-> ReadHint vs
-> ks
-> MockMonad (ZonkAny 24) (ZonkAny 25) vs (ZonkAny 26) vs
forall vs (m :: * -> *) ks.
(MonadState (Mock vs) m, MonadError Err m, LookupKeys ks vs) =>
ValueHandle vs -> ReadHint vs -> ks -> m vs
Mock.mBSVHRead (BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ValueHandle vs
getHandle (BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
 -> ValueHandle vs)
-> BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ValueHandle vs
forall a b. (a -> b) -> a -> b
$ ModelVarContext (BackingStoreState ks k vs d)
-> ModelLookUp (BackingStoreState ks k vs d)
forall state.
InLockstep state =>
ModelVarContext state -> ModelLookUp state
lookupVar ModelVarContext (BackingStoreState ks k vs d)
lookUp BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h) ReadHint vs
rhint ks
ks)
  BSVHAtSlot BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h ->
    (WithOrigin SlotNo -> BSVal ks k vs d (WithOrigin SlotNo))
-> (Either Err (WithOrigin SlotNo), Mock vs)
-> (BSVal ks k vs d (Either Err (WithOrigin SlotNo)), Mock vs)
forall {p :: * -> * -> *} {c} {ks} {k} {vs} {d} {b} {c}.
Bifunctor p =>
(c -> BSVal ks k vs d b)
-> p (Either Err c) c -> p (BSVal ks k vs d (Either Err b)) c
wrap WithOrigin SlotNo -> BSVal ks k vs d (WithOrigin SlotNo)
forall ks k vs d.
WithOrigin SlotNo -> BSVal ks k vs d (WithOrigin SlotNo)
MSlotNo ((Either Err (WithOrigin SlotNo), Mock vs)
 -> (BSVal ks k vs d a, Mock vs))
-> (Mock vs -> (Either Err (WithOrigin SlotNo), Mock vs))
-> Mock vs
-> (BSVal ks k vs d a, Mock vs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MockMonad
  (ZonkAny 27) (ZonkAny 28) vs (ZonkAny 29) (WithOrigin SlotNo)
-> Mock vs -> (Either Err (WithOrigin SlotNo), Mock vs)
forall ks k vs d a.
MockMonad ks k vs d a -> Mock vs -> (Either Err a, Mock vs)
runMockMonad (ValueHandle vs
-> MockMonad
     (ZonkAny 27) (ZonkAny 28) vs (ZonkAny 29) (WithOrigin SlotNo)
forall (m :: * -> *) vs.
Monad m =>
ValueHandle vs -> m (WithOrigin SlotNo)
Mock.mBSVHAtSlot (BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ValueHandle vs
getHandle (BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
 -> ValueHandle vs)
-> BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ValueHandle vs
forall a b. (a -> b) -> a -> b
$ ModelVarContext (BackingStoreState ks k vs d)
-> ModelLookUp (BackingStoreState ks k vs d)
forall state.
InLockstep state =>
ModelVarContext state -> ModelLookUp state
lookupVar ModelVarContext (BackingStoreState ks k vs d)
lookUp BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h))
  BSVHStat BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h ->
    (Statistics -> BSVal ks k vs d Statistics)
-> (Either Err Statistics, Mock vs)
-> (BSVal ks k vs d (Either Err Statistics), Mock vs)
forall {p :: * -> * -> *} {c} {ks} {k} {vs} {d} {b} {c}.
Bifunctor p =>
(c -> BSVal ks k vs d b)
-> p (Either Err c) c -> p (BSVal ks k vs d (Either Err b)) c
wrap Statistics -> BSVal ks k vs d Statistics
forall ks k vs d. Statistics -> BSVal ks k vs d Statistics
MStatistics ((Either Err Statistics, Mock vs) -> (BSVal ks k vs d a, Mock vs))
-> (Mock vs -> (Either Err Statistics, Mock vs))
-> Mock vs
-> (BSVal ks k vs d a, Mock vs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MockMonad (ZonkAny 30) (ZonkAny 31) vs (ZonkAny 32) Statistics
-> Mock vs -> (Either Err Statistics, Mock vs)
forall ks k vs d a.
MockMonad ks k vs d a -> Mock vs -> (Either Err a, Mock vs)
runMockMonad (ValueHandle vs
-> MockMonad (ZonkAny 30) (ZonkAny 31) vs (ZonkAny 32) Statistics
forall vs (m :: * -> *).
(MonadState (Mock vs) m, MonadError Err m, ValuesLength vs) =>
ValueHandle vs -> m Statistics
Mock.mBSVHStat (BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ValueHandle vs
getHandle (BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
 -> ValueHandle vs)
-> BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ValueHandle vs
forall a b. (a -> b) -> a -> b
$ ModelVarContext (BackingStoreState ks k vs d)
-> ModelLookUp (BackingStoreState ks k vs d)
forall state.
InLockstep state =>
ModelVarContext state -> ModelLookUp state
lookupVar ModelVarContext (BackingStoreState ks k vs d)
lookUp BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h))
 where
  wrap :: (c -> BSVal ks k vs d b)
-> p (Either Err c) c -> p (BSVal ks k vs d (Either Err b)) c
wrap c -> BSVal ks k vs d b
f = (Either Err c -> BSVal ks k vs d (Either Err b))
-> p (Either Err c) c -> p (BSVal ks k vs d (Either Err b)) c
forall a b c. (a -> b) -> p a c -> p b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Either (BSVal ks k vs d Err) (BSVal ks k vs d b)
-> BSVal ks k vs d (Either Err b)
forall ks k vs d a b.
Either (BSVal ks k vs d a) (BSVal ks k vs d b)
-> BSVal ks k vs d (Either a b)
MEither (Either (BSVal ks k vs d Err) (BSVal ks k vs d b)
 -> BSVal ks k vs d (Either Err b))
-> (Either Err c
    -> Either (BSVal ks k vs d Err) (BSVal ks k vs d b))
-> Either Err c
-> BSVal ks k vs d (Either Err b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Err -> BSVal ks k vs d Err)
-> (c -> BSVal ks k vs d b)
-> Either Err c
-> Either (BSVal ks k vs d Err) (BSVal ks k vs d b)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Err -> BSVal ks k vs d Err
forall ks k vs d. Err -> BSVal ks k vs d Err
MErr c -> BSVal ks k vs d b
f)

  getHandle :: BSVal ks k vs d (BS.BackingStoreValueHandle IO ks k vs) -> ValueHandle vs
  getHandle :: BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ValueHandle vs
getHandle (MValueHandle ValueHandle vs
h) = ValueHandle vs
h

{-------------------------------------------------------------------------------
  Generator
-------------------------------------------------------------------------------}

arbitraryBackingStoreAction ::
  forall ks k vs d.
  ( Mock.HasOps ks k vs d
  , QC.Arbitrary ks
  , QC.Arbitrary vs
  , QC.Arbitrary k
  , QC.Arbitrary d
  , QC.Arbitrary (BS.RangeQuery ks)
  ) =>
  ModelVarContext (BackingStoreState ks k vs d) ->
  BackingStoreState ks k vs d ->
  Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
arbitraryBackingStoreAction :: forall ks k vs d.
(HasOps ks k vs d, Arbitrary ks, Arbitrary vs, Arbitrary k,
 Arbitrary d, Arbitrary (RangeQuery ks)) =>
ModelVarContext (BackingStoreState ks k vs d)
-> BackingStoreState ks k vs d
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
arbitraryBackingStoreAction ModelVarContext (BackingStoreState ks k vs d)
fv (BackingStoreState Mock vs
mock Stats ks k vs d
_stats) =
  [(Int, Gen (Any (LockstepAction (BackingStoreState ks k vs d))))]
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
QC.frequency ([(Int, Gen (Any (LockstepAction (BackingStoreState ks k vs d))))]
 -> Gen (Any (LockstepAction (BackingStoreState ks k vs d))))
-> [(Int,
     Gen (Any (LockstepAction (BackingStoreState ks k vs d))))]
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> a -> b
$
    [(Int, Gen (Any (LockstepAction (BackingStoreState ks k vs d))))]
withoutVars
      [(Int, Gen (Any (LockstepAction (BackingStoreState ks k vs d))))]
-> [(Int,
     Gen (Any (LockstepAction (BackingStoreState ks k vs d))))]
-> [(Int,
     Gen (Any (LockstepAction (BackingStoreState ks k vs d))))]
forall a. [a] -> [a] -> [a]
++ case ModelVarContext (BackingStoreState ks k vs d)
-> ModelFindVariables (BackingStoreState ks k vs d)
forall state.
InLockstep state =>
ModelVarContext state -> ModelFindVariables state
findVars ModelVarContext (BackingStoreState ks k vs d)
fv (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Either Err (BS.BackingStoreValueHandle IO ks k vs))) of
        [] -> []
        [GVar
   (ModelOp (BackingStoreState ks k vs d))
   (Either Err (BackingStoreValueHandle IO ks k vs))]
vars -> Gen
  (GVar
     (ModelOp (BackingStoreState ks k vs d))
     (Either Err (BackingStoreValueHandle IO ks k vs)))
-> [(Int,
     Gen (Any (LockstepAction (BackingStoreState ks k vs d))))]
withVars ([GVar Op (Either Err (BackingStoreValueHandle IO ks k vs))]
-> Gen (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs)))
forall a. HasCallStack => [a] -> Gen a
QC.elements [GVar
   (ModelOp (BackingStoreState ks k vs d))
   (Either Err (BackingStoreValueHandle IO ks k vs))]
[GVar Op (Either Err (BackingStoreValueHandle IO ks k vs))]
vars)
 where
  withoutVars :: [(Int, Gen (Any (LockstepAction (BackingStoreState ks k vs d))))]
  withoutVars :: [(Int, Gen (Any (LockstepAction (BackingStoreState ks k vs d))))]
withoutVars =
    [
      ( Int
5
      , (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
 -> Any (LockstepAction (BackingStoreState ks k vs d)))
-> Gen
     (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
-> Any (LockstepAction (BackingStoreState ks k vs d))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen
   (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
 -> Gen (Any (LockstepAction (BackingStoreState ks k vs d))))
-> Gen
     (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> a -> b
$
          WithOrigin SlotNo
-> InitHint vs
-> Values vs
-> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
forall vs ks k d.
WithOrigin SlotNo -> InitHint vs -> Values vs -> BSAct ks k vs d ()
BSInitFromValues
            (WithOrigin SlotNo
 -> InitHint vs
 -> Values vs
 -> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen (WithOrigin SlotNo)
-> Gen
     (InitHint vs
      -> Values vs
      -> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (WithOrigin SlotNo)
forall a. Arbitrary a => Gen a
QC.arbitrary
            Gen
  (InitHint vs
   -> Values vs
   -> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen (InitHint vs)
-> Gen
     (Values vs
      -> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> InitHint vs -> Gen (InitHint vs)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proxy vs -> InitHint vs
forall vs. MakeInitHint vs => Proxy vs -> InitHint vs
Mock.makeInitHint (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @vs))
            Gen
  (Values vs
   -> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen (Values vs)
-> Gen
     (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (vs -> Values vs
forall vs. vs -> Values vs
Values (vs -> Values vs) -> Gen vs -> Gen (Values vs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen vs
forall a. Arbitrary a => Gen a
QC.arbitrary)
      )
    ,
      ( Int
5
      , (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
 -> Any (LockstepAction (BackingStoreState ks k vs d)))
-> Gen
     (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
-> Any (LockstepAction (BackingStoreState ks k vs d))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen
   (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
 -> Gen (Any (LockstepAction (BackingStoreState ks k vs d))))
-> Gen
     (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> a -> b
$
          InitHint vs
-> FsPath
-> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
forall vs ks k d. InitHint vs -> FsPath -> BSAct ks k vs d ()
BSInitFromCopy
            (InitHint vs
 -> FsPath
 -> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen (InitHint vs)
-> Gen
     (FsPath
      -> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InitHint vs -> Gen (InitHint vs)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proxy vs -> InitHint vs
forall vs. MakeInitHint vs => Proxy vs -> InitHint vs
Mock.makeInitHint (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @vs))
            Gen
  (FsPath
   -> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen FsPath
-> Gen
     (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen FsPath
genBackingStorePath
      )
    , (Int
2, Any (LockstepAction (BackingStoreState ks k vs d))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (LockstepAction (BackingStoreState ks k vs d))
 -> Gen (Any (LockstepAction (BackingStoreState ks k vs d))))
-> Any (LockstepAction (BackingStoreState ks k vs d))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> a -> b
$ Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
-> Any (LockstepAction (BackingStoreState ks k vs d))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
forall ks k vs d. BSAct ks k vs d ()
BSClose)
    , (Int
5, (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
 -> Any (LockstepAction (BackingStoreState ks k vs d)))
-> Gen
     (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
-> Any (LockstepAction (BackingStoreState ks k vs d))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen
   (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
 -> Gen (Any (LockstepAction (BackingStoreState ks k vs d))))
-> Gen
     (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> a -> b
$ SerializeTablesHint vs
-> FsPath
-> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
forall vs ks k d.
SerializeTablesHint vs -> FsPath -> BSAct ks k vs d ()
BSCopy (SerializeTablesHint vs
 -> FsPath
 -> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen (SerializeTablesHint vs)
-> Gen
     (FsPath
      -> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SerializeTablesHint vs -> Gen (SerializeTablesHint vs)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proxy vs -> SerializeTablesHint vs
forall vs.
MakeSerializeTablesHint vs =>
Proxy vs -> SerializeTablesHint vs
Mock.makeSerializeTablesHint (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @vs)) Gen
  (FsPath
   -> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen FsPath
-> Gen
     (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen FsPath
genBackingStorePath)
    , (Int
5, Any (LockstepAction (BackingStoreState ks k vs d))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (LockstepAction (BackingStoreState ks k vs d))
 -> Gen (Any (LockstepAction (BackingStoreState ks k vs d))))
-> Any (LockstepAction (BackingStoreState ks k vs d))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> a -> b
$ Action
  (Lockstep (BackingStoreState ks k vs d))
  (Either Err (BackingStoreValueHandle IO ks k vs))
-> Any (LockstepAction (BackingStoreState ks k vs d))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Action
  (Lockstep (BackingStoreState ks k vs d))
  (Either Err (BackingStoreValueHandle IO ks k vs))
forall ks k vs d.
BSAct ks k vs d (BackingStoreValueHandle IO ks k vs)
BSValueHandle)
    ,
      ( Int
5
      , (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
 -> Any (LockstepAction (BackingStoreState ks k vs d)))
-> Gen
     (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
-> Any (LockstepAction (BackingStoreState ks k vs d))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen
   (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
 -> Gen (Any (LockstepAction (BackingStoreState ks k vs d))))
-> Gen
     (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> a -> b
$
          SlotNo
-> WriteHint d
-> d
-> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
forall d ks k vs. SlotNo -> WriteHint d -> d -> BSAct ks k vs d ()
BSWrite
            (SlotNo
 -> WriteHint d
 -> d
 -> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen SlotNo
-> Gen
     (WriteHint d
      -> d
      -> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen SlotNo
genSlotNo
            Gen
  (WriteHint d
   -> d
   -> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen (WriteHint d)
-> Gen
     (d
      -> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> WriteHint d -> Gen (WriteHint d)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proxy d -> WriteHint d
forall d. MakeWriteHint d => Proxy d -> WriteHint d
Mock.makeWriteHint (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @d))
            Gen
  (d
   -> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen d
-> Gen
     (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen d
genDiff
      )
    ]

  withVars ::
    Gen (BSVar ks k vs d (Either Err (BS.BackingStoreValueHandle IO ks k vs))) ->
    [(Int, Gen (Any (LockstepAction (BackingStoreState ks k vs d))))]
  withVars :: Gen
  (GVar
     (ModelOp (BackingStoreState ks k vs d))
     (Either Err (BackingStoreValueHandle IO ks k vs)))
-> [(Int,
     Gen (Any (LockstepAction (BackingStoreState ks k vs d))))]
withVars Gen
  (GVar
     (ModelOp (BackingStoreState ks k vs d))
     (Either Err (BackingStoreValueHandle IO ks k vs)))
genVar =
    [ (Int
5, (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
 -> Any (LockstepAction (BackingStoreState ks k vs d)))
-> Gen
     (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
-> Any (LockstepAction (BackingStoreState ks k vs d))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen
   (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
 -> Gen (Any (LockstepAction (BackingStoreState ks k vs d))))
-> Gen
     (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> a -> b
$ BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
-> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
GVar Op (BackingStoreValueHandle IO ks k vs)
-> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
forall ks k vs d.
BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
-> BSAct ks k vs d ()
BSVHClose (GVar Op (BackingStoreValueHandle IO ks k vs)
 -> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
-> Gen (GVar Op (BackingStoreValueHandle IO ks k vs))
-> Gen
     (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ()))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs))
-> GVar Op (BackingStoreValueHandle IO ks k vs)
forall a. GVar Op (Either Err a) -> GVar Op a
opFromRight (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs))
 -> GVar Op (BackingStoreValueHandle IO ks k vs))
-> Gen (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs)))
-> Gen (GVar Op (BackingStoreValueHandle IO ks k vs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen
  (GVar
     (ModelOp (BackingStoreState ks k vs d))
     (Either Err (BackingStoreValueHandle IO ks k vs)))
Gen (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs)))
genVar))
    ,
      ( Int
5
      , (Action
   (Lockstep (BackingStoreState ks k vs d))
   (Either Err (Values vs, Maybe k))
 -> Any (LockstepAction (BackingStoreState ks k vs d)))
-> Gen
     (Action
        (Lockstep (BackingStoreState ks k vs d))
        (Either Err (Values vs, Maybe k)))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action
  (Lockstep (BackingStoreState ks k vs d))
  (Either Err (Values vs, Maybe k))
-> Any (LockstepAction (BackingStoreState ks k vs d))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen
   (Action
      (Lockstep (BackingStoreState ks k vs d))
      (Either Err (Values vs, Maybe k)))
 -> Gen (Any (LockstepAction (BackingStoreState ks k vs d))))
-> Gen
     (Action
        (Lockstep (BackingStoreState ks k vs d))
        (Either Err (Values vs, Maybe k)))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> a -> b
$
          BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ReadHint vs
-> RangeQuery ks
-> Action
     (Lockstep (BackingStoreState ks k vs d))
     (Either Err (Values vs, Maybe k))
GVar Op (BackingStoreValueHandle IO ks k vs)
-> ReadHint vs
-> RangeQuery ks
-> Action
     (Lockstep (BackingStoreState ks k vs d))
     (Either Err (Values vs, Maybe k))
forall ks k vs d.
BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ReadHint vs
-> RangeQuery ks
-> BSAct ks k vs d (Values vs, Maybe k)
BSVHRangeRead
            (GVar Op (BackingStoreValueHandle IO ks k vs)
 -> ReadHint vs
 -> RangeQuery ks
 -> Action
      (Lockstep (BackingStoreState ks k vs d))
      (Either Err (Values vs, Maybe k)))
-> Gen (GVar Op (BackingStoreValueHandle IO ks k vs))
-> Gen
     (ReadHint vs
      -> RangeQuery ks
      -> Action
           (Lockstep (BackingStoreState ks k vs d))
           (Either Err (Values vs, Maybe k)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs))
-> GVar Op (BackingStoreValueHandle IO ks k vs)
forall a. GVar Op (Either Err a) -> GVar Op a
opFromRight (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs))
 -> GVar Op (BackingStoreValueHandle IO ks k vs))
-> Gen (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs)))
-> Gen (GVar Op (BackingStoreValueHandle IO ks k vs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen
  (GVar
     (ModelOp (BackingStoreState ks k vs d))
     (Either Err (BackingStoreValueHandle IO ks k vs)))
Gen (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs)))
genVar)
            Gen
  (ReadHint vs
   -> RangeQuery ks
   -> Action
        (Lockstep (BackingStoreState ks k vs d))
        (Either Err (Values vs, Maybe k)))
-> Gen (ReadHint vs)
-> Gen
     (RangeQuery ks
      -> Action
           (Lockstep (BackingStoreState ks k vs d))
           (Either Err (Values vs, Maybe k)))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadHint vs -> Gen (ReadHint vs)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proxy vs -> ReadHint vs
forall vs. MakeReadHint vs => Proxy vs -> ReadHint vs
Mock.makeReadHint (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @vs))
            Gen
  (RangeQuery ks
   -> Action
        (Lockstep (BackingStoreState ks k vs d))
        (Either Err (Values vs, Maybe k)))
-> Gen (RangeQuery ks)
-> Gen
     (Action
        (Lockstep (BackingStoreState ks k vs d))
        (Either Err (Values vs, Maybe k)))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (RangeQuery ks)
forall a. Arbitrary a => Gen a
QC.arbitrary
      )
    ,
      ( Int
5
      , (Action
   (Lockstep (BackingStoreState ks k vs d)) (Either Err (Values vs))
 -> Any (LockstepAction (BackingStoreState ks k vs d)))
-> Gen
     (Action
        (Lockstep (BackingStoreState ks k vs d)) (Either Err (Values vs)))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action
  (Lockstep (BackingStoreState ks k vs d)) (Either Err (Values vs))
-> Any (LockstepAction (BackingStoreState ks k vs d))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen
   (Action
      (Lockstep (BackingStoreState ks k vs d)) (Either Err (Values vs)))
 -> Gen (Any (LockstepAction (BackingStoreState ks k vs d))))
-> Gen
     (Action
        (Lockstep (BackingStoreState ks k vs d)) (Either Err (Values vs)))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> a -> b
$
          BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ReadHint vs
-> ks
-> Action
     (Lockstep (BackingStoreState ks k vs d)) (Either Err (Values vs))
GVar Op (BackingStoreValueHandle IO ks k vs)
-> ReadHint vs
-> ks
-> Action
     (Lockstep (BackingStoreState ks k vs d)) (Either Err (Values vs))
forall ks k vs d.
BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ReadHint vs -> ks -> BSAct ks k vs d (Values vs)
BSVHRead
            (GVar Op (BackingStoreValueHandle IO ks k vs)
 -> ReadHint vs
 -> ks
 -> Action
      (Lockstep (BackingStoreState ks k vs d)) (Either Err (Values vs)))
-> Gen (GVar Op (BackingStoreValueHandle IO ks k vs))
-> Gen
     (ReadHint vs
      -> ks
      -> Action
           (Lockstep (BackingStoreState ks k vs d)) (Either Err (Values vs)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs))
-> GVar Op (BackingStoreValueHandle IO ks k vs)
forall a. GVar Op (Either Err a) -> GVar Op a
opFromRight (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs))
 -> GVar Op (BackingStoreValueHandle IO ks k vs))
-> Gen (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs)))
-> Gen (GVar Op (BackingStoreValueHandle IO ks k vs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen
  (GVar
     (ModelOp (BackingStoreState ks k vs d))
     (Either Err (BackingStoreValueHandle IO ks k vs)))
Gen (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs)))
genVar)
            Gen
  (ReadHint vs
   -> ks
   -> Action
        (Lockstep (BackingStoreState ks k vs d)) (Either Err (Values vs)))
-> Gen (ReadHint vs)
-> Gen
     (ks
      -> Action
           (Lockstep (BackingStoreState ks k vs d)) (Either Err (Values vs)))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadHint vs -> Gen (ReadHint vs)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proxy vs -> ReadHint vs
forall vs. MakeReadHint vs => Proxy vs -> ReadHint vs
Mock.makeReadHint (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @vs))
            Gen
  (ks
   -> Action
        (Lockstep (BackingStoreState ks k vs d)) (Either Err (Values vs)))
-> Gen ks
-> Gen
     (Action
        (Lockstep (BackingStoreState ks k vs d)) (Either Err (Values vs)))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen ks
forall a. Arbitrary a => Gen a
QC.arbitrary
      )
    , (Int
5, (Action
   (Lockstep (BackingStoreState ks k vs d))
   (Either Err (WithOrigin SlotNo))
 -> Any (LockstepAction (BackingStoreState ks k vs d)))
-> Gen
     (Action
        (Lockstep (BackingStoreState ks k vs d))
        (Either Err (WithOrigin SlotNo)))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action
  (Lockstep (BackingStoreState ks k vs d))
  (Either Err (WithOrigin SlotNo))
-> Any (LockstepAction (BackingStoreState ks k vs d))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen
   (Action
      (Lockstep (BackingStoreState ks k vs d))
      (Either Err (WithOrigin SlotNo)))
 -> Gen (Any (LockstepAction (BackingStoreState ks k vs d))))
-> Gen
     (Action
        (Lockstep (BackingStoreState ks k vs d))
        (Either Err (WithOrigin SlotNo)))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> a -> b
$ BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
-> Action
     (Lockstep (BackingStoreState ks k vs d))
     (Either Err (WithOrigin SlotNo))
GVar Op (BackingStoreValueHandle IO ks k vs)
-> Action
     (Lockstep (BackingStoreState ks k vs d))
     (Either Err (WithOrigin SlotNo))
forall ks k vs d.
BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
-> BSAct ks k vs d (WithOrigin SlotNo)
BSVHAtSlot (GVar Op (BackingStoreValueHandle IO ks k vs)
 -> Action
      (Lockstep (BackingStoreState ks k vs d))
      (Either Err (WithOrigin SlotNo)))
-> Gen (GVar Op (BackingStoreValueHandle IO ks k vs))
-> Gen
     (Action
        (Lockstep (BackingStoreState ks k vs d))
        (Either Err (WithOrigin SlotNo)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs))
-> GVar Op (BackingStoreValueHandle IO ks k vs)
forall a. GVar Op (Either Err a) -> GVar Op a
opFromRight (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs))
 -> GVar Op (BackingStoreValueHandle IO ks k vs))
-> Gen (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs)))
-> Gen (GVar Op (BackingStoreValueHandle IO ks k vs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen
  (GVar
     (ModelOp (BackingStoreState ks k vs d))
     (Either Err (BackingStoreValueHandle IO ks k vs)))
Gen (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs)))
genVar))
    , (Int
5, (Action
   (Lockstep (BackingStoreState ks k vs d)) (Either Err Statistics)
 -> Any (LockstepAction (BackingStoreState ks k vs d)))
-> Gen
     (Action
        (Lockstep (BackingStoreState ks k vs d)) (Either Err Statistics))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action
  (Lockstep (BackingStoreState ks k vs d)) (Either Err Statistics)
-> Any (LockstepAction (BackingStoreState ks k vs d))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Gen
   (Action
      (Lockstep (BackingStoreState ks k vs d)) (Either Err Statistics))
 -> Gen (Any (LockstepAction (BackingStoreState ks k vs d))))
-> Gen
     (Action
        (Lockstep (BackingStoreState ks k vs d)) (Either Err Statistics))
-> Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
forall a b. (a -> b) -> a -> b
$ BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
-> Action
     (Lockstep (BackingStoreState ks k vs d)) (Either Err Statistics)
GVar Op (BackingStoreValueHandle IO ks k vs)
-> Action
     (Lockstep (BackingStoreState ks k vs d)) (Either Err Statistics)
forall ks k vs d.
BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
-> BSAct ks k vs d Statistics
BSVHStat (GVar Op (BackingStoreValueHandle IO ks k vs)
 -> Action
      (Lockstep (BackingStoreState ks k vs d)) (Either Err Statistics))
-> Gen (GVar Op (BackingStoreValueHandle IO ks k vs))
-> Gen
     (Action
        (Lockstep (BackingStoreState ks k vs d)) (Either Err Statistics))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs))
-> GVar Op (BackingStoreValueHandle IO ks k vs)
forall a. GVar Op (Either Err a) -> GVar Op a
opFromRight (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs))
 -> GVar Op (BackingStoreValueHandle IO ks k vs))
-> Gen (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs)))
-> Gen (GVar Op (BackingStoreValueHandle IO ks k vs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen
  (GVar
     (ModelOp (BackingStoreState ks k vs d))
     (Either Err (BackingStoreValueHandle IO ks k vs)))
Gen (GVar Op (Either Err (BackingStoreValueHandle IO ks k vs)))
genVar))
    ]
   where
    opFromRight :: forall a. GVar Op (Either Err a) -> GVar Op a
    opFromRight :: forall a. GVar Op (Either Err a) -> GVar Op a
opFromRight = (forall x. Op x (Either Err a) -> Op x a)
-> GVar Op (Either Err a) -> GVar Op a
forall {k} (op :: * -> k -> *) (a :: k) (b :: k).
(forall x. op x a -> op x b) -> GVar op a -> GVar op b
mapGVar (\Op x (Either Err a)
op -> Op (Either Err a) a
forall b1 b. Op (Either b1 b) b
OpRight Op (Either Err a) a -> Op x (Either Err a) -> Op x a
forall b1 b a. Op b1 b -> Op a b1 -> Op a b
`OpComp` Op x (Either Err a)
op)

  genBackingStorePath :: Gen FS.FsPath
  genBackingStorePath :: Gen FsPath
genBackingStorePath = do
    file <- Gen String
genBSPFile
    pure . mkFsPath $ ["copies", file]

  -- Generate a file name for a copy of the backing store contents. We keep
  -- the set of possible file names small, such that errors (i.e., file alread
  -- exists) occur most of the time.
  genBSPFile :: Gen String
  genBSPFile :: Gen String
genBSPFile = [String] -> Gen String
forall a. HasCallStack => [a] -> Gen a
QC.elements [Int -> String
forall a. Show a => a -> String
show Int
x | Int
x <- [Int
1 :: Int .. Int
10]]

  -- Generate a slot number that is close before, at, or after the backing
  -- store's current slot number. A
  genSlotNo :: Gen SlotNo
  genSlotNo :: Gen SlotNo
genSlotNo = do
    n :: Int <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
QC.choose (-Int
5, Int
5)
    pure $ maybe 0 (+ fromIntegral n) (withOriginToMaybe seqNo)
   where
    seqNo :: WithOrigin SlotNo
seqNo = Mock vs -> WithOrigin SlotNo
forall vs. Mock vs -> WithOrigin SlotNo
backingSeqNo Mock vs
mock

  -- Generate valid diffs most of the time, and generate fully arbitrary
  -- (probably invalid) diffs some of the time.
  genDiff :: Gen d
  genDiff :: Gen d
genDiff =
    [(Int, Gen d)] -> Gen d
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
QC.frequency
      [ (Int
9, vs -> vs -> d
forall vs d. MakeDiff vs d => vs -> vs -> d
Mock.diff (Mock vs -> vs
forall vs. Mock vs -> vs
backingValues Mock vs
mock) (vs -> d) -> Gen vs -> Gen d
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen vs
forall a. Arbitrary a => Gen a
QC.arbitrary)
      , (Int
1, Gen d
forall a. Arbitrary a => Gen a
QC.arbitrary)
      ]

{-------------------------------------------------------------------------------
  Shrinker
-------------------------------------------------------------------------------}

shrinkBackingStoreAction ::
  forall ks k vs d a.
  ( Typeable vs
  , Typeable k
  , Eq ks
  , Eq vs
  , Eq d
  , Eq (BS.InitHint vs)
  , Eq (BS.WriteHint d)
  , Eq (BS.ReadHint vs)
  , Eq (SerializeTablesHint vs)
  , QC.Arbitrary d
  , QC.Arbitrary (BS.RangeQuery ks)
  , QC.Arbitrary ks
  ) =>
  ModelVarContext (BackingStoreState ks k vs d) ->
  BackingStoreState ks k vs d ->
  LockstepAction (BackingStoreState ks k vs d) a ->
  [Any (LockstepAction (BackingStoreState ks k vs d))]
shrinkBackingStoreAction :: forall ks k vs d a.
(Typeable vs, Typeable k, Eq ks, Eq vs, Eq d, Eq (InitHint vs),
 Eq (WriteHint d), Eq (ReadHint vs), Eq (SerializeTablesHint vs),
 Arbitrary d, Arbitrary (RangeQuery ks), Arbitrary ks) =>
ModelVarContext (BackingStoreState ks k vs d)
-> BackingStoreState ks k vs d
-> LockstepAction (BackingStoreState ks k vs d) a
-> [Any (LockstepAction (BackingStoreState ks k vs d))]
shrinkBackingStoreAction ModelVarContext (BackingStoreState ks k vs d)
_findVars (BackingStoreState Mock vs
_mock Stats ks k vs d
_) = \case
  BSWrite SlotNo
sl WriteHint d
st d
d ->
    [Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
-> Any (LockstepAction (BackingStoreState ks k vs d))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
 -> Any (LockstepAction (BackingStoreState ks k vs d)))
-> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
-> Any (LockstepAction (BackingStoreState ks k vs d))
forall a b. (a -> b) -> a -> b
$ SlotNo
-> WriteHint d
-> d
-> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
forall d ks k vs. SlotNo -> WriteHint d -> d -> BSAct ks k vs d ()
BSWrite SlotNo
sl WriteHint d
st d
d' | d
d' <- d -> [d]
forall a. Arbitrary a => a -> [a]
QC.shrink d
d]
      [Any (LockstepAction (BackingStoreState ks k vs d))]
-> [Any (LockstepAction (BackingStoreState ks k vs d))]
-> [Any (LockstepAction (BackingStoreState ks k vs d))]
forall a. [a] -> [a] -> [a]
++ [Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
-> Any (LockstepAction (BackingStoreState ks k vs d))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
 -> Any (LockstepAction (BackingStoreState ks k vs d)))
-> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
-> Any (LockstepAction (BackingStoreState ks k vs d))
forall a b. (a -> b) -> a -> b
$ SlotNo
-> WriteHint d
-> d
-> Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
forall d ks k vs. SlotNo -> WriteHint d -> d -> BSAct ks k vs d ()
BSWrite SlotNo
sl' WriteHint d
st d
d | SlotNo
sl' <- SlotNo -> [SlotNo]
forall a. Arbitrary a => a -> [a]
QC.shrink SlotNo
sl]
  BSVHRangeRead BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h ReadHint vs
rhint RangeQuery ks
rq ->
    [Action
  (Lockstep (BackingStoreState ks k vs d))
  (Either Err (Values vs, Maybe k))
-> Any (LockstepAction (BackingStoreState ks k vs d))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action
   (Lockstep (BackingStoreState ks k vs d))
   (Either Err (Values vs, Maybe k))
 -> Any (LockstepAction (BackingStoreState ks k vs d)))
-> Action
     (Lockstep (BackingStoreState ks k vs d))
     (Either Err (Values vs, Maybe k))
-> Any (LockstepAction (BackingStoreState ks k vs d))
forall a b. (a -> b) -> a -> b
$ BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ReadHint vs
-> RangeQuery ks
-> Action
     (Lockstep (BackingStoreState ks k vs d))
     (Either Err (Values vs, Maybe k))
forall ks k vs d.
BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ReadHint vs
-> RangeQuery ks
-> BSAct ks k vs d (Values vs, Maybe k)
BSVHRangeRead BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h ReadHint vs
rhint RangeQuery ks
rq' | RangeQuery ks
rq' <- RangeQuery ks -> [RangeQuery ks]
forall a. Arbitrary a => a -> [a]
QC.shrink RangeQuery ks
rq]
  BSVHRead BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h ReadHint vs
rhint ks
ks ->
    [Action
  (Lockstep (BackingStoreState ks k vs d)) (Either Err (Values vs))
-> Any (LockstepAction (BackingStoreState ks k vs d))
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action
   (Lockstep (BackingStoreState ks k vs d)) (Either Err (Values vs))
 -> Any (LockstepAction (BackingStoreState ks k vs d)))
-> Action
     (Lockstep (BackingStoreState ks k vs d)) (Either Err (Values vs))
-> Any (LockstepAction (BackingStoreState ks k vs d))
forall a b. (a -> b) -> a -> b
$ BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ReadHint vs
-> ks
-> Action
     (Lockstep (BackingStoreState ks k vs d)) (Either Err (Values vs))
forall ks k vs d.
BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ReadHint vs -> ks -> BSAct ks k vs d (Values vs)
BSVHRead BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h ReadHint vs
rhint ks
ks' | ks
ks' <- ks -> [ks]
forall a. Arbitrary a => a -> [a]
QC.shrink ks
ks]
  LockstepAction (BackingStoreState ks k vs d) a
_ -> []

{-------------------------------------------------------------------------------
  Interpret @'Op'@ against @'ModelValue'@
-------------------------------------------------------------------------------}

instance InterpretOp Op (ModelValue (BackingStoreState ks k vs d)) where
  intOp :: forall a b.
Op a b
-> ModelValue (BackingStoreState ks k vs d) a
-> Maybe (ModelValue (BackingStoreState ks k vs d) b)
intOp Op a b
OpId = ModelValue (BackingStoreState ks k vs d) a
-> Maybe (ModelValue (BackingStoreState ks k vs d) a)
ModelValue (BackingStoreState ks k vs d) a
-> Maybe (ModelValue (BackingStoreState ks k vs d) b)
forall a. a -> Maybe a
Just
  intOp Op a b
OpFst = \case
    MPair (BSVal ks k vs d a, BSVal ks k vs d b)
x -> ModelValue (BackingStoreState ks k vs d) b
-> Maybe (ModelValue (BackingStoreState ks k vs d) b)
forall a. a -> Maybe a
Just ((ModelValue (BackingStoreState ks k vs d) b, BSVal ks k vs d b)
-> ModelValue (BackingStoreState ks k vs d) b
forall a b. (a, b) -> a
fst (ModelValue (BackingStoreState ks k vs d) b, BSVal ks k vs d b)
(BSVal ks k vs d a, BSVal ks k vs d b)
x)
    MValuesAndLast{} -> String -> Maybe (ModelValue (BackingStoreState ks k vs d) b)
forall a. HasCallStack => String -> a
error String
"What?"
  intOp Op a b
OpSnd = \case
    MPair (BSVal ks k vs d a, BSVal ks k vs d b)
x -> ModelValue (BackingStoreState ks k vs d) b
-> Maybe (ModelValue (BackingStoreState ks k vs d) b)
forall a. a -> Maybe a
Just ((BSVal ks k vs d a, ModelValue (BackingStoreState ks k vs d) b)
-> ModelValue (BackingStoreState ks k vs d) b
forall a b. (a, b) -> b
snd (BSVal ks k vs d a, ModelValue (BackingStoreState ks k vs d) b)
(BSVal ks k vs d a, BSVal ks k vs d b)
x)
    MValuesAndLast{} -> String -> Maybe (ModelValue (BackingStoreState ks k vs d) b)
forall a. HasCallStack => String -> a
error String
"What?"
  intOp Op a b
OpLeft = \case MEither Either (BSVal ks k vs d a) (BSVal ks k vs d b)
x -> (ModelValue (BackingStoreState ks k vs d) b
 -> Maybe (ModelValue (BackingStoreState ks k vs d) b))
-> (BSVal ks k vs d b
    -> Maybe (ModelValue (BackingStoreState ks k vs d) b))
-> Either
     (ModelValue (BackingStoreState ks k vs d) b) (BSVal ks k vs d b)
-> Maybe (ModelValue (BackingStoreState ks k vs d) b)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ModelValue (BackingStoreState ks k vs d) b
-> Maybe (ModelValue (BackingStoreState ks k vs d) b)
forall a. a -> Maybe a
Just (Maybe (ModelValue (BackingStoreState ks k vs d) b)
-> BSVal ks k vs d b
-> Maybe (ModelValue (BackingStoreState ks k vs d) b)
forall a b. a -> b -> a
const Maybe (ModelValue (BackingStoreState ks k vs d) b)
forall a. Maybe a
Nothing) Either
  (ModelValue (BackingStoreState ks k vs d) b) (BSVal ks k vs d b)
Either (BSVal ks k vs d a) (BSVal ks k vs d b)
x
  intOp Op a b
OpRight = \case MEither Either (BSVal ks k vs d a) (BSVal ks k vs d b)
x -> (BSVal ks k vs d a
 -> Maybe (ModelValue (BackingStoreState ks k vs d) b))
-> (ModelValue (BackingStoreState ks k vs d) b
    -> Maybe (ModelValue (BackingStoreState ks k vs d) b))
-> Either
     (BSVal ks k vs d a) (ModelValue (BackingStoreState ks k vs d) b)
-> Maybe (ModelValue (BackingStoreState ks k vs d) b)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe (ModelValue (BackingStoreState ks k vs d) b)
-> BSVal ks k vs d a
-> Maybe (ModelValue (BackingStoreState ks k vs d) b)
forall a b. a -> b -> a
const Maybe (ModelValue (BackingStoreState ks k vs d) b)
forall a. Maybe a
Nothing) ModelValue (BackingStoreState ks k vs d) b
-> Maybe (ModelValue (BackingStoreState ks k vs d) b)
forall a. a -> Maybe a
Just Either
  (BSVal ks k vs d a) (ModelValue (BackingStoreState ks k vs d) b)
Either (BSVal ks k vs d a) (BSVal ks k vs d b)
x
  intOp (OpComp Op b1 b
g Op a b1
f) = Op b1 b
-> ModelValue (BackingStoreState ks k vs d) b1
-> Maybe (ModelValue (BackingStoreState ks k vs d) b)
forall a b.
Op a b
-> ModelValue (BackingStoreState ks k vs d) a
-> Maybe (ModelValue (BackingStoreState ks k vs d) b)
forall {k} (op :: k -> k -> *) (f :: k -> *) (a :: k) (b :: k).
InterpretOp op f =>
op a b -> f a -> Maybe (f b)
intOp Op b1 b
g (ModelValue (BackingStoreState ks k vs d) b1
 -> Maybe (ModelValue (BackingStoreState ks k vs d) b))
-> (ModelValue (BackingStoreState ks k vs d) a
    -> Maybe (ModelValue (BackingStoreState ks k vs d) b1))
-> ModelValue (BackingStoreState ks k vs d) a
-> Maybe (ModelValue (BackingStoreState ks k vs d) b)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Op a b1
-> ModelValue (BackingStoreState ks k vs d) a
-> Maybe (ModelValue (BackingStoreState ks k vs d) b1)
forall a b.
Op a b
-> ModelValue (BackingStoreState ks k vs d) a
-> Maybe (ModelValue (BackingStoreState ks k vs d) b)
forall {k} (op :: k -> k -> *) (f :: k -> *) (a :: k) (b :: k).
InterpretOp op f =>
op a b -> f a -> Maybe (f b)
intOp Op a b1
f

{-------------------------------------------------------------------------------
  Interpreter for implementation (@'RealMonad'@)
-------------------------------------------------------------------------------}

runIO ::
  forall ks k vs d a.
  LockstepAction (BackingStoreState ks k vs d) a ->
  LookUp ->
  RealMonad IO ks k vs d a
runIO :: forall ks k vs d a.
LockstepAction (BackingStoreState ks k vs d) a
-> LookUp -> RealMonad IO ks k vs d a
runIO LockstepAction (BackingStoreState ks k vs d) a
action LookUp
lookUp = (RealEnv IO ks k vs d -> IO a)
-> ReaderT (RealEnv IO ks k vs d) IO a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((RealEnv IO ks k vs d -> IO a)
 -> ReaderT (RealEnv IO ks k vs d) IO a)
-> (RealEnv IO ks k vs d -> IO a)
-> ReaderT (RealEnv IO ks k vs d) IO a
forall a b. (a -> b) -> a -> b
$ \RealEnv IO ks k vs d
renv ->
  RealEnv IO ks k vs d
-> LockstepAction (BackingStoreState ks k vs d) a -> IO a
aux RealEnv IO ks k vs d
renv LockstepAction (BackingStoreState ks k vs d) a
action
 where
  aux ::
    RealEnv IO ks k vs d ->
    LockstepAction (BackingStoreState ks k vs d) a ->
    IO a
  aux :: RealEnv IO ks k vs d
-> LockstepAction (BackingStoreState ks k vs d) a -> IO a
aux RealEnv IO ks k vs d
renv = \case
    BSInitFromValues WithOrigin SlotNo
sl InitHint vs
h (Values vs
vs) -> IO () -> IO (Either Err ())
forall (m :: * -> *) a. IOLike m => m a -> m (Either Err a)
catchErr (IO () -> IO (Either Err ())) -> IO () -> IO (Either Err ())
forall a b. (a -> b) -> a -> b
$ do
      bs <- BackingStoreInitializer IO ks k vs d
bsi (WithOrigin SlotNo -> InitHint vs -> vs -> InitFrom vs
forall values.
WithOrigin SlotNo -> InitHint values -> values -> InitFrom values
BS.InitFromValues WithOrigin SlotNo
sl InitHint vs
h vs
vs)
      void $ swapMVar bsVar bs
    BSInitFromCopy InitHint vs
h FsPath
bsp -> IO () -> IO (Either Err ())
forall (m :: * -> *) a. IOLike m => m a -> m (Either Err a)
catchErr (IO () -> IO (Either Err ())) -> IO () -> IO (Either Err ())
forall a b. (a -> b) -> a -> b
$ do
      bs <- BackingStoreInitializer IO ks k vs d
bsi (InitHint vs -> FsPath -> InitFrom vs
forall values. InitHint values -> FsPath -> InitFrom values
BS.InitFromCopy InitHint vs
h FsPath
bsp)
      void $ swapMVar bsVar bs
    LockstepAction (BackingStoreState ks k vs d) a
R:ActionLockstepa ks k vs d a
BSClose ->
      IO () -> IO (Either Err ())
forall (m :: * -> *) a. IOLike m => m a -> m (Either Err a)
catchErr (IO () -> IO (Either Err ())) -> IO () -> IO (Either Err ())
forall a b. (a -> b) -> a -> b
$
        StrictMVar IO (BackingStore IO ks k vs d)
-> IO (BackingStore IO ks k vs d)
forall (m :: * -> *) a. MonadMVar m => StrictMVar m a -> m a
readMVar StrictMVar IO (BackingStore IO ks k vs d)
bsVar IO (BackingStore IO ks k vs d)
-> (BackingStore IO ks k vs d -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= BackingStore IO ks k vs d -> IO ()
forall (m :: * -> *) keys key values diff.
BackingStore m keys key values diff -> m ()
BS.bsClose
    BSCopy SerializeTablesHint vs
s FsPath
bsp ->
      IO () -> IO (Either Err ())
forall (m :: * -> *) a. IOLike m => m a -> m (Either Err a)
catchErr (IO () -> IO (Either Err ())) -> IO () -> IO (Either Err ())
forall a b. (a -> b) -> a -> b
$
        StrictMVar IO (BackingStore IO ks k vs d)
-> IO (BackingStore IO ks k vs d)
forall (m :: * -> *) a. MonadMVar m => StrictMVar m a -> m a
readMVar StrictMVar IO (BackingStore IO ks k vs d)
bsVar IO (BackingStore IO ks k vs d)
-> (BackingStore IO ks k vs d -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \BackingStore IO ks k vs d
bs -> BackingStore IO ks k vs d
-> SerializeTablesHint vs -> FsPath -> IO ()
forall (m :: * -> *) keys key values diff.
BackingStore m keys key values diff
-> SerializeTablesHint values -> FsPath -> m ()
BS.bsCopy BackingStore IO ks k vs d
bs SerializeTablesHint vs
s FsPath
bsp
    LockstepAction (BackingStoreState ks k vs d) a
R:ActionLockstepa ks k vs d a
BSValueHandle ->
      IO (BackingStoreValueHandle IO ks k vs)
-> IO (Either Err (BackingStoreValueHandle IO ks k vs))
forall (m :: * -> *) a. IOLike m => m a -> m (Either Err a)
catchErr (IO (BackingStoreValueHandle IO ks k vs)
 -> IO (Either Err (BackingStoreValueHandle IO ks k vs)))
-> IO (BackingStoreValueHandle IO ks k vs)
-> IO (Either Err (BackingStoreValueHandle IO ks k vs))
forall a b. (a -> b) -> a -> b
$
        StrictMVar IO (BackingStore IO ks k vs d)
-> IO (BackingStore IO ks k vs d)
forall (m :: * -> *) a. MonadMVar m => StrictMVar m a -> m a
readMVar StrictMVar IO (BackingStore IO ks k vs d)
bsVar IO (BackingStore IO ks k vs d)
-> (BackingStore IO ks k vs d
    -> IO (BackingStoreValueHandle IO ks k vs))
-> IO (BackingStoreValueHandle IO ks k vs)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= BackingStore IO ks k vs d
-> IO (BackingStoreValueHandle IO ks k vs)
forall (m :: * -> *) keys key values diff.
BackingStore m keys key values diff
-> m (BackingStoreValueHandle m keys key values)
BS.bsValueHandle
    BSWrite SlotNo
sl WriteHint d
whint d
d ->
      IO () -> IO (Either Err ())
forall (m :: * -> *) a. IOLike m => m a -> m (Either Err a)
catchErr (IO () -> IO (Either Err ())) -> IO () -> IO (Either Err ())
forall a b. (a -> b) -> a -> b
$
        StrictMVar IO (BackingStore IO ks k vs d)
-> IO (BackingStore IO ks k vs d)
forall (m :: * -> *) a. MonadMVar m => StrictMVar m a -> m a
readMVar StrictMVar IO (BackingStore IO ks k vs d)
bsVar IO (BackingStore IO ks k vs d)
-> (BackingStore IO ks k vs d -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \BackingStore IO ks k vs d
bs -> BackingStore IO ks k vs d -> SlotNo -> WriteHint d -> d -> IO ()
forall (m :: * -> *) keys key values diff.
BackingStore m keys key values diff
-> SlotNo -> WriteHint diff -> diff -> m ()
BS.bsWrite BackingStore IO ks k vs d
bs SlotNo
sl WriteHint d
whint d
d
    BSVHClose BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
var ->
      IO () -> IO (Either Err ())
forall (m :: * -> *) a. IOLike m => m a -> m (Either Err a)
catchErr (IO () -> IO (Either Err ())) -> IO () -> IO (Either Err ())
forall a b. (a -> b) -> a -> b
$
        BackingStoreValueHandle IO ks k vs -> IO ()
forall (m :: * -> *) keys key values.
BackingStoreValueHandle m keys key values -> m ()
BS.bsvhClose (BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
-> BackingStoreValueHandle IO ks k vs
forall x. BSVar ks k vs d x -> x
lookUp' BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
var)
    BSVHRangeRead BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
var ReadHint vs
rhint RangeQuery ks
rq ->
      IO (Values vs, Maybe k) -> IO (Either Err (Values vs, Maybe k))
forall (m :: * -> *) a. IOLike m => m a -> m (Either Err a)
catchErr (IO (Values vs, Maybe k) -> IO (Either Err (Values vs, Maybe k)))
-> IO (Values vs, Maybe k) -> IO (Either Err (Values vs, Maybe k))
forall a b. (a -> b) -> a -> b
$
        (vs -> Values vs) -> (vs, Maybe k) -> (Values vs, Maybe k)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first vs -> Values vs
forall vs. vs -> Values vs
Values
          ((vs, Maybe k) -> (Values vs, Maybe k))
-> IO (vs, Maybe k) -> IO (Values vs, Maybe k)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BackingStoreValueHandle IO ks k vs
-> ReadHint vs -> RangeQuery ks -> IO (vs, Maybe k)
forall (m :: * -> *) keys key values.
BackingStoreValueHandle m keys key values
-> ReadHint values -> RangeQuery keys -> m (values, Maybe key)
BS.bsvhRangeRead (BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
-> BackingStoreValueHandle IO ks k vs
forall x. BSVar ks k vs d x -> x
lookUp' BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
var) ReadHint vs
rhint RangeQuery ks
rq
    BSVHRead BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
var ReadHint vs
rhint ks
ks ->
      IO (Values vs) -> IO (Either Err (Values vs))
forall (m :: * -> *) a. IOLike m => m a -> m (Either Err a)
catchErr (IO (Values vs) -> IO (Either Err (Values vs)))
-> IO (Values vs) -> IO (Either Err (Values vs))
forall a b. (a -> b) -> a -> b
$
        vs -> Values vs
forall vs. vs -> Values vs
Values
          (vs -> Values vs) -> IO vs -> IO (Values vs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BackingStoreValueHandle IO ks k vs -> ReadHint vs -> ks -> IO vs
forall (m :: * -> *) keys key values.
BackingStoreValueHandle m keys key values
-> ReadHint values -> keys -> m values
BS.bsvhRead (BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
-> BackingStoreValueHandle IO ks k vs
forall x. BSVar ks k vs d x -> x
lookUp' BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
var) ReadHint vs
rhint ks
ks
    BSVHAtSlot BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
var ->
      IO (WithOrigin SlotNo) -> IO (Either Err (WithOrigin SlotNo))
forall (m :: * -> *) a. IOLike m => m a -> m (Either Err a)
catchErr (IO (WithOrigin SlotNo) -> IO (Either Err (WithOrigin SlotNo)))
-> IO (WithOrigin SlotNo) -> IO (Either Err (WithOrigin SlotNo))
forall a b. (a -> b) -> a -> b
$
        WithOrigin SlotNo -> IO (WithOrigin SlotNo)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BackingStoreValueHandle IO ks k vs -> WithOrigin SlotNo
forall (m :: * -> *) keys key values.
BackingStoreValueHandle m keys key values -> WithOrigin SlotNo
BS.bsvhAtSlot (BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
-> BackingStoreValueHandle IO ks k vs
forall x. BSVar ks k vs d x -> x
lookUp' BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
var))
    BSVHStat BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
var ->
      IO Statistics -> IO (Either Err Statistics)
forall (m :: * -> *) a. IOLike m => m a -> m (Either Err a)
catchErr (IO Statistics -> IO (Either Err Statistics))
-> IO Statistics -> IO (Either Err Statistics)
forall a b. (a -> b) -> a -> b
$
        BackingStoreValueHandle IO ks k vs -> IO Statistics
forall (m :: * -> *) keys key values.
BackingStoreValueHandle m keys key values -> m Statistics
BS.bsvhStat (BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
-> BackingStoreValueHandle IO ks k vs
forall x. BSVar ks k vs d x -> x
lookUp' BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
var)
   where
    RealEnv
      { reBackingStoreInit :: forall (m :: * -> *) ks k vs d.
RealEnv m ks k vs d -> BackingStoreInitializer m ks k vs d
reBackingStoreInit = BackingStoreInitializer IO ks k vs d
bsi
      , reBackingStore :: forall (m :: * -> *) ks k vs d.
RealEnv m ks k vs d -> StrictMVar m (BackingStore m ks k vs d)
reBackingStore = StrictMVar IO (BackingStore IO ks k vs d)
bsVar
      } = RealEnv IO ks k vs d
renv

    lookUp' :: BSVar ks k vs d x -> x
    lookUp' :: forall x. BSVar ks k vs d x -> x
lookUp' = LookUp -> GVar Op x -> x
RealLookUp Op
forall (op :: * -> * -> *).
InterpretOp op Identity =>
RealLookUp op
realLookupVar Var a -> a
LookUp
lookUp

catchErr :: forall m a. IOLike m => m a -> m (Either Err a)
catchErr :: forall (m :: * -> *) a. IOLike m => m a -> m (Either Err a)
catchErr m a
act =
  m (Either Err a) -> [Handler m (Either Err a)] -> m (Either Err a)
forall (m :: * -> *) a. MonadCatch m => m a -> [Handler m a] -> m a
catches
    (a -> Either Err a
forall a b. b -> Either a b
Right (a -> Either Err a) -> m a -> m (Either Err a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
act)
    [(InMemoryBackingStoreExn -> Maybe Err) -> Handler m (Either Err a)
forall (m :: * -> *) e a.
(IOLike m, Exception e) =>
(e -> Maybe Err) -> Handler m (Either Err a)
mkHandler InMemoryBackingStoreExn -> Maybe Err
fromTVarExn, (InMemoryBackingStoreInitExn -> Maybe Err)
-> Handler m (Either Err a)
forall (m :: * -> *) e a.
(IOLike m, Exception e) =>
(e -> Maybe Err) -> Handler m (Either Err a)
mkHandler InMemoryBackingStoreInitExn -> Maybe Err
fromTVarExn', (LMDBErr -> Maybe Err) -> Handler m (Either Err a)
forall (m :: * -> *) e a.
(IOLike m, Exception e) =>
(e -> Maybe Err) -> Handler m (Either Err a)
mkHandler LMDBErr -> Maybe Err
fromDbErr]

{-------------------------------------------------------------------------------
  Statistics and tagging
-------------------------------------------------------------------------------}

data Stats ks k vs d = Stats
  { forall ks k vs d.
Stats ks k vs d -> Map (ValueHandle vs) (WithOrigin SlotNo)
handleSlots :: Map (ValueHandle vs) (WithOrigin SlotNo)
  -- ^ Slots that value handles were created in
  , forall ks k vs d. Stats ks k vs d -> Map SlotNo Int
writeSlots :: Map SlotNo Int
  -- ^ Slots in which writes were performed
  , forall ks k vs d. Stats ks k vs d -> Bool
readAfterWrite :: Bool
  -- ^ A value handle was created before a write, and read after the write
  , forall ks k vs d. Stats ks k vs d -> Bool
rangeReadAfterWrite :: Bool
  -- ^ A value handle was created before a write, and range read after the
  -- write
  }
  deriving stock (Int -> Stats ks k vs d -> ShowS
[Stats ks k vs d] -> ShowS
Stats ks k vs d -> String
(Int -> Stats ks k vs d -> ShowS)
-> (Stats ks k vs d -> String)
-> ([Stats ks k vs d] -> ShowS)
-> Show (Stats ks k vs d)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall ks k vs d. Show vs => Int -> Stats ks k vs d -> ShowS
forall ks k vs d. Show vs => [Stats ks k vs d] -> ShowS
forall ks k vs d. Show vs => Stats ks k vs d -> String
$cshowsPrec :: forall ks k vs d. Show vs => Int -> Stats ks k vs d -> ShowS
showsPrec :: Int -> Stats ks k vs d -> ShowS
$cshow :: forall ks k vs d. Show vs => Stats ks k vs d -> String
show :: Stats ks k vs d -> String
$cshowList :: forall ks k vs d. Show vs => [Stats ks k vs d] -> ShowS
showList :: [Stats ks k vs d] -> ShowS
Show, Stats ks k vs d -> Stats ks k vs d -> Bool
(Stats ks k vs d -> Stats ks k vs d -> Bool)
-> (Stats ks k vs d -> Stats ks k vs d -> Bool)
-> Eq (Stats ks k vs d)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall ks k vs d. Stats ks k vs d -> Stats ks k vs d -> Bool
$c== :: forall ks k vs d. Stats ks k vs d -> Stats ks k vs d -> Bool
== :: Stats ks k vs d -> Stats ks k vs d -> Bool
$c/= :: forall ks k vs d. Stats ks k vs d -> Stats ks k vs d -> Bool
/= :: Stats ks k vs d -> Stats ks k vs d -> Bool
Eq)

initStats :: Stats ks k vs d
initStats :: forall ks k vs d. Stats ks k vs d
initStats =
  Stats
    { handleSlots :: Map (ValueHandle vs) (WithOrigin SlotNo)
handleSlots = Map (ValueHandle vs) (WithOrigin SlotNo)
forall k a. Map k a
Map.empty
    , writeSlots :: Map SlotNo Int
writeSlots = Map SlotNo Int
forall k a. Map k a
Map.empty
    , readAfterWrite :: Bool
readAfterWrite = Bool
False
    , rangeReadAfterWrite :: Bool
rangeReadAfterWrite = Bool
False
    }

updateStats ::
  forall ks k vs d a.
  ( Mock.HasOps ks k vs d
  , QC.Arbitrary ks
  , QC.Arbitrary vs
  , QC.Arbitrary k
  , QC.Arbitrary d
  , QC.Arbitrary (BS.RangeQuery ks)
  ) =>
  LockstepAction (BackingStoreState ks k vs d) a ->
  ModelVarContext (BackingStoreState ks k vs d) ->
  BSVal ks k vs d a ->
  Stats ks k vs d ->
  Stats ks k vs d
updateStats :: forall ks k vs d a.
(HasOps ks k vs d, Arbitrary ks, Arbitrary vs, Arbitrary k,
 Arbitrary d, Arbitrary (RangeQuery ks)) =>
LockstepAction (BackingStoreState ks k vs d) a
-> ModelVarContext (BackingStoreState ks k vs d)
-> BSVal ks k vs d a
-> Stats ks k vs d
-> Stats ks k vs d
updateStats LockstepAction (BackingStoreState ks k vs d) a
action ModelVarContext (BackingStoreState ks k vs d)
lookUp BSVal ks k vs d a
result stats :: Stats ks k vs d
stats@Stats{Map (ValueHandle vs) (WithOrigin SlotNo)
handleSlots :: forall ks k vs d.
Stats ks k vs d -> Map (ValueHandle vs) (WithOrigin SlotNo)
handleSlots :: Map (ValueHandle vs) (WithOrigin SlotNo)
handleSlots, Map SlotNo Int
writeSlots :: forall ks k vs d. Stats ks k vs d -> Map SlotNo Int
writeSlots :: Map SlotNo Int
writeSlots} =
  Stats ks k vs d -> Stats ks k vs d
updateHandleSlots
    (Stats ks k vs d -> Stats ks k vs d)
-> (Stats ks k vs d -> Stats ks k vs d)
-> Stats ks k vs d
-> Stats ks k vs d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stats ks k vs d -> Stats ks k vs d
updateWriteSlots
    (Stats ks k vs d -> Stats ks k vs d)
-> (Stats ks k vs d -> Stats ks k vs d)
-> Stats ks k vs d
-> Stats ks k vs d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stats ks k vs d -> Stats ks k vs d
updateReadAfterWrite
    (Stats ks k vs d -> Stats ks k vs d)
-> (Stats ks k vs d -> Stats ks k vs d)
-> Stats ks k vs d
-> Stats ks k vs d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stats ks k vs d -> Stats ks k vs d
updateRangeReadAfterWrite
    (Stats ks k vs d -> Stats ks k vs d)
-> Stats ks k vs d -> Stats ks k vs d
forall a b. (a -> b) -> a -> b
$ Stats ks k vs d
stats
 where
  getHandle :: BSVal ks k vs d (BS.BackingStoreValueHandle IO ks k vs) -> ValueHandle vs
  getHandle :: BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ValueHandle vs
getHandle (MValueHandle ValueHandle vs
h) = ValueHandle vs
h

  updateHandleSlots :: Stats ks k vs d -> Stats ks k vs d
  updateHandleSlots :: Stats ks k vs d -> Stats ks k vs d
updateHandleSlots Stats ks k vs d
s = case (LockstepAction (BackingStoreState ks k vs d) a
action, BSVal ks k vs d a
result) of
    (LockstepAction (BackingStoreState ks k vs d) a
R:ActionLockstepa ks k vs d a
BSValueHandle, MEither (Right (MValueHandle ValueHandle vs
h))) ->
      Stats ks k vs d
s{handleSlots = Map.insert h (seqNo h) handleSlots}
    (LockstepAction (BackingStoreState ks k vs d) a
R:ActionLockstepa ks k vs d a
BSClose, MEither (Right BSVal ks k vs d b
_)) ->
      Stats ks k vs d
s{handleSlots = Map.empty}
    (BSVHClose BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h, MEither (Right BSVal ks k vs d b
_)) ->
      Stats ks k vs d
s{handleSlots = Map.delete (getHandle $ lookupVar lookUp h) handleSlots}
    (LockstepAction (BackingStoreState ks k vs d) a, BSVal ks k vs d a)
_ -> Stats ks k vs d
s

  updateWriteSlots :: Stats ks k vs d -> Stats ks k vs d
  updateWriteSlots :: Stats ks k vs d -> Stats ks k vs d
updateWriteSlots Stats ks k vs d
s = case (LockstepAction (BackingStoreState ks k vs d) a
action, BSVal ks k vs d a
result) of
    (BSWrite SlotNo
sl WriteHint d
_ d
d, MEither (Right (MUnit ())))
      | Int
1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= d -> Int
forall d. DiffSize d => d -> Int
Mock.diffSize d
d ->
          Stats ks k vs d
s{writeSlots = Map.insert sl (Mock.diffSize d) writeSlots}
    (LockstepAction (BackingStoreState ks k vs d) a
R:ActionLockstepa ks k vs d a
BSClose, MEither (Right BSVal ks k vs d b
_)) ->
      Stats ks k vs d
s{writeSlots = Map.empty}
    (LockstepAction (BackingStoreState ks k vs d) a, BSVal ks k vs d a)
_ -> Stats ks k vs d
s

  updateReadAfterWrite :: Stats ks k vs d -> Stats ks k vs d
  updateReadAfterWrite :: Stats ks k vs d -> Stats ks k vs d
updateReadAfterWrite Stats ks k vs d
s = case (LockstepAction (BackingStoreState ks k vs d) a
action, BSVal ks k vs d a
result) of
    (BSVHRead BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h ReadHint vs
_ ks
_, MEither (Right (MValues vs
vs)))
      | ValueHandle vs
h' <- BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ValueHandle vs
getHandle (BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
 -> ValueHandle vs)
-> BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ValueHandle vs
forall a b. (a -> b) -> a -> b
$ ModelVarContext (BackingStoreState ks k vs d)
-> ModelLookUp (BackingStoreState ks k vs d)
forall state.
InLockstep state =>
ModelVarContext state -> ModelLookUp state
lookupVar ModelVarContext (BackingStoreState ks k vs d)
lookUp BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h
      , Just WithOrigin SlotNo
wosl <- ValueHandle vs
-> Map (ValueHandle vs) (WithOrigin SlotNo)
-> Maybe (WithOrigin SlotNo)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ValueHandle vs
h' Map (ValueHandle vs) (WithOrigin SlotNo)
handleSlots
      , Just (SlotNo
sl, Int
_) <- Map SlotNo Int -> Maybe (SlotNo, Int)
forall k a. Map k a -> Maybe (k, a)
Map.lookupMax Map SlotNo Int
writeSlots
      , WithOrigin SlotNo
wosl WithOrigin SlotNo -> WithOrigin SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< SlotNo -> WithOrigin SlotNo
forall t. t -> WithOrigin t
at SlotNo
sl
      , Int
1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= vs -> Int
forall vs. ValuesLength vs => vs -> Int
Mock.valuesLength vs
vs ->
          Stats ks k vs d
s{readAfterWrite = True}
    (LockstepAction (BackingStoreState ks k vs d) a, BSVal ks k vs d a)
_ -> Stats ks k vs d
s

  updateRangeReadAfterWrite :: Stats ks k vs d -> Stats ks k vs d
  updateRangeReadAfterWrite :: Stats ks k vs d -> Stats ks k vs d
updateRangeReadAfterWrite Stats ks k vs d
s = case (LockstepAction (BackingStoreState ks k vs d) a
action, BSVal ks k vs d a
result) of
    (BSVHRangeRead BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h ReadHint vs
_ RangeQuery ks
_, MEither (Right (MValuesAndLast (vs
vs, Maybe k
_))))
      | ValueHandle vs
h' <- BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ValueHandle vs
getHandle (BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
 -> ValueHandle vs)
-> BSVal ks k vs d (BackingStoreValueHandle IO ks k vs)
-> ValueHandle vs
forall a b. (a -> b) -> a -> b
$ ModelVarContext (BackingStoreState ks k vs d)
-> ModelLookUp (BackingStoreState ks k vs d)
forall state.
InLockstep state =>
ModelVarContext state -> ModelLookUp state
lookupVar ModelVarContext (BackingStoreState ks k vs d)
lookUp BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
h
      , Just WithOrigin SlotNo
wosl <- ValueHandle vs
-> Map (ValueHandle vs) (WithOrigin SlotNo)
-> Maybe (WithOrigin SlotNo)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ValueHandle vs
h' Map (ValueHandle vs) (WithOrigin SlotNo)
handleSlots
      , Just (SlotNo
sl, Int
_) <- Map SlotNo Int -> Maybe (SlotNo, Int)
forall k a. Map k a -> Maybe (k, a)
Map.lookupMax Map SlotNo Int
writeSlots
      , WithOrigin SlotNo
wosl WithOrigin SlotNo -> WithOrigin SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< SlotNo -> WithOrigin SlotNo
forall t. t -> WithOrigin t
at SlotNo
sl
      , Int
1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= vs -> Int
forall vs. ValuesLength vs => vs -> Int
Mock.valuesLength vs
vs ->
          Stats ks k vs d
s{rangeReadAfterWrite = True}
    (LockstepAction (BackingStoreState ks k vs d) a, BSVal ks k vs d a)
_ -> Stats ks k vs d
s

data TagAction
  = TBSInitFromValues
  | TBSInitFromCopy
  | TBSClose
  | TBSCopy
  | TBSValueHandle
  | TBSWrite
  | TBSVHClose
  | TBSVHRangeRead
  | TBSVHRead
  | TBSVHAtSlot
  | TBSVHStat
  deriving (Int -> TagAction -> ShowS
[TagAction] -> ShowS
TagAction -> String
(Int -> TagAction -> ShowS)
-> (TagAction -> String)
-> ([TagAction] -> ShowS)
-> Show TagAction
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TagAction -> ShowS
showsPrec :: Int -> TagAction -> ShowS
$cshow :: TagAction -> String
show :: TagAction -> String
$cshowList :: [TagAction] -> ShowS
showList :: [TagAction] -> ShowS
Show, TagAction -> TagAction -> Bool
(TagAction -> TagAction -> Bool)
-> (TagAction -> TagAction -> Bool) -> Eq TagAction
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TagAction -> TagAction -> Bool
== :: TagAction -> TagAction -> Bool
$c/= :: TagAction -> TagAction -> Bool
/= :: TagAction -> TagAction -> Bool
Eq, Eq TagAction
Eq TagAction =>
(TagAction -> TagAction -> Ordering)
-> (TagAction -> TagAction -> Bool)
-> (TagAction -> TagAction -> Bool)
-> (TagAction -> TagAction -> Bool)
-> (TagAction -> TagAction -> Bool)
-> (TagAction -> TagAction -> TagAction)
-> (TagAction -> TagAction -> TagAction)
-> Ord TagAction
TagAction -> TagAction -> Bool
TagAction -> TagAction -> Ordering
TagAction -> TagAction -> TagAction
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: TagAction -> TagAction -> Ordering
compare :: TagAction -> TagAction -> Ordering
$c< :: TagAction -> TagAction -> Bool
< :: TagAction -> TagAction -> Bool
$c<= :: TagAction -> TagAction -> Bool
<= :: TagAction -> TagAction -> Bool
$c> :: TagAction -> TagAction -> Bool
> :: TagAction -> TagAction -> Bool
$c>= :: TagAction -> TagAction -> Bool
>= :: TagAction -> TagAction -> Bool
$cmax :: TagAction -> TagAction -> TagAction
max :: TagAction -> TagAction -> TagAction
$cmin :: TagAction -> TagAction -> TagAction
min :: TagAction -> TagAction -> TagAction
Ord, TagAction
TagAction -> TagAction -> Bounded TagAction
forall a. a -> a -> Bounded a
$cminBound :: TagAction
minBound :: TagAction
$cmaxBound :: TagAction
maxBound :: TagAction
Bounded, Int -> TagAction
TagAction -> Int
TagAction -> [TagAction]
TagAction -> TagAction
TagAction -> TagAction -> [TagAction]
TagAction -> TagAction -> TagAction -> [TagAction]
(TagAction -> TagAction)
-> (TagAction -> TagAction)
-> (Int -> TagAction)
-> (TagAction -> Int)
-> (TagAction -> [TagAction])
-> (TagAction -> TagAction -> [TagAction])
-> (TagAction -> TagAction -> [TagAction])
-> (TagAction -> TagAction -> TagAction -> [TagAction])
-> Enum TagAction
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 :: TagAction -> TagAction
succ :: TagAction -> TagAction
$cpred :: TagAction -> TagAction
pred :: TagAction -> TagAction
$ctoEnum :: Int -> TagAction
toEnum :: Int -> TagAction
$cfromEnum :: TagAction -> Int
fromEnum :: TagAction -> Int
$cenumFrom :: TagAction -> [TagAction]
enumFrom :: TagAction -> [TagAction]
$cenumFromThen :: TagAction -> TagAction -> [TagAction]
enumFromThen :: TagAction -> TagAction -> [TagAction]
$cenumFromTo :: TagAction -> TagAction -> [TagAction]
enumFromTo :: TagAction -> TagAction -> [TagAction]
$cenumFromThenTo :: TagAction -> TagAction -> TagAction -> [TagAction]
enumFromThenTo :: TagAction -> TagAction -> TagAction -> [TagAction]
Enum)

-- | Identify actions by their constructor.
tAction :: LockstepAction (BackingStoreState ks k vs d) a -> TagAction
tAction :: forall ks k vs d a.
LockstepAction (BackingStoreState ks k vs d) a -> TagAction
tAction = \case
  BSInitFromValues WithOrigin SlotNo
_ InitHint vs
_ Values vs
_ -> TagAction
TBSInitFromValues
  BSInitFromCopy InitHint vs
_ FsPath
_ -> TagAction
TBSInitFromCopy
  LockstepAction (BackingStoreState ks k vs d) a
R:ActionLockstepa ks k vs d a
BSClose -> TagAction
TBSClose
  BSCopy SerializeTablesHint vs
_ FsPath
_ -> TagAction
TBSCopy
  LockstepAction (BackingStoreState ks k vs d) a
R:ActionLockstepa ks k vs d a
BSValueHandle -> TagAction
TBSValueHandle
  BSWrite SlotNo
_ WriteHint d
_ d
_ -> TagAction
TBSWrite
  BSVHClose BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
_ -> TagAction
TBSVHClose
  BSVHRangeRead BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
_ ReadHint vs
_ RangeQuery ks
_ -> TagAction
TBSVHRangeRead
  BSVHRead BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
_ ReadHint vs
_ ks
_ -> TagAction
TBSVHRead
  BSVHAtSlot BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
_ -> TagAction
TBSVHAtSlot
  BSVHStat BSVar ks k vs d (BackingStoreValueHandle IO ks k vs)
_ -> TagAction
TBSVHStat

data Tag
  = -- | A value handle is created before a write, and read after the write. The
    -- write should not affect the result of the read.
    ReadAfterWrite
  | -- | A value handle is created before a write, and read after the write. The
    -- write should not affect the result of the read.
    RangeReadAfterWrite
  | ErrorBecauseBackingStoreIsClosed TagAction
  | ErrorBecauseBackingStoreValueHandleIsClosed TagAction
  deriving Int -> Tag -> ShowS
[Tag] -> ShowS
Tag -> String
(Int -> Tag -> ShowS)
-> (Tag -> String) -> ([Tag] -> ShowS) -> Show Tag
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Tag -> ShowS
showsPrec :: Int -> Tag -> ShowS
$cshow :: Tag -> String
show :: Tag -> String
$cshowList :: [Tag] -> ShowS
showList :: [Tag] -> ShowS
Show

tagBSAction ::
  Stats ks k vs d ->
  Stats ks k vs d ->
  LockstepAction (BackingStoreState ks k vs d) a ->
  BSVal ks k vs d a ->
  [Tag]
tagBSAction :: forall ks k vs d a.
Stats ks k vs d
-> Stats ks k vs d
-> LockstepAction (BackingStoreState ks k vs d) a
-> BSVal ks k vs d a
-> [Tag]
tagBSAction Stats ks k vs d
before Stats ks k vs d
after LockstepAction (BackingStoreState ks k vs d) a
action BSVal ks k vs d a
result =
  [Tag]
globalTags [Tag] -> [Tag] -> [Tag]
forall a. [a] -> [a] -> [a]
++ case (LockstepAction (BackingStoreState ks k vs d) a
action, BSVal ks k vs d a
result) of
    (LockstepAction (BackingStoreState ks k vs d) a
_, MEither (Left (MErr Err
ErrBackingStoreClosed))) ->
      [TagAction -> Tag
ErrorBecauseBackingStoreIsClosed (LockstepAction (BackingStoreState ks k vs d) a -> TagAction
forall ks k vs d a.
LockstepAction (BackingStoreState ks k vs d) a -> TagAction
tAction LockstepAction (BackingStoreState ks k vs d) a
action)]
    (LockstepAction (BackingStoreState ks k vs d) a
_, MEither (Left (MErr Err
ErrBackingStoreValueHandleClosed))) ->
      [TagAction -> Tag
ErrorBecauseBackingStoreValueHandleIsClosed (LockstepAction (BackingStoreState ks k vs d) a -> TagAction
forall ks k vs d a.
LockstepAction (BackingStoreState ks k vs d) a -> TagAction
tAction LockstepAction (BackingStoreState ks k vs d) a
action)]
    (LockstepAction (BackingStoreState ks k vs d) a, BSVal ks k vs d a)
_ -> []
 where
  globalTags :: [Tag]
globalTags =
    [[Tag]] -> [Tag]
forall a. Monoid a => [a] -> a
mconcat
      [ [ Tag
ReadAfterWrite
        | Bool -> Bool
not (Stats ks k vs d -> Bool
forall ks k vs d. Stats ks k vs d -> Bool
readAfterWrite Stats ks k vs d
before)
        , Stats ks k vs d -> Bool
forall ks k vs d. Stats ks k vs d -> Bool
readAfterWrite Stats ks k vs d
after
        ]
      , [ Tag
RangeReadAfterWrite
        | Bool -> Bool
not (Stats ks k vs d -> Bool
forall ks k vs d. Stats ks k vs d -> Bool
rangeReadAfterWrite Stats ks k vs d
before)
        , Stats ks k vs d -> Bool
forall ks k vs d. Stats ks k vs d -> Bool
rangeReadAfterWrite Stats ks k vs d
after
        ]
      ]

{-------------------------------------------------------------------------------
  Errors
-------------------------------------------------------------------------------}

mkHandler ::
  (IOLike m, Exception e) =>
  (e -> Maybe Err) ->
  Handler m (Either Err a)
mkHandler :: forall (m :: * -> *) e a.
(IOLike m, Exception e) =>
(e -> Maybe Err) -> Handler m (Either Err a)
mkHandler e -> Maybe Err
fhandler = (e -> m (Either Err a)) -> Handler m (Either Err a)
forall {k} (m :: k -> *) (a :: k) e.
Exception e =>
(e -> m a) -> Handler m a
Handler ((e -> m (Either Err a)) -> Handler m (Either Err a))
-> (e -> m (Either Err a)) -> Handler m (Either Err a)
forall a b. (a -> b) -> a -> b
$
  \e
e -> m (Either Err a)
-> (Err -> m (Either Err a)) -> Maybe Err -> m (Either Err a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (e -> m (Either Err a)
forall e a. Exception e => e -> m a
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwIO e
e) (Either Err a -> m (Either Err a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Err a -> m (Either Err a))
-> (Err -> Either Err a) -> Err -> m (Either Err a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Err -> Either Err a
forall a b. a -> Either a b
Left) (e -> Maybe Err
fhandler e
e)

-- | Map LMDB errors to mock errors.
fromDbErr :: LMDB.LMDBErr -> Maybe Err
fromDbErr :: LMDBErr -> Maybe Err
fromDbErr = \case
  LMDBErr
LMDBErrNoDbSeqNo -> Maybe Err
forall a. Maybe a
Nothing
  LMDBErrNonMonotonicSeq WithOrigin SlotNo
wo WithOrigin SlotNo
wo' -> Err -> Maybe Err
forall a. a -> Maybe a
Just (Err -> Maybe Err) -> Err -> Maybe Err
forall a b. (a -> b) -> a -> b
$ WithOrigin SlotNo -> WithOrigin SlotNo -> Err
ErrNonMonotonicSeqNo WithOrigin SlotNo
wo WithOrigin SlotNo
wo'
  LMDBErrInitialisingNonEmpty String
_ -> Maybe Err
forall a. Maybe a
Nothing
  LMDBErrNoValueHandle Int
_ -> Err -> Maybe Err
forall a. a -> Maybe a
Just Err
ErrBackingStoreValueHandleClosed
  LMDBErr
LMDBErrBadRead -> Maybe Err
forall a. Maybe a
Nothing
  LMDBErr
LMDBErrBadRangeRead -> Maybe Err
forall a. Maybe a
Nothing
  LMDBErrDirExists String
_ -> Err -> Maybe Err
forall a. a -> Maybe a
Just Err
ErrCopyPathAlreadyExists
  LMDBErrDirDoesntExist String
_ -> Err -> Maybe Err
forall a. a -> Maybe a
Just Err
ErrCopyPathDoesNotExist
  LMDBErrDirIsNotLMDB String
_ -> Maybe Err
forall a. Maybe a
Nothing
  LMDBErr
LMDBErrClosed -> Err -> Maybe Err
forall a. a -> Maybe a
Just Err
ErrBackingStoreClosed
  LMDBErr
LMDBErrInitialisingAlreadyHasState -> Maybe Err
forall a. Maybe a
Nothing
  LMDBErr
LMDBErrUnableToReadSeqNo -> Maybe Err
forall a. Maybe a
Nothing
  LMDBErrNotADir FsPath
_ -> Maybe Err
forall a. Maybe a
Nothing

-- | Map InMemory (i.e., @TVarBackingStore@) errors to mock errors.
fromTVarExn :: BS.InMemoryBackingStoreExn -> Maybe Err
fromTVarExn :: InMemoryBackingStoreExn -> Maybe Err
fromTVarExn = \case
  InMemoryBackingStoreExn
BS.InMemoryBackingStoreClosedExn -> Err -> Maybe Err
forall a. a -> Maybe a
Just Err
ErrBackingStoreClosed
  InMemoryBackingStoreExn
BS.InMemoryBackingStoreValueHandleClosedExn -> Err -> Maybe Err
forall a. a -> Maybe a
Just Err
ErrBackingStoreValueHandleClosed
  InMemoryBackingStoreExn
BS.InMemoryBackingStoreDirectoryExists -> Err -> Maybe Err
forall a. a -> Maybe a
Just Err
ErrCopyPathAlreadyExists
  BS.InMemoryBackingStoreNonMonotonicSeq WithOrigin SlotNo
wo WithOrigin SlotNo
wo' -> Err -> Maybe Err
forall a. a -> Maybe a
Just (Err -> Maybe Err) -> Err -> Maybe Err
forall a b. (a -> b) -> a -> b
$ WithOrigin SlotNo -> WithOrigin SlotNo -> Err
ErrNonMonotonicSeqNo WithOrigin SlotNo
wo WithOrigin SlotNo
wo'
  BS.InMemoryBackingStoreDeserialiseExn DeserialiseFailure
_ -> Maybe Err
forall a. Maybe a
Nothing
  InMemoryBackingStoreExn
BS.InMemoryIncompleteDeserialiseExn -> Maybe Err
forall a. Maybe a
Nothing

fromTVarExn' :: BS.InMemoryBackingStoreInitExn -> Maybe Err
fromTVarExn' :: InMemoryBackingStoreInitExn -> Maybe Err
fromTVarExn' = \case
  BS.StoreDirIsIncompatible FsErrorPath
_ -> Err -> Maybe Err
forall a. a -> Maybe a
Just Err
ErrCopyPathDoesNotExist