Migrate to `Felix` namespaceHEADhotg

1 files changed, 1675 insertions, 0 deletions

diff --git a/source/Felix/Test/Unit/Store.hs b/source/Felix/Test/Unit/Store.hs
new file mode 100644
index 0000000..423204c
--- /dev/null
+++ b/source/Felix/Test/Unit/Store.hs
@@ -0,0 +1,1675 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module Felix.Test.Unit.Store (unitTests) where
+
+import Base
+import Felix.Checking.Authority qualified as Authority
+import Felix.Checking.Core qualified as Core
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Foundation qualified as Foundation
+import Felix.Checking.Identity qualified as Identity
+import Felix.Checking.Module qualified as Typed
+import Felix.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 Felix.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