Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 1675 deletions

diff --git a/source/Test/Unit/Store.hs b/source/Test/Unit/Store.hs
deleted file mode 100644
index fb207d1..0000000
--- a/source/Test/Unit/Store.hs
+++ /dev/null
@@ -1,1675 +0,0 @@
-{-# LANGUAGE NoImplicitPrelude #-}
-
-module Test.Unit.Store (unitTests) where
-
-import Base
-import Checking.Authority qualified as Authority
-import Checking.Core qualified as Core
-import Checking.Declaration qualified as Declaration
-import Checking.Foundation qualified as Foundation
-import Checking.Identity qualified as Identity
-import Checking.Module qualified as Typed
-import Checking.Semantic qualified as Semantic
-import Felix.Cache.Codec qualified as Cache
-import Felix.Math.Codec
-import Felix.Module
-import Felix.Parsed.Identity qualified as Parsed
-import Felix.Parsed.Payload qualified as ParsedPayload
-import Felix.Source.Content qualified as Content
-import Felix.Source
-import Felix.Store qualified as Store
-import Felix.Provers qualified as Provers
-import Syntax.Interface qualified as Syntax
-
-import Control.Concurrent (threadDelay)
-import Control.Exception qualified as Exception
-import Data.ByteString qualified as ByteString
-import Data.ByteString.Char8 qualified as ByteString.Char8
-import Data.IORef qualified as IORef
-import Database.SQLite.Simple qualified as SQLite
-import Database.SQLite.Simple.Types (Only(..))
-import System.Directory qualified as Directory
-import System.Environment qualified as Environment
-import System.FilePath.Posix qualified as Posix
-import System.IO.Temp qualified as Temp
-import Test.Tasty
-import Test.Tasty.HUnit
-import UnliftIO.Async (concurrently)
-
-
-unitTests :: TestTree
-unitTests =
-    testGroup "SQLite store"
-        [ testCase "initializes and reopens the current schema"
-            initializesAndReopensCurrentSchema
-        , testCase "serializes invocation-local coordinator access"
-            serializesCoordinatorAccess
-        , testCase "rejects incompatibility without configuring the store"
-            rejectsIncompatibilityWithoutConfiguration
-        , testCase "rejects malformed compatibility metadata"
-            rejectsMalformedCompatibilityMetadata
-        , testCase "rejects a compatible incomplete schema"
-            rejectsCompatibleIncompleteSchema
-        , testCase "round-trips exact parsed artifacts"
-            roundTripsExactParsedArtifacts
-        , testCase "rejects malformed parsed payloads"
-            rejectsMalformedParsedPayloads
-        , testCase "rejects disagreeing parsed artifact identities"
-            rejectsDisagreeingParsedArtifactIdentities
-        , testCase "rejects malformed typed validation rows"
-            rejectsMalformedTypedValidationRows
-        , testCase "publishes a completed prefix before readiness"
-            publishesCompletedPrefixBeforeReadiness
-        , testCase "installs a sealed producer for a cached importer"
-            installsSealedProducerForCachedImporter
-        , testCase "validates exact cached installation inputs"
-            validatesExactCachedInstallationInputs
-        , testCase "rejects invalid cached root authority and closure"
-            rejectsInvalidCachedRootAuthorityAndClosure
-        , testCase "rejects disagreeing module artifact columns"
-            rejectsDisagreeingModuleArtifactColumns
-        , testCase "validates shared closures once per invocation"
-            validatesSharedClosuresOncePerInvocation
-        , testCase "rolls back a failed readiness transaction"
-            rollsBackFailedReadiness
-        , testCase "rolls back an unequal duplicate batch"
-            rollsBackUnequalDuplicateBatch
-        , testCase "rejects malformed canonical payloads"
-            rejectsMalformedCanonicalPayloads
-        , testCase "plans default and explicit persistent stores"
-            plansPersistentStores
-        , testCase "cleans fresh stores on return and exceptions"
-            cleansFreshStores
-        , testCase "does not fall back after fatal startup"
-            doesNotFallBackAfterFatalStartup
-        ]
-
-serializesCoordinatorAccess :: Assertion
-serializesCoordinatorAccess = do
-    coordinator <- Store.newStoreCoordinator
-    active <- IORef.newIORef (0 :: Int)
-    maximumActive <- IORef.newIORef (0 :: Int)
-    let operation =
-            Store.withStoreCoordinator coordinator
-                (Exception.bracket_
-                    (IORef.atomicModifyIORef' active
-                        (\current ->
-                            let next = current + 1
-                            in (next, ())))
-                    (IORef.atomicModifyIORef' active
-                        (\current -> (current - 1, ())))
-                    (do
-                        current <- IORef.readIORef active
-                        IORef.atomicModifyIORef' maximumActive
-                            (\observed -> (max current observed, ()))
-                        threadDelay 50000))
-    void (concurrently operation operation)
-    IORef.readIORef maximumActive >>= assertEqual "maximum owner count" 1
-
-roundTripsExactParsedArtifacts :: Assertion
-roundTripsExactParsedArtifacts =
-    withStoreFixture "felix-store-parsed" \path theory _fixture -> do
-        (_startup, store) <- expectOpen path theory
-        (key, artifact, unequal) <- makeParsedArtifacts
-        assertEqual "initial exact lookup misses" (Right Nothing)
-            =<< Store.loadParsedArtifact store key
-        assertEqual "published parsed artifact"
-            (Right artifact)
-            =<< Store.writeParsedArtifact store key artifact
-        assertEqual "exact parsed round trip"
-            (Right (Just artifact))
-            =<< Store.loadParsedArtifact store key
-        assertEqual "equal publication is idempotent"
-            (Right artifact)
-            =<< Store.writeParsedArtifact store key artifact
-        Store.writeParsedArtifact store key unequal >>= \case
-            Left Store.StoreRowPayloadMismatch{} ->
-                pure ()
-            other ->
-                assertFailure
-                    ("unexpected unequal parsed publication: " <> show other)
-        Store.closeStore store
-
-rejectsMalformedParsedPayloads :: Assertion
-rejectsMalformedParsedPayloads = do
-    check "malformed" (ByteString.singleton 0xff)
-    check "noncanonical" . (<> ByteString.singleton 0x00)
-        =<< parsedPayloadBytes
-  where
-    check label corrupted =
-        withStoreFixture ("felix-store-parsed-" <> label)
-            \path theory _fixture -> do
-                (_startup, store) <- expectOpen path theory
-                (key, artifact, _unequal) <- makeParsedArtifacts
-                _ <- expectRightIO
-                    (Store.writeParsedArtifact store key artifact)
-                Store.closeStore store
-                updateParsedPayload path key corrupted
-                (_reopened, current) <- expectOpen path theory
-                Store.loadParsedArtifact current key >>= \case
-                    Left Store.StoreRowDecodeFailure{} ->
-                        pure ()
-                    other ->
-                        assertFailure
-                            ("unexpected " <> label
-                                <> " parsed row result: " <> show other)
-                Store.closeStore current
-
-    parsedPayloadBytes = do
-        (_key, artifact, _unequal) <- makeParsedArtifacts
-        pure
-            (ParsedPayload.canonicalParsedPayloadBytes
-                (ParsedPayload.parsedArtifactPayload artifact))
-
-rejectsDisagreeingParsedArtifactIdentities :: Assertion
-rejectsDisagreeingParsedArtifactIdentities =
-    withStoreFixture "felix-store-parsed-id" \path theory _fixture -> do
-        (_startup, store) <- expectOpen path theory
-        (key, artifact, _unequal) <- makeParsedArtifacts
-        _ <- expectRightIO (Store.writeParsedArtifact store key artifact)
-        Store.closeStore store
-        connection <- SQLite.open path
-        SQLite.execute connection
-            "UPDATE parsed_artifacts SET parsed_module_id = ? \
-            \WHERE parsed_module_key = ?"
-            ( ByteString.replicate 32 0
-            , Cache.cacheDigestBytes (Parsed.parsedModuleKeyDigest key)
-            )
-        SQLite.close connection
-        (_reopened, current) <- expectOpen path theory
-        Store.loadParsedArtifact current key >>= \case
-            Left Store.StoreParsedArtifactIdMismatch ->
-                pure ()
-            other ->
-                assertFailure
-                    ("unexpected parsed identity result: " <> show other)
-        Store.closeStore current
-
-makeParsedArtifacts
-    :: IO
-        ( Parsed.ParsedModuleKey
-        , ParsedPayload.ParsedArtifact
-        , ParsedPayload.ParsedArtifact
-        )
-makeParsedArtifacts = do
-    key <- expectRight
-        (Parsed.parsedModuleKey
-            (Content.sourceContentIdBytes "parsed-source")
-            Syntax.baseSyntaxInterfaceId
-            [])
-    emptyDelta <- expectRight (Syntax.canonicalSyntaxDelta [])
-    emptySyntax <- expectRight (Syntax.moduleSyntaxInterface [] emptyDelta)
-    otherDelta <- expectRight
-        (Syntax.canonicalSyntaxDelta
-            [Syntax.CanonicalStructureOperation "other"])
-    otherSyntax <- expectRight
-        (Syntax.moduleSyntaxInterface [] otherDelta)
-    let payload syntax =
-            ParsedPayload.canonicalParsedPayload
-                [] [] [] (Syntax.moduleSyntaxAssertedId syntax)
-    pure
-        ( key
-        , ParsedPayload.parsedArtifact key (payload emptySyntax)
-        , ParsedPayload.parsedArtifact key (payload otherSyntax)
-        )
-
-updateParsedPayload
-    :: FilePath
-    -> Parsed.ParsedModuleKey
-    -> ByteString.ByteString
-    -> IO ()
-updateParsedPayload path key payload = do
-    connection <- SQLite.open path
-    SQLite.execute connection
-        "UPDATE parsed_artifacts SET payload = ? \
-        \WHERE parsed_module_key = ?"
-        ( payload
-        , Cache.cacheDigestBytes (Parsed.parsedModuleKeyDigest key)
-        )
-    SQLite.close connection
-
-rejectsMalformedTypedValidationRows :: Assertion
-rejectsMalformedTypedValidationRows =
-    withStoreFixture "felix-store-malformed-typed" \path theory fixture -> do
-        (_startup, store) <- expectOpen path theory
-        (_owner, prefix, _syntax, _semantic, _key, _artifact, _proposition) <-
-            makeCommittedModule theory fixture
-        batch <- case Declaration.pendingModulePrefixBatches prefix of
-            [one] -> pure one
-            batches ->
-                assertFailure
-                    ("unexpected prefix batch count: " <> show (length batches))
-                    >> fail "unreachable"
-        proof <- case Declaration.committedBatchProofValidations batch of
-            [one] -> pure one
-            proofs ->
-                assertFailure
-                    ("unexpected proof validation count: " <> show (length proofs))
-                    >> fail "unreachable"
-        let key = Semantic.proofValidationRecordKey proof
-            certificate = Semantic.proofValidationRecordCertificate proof
-            theorem = Identity.theoremId
-                (Authority.factAuthorityTheorem
-                    (Authority.validationTarget certificate))
-            wrongKey = Semantic.proofValidationKey
-                theorem
-                (Semantic.proofSyntaxId "other-row")
-                (Declaration.committedBatchPreviousPrefix batch)
-            wrongProof =
-                Semantic.proofValidationRecord wrongKey certificate
-        expectRightIO (Store.writePendingModulePrefix store prefix)
-        Store.closeStore store
-        connection <- SQLite.open path
-        SQLite.execute connection
-            "UPDATE proof_validations SET payload = ? \
-            \WHERE validation_key = ?"
-            ( Cache.encodeCache
-                (Semantic.putProofValidationRecordCache wrongProof)
-            , Cache.cacheDigestBytes
-                (Semantic.proofValidationKeyDigest key)
-            )
-        SQLite.close connection
-        (_reopened, current) <- expectOpen path theory
-        Store.loadProofValidation current key >>= \case
-            Left Store.StoreValidationRecordKeyMismatch{} -> pure ()
-            Left other ->
-                assertFailure
-                    ("unexpected typed key mismatch: " <> show other)
-            Right _ ->
-                assertFailure "typed key mismatch was accepted"
-        Store.closeStore current
-        connection' <- SQLite.open path
-        SQLite.execute connection'
-            "UPDATE proof_validations SET payload = ? \
-            \WHERE validation_key = ?"
-            ( ByteString.singleton 0xff
-            , Cache.cacheDigestBytes
-                (Semantic.proofValidationKeyDigest key)
-            )
-        SQLite.close connection'
-        (_reopenedMalformed, malformed) <- expectOpen path theory
-        Store.loadProofValidation malformed key >>= \case
-            Left Store.StoreRowDecodeFailure{} -> pure ()
-            Left other ->
-                assertFailure
-                    ("unexpected malformed typed row: " <> show other)
-            Right _ ->
-                assertFailure "malformed typed row was accepted"
-        Store.closeStore malformed
-
-publishesCompletedPrefixBeforeReadiness :: Assertion
-publishesCompletedPrefixBeforeReadiness =
-    withStoreFixture "felix-store-prefix" \path theory fixture -> do
-        (_startup, store) <- expectOpen path theory
-        (_owner, prefix, syntax, semantic, artifactKey, artifact, proposition) <-
-            makeCommittedModule theory fixture
-        expectRightIO (Store.writePendingModulePrefix store prefix)
-        connection <- SQLite.open path
-        [Only propositionRows] <- SQLite.query connection
-            "SELECT COUNT(*) FROM canonical_propositions \
-            \WHERE proposition_id = ?"
-            (Only
-                (Cache.encodeCache
-                    (Identity.putPropositionIdCache
-                        (Identity.checkedPropositionId proposition))))
-            :: IO [Only Int]
-        [Only artifactRowsBefore] <- SQLite.query_ connection
-            "SELECT COUNT(*) FROM module_artifacts"
-            :: IO [Only Int]
-        SQLite.close connection
-        assertEqual "completed prefix proposition is visible" 1 propositionRows
-        assertEqual "prefix publication does not publish readiness"
-            0 artifactRowsBefore
-        expectRightIO
-            (Store.writeSealedModule
-                store
-                prefix
-                [syntax]
-                [semantic]
-                artifact)
-        memo <- Store.newStoreMemo store
-        installation <- expectRightIO
-            (Store.loadCachedModuleInstallation
-                memo
-                store
-                artifactKey
-                (Syntax.moduleSyntaxAssertedId syntax))
-        case installation of
-            Just loaded -> do
-                assertEqual "validated semantic interface" semantic
-                    (Store.cachedInstallationSemantic loaded)
-                assertEqual "validated imported proposition count" 1
-                    (length (Store.cachedInstallationPropositions loaded))
-            Nothing ->
-                assertFailure "validated module installation was absent"
-        Store.closeStore store
-
-installsSealedProducerForCachedImporter :: Assertion
-installsSealedProducerForCachedImporter =
-    withStoreFixture "felix-store-cached-import" \path theory fixture -> do
-        (_startup, store) <- expectOpen path theory
-        foundation <- expectRight Foundation.checkedFoundation
-        (_owner, prefix, syntax, semantic, artifactKey, artifact, proposition) <-
-            makeCommittedModule theory fixture
-        expectRightIO
-            (Store.writeSealedModule
-                store
-                prefix
-                [syntax]
-                [semantic]
-                artifact)
-        memo <- Store.newStoreMemo store
-        installation <-
-            expectRightIO
-                (Store.loadCachedModuleInstallation
-                    memo
-                    store
-                    artifactKey
-                    (Syntax.moduleSyntaxAssertedId syntax))
-            >>= \case
-                Nothing ->
-                    assertFailure "sealed producer was not loadable"
-                        >> fail "unreachable"
-                Just loaded ->
-                    pure loaded
-        cached <- expectRight
-            (Typed.cachedSealedTypedModule
-                foundation
-                []
-                installation)
-        let loadedSemantic = Store.cachedInstallationSemantic installation
-        fingerprint <-
-            case concatMap
-                    Semantic.declarationDeltaFacts
-                    (Semantic.semanticInterfaceDeclarations loadedSemantic) of
-                [occurrence] ->
-                    pure (Semantic.semanticFactFingerprint occurrence)
-                occurrences ->
-                    assertFailure
-                        ("unexpected cached producer facts: "
-                            <> show (length occurrences))
-                        >> fail "unreachable"
-        namespaceDigest <- expectRight
-            (hashCanonicalFields
-                "store-cached-import-consumer"
-                ["consumer"])
-        relative <- expectRight (safeRelativePath "consumer.tex")
-        let consumerOwner =
-                moduleNameFromParts
-                    (sourceNamespaceIdFromDigest namespaceDigest)
-                    relative
-            resolver = Declaration.vampireResolver \_ ->
-                pure
-                    (Left
-                        (Provers.ProverLaunchFailed
-                            "unused"
-                            "cached importer does not run Vampire"))
-        result <-
-            (Declaration.runModuleDriver
-                foundation
-                consumerOwner
-                [Semantic.semanticInterfaceAssertedId loadedSemantic]
-                resolver
-                Declaration.FreshValidation
-                do
-                    Declaration.importSealedModuleDriver
-                        (Typed.sealedTypedModuleEvidence cached)
-                    (_value, batch) <- Declaration.commitProofDeclaration
-                        (Semantic.proofSyntaxId "cached-import-consumer") do
-                            candidate <- Declaration.reserveCandidate
-                                (Declaration.candidateSpec
-                                    proposition
-                                    Semantic.SearchIneligible
-                                    [])
-                            Declaration.authorizeOmittedCandidate candidate do
-                                _ <- Declaration.useAuthorizedFact fingerprint
-                                Declaration.recordOmittedUse
-                    pure batch
-                :: IO
-                    (Either
-                        Declaration.DriverOpenError
-                        (Declaration.DriverResult Text
-                            Declaration.CommittedDeclarationBatch)))
-        case result of
-            Left failure ->
-                assertFailure ("cached importer could not open: " <> show failure)
-            Right (Declaration.DriverSucceeded _ _ _ _closure) ->
-                pure ()
-            Right (Declaration.DriverFailed failure _prefix) ->
-                assertFailure ("cached importer failed: " <> show failure)
-            Right (Declaration.DriverSealFailed failure _prefix) ->
-                assertFailure ("cached importer did not seal: " <> show failure)
-        Store.closeStore store
-
-validatesExactCachedInstallationInputs :: Assertion
-validatesExactCachedInstallationInputs =
-    withStoreFixture "felix-store-exact-install" \path theory fixture -> do
-        (_startup, store) <- expectOpen path theory
-        (owner, prefix, syntax, semantic, artifactKey, artifact, proposition) <-
-            makeCommittedModule theory fixture
-        _ <- expectRightIO
-            (Store.writeSealedModule
-                store prefix [syntax] [semantic] artifact)
-        otherDelta <- expectRight
-            (Syntax.canonicalSyntaxDelta
-                [Syntax.CanonicalStructureOperation "other-syntax"])
-        otherSyntax <- expectRight
-            (Syntax.moduleSyntaxInterface [] otherDelta)
-        wrongSyntaxMemo <- Store.newStoreMemo store
-        Store.loadCachedModuleInstallation
-            wrongSyntaxMemo
-            store
-            artifactKey
-            (Syntax.moduleSyntaxAssertedId otherSyntax)
-            >>= \case
-                Left Store.StoreModuleArtifactSyntaxMismatch{} -> pure ()
-                _ ->
-                    assertFailure "unexpected syntax-input result"
-
-        parent <- expectRight
-            (Semantic.semanticInterface preludeModuleName [] [])
-        mismatched <- expectRight
-            (Semantic.semanticInterface
-                owner
-                [Semantic.semanticInterfaceAssertedId parent]
-                (Semantic.semanticInterfaceDeclarations semantic))
-        mismatchKey <- makeArtifactKey owner theory "direct-mismatch"
-        let mismatchArtifact =
-                Semantic.moduleArtifactResult
-                    mismatchKey
-                    (Syntax.moduleSyntaxAssertedId syntax)
-                    (Semantic.semanticInterfaceAssertedId mismatched)
-        writeRawModuleRows
-            path
-            [fixtureFirstObject fixture]
-            [proposition]
-            syntax
-            [parent, mismatched]
-            mismatchArtifact
-        directMemo <- Store.newStoreMemo store
-        Store.loadCachedModuleInstallation
-            directMemo
-            store
-            mismatchKey
-            (Syntax.moduleSyntaxAssertedId syntax)
-            >>= \case
-                Left Store.StoreModuleArtifactDirectMismatch{} -> pure ()
-                _ ->
-                    assertFailure "unexpected direct-input result"
-        Store.closeStore store
-
-rejectsInvalidCachedRootAuthorityAndClosure :: Assertion
-rejectsInvalidCachedRootAuthorityAndClosure =
-    withStoreFixture "felix-store-invalid-install" \path theory fixture -> do
-        (_startup, store) <- expectOpen path theory
-        (owner, _prefix, syntax, semantic, _artifactKey, _artifact, proposition) <-
-            makeCommittedModule theory fixture
-        otherTheory <- expectRight
-            (Cache.decodeCache
-                Identity.getTheoryIdCache
-                (ByteString.replicate 32 0x5a))
-        original <- case Semantic.semanticInterfaceDeclarations semantic of
-            [delta] -> pure delta
-            deltas ->
-                assertFailure
-                    ("unexpected declaration count: " <> show (length deltas))
-                    >> fail "unreachable"
-        occurrence <- case Semantic.declarationDeltaFacts original of
-            [fact] -> pure fact
-            facts ->
-                assertFailure
-                    ("unexpected fact count: " <> show (length facts))
-                    >> fail "unreachable"
-        let badAuthority =
-                Authority.factAuthority
-                    (Identity.theoremRef
-                        otherTheory
-                        (Semantic.semanticFactProposition occurrence))
-                    (Authority.factAuthoritySafety
-                        (Semantic.semanticFactAuthority occurrence))
-            badOccurrence =
-                Semantic.semanticFactOccurrence
-                    (Semantic.semanticFactSlot occurrence)
-                    badAuthority
-                    (Semantic.semanticFactSearchEligibility occurrence)
-        badDelta <- expectRight
-            (Semantic.declarationInterfaceDelta
-                (Semantic.declarationDeltaSlot original)
-                [badOccurrence]
-                (Semantic.declarationDeltaAliases original)
-                (Semantic.declarationDeltaObjects original)
-                (Semantic.declarationDeltaPropositions original)
-                (Semantic.declarationDeltaEnvironment original))
-        badSemantic <- expectRight
-            (Semantic.semanticInterface owner [] [badDelta])
-        badKey <- makeArtifactKey owner theory "bad-authority"
-        let badArtifact =
-                Semantic.moduleArtifactResult
-                    badKey
-                    (Syntax.moduleSyntaxAssertedId syntax)
-                    (Semantic.semanticInterfaceAssertedId badSemantic)
-        writeRawModuleRows
-            path
-            [fixtureFirstObject fixture]
-            [proposition]
-            syntax
-            [badSemantic]
-            badArtifact
-        badMemo <- Store.newStoreMemo store
-        Store.loadCachedModuleInstallation
-            badMemo store badKey (Syntax.moduleSyntaxAssertedId syntax)
-            >>= \case
-                Left Store.StoreImportedOccurrenceValidationFailure{} -> pure ()
-                _ ->
-                    assertFailure "unexpected root-authority result"
-
-        childKey <- makeArtifactKey owner theory "missing-late-child"
-        let childArtifact =
-                Semantic.moduleArtifactResult
-                    childKey
-                    (Syntax.moduleSyntaxAssertedId syntax)
-                    (Semantic.semanticInterfaceAssertedId semantic)
-        writeRawModuleRows
-            path
-            [fixtureFirstObject fixture]
-            [proposition]
-            syntax
-            [semantic]
-            childArtifact
-        connection <- SQLite.open path
-        SQLite.execute connection
-            "DELETE FROM canonical_objects WHERE object_id = ?"
-            (Only
-                (Cache.encodeCache
-                    (Identity.putObjectIdCache
-                        (Identity.assertedObjectId
-                            (fixtureFirstObject fixture)))))
-        SQLite.close connection
-        childMemo <- Store.newStoreMemo store
-        Store.loadCachedModuleInstallation
-            childMemo store childKey (Syntax.moduleSyntaxAssertedId syntax)
-            >>= \case
-                Left Store.StoreAssertedChildMissing{} -> pure ()
-                _ ->
-                    assertFailure "unexpected missing-child result"
-        Store.closeStore store
-
-rejectsDisagreeingModuleArtifactColumns :: Assertion
-rejectsDisagreeingModuleArtifactColumns =
-    withStoreFixture "felix-store-artifact-columns" \path theory fixture -> do
-        (_startup, store) <- expectOpen path theory
-        (_owner, prefix, syntax, semantic, key, artifact, _proposition) <-
-            makeCommittedModule theory fixture
-        _ <- expectRightIO
-            (Store.writeSealedModule
-                store prefix [syntax] [semantic] artifact)
-        connection <- SQLite.open path
-        SQLite.execute_ connection "PRAGMA foreign_keys = OFF"
-        SQLite.execute connection
-            "UPDATE module_artifacts SET syntax_interface_id = ? \
-            \WHERE module_artifact_id = ?"
-            ( ByteString.replicate 32 0x3c
-            , Cache.cacheDigestBytes
-                (Semantic.moduleArtifactIdDigest
-                    (Semantic.moduleArtifactResultId artifact))
-            )
-        SQLite.close connection
-        memo <- Store.newStoreMemo store
-        Store.loadCachedModuleInstallation
-            memo
-            store
-            key
-            (Syntax.moduleSyntaxAssertedId syntax)
-            >>= \case
-                Left Store.StoreModuleArtifactColumnsMismatch -> pure ()
-                Left other ->
-                    assertFailure
-                        ("unexpected artifact-column load: " <> show other)
-                Right _ ->
-                    assertFailure "disagreeing artifact columns were accepted"
-        Store.writeSealedModule
-            store prefix [syntax] [semantic] artifact >>= \case
-            Left Store.StoreRowPayloadMismatch{} -> pure ()
-            other ->
-                assertFailure
-                    ("unexpected artifact-column rewrite: " <> show other)
-        Store.closeStore store
-
-validatesSharedClosuresOncePerInvocation :: Assertion
-validatesSharedClosuresOncePerInvocation =
-    withStoreFixture "felix-store-linear-closure" \path theory fixture -> do
-        (_startup, store) <- expectOpen path theory
-        let baseObject = fixtureFirstObject fixture
-            first = transparentSetObject theory baseObject
-            second = transparentSetObject theory first
-            third = transparentSetObject theory second
-            objects = [baseObject, first, second, third]
-        closure <- expectRight
-            (Identity.validateObjectClosure theory objects)
-        proposition <- expectRight
-            (Identity.validatePropositionContent
-                closure
-                (Core.CEq
-                    Core.TySet
-                    (Core.CGlobal (Identity.assertedObjectId third))
-                    (Core.CGlobal (Identity.assertedObjectId third))))
-        baseOwner <- testModuleName "linear-base.tex"
-        leftOwner <- testModuleName "linear-left.tex"
-        rightOwner <- testModuleName "linear-right.tex"
-        rootOwner <- testModuleName "linear-root.tex"
-        let theorem = Identity.theoremRef
-                theory
-                (Identity.checkedPropositionId proposition)
-            occurrence = Semantic.semanticFactOccurrence
-                (Semantic.factSlot baseOwner (localFactOrdinal 0))
-                (Authority.factAuthority
-                    theorem Authority.cleanAuthoritySafety)
-                Semantic.SearchEligible
-        baseDelta <- expectRight
-            (Semantic.declarationInterfaceDelta
-                (Semantic.declarationSlot
-                    baseOwner
-                    (localDeclarationOrdinal 0))
-                [occurrence]
-                []
-                (Identity.assertedObjectId <$> objects)
-                [Identity.checkedPropositionId proposition]
-                Semantic.emptySemanticEnvironmentDelta)
-        baseSemantic <- expectRight
-            (Semantic.semanticInterface baseOwner [] [baseDelta])
-        leftSemantic <- expectRight
-            (Semantic.semanticInterface
-                leftOwner
-                [Semantic.semanticInterfaceAssertedId baseSemantic]
-                [])
-        rightSemantic <- expectRight
-            (Semantic.semanticInterface
-                rightOwner
-                [Semantic.semanticInterfaceAssertedId baseSemantic]
-                [])
-        rootSemantic <- expectRight
-            (Semantic.semanticInterface
-                rootOwner
-                [ Semantic.semanticInterfaceAssertedId leftSemantic
-                , Semantic.semanticInterfaceAssertedId rightSemantic
-                ]
-                [])
-
-        emptyDelta <- expectRight (Syntax.canonicalSyntaxDelta [])
-        leftDelta <- expectRight
-            (Syntax.canonicalSyntaxDelta
-                [Syntax.CanonicalStructureOperation "linear-left"])
-        rightDelta <- expectRight
-            (Syntax.canonicalSyntaxDelta
-                [Syntax.CanonicalStructureOperation "linear-right"])
-        baseSyntax <- expectRight
-            (Syntax.moduleSyntaxInterface [] emptyDelta)
-        leftSyntax <- expectRight
-            (Syntax.moduleSyntaxInterface
-                [Syntax.moduleSyntaxAssertedId baseSyntax]
-                leftDelta)
-        rightSyntax <- expectRight
-            (Syntax.moduleSyntaxInterface
-                [Syntax.moduleSyntaxAssertedId baseSyntax]
-                rightDelta)
-        rootSyntax <- expectRight
-            (Syntax.moduleSyntaxInterface
-                [ Syntax.moduleSyntaxAssertedId leftSyntax
-                , Syntax.moduleSyntaxAssertedId rightSyntax
-                ]
-                emptyDelta)
-
-        rootKey <- makeArtifactKeyWithDirect
-            rootOwner
-            theory
-            [ Semantic.semanticInterfaceAssertedId leftSemantic
-            , Semantic.semanticInterfaceAssertedId rightSemantic
-            ]
-            "linear-root"
-        leftKey <- makeArtifactKeyWithDirect
-            leftOwner
-            theory
-            [Semantic.semanticInterfaceAssertedId baseSemantic]
-            "linear-left"
-        let rootArtifact = Semantic.moduleArtifactResult
-                rootKey
-                (Syntax.moduleSyntaxAssertedId rootSyntax)
-                (Semantic.semanticInterfaceAssertedId rootSemantic)
-            leftArtifact = Semantic.moduleArtifactResult
-                leftKey
-                (Syntax.moduleSyntaxAssertedId leftSyntax)
-                (Semantic.semanticInterfaceAssertedId leftSemantic)
-        connection <- SQLite.open path
-        SQLite.withTransaction connection do
-            traverse_ (insertRawObject connection) objects
-            insertRawProposition connection proposition
-            traverse_
-                (insertRawSyntaxInterface connection)
-                [baseSyntax, leftSyntax, rightSyntax, rootSyntax]
-            traverse_
-                (insertRawSemanticInterface connection)
-                [baseSemantic, leftSemantic, rightSemantic, rootSemantic]
-            insertRawModuleArtifact connection rootArtifact
-            insertRawModuleArtifact connection leftArtifact
-        SQLite.close connection
-
-        memo <- Store.newStoreMemo store
-        expectInstallation memo store rootKey rootSyntax
-        expectInstallation memo store leftKey leftSyntax
-        expectInstallation memo store rootKey rootSyntax
-        visits <- Store.storeMemoVisits memo
-        assertEqual "unique artifact rows" 2
-            (Store.storeArtifactRowsDecoded visits)
-        assertEqual "unique artifact validations" 2
-            (Store.storeArtifactsValidated visits)
-        assertEqual "syntax diamond rows" 4
-            (Store.storeSyntaxRowsDecoded visits)
-        assertEqual "syntax diamond validations" 4
-            (Store.storeSyntaxRowsValidated visits)
-        assertEqual "semantic diamond rows" 4
-            (Store.storeSemanticRowsDecoded visits)
-        assertEqual "semantic diamond validations" 4
-            (Store.storeSemanticRowsValidated visits)
-        assertEqual "transparent-chain rows" 4
-            (Store.storeObjectRowsDecoded visits)
-        assertEqual "transparent-chain validations" 4
-            (Store.storeObjectRowsValidated visits)
-        assertEqual "proposition rows" 1
-            (Store.storePropositionRowsDecoded visits)
-        assertEqual "proposition validations" 1
-            (Store.storePropositionRowsValidated visits)
-        Store.closeStore store
-  where
-    expectInstallation memo store key syntax =
-        Store.loadCachedModuleInstallation
-            memo store key (Syntax.moduleSyntaxAssertedId syntax)
-            >>= \case
-                Right (Just _installation) -> pure ()
-                _ -> assertFailure "cached closure installation failed"
-
-transparentSetObject
-    :: Identity.TheoryId
-    -> Identity.AssertedObject
-    -> Identity.AssertedObject
-transparentSetObject theory dependency =
-    Identity.assertedObject identity content
-  where
-    content = Identity.TransparentObjectContent
-        theory
-        Core.TySet
-        (Core.CGlobal (Identity.assertedObjectId dependency))
-    identity = Identity.transparentObjectId
-        theory
-        Core.TySet
-        (Core.CGlobal (Identity.assertedObjectId dependency))
-
-testModuleName :: FilePath -> IO ModuleName
-testModuleName path = do
-    digest <- expectRight
-        (hashCanonicalFields
-            "store-linear-module"
-            [ByteString.Char8.pack path])
-    relative <- expectRight (safeRelativePath path)
-    pure
-        (moduleNameFromParts
-            (sourceNamespaceIdFromDigest digest)
-            relative)
-
-makeArtifactKey
-    :: ModuleName
-    -> Identity.TheoryId
-    -> ByteString.ByteString
-    -> IO Semantic.ModuleArtifactKey
-makeArtifactKey owner theory label = do
-    makeArtifactKeyWithDirect owner theory [] label
-
-makeArtifactKeyWithDirect
-    :: ModuleName
-    -> Identity.TheoryId
-    -> [Semantic.SemanticInterfaceId]
-    -> ByteString.ByteString
-    -> IO Semantic.ModuleArtifactKey
-makeArtifactKeyWithDirect owner theory direct label = do
-    parsedKey <- expectRight
-        (Parsed.parsedModuleKey
-            (Content.sourceContentIdBytes label)
-            Syntax.baseSyntaxInterfaceId
-            [])
-    expectRight
-        (Semantic.moduleArtifactKey
-            owner
-            (Parsed.parsedModuleId parsedKey label)
-            direct
-            theory)
-
-writeRawModuleRows
-    :: FilePath
-    -> [Identity.AssertedObject]
-    -> [Identity.CheckedPropositionContent]
-    -> Syntax.ModuleSyntaxInterface
-    -> [Semantic.SemanticInterface]
-    -> Semantic.ModuleArtifactResult
-    -> IO ()
-writeRawModuleRows path objects propositions syntax semantics artifact = do
-    connection <- SQLite.open path
-    SQLite.withTransaction connection do
-        traverse_ (insertRawObject connection) objects
-        traverse_ (insertRawProposition connection) propositions
-        insertRawSyntaxInterface connection syntax
-        traverse_ (insertRawSemanticInterface connection) semantics
-        insertRawModuleArtifact connection artifact
-    SQLite.close connection
-
-insertRawObject :: SQLite.Connection -> Identity.AssertedObject -> IO ()
-insertRawObject connection object =
-    SQLite.execute connection
-        "INSERT OR IGNORE INTO canonical_objects (object_id, payload) \
-        \VALUES (?, ?)"
-        ( Cache.encodeCache
-            (Identity.putObjectIdCache
-                (Identity.assertedObjectId object))
-        , Cache.encodeCache
-            (Identity.putObjectContentCache
-                (Identity.assertedObjectContent object))
-        )
-
-insertRawProposition
-    :: SQLite.Connection
-    -> Identity.CheckedPropositionContent
-    -> IO ()
-insertRawProposition connection proposition =
-    SQLite.execute connection
-        "INSERT OR IGNORE INTO canonical_propositions \
-        \(proposition_id, payload) VALUES (?, ?)"
-        ( Cache.encodeCache
-            (Identity.putPropositionIdCache
-                (Identity.checkedPropositionId proposition))
-        , Cache.encodeCache
-            (Cache.putCanonicalTermCache
-                Identity.putObjectIdCache
-                (Core.frozenCoreTerm
-                    (Identity.checkedPropositionTerm proposition)))
-        )
-
-insertRawSyntaxInterface
-    :: SQLite.Connection
-    -> Syntax.ModuleSyntaxInterface
-    -> IO ()
-insertRawSyntaxInterface connection interface =
-    SQLite.execute connection
-        "INSERT OR IGNORE INTO syntax_interfaces \
-        \(syntax_interface_id, payload) VALUES (?, ?)"
-        ( Cache.cacheDigestBytes
-            (Syntax.syntaxInterfaceIdDigest
-                (Syntax.moduleSyntaxAssertedId interface))
-        , Cache.encodeCache
-            (Syntax.putModuleSyntaxInterfaceCache interface)
-        )
-
-insertRawSemanticInterface
-    :: SQLite.Connection
-    -> Semantic.SemanticInterface
-    -> IO ()
-insertRawSemanticInterface connection interface =
-    SQLite.execute connection
-        "INSERT OR IGNORE INTO semantic_interfaces \
-        \(semantic_interface_id, payload) VALUES (?, ?)"
-        ( Cache.cacheDigestBytes
-            (Semantic.semanticInterfaceIdDigest
-                (Semantic.semanticInterfaceAssertedId interface))
-        , Cache.encodeCache
-            (Semantic.putSemanticInterfaceCache interface)
-        )
-
-insertRawModuleArtifact
-    :: SQLite.Connection
-    -> Semantic.ModuleArtifactResult
-    -> IO ()
-insertRawModuleArtifact connection artifact =
-    SQLite.execute connection
-        "INSERT OR IGNORE INTO module_artifacts \
-        \(module_artifact_id, syntax_interface_id, \
-        \semantic_interface_id, payload) VALUES (?, ?, ?, ?)"
-        ( Cache.cacheDigestBytes
-            (Semantic.moduleArtifactIdDigest
-                (Semantic.moduleArtifactResultId artifact))
-        , Cache.cacheDigestBytes
-            (Syntax.syntaxInterfaceIdDigest
-                (Semantic.moduleArtifactResultSyntax artifact))
-        , Cache.cacheDigestBytes
-            (Semantic.semanticInterfaceIdDigest
-                (Semantic.moduleArtifactResultSemantic artifact))
-        , Cache.encodeCache
-            (Semantic.putModuleArtifactResultCache artifact)
-        )
-
-storedPropositionCount
-    :: FilePath
-    -> Identity.PropositionId
-    -> IO Int
-storedPropositionCount path identity = do
-    connection <- SQLite.open path
-    [Only rowCount] <- SQLite.query connection
-        "SELECT COUNT(*) FROM canonical_propositions \
-        \WHERE proposition_id = ?"
-        (Only
-            (Cache.encodeCache
-                (Identity.putPropositionIdCache identity)))
-    SQLite.close connection
-    pure rowCount
-
-storedObjectCount
-    :: FilePath
-    -> Identity.ObjectId
-    -> IO Int
-storedObjectCount path identity = do
-    connection <- SQLite.open path
-    [Only rowCount] <- SQLite.query connection
-        "SELECT COUNT(*) FROM canonical_objects WHERE object_id = ?"
-        (Only
-            (Cache.encodeCache
-                (Identity.putObjectIdCache identity)))
-    SQLite.close connection
-    pure rowCount
-
-storedArtifactCount
-    :: FilePath
-    -> Semantic.ModuleArtifactId
-    -> IO Int
-storedArtifactCount path identity = do
-    connection <- SQLite.open path
-    [Only rowCount] <- SQLite.query connection
-        "SELECT COUNT(*) FROM module_artifacts \
-        \WHERE module_artifact_id = ?"
-        (Only
-            (Cache.cacheDigestBytes
-                (Semantic.moduleArtifactIdDigest identity)))
-    SQLite.close connection
-    pure rowCount
-
-rollsBackFailedReadiness :: Assertion
-rollsBackFailedReadiness =
-    withStoreFixture "felix-store-readiness-rollback" \path theory fixture -> do
-        (_startup, store) <- expectOpen path theory
-        (owner, prefix, _syntax, semantic, _artifactKey, artifact, proposition) <-
-            makeCommittedModule theory fixture
-        missingDelta <- expectRight
-            (Syntax.canonicalSyntaxDelta
-                [Syntax.CanonicalStructureOperation "missing-child"])
-        missingInterface <- expectRight
-            (Syntax.moduleSyntaxInterface [] missingDelta)
-        syntaxDelta <- expectRight
-            (Syntax.canonicalSyntaxDelta [])
-        brokenSyntax <- expectRight
-            (Syntax.moduleSyntaxInterface
-                [Syntax.moduleSyntaxAssertedId missingInterface]
-                syntaxDelta)
-        brokenParsedKey <- expectRight
-            (Parsed.parsedModuleKey
-                (Content.sourceContentIdBytes "rollback-source")
-                Syntax.baseSyntaxInterfaceId
-                [])
-        brokenArtifactKey <- expectRight
-            (Semantic.moduleArtifactKey
-                owner
-                (Parsed.parsedModuleId
-                    brokenParsedKey
-                    "rollback-parsed")
-                []
-                theory)
-        let brokenArtifact =
-                Semantic.moduleArtifactResult
-                    brokenArtifactKey
-                    (Syntax.moduleSyntaxAssertedId brokenSyntax)
-                    (Semantic.semanticInterfaceAssertedId semantic)
-        result <- Store.writeSealedModule
-            store
-            prefix
-            [brokenSyntax]
-            [semantic]
-            brokenArtifact
-        case result of
-            Left Store.StoreAssertedChildMissing{} ->
-                pure ()
-            Left other ->
-                assertFailure
-                    ("unexpected readiness failure: " <> show other)
-            Right _ ->
-                assertFailure "broken readiness transaction was accepted"
-        assertEqual "failed readiness did not publish the prefix" 0
-            =<< storedPropositionCount
-                path
-                (Identity.checkedPropositionId proposition)
-        assertEqual "failed readiness leaves no module root" 0
-            =<< storedArtifactCount
-                path
-                (Semantic.moduleArtifactResultId artifact)
-        -- A later failed seal must not erase a prefix published by an
-        -- earlier successful source prefix flush.
-        expectRightIO (Store.writePendingModulePrefix store prefix)
-        assertEqual "successful prefix is visible before retry" 1
-            =<< storedPropositionCount
-                path
-                (Identity.checkedPropositionId proposition)
-        retry <- Store.writeSealedModule
-            store
-            prefix
-            [brokenSyntax]
-            [semantic]
-            brokenArtifact
-        case retry of
-            Left Store.StoreAssertedChildMissing{} ->
-                pure ()
-            Left other ->
-                assertFailure
-                    ("unexpected retry readiness failure: " <> show other)
-            Right _ ->
-                assertFailure "broken readiness retry was accepted"
-        assertEqual "failed retry retains successful prefix" 1
-            =<< storedPropositionCount
-                path
-                (Identity.checkedPropositionId proposition)
-        assertEqual "failed retry still leaves no module root" 0
-            =<< storedArtifactCount
-                path
-                (Semantic.moduleArtifactResultId artifact)
-        Store.closeStore store
-makeCommittedModule
-    :: Identity.TheoryId
-    -> StoreFixture
-    -> IO
-        ( ModuleName
-        , Declaration.PendingModulePrefix
-        , Syntax.ModuleSyntaxInterface
-        , Semantic.SemanticInterface
-        , Semantic.ModuleArtifactKey
-        , Semantic.ModuleArtifactResult
-        , Identity.CheckedPropositionContent
-        )
-makeCommittedModule theory fixture = do
-    foundation <- expectRight Foundation.checkedFoundation
-    namespaceDigest <- expectRight
-        (hashCanonicalFields "store-module-test" ["prefix"])
-    relative <- expectRight (safeRelativePath "module.tex")
-    let owner =
-            moduleNameFromParts
-                (sourceNamespaceIdFromDigest namespaceDigest)
-                relative
-        proposition = fixtureProposition fixture
-        resolver = Declaration.vampireResolver \_ ->
-            pure
-                (Left
-                    (Provers.ProverLaunchFailed
-                        "unused"
-                        "store fixture does not run Vampire"))
-    driver <- Declaration.runModuleDriver
-        foundation
-        owner
-        []
-        resolver
-        Declaration.FreshValidation
-        do
-            (_value, _batch) <- Declaration.commitProofDeclaration
-                (Semantic.proofSyntaxId "store-prefix") do
-                    Declaration.addDeclarationObject
-                        (fixtureFirstObject fixture)
-                    candidate <- Declaration.reserveCandidate
-                        (Declaration.candidateSpec
-                            proposition
-                            Semantic.SearchIneligible
-                            [])
-                    Declaration.authorizeOmittedCandidate candidate
-                        Declaration.recordOmittedUse
-            pure ()
-    (_value, prefix, semantic) <-
-        case driver of
-            Right (Declaration.DriverSucceeded value interface pending _closure) ->
-                pure (value, pending, interface)
-            Right (Declaration.DriverFailed failure _prefix) ->
-                assertFailure
-                    ("unexpected declaration failure: "
-                        <> show
-                            (failure
-                                :: Declaration.DriverFailure
-                                    Declaration.DeclarationError))
-                    >> fail "unreachable"
-            Right (Declaration.DriverSealFailed failure _prefix) ->
-                assertFailure ("unexpected seal failure: " <> show failure)
-                    >> fail "unreachable"
-            Left failure ->
-                assertFailure ("unexpected driver-open failure: " <> show failure)
-                    >> fail "unreachable"
-    delta <- expectRight (Syntax.canonicalSyntaxDelta [])
-    syntax <- expectRight (Syntax.moduleSyntaxInterface [] delta)
-    parsedKey <- expectRight
-        (Parsed.parsedModuleKey
-            (Content.sourceContentIdBytes "store-module-source")
-            Syntax.baseSyntaxInterfaceId
-            [])
-    artifactKey <- expectRight
-        (Semantic.moduleArtifactKey
-            owner
-            (Parsed.parsedModuleId parsedKey "store-module-parsed")
-            []
-            theory)
-    let artifact =
-            Semantic.moduleArtifactResult
-                artifactKey
-                (Syntax.moduleSyntaxAssertedId syntax)
-                (Semantic.semanticInterfaceAssertedId semantic)
-    pure
-        ( owner
-        , prefix
-        , syntax
-        , semantic
-        , artifactKey
-        , artifact
-        , proposition
-        )
-
-makePendingPrefix
-    :: StoreFixture
-    -> [Identity.AssertedObject]
-    -> IO Declaration.PendingModulePrefix
-makePendingPrefix fixture objects = do
-    foundation <- expectRight Foundation.checkedFoundation
-    owner <- testModuleName "rollback-prefix.tex"
-    let proposition = fixtureProposition fixture
-        resolver = Declaration.vampireResolver \_ ->
-            pure
-                (Left
-                    (Provers.ProverLaunchFailed
-                        "unused"
-                        "store fixture does not run Vampire"))
-    driver <- Declaration.runModuleDriver
-        foundation
-        owner
-        []
-        resolver
-        Declaration.FreshValidation
-        do
-            (_value, _batch) <- Declaration.commitProofDeclaration
-                (Semantic.proofSyntaxId "store-rollback") do
-                    traverse_ Declaration.addDeclarationObject objects
-                    candidate <- Declaration.reserveCandidate
-                        (Declaration.candidateSpec
-                            proposition
-                            Semantic.SearchIneligible
-                            [])
-                    Declaration.authorizeOmittedCandidate candidate
-                        Declaration.recordOmittedUse
-            pure ()
-    case driver of
-        Right (Declaration.DriverSucceeded _value _interface prefix _closure) ->
-            pure prefix
-        Right (Declaration.DriverFailed failure _prefix) ->
-            assertFailure
-                ("unexpected declaration failure: "
-                    <> show
-                        (failure
-                            :: Declaration.DriverFailure
-                                Declaration.DeclarationError))
-                >> fail "unreachable"
-        Right (Declaration.DriverSealFailed failure _prefix) ->
-            assertFailure ("unexpected seal failure: " <> show failure)
-                >> fail "unreachable"
-        Left failure ->
-            assertFailure ("unexpected driver-open failure: " <> show failure)
-                >> fail "unreachable"
-
-initializesAndReopensCurrentSchema :: Assertion
-initializesAndReopensCurrentSchema =
-    withStoreFixture "felix-store-startup" \path theory _fixture -> do
-        (startup, store) <- expectOpen path theory
-        assertEqual "new store status"
-            Store.InitializedNewStore startup
-        Store.closeStore store
-
-        (reopened, current) <- expectOpen path theory
-        assertEqual "current store status"
-            Store.OpenedCurrentStore reopened
-        Store.closeStore current
-
-        connection <- SQLite.open path
-        names <- SQLite.query_ connection
-            "SELECT name FROM sqlite_master \
-            \WHERE type = 'table' AND name NOT LIKE 'sqlite_%' \
-            \ORDER BY name"
-            :: IO [Only Text]
-        journal <- SQLite.query_ connection
-            "PRAGMA journal_mode"
-            :: IO [Only Text]
-        SQLite.close connection
-        assertEqual "complete schema table count" 9 (length names)
-        assertEqual "rollback journal persists"
-            [Only "delete"] journal
-
-rejectsIncompatibilityWithoutConfiguration :: Assertion
-rejectsIncompatibilityWithoutConfiguration =
-    withStoreFixture "felix-store-incompatible" \path theory _fixture -> do
-        connection <- SQLite.open path
-        _ <- SQLite.query_ connection
-            "PRAGMA journal_mode = WAL"
-            :: IO [Only Text]
-        SQLite.execute_ connection
-            "CREATE TABLE store_compatibility ( \
-            \singleton INTEGER, cache_epoch INTEGER, theory_id BLOB )"
-        SQLite.execute connection
-            "INSERT INTO store_compatibility VALUES (1, ?, ?)"
-            ( 999 :: Int
-            , Cache.encodeCache (Identity.putTheoryIdCache theory)
-            )
-        SQLite.execute_ connection
-            "CREATE TABLE untouched (value INTEGER)"
-        SQLite.close connection
-
-        result <- Store.openStore path theory
-        case result of
-            Left
-                (Store.IncompatibleStore
-                    Store.StoreCompatibilityMismatch{}) ->
-                pure ()
-            Left other ->
-                assertFailure
-                    ("unexpected incompatibility result: " <> show other)
-            Right (_startup, store) -> do
-                Store.closeStore store
-                assertFailure "incompatible store was accepted"
-
-        inspected <- SQLite.open path
-        names <- SQLite.query_ inspected
-            "SELECT name FROM sqlite_master \
-            \WHERE type = 'table' AND name NOT LIKE 'sqlite_%' \
-            \ORDER BY name"
-            :: IO [Only Text]
-        journal <- SQLite.query_ inspected
-            "PRAGMA journal_mode"
-            :: IO [Only Text]
-        SQLite.close inspected
-        assertEqual "startup creates no schema"
-            [Only "store_compatibility", Only "untouched"] names
-        assertEqual "startup applies no journal configuration"
-            [Only "wal"] journal
-
-rejectsMalformedCompatibilityMetadata :: Assertion
-rejectsMalformedCompatibilityMetadata =
-    withStoreFixture "felix-store-malformed" \path theory _fixture -> do
-        connection <- SQLite.open path
-        SQLite.execute_ connection
-            "CREATE TABLE store_compatibility ( \
-            \singleton INTEGER, cache_epoch, theory_id )"
-        SQLite.execute connection
-            "INSERT INTO store_compatibility VALUES (1, ?, ?)"
-            ( "not-an-epoch" :: Text
-            , Cache.encodeCache (Identity.putTheoryIdCache theory)
-            )
-        SQLite.close connection
-
-        result <- Store.openStore path theory
-        case result of
-            Left
-                (Store.IncompatibleStore
-                    Store.StoreCompatibilityMalformed{}) ->
-                pure ()
-            Left other ->
-                assertFailure
-                    ("unexpected malformed result: " <> show other)
-            Right (_startup, store) -> do
-                Store.closeStore store
-                assertFailure "malformed metadata was accepted"
-
-rejectsCompatibleIncompleteSchema :: Assertion
-rejectsCompatibleIncompleteSchema =
-    withStoreFixture "felix-store-incomplete" \path theory _fixture -> do
-        (_startup, store) <- expectOpen path theory
-        Store.closeStore store
-        connection <- SQLite.open path
-        SQLite.execute_ connection
-            "DROP TABLE canonical_propositions"
-        SQLite.close connection
-
-        result <- Store.openStore path theory
-        case result of
-            Left
-                (Store.FatalStoreStartup
-                    Store.StoreSchemaIntegrityFailure{}) ->
-                pure ()
-            Left other ->
-                assertFailure
-                    ("unexpected incomplete-schema result: " <> show other)
-            Right (_startup, current) -> do
-                Store.closeStore current
-                assertFailure "incomplete current schema was accepted"
-
-rollsBackUnequalDuplicateBatch :: Assertion
-rollsBackUnequalDuplicateBatch =
-    withStoreFixture "felix-store-rollback" \path theory fixture -> do
-        (_startup, store) <- expectOpen path theory
-        let first = fixtureFirstObject fixture
-            second = fixtureSecondObject fixture
-        prefix <- makePendingPrefix fixture [first, second]
-        Store.closeStore store
-
-        connection <- SQLite.open path
-        SQLite.execute connection
-            "INSERT INTO canonical_objects (object_id, payload) VALUES (?, ?)"
-            ( Cache.encodeCache
-                (Identity.putObjectIdCache
-                    (Identity.assertedObjectId second))
-            , Cache.encodeCache
-                (Identity.putObjectContentCache
-                    (Identity.assertedObjectContent
-                        first))
-            )
-        SQLite.close connection
-
-        (_reopened, current) <- expectOpen path theory
-        result <- Store.writePendingModulePrefix current prefix
-        case result of
-            Left Store.StoreRowPayloadMismatch{} ->
-                pure ()
-            Left other ->
-                assertFailure
-                    ("unexpected duplicate result: " <> show other)
-            Right () ->
-                assertFailure "unequal duplicate was accepted"
-        assertEqual "earlier insertion was rolled back" 0
-            =<< storedObjectCount path (Identity.assertedObjectId first)
-        Store.closeStore current
-
-rejectsMalformedCanonicalPayloads :: Assertion
-rejectsMalformedCanonicalPayloads =
-    withStoreFixture "felix-store-decode" \path theory fixture -> do
-        (_startup, store) <- expectOpen path theory
-        let object = fixtureFirstObject fixture
-        (_owner, prefix, syntax, semantic, key, artifact, _proposition) <-
-            makeCommittedModule theory fixture
-        expectRightIO
-            (Store.writeSealedModule
-                store prefix [syntax] [semantic] artifact)
-        Store.closeStore store
-
-        connection <- SQLite.open path
-        SQLite.execute connection
-            "UPDATE canonical_objects SET payload = ? \
-            \WHERE object_id = ?"
-            ( ByteString.singleton 0xff
-            , Cache.encodeCache
-                (Identity.putObjectIdCache
-                    (Identity.assertedObjectId object))
-            )
-        SQLite.close connection
-
-        (_reopened, current) <- expectOpen path theory
-        memo <- Store.newStoreMemo current
-        result <- Store.loadCachedModuleInstallation
-            memo current key (Syntax.moduleSyntaxAssertedId syntax)
-        case result of
-            Left Store.StoreRowDecodeFailure{} ->
-                pure ()
-            Left other ->
-                assertFailure
-                    ("unexpected malformed-row result: " <> show other)
-            Right _ ->
-                assertFailure "malformed canonical payload was accepted"
-        Store.closeStore current
-
-plansPersistentStores :: Assertion
-plansPersistentStores =
-    Temp.withSystemTempDirectory "felix-store-planning" \root -> do
-        (theory, _fixture) <- makeStoreFixture
-        let cacheRoot = root Posix.</> "cache"
-            expectedDefault =
-                cacheRoot Posix.</> "felix" Posix.</> "store.sqlite"
-            explicitParent = root Posix.</> "explicit"
-            explicitPath = explicitParent Posix.</> "selected.sqlite"
-        Directory.createDirectory cacheRoot
-        Directory.createDirectory explicitParent
-        withEnvironment "XDG_CACHE_HOME" cacheRoot do
-            defaultPlan <- expectRightIO
-                (Store.planStore Store.DefaultStore)
-            defaultResult <- Store.withStoreLease defaultPlan \lease -> do
-                assertEqual "default store path"
-                    expectedDefault
-                    (Store.storePathFilePath
-                        (Store.storeLeasePath lease))
-                assertBool "planning does not create the default parent"
-                    . not
-                    =<< Directory.doesPathExist
-                        (cacheRoot Posix.</> "felix")
-                Store.withOpenStore lease theory \_startup _store ->
-                    Directory.doesFileExist expectedDefault
-            assertEqual "default store opens at the XDG path"
-                (Right True) defaultResult
-
-        explicitPlan <- expectRightIO
-            (Store.planStore
-                (Store.ExplicitStore explicitPath))
-        explicitResult <- Store.withStoreLease explicitPlan \lease -> do
-            assertEqual "explicit store path"
-                explicitPath
-                (Store.storePathFilePath
-                    (Store.storeLeasePath lease))
-            Store.withOpenStore lease theory \_startup _store ->
-                Directory.doesFileExist explicitPath
-        assertEqual "explicit store opens without creating its parent"
-            (Right True) explicitResult
-
-        missing <- Store.planStore
-            (Store.ExplicitStore
-                (root Posix.</> "missing" Posix.</> "store.sqlite"))
-        case missing of
-            Left Store.ExplicitStoreParentMissing{} ->
-                pure ()
-            Left other ->
-                assertFailure
-                    ("unexpected missing-parent result: " <> show other)
-            Right _ ->
-                assertFailure "missing explicit parent was accepted"
-
-cleansFreshStores :: Assertion
-cleansFreshStores = do
-    (theory, _fixture) <- makeStoreFixture
-    plan <- expectRightIO
-        (Store.planStore Store.FreshTemporaryStore)
-
-    successPath <- IORef.newIORef Nothing
-    success <- Store.withStoreLease plan \lease -> do
-        let path = Store.storePathFilePath
-                (Store.storeLeasePath lease)
-        IORef.writeIORef successPath (Just path)
-        Store.withOpenStore lease theory \_startup _store ->
-            Directory.doesFileExist path
-    assertEqual "fresh store opened" (Right True) success
-    assertFreshRemoved successPath
-
-    failurePath <- IORef.newIORef Nothing
-    failed <- Exception.try
-        (Store.withStoreLease plan \lease -> do
-            let path = Store.storePathFilePath
-                    (Store.storeLeasePath lease)
-            IORef.writeIORef failurePath (Just path)
-            void
-                (Store.withOpenStore lease theory \_startup _store ->
-                    ioError (userError "fresh action failed")))
-        :: IO (Either IOError ())
-    case failed of
-        Left _ ->
-            pure ()
-        Right () ->
-            assertFailure "fresh-store action exception did not escape"
-    assertFreshRemoved failurePath
-
-doesNotFallBackAfterFatalStartup :: Assertion
-doesNotFallBackAfterFatalStartup =
-    Temp.withSystemTempDirectory "felix-store-no-fallback" \root -> do
-        (theory, _fixture) <- makeStoreFixture
-        let persistentParent = root Posix.</> "persistent"
-            persistentPath = persistentParent Posix.</> "store.sqlite"
-            cacheRoot = root Posix.</> "cache"
-        Directory.createDirectory persistentParent
-        Directory.createDirectory cacheRoot
-        plan <- expectRightIO
-            (Store.planStore
-                (Store.ExplicitStore persistentPath))
-        initialized <- Store.withStoreLease plan \lease ->
-            Store.withOpenStore lease theory \_startup _store ->
-                pure ()
-        assertEqual "fixture store initialized"
-            (Right ()) initialized
-        connection <- SQLite.open persistentPath
-        SQLite.execute_ connection
-            "DROP TABLE canonical_objects"
-        SQLite.close connection
-
-        withEnvironment "XDG_CACHE_HOME" cacheRoot do
-            result <- Store.withStoreLease plan \lease ->
-                Store.withOpenStore lease theory \_startup _store ->
-                    pure ()
-            case result of
-                Left
-                    (Store.StoreLifecycleOpenFailed
-                        (Store.FatalStoreStartup
-                            Store.StoreSchemaIntegrityFailure{})) ->
-                    pure ()
-                Left other ->
-                    assertFailure
-                        ("unexpected fatal-startup result: " <> show other)
-                Right () ->
-                    assertFailure "corrupt persistent store was accepted"
-            assertBool "fatal startup creates no default fallback"
-                . not
-                =<< Directory.doesPathExist
-                    (cacheRoot Posix.</> "felix")
-
-
-data StoreFixture = StoreFixture
-    !Identity.AssertedObject
-    !Identity.AssertedObject
-    !Identity.CheckedPropositionContent
-
-fixtureFirstObject :: StoreFixture -> Identity.AssertedObject
-fixtureFirstObject (StoreFixture object _second _proposition) =
-    object
-
-fixtureSecondObject :: StoreFixture -> Identity.AssertedObject
-fixtureSecondObject (StoreFixture _first object _proposition) =
-    object
-
-fixtureProposition
-    :: StoreFixture
-    -> Identity.CheckedPropositionContent
-fixtureProposition (StoreFixture _first _second proposition) =
-    proposition
-
-makeStoreFixture
-    :: IO (Identity.TheoryId, StoreFixture)
-makeStoreFixture = do
-    foundation <- expectRight Foundation.checkedFoundation
-    let theory = Identity.theoryId foundation
-        first = intrinsicObject theory Core.Empty
-        second = intrinsicObject theory Core.PairSet
-    closure <- expectRight
-        (Identity.validateObjectClosure theory [first, second])
-    proposition <- expectRight
-        (Identity.validatePropositionContent
-            closure
-            (Core.CEq
-                Core.TySet
-                (Core.CGlobal (Identity.assertedObjectId first))
-                (Core.CGlobal (Identity.assertedObjectId first))))
-    pure
-        ( theory
-        , StoreFixture first second proposition
-        )
-
-intrinsicObject
-    :: Identity.TheoryId
-    -> Core.CoreIntrinsicTag
-    -> Identity.AssertedObject
-intrinsicObject theory tag =
-    Identity.assertedObject identity content
-  where
-    coreType = Core.coreIntrinsicType tag
-    content =
-        Identity.IntrinsicObjectContent
-            theory tag coreType
-    identity =
-        Identity.intrinsicObjectId
-            theory tag coreType
-
-withStoreFixture
-    :: String
-    -> ( FilePath
-        -> Identity.TheoryId
-        -> StoreFixture
-        -> IO a
-       )
-    -> IO a
-withStoreFixture template action =
-    Temp.withSystemTempDirectory template \root -> do
-        (theory, fixture) <- makeStoreFixture
-        action
-            (root Posix.</> "store.sqlite")
-            theory
-            fixture
-
-expectOpen
-    :: FilePath
-    -> Identity.TheoryId
-    -> IO (Store.StoreStartup, Store.Store)
-expectOpen path theory = do
-    result <- Store.openStore path theory
-    case result of
-        Left failure ->
-            assertFailure (show failure) >> fail "unreachable"
-        Right opened ->
-            pure opened
-
-expectRight :: Show failure => Either failure value -> IO value
-expectRight = \case
-    Left failure ->
-        assertFailure (show failure) >> fail "unreachable"
-    Right value ->
-        pure value
-
-expectRightIO
-    :: Show failure
-    => IO (Either failure value)
-    -> IO value
-expectRightIO action =
-    expectRight =<< action
-
-assertFreshRemoved :: IORef.IORef (Maybe FilePath) -> Assertion
-assertFreshRemoved pathReference = do
-    selected <- IORef.readIORef pathReference
-    case selected of
-        Nothing ->
-            assertFailure "fresh store path was not allocated"
-        Just path -> do
-            assertBool "fresh database was removed"
-                . not
-                =<< Directory.doesPathExist path
-            assertBool "fresh database directory was removed"
-                . not
-                =<< Directory.doesPathExist
-                    (Posix.takeDirectory path)
-
-withEnvironment
-    :: String
-    -> String
-    -> IO value
-    -> IO value
-withEnvironment name value action =
-    Exception.bracket
-        (Environment.lookupEnv name)
-        restore
-        \_previous -> do
-            Environment.setEnv name value
-            action
-  where
-    restore = \case
-        Nothing ->
-            Environment.unsetEnv name
-        Just previous ->
-            Environment.setEnv name previous