From 147a77524f5649599b93f8b7a40239dfc591b3f2 Mon Sep 17 00:00:00 2001
From: Joris Dral <joris@well-typed.com>
Date: Wed, 12 Mar 2025 13:06:43 +0100
Subject: [PATCH 1/2] Update to `quickcheck-lockstep-0.8`

The most invasive change is that the `Realized` type family disappeared, but as
a result we also have to run the `IOSim` test with the `RealWorld` state token.
The `quickcheck-dynamic` library requires the return types of actions to be
`Typeable`, and if the state token appears in the return type of an action
(which it does in our tests), then the state token has to be typeable, which is
only really possible if we use `RealWorld`.
---
 cabal.project.release                         |   4 +-
 lsm-tree.cabal                                |   5 +-
 test-prototypes/Test/ScheduledMergesQLS.hs    |   4 +-
 .../Test/Database/LSMTree/Internal/Readers.hs |   2 +-
 test/Test/Database/LSMTree/StateMachine.hs    | 439 +++++++++---------
 test/Test/Database/LSMTree/StateMachine/DL.hs |   7 +-
 test/Test/Database/LSMTree/StateMachine/Op.hs |  41 +-
 test/Test/Util/Orphans.hs                     |  60 +--
 test/Test/Util/QLS.hs                         |   2 +-
 9 files changed, 245 insertions(+), 319 deletions(-)

diff --git a/cabal.project.release b/cabal.project.release
index 09b4579c9..75f03d34f 100644
--- a/cabal.project.release
+++ b/cabal.project.release
@@ -1,7 +1,7 @@
 index-state:
   -- Bump this if you need newer packages from Hackage
-  -- current date: fs-api-0.4.0.0 and fs-sim-0.4.0.0
-  , hackage.haskell.org 2025-07-01T00:00:00Z
+  -- current date: quickcheck-lockstep-0.8.0
+  , hackage.haskell.org 2025-07-03T13:54:16Z
 
 packages:
   .
diff --git a/lsm-tree.cabal b/lsm-tree.cabal
index 16976fc28..f0acf0411 100644
--- a/lsm-tree.cabal
+++ b/lsm-tree.cabal
@@ -893,12 +893,11 @@ test-suite lsm-tree-test
     , quickcheck-classes
     , quickcheck-dynamic
     , quickcheck-instances
-    , quickcheck-lockstep
+    , quickcheck-lockstep     >=0.8
     , random
     , safe-wild-cards
     , semialign
     , split
-    , stm
     , tasty
     , tasty-golden
     , tasty-hunit
@@ -1208,7 +1207,7 @@ test-suite prototypes-test
     , primitive
     , QuickCheck
     , quickcheck-dynamic
-    , quickcheck-lockstep
+    , quickcheck-lockstep  >=0.8
     , tasty
     , tasty-hunit
     , tasty-quickcheck
diff --git a/test-prototypes/Test/ScheduledMergesQLS.hs b/test-prototypes/Test/ScheduledMergesQLS.hs
index c3d94aab6..dd38c9bcc 100644
--- a/test-prototypes/Test/ScheduledMergesQLS.hs
+++ b/test-prototypes/Test/ScheduledMergesQLS.hs
@@ -383,7 +383,7 @@ deriving stock instance Eq (ModelValue Model a)
 
 
 runActionIO :: Action (Lockstep Model) a
-            -> LookUp IO
+            -> LookUp
             -> ReaderT (PrimVar RealWorld TableId) IO a
 runActionIO action lookUp = ReaderT $ \tidVar -> do
   case action of
@@ -408,7 +408,7 @@ runActionIO action lookUp = ReaderT $ \tidVar -> do
     ADump      var      -> stToIO $ logicalValue (lookUpVar var)
   where
     lookUpVar :: ModelVar Model a -> a
-    lookUpVar = realLookupVar (Proxy :: Proxy IO) lookUp
+    lookUpVar = realLookupVar lookUp
 
     tr :: Tracer (ST RealWorld) Event
     tr = nullTracer
diff --git a/test/Test/Database/LSMTree/Internal/Readers.hs b/test/Test/Database/LSMTree/Internal/Readers.hs
index cc8b8b247..d65d8d916 100644
--- a/test/Test/Database/LSMTree/Internal/Readers.hs
+++ b/test/Test/Database/LSMTree/Internal/Readers.hs
@@ -416,7 +416,7 @@ instance RunLockstep ReadersState RealMonad where
       Pop {}          -> OEither . bimap OId (OTuple3 . trimap OId OId OId)
       DropWhileKey {} -> OEither . bimap OId (OTuple2 . bimap OId OId)
 
-runIO :: LockstepAction ReadersState a -> LookUp RealMonad -> RealMonad (Realized RealMonad a)
+runIO :: LockstepAction ReadersState a -> LookUp -> RealMonad a
 runIO act lu = case act of
     New offset srcDatas -> ReaderT $ \(hfs, hbio) -> do
       RealState numRuns mCtx <- get
