path: root/source/Test/Unit/Store.hs

{-# 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 Provers qualified
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