diff --git a/cabal.project b/cabal.project
index 9c97a6c5ba..331eefaa29 100644
--- a/cabal.project
+++ b/cabal.project
@@ -89,3 +89,11 @@ source-repository-package
    subdir:
      ouroboros-network-api
      ouroboros-network
+
+source-repository-package
+   type: git
+   location: https://github.com/input-output-hk/quickcheck-dynamic
+   tag: 6e7e9109492f849fdb7bef04fe98de0c28d3614f
+   --sha256: sha256-zZ7WsMfRs1fG16bmvI5vIh4fhQ8RGyEvYGLSWlrxpg0=
+   subdir:
+     quickcheck-dynamic
diff --git a/ouroboros-consensus-diffusion/test/consensus-test/Test/Consensus/GSM.hs b/ouroboros-consensus-diffusion/test/consensus-test/Test/Consensus/GSM.hs
index 44a57f4c32..de11f19320 100644
--- a/ouroboros-consensus-diffusion/test/consensus-test/Test/Consensus/GSM.hs
+++ b/ouroboros-consensus-diffusion/test/consensus-test/Test/Consensus/GSM.hs
@@ -525,6 +525,7 @@ wrapPositiveAction ::
   ( Show (QD.Action state a)
   , Eq (QD.Action state a)
   , Typeable a
+  , Show a
   ) =>
   QD.Action state a ->
   QD.Actions state
diff --git a/ouroboros-consensus/ouroboros-consensus.cabal b/ouroboros-consensus/ouroboros-consensus.cabal
index 5f2cd98720..8f8ab9e97b 100644
--- a/ouroboros-consensus/ouroboros-consensus.cabal
+++ b/ouroboros-consensus/ouroboros-consensus.cabal
@@ -780,8 +780,6 @@ test-suite storage-test
     Test.Ouroboros.Storage.LedgerDB.Snapshots
     Test.Ouroboros.Storage.LedgerDB.StateMachine
     Test.Ouroboros.Storage.LedgerDB.StateMachine.TestBlock
-    Test.Ouroboros.Storage.LedgerDB.V1.BackingStore
-    Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep
     Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Mock
     Test.Ouroboros.Storage.LedgerDB.V1.DbChangelog
     Test.Ouroboros.Storage.LedgerDB.V1.LMDB
@@ -801,12 +799,10 @@ test-suite storage-test
     bifunctors,
     bytestring,
     cardano-binary,
-    cardano-ledger-binary:testlib,
     cardano-ledger-core:{cardano-ledger-core, testlib},
     cardano-slotting:{cardano-slotting, testlib},
     cardano-strict-containers,
     cborg,
-    constraints,
     containers,
     contra-tracer,
     diff-containers,
@@ -815,7 +811,7 @@ test-suite storage-test
     fs-api ^>=0.4,
     fs-sim ^>=0.4,
     generics-sop,
-    io-classes:{io-classes, strict-mvar, strict-stm},
+    io-classes:{strict-stm},
     io-sim,
     mempack,
     mtl,
@@ -826,7 +822,6 @@ test-suite storage-test
     ouroboros-network-protocols,
     pretty-show,
     quickcheck-dynamic,
-    quickcheck-lockstep ^>=0.8,
     quickcheck-state-machine:no-vendored-treediff ^>=0.10,
     random,
     resource-registry,
diff --git a/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/LedgerDB.hs b/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/LedgerDB.hs
index cdc2d6418e..36001a8cea 100644
--- a/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/LedgerDB.hs
+++ b/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/LedgerDB.hs
@@ -9,7 +9,6 @@ import qualified Test.Ouroboros.Storage.LedgerDB.Serialisation as Serialisation
 import qualified Test.Ouroboros.Storage.LedgerDB.SnapshotPolicy as SnapshotPolicy
 import qualified Test.Ouroboros.Storage.LedgerDB.Snapshots as Snapshots
 import qualified Test.Ouroboros.Storage.LedgerDB.StateMachine as StateMachine
-import qualified Test.Ouroboros.Storage.LedgerDB.V1.BackingStore as BackingStore
 import qualified Test.Ouroboros.Storage.LedgerDB.V1.DbChangelog as DbChangelog
 import Test.Tasty (TestTree, testGroup)
 
