diff options
Diffstat (limited to 'source/Felix/Test/Unit/Store.hs')
| -rw-r--r-- | source/Felix/Test/Unit/Store.hs | 1675 |
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 |