diff --git a/test/Test/Database/LSMTree/StateMachine.hs b/test/Test/Database/LSMTree/StateMachine.hs
index 0024524e5..6d6d5a330 100644
--- a/test/Test/Database/LSMTree/StateMachine.hs
+++ b/test/Test/Database/LSMTree/StateMachine.hs
@@ -60,6 +60,7 @@ import           Control.Monad.Class.MonadThrow (Exception (..), Handler (..),
 import           Control.Monad.IOSim
 import           Control.Monad.Primitive
 import           Control.Monad.Reader (ReaderT (..))
+import qualified Control.Monad.ST.Lazy as ST
 import           Control.RefCount (RefException, checkForgottenRefs,
                      ignoreForgottenRefs)
 import           Control.Tracer (Tracer, nullTracer)
@@ -157,7 +158,7 @@ tests = testGroup "Test.Database.LSMTree.StateMachine" [
     ]
 
 labelledExamples :: IO ()
-labelledExamples = QC.labelledExamples $ Lockstep.Run.tagActions (Proxy @(ModelState R.Table))
+labelledExamples = QC.labelledExamples $ Lockstep.Run.tagActions (Proxy @(ModelState IO R.Table))
 
 {-------------------------------------------------------------------------------
   propLockstep: reference implementation
@@ -171,11 +172,11 @@ deriving via AllowThunk (ModelIO.Session IO)
     instance NoThunks (ModelIO.Session IO)
 
 propLockstep_ModelIOImpl ::
-     Actions (Lockstep (ModelState ModelIO.Table))
+     Actions (Lockstep (ModelState IO ModelIO.Table))
   -> QC.Property
 propLockstep_ModelIOImpl =
     runActionsBracket
-      (Proxy @(ModelState ModelIO.Table))
+      (Proxy @(ModelState IO ModelIO.Table))
       CheckCleanup
       NoCheckRefs -- there are no references to check for in the ModelIO implementation
       acquire
@@ -290,11 +291,11 @@ instance Arbitrary R.FencePointerIndexType where
 propLockstep_RealImpl_RealFS_IO ::
      Tracer IO R.LSMTreeTrace
   -> QC.Fixed R.Salt
-  -> Actions (Lockstep (ModelState R.Table))
+  -> Actions (Lockstep (ModelState IO R.Table))
   -> QC.Property
 propLockstep_RealImpl_RealFS_IO tr (QC.Fixed salt) =
     runActionsBracket
-      (Proxy @(ModelState R.Table))
+      (Proxy @(ModelState IO R.Table))
       CheckCleanup
       CheckRefs
       acquire
@@ -338,11 +339,11 @@ propLockstep_RealImpl_MockFS_IO ::
   -> CheckFS
   -> CheckRefs
   -> QC.Fixed R.Salt
-  -> Actions (Lockstep (ModelState R.Table))
+  -> Actions (Lockstep (ModelState IO R.Table))
   -> QC.Property
 propLockstep_RealImpl_MockFS_IO tr cleanupFlag fsFlag refsFlag (QC.Fixed salt) =
     runActionsBracket
-      (Proxy @(ModelState R.Table))
+      (Proxy @(ModelState IO R.Table))
       cleanupFlag
       refsFlag
       (acquire_RealImpl_MockFS tr salt)
@@ -378,13 +379,17 @@ propLockstep_RealImpl_MockFS_IOSim ::
   -> CheckFS
   -> CheckRefs
   -> QC.Fixed R.Salt
-  -> Actions (Lockstep (ModelState R.Table))
   -> QC.Property
-propLockstep_RealImpl_MockFS_IOSim tr cleanupFlag fsFlag refsFlag (QC.Fixed salt) actions =
-    monadicIOSim_ prop
+propLockstep_RealImpl_MockFS_IOSim tr cleanupFlag fsFlag refsFlag (QC.Fixed salt) =
+    flip QC.monadic prop $ \x -> QC.ioProperty $ do
+        trac <- ST.stToIO $ runSimTraceST x
+        case traceResult False trac of
+          Left e  -> pure $ QC.counterexample (show e) False
+          Right p -> pure p
   where
-    prop :: forall s. PropertyM (IOSim s) Property
+    prop :: forall s. Typeable s => PropertyM (IOSim s) Property
     prop = do
+        actions <- QC.pick QC.arbitrary
         (fsVar, session, errsVar, logVar) <- QC.run (acquire_RealImpl_MockFS tr salt)
         faultsVar <- QC.run $ newMutVar []
         let
@@ -397,7 +402,7 @@ propLockstep_RealImpl_MockFS_IOSim tr cleanupFlag fsFlag refsFlag (QC.Fixed salt
             , envInjectFaultResults = faultsVar
             }
         void $ QD.runPropertyReaderT
-                (QD.runActions @(Lockstep (ModelState R.Table)) actions)
+                (QD.runActions @(Lockstep (ModelState (IOSim s) R.Table)) actions)
                 env
         faults <- QC.run $ readMutVar faultsVar
         p <- QC.run $ propCleanup cleanupFlag $
@@ -596,22 +601,22 @@ instance R.ResolveValue Value where
   Model state
 -------------------------------------------------------------------------------}
 
-type ModelState :: ((Type -> Type) -> Type -> Type -> Type -> Type) -> Type
-data ModelState h = ModelState Model.Model Stats
+type ModelState :: (Type -> Type) -> ((Type -> Type) -> Type -> Type -> Type -> Type) -> Type
+data ModelState m h = ModelState Model.Model Stats
   deriving stock Show
 
-initModelState :: ModelState h
+initModelState :: ModelState m h
 initModelState = ModelState Model.initModel initStats
 
 {-------------------------------------------------------------------------------
   Type synonyms
 -------------------------------------------------------------------------------}
 
-type Act h a = Action (Lockstep (ModelState h)) a
-type Act' h a = Action' h (Either Model.Err a)
-type Var h a = ModelVar (ModelState h) a
-type Val h a = ModelValue (ModelState h) a
-type Obs h a = Observable (ModelState h) a
+type Act m h a = Action (Lockstep (ModelState m h)) a
+type Act' m h a = Action' m h (Either Model.Err a)
+type Var m h a = ModelVar (ModelState m h) a
+type Val m h a = ModelValue (ModelState m h) a
+type Obs m h a = Observable (ModelState m h) a
 
 type K a = (
     Class.C_ a
@@ -647,9 +652,10 @@ instance ( Show (Class.TableConfig h)
          , Eq (Class.TableConfig h)
          , Arbitrary (Class.TableConfig h)
          , Typeable h
-         ) => StateModel (Lockstep (ModelState h)) where
-  data instance Action (Lockstep (ModelState h)) a where
-    Action :: Maybe Errors -> Action' h a -> Act h a
+         , Typeable m
+         ) => StateModel (Lockstep (ModelState m h)) where
+  data instance Action (Lockstep (ModelState m h)) a where
+    Action :: Maybe Errors -> Action' m h a -> Act m h a
 
   initialState    = Lockstep.Defaults.initialState initModelState
   nextState       = Lockstep.Defaults.nextState
@@ -662,115 +668,116 @@ instance ( Show (Class.TableConfig h)
   actionName (Action _ action') = head . words . show $ action'
 
 deriving stock instance Show (Class.TableConfig h)
-                     => Show (LockstepAction (ModelState h) a)
+                     => Show (LockstepAction (ModelState m h) a)
 
 instance ( Eq (Class.TableConfig h)
          , Typeable h
-         ) => Eq (LockstepAction (ModelState h) a) where
-  (==) :: LockstepAction (ModelState h) a -> LockstepAction (ModelState h) a -> Bool
+         , Typeable m
+         ) => Eq (LockstepAction (ModelState m h) a) where
+  (==) :: LockstepAction (ModelState m h) a -> LockstepAction (ModelState m h) a -> Bool
   Action merrs1 x == Action merrs2 y = merrs1 == merrs2 && x == y
     where
-      _coveredAllCases :: Action (Lockstep (ModelState h)) a -> ()
+      _coveredAllCases :: Action (Lockstep (ModelState m h)) a -> ()
       _coveredAllCases = \case
           Action{} -> ()
 
-data Action' h a where
+data Action' m h a where
   -- Tables
   NewTableWith ::
        C k v b
     => {-# UNPACK #-} !(PrettyProxy (k, v, b))
     -> Class.TableConfig h
-    -> Act' h (WrapTable h IO k v b)
+    -> Act' m h (WrapTable h m k v b)
   CloseTable ::
        C k v b
-    => Var h (WrapTable h IO k v b)
-    -> Act' h ()
+    => Var m h (WrapTable h m k v b)
+    -> Act' m h ()
   -- Queries
   Lookups ::
        C k v b
-    => V.Vector k -> Var h (WrapTable h IO k v b)
-    -> Act' h (V.Vector (LookupResult v (WrapBlobRef h IO b)))
+    => V.Vector k -> Var m h (WrapTable h m k v b)
+    -> Act' m h (V.Vector (LookupResult v (WrapBlobRef h m b)))
   RangeLookup ::
        (C k v b, Ord k)
-    => R.Range k -> Var h (WrapTable h IO k v b)
-    -> Act' h (V.Vector (Entry k v (WrapBlobRef h IO b)))
+    => R.Range k -> Var m h (WrapTable h m k v b)
+    -> Act' m h (V.Vector (Entry k v (WrapBlobRef h m b)))
   -- Cursor
   NewCursor ::
        C k v b
     => Maybe k
-    -> Var h (WrapTable h IO k v b)
-    -> Act' h (WrapCursor h IO k v b)
+    -> Var m h (WrapTable h m k v b)
+    -> Act' m h (WrapCursor h m k v b)
   CloseCursor ::
        C k v b
-    => Var h (WrapCursor h IO k v b)
-    -> Act' h ()
+    => Var m h (WrapCursor h m k v b)
+    -> Act' m h ()
   ReadCursor ::
        C k v b
     => Int
-    -> Var h (WrapCursor h IO k v b)
-    -> Act' h (V.Vector (Entry k v (WrapBlobRef h IO b)))
+    -> Var m h (WrapCursor h m k v b)
+    -> Act' m h (V.Vector (Entry k v (WrapBlobRef h m b)))
   -- Updates
   Updates ::
        C k v b
-    => V.Vector (k, R.Update v b) -> Var h (WrapTable h IO k v b)
-    -> Act' h ()
+    => V.Vector (k, R.Update v b) -> Var m h (WrapTable h m k v b)
+    -> Act' m h ()
   Inserts ::
        C k v b
-    => V.Vector (k, v, Maybe b) -> Var h (WrapTable h IO k v b)
-    -> Act' h ()
+    => V.Vector (k, v, Maybe b) -> Var m h (WrapTable h m k v b)
+    -> Act' m h ()
   Deletes ::
        C k v b
-    => V.Vector k -> Var h (WrapTable h IO k v b)
-    -> Act' h ()
+    => V.Vector k -> Var m h (WrapTable h m k v b)
+    -> Act' m h ()
   Upserts ::
        C k v b
-    => V.Vector (k, v) -> Var h (WrapTable h IO k v b)
-    -> Act' h ()
+    => V.Vector (k, v) -> Var m h (WrapTable h m k v b)
+    -> Act' m h ()
   -- Blobs
   RetrieveBlobs ::
        B b
-    => Var h (V.Vector (WrapBlobRef h IO b))
-    -> Act' h (V.Vector (WrapBlob b))
+    => Var m h (V.Vector (WrapBlobRef h m b))
+    -> Act' m h (V.Vector (WrapBlob b))
   -- Snapshots
   SaveSnapshot ::
        C k v b
     => Maybe SilentCorruption
     -> R.SnapshotName
     -> R.SnapshotLabel
-    -> Var h (WrapTable h IO k v b)
-    -> Act' h ()
+    -> Var m h (WrapTable h m k v b)
+    -> Act' m h ()
   OpenTableFromSnapshot ::
        C k v b
     => {-# UNPACK #-} !(PrettyProxy (k, v, b))
     -> R.SnapshotName
     -> R.SnapshotLabel
-    -> Act' h (WrapTable h IO k v b)
-  DeleteSnapshot :: R.SnapshotName -> Act' h ()
-  ListSnapshots  :: Act' h [R.SnapshotName]
+    -> Act' m h (WrapTable h m k v b)
+  DeleteSnapshot :: R.SnapshotName -> Act' m h ()
+  ListSnapshots  :: Act' m h [R.SnapshotName]
   -- Duplicate tables
   Duplicate ::
        C k v b
-    => Var h (WrapTable h IO k v b)
-    -> Act' h (WrapTable h IO k v b)
+    => Var m h (WrapTable h m k v b)
+    -> Act' m h (WrapTable h m k v b)
   -- Table union
   Union ::
        C k v b
-    => Var h (WrapTable h IO k v b)
-    -> Var h (WrapTable h IO k v b)
-    -> Act' h (WrapTable h IO k v b)
+    => Var m h (WrapTable h m k v b)
+    -> Var m h (WrapTable h m k v b)
+    -> Act' m h (WrapTable h m k v b)
   Unions ::
        C k v b
-    => NonEmpty (Var h (WrapTable h IO k v b))
-    -> Act' h (WrapTable h IO k v b)
+    => NonEmpty (Var m h (WrapTable h m k v b))
+    -> Act' m h (WrapTable h m k v b)
   RemainingUnionDebt ::
        C k v b
-    => Var h (WrapTable h IO k v b)
-    -> Act' h R.UnionDebt
+    => Var m h (WrapTable h m k v b)
+    -> Act' m h R.UnionDebt
   SupplyUnionCredits ::
        C k v b
-    => Var h (WrapTable h IO k v b)
+    => Var m h (WrapTable h m k v b)
     -> R.UnionCredits
-    -> Act' h R.UnionCredits
+    -> Act' m h R.UnionCredits
   -- | Alternative version of 'SupplyUnionCredits' that supplies a portion of
   -- the table's current union debt as union credits.
   --
@@ -781,9 +788,9 @@ data Action' h a where
   -- so that unions are more likely to finish during a sequence of actions.
   SupplyPortionOfDebt ::
        C k v b
-    => Var h (WrapTable h IO k v b)
+    => Var m h (WrapTable h m k v b)
     -> Portion
-    -> Act' h R.UnionCredits
+    -> Act' m h R.UnionCredits
 
 portionOf :: Portion -> R.UnionDebt -> R.UnionCredits
 portionOf (Portion denominator) (R.UnionDebt debt)
@@ -795,14 +802,15 @@ newtype Portion = Portion Int -- ^ Denominator: should be non-negative
   deriving stock (Show, Eq)
 
 deriving stock instance Show (Class.TableConfig h)
-                     => Show (Action' h a)
+                     => Show (Action' m h a)
 
 instance ( Eq (Class.TableConfig h)
          , Typeable h
-         ) => Eq (Action' h a) where
+         , Typeable m
+         ) => Eq (Action' m h a) where
   x == y = go x y
     where
-      go :: Action' h a -> Action' h a -> Bool
+      go :: Action' m h a -> Action' m h a -> Bool
       go
         (NewTableWith (PrettyProxy :: PrettyProxy kvb) conf1)
         (NewTableWith (PrettyProxy :: PrettyProxy kvb) conf2) =
@@ -853,7 +861,7 @@ instance ( Eq (Class.TableConfig h)
         Just var1 == cast var2 && portion1 == portion2
       go _ _ = False
 
-      _coveredAllCases :: Action' h a -> ()
+      _coveredAllCases :: Action' m h a -> ()
       _coveredAllCases = \case
           NewTableWith{} -> ()
           CloseTable{} -> ()
@@ -896,72 +904,73 @@ instance ( Eq (Class.TableConfig h)
          , Show (Class.TableConfig h)
          , Arbitrary (Class.TableConfig h)
          , Typeable h
-         ) => InLockstep (ModelState h) where
-  type instance ModelOp (ModelState h) = Op
+         , Typeable m
+         ) => InLockstep (ModelState m h) where
+  type instance ModelOp (ModelState m h) = Op
 
-  data instance ModelValue (ModelState h) a where
+  data instance ModelValue (ModelState m h) a where
     -- handle-like
     MTable ::
       Model.Table k v b ->
-      Val h (WrapTable h IO k v b)
-    MCursor :: Model.Cursor k v b -> Val h (WrapCursor h IO k v b)
+      Val m h (WrapTable h m k v b)
+    MCursor :: Model.Cursor k v b -> Val m h (WrapCursor h m k v b)
     MBlobRef ::
       (Class.C_ b) =>
       Model.BlobRef b ->
-      Val h (WrapBlobRef h IO b)
+      Val m h (WrapBlobRef h m b)
     -- values
     MLookupResult ::
       (Class.C_ v, Class.C_ b) =>
-      LookupResult v (Val h (WrapBlobRef h IO b)) ->
-      Val h (LookupResult v (WrapBlobRef h IO b))
+      LookupResult v (Val m h (WrapBlobRef h m b)) ->
+      Val m h (LookupResult v (WrapBlobRef h m b))
     MEntry ::
       (Class.C k v b) =>
-      Entry k v (Val h (WrapBlobRef h IO b)) ->
-      Val h (Entry k v (WrapBlobRef h IO b))
+      Entry k v (Val m h (WrapBlobRef h m b)) ->
+      Val m h (Entry k v (WrapBlobRef h m b))
     MBlob ::
       (Show b, Typeable b, Eq b) =>
       WrapBlob b ->
-      Val h (WrapBlob b)
-    MSnapshotName :: R.SnapshotName -> Val h R.SnapshotName
-    MUnionDebt :: R.UnionDebt -> Val h R.UnionDebt
-    MUnionCredits :: R.UnionCredits -> Val h R.UnionCredits
-    MUnionCreditsPortion :: R.UnionCredits -> Val h R.UnionCredits
-    MErr :: Model.Err -> Val h Model.Err
+      Val m h (WrapBlob b)
+    MSnapshotName :: R.SnapshotName -> Val m h R.SnapshotName
+    MUnionDebt :: R.UnionDebt -> Val m h R.UnionDebt
+    MUnionCredits :: R.UnionCredits -> Val m h R.UnionCredits
+    MUnionCreditsPortion :: R.UnionCredits -> Val m h R.UnionCredits
+    MErr :: Model.Err -> Val m h Model.Err
     -- combinators
-    MUnit :: () -> Val h ()
-    MPair :: (Val h a, Val h b) -> Val h (a, b)
-    MEither :: Either (Val h a) (Val h b) -> Val h (Either a b)
-    MList :: [Val h a] -> Val h [a]
-    MVector :: V.Vector (Val h a) -> Val h (V.Vector a)
+    MUnit :: () -> Val m h ()
+    MPair :: (Val m h a, Val m h b) -> Val m h (a, b)
+    MEither :: Either (Val m h a) (Val m h b) -> Val m h (Either a b)
+    MList :: [Val m h a] -> Val m h [a]
+    MVector :: V.Vector (Val m h a) -> Val m h (V.Vector a)
 
-  data instance Observable (ModelState h) a where
+  data instance Observable (ModelState m h) a where
     -- handle-like (opaque)
-    OTable :: Obs h (WrapTable h IO k v b)
-    OCursor :: Obs h (WrapCursor h IO k v b)
-    OBlobRef :: Obs h (WrapBlobRef h IO b)
+    OTable :: Obs m h (WrapTable h m k v b)
+    OCursor :: Obs m h (WrapCursor h m k v b)
+    OBlobRef :: Obs m h (WrapBlobRef h m b)
     -- values
     OLookupResult ::
       (Class.C_ v, Class.C_ b) =>
-      LookupResult v (Obs h (WrapBlobRef h IO b)) ->
-      Obs h (LookupResult v (WrapBlobRef h IO b))
+      LookupResult v (Obs m h (WrapBlobRef h m b)) ->
+      Obs m h (LookupResult v (WrapBlobRef h m b))
     OEntry ::
       (Class.C k v b) =>
-      Entry k v (Obs h (WrapBlobRef h IO b)) ->
-      Obs h (Entry k v (WrapBlobRef h IO b))
+      Entry k v (Obs m h (WrapBlobRef h m b)) ->
+      Obs m h (Entry k v (WrapBlobRef h m b))
     OBlob ::
       (Show b, Typeable b, Eq b) =>
       WrapBlob b ->
-      Obs h (WrapBlob b)
-    OUnionCredits :: R.UnionCredits -> Obs h R.UnionCredits
-    OUnionCreditsPortion :: R.UnionCredits -> Obs h R.UnionCredits
-    OId :: (Show a, Typeable a, Eq a) => a -> Obs h a
+      Obs m h (WrapBlob b)
+    OUnionCredits :: R.UnionCredits -> Obs m h R.UnionCredits
+    OUnionCreditsPortion :: R.UnionCredits -> Obs m h R.UnionCredits
+    OId :: (Show a, Typeable a, Eq a) => a -> Obs m h a
     -- combinators
-    OPair :: (Obs h a, Obs h b) -> Obs h (a, b)
-    OEither :: Either (Obs h a) (Obs h b) -> Obs h (Either a b)
-    OList :: [Obs h a] -> Obs h [a]
-    OVector :: V.Vector (Obs h a) -> Obs h (V.Vector a)
+    OPair :: (Obs m h a, Obs m h b) -> Obs m h (a, b)
+    OEither :: Either (Obs m h a) (Obs m h b) -> Obs m h (Either a b)
+    OList :: [Obs m h a] -> Obs m h [a]
+    OVector :: V.Vector (Obs m h a) -> Obs m h (V.Vector a)
 
-  observeModel :: Val h a -> Obs h a
+  observeModel :: Val m h a -> Obs m h a
   observeModel = \case
       MTable _               -> OTable
       MCursor _              -> OCursor
@@ -981,19 +990,19 @@ instance ( Eq (Class.TableConfig h)
       MVector x              -> OVector $ V.map observeModel x
 
   modelNextState ::  forall a.
-       LockstepAction (ModelState h) a
-    -> ModelVarContext (ModelState h)
-    -> ModelState h
-    -> (ModelValue (ModelState h) a, ModelState h)
+       LockstepAction (ModelState m h) a
+    -> ModelVarContext (ModelState m h)
+    -> ModelState m h
+    -> (ModelValue (ModelState m h) a, ModelState m h)
   modelNextState action ctx (ModelState state stats) =
       auxStats $ runModel (lookupVar ctx) action state
     where
-      auxStats :: (Val h a, Model.Model) -> (Val h a, ModelState h)
+      auxStats :: (Val m h a, Model.Model) -> (Val m h a, ModelState m h)
       auxStats (result, state') = (result, ModelState state' stats')
         where
           stats' = updateStats action (lookupVar ctx) state state' result stats
 
-  usedVars :: LockstepAction (ModelState h) a -> [AnyGVar (ModelOp (ModelState h))]
+  usedVars :: LockstepAction (ModelState m h) a -> [AnyGVar (ModelOp (ModelState m h))]
   usedVars (Action _ action') = case action' of
       NewTableWith _ _               -> []
       CloseTable tableVar            -> [SomeGVar tableVar]
@@ -1019,31 +1028,31 @@ instance ( Eq (Class.TableConfig h)
       SupplyPortionOfDebt tableVar _ -> [SomeGVar tableVar]
 
   arbitraryWithVars ::
-       ModelVarContext (ModelState h)
-    -> ModelState h
-    -> Gen (Any (LockstepAction (ModelState h)))
+       ModelVarContext (ModelState m h)
+    -> ModelState m h
+    -> Gen (Any (LockstepAction (ModelState m h)))
   arbitraryWithVars ctx st =
     QC.scale (max 100) $
     arbitraryActionWithVars (Proxy @(Key, Value, Blob)) keyValueBlobLabel ctx st
 
   shrinkWithVars ::
-       ModelVarContext (ModelState h)
-    -> ModelState h
-    -> LockstepAction (ModelState h) a
-    -> [Any (LockstepAction (ModelState h))]
+       ModelVarContext (ModelState m h)
+    -> ModelState m h
+    -> LockstepAction (ModelState m h) a
+    -> [Any (LockstepAction (ModelState m h))]
   shrinkWithVars = shrinkActionWithVars
 
   tagStep ::
-       (ModelState h, ModelState h)
-    -> LockstepAction (ModelState h) a
-    -> Val h a
+       (ModelState m h, ModelState m h)
+    -> LockstepAction (ModelState m h) a
+    -> Val m h a
     -> [String]
   tagStep states action = map show . tagStep' states action
 
-deriving stock instance Show (Class.TableConfig h) => Show (Val h a)
-deriving stock instance Show (Obs h a)
+deriving stock instance Show (Class.TableConfig h) => Show (Val m h a)
+deriving stock instance Show (Obs m h a)
 
-instance Eq (Obs h a) where
+instance Eq (Obs m h a) where
   obsReal == obsModel = case (obsReal, obsModel) of
       -- The model is conservative about blob retrieval: the model invalidates a
       -- blob reference immediately after an update to the table, and if the SUT
@@ -1114,7 +1123,7 @@ instance Eq (Obs h a) where
       (OVector x, OVector y) -> x == y
       (_, _) -> False
     where
-      _coveredAllCases :: Obs h a -> ()
+      _coveredAllCases :: Obs m h a -> ()
       _coveredAllCases = \case
           OTable{} -> ()
           OCursor{} -> ()
@@ -1186,12 +1195,12 @@ instance ( Eq (Class.TableConfig h)
          , Show (Class.TableConfig h)
          , Arbitrary (Class.TableConfig h)
          , Typeable h
-         ) => RunLockstep (ModelState h) (RealMonad h IO) where
+         ) => RunLockstep (ModelState IO h) (RealMonad h IO) where
   observeReal ::
        Proxy (RealMonad h IO)
-    -> LockstepAction (ModelState h) a
-    -> Realized (RealMonad h IO) a
-    -> Obs h a
+    -> LockstepAction (ModelState IO h) a
+    -> a
+    -> Obs IO h a
   observeReal _proxy (Action _ action') result = case action' of
       NewTableWith{}          -> OEither $ bimap OId (const OTable) result
       CloseTable{}            -> OEither $ bimap OId OId result
@@ -1221,8 +1230,8 @@ instance ( Eq (Class.TableConfig h)
 
   showRealResponse ::
        Proxy (RealMonad h IO)
-    -> LockstepAction (ModelState h) a
-    -> Maybe (Dict (Show (Realized (RealMonad h IO) a)))
+    -> LockstepAction (ModelState IO h) a
+    -> Maybe (Dict (Show a))
   showRealResponse _ (Action _ action') = case action' of
       NewTableWith{}          -> Nothing
       CloseTable{}            -> Just Dict
@@ -1252,12 +1261,13 @@ instance ( Eq (Class.TableConfig h)
          , Show (Class.TableConfig h)
          , Arbitrary (Class.TableConfig h)
          , Typeable h
-         ) => RunLockstep (ModelState h) (RealMonad h (IOSim s)) where
+         , Typeable s
+         ) => RunLockstep (ModelState (IOSim s) h) (RealMonad h (IOSim s)) where
   observeReal ::
        Proxy (RealMonad h (IOSim s))
-    -> LockstepAction (ModelState h) a
-    -> Realized (RealMonad h (IOSim s)) a
-    -> Obs h a
+    -> LockstepAction (ModelState (IOSim s) h) a
+    -> a
+    -> Obs (IOSim s) h a
   observeReal _proxy (Action _ action') result = case action' of
       NewTableWith{}          -> OEither $ bimap OId (const OTable) result
       CloseTable{}            -> OEither $ bimap OId OId result
@@ -1287,8 +1297,8 @@ instance ( Eq (Class.TableConfig h)
 
   showRealResponse ::
        Proxy (RealMonad h (IOSim s))
-    -> LockstepAction (ModelState h) a
-    -> Maybe (Dict (Show (Realized (RealMonad h (IOSim s)) a)))
+    -> LockstepAction (ModelState (IOSim s) h) a
+    -> Maybe (Dict (Show a))
   showRealResponse _ (Action _ action') = case action' of
       NewTableWith{}          -> Nothing
       CloseTable{}            -> Just Dict
@@ -1322,7 +1332,7 @@ instance ( Eq (Class.TableConfig h)
          , Show (Class.TableConfig h)
          , Arbitrary (Class.TableConfig h)
          , Typeable h
-         ) => RunModel (Lockstep (ModelState h)) (RealMonad h IO) where
+         ) => RunModel (Lockstep (ModelState IO h)) (RealMonad h IO) where
   perform _     = runIO
   postcondition = Lockstep.Defaults.postcondition
   monitoring    = Lockstep.Defaults.monitoring (Proxy @(RealMonad h IO))
@@ -1332,7 +1342,8 @@ instance ( Eq (Class.TableConfig h)
          , Show (Class.TableConfig h)
          , Arbitrary (Class.TableConfig h)
          , Typeable h
-         ) => RunModel (Lockstep (ModelState h)) (RealMonad h (IOSim s)) where
+         , Typeable s
+         ) => RunModel (Lockstep (ModelState (IOSim s) h)) (RealMonad h (IOSim s)) where
   perform _     = runIOSim
   postcondition = Lockstep.Defaults.postcondition
   monitoring    = Lockstep.Defaults.monitoring (Proxy @(RealMonad h (IOSim s)))
@@ -1348,9 +1359,9 @@ instance ( Eq (Class.TableConfig h)
 -- we start generating injected errors for these actions and testing with them.
 
 runModel ::
-     ModelLookUp (ModelState h)
-  -> LockstepAction (ModelState h) a
-  -> Model.Model -> (Val h a, Model.Model)
+     ModelLookUp (ModelState m h)
+  -> LockstepAction (ModelState m h) a
+  -> Model.Model -> (Val m h a, Model.Model)
 runModel lookUp (Action merrs action') = case action' of
     NewTableWith _ _cfg ->
       wrap MTable
@@ -1467,22 +1478,22 @@ runModel lookUp (Action merrs action') = case action' of
           (pure ()) -- TODO(err)
   where
     getTable ::
-         ModelValue (ModelState h) (WrapTable h IO k v b)
+         ModelValue (ModelState m h) (WrapTable h m k v b)
       -> Model.Table k v b
     getTable (MTable t) = t
 
     getCursor ::
-         ModelValue (ModelState h) (WrapCursor h IO k v b)
+         ModelValue (ModelState m h) (WrapCursor h m k v b)
       -> Model.Cursor k v b
     getCursor (MCursor t) = t
 
-    getBlobRefs :: ModelValue (ModelState h) (V.Vector (WrapBlobRef h IO b)) -> V.Vector (Model.BlobRef b)
+    getBlobRefs :: ModelValue (ModelState m h) (V.Vector (WrapBlobRef h m b)) -> V.Vector (Model.BlobRef b)
     getBlobRefs (MVector brs) = fmap (\(MBlobRef br) -> br) brs
 
 wrap ::
-     (a -> Val h b)
+     (a -> Val m h b)
   -> (Either Model.Err a, Model.Model)
-  -> (Val h (Either Model.Err b), Model.Model)
+  -> (Val m h (Either Model.Err b), Model.Model)
 wrap f = first (MEither . bimap MErr f)
 
 {-------------------------------------------------------------------------------
@@ -1498,16 +1509,16 @@ wrap f = first (MEither . bimap MErr f)
 
 runIO ::
      forall a h. Class.IsTable h
-  => LockstepAction (ModelState h) a
-  -> LookUp (RealMonad h IO)
-  -> RealMonad h IO (Realized (RealMonad h IO) a)
+  => LockstepAction (ModelState IO h) a
+  -> LookUp
+  -> RealMonad h IO a
 runIO action lookUp = ReaderT $ \ !env -> do
     aux env action
   where
     aux ::
          RealEnv h IO
-      -> LockstepAction (ModelState h) a
-      -> IO (Realized IO a)
+      -> LockstepAction (ModelState IO h) a
+      -> IO a
     aux env (Action merrs action') = case action' of
         NewTableWith _ cfg ->
           runRealWithInjectedErrors "NewTableWith" env merrs
@@ -1604,21 +1615,21 @@ runIO action lookUp = ReaderT $ \ !env -> do
       where
         session = envSession env
 
-    lookUp' :: Var h x -> Realized IO x
-    lookUp' = realLookupVar (Proxy @(RealMonad h IO)) lookUp
+    lookUp' :: Var m h x -> x
+    lookUp' = realLookupVar lookUp
 
 runIOSim ::
      forall s a h. Class.IsTable h
-  => LockstepAction (ModelState h) a
-  -> LookUp (RealMonad h (IOSim s))
-  -> RealMonad h (IOSim s) (Realized (RealMonad h (IOSim s)) a)
+  => LockstepAction (ModelState (IOSim s) h) a
+  -> LookUp
+  -> RealMonad h (IOSim s) a
 runIOSim action lookUp = ReaderT $ \ !env -> do
     aux env action
   where
     aux ::
          RealEnv h (IOSim s)
-      -> LockstepAction (ModelState h) a
-      -> IOSim s (Realized (IOSim s) a)
+      -> LockstepAction (ModelState (IOSim s) h) a
+      -> IOSim s a
     aux env (Action merrs action') = case action' of
         NewTableWith _ cfg ->
           runRealWithInjectedErrors "NewTableWith" env merrs
@@ -1715,8 +1726,8 @@ runIOSim action lookUp = ReaderT $ \ !env -> do
       where
         session = envSession env
 
-    lookUp' :: Var h x -> Realized (IOSim s) x
-    lookUp' = realLookupVar (Proxy @(RealMonad h (IOSim s))) lookUp
+    lookUp' :: Var m h x -> x
+    lookUp' = realLookupVar lookUp
 
 -- | @'runRealWithInjectedErrors' _ errsVar merrs action rollback@ runs @action@
 -- with injected errors if available in @merrs@.
@@ -1794,19 +1805,20 @@ catchErr hs action = catches (Right <$> action) (fmap f hs)
 -------------------------------------------------------------------------------}
 
 arbitraryActionWithVars ::
-     forall h k v b. (
+     forall m h k v b. (
        C k v b
      , Ord k
      , Eq (Class.TableConfig h)
      , Show (Class.TableConfig h)
      , Arbitrary (Class.TableConfig h)
      , Typeable h
+     , Typeable m
      )
   => Proxy (k, v, b)
   -> R.SnapshotLabel
-  -> ModelVarContext (ModelState h)
-  -> ModelState h
-  -> Gen (Any (LockstepAction (ModelState h)))
+  -> ModelVarContext (ModelState m h)
+  -> ModelState m h
+  -> Gen (Any (LockstepAction (ModelState m h)))
 arbitraryActionWithVars _ label ctx (ModelState st _stats) =
     QC.frequency $
       concat
@@ -1817,10 +1829,10 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) =
         , genActionsBlobRef
         ]
   where
-    _coveredAllCases :: LockstepAction (ModelState h) a -> ()
+    _coveredAllCases :: LockstepAction (ModelState m h) a -> ()
     _coveredAllCases (Action _ action') = _coveredAllCases' action'
 
-    _coveredAllCases' :: Action' h a -> ()
+    _coveredAllCases' :: Action' m h a -> ()
     _coveredAllCases' = \case
         NewTableWith{} -> ()
         CloseTable{} -> ()
@@ -1847,7 +1859,7 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) =
 
     genTableVar = QC.elements tableVars
 
-    tableVars :: [Var h (WrapTable h IO k v b)]
+    tableVars :: [Var m h (WrapTable h m k v b)]
     tableVars =
       [ fromRight v
       | v <- findVars ctx Proxy
@@ -1859,7 +1871,7 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) =
 
     genUnionDescendantTableVar = QC.elements unionDescendantTableVars
 
-    unionDescendantTableVars :: [Var h (WrapTable h IO k v b)]
+    unionDescendantTableVars :: [Var m h (WrapTable h m k v b)]
     unionDescendantTableVars =
         [ v
         | v <- tableVars
@@ -1870,7 +1882,7 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) =
 
     genCursorVar = QC.elements cursorVars
 
-    cursorVars :: [Var h (WrapCursor h IO k v b)]
+    cursorVars :: [Var m h (WrapCursor h m k v b)]
     cursorVars =
       [ fromRight v
       | v <- findVars ctx Proxy
@@ -1882,12 +1894,12 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) =
 
     genBlobRefsVar = QC.elements blobRefsVars
 
-    blobRefsVars :: [Var h (V.Vector (WrapBlobRef h IO b))]
+    blobRefsVars :: [Var m h (V.Vector (WrapBlobRef h m b))]
     blobRefsVars = fmap (mapGVar (OpComp OpLookupResults)) lookupResultVars
                 ++ fmap (mapGVar (OpComp OpEntrys))  queryResultVars
       where
-        lookupResultVars :: [Var h (V.Vector (LookupResult  v (WrapBlobRef h IO b)))]
-        queryResultVars  :: [Var h (V.Vector (Entry k v (WrapBlobRef h IO b)))]
+        lookupResultVars :: [Var m h (V.Vector (LookupResult  v (WrapBlobRef h m b)))]
+        queryResultVars  :: [Var m h (V.Vector (Entry k v (WrapBlobRef h m b)))]
 
         lookupResultVars = fromRight <$> findVars ctx Proxy
         queryResultVars  = fromRight <$> findVars ctx Proxy
@@ -1905,7 +1917,7 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) =
         , let snapshotname = R.toSnapshotName name
         ]
 
-    genActionsSession :: [(Int, Gen (Any (LockstepAction (ModelState h))))]
+    genActionsSession :: [(Int, Gen (Any (LockstepAction (ModelState m h))))]
     genActionsSession =
         [ (1, fmap Some $ (Action <$> genErrors <*>) $
             NewTableWith @k @v @b <$> pure PrettyProxy <*> QC.arbitrary)
@@ -1939,7 +1951,7 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) =
         , let genErrors = pure Nothing -- TODO: generate errors
         ]
 
-    genActionsTables :: [(Int, Gen (Any (LockstepAction (ModelState h))))]
+    genActionsTables :: [(Int, Gen (Any (LockstepAction (ModelState m h))))]
     genActionsTables
       | null tableVars = []
       | otherwise      =
@@ -1994,7 +2006,7 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) =
         ]
 
     -- | Generate table actions that have to do with unions.
-    genActionsUnion :: [(Int, Gen (Any (LockstepAction (ModelState h))))]
+    genActionsUnion :: [(Int, Gen (Any (LockstepAction (ModelState m h))))]
     genActionsUnion
       | null tableVars = []
       | otherwise =
@@ -2041,7 +2053,7 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) =
         -- TODO: tweak distribution once table unions are implemented
         genPortion = Portion <$> QC.elements [1, 2, 3]
 
-    genActionsCursor :: [(Int, Gen (Any (LockstepAction (ModelState h))))]
+    genActionsCursor :: [(Int, Gen (Any (LockstepAction (ModelState m h))))]
     genActionsCursor
       | null cursorVars = []
       | otherwise       =
@@ -2054,7 +2066,7 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) =
         | let genErrors = pure Nothing -- TODO: generate errors
         ]
 
-    genActionsBlobRef :: [(Int, Gen (Any (LockstepAction (ModelState h))))]
+    genActionsBlobRef :: [(Int, Gen (Any (LockstepAction (ModelState m h))))]
     genActionsBlobRef =
         [ (5, fmap Some $ (Action <$> genErrors <*>) $
             RetrieveBlobs <$> genBlobRefsVar)
@@ -2063,8 +2075,8 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) =
         ]
 
     fromRight ::
-         Var h (Either Model.Err a)
-      -> Var h a
+         Var m h (Either Model.Err a)
+      -> Var m h a
     fromRight = mapGVar (\op -> OpFromRight `OpComp` op)
 
     genLookupKeys :: Gen (V.Vector k)
@@ -2099,15 +2111,16 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) =
     genBlob = QC.arbitrary
 
 shrinkActionWithVars ::
-     forall h a. (
+     forall m h a. (
        Eq (Class.TableConfig h)
      , Arbitrary (Class.TableConfig h)
      , Typeable h
+     , Typeable m
      )
-  => ModelVarContext (ModelState h)
-  -> ModelState h
-  -> LockstepAction (ModelState h) a
-  -> [Any (LockstepAction (ModelState h))]
+  => ModelVarContext (ModelState m h)
+  -> ModelState m h
+  -> LockstepAction (ModelState m h) a
+  -> [Any (LockstepAction (ModelState m h))]
 shrinkActionWithVars _ctx _st (Action merrs action') =
         [ -- TODO: it's somewhat unfortunate, but we have to dynamically
           -- construct evidence that @a@ is typeable, which is a requirement
@@ -2122,7 +2135,7 @@ shrinkActionWithVars _ctx _st (Action merrs action') =
 
 -- | Dynamically construct evidence that the result type @a@ of an action is
 -- typeable.
-dictIsTypeable :: Typeable h => Action' h a -> Dict (Typeable a)
+dictIsTypeable :: (Typeable m, Typeable h) => Action' m h a -> Dict (Typeable a)
 dictIsTypeable = \case
       NewTableWith{}          -> Dict
       CloseTable{}            -> Dict
@@ -2148,15 +2161,16 @@ dictIsTypeable = \case
       SupplyPortionOfDebt{}   -> Dict
 
 shrinkAction'WithVars ::
-     forall h a. (
+     forall m h a. (
        Eq (Class.TableConfig h)
      , Arbitrary (Class.TableConfig h)
      , Typeable h
+     , Typeable m
      )
-  => ModelVarContext (ModelState h)
-  -> ModelState h
-  -> Action' h a
-  -> [Any (Action' h)]
+  => ModelVarContext (ModelState m h)
+  -> ModelState m h
+  -> Action' m h a
+  -> [Any (Action' m h)]
 shrinkAction'WithVars _ctx _st a = case a of
     NewTableWith p conf -> [
         Some $ NewTableWith p conf'
@@ -2231,7 +2245,7 @@ shrinkAction'WithVars _ctx _st a = case a of
   Interpret 'Op' against 'ModelValue'
 -------------------------------------------------------------------------------}
 
-instance InterpretOp Op (ModelValue (ModelState h)) where
+instance InterpretOp Op (ModelValue (ModelState m h)) where
   intOp = \case
     OpId                 -> Just
     OpFst                -> \case MPair   x -> Just (fst x)
@@ -2309,16 +2323,17 @@ initStats = Stats {
     }
 
 updateStats ::
-     forall h a. ( Show (Class.TableConfig h)
+     forall m h a. ( Show (Class.TableConfig h)
      , Eq (Class.TableConfig h)
      , Arbitrary (Class.TableConfig h)
      , Typeable h
+     , Typeable m
      )
-  => LockstepAction (ModelState h) a
-  -> ModelLookUp (ModelState h)
+  => LockstepAction (ModelState m h) a
+  -> ModelLookUp (ModelState m h)
   -> Model.Model
   -> Model.Model
-  -> Val h a
+  -> Val m h a
   -> Stats
   -> Stats
 updateStats action@(Action _merrs action') lookUp modelBefore modelAfter result =
@@ -2352,7 +2367,7 @@ updateStats action@(Action _merrs action') lookUp modelBefore modelAfter result
       (Lookups _ _, MEither (Right (MVector lrs))) -> stats {
           numLookupsResults =
             let count :: (Int, Int, Int)
-                      -> Val h (LookupResult v (WrapBlobRef h IO blob))
+                      -> Val m h (LookupResult v (WrapBlobRef h m blob))
                       -> (Int, Int, Int)
                 count (nf, f, fwb) (MLookupResult x) = case x of
                   NotFound        -> (nf+1, f  , fwb  )
@@ -2457,7 +2472,7 @@ updateStats action@(Action _merrs action') lookUp modelBefore modelAfter result
 
         -- Note that batches (of inserts lookups etc) count as one action.
         updateCount :: forall k v b.
-                       Var h (WrapTable h IO k v b)
+                       Var m h (WrapTable h m k v b)
                     -> Stats
         updateCount tableVar =
           let tid = getTableId (lookUp tableVar)
@@ -2501,7 +2516,7 @@ updateStats action@(Action _merrs action') lookUp modelBefore modelAfter result
 
     -- insert an entry into the parentTable for a table derived from a parent
     insertParentTableDerived :: forall k v b.
-                                [GVar Op (WrapTable h IO k v b)]
+                                [GVar Op (WrapTable h m k v b)]
                              -> Model.Table k v b -> Stats -> Stats
     insertParentTableDerived ptblVars tbl stats =
       let uptblIds :: [Model.TableID] -- the set of ultimate parent table ids
@@ -2558,7 +2573,7 @@ updateStats action@(Action _merrs action') lookUp modelBefore modelAfter result
       where
         -- add the current table to the front of the list of tables, if it's
         -- not the latest one already
-        updateLastActionLog :: GVar Op (WrapTable h IO k v b) -> Stats
+        updateLastActionLog :: GVar Op (WrapTable h m k v b) -> Stats
         updateLastActionLog tableVar =
           stats {
             dupTableActionLog = List.foldl'
@@ -2596,7 +2611,7 @@ updateStats action@(Action _merrs action') lookUp modelBefore modelAfter result
           | otherwise
           = stats
 
-    getTableId :: ModelValue (ModelState h) (WrapTable h IO k v b)
+    getTableId :: ModelValue (ModelState m h) (WrapTable h m k v b)
                      -> Model.TableID
     getTableId (MTable t) = Model.tableID t
 
@@ -2625,9 +2640,9 @@ data Tag =
 
 -- | This is run for after every action
 tagStep' ::
-     (ModelState h, ModelState h)
-  -> LockstepAction (ModelState h) a
-  -> Val h a
+     (ModelState m h, ModelState m h)
+  -> LockstepAction (ModelState m h) a
+  -> Val m h a
   -> [Tag]
 tagStep' (ModelState _stateBefore statsBefore,
           ModelState _stateAfter _statsAfter)
@@ -2744,7 +2759,7 @@ data FinalTag =
   deriving stock Show
 
 -- | This is run only after completing every action
-tagFinalState' :: Lockstep (ModelState h) -> [(String, [FinalTag])]
+tagFinalState' :: Lockstep (ModelState m h) -> [(String, [FinalTag])]
 tagFinalState' (getModel -> ModelState finalState finalStats) = concat [
       tagNumLookupsResults
     , tagNumUpdates
@@ -2849,7 +2864,7 @@ tagFinalState' (getModel -> ModelState finalState finalStats) = concat [
 runActionsBracket ::
      forall state st m e prop.  (
        RunLockstep state m
-     , e ~ Error (Lockstep state)
+     , e ~ Error (Lockstep state) m
      , forall a. IsPerformResult e a
      , QC.Testable prop
      )
diff --git a/test/Test/Database/LSMTree/StateMachine/DL.hs b/test/Test/Database/LSMTree/StateMachine/DL.hs
index e1cf05cf6..b09ed841e 100644
--- a/test/Test/Database/LSMTree/StateMachine/DL.hs
+++ b/test/Test/Database/LSMTree/StateMachine/DL.hs
@@ -11,6 +11,7 @@ import           Control.Monad (void)
 import           Control.RefCount
 import           Control.Tracer
 import qualified Data.Map.Strict as Map
+import           Data.Typeable (Typeable)
 import qualified Data.Vector as V
 import           Database.LSMTree as R
 import qualified Database.LSMTree.Internal.Config as R (TableConfig (..))
@@ -42,7 +43,7 @@ tests = testGroup "Test.Database.LSMTree.StateMachine.DL" [
     , test_noSwallowedExceptions
     ]
 
-instance DynLogicModel (Lockstep (ModelState R.Table))
+instance DynLogicModel (Lockstep (ModelState IO R.Table))
 
 -- | An example of how dynamic logic formulas can be run.
 --
@@ -64,7 +65,7 @@ prop_example =
     tr = nullTracer
 
 -- | Create an initial "large" table
-dl_example :: DL (Lockstep (ModelState R.Table)) ()
+dl_example :: Typeable m => DL (Lockstep (ModelState m R.Table)) ()
 dl_example = do
     -- Create an initial table and fill it with some inserts
     var3 <- action $ Action Nothing $ NewTableWith (PrettyProxy @((Key, Value, Blob))) (R.TableConfig {
@@ -152,7 +153,7 @@ prop_noSwallowedExceptions salt = forAllDL dl_noSwallowExceptions runner
 
 -- | Run any number of actions using the default actions generator, and finally
 -- run a single action with errors *definitely* enabled.
-dl_noSwallowExceptions :: DL (Lockstep (ModelState R.Table)) ()
+dl_noSwallowExceptions :: Typeable m => DL (Lockstep (ModelState m R.Table)) ()
 dl_noSwallowExceptions = do
     -- Run any number of actions as normal
     anyActions_
diff --git a/test/Test/Database/LSMTree/StateMachine/Op.hs b/test/Test/Database/LSMTree/StateMachine/Op.hs
index 6f68a98f2..9eeff5e0a 100644
--- a/test/Test/Database/LSMTree/StateMachine/Op.hs
+++ b/test/Test/Database/LSMTree/StateMachine/Op.hs
@@ -15,9 +15,7 @@ module Test.Database.LSMTree.StateMachine.Op (
   ) where
 
 import           Control.Monad ((<=<))
-import           Control.Monad.IOSim (IOSim)
-import           Control.Monad.Reader (ReaderT)
-import           Control.Monad.State (StateT)
+import           Control.Monad.Identity (Identity (..))
 import qualified Data.Vector as V
 import qualified Database.LSMTree.Class as Class
 import           GHC.Show (appPrec)
@@ -39,8 +37,8 @@ data Op a b where
   OpFromLeft           :: Op (Either a b) a
   OpFromRight          :: Op (Either a b) b
   OpComp               :: Op b c -> Op a b -> Op a c
-  OpLookupResults      :: Op (V.Vector (Class.LookupResult v (WrapBlobRef h IO b))) (V.Vector (WrapBlobRef h IO b))
-  OpEntrys             :: Op (V.Vector (Class.Entry k v (WrapBlobRef h IO b))) (V.Vector (WrapBlobRef h IO b))
+  OpLookupResults      :: Op (V.Vector (Class.LookupResult v (WrapBlobRef h m b))) (V.Vector (WrapBlobRef h m b))
+  OpEntrys             :: Op (V.Vector (Class.Entry k v (WrapBlobRef h m b))) (V.Vector (WrapBlobRef h m b))
 
 intOpId :: Op a b -> a -> Maybe b
 intOpId OpId            = Just
@@ -61,37 +59,8 @@ intOpId OpEntrys        = Just . V.mapMaybe getBlobRef
 instance Operation Op where
   opIdentity = OpId
 
-instance InterpretOp Op (Op.WrapRealized IO) where
-  intOp ::
-       Op a b
-    -> Op.WrapRealized IO a
-    -> Maybe (Op.WrapRealized IO b)
-  intOp = Op.intOpRealizedId intOpId
-
-instance InterpretOp Op (Op.WrapRealized m)
-      => InterpretOp Op (Op.WrapRealized (StateT s m)) where
-  intOp = Op.intOpTransformer
-
-instance InterpretOp Op (Op.WrapRealized m)
-      => InterpretOp Op (Op.WrapRealized (ReaderT r m)) where
-  intOp = Op.intOpTransformer
-
-instance InterpretOp Op (Op.WrapRealized (IOSim s)) where
-  intOp ::
-       Op a b
-    -> Op.WrapRealized (IOSim s) a
-    -> Maybe (Op.WrapRealized (IOSim s) b)
-  intOp = \case
-      OpId                 -> Just
-      OpFst                -> Just . Op.WrapRealized . fst . Op.unwrapRealized
-      OpSnd                -> Just . Op.WrapRealized . snd . Op.unwrapRealized
-      OpLeft               -> Just . Op.WrapRealized . Left . Op.unwrapRealized
-      OpRight              -> Just . Op.WrapRealized . Right . Op.unwrapRealized
-      OpFromLeft           -> either (Just . Op.WrapRealized) (const Nothing) . Op.unwrapRealized
-      OpFromRight          -> either (const Nothing) (Just . Op.WrapRealized) . Op.unwrapRealized
-      OpComp g f           -> Op.intOp g <=< Op.intOp f
-      OpLookupResults      -> Just  . Op.WrapRealized . V.mapMaybe getBlobRef . Op.unwrapRealized
-      OpEntrys             -> Just . Op.WrapRealized . V.mapMaybe getBlobRef . Op.unwrapRealized
+instance InterpretOp Op Identity where
+  intOp = Op.intOpIdentity intOpId
 
 {-------------------------------------------------------------------------------
   'Show' and 'Eq' instances
diff --git a/test/Test/Util/Orphans.hs b/test/Test/Util/Orphans.hs
index edd280d5d..341e4e9ab 100644
--- a/test/Test/Util/Orphans.hs
+++ b/test/Test/Util/Orphans.hs
@@ -12,66 +12,8 @@
 
 module Test.Util.Orphans () where
 
-import           Control.Concurrent.Class.MonadMVar (MonadMVar (..))
-import           Control.Concurrent.Class.MonadSTM (MonadSTM (..))
-import qualified Control.Concurrent.MVar as Real
-import qualified Control.Concurrent.STM as Real
-import           Control.Monad ((<=<))
-import           Control.Monad.IOSim (IOSim)
-import           Data.Kind (Type)
-import           Database.LSMTree (Cursor, Entry, LookupResult, Table)
-import           Database.LSMTree.Internal.Serialise (SerialiseKey,
-                     SerialiseValue)
-import           Database.LSMTree.Internal.Types (BlobRef)
+import           Database.LSMTree (SerialiseKey, SerialiseValue)
 import           Test.QuickCheck.Modifiers (Small (..))
-import           Test.QuickCheck.StateModel (Realized)
-import           Test.QuickCheck.StateModel.Lockstep (InterpretOp)
-import qualified Test.QuickCheck.StateModel.Lockstep.Op as Op
-import qualified Test.QuickCheck.StateModel.Lockstep.Op.SumProd as SumProd
-import           Test.Util.TypeFamilyWrappers (WrapBlob (..), WrapBlobRef (..),
-                     WrapCursor, WrapTable (..))
-
-{-------------------------------------------------------------------------------
-  IOSim
--------------------------------------------------------------------------------}
-
-type instance Realized (IOSim s) a = RealizeIOSim s a
-
-type RealizeIOSim :: Type -> Type -> Type
-type family RealizeIOSim s a where
-  -- io-classes
-  RealizeIOSim s (Real.TVar a) = TVar (IOSim s) a
-  RealizeIOSim s (Real.TMVar a) = TMVar (IOSim s) a
-  RealizeIOSim s (Real.MVar a) = MVar (IOSim s) a
-  -- lsm-tree
-  RealizeIOSim s (Table IO k v b) = Table (IOSim s) k v b
-  RealizeIOSim s (LookupResult v b) = LookupResult v (RealizeIOSim s b)
-  RealizeIOSim s (Entry k v b) = Entry k v (RealizeIOSim s b)
-  RealizeIOSim s (Cursor IO k v b) = Table (IOSim s) k v b
-  RealizeIOSim s (BlobRef IO b) = BlobRef (IOSim s) b
-  -- Type family wrappers
-  RealizeIOSim s (WrapTable h IO k v b) = WrapTable h (IOSim s) k v b
-  RealizeIOSim s (WrapCursor h IO k v b) = WrapCursor h (IOSim s) k v b
-  RealizeIOSim s (WrapBlobRef h IO b) = WrapBlobRef h (IOSim s) b
-  RealizeIOSim s (WrapBlob b) = WrapBlob b
-  -- Congruence
-  RealizeIOSim s (f a b) = f (RealizeIOSim s a) (RealizeIOSim s b)
-  RealizeIOSim s (f a) = f (RealizeIOSim s a)
-  -- Default
-  RealizeIOSim s a = a
-
-instance InterpretOp SumProd.Op (Op.WrapRealized (IOSim s)) where
-  intOp ::
-       SumProd.Op a b
-    -> Op.WrapRealized (IOSim s) a
-    -> Maybe (Op.WrapRealized (IOSim s) b)
-  intOp = \case
-      SumProd.OpId    -> Just
-      SumProd.OpFst   -> Just . Op.WrapRealized . fst . Op.unwrapRealized
-      SumProd.OpSnd   -> Just . Op.WrapRealized . snd . Op.unwrapRealized
-      SumProd.OpLeft  -> either (Just . Op.WrapRealized) (const Nothing) . Op.unwrapRealized
-      SumProd.OpRight -> either (const Nothing) (Just . Op.WrapRealized) . Op.unwrapRealized
-      SumProd.OpComp g f -> Op.intOp g <=< Op.intOp f
 
 {-------------------------------------------------------------------------------
   QuickCheck
diff --git a/test/Test/Util/QLS.hs b/test/Test/Util/QLS.hs
index 8474aac3a..f1c10f3fc 100644
--- a/test/Test/Util/QLS.hs
+++ b/test/Test/Util/QLS.hs
@@ -23,7 +23,7 @@ import           Test.QuickCheck.StateModel.Lockstep
 
 runActionsBracket ::
      ( RunLockstep state m
-     , e ~ Error (Lockstep state)
+     , e ~ Error (Lockstep state) m
      , forall a. IsPerformResult e a
      , Testable prop
      )

From 79eba848e1784b83ba390ad9dd44c1fd7d271ee1 Mon Sep 17 00:00:00 2001
From: Joris Dral <joris@well-typed.com>
Date: Thu, 3 Jul 2025 16:12:33 +0200
Subject: [PATCH 2/2] QLS: generalise and use `runActionsBracket` for `IO` and
 `IOSim`

---
 test/Test/Database/LSMTree/StateMachine.hs | 85 +++++++++-------------
 test/Test/Util/QLS.hs                      | 51 +++++++++----
 2 files changed, 70 insertions(+), 66 deletions(-)

diff --git a/test/Test/Database/LSMTree/StateMachine.hs b/test/Test/Database/LSMTree/StateMachine.hs
index 6d6d5a330..24f5aa262 100644
--- a/test/Test/Database/LSMTree/StateMachine.hs
+++ b/test/Test/Database/LSMTree/StateMachine.hs
@@ -53,14 +53,14 @@ import           Control.ActionRegistry (AbortActionRegistryError (..),
 import           Control.Concurrent.Class.MonadMVar.Strict
 import           Control.Concurrent.Class.MonadSTM.Strict
 import           Control.Exception (assert)
-import           Control.Monad (forM_, void, (<=<))
+import           Control.Monad (forM_, (<=<))
+import           Control.Monad.Class.MonadST (MonadST)
 import           Control.Monad.Class.MonadThrow (Exception (..), Handler (..),
-                     MonadCatch (..), MonadThrow (..), SomeException, catches,
-                     displayException, fromException)
+                     MonadCatch (..), MonadMask, MonadThrow (..), SomeException,
+                     catches, displayException, fromException)
 import           Control.Monad.IOSim
 import           Control.Monad.Primitive
 import           Control.Monad.Reader (ReaderT (..))
-import qualified Control.Monad.ST.Lazy as ST
 import           Control.RefCount (RefException, checkForgottenRefs,
                      ignoreForgottenRefs)
 import           Control.Tracer (Tracer, nullTracer)
@@ -120,10 +120,6 @@ import           Test.Database.LSMTree.StateMachine.Op (HasBlobRef (getBlobRef),
                      Op (..))
 import qualified Test.QuickCheck as QC
 import           Test.QuickCheck (Arbitrary, Gen, Property)
-import qualified Test.QuickCheck.Extras as QD
-import qualified Test.QuickCheck.Monadic as QC
-import           Test.QuickCheck.Monadic (PropertyM)
-import qualified Test.QuickCheck.StateModel as QD
 import           Test.QuickCheck.StateModel hiding (Var)
 import           Test.QuickCheck.StateModel.Lockstep
 import qualified Test.QuickCheck.StateModel.Lockstep.Defaults as Lockstep.Defaults
@@ -365,53 +361,37 @@ propLockstep_RealImpl_MockFS_IO tr cleanupFlag fsFlag refsFlag (QC.Fixed salt) =
         )
       tagFinalState'
 
--- We can not use @bracket@ inside @PropertyM@, so @acquire_RealImpl_MockFS@ and
--- @release_RealImpl_MockFS@ are not run in a masked state and it is not
--- guaranteed that the latter runs if the former succeeded. Therefore, if
--- @runActions@ fails (with exceptions), then not having @bracket@ might lead to
--- more exceptions, which can obfuscate the original reason that the property
--- failed. Because of this, if @prop@ fails, it's probably best to also try
--- running the @IO@ version of this property with the failing seed, and compare
--- the counterexamples to see which one is more interesting.
 propLockstep_RealImpl_MockFS_IOSim ::
      (forall s. Tracer (IOSim s) R.LSMTreeTrace)
   -> CheckCleanup
   -> CheckFS
   -> CheckRefs
   -> QC.Fixed R.Salt
+  -> Actions (Lockstep (ModelState (IOSim RealWorld) R.Table))
   -> QC.Property
 propLockstep_RealImpl_MockFS_IOSim tr cleanupFlag fsFlag refsFlag (QC.Fixed salt) =
-    flip QC.monadic prop $ \x -> QC.ioProperty $ do
-        trac <- ST.stToIO $ runSimTraceST x
-        case traceResult False trac of
-          Left e  -> pure $ QC.counterexample (show e) False
-          Right p -> pure p
-  where
-    prop :: forall s. Typeable s => PropertyM (IOSim s) Property
-    prop = do
-        actions <- QC.pick QC.arbitrary
-        (fsVar, session, errsVar, logVar) <- QC.run (acquire_RealImpl_MockFS tr salt)
-        faultsVar <- QC.run $ newMutVar []
-        let
-          env :: RealEnv R.Table (IOSim s)
-          env = RealEnv {
-              envSession = session
-            , envHandlers = realErrorHandlers @(IOSim s)
-            , envErrors = errsVar
-            , envErrorsLog = logVar
-            , envInjectFaultResults = faultsVar
-            }
-        void $ QD.runPropertyReaderT
-                (QD.runActions @(Lockstep (ModelState (IOSim s) R.Table)) actions)
-                env
-        faults <- QC.run $ readMutVar faultsVar
-        p <- QC.run $ propCleanup cleanupFlag $
-          release_RealImpl_MockFS fsFlag (fsVar, session, errsVar, logVar)
-        p' <- QC.run $ propRefs refsFlag
-        pure
-          $ tagFinalState actions tagFinalState'
-          $ QC.tabulate "Fault results" (fmap show faults)
-          $ p QC..&&. p'
+    runActionsBracket
+      (Proxy @(ModelState (IOSim RealWorld) R.Table))
+      cleanupFlag
+      refsFlag
+      (acquire_RealImpl_MockFS tr salt)
+      (release_RealImpl_MockFS fsFlag)
+      (\r (_, session, errsVar, logVar) -> do
+            faultsVar <- newMutVar []
+            let
+              env :: RealEnv R.Table (IOSim RealWorld)
+              env = RealEnv {
+                  envSession = session
+                , envHandlers = realErrorHandlers @(IOSim RealWorld)
+                , envErrors = errsVar
+                , envErrorsLog = logVar
+                , envInjectFaultResults = faultsVar
+                }
+            prop <- runReaderT r env
+            faults <- readMutVar faultsVar
+            pure $ QC.tabulate "Fault results" (fmap show faults) prop
+        )
+      tagFinalState'
 
 acquire_RealImpl_MockFS ::
      R.IOLike m
@@ -2862,18 +2842,21 @@ tagFinalState' (getModel -> ModelState finalState finalStats) = concat [
 -- count how often something happens over the course of running these actions,
 -- then we would want to only tag the final state, not intermediate steps.
 runActionsBracket ::
-     forall state st m e prop.  (
+     forall state st m n e prop.  (
        RunLockstep state m
      , e ~ Error (Lockstep state) m
      , forall a. IsPerformResult e a
      , QC.Testable prop
+     , MonadMask n
+     , MonadST n
+     , QLS.IOProperty n
      )
   => Proxy state
   -> CheckCleanup
   -> CheckRefs
-  -> IO st
-  -> (st -> IO prop)
-  -> (m QC.Property -> st -> IO QC.Property)
+  -> n st
+  -> (st -> n prop)
+  -> (m QC.Property -> st -> n QC.Property)
   -> (Lockstep state -> [(String, [FinalTag])])
   -> Actions (Lockstep state) -> QC.Property
 runActionsBracket p cleanupFlag refsFlag init cleanup runner tagger actions =
diff --git a/test/Test/Util/QLS.hs b/test/Test/Util/QLS.hs
index f1c10f3fc..7b51ab50d 100644
--- a/test/Test/Util/QLS.hs
+++ b/test/Test/Util/QLS.hs
@@ -6,13 +6,18 @@
 -- TODO: it might be nice to upstream these utilities to @quickcheck-lockstep@
 -- at some point.
 module Test.Util.QLS (
-    runActionsBracket
+    IOProperty (..)
+  , runActionsBracket
   ) where
 
 import           Prelude hiding (init)
 
-import           Control.Exception
 import           Control.Monad (void)
+import           Control.Monad.Class.MonadST
+import           Control.Monad.Class.MonadThrow
+import           Control.Monad.IOSim (IOSim, runSimTraceST, traceResult)
+import           Control.Monad.Primitive (RealWorld)
+import qualified Control.Monad.ST.Lazy as ST
 import           Data.Typeable
 import qualified Test.QuickCheck as QC
 import           Test.QuickCheck (Property, Testable)
@@ -21,16 +26,32 @@ import qualified Test.QuickCheck.StateModel as StateModel
 import           Test.QuickCheck.StateModel hiding (runActions)
 import           Test.QuickCheck.StateModel.Lockstep
 
+class IOProperty m where
+  ioProperty :: m Property -> Property
+
+instance IOProperty IO where
+  ioProperty = QC.ioProperty
+
+instance IOProperty (IOSim RealWorld) where
+  ioProperty x = QC.ioProperty $ do
+      trac <- ST.stToIO $ runSimTraceST x
+      case traceResult False trac of
+        Left e  -> pure $ QC.counterexample (show e) False
+        Right p -> pure p
+
 runActionsBracket ::
      ( RunLockstep state m
      , e ~ Error (Lockstep state) m
      , forall a. IsPerformResult e a
      , Testable prop
+     , MonadMask n
+     , MonadST n
+     , IOProperty n
      )
   => Proxy state
-  -> IO st -- ^ Initialisation
-  -> (st -> IO prop) -- ^ Cleanup
-  -> (m Property -> st -> IO Property) -- ^ Runner
+  -> n st -- ^ Initialisation
+  -> (st -> n prop) -- ^ Cleanup
+  -> (m Property -> st -> n Property) -- ^ Runner
   -> Actions (Lockstep state)
   -> Property
 runActionsBracket _ init cleanup runner actions =
@@ -38,24 +59,24 @@ runActionsBracket _ init cleanup runner actions =
       void $ StateModel.runActions actions
 
 ioPropertyBracket ::
-     (Testable a, Testable b)
-  => IO st
-  -> (st -> IO b)
-  -> (m a -> st -> IO a)
+     (Testable a, Testable b, MonadMask n, MonadST n, IOProperty n)
+  => n st
+  -> (st -> n b)
+  -> (m a -> st -> n a)
   -> m a
   -> Property
 ioPropertyBracket init cleanup runner prop =
-    QC.ioProperty $ mask $ \restore -> do
+    ioProperty $ mask $ \restore -> do
       st <- init
       a <- restore (runner prop st) `onException` cleanup st
       b <- cleanup st
       pure $ a QC..&&. b
 
-monadicBracketIO :: forall st a b m.
-     (Monad m, Testable a, Testable b)
-  => IO st
-  -> (st -> IO b)
-  -> (m Property -> st -> IO Property)
+monadicBracketIO :: forall st a b m n.
+     (Monad m, Testable a, Testable b, MonadMask n, MonadST n, IOProperty n)
+  => n st
+  -> (st -> n b)
+  -> (m Property -> st -> n Property)
   -> PropertyM m a
   -> Property
 monadicBracketIO init cleanup runner =