@@ -19,8 +18,7 @@ tests =
     "LedgerDB"
     [ testGroup
         "V1"
-        [ BackingStore.tests
-        , DbChangelog.tests
+        [ DbChangelog.tests
         ]
     , -- Independent of the LedgerDB implementation
       SnapshotPolicy.tests
diff --git a/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/LedgerDB/StateMachine.hs b/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/LedgerDB/StateMachine.hs
index 1c45dae1be..37302cd16e 100644
--- a/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/LedgerDB/StateMachine.hs
+++ b/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/LedgerDB/StateMachine.hs
@@ -604,6 +604,7 @@ data Environment
       !(ResourceRegistry IO)
 
 data LedgerDBError = ErrorValidateExceededRollback
+  deriving Show
 
 instance RunModel Model (StateT Environment IO) where
   type Error Model (StateT Environment IO) = LedgerDBError
diff --git a/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/LedgerDB/V1/BackingStore.hs b/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/LedgerDB/V1/BackingStore.hs
deleted file mode 100644
index 7772d34d46..0000000000
--- a/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/LedgerDB/V1/BackingStore.hs
+++ /dev/null
@@ -1,328 +0,0 @@
-{-# LANGUAGE DerivingVia #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE GeneralisedNewtypeDeriving #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# OPTIONS_GHC -Wno-orphans #-}
-
-{- HLINT ignore "Use camelCase" -}
-
-module Test.Ouroboros.Storage.LedgerDB.V1.BackingStore
-  ( labelledExamples
-  , tests
-  ) where
-
-import Cardano.Binary (FromCBOR (..), ToCBOR (..))
-import Cardano.Slotting.Slot
-import Control.Concurrent.Class.MonadMVar.Strict
-import Control.Concurrent.Class.MonadSTM.Strict.TMVar
-import Control.Monad.Class.MonadThrow (Handler (..), catches)
-import Control.Monad.IO.Class (MonadIO (..))
-import Control.Monad.Reader (runReaderT)
-import qualified Data.Map.Strict as Map
-import Data.MemPack
-import qualified Data.SOP.Dict as Dict
-import qualified Data.Set as Set
-import Data.Typeable
-import Ouroboros.Consensus.Ledger.Tables
-import qualified Ouroboros.Consensus.Ledger.Tables.Diff as Diff
-import Ouroboros.Consensus.Ledger.Tables.Utils
-import qualified Ouroboros.Consensus.Storage.LedgerDB.V1.BackingStore as BS
-import qualified Ouroboros.Consensus.Storage.LedgerDB.V1.BackingStore.Impl.InMemory as InMemory
-import qualified Ouroboros.Consensus.Storage.LedgerDB.V1.BackingStore.Impl.LMDB as LMDB
-import Ouroboros.Consensus.Util.IOLike hiding
-  ( MonadMask (..)
-  , newMVar
-  , newTVarIO
-  , readMVar
-  )
-import qualified System.Directory as Dir
-import System.FS.API hiding (Handle)
-import System.FS.IO (ioHasFS)
-import qualified System.FS.Sim.MockFS as MockFS
-import System.FS.Sim.STM
-import qualified System.FilePath as FilePath
-import System.IO.Temp (createTempDirectory)
-import Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep
-import qualified Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Mock as Mock
-import Test.Ouroboros.Storage.LedgerDB.V1.LMDB (testLMDBLimits)
-import Test.QuickCheck (Arbitrary (..), Property)
-import qualified Test.QuickCheck as QC
-import Test.QuickCheck.StateModel as StateModel
-import Test.QuickCheck.StateModel.Lockstep as Lockstep
-import Test.QuickCheck.StateModel.Lockstep.Run as Lockstep
-import Test.Tasty
-import Test.Tasty.QuickCheck (QuickCheckTests (..), testProperty)
-import Test.Util.LedgerStateOnlyTables
-import Test.Util.Orphans.Arbitrary ()
-import Test.Util.Orphans.IOLike ()
-import Test.Util.Orphans.ToExpr ()
-
-{-------------------------------------------------------------------------------
-  Main test tree
--------------------------------------------------------------------------------}
-
-tests :: TestTree
-tests =
-  testGroup
-    "BackingStore"
-    [ adjustOption (scaleQuickCheckTests 10) $
-        testProperty "InMemory IO SimHasFS" $
-          testWithIO $
-            setupBSEnv InMemory.InMemArgs setupSimHasFS (pure ())
-    , adjustOption (scaleQuickCheckTests 10) $
-        testProperty "InMemory IO IOHasFS" $
-          testWithIO $ do
-            (fp, cleanup) <- setupTempDir
-            setupBSEnv InMemory.InMemArgs (setupIOHasFS fp) cleanup
-    , adjustOption (scaleQuickCheckTests 2) $
-        testProperty "LMDB IO IOHasFS" $
-          testWithIO $ do
-            (fp, cleanup) <- setupTempDir
-            lmdbTmpDir <- (FilePath.</> "BS_LMDB") <$> Dir.getTemporaryDirectory
-            setupBSEnv
-              (LMDB.LMDBBackingStoreArgs lmdbTmpDir (testLMDBLimits maxOpenValueHandles) Dict.Dict)
-              (setupIOHasFS fp)
-              (cleanup >> Dir.removeDirectoryRecursive lmdbTmpDir)
-    ]
-
-scaleQuickCheckTests :: Int -> QuickCheckTests -> QuickCheckTests
-scaleQuickCheckTests c (QuickCheckTests n) = QuickCheckTests $ c * n
-
-testWithIO ::
-  IO (BSEnv IO K K' V D) ->
-  Actions (Lockstep T) ->
-  Property
-testWithIO mkBSEnv = runActionsBracket pT mkBSEnv bsCleanup runner
-
-runner ::
-  RealMonad m ks k vs d a ->
-  BSEnv m ks k vs d ->
-  m a
-runner c r = runReaderT c $ bsRealEnv r
-
--- | Generate minimal examples for each label.
-labelledExamples :: IO ()
-labelledExamples = QC.labelledExamples $ tagActions pT
-
-{-------------------------------------------------------------------------------
-  Resources
--------------------------------------------------------------------------------}
-
-data BSEnv m ks k vs d = BSEnv
-  { bsRealEnv :: RealEnv m ks k vs d
-  , bsCleanup :: m ()
-  }
-
--- | Set up a simulated @'HasFS'@.
-setupSimHasFS :: IOLike m => m (SomeHasFS m)
-setupSimHasFS = SomeHasFS . simHasFS <$> newTMVarIO MockFS.empty
-
--- | Set up a @'HasFS'@ for @'IO'@.
-setupIOHasFS :: (PrimState m ~ PrimState IO, MonadIO m) => FilePath -> m (SomeHasFS m)
-setupIOHasFS = pure . SomeHasFS . ioHasFS . MountPoint
-
--- | In case we are running tests in @'IO'@, we must do some temporary directory
--- management.
-setupTempDir :: MonadIO m => m (FilePath, m ())
-setupTempDir = do
-  sysTmpDir <- liftIO Dir.getTemporaryDirectory
-  qsmTmpDir <- liftIO $ createTempDirectory sysTmpDir "BS_QSM"
-  pure (qsmTmpDir, liftIO $ Dir.removeDirectoryRecursive qsmTmpDir)
-
-setupBSEnv ::
-  BS.Backend m backend (OTLedgerState (QC.Fixed Word) (QC.Fixed Word)) =>
-  IOLike m =>
-  BS.Args m backend ->
-  m (SomeHasFS m) ->
-  m () ->
-  m (BSEnv m K K' V D)
-setupBSEnv mkBsArgs mkShfs cleanup = do
-  shfs@(SomeHasFS hfs) <- mkShfs
-
-  createDirectory hfs (mkFsPath ["copies"])
-
-  let bsi = BS.newBackingStoreInitialiser mempty mkBsArgs (BS.SnapshotsFS shfs)
-
-  bsVar <- newMVar =<< bsi (BS.InitFromValues Origin emptyOTLedgerState emptyLedgerTables)
-
-  let
-    bsCleanup = do
-      bs <- readMVar bsVar
-      catches (BS.bsClose bs) closeHandlers
-      cleanup
-
-  pure
-    BSEnv
-      { bsRealEnv =
-          RealEnv
-            { reBackingStoreInit = bsi
-            , reBackingStore = bsVar
-            }
-      , bsCleanup
-      }
-
--- | A backing store will throw an error on close if it has already been closed,
--- which we ignore if we are performing a close as part of resource cleanup.
-closeHandlers :: IOLike m => [Handler m ()]
-closeHandlers =
-  [ Handler $ \case
-      InMemory.InMemoryBackingStoreClosedExn -> pure ()
-      e -> throwIO e
-  , Handler $ \case
-      LMDB.LMDBErrClosed -> pure ()
-      e -> throwIO e
-  ]
-
-{-------------------------------------------------------------------------------
-  Types under test
--------------------------------------------------------------------------------}
-
-type T = BackingStoreState K K' V D
-
-pT :: Proxy T
-pT = Proxy
-
-type K = LedgerTables (OTLedgerState (QC.Fixed Word) (QC.Fixed Word)) KeysMK
-type K' = QC.Fixed Word
-type V = LedgerTables (OTLedgerState (QC.Fixed Word) (QC.Fixed Word)) ValuesMK
-type D = LedgerTables (OTLedgerState (QC.Fixed Word) (QC.Fixed Word)) DiffMK
-
-{-------------------------------------------------------------------------------
-  @'HasOps'@ instances
--------------------------------------------------------------------------------}
-
-instance Mock.EmptyValues V where
-  emptyValues = emptyLedgerTables
-
-instance Mock.ApplyDiff V D where
-  applyDiff = applyDiffs'
-
-instance Mock.LookupKeysRange K K' V where
-  lookupKeysRange = \prev n vs ->
-    let m'@(LedgerTables (ValuesMK v)) = case prev of
-          Nothing ->
-            ltmap (rangeRead n) vs
-          Just ks ->
-            ltliftA2 (rangeRead' n) ks vs
-     in (m', fst <$> Map.lookupMax v)
-   where
-    rangeRead :: Int -> ValuesMK k v -> ValuesMK k v
-    rangeRead n (ValuesMK vs) =
-      ValuesMK $ Map.take n vs
-
-    rangeRead' ::
-      Ord k =>
-      Int ->
-      KeysMK k v ->
-      ValuesMK k v ->
-      ValuesMK k v
-    rangeRead' n ksmk vsmk =
-      case Set.lookupMax ks of
-        Nothing -> ValuesMK Map.empty
-        Just k ->
-          ValuesMK $
-            Map.take n $
-              snd $
-                Map.split k vs
-     where
-      KeysMK ks = ksmk
-      ValuesMK vs = vsmk
-
-instance Mock.LookupKeys K V where
-  lookupKeys = ltliftA2 readKeys
-   where
-    readKeys ::
-      Ord k =>
-      KeysMK k v ->
-      ValuesMK k v ->
-      ValuesMK k v
-    readKeys (KeysMK ks) (ValuesMK vs) =
-      ValuesMK $ Map.restrictKeys vs ks
-
-instance Mock.ValuesLength V where
-  valuesLength (LedgerTables (ValuesMK m)) =
-    Map.size m
-
-instance Mock.MakeDiff V D where
-  diff t1 t2 = trackingToDiffs $ calculateDifference t1 t2
-
-instance Mock.DiffSize D where
-  diffSize (LedgerTables (DiffMK (Diff.Diff m))) = Map.size m
-
-instance Mock.KeysSize K where
-  keysSize (LedgerTables (KeysMK s)) = Set.size s
-
-instance Mock.MakeInitHint V where
-  makeInitHint _ = emptyOTLedgerState
-
-instance Mock.MakeWriteHint D where
-  makeWriteHint _ = (emptyOTLedgerState, emptyOTLedgerState)
-
-instance Mock.MakeReadHint V where
-  makeReadHint _ = emptyOTLedgerState
-
-instance Mock.MakeSerializeTablesHint V where
-  makeSerializeTablesHint _ = emptyOTLedgerState
-
-instance Mock.HasOps K K' V D
-
-{-------------------------------------------------------------------------------
-  Orphan Arbitrary instances
--------------------------------------------------------------------------------}
-
-deriving newtype instance
-  QC.Arbitrary (mk k v) =>
-  QC.Arbitrary (OTLedgerTables k v mk)
-
-instance
-  (Ord k, QC.Arbitrary k) =>
-  QC.Arbitrary (KeysMK k v)
-  where
-  arbitrary = KeysMK <$> QC.arbitrary
-  shrink (KeysMK ks) = KeysMK <$> QC.shrink ks
-
-instance
-  (Ord k, QC.Arbitrary k, QC.Arbitrary v) =>
-  QC.Arbitrary (DiffMK k v)
-  where
-  arbitrary = DiffMK <$> QC.arbitrary
-  shrink (DiffMK d) = DiffMK <$> QC.shrink d
-
-instance
-  (Ord k, QC.Arbitrary k, QC.Arbitrary v) =>
-  QC.Arbitrary (ValuesMK k v)
-  where
-  arbitrary = ValuesMK <$> QC.arbitrary
-  shrink (ValuesMK vs) = ValuesMK <$> QC.shrink vs
-
-deriving newtype instance
-  (Ord k, QC.Arbitrary k, QC.Arbitrary v) =>
-  QC.Arbitrary (Diff.Diff k v)
-instance QC.Arbitrary v => QC.Arbitrary (Diff.Delta v) where
-  arbitrary =
-    QC.oneof
-      [ Diff.Insert <$> QC.arbitrary
-      , pure Diff.Delete
-      ]
-
-instance QC.Arbitrary ks => QC.Arbitrary (BS.RangeQuery ks) where
-  arbitrary = BS.RangeQuery <$> QC.arbitrary <*> QC.arbitrary
-  shrink (BS.RangeQuery x y) = BS.RangeQuery <$> QC.shrink x <*> QC.shrink y
-
-instance NoThunks a => NoThunks (QC.Fixed a) where
-  wNoThunks ctxt = wNoThunks ctxt . QC.getFixed
-  showTypeOf _ = "Fixed " ++ showTypeOf (Proxy @a)
-
-deriving newtype instance MemPack a => MemPack (QC.Fixed a)
-deriving newtype instance FromCBOR a => FromCBOR (QC.Fixed a)
-deriving newtype instance ToCBOR a => ToCBOR (QC.Fixed a)
diff --git a/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/LedgerDB/V1/BackingStore/Lockstep.hs b/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/LedgerDB/V1/BackingStore/Lockstep.hs
deleted file mode 100644
index 9f753b8d84..0000000000
--- a/ouroboros-consensus/test/storage-test/Test/Ouroboros/Storage/LedgerDB/V1/BackingStore/Lockstep.hs
+++ /dev/null
@@ -1,988 +0,0 @@
-{-# 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 {unValues :: vs}
-  deriving stock (Show, Eq, Ord)
-  deriving newtype QC.Arbitrary
-
-{-------------------------------------------------------------------------------
-  Model state
--------------------------------------------------------------------------------}
-
-data BackingStoreState ks k vs d = BackingStoreState
-  { bssMock :: Mock vs
-  , bssStats :: Stats ks k vs d
-  }
-  deriving (Show, Eq)
-
-initState :: Mock.EmptyValues vs => BackingStoreState ks k vs d
-initState =
-  BackingStoreState
-    { bssMock = Mock.emptyMock
-    , bssStats = 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 = 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
-  { reBackingStoreInit :: BackingStoreInitializer 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.initialState initState
-  nextState = Lockstep.nextState
-  precondition st act =
-    Lockstep.precondition st act
-      && modelPrecondition (getModel st) act
-  arbitraryAction = Lockstep.arbitraryAction
-  shrinkAction = 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 = \_st -> runIO
-  postcondition = Lockstep.postcondition
-  monitoring = Lockstep.monitoring (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 (BackingStoreState mock _stats) action = case action of
-  BSInitFromValues _ _ _ -> isClosed mock
-  BSInitFromCopy _ _ -> isClosed mock
-  BSCopy _ _ -> canOpenReader
-  BSValueHandle -> canOpenReader
-  _ -> True
- where
-  canOpenReader = Map.size openValueHandles < maxOpenValueHandles
-  openValueHandles = Map.filter (== Mock.Open) (valueHandles 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 = \case
-    MValueHandle _ -> OValueHandle
-    MErr x -> OId x
-    MSlotNo x -> OId x
-    MValues x -> OValues x
-    MValuesAndLast x -> OValuesAndLast x
-    MUnit x -> OId x
-    MStatistics x -> OId x
-    MEither x -> OEither $ bimap observeModel observeModel x
-    MPair x -> OPair $ bimap observeModel observeModel 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 action lookUp (BackingStoreState mock stats) =
-    auxStats $ runMock lookUp action mock
-   where
-    auxStats ::
-      (BSVal ks k vs d a, Mock vs) ->
-      (BSVal ks k vs d a, BackingStoreState ks k vs d)
-    auxStats (result, state') =
-      ( result
-      , BackingStoreState state' $ updateStats action lookUp result 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 = \case
-    BSInitFromValues _ _ _ -> []
-    BSInitFromCopy _ _ -> []
-    BSClose -> []
-    BSCopy _ _ -> []
-    BSValueHandle -> []
-    BSWrite _ _ _ -> []
-    BSVHClose h -> [SomeGVar h]
-    BSVHRangeRead h _ _ -> [SomeGVar h]
-    BSVHRead h _ _ -> [SomeGVar h]
-    BSVHAtSlot h -> [SomeGVar h]
-    BSVHStat h -> [SomeGVar h]
-
-  arbitraryWithVars ::
-    ModelVarContext (BackingStoreState ks k vs d) ->
-    BackingStoreState ks k vs d ->
-    Gen (Any (LockstepAction (BackingStoreState ks k vs d)))
-  arbitraryWithVars = 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 = 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 (BackingStoreState _ before, BackingStoreState _ after) action val =
-    map show $ tagBSAction before after action 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 _proxy = \case
-    BSInitFromValues _ _ _ -> OEither . bimap OId OId
-    BSInitFromCopy _ _ -> OEither . bimap OId OId
-    BSClose -> OEither . bimap OId OId
-    BSCopy _ _ -> OEither . bimap OId OId
-    BSValueHandle -> OEither . bimap OId (const OValueHandle)
-    BSWrite _ _ _ -> OEither . bimap OId OId
-    BSVHClose _ -> OEither . bimap OId OId
-    BSVHRangeRead _ _ _ -> OEither . bimap OId (OValuesAndLast . first unValues)
-    BSVHRead _ _ _ -> OEither . bimap OId (OValues . unValues)
-    BSVHAtSlot _ -> OEither . bimap OId OId
-    BSVHStat _ -> OEither . bimap OId OId
-
-  showRealResponse ::
-    Proxy (RealMonad IO ks k vs d) ->
-    LockstepAction (BackingStoreState ks k vs d) a ->
-    Maybe (Dict (Show a))
-  showRealResponse _proxy = \case
-    BSInitFromValues _ _ _ -> Just Dict
-    BSInitFromCopy _ _ -> Just Dict
-    BSClose -> Just Dict
-    BSCopy _ _ -> Just Dict
-    BSValueHandle -> Nothing
-    BSWrite _ _ _ -> Just Dict
-    BSVHClose _ -> Just Dict
-    BSVHRangeRead _ _ _ -> Just Dict
-    BSVHRead _ _ _ -> Just Dict
-    BSVHAtSlot _ -> Just Dict
-    BSVHStat _ -> Just 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 lookUp = \case
-  BSInitFromValues sl h (Values vs) ->
-    wrap MUnit . runMockMonad (Mock.mBSInitFromValues sl h vs)
-  BSInitFromCopy h bsp ->
-    wrap MUnit . runMockMonad (Mock.mBSInitFromCopy h bsp)
-  BSClose ->
-    wrap MUnit . runMockMonad Mock.mBSClose
-  BSCopy h bsp ->
-    wrap MUnit . runMockMonad (Mock.mBSCopy h bsp)
-  BSValueHandle ->
-    wrap MValueHandle . runMockMonad Mock.mBSValueHandle
-  BSWrite sl whint d ->
-    wrap MUnit . runMockMonad (Mock.mBSWrite sl whint d)
-  BSVHClose h ->
-    wrap MUnit . runMockMonad (Mock.mBSVHClose (getHandle $ lookupVar lookUp h))
-  BSVHRangeRead h rhint rq ->
-    wrap MValuesAndLast . runMockMonad (Mock.mBSVHRangeRead (getHandle $ lookupVar lookUp h) rhint rq)
-  BSVHRead h rhint ks ->
-    wrap MValues . runMockMonad (Mock.mBSVHRead (getHandle $ lookupVar lookUp h) rhint ks)
-  BSVHAtSlot h ->
-    wrap MSlotNo . runMockMonad (Mock.mBSVHAtSlot (getHandle $ lookupVar lookUp h))
-  BSVHStat h ->
-    wrap MStatistics . runMockMonad (Mock.mBSVHStat (getHandle $ lookupVar lookUp h))
- where
-  wrap f = first (MEither . bimap MErr f)
-
-  getHandle :: BSVal ks k vs d (BS.BackingStoreValueHandle IO ks k vs) -> ValueHandle vs
-  getHandle (MValueHandle h) = 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 fv (BackingStoreState mock _stats) =
-  QC.frequency $
-    withoutVars
-      ++ case findVars fv (Proxy @(Either Err (BS.BackingStoreValueHandle IO ks k vs))) of
-        [] -> []
-        vars -> withVars (QC.elements vars)
- where
-  withoutVars :: [(Int, Gen (Any (LockstepAction (BackingStoreState ks k vs d))))]
-  withoutVars =
-    [
-      ( 5
-      , fmap Some $
-          BSInitFromValues
-            <$> QC.arbitrary
-            <*> pure (Mock.makeInitHint (Proxy @vs))
-            <*> (Values <$> QC.arbitrary)
-      )
-    ,
-      ( 5
-      , fmap Some $
-          BSInitFromCopy
-            <$> pure (Mock.makeInitHint (Proxy @vs))
-            <*> genBackingStorePath
-      )
-    , (2, pure $ Some BSClose)
-    , (5, fmap Some $ BSCopy <$> pure (Mock.makeSerializeTablesHint (Proxy @vs)) <*> genBackingStorePath)
-    , (5, pure $ Some BSValueHandle)
-    ,
-      ( 5
-      , fmap Some $
-          BSWrite
-            <$> genSlotNo
-            <*> pure (Mock.makeWriteHint (Proxy @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 genVar =
-    [ (5, fmap Some $ BSVHClose <$> (opFromRight <$> genVar))
-    ,
-      ( 5
-      , fmap Some $
-          BSVHRangeRead
-            <$> (opFromRight <$> genVar)
-            <*> pure (Mock.makeReadHint (Proxy @vs))
-            <*> QC.arbitrary
-      )
-    ,
-      ( 5
-      , fmap Some $
-          BSVHRead
-            <$> (opFromRight <$> genVar)
-            <*> pure (Mock.makeReadHint (Proxy @vs))
-            <*> QC.arbitrary
-      )
-    , (5, fmap Some $ BSVHAtSlot <$> (opFromRight <$> genVar))
-    , (5, fmap Some $ BSVHStat <$> (opFromRight <$> genVar))
-    ]
-   where
-    opFromRight :: forall a. GVar Op (Either Err a) -> GVar Op a
-    opFromRight = mapGVar (\op -> OpRight `OpComp` op)
-
-  genBackingStorePath :: Gen FS.FsPath
-  genBackingStorePath = do
-    file <- 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 = QC.elements [show x | x <- [1 :: 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 = do
-    n :: Int <- QC.choose (-5, 5)
-    pure $ maybe 0 (+ fromIntegral n) (withOriginToMaybe seqNo)
-   where
-    seqNo = backingSeqNo mock
-
-  -- Generate valid diffs most of the time, and generate fully arbitrary
-  -- (probably invalid) diffs some of the time.
-  genDiff :: Gen d
-  genDiff =
-    QC.frequency
-      [ (9, Mock.diff (backingValues mock) <$> QC.arbitrary)
-      , (1, 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 _findVars (BackingStoreState _mock _) = \case
-  BSWrite sl st d ->
-    [Some $ BSWrite sl st d' | d' <- QC.shrink d]
-      ++ [Some $ BSWrite sl' st d | sl' <- QC.shrink sl]
-  BSVHRangeRead h rhint rq ->
-    [Some $ BSVHRangeRead h rhint rq' | rq' <- QC.shrink rq]
-  BSVHRead h rhint ks ->
-    [Some $ BSVHRead h rhint ks' | ks' <- QC.shrink ks]
-  _ -> []
-
-{-------------------------------------------------------------------------------
-  Interpret @'Op'@ against @'ModelValue'@
--------------------------------------------------------------------------------}
-
-instance InterpretOp Op (ModelValue (BackingStoreState ks k vs d)) where
-  intOp OpId = Just
-  intOp OpFst = \case
-    MPair x -> Just (fst x)
-    MValuesAndLast{} -> error "What?"
-  intOp OpSnd = \case
-    MPair x -> Just (snd x)
-    MValuesAndLast{} -> error "What?"
-  intOp OpLeft = \case MEither x -> either Just (const Nothing) x
-  intOp OpRight = \case MEither x -> either (const Nothing) Just x
-  intOp (OpComp g f) = intOp g <=< intOp 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 action lookUp = ReaderT $ \renv ->
-  aux renv action
- where
-  aux ::
-    RealEnv IO ks k vs d ->
-    LockstepAction (BackingStoreState ks k vs d) a ->
-    IO a
-  aux renv = \case
-    BSInitFromValues sl h (Values vs) -> catchErr $ do
-      bs <- bsi (BS.InitFromValues sl h vs)
-      void $ swapMVar bsVar bs
-    BSInitFromCopy h bsp -> catchErr $ do
-      bs <- bsi (BS.InitFromCopy h bsp)
-      void $ swapMVar bsVar bs
-    BSClose ->
-      catchErr $
-        readMVar bsVar >>= BS.bsClose
-    BSCopy s bsp ->
-      catchErr $
-        readMVar bsVar >>= \bs -> BS.bsCopy bs s bsp
-    BSValueHandle ->
-      catchErr $
-        readMVar bsVar >>= BS.bsValueHandle
-    BSWrite sl whint d ->
-      catchErr $
-        readMVar bsVar >>= \bs -> BS.bsWrite bs sl whint d
-    BSVHClose var ->
-      catchErr $
-        BS.bsvhClose (lookUp' var)
-    BSVHRangeRead var rhint rq ->
-      catchErr $
-        first Values
-          <$> BS.bsvhRangeRead (lookUp' var) rhint rq
-    BSVHRead var rhint ks ->
-      catchErr $
-        Values
-          <$> BS.bsvhRead (lookUp' var) rhint ks
-    BSVHAtSlot var ->
-      catchErr $
-        pure (BS.bsvhAtSlot (lookUp' var))
-    BSVHStat var ->
-      catchErr $
-        BS.bsvhStat (lookUp' var)
-   where
-    RealEnv
-      { reBackingStoreInit = bsi
-      , reBackingStore = bsVar
-      } = renv
-
-    lookUp' :: BSVar ks k vs d x -> x
-    lookUp' = realLookupVar lookUp
-
-catchErr :: forall m a. IOLike m => m a -> m (Either Err a)
-catchErr act =
-  catches
-    (Right <$> act)
-    [mkHandler fromTVarExn, mkHandler fromTVarExn', mkHandler fromDbErr]
-
-{-------------------------------------------------------------------------------
-  Statistics and tagging
--------------------------------------------------------------------------------}
-
-data Stats ks k vs d = Stats
-  { handleSlots :: Map (ValueHandle vs) (WithOrigin SlotNo)
-  -- ^ Slots that value handles were created in
-  , writeSlots :: Map SlotNo Int
-  -- ^ Slots in which writes were performed
-  , readAfterWrite :: Bool
-  -- ^ A value handle was created before a write, and read after the write
-  , rangeReadAfterWrite :: Bool
-  -- ^ A value handle was created before a write, and range read after the
-  -- write
-  }
-  deriving stock (Show, Eq)
-
-initStats :: Stats ks k vs d
-initStats =
-  Stats
-    { handleSlots = Map.empty
-    , writeSlots = Map.empty
-    , readAfterWrite = False
-    , rangeReadAfterWrite = 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 action lookUp result stats@Stats{handleSlots, writeSlots} =
-  updateHandleSlots
-    . updateWriteSlots
-    . updateReadAfterWrite
-    . updateRangeReadAfterWrite
-    $ stats
- where
-  getHandle :: BSVal ks k vs d (BS.BackingStoreValueHandle IO ks k vs) -> ValueHandle vs
-  getHandle (MValueHandle h) = h
-
-  updateHandleSlots :: Stats ks k vs d -> Stats ks k vs d
-  updateHandleSlots s = case (action, result) of
-    (BSValueHandle, MEither (Right (MValueHandle h))) ->
-      s{handleSlots = Map.insert h (seqNo h) handleSlots}
-    (BSClose, MEither (Right _)) ->
-      s{handleSlots = Map.empty}
-    (BSVHClose h, MEither (Right _)) ->
-      s{handleSlots = Map.delete (getHandle $ lookupVar lookUp h) handleSlots}
-    _ -> s
-
-  updateWriteSlots :: Stats ks k vs d -> Stats ks k vs d
-  updateWriteSlots s = case (action, result) of
-    (BSWrite sl _ d, MEither (Right (MUnit ())))
-      | 1 <= Mock.diffSize d ->
-          s{writeSlots = Map.insert sl (Mock.diffSize d) writeSlots}
-    (BSClose, MEither (Right _)) ->
-      s{writeSlots = Map.empty}
-    _ -> s
-
-  updateReadAfterWrite :: Stats ks k vs d -> Stats ks k vs d
-  updateReadAfterWrite s = case (action, result) of
-    (BSVHRead h _ _, MEither (Right (MValues vs)))
-      | h' <- getHandle $ lookupVar lookUp h
-      , Just wosl <- Map.lookup h' handleSlots
-      , Just (sl, _) <- Map.lookupMax writeSlots
-      , wosl < at sl
-      , 1 <= Mock.valuesLength vs ->
-          s{readAfterWrite = True}
-    _ -> s
-
-  updateRangeReadAfterWrite :: Stats ks k vs d -> Stats ks k vs d
-  updateRangeReadAfterWrite s = case (action, result) of
-    (BSVHRangeRead h _ _, MEither (Right (MValuesAndLast (vs, _))))
-      | h' <- getHandle $ lookupVar lookUp h
-      , Just wosl <- Map.lookup h' handleSlots
-      , Just (sl, _) <- Map.lookupMax writeSlots
-      , wosl < at sl
-      , 1 <= Mock.valuesLength vs ->
-          s{rangeReadAfterWrite = True}
-    _ -> s
-
-data TagAction
-  = TBSInitFromValues
-  | TBSInitFromCopy
-  | TBSClose
-  | TBSCopy
-  | TBSValueHandle
-  | TBSWrite
-  | TBSVHClose
-  | TBSVHRangeRead
-  | TBSVHRead
-  | TBSVHAtSlot
-  | TBSVHStat
-  deriving (Show, Eq, Ord, Bounded, Enum)
-
--- | Identify actions by their constructor.
-tAction :: LockstepAction (BackingStoreState ks k vs d) a -> TagAction
-tAction = \case
-  BSInitFromValues _ _ _ -> TBSInitFromValues
-  BSInitFromCopy _ _ -> TBSInitFromCopy
-  BSClose -> TBSClose
-  BSCopy _ _ -> TBSCopy
-  BSValueHandle -> TBSValueHandle
-  BSWrite _ _ _ -> TBSWrite
-  BSVHClose _ -> TBSVHClose
-  BSVHRangeRead _ _ _ -> TBSVHRangeRead
-  BSVHRead _ _ _ -> TBSVHRead
-  BSVHAtSlot _ -> TBSVHAtSlot
-  BSVHStat _ -> 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 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 before after action result =
-  globalTags ++ case (action, result) of
-    (_, MEither (Left (MErr ErrBackingStoreClosed))) ->
-      [ErrorBecauseBackingStoreIsClosed (tAction action)]
-    (_, MEither (Left (MErr ErrBackingStoreValueHandleClosed))) ->
-      [ErrorBecauseBackingStoreValueHandleIsClosed (tAction action)]
-    _ -> []
- where
-  globalTags =
-    mconcat
-      [ [ ReadAfterWrite
-        | not (readAfterWrite before)
-        , readAfterWrite after
-        ]
-      , [ RangeReadAfterWrite
-        | not (rangeReadAfterWrite before)
-        , rangeReadAfterWrite after
-        ]
-      ]
-
-{-------------------------------------------------------------------------------
-  Errors
--------------------------------------------------------------------------------}
-
-mkHandler ::
-  (IOLike m, Exception e) =>
-  (e -> Maybe Err) ->
-  Handler m (Either Err a)
-mkHandler fhandler = Handler $
-  \e -> maybe (throwIO e) (return . Left) (fhandler e)
-
--- | Map LMDB errors to mock errors.
-fromDbErr :: LMDB.LMDBErr -> Maybe Err
-fromDbErr = \case
-  LMDBErrNoDbSeqNo -> Nothing
-  LMDBErrNonMonotonicSeq wo wo' -> Just $ ErrNonMonotonicSeqNo wo wo'
-  LMDBErrInitialisingNonEmpty _ -> Nothing
-  LMDBErrNoValueHandle _ -> Just ErrBackingStoreValueHandleClosed
-  LMDBErrBadRead -> Nothing
-  LMDBErrBadRangeRead -> Nothing
-  LMDBErrDirExists _ -> Just ErrCopyPathAlreadyExists
-  LMDBErrDirDoesntExist _ -> Just ErrCopyPathDoesNotExist
-  LMDBErrDirIsNotLMDB _ -> Nothing
-  LMDBErrClosed -> Just ErrBackingStoreClosed
-  LMDBErrInitialisingAlreadyHasState -> Nothing
-  LMDBErrUnableToReadSeqNo -> Nothing
-  LMDBErrNotADir _ -> Nothing
-
--- | Map InMemory (i.e., @TVarBackingStore@) errors to mock errors.
-fromTVarExn :: BS.InMemoryBackingStoreExn -> Maybe Err
-fromTVarExn = \case
-  BS.InMemoryBackingStoreClosedExn -> Just ErrBackingStoreClosed
-  BS.InMemoryBackingStoreValueHandleClosedExn -> Just ErrBackingStoreValueHandleClosed
-  BS.InMemoryBackingStoreDirectoryExists -> Just ErrCopyPathAlreadyExists
-  BS.InMemoryBackingStoreNonMonotonicSeq wo wo' -> Just $ ErrNonMonotonicSeqNo wo wo'
-  BS.InMemoryBackingStoreDeserialiseExn _ -> Nothing
-  BS.InMemoryIncompleteDeserialiseExn -> Nothing
-
-fromTVarExn' :: BS.InMemoryBackingStoreInitExn -> Maybe Err
-fromTVarExn' = \case
-  BS.StoreDirIsIncompatible _ -> Just ErrCopyPathDoesNotExist