{-# LANGUAGE NoImplicitPrelude #-} module Felix.Test.Unit.Module (unitTests) where import Base import Felix.Checking.Authority qualified as Authority import Felix.Checking.Backend.Problem qualified as Backend import Felix.Checking.Core qualified as Core import Felix.Checking.Declaration qualified as Declaration import Felix.Checking.Exact qualified as Exact import Felix.Checking.Exact.Datatype qualified as ExactDatatype import Felix.Checking.Exact.Inductive qualified as ExactInductive import Felix.Checking.Exact.Proof qualified as ExactProof import Felix.Checking.FinalPrelude qualified as FinalPrelude import Felix.Checking.Foundation qualified as Foundation import Felix.Checking.Identity qualified as Identity import Felix.Checking.Module qualified as Module import Felix.Checking.Semantic qualified as Semantic import Felix.Checking.Typed.Inductive qualified as TypedInductive import Felix.CommandLine qualified as CommandLine import Felix.Math.Codec import Felix.Module import Felix.Parse qualified as Parse import Felix.Prelude qualified as Prelude import Felix.Provers qualified as Provers import Felix.Report.Location import Felix.Source import Felix.Source.Content qualified as Content import Felix.Store qualified as Store import Felix.Syntax.Abstract qualified as Raw import Felix.Syntax.Interface qualified as Syntax import Felix.Syntax.Internal qualified as Internal import Felix.Syntax.Lexicon qualified as Lexicon import Felix.Syntax.Pragma qualified as Pragma import Felix.Verification qualified as Verification import Felix.Workspace qualified as Workspace import Paths_felix qualified as Paths import Control.Concurrent (threadDelay) import Control.Concurrent.STM ( atomically , check , newEmptyTMVarIO , newTQueueIO , newTVarIO , putTMVar , readTQueue , readTVar , takeTMVar , tryReadTMVar , tryReadTQueue , writeTQueue , writeTVar ) import Control.Exception (bracket) import Control.Exception qualified as Exception import Control.Monad (foldM, when) import Data.ByteString qualified as ByteString import Data.Text qualified as StrictText import Data.Text.Encoding qualified as Text import Data.IORef ( IORef , atomicModifyIORef' , modifyIORef' , newIORef , readIORef ) import Data.List (sort) import Data.Map.Strict qualified as Map import Data.Set qualified as Set import Data.Vector qualified as Vector import Numeric.Natural (Natural) import System.Directory ( createDirectoryIfMissing , doesFileExist , getCurrentDirectory , getPermissions , setOwnerExecutable , setPermissions ) import System.FilePath.Posix qualified as Posix import System.IO.Temp qualified as Temp import System.Timeout qualified as Timeout import Test.Tasty import Test.Tasty.HUnit import UnliftIO.Async (withAsync, wait) unitTests :: TestTree unitTests = testGroup "Typed module inputs" [ testCase "constructs the empty bootstrap ordinarily" constructsEmptyBootstrap , testCase "identifies comment-only reserved input" identifiesCommentOnlyInput , testCase "loads and parses the packaged final prelude" parsesPackagedFinalPrelude , testCase "renders packaged final-prelude failures" rendersPackagedPreludeFailures , testCase "confines exact foundation-leaf completion" confinesFoundationLeafCompletion , testCase "builds the confined final prelude" buildsConfinedFinalPrelude , testCase "publishes the final prelude as an ordinary sealed root" publishesFinalPreludeRoot , testCase "retains exact omitted-proof locations" retainsExactOmittedProofLocation , testCase "coalesces syntax without collapsing semantic imports" coalescesSharedDirectSyntax , testCase "makes selected source errors terminal" rejectsUnsupportedTypedSource , testCase "reuses one verification session for successive checks" reusesVerificationSession , testCase "compiles exact declarations across an import" compilesExactDeclarationGraph , testCase "compiles and imports exact structures" compilesExactStructures , testCase "compiles and caches contextual abbreviations" compilesContextualAbbreviations , testCase "rejects an unknown exact structure parent atomically" rejectsUnknownExactStructureParent , testCase "compiles exact relation expressions" compilesExactRelationExpressions , testCase "resolves source-owned set application" resolvesSourceOwnedApplication , testCase "scopes quantified terms in proposition contexts" confinesExactQuantifiedTerms , testCase "closes the exact definition declaration boundary" closesExactDefinitionDeclarationBoundary , testCase "compiles exact ordinary proofs" compilesExactOrdinaryProofs , testCase "restores exact binder and witness proof forms" restoresExactBinderAndWitnessProofForms , testCase "restores exact local reasoning and calculations" restoresExactLocalReasoningAndCalculations , testCase "selects calculation link failures by source order" selectsCalculationLinkFailureBySourceOrder , testCase "compiles and reuses proof-local set definitions" compilesAndReusesProofLocalSetDefinitions , testCase "compiles and reuses proof-local function graphs" compilesAndReusesProofLocalFunctionGraphs , testCase "restores exact cases and classical contradiction" confinesTerminalExactContradiction , testCase "compiles exact separation comprehensions" compilesExactSeparationComprehensions , testCase "compiles exact replacement comprehensions" compilesExactReplacementComprehensions , testCase "compiles and reuses relational replacement" compilesAndReusesRelationalReplacement , testCase "compiles and reuses exact finite sets" compilesAndReusesExactFiniteSets , testCase "prepares exact deterministic datatypes" preparesExactDatatypes , testCase "rejects nested exact datatype recursion" rejectsNestedExactDatatypeRecursion , testCase "compiles and reuses exact datatypes" compilesAndReusesExactDatatypes , testCase "prepares exact direct inductives" preparesExactDirectInductives , testCase "prepares nested exact inductive recursion" preparesNestedExactInductiveRecursion , testCase "compiles transparent nested inductive wrappers" compilesTransparentNestedInductiveWrappers , testCase "normalizes nested exact inductive contexts" normalizesNestedExactInductiveContexts , testCase "compiles and reuses exact inductives" compilesAndReusesExactInductives , testCase "authorizes recursive exact inductives" authorizesRecursiveExactInductives , testCase "reuses exact separation validation" reusesExactSeparationValidation , testCase "compiles exact source axioms" compilesExactSourceAxioms , testCase "does not treat marker-only nouns as the fixed set noun" doesNotTreatMarkerOnlyNounAsSet , testCase "rejects proof-local generalization" rejectsProofLocalGeneralization , testCase "restores checked set induction" restoresCheckedSetInduction , testCase "compiles exact omitted proofs" compilesExactOmittedProofs , testCase "propagates and reuses exact escape authority" reusesExactEscapeAuthority , testCase "checks continuations after omitted subclaims" rejectsAfterExactOmittedSubclaim , testCase "reuses exact proof validation across module misses" reusesExactProofValidationAcrossModuleMisses , testCase "rejects declarations of fixed semantics" rejectsFixedSemanticDeclaration , testCase "rejects inductive carriers with fixed semantics" rejectsFixedSemanticInductive , testCase "keeps exact semantics independent of fixity" keepsExactSemanticsIndependentOfFixity , testCase "loads a cached exact producer for a fresh importer" loadsCachedExactProducerForFreshImporter , testCase "reports admitted source escapes on fresh, warm, and failure paths" reportsAdmittedSourceEscapes , testCase "selects concurrent module failures by source order" selectsConcurrentModuleFailureDeterministically , testCase "batches independent structure obligations atomically" batchesStructureObligationsAtomically , testCase "speculates dependent proof obligations without admitting ahead" speculatesDependentProofObligationsWithoutAdmittingAhead , testCase "starts diamond consumers after sealed acknowledgements" schedulesDiamondAfterSealedImports , testCase "classifies typed Vampire failures conservatively" classifiesTypedVampireFailures , testCase "retains the exact prefix before a later failure" retainsExactPrefixBeforeFailure , testCase "routes every production root through exact checking" routesProductionVerification , testCase "installs nonempty implicit prelude evidence" installsNonemptyImplicitPreludeEvidence ] constructsEmptyBootstrap :: Assertion constructsEmptyBootstrap = do foundation <- expectRight Foundation.checkedFoundation result <- Module.buildBootstrapPreludeFixture foundation unusedResolver session <- expectRight result let input = Module.bootstrapPreludeInput session parsed = Module.identifiedModuleParsed input sealed = Module.bootstrapPreludeModule session syntax = Module.sealedTypedModuleSyntax sealed semantic = Module.sealedTypedModuleSemantic sealed assertEqual "reserved owner" preludeModuleName (Module.identifiedModuleOwner input) case Module.identifiedModuleBinding input of Module.ReservedModuleBinding fileId label -> do assertEqual "diagnostic label" Prelude.preludeDiagnosticLabel label assertEqual "registered display label" (Just Prelude.preludeDiagnosticLabel) (lookupFilePath fileId) assertEqual "registered identity label" (Just Prelude.preludeDiagnosticLabel) (lookupFileIdentityPath fileId) Module.PhysicalModuleBinding source -> assertFailure ("bootstrap acquired a physical source: " <> show source) assertEqual "empty parsed blocks" [] (Parse.identifiedParsedModuleBlocks parsed) assertEqual "exact empty source identity" (Content.sourceContentIdBytes ByteString.empty) (Parse.identifiedParsedModuleSourceContentId parsed) assertEqual "no syntax imports" [] (Syntax.moduleSyntaxDirectInputs syntax) assertEqual "empty local syntax" [] (Syntax.canonicalSyntaxDeltaEntries (Syntax.moduleSyntaxLocalDelta syntax)) assertEqual "semantic owner" preludeModuleName (Semantic.semanticInterfaceOwner semantic) assertEqual "no semantic imports" [] (Semantic.semanticInterfaceDirectInputs semantic) assertEqual "no semantic declarations" [] (Semantic.semanticInterfaceDeclarations semantic) expectedPrefix <- expectRight (Semantic.initialPrefixContextId (Identity.theoryId foundation) preludeModuleName []) assertEqual "empty sealed prefix" expectedPrefix (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix sealed)) identifiesCommentOnlyInput :: Assertion identifiesCommentOnlyInput = do emptySource <- expectRight =<< Prelude.parseReservedPreludeSource Prelude.emptyBootstrapSourceInput source <- expectRight (Prelude.reservedPreludeSourceInput (Text.encodeUtf8 "% an in-memory comment\n")) first <- expectRight =<< Prelude.parseReservedPreludeSource source second <- expectRight =<< Prelude.parseReservedPreludeSource source let emptyParsed = Prelude.reservedParsedPreludeModule emptySource firstParsed = Prelude.reservedParsedPreludeModule first secondParsed = Prelude.reservedParsedPreludeModule second assertEqual "reserved live source binding" Parse.FreshReservedSource (Parse.freshModuleInputBinding (Prelude.reservedParsedPreludeInput first)) assertEqual "comment-only source has no blocks" [] (Parse.identifiedParsedModuleBlocks firstParsed) assertBool "content changes parsed identity" (Parse.identifiedParsedModuleId emptyParsed /= Parse.identifiedParsedModuleId firstParsed) assertEqual "same input has stable parsed identity" (Parse.identifiedParsedModuleId firstParsed) (Parse.identifiedParsedModuleId secondParsed) assertEqual "comments do not change syntax" (Syntax.moduleSyntaxAssertedId (Parse.identifiedParsedModuleSyntaxInterface emptyParsed)) (Syntax.moduleSyntaxAssertedId (Parse.identifiedParsedModuleSyntaxInterface firstParsed)) parsesPackagedFinalPrelude :: Assertion parsesPackagedFinalPrelude = do path <- Paths.getDataFileName "data/felix-prelude.tex" expectedBytes <- ByteString.readFile path source <- expectRight =<< Prelude.loadReservedPreludeSourceInput assertEqual "exact packaged bytes" expectedBytes (Prelude.reservedPreludeSourceBytes source) assertEqual "reserved owner" preludeModuleName (Prelude.reservedPreludeSourceOwner source) assertEqual "diagnostic label" Prelude.preludeDiagnosticLabel (Prelude.reservedPreludeSourceLabel source) first <- expectRight =<< Prelude.parseReservedPreludeSource source second <- expectRight =<< Prelude.parseReservedPreludeSource source let firstInput = Prelude.reservedParsedPreludeInput first firstParsed = Prelude.reservedParsedPreludeModule first secondParsed = Prelude.reservedParsedPreludeModule second assertEqual "no textual imports" [] (Parse.freshModuleInputImports firstInput) assertBool "declaration-bearing source" (not (null (Parse.identifiedParsedModuleBlocks firstParsed))) assertEqual "deterministic syntax interface" (Syntax.moduleSyntaxAssertedId (Parse.identifiedParsedModuleSyntaxInterface firstParsed)) (Syntax.moduleSyntaxAssertedId (Parse.identifiedParsedModuleSyntaxInterface secondParsed)) rendersPackagedPreludeFailures :: Assertion rendersPackagedPreludeFailures = do assertEqual "load failure" "/missing/felix-prelude.tex: unable to read packaged final prelude: not found" (Prelude.renderPreludeLoadError (Prelude.PreludeSourceReadFailed "/missing/felix-prelude.tex" "not found")) assertEqual "located syntax failure" ": syntax pragma location is out of range at 7:3" (Prelude.renderPreludeParseError parseFailure) assertEqual "authority-free API presentation" ("packaged final prelude parsing failed: " <> ": syntax pragma location is out of range at 7:3") (Workspace.renderAuthorityFreeParseError (Workspace.AuthorityFreePreludeParseFailed parseFailure)) where parseFailure = Prelude.PreludeSyntaxPragmaFailed (Pragma.SyntaxPragmaLocationOutOfRange Prelude.preludeDiagnosticLabel 7 3) confinesFoundationLeafCompletion :: Assertion confinesFoundationLeafCompletion = do foundation <- expectRight Foundation.checkedFoundation packaged <- expectRight =<< Prelude.loadReservedPreludeSourceInput parsed <- expectRight =<< Prelude.parseReservedPreludeSource packaged matching <- sole "matching foundation claim" (take 1 (Parse.identifiedParsedModuleBlocks (Prelude.reservedParsedPreludeModule parsed))) mismatchInput <- expectRight (Prelude.reservedPreludeSourceInput (Text.encodeUtf8 "\\begin{proposition}\\label{not_foundation}\n $\\emptyset = \\emptyset$.\n\\end{proposition}\n")) mismatchParsed <- expectRight =<< Prelude.parseReservedPreludeSource mismatchInput mismatch <- sole "mismatching claim" (Parse.identifiedParsedModuleBlocks (Prelude.reservedParsedPreludeModule mismatchParsed)) outcome <- Declaration.runModuleDriver foundation preludeModuleName [] unusedResolver Declaration.FreshValidation do explicit <- admitFoundationClaim foundation matching (Just (Raw.Omitted (locate matching))) nonmatching <- admitFoundationClaim foundation mismatch Nothing committed <- admitFoundationClaim foundation matching Nothing pure (explicit, nonmatching, committed) case outcome of Right (Declaration.DriverSucceeded (explicit, nonmatching, committed) _semantic _prefix _closure) -> do case explicit of Left ExactProof.ExactProofFoundationLeafRequiresImplicitAuto{} -> pure () Left other -> assertFailure ("explicit foundation result: " <> show other) Right{} -> assertFailure "explicit foundation proof was accepted" batch <- expectRight committed case nonmatching of Left ExactProof.ExactProofFoundationLeafTargetMismatch{} -> pure () Left other -> assertFailure ("mismatching foundation result: " <> show other) Right{} -> assertFailure "mismatching foundation claim was accepted" assertEqual "foundation tag" Foundation.UnivOfContains (case Declaration.committedBatchProofValidations batch of [record] -> case Authority.validationDirectAuthorization (Semantic.proofValidationRecordCertificate record) of Authority.CheckedKernelConstruction (Authority.FoundationLeaf tag) -> tag authorization -> error ("unexpected foundation authorization: " <> show authorization) records -> error ("unexpected foundation validation count: " <> show (length records))) Right Declaration.DriverFailed{} -> assertFailure "foundation driver failed" Right (Declaration.DriverSealFailed failure _prefix) -> assertFailure ("foundation driver did not seal: " <> show failure) Left failure -> assertFailure ("foundation driver did not open: " <> show failure) where admitFoundationClaim foundation block proof = Declaration.runProspectiveLoweringDriver (ExactProof.prepareFinalPreludeFoundationClaim foundation block proof) >>= \case Left failure -> pure (Left failure) Right prepared -> do lowered <- Declaration.runProspectiveLoweringDriver (ExactProof.lowerPreparedFinalPreludeFoundationClaim prepared) checked <- either Declaration.failDeclarationDriver pure lowered batch <- Declaration.admitCheckedDeclaration checked ExactProof.authorizeCheckedFinalPreludeFoundationClaim pure (Right batch) buildsConfinedFinalPrelude :: Assertion buildsConfinedFinalPrelude = do foundation <- expectRight Foundation.checkedFoundation FinalPrelude.buildFinalPreludeCandidate foundation finalPreludeResolver >>= \case FinalPrelude.FinalPreludeBuilt candidate -> do assertEqual "confined semantic owner" preludeModuleName (Semantic.semanticInterfaceOwner (FinalPrelude.finalPreludeSemantic candidate)) assertEqual "confined semantic imports" [] (Semantic.semanticInterfaceDirectInputs (FinalPrelude.finalPreludeSemantic candidate)) let baseDeltas = [ delta | delta <- Semantic.semanticInterfaceDeclarations (FinalPrelude.finalPreludeSemantic candidate) , not (null (Semantic.semanticEnvironmentStructures (Semantic.declarationDeltaEnvironment delta))) ] case baseDeltas of [delta] -> do assertEqual "base structure has no facts" [] (Semantic.declarationDeltaFacts delta) assertEqual "base structure has no propositions" [] (Semantic.declarationDeltaPropositions delta) case Semantic.semanticEnvironmentStructures (Semantic.declarationDeltaEnvironment delta) of [descriptor] -> do assertEqual "base structure is metadata-only" Nothing (Semantic.semanticStructureDescriptorPredicate descriptor) case Semantic.semanticStructureDescriptorOperations descriptor of [operation] -> case Identity.lookupCheckedObjectContent (Semantic.semanticStructureOperationObject operation) (FinalPrelude.finalPreludeObjects candidate) of Just Identity.OpaqueObjectContent{} -> pure () content -> assertFailure ("expected opaque carrier, got " <> show content) operations -> assertFailure ("expected one base operation, got " <> show operations) descriptors -> assertFailure ("expected one base descriptor, got " <> show descriptors) deltas -> assertFailure ("expected one base structure delta, got " <> show (length deltas)) let role roleName = maybe (assertFailure ("missing final-prelude role " <> show roleName)) pure (FinalPrelude.finalPreludePublicRole candidate roleName) omega <- role FinalPrelude.PreludeOmegaObject naturals <- role FinalPrelude.PreludeNaturalsAlias assertEqual "naturals expands to Omega" omega naturals traverse_ (void . role) (Set.toList FinalPrelude.expectedFinalPreludePublicRoles) let foundationTags = Set.fromList [ tag | batch <- Declaration.pendingModulePrefixBatches (FinalPrelude.finalPreludePrefix candidate) , record <- Declaration.committedBatchProofValidations batch , Authority.CheckedKernelConstruction (Authority.FoundationLeaf tag) <- [ Authority.validationDirectAuthorization (Semantic.proofValidationRecordCertificate record) ] ] assertBool "protected foundation presentation" ( Set.fromList [ Foundation.SetExtensionality , Foundation.EmptyCharacteristic , Foundation.PairSetCharacteristic , Foundation.FamilyUnionCharacteristic ] `Set.isSubsetOf` foundationTags ) assertFinalPreludeFoundationAlias candidate "pairset_iff" Foundation.PairSetCharacteristic assertFinalPreludeFoundationAlias candidate "pow_iff" Foundation.PowerSetCharacteristic assertRejectsAdditionalOmegaFact candidate FinalPrelude.FinalPreludeBuildFailed failure prefix -> assertFailure ("final prelude failed after " <> show (length (Declaration.pendingModulePrefixBatches prefix)) <> " declarations: " <> show failure) FinalPrelude.FinalPreludeBuildOpenFailed failure -> assertFailure ("final prelude did not open: " <> show failure) FinalPrelude.FinalPreludeSourceLoadFailed failure -> assertFailure ("final prelude did not load: " <> show failure) FinalPrelude.FinalPreludeSourceParseFailed failure -> assertFailure ("final prelude did not parse: " <> show failure) assertRejectsAdditionalOmegaFact :: FinalPrelude.FinalPreludeCandidate -> Assertion assertRejectsAdditionalOmegaFact candidate = do omegaId <- case FinalPrelude.finalPreludePublicRole candidate FinalPrelude.PreludeOmegaObject of Just (FinalPrelude.FinalPreludeObjectRole identity) -> pure identity role -> assertFailure ("unexpected Omega role " <> show role) >> fail "unreachable" batch <- batchByAlias (FinalPrelude.finalPreludePrefix candidate) "prelude_omega" let delta = Declaration.committedBatchDelta batch facts = Semantic.declarationDeltaFacts delta aliases = Semantic.declarationDeltaAliases delta propositions = Declaration.committedBatchPropositions batch certificates <- maybe (assertFailure "Omega declaration validation is absent" >> fail "unreachable") (pure . Semantic.declarationValidationRecordCertificates) (Declaration.committedBatchDeclarationValidation batch) (omegaBody, extensional, descriptor, extraFact, extraProposition, extraCertificate) <- case (facts, propositions, certificates) of ( [_equationFact, extensionalFact] , [equationProposition, extensionalProposition] , [ _equationCertificate , extensionalCertificate ] ) -> do body <- case Core.frozenCoreTerm (Identity.checkedPropositionTerm equationProposition) of Core.CEq Core.TySet (Core.CGlobal identity) candidateBody | identity == omegaId -> pure candidateBody target -> assertFailure ("unexpected Omega equation " <> show target) >> fail "unreachable" constructionDescriptor <- case Authority.validationDirectAuthorization extensionalCertificate of Authority.CheckedKernelConstruction (Authority.CheckedSetConstructionExtensionality identity candidateDescriptor) | identity == omegaId -> pure candidateDescriptor authorization -> assertFailure ("unexpected Omega extensional authority " <> show authorization) >> fail "unreachable" pure ( body , Identity.checkedPropositionTerm extensionalProposition , constructionDescriptor , extensionalFact , extensionalProposition , extensionalCertificate ) (candidateFacts, candidatePropositions, candidateCertificates) -> assertFailure ("unexpected Omega inventory shape " <> show ( length candidateFacts , length candidatePropositions , length candidateCertificates )) >> fail "unreachable" case FinalPrelude.validateOmegaFactInventory omegaId omegaBody extensional descriptor (facts <> [extraFact]) aliases (propositions <> [extraProposition]) (certificates <> [extraCertificate]) of Left (FinalPrelude.FinalPreludeFactContentMismatch "prelude_omega") -> pure () result -> assertFailure ("additional Omega construction fact was accepted: " <> show result) publishesFinalPreludeRoot :: Assertion publishesFinalPreludeRoot = do foundation <- expectRight Foundation.checkedFoundation Temp.withSystemTempDirectory "felix-final-prelude-root" \directory -> do let path = directory Posix. "store.sqlite" theory = Identity.theoryId foundation open = do (_startup, store) <- Store.openStore path theory >>= expectRight pure store bracket open Store.closeStore \store -> do freshMemo <- Store.newStoreMemo store session <- expectRight =<< Module.acquireFinalPreludeSession freshMemo store foundation finalPreludeResolver let input = Module.finalPreludeInput session sealed = Module.finalPreludeModule session syntax = Module.sealedTypedModuleSyntax sealed semantic = Module.sealedTypedModuleSemantic sealed assertEqual "empty store constructs the final-prelude root" Module.ModuleRootMiss (Module.finalPreludeAcquisition session) assertEqual "final prelude owner" preludeModuleName (Module.identifiedModuleOwner input) assertEqual "final prelude has no semantic parents" [] (Semantic.semanticInterfaceDirectInputs semantic) warmMemo <- Store.newStoreMemo store warmSession <- expectRight =<< Module.acquireFinalPreludeSession warmMemo store foundation unusedResolver let cached = Module.finalPreludeModule warmSession assertEqual "persisted final-prelude root is a cache hit" Module.ModuleRootHit (Module.finalPreludeAcquisition warmSession) assertEqual "generic root syntax" syntax (Module.sealedTypedModuleSyntax cached) assertEqual "generic root semantics" semantic (Module.sealedTypedModuleSemantic cached) assertEqual "cached base structure descriptor" (semanticStructureDescriptors semantic) (semanticStructureDescriptors (Module.sealedTypedModuleSemantic cached)) assertEqual "generic root final prefix" (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix sealed)) (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix cached)) visits <- Store.storeMemoVisits warmMemo assertEqual "cached prelude validates one artifact root" 1 (Store.storeArtifactsValidated visits) semanticStructureDescriptors :: Semantic.SemanticInterface -> [Semantic.SemanticStructureDescriptor] semanticStructureDescriptors semantic = [ descriptor | delta <- Semantic.semanticInterfaceDeclarations semantic , descriptor <- Semantic.semanticEnvironmentStructures (Semantic.declarationDeltaEnvironment delta) ] assertTransparentObjectAlias :: Module.SealedTypedModule -> Text -> Assertion assertTransparentObjectAlias sealed name = do target <- localObjectAliasTarget sealed name assertEqual ("transparent object for " <> StrictText.unpack name) Identity.TransparentObject (Identity.objectIdFamily target) localObjectKeyTarget :: Module.SealedTypedModule -> Semantic.SemanticGlobalKey -> IO Identity.ObjectId localObjectKeyTarget sealed key = do binding <- sole ("semantic binding for " <> show key) [ candidate | delta <- localSemanticDeltas sealed , candidate <- Semantic.semanticEnvironmentBindings (Semantic.declarationDeltaEnvironment delta) , Semantic.semanticGlobalBindingKey candidate == key ] pure (Semantic.semanticGlobalTargetObject (Semantic.semanticGlobalBindingTarget binding)) localObjectAliasTarget :: Module.SealedTypedModule -> Text -> IO Identity.ObjectId localObjectAliasTarget sealed name = do delta <- localDeltaByAlias sealed name binding <- sole ("semantic binding for " <> StrictText.unpack name) (Semantic.semanticEnvironmentBindings (Semantic.declarationDeltaEnvironment delta)) pure (Semantic.semanticGlobalTargetObject (Semantic.semanticGlobalBindingTarget binding)) checkedPropositionTermByAlias :: Module.SealedTypedModule -> Text -> IO (Core.FrozenCheckedCore Identity.ObjectId) checkedPropositionTermByAlias sealed name = do batch <- batchByAlias (Module.sealedTypedModulePrefix sealed) name alias <- sole ("semantic alias for " <> StrictText.unpack name) [ candidate | candidate <- Semantic.declarationDeltaAliases (Declaration.committedBatchDelta batch) , Semantic.semanticAliasName candidate == Semantic.semanticName name ] occurrence <- sole ("semantic fact for " <> StrictText.unpack name) [ candidate | candidate <- Semantic.declarationDeltaFacts (Declaration.committedBatchDelta batch) , Semantic.semanticFactFingerprint candidate == Semantic.semanticAliasTarget alias ] proposition <- sole ("checked proposition for " <> StrictText.unpack name) [ candidate | candidate <- Declaration.committedBatchPropositions batch , Identity.checkedPropositionId candidate == Semantic.semanticFactProposition occurrence ] pure (Identity.checkedPropositionTerm proposition) batchByAlias :: Declaration.PendingModulePrefix -> Text -> IO Declaration.CommittedDeclarationBatch batchByAlias prefix name = sole ("declaration batch for " <> StrictText.unpack name) [ batch | batch <- Declaration.pendingModulePrefixBatches prefix , alias <- Semantic.declarationDeltaAliases (Declaration.committedBatchDelta batch) , Semantic.semanticAliasName alias == Semantic.semanticName name ] assertFinalPreludeFoundationAlias :: FinalPrelude.FinalPreludeCandidate -> Text -> Foundation.FoundationAxiomTag -> Assertion assertFinalPreludeFoundationAlias candidate name tag = do batch <- batchByAlias (FinalPrelude.finalPreludePrefix candidate) name fact <- sole ("foundation fact " <> StrictText.unpack name) (Semantic.declarationDeltaFacts (Declaration.committedBatchDelta batch)) assertEqual ("foundation safety for " <> StrictText.unpack name) Authority.cleanAuthoritySafety (Authority.factAuthoritySafety (Semantic.semanticFactAuthority fact)) validation <- sole ("foundation validation for " <> StrictText.unpack name) (Declaration.committedBatchProofValidations batch) assertEqual ("exact foundation authority for " <> StrictText.unpack name) (Authority.CheckedKernelConstruction (Authority.FoundationLeaf tag)) (Authority.validationDirectAuthorization (Semantic.proofValidationRecordCertificate validation)) localDeltaByAlias :: Module.SealedTypedModule -> Text -> IO Semantic.DeclarationInterfaceDelta localDeltaByAlias sealed name = sole ("declaration delta for " <> StrictText.unpack name) [ delta | delta <- localSemanticDeltas sealed , any ((== Semantic.semanticName name) . Semantic.semanticAliasName) (Semantic.declarationDeltaAliases delta) ] localSemanticDeltas :: Module.SealedTypedModule -> [Semantic.DeclarationInterfaceDelta] localSemanticDeltas = Semantic.semanticInterfaceDeclarations . Module.sealedTypedModuleSemantic retainsExactOmittedProofLocation :: Assertion retainsExactOmittedProofLocation = do foundation <- expectRight Foundation.checkedFoundation source <- expectRight (Prelude.reservedPreludeSourceInput (Text.encodeUtf8 (StrictText.unlines [ "\\begin{proposition}\\label{omitted_location}" , " For all $x$ we have $x = x$." , "\\end{proposition}" , "\\begin{proof}" , " Omitted." , "\\end{proof}" ]))) parsed <- expectRight =<< Prelude.parseReservedPreludeSource source let blocks = Parse.identifiedParsedModuleBlocks (Prelude.reservedParsedPreludeModule parsed) claim <- sole "omitted claim" [ block | block@Raw.BlockClaim{} <- blocks ] proof <- sole "omitted proof" [ sourceProof | Raw.BlockProof _location sourceProof _end <- blocks ] outcome <- Declaration.runModuleDriver foundation preludeModuleName [] unusedResolver Declaration.FreshValidation do Declaration.runProspectiveLoweringDriver (ExactProof.prepareExactProof claim (Just proof)) >>= either Declaration.failModuleDriver pure case outcome of Right (Declaration.DriverSucceeded prepared _semantic prefix _closure) -> do location <- maybe (assertFailure "prepared omitted proof lost its location") pure (ExactProof.preparedExactProofFirstOmission prepared) assertEqual "omitted source line" 5 (locLine location) assertBool "preparation publishes no declaration" (null (Declaration.pendingModulePrefixBatches prefix)) Right (Declaration.DriverFailed failure _prefix) -> assertFailure ("omitted preparation failed: " <> show failure) Right (Declaration.DriverSealFailed failure _prefix) -> assertFailure ("omitted preparation did not seal: " <> show failure) Left failure -> assertFailure ("omitted preparation did not open: " <> show failure) coalescesSharedDirectSyntax :: Assertion coalescesSharedDirectSyntax = do foundation <- expectRight Foundation.checkedFoundation session <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver root <- getCurrentDirectory mounts <- expectRight =<< prepareSourceMounts [ (sourceMountId "project", root) , (sourceMountId "library", root Posix. "library") , (sourceMountId "debug", root Posix. "debug") ] let bootstrapSyntax = Module.sealedTypedModuleSyntax (Module.bootstrapPreludeModule session) syntaxInputs _source = [bootstrapSyntax] request <- expectRight (searchedRoot "test/phase3/typed-shared-root.tex") workspace <- expectRight =<< Parse.parseSourceWorkspaceWithSyntaxInputs mounts request syntaxInputs case Parse.parsedWorkspaceModules workspace of [firstParsed, secondParsed, rootParsed] -> do first <- seal foundation session firstParsed [] second <- seal foundation session secondParsed [] assertEqual "distinct modules share one syntax interface" (Syntax.moduleSyntaxAssertedId (Module.sealedTypedModuleSyntax first)) (Syntax.moduleSyntaxAssertedId (Module.sealedTypedModuleSyntax second)) assertBool "semantic module owners remain distinct" (Module.sealedTypedModuleOwner first /= Module.sealedTypedModuleOwner second) assertBool "semantic interfaces remain distinct" (Semantic.semanticInterfaceAssertedId (Module.sealedTypedModuleSemantic first) /= Semantic.semanticInterfaceAssertedId (Module.sealedTypedModuleSemantic second)) let rootSyntax = Parse.parsedModuleSyntaxInterface rootParsed assertEqual "root coalesces the shared direct syntax" [ Syntax.moduleSyntaxAssertedId bootstrapSyntax , Syntax.moduleSyntaxAssertedId (Module.sealedTypedModuleSyntax first) ] (Syntax.moduleSyntaxDirectInputs rootSyntax) sealedRoot <- seal foundation session rootParsed [first, second] assertEqual "root retains both semantic imports" [ Semantic.semanticInterfaceAssertedId (Module.sealedTypedModuleSemantic (Module.bootstrapPreludeModule session)) , Semantic.semanticInterfaceAssertedId (Module.sealedTypedModuleSemantic first) , Semantic.semanticInterfaceAssertedId (Module.sealedTypedModuleSemantic second) ] (Semantic.semanticInterfaceDirectInputs (Module.sealedTypedModuleSemantic sealedRoot)) modules -> assertFailure ("unexpected shared-syntax module count: " <> show (length modules)) where seal foundation session parsed direct = do input <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness session) unusedResolver Declaration.FreshValidation parsed direct) Module.runTypedModule input >>= \case Module.TypedModuleSucceeded sealed -> pure sealed Module.TypedModuleOpenFailed{} -> assertFailure "empty typed module did not open" >> fail "unreachable" Module.TypedModuleFailed{} -> assertFailure "empty typed module did not seal" >> fail "unreachable" rejectsUnsupportedTypedSource :: Assertion rejectsUnsupportedTypedSource = do result <- (checkFileFresh (Provers.vampire "vampire" Provers.defaultTimeLimit Provers.defaultMemoryLimit) "test/phase3/typed-unsupported.tex") case result of Right ( Verification.VerificationCheckingFailure _report (failure@(Verification.VerificationTypedModuleError source (Module.TypedActionFailed (Module.TypedExactCompileFailed (Exact.ExactGuardedOpaqueSignature location))) prefix)) , _slowReport ) -> do assertEqual "failed source" "test/phase3/typed-unsupported.tex" (safeRelativePathFilePath (resolvedSourceRelativePath source)) assertEqual "unsupported source location line" 2 (locLine location) assertEqual "failure retains the initial module prefix" 0 (length (Declaration.pendingModulePrefixBatches prefix)) let diagnostic = Verification.renderVerificationDriverError failure assertBool "diagnostic retains resolved source" ("project:test/phase3/typed-unsupported.tex" `StrictText.isInfixOf` diagnostic) assertBool "diagnostic retains best location" ("typed-unsupported.tex 2:14" `StrictText.isInfixOf` diagnostic) assertBool "diagnostic explains the typed failure" ("opaque signature cannot have a header assumption" `StrictText.isInfixOf` diagnostic) Left err -> assertFailure ("unexpected verification driver error: " <> show err) Right{} -> assertFailure "unsupported typed source was admitted" reusesVerificationSession :: Assertion reusesVerificationSession = withAcceptedFixtureVampire "felix-session-reuse" \prover -> do plan <- Store.planStore Store.FreshTemporaryStore >>= expectRight graph <- Workspace.prepareDefaultSourceGraph source >>= expectRight Store.withStoreLease plan \lease -> do opened <- Verification.withVerificationSession lease \session -> do let request = Verification.CheckRequest { Verification.checkSourceGraph = graph , Verification.checkStoreValidationMode = Verification.FreshStoreValidation , Verification.checkEffectiveJobs = testSequentialJobs , Verification.checkVampire = prover , Verification.checkRequestObserver = ignoredVerificationRequests } first <- Verification.checkWorkspace session request >>= expectRight second <- Verification.checkWorkspace session request >>= expectRight traverse_ assertUnsupported [ Verification.checkVerificationResult first , Verification.checkVerificationResult second ] void (expectRight opened) where source = "test/phase3/typed-unsupported.tex" assertUnsupported = \case Verification.VerificationCheckingFailure _report Verification.VerificationTypedModuleError{} -> pure () other -> assertFailure ("successive session check had unexpected result: " <> show other) compilesExactDeclarationGraph :: Assertion compilesExactDeclarationGraph = do (_foundation, _bootstrap, workspace, sealedModules) <- compileExactFixture "test/phase5/exact-importer.tex" assertEqual "dependency-closed module count" 2 (length sealedModules) assertEqual "imported-before-importer source order" [ "test/phase5/exact-producer.tex" , "test/phase5/exact-importer.tex" ] [ safeRelativePathFilePath (resolvedSourceRelativePath (Parse.parsedModuleResolved parsed)) | parsed <- toList (Parse.parsedWorkspaceImportedBeforeImporter workspace) ] case sealedModules of [producer, importer] -> do let producerPrefix = Module.sealedTypedModulePrefix producer importerPrefix = Module.sealedTypedModulePrefix importer producerBatches = Declaration.pendingModulePrefixBatches producerPrefix importerBatches = Declaration.pendingModulePrefixBatches importerPrefix assertEqual "producer declaration batches" 3 (length producerBatches) assertEqual "importer declaration batches" 1 (length importerBatches) assertEqual "producer declaration order" [0, 1, 2] [ localDeclarationOrdinalValue (Semantic.declarationSlotOrdinal (Declaration.committedBatchSlot batch)) | batch <- producerBatches ] let producerDeltas = Semantic.semanticInterfaceDeclarations (Module.sealedTypedModuleSemantic producer) importerDeltas = Semantic.semanticInterfaceDeclarations (Module.sealedTypedModuleSemantic importer) assertEqual "one exact binding per producer declaration" [1, 1, 1] (bindingCount <$> producerDeltas) assertEqual "one exact importer binding" [1] (bindingCount <$> importerDeltas) assertEqual "producer object families" ["opaque", "transparent"] [ objectFamilyName (Identity.assertedObjectContent object) | batch <- producerBatches , object <- Declaration.committedBatchObjects batch ] definitionDelta <- sole "producer definition delta" (drop 2 producerDeltas) definitionBinding <- sole "producer definition binding" (bindings definitionDelta) definitionFact <- sole "producer definition fact" (Semantic.declarationDeltaFacts definitionDelta) definitionAlias <- sole "producer definition alias" (Semantic.declarationDeltaAliases definitionDelta) assertEqual "definition alias" (Semantic.semanticName "phase5_definition") (Semantic.semanticAliasName definitionAlias) assertEqual "definition is proof-search eligible" Semantic.SearchEligible (Semantic.semanticFactSearchEligibility definitionFact) assertEqual "definition authority is clean" Authority.cleanAuthoritySafety (Authority.factAuthoritySafety (Semantic.semanticFactAuthority definitionFact)) definitionBatch <- sole "producer definition batch" (drop 2 producerBatches) validation <- maybe (assertFailure "definition declaration validation is absent" >> fail "unreachable") pure (Declaration.committedBatchDeclarationValidation definitionBatch) certificate <- sole "definition validation certificate" (Semantic.declarationValidationRecordCertificates validation) assertEqual "direct defining-equation authority" (Authority.CheckedKernelConstruction (Authority.CheckedDefinitionEquation (Semantic.semanticGlobalTargetObject (Semantic.semanticGlobalBindingTarget definitionBinding)))) (Authority.validationDirectAuthorization certificate) aliasDelta <- sole "producer abbreviation delta" (take 1 (drop 1 producerDeltas)) aliasBinding <- sole "producer abbreviation binding" (bindings aliasDelta) seedDelta <- sole "producer signature delta" (take 1 producerDeltas) seedBinding <- sole "producer signature binding" (bindings seedDelta) let seedTarget = Semantic.semanticGlobalTargetObject (Semantic.semanticGlobalBindingTarget seedBinding) aliasTarget = Semantic.semanticGlobalTargetObject (Semantic.semanticGlobalBindingTarget aliasBinding) definitionTarget = Semantic.semanticGlobalTargetObject (Semantic.semanticGlobalBindingTarget definitionBinding) assertEqual "abbreviation expands transparently" (Semantic.TransparentExpansion aliasTarget) (Semantic.semanticGlobalBindingTarget aliasBinding) assertEqual "definition remains a named global" (Semantic.GlobalReference definitionTarget) (Semantic.semanticGlobalBindingTarget definitionBinding) assertEqual "definition content coalesces with its expansion" aliasTarget definitionTarget assertEqual "coalesced definition adds no object" [] (Declaration.committedBatchObjects definitionBatch) aliasBatch <- sole "producer abbreviation batch" (take 1 (drop 1 producerBatches)) aliasObject <- sole "producer abbreviation object" (Declaration.committedBatchObjects aliasBatch) case Identity.assertedObjectContent aliasObject of Identity.TransparentObjectContent _theory _coreType body -> assertEqual "expanded body retains only the opaque seed" (Set.singleton seedTarget) (Core.canonicalTermGlobals body) content -> assertFailure ("abbreviation object is not transparent: " <> show content) importerBatch <- sole "importer declaration batch" importerBatches importerDelta <- sole "importer semantic delta" importerDeltas importerBinding <- sole "importer binding" (bindings importerDelta) assertEqual "equal transparent content reuses the producer object" (Semantic.semanticGlobalBindingTarget definitionBinding) (Semantic.semanticGlobalBindingTarget importerBinding) assertEqual "reused transparent content adds no object" [] (Declaration.committedBatchObjects importerBatch) modules -> assertFailure ("unexpected exact module count: " <> show (length modules)) where bindingCount = length . bindings bindings = Semantic.semanticEnvironmentBindings . Semantic.declarationDeltaEnvironment objectFamilyName :: Identity.ObjectContent -> String objectFamilyName = \case Identity.OpaqueObjectContent{} -> "opaque" Identity.TransparentObjectContent{} -> "transparent" Identity.IntrinsicObjectContent{} -> "intrinsic" compilesExactStructures :: Assertion compilesExactStructures = do foundation <- expectRight Foundation.checkedFoundation repository <- getCurrentDirectory Temp.withSystemTempDirectory "felix-exact-structures" \directory -> do let path = directory Posix. "store.sqlite" executable = directory Posix. "vampire" writeAcceptedFixtureVampire executable runs <- newIORef (0 :: Int) let resolver = countingAcceptedResolver executable runs (_startup, store) <- Store.openStore path (Identity.theoryId foundation) >>= expectRight bracket (pure store) Store.closeStore \opened -> do prelude <- expectRight =<< acquireFinalPreludeSession opened foundation resolver carrierOperation <- sole "base carrier operation" [ operation | descriptor <- semanticStructureDescriptors (Module.sealedTypedModuleSemantic (Module.finalPreludeModule prelude)) , operation <- Semantic.semanticStructureDescriptorOperations descriptor ] mounts <- exactFixtureMounts repository workspace <- parseFinalExactWorkspace prelude mounts "test/phase5/exact-structure-child.tex" sealed <- compileFinalParsedWorkspaceWithResolver foundation prelude resolver workspace freshRuns <- readIORef runs warm <- installAndLoadStructures opened foundation prelude workspace sealed warmRuns <- readIORef runs assertEqual "warm structures preserve descriptors" (structureDescriptors <$> sealed) (structureDescriptors <$> warm) assertEqual "warm structures make no prover calls" freshRuns warmRuns case sealed of [parent, child] -> do let parentBatches = Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix parent) parentDeltas = Semantic.semanticInterfaceDeclarations (Module.sealedTypedModuleSemantic parent) childBatches = Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix child) childDeltas = Semantic.semanticInterfaceDeclarations (Module.sealedTypedModuleSemantic child) parentBatch <- sole "parent structure batch" (take 1 parentBatches) parentDelta <- sole "parent structure delta" (take 1 parentDeltas) parentDescriptor <- sole "parent structure descriptor" (Semantic.semanticEnvironmentStructures (Semantic.declarationDeltaEnvironment parentDelta)) parentOperation <- sole "parent structure operation" (Semantic.semanticStructureDescriptorOperations parentDescriptor) parentPredicate <- maybe (assertFailure "parent structure has no predicate" >> fail "unreachable") pure (Semantic.semanticStructureDescriptorPredicate parentDescriptor) assertEqual "structure object family order" ["opaque", "transparent"] [ objectFamilyName (Identity.assertedObjectContent object) | object <- Declaration.committedBatchObjects parentBatch ] assertEqual "structure fact aliases" [ Semantic.semanticName "pointed_set" , Semantic.semanticName "pointed_refl" ] (Semantic.semanticAliasName <$> Semantic.declarationDeltaAliases parentDelta) definitionFact <- sole "structure definition fact" (take 1 (Semantic.declarationDeltaFacts parentDelta)) definitionTarget <- targetForOccurrence parentBatch definitionFact assertEqual "pointwise structure definition" (Core.CForall Core.TySet (Core.CEq Core.TyProp (Core.CApp (Core.CGlobal parentPredicate) (Core.CBound 0)) (Core.CEq Core.TySet (Core.CBound 0) (Core.CBound 0)))) definitionTarget validations <- maybe (assertFailure "structure validation is absent" >> fail "unreachable") (pure . Semantic.declarationValidationRecordCertificates) (Declaration.committedBatchDeclarationValidation parentBatch) case validations of definitionValidation : projectionValidation : [] -> do assertEqual "structure definition authority" (Authority.CheckedKernelConstruction (Authority.CheckedDefinitionEquation parentPredicate)) (Authority.validationDirectAuthorization definitionValidation) projectionFact <- sole "structure projection fact" (drop 1 (Semantic.declarationDeltaFacts parentDelta)) assertEqual "projection has independent authority" (Semantic.semanticFactAuthority projectionFact) (Authority.validationTarget projectionValidation) assertEqual "projection authority is clean" Authority.cleanAuthoritySafety (Authority.factAuthoritySafety (Authority.validationTarget projectionValidation)) records -> assertFailure ("expected two structure validations, got " <> show records) assertBool "all parent structure facts are clean" (all ((== Authority.cleanAuthoritySafety) . Authority.factAuthoritySafety . Semantic.semanticFactAuthority) (Semantic.declarationDeltaFacts parentDelta)) let claimGlobals marker = do batch <- batchWithAlias marker parentBatches occurrence <- sole (marker <> " occurrence") (Semantic.declarationDeltaFacts (Declaration.committedBatchDelta batch)) Core.canonicalTermGlobals <$> targetForOccurrence batch occurrence carrierGlobals <- claimGlobals "pointed_carrier" operationGlobals <- claimGlobals "pointed_operation" assertBool "membership uses inherited carrier" (Semantic.semanticStructureOperationObject carrierOperation `Set.member` carrierGlobals) assertBool "implicit and explicit operation share one object" (Semantic.semanticStructureOperationObject parentOperation `Set.member` operationGlobals) let assertEquivalentClaim surface explicit = do surfaceTerm <- checkedPropositionTermByAlias parent surface explicitTerm <- checkedPropositionTermByAlias parent explicit assertEqual (StrictText.unpack surface <> " uses the inherited carrier") explicitTerm surfaceTerm assertEquivalentClaim "pointed_self_member" "pointed_self_member_explicit" assertEquivalentClaim "pointed_self_not_member" "pointed_self_not_member_explicit" assertEquivalentClaim "pointed_self_element" "pointed_self_element_explicit" assertEquivalentClaim "pointed_header_member" "pointed_header_member_explicit" childBatch <- sole "child structure batch" childBatches childDelta <- sole "child structure delta" childDeltas childDescriptor <- sole "child structure descriptor" (Semantic.semanticEnvironmentStructures (Semantic.declarationDeltaEnvironment childDelta)) assertEqual "child allocates no replacement operation" [] (Semantic.semanticStructureDescriptorOperations childDescriptor) assertEqual "child owns only its transparent predicate" ["transparent"] [ objectFamilyName (Identity.assertedObjectContent object) | object <- Declaration.committedBatchObjects childBatch ] modules -> assertFailure ("expected parent and child structures, got " <> show (length modules)) where installAndLoadStructures store foundation prelude workspace sealed = do memo <- Store.newStoreMemo store case ( toList (Parse.parsedWorkspaceImportedBeforeImporter workspace) , sealed ) of ([parentParsed, childParsed], [parent, child]) -> do cachedParent <- persistAndLoad memo [] parentParsed parent cachedChild <- persistAndLoad memo [cachedParent] childParsed child pure [cachedParent, cachedChild] (parsed, modules) -> assertFailure ("expected two structure installations, got " <> show (length parsed) <> " parsed and " <> show (length modules) <> " checked modules") >> fail "unreachable" where preludeModule = Module.finalPreludeModule prelude persistAndLoad memo parents parsed sealedModule = do let input = Module.identifiedPhysicalModule parsed syntax = Module.sealedTypedModuleSyntax sealedModule semantic = Module.sealedTypedModuleSemantic sealedModule key <- expectRight (Semantic.moduleArtifactKey (Module.identifiedModuleOwner input) (Parse.identifiedParsedModuleId (Module.identifiedModuleParsed input)) (Semantic.semanticInterfaceDirectInputs semantic) (Identity.theoryId foundation)) let artifact = Semantic.moduleArtifactResult key (Syntax.moduleSyntaxAssertedId syntax) (Semantic.semanticInterfaceAssertedId semantic) acknowledged <- expectRight =<< Store.writeSealedModule store (Module.sealedTypedModulePrefix sealedModule) [syntax] [semantic] artifact assertEqual "cached structure artifact acknowledgement" artifact acknowledged loaded <- expectRight =<< Store.loadCachedModuleInstallation memo store key (Syntax.moduleSyntaxAssertedId (Parse.parsedModuleSyntaxInterface parsed)) installation <- maybe (assertFailure "cached structure installation is absent" >> fail "unreachable") pure loaded expectRight (Module.cachedSealedTypedModule foundation (preludeModule : parents) installation) structureDescriptors = semanticStructureDescriptors . Module.sealedTypedModuleSemantic objectFamilyName :: Identity.ObjectContent -> String objectFamilyName = \case Identity.OpaqueObjectContent{} -> "opaque" Identity.TransparentObjectContent{} -> "transparent" Identity.IntrinsicObjectContent{} -> "intrinsic" targetForOccurrence batch occurrence = maybe (assertFailure "structure proposition is absent" >> fail "unreachable") (pure . Core.frozenCoreTerm . Identity.checkedPropositionTerm) (find ((== Semantic.semanticFactProposition occurrence) . Identity.checkedPropositionId) (Declaration.committedBatchPropositions batch)) batchWithAlias marker batches = maybe (assertFailure ("missing batch alias " <> marker) >> fail "unreachable") pure (find (elem (Semantic.semanticName (StrictText.pack marker)) . fmap Semantic.semanticAliasName . Semantic.declarationDeltaAliases . Declaration.committedBatchDelta) batches) compilesContextualAbbreviations :: Assertion compilesContextualAbbreviations = do foundation <- expectRight Foundation.checkedFoundation repository <- getCurrentDirectory Temp.withSystemTempDirectory "felix-contextual-abbreviation" \directory -> do let storePath = directory Posix. "store.sqlite" executable = directory Posix. "vampire" relative = "test/phase5/exact-contextual-abbreviation.tex" writeAcceptedFixtureVampire executable runs <- newIORef (0 :: Int) let resolver = countingAcceptedResolver executable runs (_startup, store) <- Store.openStore storePath (Identity.theoryId foundation) >>= expectRight bracket (pure store) Store.closeStore \opened -> do prelude <- expectRight =<< acquireFinalPreludeSession opened foundation resolver mounts <- exactFixtureMounts repository workspace <- parseFinalExactWorkspace prelude mounts relative sealed <- sole "contextual abbreviation module" =<< compileFinalParsedWorkspaceWithResolver foundation prelude resolver workspace let deltas = Semantic.semanticInterfaceDeclarations (Module.sealedTypedModuleSemantic sealed) contextualTargets = [ (identity, requirements) | delta <- deltas , binding <- Semantic.semanticEnvironmentBindings (Semantic.declarationDeltaEnvironment delta) , Semantic.ContextualTransparentExpansion identity requirements <- [Semantic.semanticGlobalBindingTarget binding] ] assertEqual "contextual target count" 2 (length contextualTargets) requirements <- sole "canonical contextual requirement set" (nubOrd (snd <$> contextualTargets)) assertEqual "one structure operation requirement" 1 (Map.size requirements) let batches = Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix sealed) traverse_ (assertReflexiveFact batches) [ "phase5_context_dot_explicit" , "phase5_context_inherited" , "phase5_context_nested" , "phase5_context_explicit_unique" ] parsed <- pure (Parse.parsedWorkspaceRootModule workspace) let syntax = Module.sealedTypedModuleSyntax sealed semantic = Module.sealedTypedModuleSemantic sealed key <- expectRight (Semantic.moduleArtifactKey (moduleName (Parse.parsedModuleAddress parsed)) (Parse.parsedModuleId parsed) (Semantic.semanticInterfaceDirectInputs semantic) (Identity.theoryId foundation)) let artifact = Semantic.moduleArtifactResult key (Syntax.moduleSyntaxAssertedId syntax) (Semantic.semanticInterfaceAssertedId semantic) void (expectRight =<< Store.writeSealedModule opened (Module.sealedTypedModulePrefix sealed) [syntax] [semantic] artifact) memo <- Store.newStoreMemo opened loaded <- expectRight =<< Store.loadCachedModuleInstallation memo opened key (Syntax.moduleSyntaxAssertedId (Parse.parsedModuleSyntaxInterface parsed)) installation <- maybe (assertFailure "contextual cached installation is absent" >> fail "unreachable") pure loaded cached <- expectRight (Module.cachedSealedTypedModule foundation [Module.finalPreludeModule prelude] installation) assertEqual "cached contextual semantic target" semantic (Module.sealedTypedModuleSemantic cached) runsBeforeConsumer <- readIORef runs consumerWorkspace <- parseFinalExactWorkspace prelude mounts "test/phase5/exact-contextual-abbreviation-consumer.tex" let consumerParsed = Parse.parsedWorkspaceRootModule consumerWorkspace consumerInput <- expectRight (Module.typedModuleInput foundation (Module.finalPreludeReadiness prelude) resolver Declaration.FreshValidation consumerParsed [cached]) consumer <- Module.runTypedModule consumerInput >>= \case Module.TypedModuleSucceeded sealedConsumer -> pure sealedConsumer Module.TypedModuleOpenFailed failure -> assertFailure ("contextual consumer did not open: " <> show failure) >> fail "unreachable" Module.TypedModuleFailed failure _prefix -> assertFailure ("contextual consumer did not seal: " <> show failure) >> fail "unreachable" let consumerTargets = [ Semantic.semanticGlobalTargetObject (Semantic.semanticGlobalBindingTarget binding) | delta <- localSemanticDeltas consumer , binding <- Semantic.semanticEnvironmentBindings (Semantic.declarationDeltaEnvironment delta) ] assertEqual "two contextual consumer declarations" 2 (length consumerTargets) void (sole "quantified contextual binder matches its explicit parameter" (nubOrd consumerTargets)) runsAfterConsumer <- readIORef runs assertEqual "contextual abbreviations require no prover call" runsBeforeConsumer runsAfterConsumer verifyFailure foundation resolver prelude mounts sealed "test/phase5/exact-contextual-abbreviation-missing.tex" (\case Exact.ExactContextualExpansionNotAvailable location _key -> assertEqual "missing context line" 5 (locLine location) failure -> assertFailure ("unexpected missing-context failure: " <> show failure)) verifyFailure foundation resolver prelude mounts sealed "test/phase5/exact-contextual-abbreviation-ambiguous.tex" (\case Exact.ExactStructureOperationAmbiguous location _symbol objects -> do assertEqual "ambiguous operation line" 16 (locLine location) assertEqual "two distinct operation objects" 2 (length objects) failure -> assertFailure ("unexpected operation ambiguity failure: " <> show failure)) where assertReflexiveFact batches marker = do batch <- maybe (assertFailure ("missing contextual fact " <> marker) >> fail "unreachable") pure (find (elem (Semantic.semanticName (StrictText.pack marker)) . fmap Semantic.semanticAliasName . Semantic.declarationDeltaAliases . Declaration.committedBatchDelta) batches) proposition <- sole (marker <> " proposition") (Declaration.committedBatchPropositions batch) let body = stripClaimEnvelope (Core.frozenCoreTerm (Identity.checkedPropositionTerm proposition)) case body of Core.CEq _ left right -> assertEqual (marker <> " canonical sides") left right _ -> assertFailure (marker <> " did not elaborate to reflexive equality: " <> show body) stripClaimEnvelope = \case Core.CForall _ body -> stripClaimEnvelope body Core.CImp _ body -> stripClaimEnvelope body term -> term verifyFailure foundation resolver prelude mounts imported relative checkFailure = do workspace <- parseFinalExactWorkspace prelude mounts relative let parsed = Parse.parsedWorkspaceRootModule workspace input <- expectRight (Module.typedModuleInput foundation (Module.finalPreludeReadiness prelude) resolver Declaration.FreshValidation parsed [imported]) Module.runTypedModule input >>= \case Module.TypedModuleFailed (Module.TypedActionFailed (Module.TypedExactCompileFailed failure)) _prefix -> checkFailure failure Module.TypedModuleFailed (Module.TypedActionFailed (Module.TypedExactProofFailed (ExactProof.ExactProofElaborationFailed failure))) _prefix -> checkFailure failure Module.TypedModuleSucceeded{} -> assertFailure (relative <> " was unexpectedly accepted") Module.TypedModuleOpenFailed failure -> assertFailure (relative <> " did not open: " <> show failure) Module.TypedModuleFailed failure _prefix -> assertFailure (relative <> " failed unexpectedly: " <> show failure) rejectsUnknownExactStructureParent :: Assertion rejectsUnknownExactStructureParent = Temp.withSystemTempDirectory "felix-exact-structure-parent" \root -> do let relative = "entry.tex" path = root Posix. relative source = "\\begin{struct}\\label{known_structure}\n" <> " A known structure $X$ is a onesorted structure.\n" <> "\\end{struct}\n\n" <> "\\begin{struct}\\label{invalid_structure}\n" <> " An invalid structure $X$ is a future structure.\n" <> "\\end{struct}\n\n" <> "\\begin{struct}\\label{future_structure}\n" <> " A future structure $X$ is a onesorted structure.\n" <> "\\end{struct}\n" ByteString.writeFile path (Text.encodeUtf8 (StrictText.pack source)) foundation <- expectRight Foundation.checkedFoundation Temp.withSystemTempDirectory "felix-exact-structure-store" \directory -> do let storePath = directory Posix. "store.sqlite" executable = directory Posix. "vampire" writeAcceptedFixtureVampire executable runs <- newIORef (0 :: Int) let resolver = countingAcceptedResolver executable runs (_startup, store) <- Store.openStore storePath (Identity.theoryId foundation) >>= expectRight bracket (pure store) Store.closeStore \opened -> do prelude <- expectRight =<< acquireFinalPreludeSession opened foundation resolver mounts <- exactFixtureMounts root workspace <- parseFinalExactWorkspace prelude mounts relative let parsed = Parse.parsedWorkspaceRootModule workspace input <- expectRight (Module.typedModuleInput foundation (Module.finalPreludeReadiness prelude) resolver Declaration.FreshValidation parsed []) Module.runTypedModule input >>= \case Module.TypedModuleFailed (Module.TypedActionFailed (Module.TypedExactCompileFailed (Exact.ExactStructureNotVisible location _phrase))) prefix -> do assertEqual "unknown parent line" 5 (locLine location) assertEqual "only the valid structure was published" 1 (length (Declaration.pendingModulePrefixBatches prefix)) Module.TypedModuleSucceeded{} -> assertFailure "unknown structure parent was accepted" Module.TypedModuleOpenFailed failure -> assertFailure ("invalid structure module did not open: " <> show failure) Module.TypedModuleFailed failure _prefix -> assertFailure ("unexpected invalid structure failure: " <> show failure) compilesExactRelationExpressions :: Assertion compilesExactRelationExpressions = do foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver repository <- getCurrentDirectory mounts <- exactFixtureMounts repository workspace <- parseExactWorkspace bootstrap mounts "test/phase5/exact-relation-expression.tex" observed <- newIORef [] withAcceptedFixtureVampire "felix-exact-relation-expression" \prover -> do let resolver = Declaration.vampireResolver \prepared -> do let problem = Provers.preparedTypedProverLogicalProblem prepared claim = Backend.typedProblemClaim problem locals = Backend.typedProblemLocalPremises problem modifyIORef' observed (<> [ [ Backend.supportedPropositionTerm (Backend.typedLocalPremiseProposition premise) == Backend.supportedPropositionTerm claim | premise <- Vector.toList locals ] ]) (Provers.runPreparedTypedProver prover prepared) void (compileParsedWorkspaceWithResolver foundation bootstrap resolver workspace) assertEqual "relation expression is ordered-pair membership" [[True]] =<< readIORef observed missingPair <- withAcceptedFixtureVampire "felix-exact-relation-expression-missing-pair" \prover -> (checkFileFresh prover "test/phase5/exact-relation-expression-missing-pair.tex") case missingPair of Right ( Verification.VerificationCheckingFailure _report (Verification.VerificationTypedModuleError _source (Module.TypedActionFailed (Module.TypedExactProofFailed (ExactProof.ExactProofElaborationFailed (Exact.ExactGlobalNotVisible location key)))) prefix) , _slowReport ) -> do assertEqual "missing ordered-pair provider line" 2 (locLine location) assertEqual "missing ordered-pair semantic key" (Semantic.SemanticExpressionFunction (Raw.mixfixPattern Raw.PairSymbol)) key assertEqual "missing provider publishes no declaration" 0 (length (Declaration.pendingModulePrefixBatches prefix)) Left err -> assertFailure ("unexpected relation-expression failure: " <> show err) Right{} -> assertFailure "relation expression without ordered pairing was admitted" resolvesSourceOwnedApplication :: Assertion resolvesSourceOwnedApplication = do foundation <- expectRight Foundation.checkedFoundation repository <- getCurrentDirectory withAcceptedFixtureVampire "felix-exact-application" \prover -> Temp.withSystemTempDirectory "felix-exact-application" \directory -> do let storePath = directory Posix. "store.sqlite" resolver = Declaration.vampireResolver (Provers.runPreparedTypedProver prover) bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) Store.closeStore \store -> do prelude <- expectRight =<< acquireFinalPreludeSession store foundation resolver mounts <- exactFixtureMounts repository workspace <- parseFinalExactWorkspace prelude mounts "test/phase5/exact-application.tex" sealed <- compileFinalParsedWorkspaceWithResolver foundation prelude resolver workspace root <- case reverse sealed of rootModule : _ -> pure rootModule [] -> assertFailure "application fixture root is absent" >> fail "unreachable" assertTransparentObjectAlias root "phase5_apply" let applyKey = Semantic.SemanticExpressionFunction (Raw.mixfixPattern Raw.ApplySymbol) applyObject <- localObjectKeyTarget root applyKey surface <- checkedPropositionTermByAlias root "phase5_application_surface" explicit <- checkedPropositionTermByAlias root "phase5_application_explicit" assertEqual "surface and explicit application lower identically" explicit surface assertBool "surface application resolves through the declared object" (applyObject `Set.member` Core.frozenCoreGlobals surface) missing <- withAcceptedFixtureVampire "felix-exact-application-missing" \prover -> (checkFileFresh prover "test/phase5/exact-application-missing.tex") case missing of Right ( Verification.VerificationCheckingFailure _report (Verification.VerificationTypedModuleError _source (Module.TypedActionFailed (Module.TypedExactProofFailed (ExactProof.ExactProofElaborationFailed (Exact.ExactGlobalNotVisible location key)))) prefix) , _slowReport ) -> do assertEqual "unresolved application line" 2 (locLine location) assertEqual "unresolved application key" (Semantic.SemanticExpressionFunction (Raw.mixfixPattern Raw.ApplySymbol)) key assertEqual "unresolved application publishes no declaration" 0 (length (Declaration.pendingModulePrefixBatches prefix)) Left failure -> assertFailure ("unexpected unresolved application failure: " <> show failure) Right{} -> assertFailure "application without its source binding was admitted" confinesExactQuantifiedTerms :: Assertion confinesExactQuantifiedTerms = do foundation <- expectRight Foundation.checkedFoundation repository <- getCurrentDirectory withAcceptedFixtureVampire "felix-exact-quantified-subject" \prover -> Temp.withSystemTempDirectory "felix-quantified-subject" \directory -> do let storePath = directory Posix. "store.sqlite" resolver = Declaration.vampireResolver (Provers.runPreparedTypedProver prover) bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) Store.closeStore \store -> do prelude <- expectRight =<< acquireFinalPreludeSession store foundation resolver mounts <- exactFixtureMounts repository workspace <- parseFinalExactWorkspace prelude mounts "test/phase5/exact-quantified-subject.tex" sealed <- compileFinalParsedWorkspaceWithResolver foundation prelude resolver workspace root <- case reverse sealed of rootModule : _ -> pure rootModule [] -> assertFailure "quantified-subject root is absent" >> fail "unreachable" quantified <- checkedPropositionTermByAlias root "phase5_quantified_subject" explicit <- checkedPropositionTermByAlias root "phase5_explicit_quantifier" assertEqual "quantified noun subject retains its domain constraint" explicit quantified propositionWorkspace <- parseFinalExactWorkspace prelude mounts "test/phase5/exact-quantified-proposition-terms.tex" observations <- newIORef [] let observingResolver = Declaration.vampireResolver \prepared -> do let problem = Provers.preparedTypedProverLogicalProblem prepared request = Provers.preparedTypedProverRequest prepared modifyIORef' observations (<> [ ( Provers.preparedVerificationRequestId request , Backend.supportedPropositionTerm (Backend.typedProblemClaim problem) , Backend.typedProblemRoute problem , Backend.typedProblemAuxiliaryTag <$> Vector.toList (Backend.typedProblemAuxiliaries problem) ) ]) (Provers.runPreparedTypedProver prover prepared) freshModules <- compileFinalParsedWorkspaceWithResolver foundation prelude observingResolver propositionWorkspace freshRoot <- case reverse freshModules of rootModule : _ -> pure rootModule [] -> assertFailure "quantified proposition-term root is absent" >> fail "unreachable" let member left right = Core.CApp (Core.CApp (Core.CIntrinsic Core.Member) left) right memberAtX = member (Core.CBound 0) (Core.CBound 1) expectedFunctionTarget = Core.CForall Core.TySet (Core.CEq Core.TySet (Core.CBound 0) (Core.CBound 0)) expectedVerbRequestTarget = Core.CForall Core.TySet (Core.CImp memberAtX memberAtX) expectedVerbProposition = Core.CForall Core.TySet (Core.CForall Core.TySet (Core.CImp memberAtX memberAtX)) expectedTargets = [ expectedFunctionTarget , expectedVerbRequestTarget ] ordinaryImplicitAuxiliaries = [ Foundation.EmptyCharacteristic , Foundation.PairSetCharacteristic , Foundation.FamilyUnionCharacteristic , Foundation.PowerSetCharacteristic ] freshObservations <- readIORef observations assertEqual "nested function and verb terms have exact FOF targets" [ ( target , Backend.RouteFof , ordinaryImplicitAuxiliaries ) | target <- expectedTargets ] [ (target, route, auxiliaries) | (_request, target, route, auxiliaries) <- freshObservations ] functionTarget <- checkedPropositionTermByAlias freshRoot "phase5_quantified_function_argument" verbTarget <- checkedPropositionTermByAlias freshRoot "phase5_quantified_verb_argument" assertEqual "nested function proposition core" expectedFunctionTarget (Core.frozenCoreTerm functionTarget) assertEqual "nested verb proposition core" expectedVerbProposition (Core.frozenCoreTerm verbTarget) let proofRecords moduleValue = concatMap Declaration.committedBatchProofValidations (Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix moduleValue)) proofAuthorizations moduleValue = Authority.validationDirectAuthorization . Semantic.proofValidationRecordCertificate <$> proofRecords moduleValue case proofAuthorizations freshRoot of [ Authority.CheckedSourceProof [_functionRequest] , Authority.CheckedSourceProof [_verbRequest] ] -> pure () authorizations -> assertFailure ("unexpected quantified-term authority: " <> show authorizations) assertBool "quantified terms add no escape-backed authority" (all ((== Authority.cleanAuthoritySafety) . Authority.factAuthoritySafety . Semantic.semanticFactAuthority) (concatMap (Semantic.declarationDeltaFacts . Declaration.committedBatchDelta) (Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix freshRoot)))) traverse_ (expectRightIO . Store.writePendingModulePrefix store . Module.sealedTypedModulePrefix) freshModules let validation = Declaration.WarmValidation (Declaration.validationLookup (expectRightIO . Store.loadProofValidation store) (expectRightIO . Store.loadDeclarationValidation store)) warmModules <- compileParsedWorkspaceWithReadiness foundation (Module.finalPreludeReadiness prelude) unusedResolver validation propositionWorkspace warmRoot <- case reverse warmModules of rootModule : _ -> pure rootModule [] -> assertFailure "warm quantified proposition-term root is absent" >> fail "unreachable" assertEqual "fresh and warm quantified semantic interface" (Module.sealedTypedModuleSemantic freshRoot) (Module.sealedTypedModuleSemantic warmRoot) assertEqual "fresh and warm quantified request authority" (proofAuthorizations freshRoot) (proofAuthorizations warmRoot) assertEqual "fresh and warm quantified prefix" (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix freshRoot)) (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix warmRoot)) negative <- withAcceptedFixtureVampire "felix-exact-quantified-term-valued" \prover -> (checkFileFresh prover "test/phase5/exact-quantified-term-valued.tex") case negative of Right ( Verification.VerificationCheckingFailure _report (Verification.VerificationTypedModuleError _source (Module.TypedActionFailed (Module.TypedExactCompileFailed (Exact.ExactQuantifiedTermRequiresPropositionContext location))) prefix) , _slowReport ) -> do assertEqual "term-valued quantified term line" 2 (locLine location) assertBool "failed term-valued abbreviation publishes no prefix" (null (Declaration.pendingModulePrefixBatches prefix)) Left failure -> assertFailure ("unexpected term-valued quantified-term failure: " <> show failure) Right{} -> assertFailure "term-valued quantified exact term was admitted" closesExactDefinitionDeclarationBoundary :: Assertion closesExactDefinitionDeclarationBoundary = do repository <- getCurrentDirectory foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver repositoryMounts <- exactFixtureMounts repository Temp.withSystemTempDirectory "felix-definition-boundary" \directory -> do mounts <- exactFixtureMounts directory annotatedText <- readFile (repository Posix. "test/phase5/exact-definition-boundary.tex") let relative = "entry.tex" sourcePath = directory Posix. relative unannotatedText = StrictText.unpack (StrictText.replace "A set " "" (StrictText.pack annotatedText)) writeFile sourcePath annotatedText annotatedWorkspace <- parseExactWorkspace bootstrap mounts relative annotated <- sole "annotated definition module" =<< compileParsedWorkspace foundation bootstrap annotatedWorkspace assertEqual "annotated definition declaration count" 4 (length (Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix annotated))) assertBool "annotated definitions prepare no Vampire validations" (null (proofValidationRecords annotated)) let annotatedBatches = Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix annotated) symbolicBatch <- sole "symbolic primary declaration" (take 1 (drop 2 annotatedBatches)) wrapperBatch <- sole "functional wrapper declaration" (take 1 (drop 3 annotatedBatches)) symbolicObject <- bindingObject "symbolic primary" symbolicBatch wrapperObject <- bindingObject "functional wrapper" wrapperBatch wrapperContent <- sole "functional wrapper transparent object" [ Identity.assertedObjectContent object | batch <- Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix annotated) , object <- Declaration.committedBatchObjects batch , Identity.assertedObjectId object == wrapperObject ] case wrapperContent of Identity.TransparentObjectContent _theory _type body -> assertEqual "functional wrapper applies the primary symbolic object" (Set.singleton symbolicObject) (Core.canonicalTermGlobals body) content -> assertFailure ("functional wrapper is not transparent: " <> show content) writeFile sourcePath unannotatedText unannotatedWorkspace <- parseExactWorkspace bootstrap mounts relative unannotated <- sole "unannotated definition module" =<< compileParsedWorkspace foundation bootstrap unannotatedWorkspace assertEqual "canonical set annotations do not change the semantic interface" (Module.sealedTypedModuleSemantic unannotated) (Module.sealedTypedModuleSemantic annotated) assertEqual "canonical set annotations do not change declaration identity" (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix unannotated)) (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix annotated)) assertEqual "canonical set annotations do not change direct authority" (directDeclarationAuthorizations unannotated) (directDeclarationAuthorizations annotated) let storePath = directory Posix. "store.sqlite" bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) Store.closeStore \store -> do expectRightIO (Store.writePendingModulePrefix store (Module.sealedTypedModulePrefix annotated)) let validation = Declaration.WarmValidation (Declaration.validationLookup (expectRightIO . Store.loadProofValidation store) (expectRightIO . Store.loadDeclarationValidation store)) warm <- sole "warm annotated definition module" =<< compileParsedWorkspaceWithValidation foundation bootstrap unusedResolver validation annotatedWorkspace assertEqual "warm annotated semantic interface" (Module.sealedTypedModuleSemantic annotated) (Module.sealedTypedModuleSemantic warm) assertEqual "warm annotated declaration identity" (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix annotated)) (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix warm)) assertEqual "warm annotated direct authority" (directDeclarationAuthorizations annotated) (directDeclarationAuthorizations warm) assertBool "warm annotated definitions run no prover" (null (proofValidationRecords warm)) annotationFailure <- exactFailure foundation bootstrap repositoryMounts "test/phase5/exact-definition-annotation-failure.tex" case annotationFailure of ( Exact.ExactNonCanonicalSetDefinitionAnnotation location , prefix ) -> do assertEqual "nontrivial annotation line" 2 (locLine location) assertBool "nontrivial annotation publishes no prefix" (null (Declaration.pendingModulePrefixBatches prefix)) assertBool "annotation diagnostic gives the explicit migration" ("total condition in the definiens" `StrictText.isInfixOf` Exact.renderExactCompileError (fst annotationFailure)) (failure, _prefix) -> assertFailure ("unexpected annotation failure: " <> show failure) aliasFailure <- exactFailure foundation bootstrap repositoryMounts "test/phase5/exact-definition-alias-failure.tex" case aliasFailure of (Exact.ExactDefinitionCombinedSymbolicAlias location, prefix) -> do assertEqual "combined symbolic alias line" 2 (locLine location) assertBool "combined symbolic alias publishes no prefix" (null (Declaration.pendingModulePrefixBatches prefix)) assertBool "combined alias diagnostic gives the wrapper migration" ("define the symbolic operator first" `StrictText.isInfixOf` Exact.renderExactCompileError (fst aliasFailure)) (failure, _prefix) -> assertFailure ("unexpected combined-alias failure: " <> show failure) guardFailure <- exactFailure foundation bootstrap repositoryMounts "test/phase5/exact-definition-guard-failure.tex" case guardFailure of (Exact.ExactGuardedTransparentDefinition location, prefix) -> do assertEqual "guarded definition line" 2 (locLine location) assertBool "guarded definition publishes no prefix" (null (Declaration.pendingModulePrefixBatches prefix)) assertBool "guard diagnostic gives the total-definition migration" ("where a corresponding opaque signature form exists" `StrictText.isInfixOf` Exact.renderExactCompileError (fst guardFailure)) (failure, _prefix) -> assertFailure ("unexpected guarded-definition failure: " <> show failure) assertRussellSetAnnotation bootstrap repository where proofValidationRecords moduleValue = concatMap Declaration.committedBatchProofValidations (Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix moduleValue)) directDeclarationAuthorizations moduleValue = [ Authority.validationDirectAuthorization certificate | batch <- Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix moduleValue) , validation <- maybeToList (Declaration.committedBatchDeclarationValidation batch) , certificate <- Semantic.declarationValidationRecordCertificates validation ] bindingObject label batch = do binding <- sole (label <> " semantic binding") (Semantic.semanticEnvironmentBindings (Semantic.declarationDeltaEnvironment (Declaration.committedBatchDelta batch))) pure (Semantic.semanticGlobalTargetObject (Semantic.semanticGlobalBindingTarget binding)) exactFailure foundation bootstrap mounts relative = do workspace <- parseExactWorkspace bootstrap mounts relative parsed <- sole "failed exact definition module" (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) input <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) unusedResolver Declaration.FreshValidation parsed []) Module.runTypedModule input >>= \case Module.TypedModuleFailed (Module.TypedActionFailed (Module.TypedExactCompileFailed failure)) prefix -> pure (failure, prefix) result -> assertFailure (case result of Module.TypedModuleSucceeded{} -> "expected exact definition failure, but the module succeeded" Module.TypedModuleOpenFailed{} -> "expected exact definition failure, but the module did not open" Module.TypedModuleFailed{} -> "expected an exact compile failure, but checking failed differently") >> fail "unreachable" assertRussellSetAnnotation bootstrap repository = do mounts <- exactFixtureMounts repository workspace <- parseExactWorkspace bootstrap mounts "test/examples/russell.tex" parsed <- sole "Russell parity module" (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) case Parse.identifiedParsedModuleBlocks (Module.identifiedModuleParsed (Module.identifiedPhysicalModule parsed)) of Raw.BlockDefn _location _title _marker (Raw.Defn [] (Raw.DefnAdj (Just (Raw.NounPhrase [] (Raw.Noun _ noun []) Nothing [] Nothing)) _subject _adjective) _statement) : _ -> assertBool "Russell uses the canonical built-in set noun" (Lexicon.isBuiltinSetNoun noun) _ -> assertFailure "Russell source does not retain its annotated adjective head" compilesExactOrdinaryProofs :: Assertion compilesExactOrdinaryProofs = Temp.withSystemTempDirectory "felix-exact-proofs" \root -> do repository <- getCurrentDirectory foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts repository workspace <- parseExactWorkspace bootstrap mounts "test/phase5/exact-proofs.tex" let executable = root Posix. "vampire" writeFile executable (unlines [ "#!/bin/sh" , "cat >/dev/null" , "printf '%s\\n' '% SZS status Theorem for exact-proof'" ]) permissions <- getPermissions executable setPermissions executable (setOwnerExecutable True permissions) observations <- newIORef [] let resolver = Declaration.vampireResolver \prepared -> do let problem = Provers.preparedTypedProverLogicalProblem prepared claim = Backend.typedProblemClaim problem locals = Backend.typedProblemLocalPremises problem modifyIORef' observations (<> [ ( Vector.length (Backend.typedProblemGlobalPremises problem) , Vector.length locals , [ Vector.length (Backend.supportedPropositionSupport (Backend.typedLocalPremiseProposition premise)) | premise <- Vector.toList locals ] , [ Backend.supportedPropositionTerm (Backend.typedLocalPremiseProposition premise) == Backend.supportedPropositionTerm claim | premise <- Vector.toList locals ] ) ]) (Provers.runPreparedTypedProver (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) sealed <- compileParsedWorkspaceWithResolver foundation bootstrap resolver workspace rootModule <- sole "exact proof root" (drop 1 sealed) let batches = Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix rootModule) assertEqual "one definition and five theorem declarations" 6 (length batches) let proofBatches = drop 1 batches assertEqual "only closed theorem facts are published" [1, 1, 1, 1, 1] [ length (Semantic.declarationDeltaFacts (Declaration.committedBatchDelta batch)) | batch <- proofBatches ] assertEqual "proof request aggregation follows source structure" [1, 2, 2, 1, 1] [ case Declaration.committedBatchProofValidations batch of [record] -> case Authority.validationDirectAuthorization (Semantic.proofValidationRecordCertificate record) of Authority.CheckedSourceProof requests -> length requests authorization -> error ("unexpected exact proof authority: " <> show authorization) records -> error ("unexpected exact proof validation count: " <> show (length records)) | batch <- proofBatches ] headerBatch <- sole "header-envelope proof batch" (take 1 (drop 3 proofBatches)) headerProposition <- sole "header-envelope checked proposition" (Declaration.committedBatchPropositions headerBatch) assertEqual "header-envelope closed target" (Core.CForall Core.TySet (Core.CForall Core.TySet (Core.CImp (member (Core.CBound 0) (Core.CBound 1)) (member (Core.CBound 0) (Core.CBound 1))))) (Core.frozenCoreTerm (Identity.checkedPropositionTerm headerProposition)) headerFact <- sole "header-envelope published fact" (Semantic.declarationDeltaFacts (Declaration.committedBatchDelta headerBatch)) assertEqual "header-envelope proof remains clean" Authority.cleanAuthoritySafety (Authority.factAuthoritySafety (Semantic.semanticFactAuthority headerFact)) observed <- readIORef observations case observed of (implicitGlobals, 0, [], []) : [ (0, 1, [1], _structuralMatches) , (1, 2, [1, 1], _subclaimMatches) , (0, 0, [], []) , (0, 1, [1], _followingMatches) , (0, 1, [2], [True]) , (generalizedGlobals, 0, [], []) ] -> do assertBool "implicit Auto selects visible FOF facts" (implicitGlobals > 0) assertBool "generalized Auto selects visible FOF facts" (generalizedGlobals > 0) _ -> assertFailure ("unexpected exact proof premise policies: " <> show observed) where member element set = Core.CApp (Core.CApp (Core.CIntrinsic Core.Member) element) set restoresExactBinderAndWitnessProofForms :: Assertion restoresExactBinderAndWitnessProofForms = Temp.withSystemTempDirectory "felix-exact-proof-parity" \root -> do repository <- getCurrentDirectory foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts repository workspace <- parseExactWorkspace bootstrap mounts "test/phase5/exact-proof-parity.tex" parsed <- sole "parsed proof-parity module" (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) let blocks = Parse.identifiedParsedModuleBlocks (Parse.parsedModuleIdentified parsed) claims = [claim | claim@Raw.BlockClaim{} <- blocks] proofs = [ proof | Raw.BlockProof _location proof _end <- blocks ] omittedClaim <- case reverse claims of claim : _ -> pure claim [] -> assertFailure "missing omitted witness claim" >> fail "unreachable" omittedProof <- case reverse proofs of proof : _ -> pure proof [] -> assertFailure "missing omitted witness proof" >> fail "unreachable" Declaration.runModuleDriver foundation preludeModuleName [] unusedResolver Declaration.FreshValidation do Declaration.runProspectiveLoweringDriver (ExactProof.prepareExactProof omittedClaim (Just omittedProof)) >>= either Declaration.failModuleDriver pure >>= \case Right (Declaration.DriverSucceeded prepared _semantic _prefix _closure) -> case ExactProof.preparedExactProofFirstOmission prepared of Just location -> assertEqual "nested Take retains first omission" 106 (locLine location) Nothing -> assertFailure "nested Take lost its omission" Right Declaration.DriverFailed{} -> assertFailure "omitted witness preparation failed" Right Declaration.DriverSealFailed{} -> assertFailure "omitted witness preparation did not seal" Left failure -> assertFailure ("omitted witness preparation did not open: " <> show failure) let executable = root Posix. "vampire" storePath = root Posix. "store.sqlite" writeFile executable (unlines [ "#!/bin/sh" , "cat >/dev/null" , "printf '%s\\n' '% SZS status Theorem for exact-proof-parity'" ]) permissions <- getPermissions executable setPermissions executable (setOwnerExecutable True permissions) observations <- newIORef [] fresh <- sole "proof-parity module" =<< compileParsedWorkspaceWithValidation foundation bootstrap (observingAcceptedResolver executable observations) Declaration.FreshValidation workspace observed <- readIORef observations assertEqual "restored proof request count" 17 (length observed) assertEqual "restored proof declarations preserve discharge order" [1, 1, 1, 1, 1, 1, 3, 2, 2, 3, 1] (proofRequestCounts fresh) case observed of first : second : third : fourth : _rest -> do assertGuardRequest "single bounded fix" 2 first assertGuardRequest "multiple bounded fix" 3 second assertGuardRequest "negative bounded fix" 2 third assertGuardRequest "fix such that" 2 fourth _ -> assertFailure "missing bounded-fix requests" case drop 4 observed of leftFirst : rightFirst : _ -> do assertSequentialAssumptions "left conjunct first" leftFirst assertSequentialAssumptions "right conjunct first" rightFirst _ -> assertFailure "missing conjunction-assumption requests" assertTakeSequence "bounded TakeVar" (drop 6 observed) assertTakeSequence "existential Have" (drop 13 observed) case drop 9 observed of namedDischarge : _namedFinal : anonymousDischarge : _ -> do assertExactDischarge "named noun" namedDischarge assertEqual "named noun opens two witness binders" 2 (leadingExistentials (observedClaimTerm namedDischarge)) assertExactDischarge "anonymous noun" anonymousDischarge assertEqual "anonymous noun opens one unnameable binder" 1 (leadingExistentials (observedClaimTerm anonymousDischarge)) _ -> assertFailure "missing noun-witness requests" lastBatch <- case reverse (Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix fresh)) of batch : _ -> pure batch [] -> assertFailure "missing restored-proof batches" >> fail "unreachable" lastFact <- sole "omitted witness fact" (Semantic.declarationDeltaFacts (Declaration.committedBatchDelta lastBatch)) assertEqual "omitted continuation remains escape-backed" (Authority.authoritySafety (Authority.singletonEscapeKind Authority.Omitted)) (Authority.factAuthoritySafety (Semantic.semanticFactAuthority lastFact)) assertBool "proof-local witnesses publish no objects" (all (null . Declaration.committedBatchObjects) (Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix fresh))) bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) Store.closeStore \store -> do expectRightIO (Store.writePendingModulePrefix store (Module.sealedTypedModulePrefix fresh)) let validation = Declaration.WarmValidation (Declaration.validationLookup (expectRightIO . Store.loadProofValidation store) (expectRightIO . Store.loadDeclarationValidation store)) warmRuns <- newIORef (0 :: Int) warm <- sole "warm proof-parity module" =<< compileParsedWorkspaceWithValidation foundation bootstrap (countingAcceptedResolver executable warmRuns) validation workspace assertEqual "warm restored proofs skip Vampire" 0 =<< readIORef warmRuns assertEqual "fresh and warm proof validation keys and authority" (proofValidationRecords fresh) (proofValidationRecords warm) assertEqual "fresh and warm checked proposition identities" (map Identity.checkedPropositionId (concatMap Declaration.committedBatchPropositions (Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix fresh)))) (map Identity.checkedPropositionId (concatMap Declaration.committedBatchPropositions (Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix warm)))) assertProofParityFailure foundation bootstrap mounts "test/phase5/exact-proof-parity-invalid-fix.tex" (\case ExactProof.ExactProofGoalStatementMismatch location -> locLine location == 6 _ -> False) assertProofParityFailure foundation bootstrap mounts "test/phase5/exact-proof-parity-invalid-fix-shape.tex" (\case ExactProof.ExactProofExpectedUniversalGoal location -> locLine location == 6 _ -> False) assertProofParityFailure foundation bootstrap mounts "test/phase5/exact-proof-parity-invalid-assume.tex" (\case ExactProof.ExactProofGoalStatementMismatch location -> locLine location == 6 _ -> False) where observingAcceptedResolver executable observations = Declaration.vampireResolver \prepared -> do let problem = Provers.preparedTypedProverLogicalProblem prepared claim = Backend.typedProblemClaim problem locals = Backend.typedProblemLocalPremises problem observation = ProofParityObservation (snd <$> Vector.toList (Backend.supportedPropositionSupport claim)) (Backend.supportedPropositionTerm claim) [ ( Backend.localPremiseOrdinalValue (Backend.typedLocalPremiseOrdinal premise) , snd <$> Vector.toList (Backend.supportedPropositionSupport (Backend.typedLocalPremiseProposition premise)) , Backend.supportedPropositionTerm (Backend.typedLocalPremiseProposition premise) ) | premise <- Vector.toList locals ] modifyIORef' observations (<> [observation]) (Provers.runPreparedTypedProver (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) assertGuardRequest label supportCount observation = do assertEqual (label <> " support") supportCount (length (observedClaimSupport observation)) case observedLocals observation of [(_ordinal, _support, local)] -> assertEqual (label <> " exact guard") (observedClaimTerm observation) local locals -> assertFailure (label <> ": expected one guard, found " <> show (length locals)) assertTakeSequence label observations = case observations of discharge : continuation : _ -> do assertExactDischarge label discharge assertEqual (label <> " continuation premise ordinals") [0, 1] [ ordinal | (ordinal, _support, _term) <- observedLocals continuation ] assertEqual (label <> " continuation witness support") 2 (length (observedClaimSupport continuation)) _ -> assertFailure (label <> ": missing request sequence") assertSequentialAssumptions label observation = do assertEqual (label <> " premise ordinals") [0, 1] [ ordinal | (ordinal, _support, _term) <- observedLocals observation ] case observedLocals observation of (_ordinal, _support, first) : _ -> assertEqual (label <> " retained source order") (observedClaimTerm observation) first [] -> assertFailure (label <> ": no scoped assumptions") assertExactDischarge label discharge = case observedLocals discharge of [(_ordinal, _support, local)] -> assertEqual (label <> " exact existential discharge") (observedClaimTerm discharge) local locals -> assertFailure (label <> ": unexpected discharge premises " <> show (length locals)) proofRequestCounts sealed = [ case Declaration.committedBatchProofValidations batch of [record] -> case Authority.validationDirectAuthorization (Semantic.proofValidationRecordCertificate record) of Authority.CheckedSourceProof requests -> length requests Authority.OmittedAuthorization -> 1 authorization -> error ("unexpected restored-proof authority: " <> show authorization) records -> error ("unexpected restored-proof validation count: " <> show (length records)) | batch <- Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix sealed) ] proofValidationRecords sealed = concatMap Declaration.committedBatchProofValidations (Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix sealed)) leadingExistentials :: Core.CanonicalTerm Identity.ObjectId -> Int leadingExistentials = \case Core.CImp (Core.CForall Core.TySet (Core.CImp body Core.CFalsum)) Core.CFalsum -> 1 + leadingExistentials body _ -> 0 data ProofParityObservation = ProofParityObservation { observedClaimSupport :: ![Core.CoreType] , observedClaimTerm :: !(Core.CanonicalTerm Identity.ObjectId) , observedLocals :: ![(Natural, [Core.CoreType], Core.CanonicalTerm Identity.ObjectId)] } restoresExactLocalReasoningAndCalculations :: Assertion restoresExactLocalReasoningAndCalculations = Temp.withSystemTempDirectory "felix-exact-local-reasoning" \root -> do repository <- getCurrentDirectory foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts repository workspace <- parseExactWorkspace bootstrap mounts "test/phase5/exact-proof-local-reasoning.tex" let executable = root Posix. "vampire" storePath = root Posix. "store.sqlite" writeAcceptedFixtureVampire executable observations <- newIORef [] fresh <- sole "exact local-reasoning module" =<< compileParsedWorkspaceWithValidation foundation bootstrap (observingResolver executable observations) Declaration.FreshValidation workspace observed <- readIORef observations assertEqual "local-reasoning request count" 16 (length observed) assertEqual "proof forms retain source request order" [2, 3, 3, 2, 2, 3, 1] (requestCounts fresh) case observed of sufficesImplication : sufficesReduction : equalityFirst : equalitySecond : equalityContinuation : biconditionalFirst : biconditionalSecond : biconditionalContinuation : quantifiedLink : quantifiedContinuation : sinceStructuralClaim : sinceStructuralContinuation : sinceDischarge : sinceClaim : sinceContinuation : _omittedSufficesImplication : [] -> do case localReasoningTarget sufficesImplication of Core.CImp antecedent conclusion -> do assertEqual "Suffices implication starts from the reduction" (localReasoningTarget sufficesReduction) antecedent assertBool "Suffices keeps its distinct current goal as conclusion" (conclusion /= antecedent) implication -> assertFailure ("expected Suffices implication, found " <> show implication) assertEqual "first equality link uses its destination citation" 1 (localReasoningGlobalCount equalityFirst) assertEqual "second equality link uses local-only justification" 0 (localReasoningGlobalCount equalitySecond) assertDerivedContinuation "equality calculation" [0, 1] (localReasoningTarget equalityContinuation) equalityContinuation assertPairwiseDistinct "equality links and endpoint" [ localReasoningTarget equalityFirst , localReasoningTarget equalitySecond , localReasoningTarget equalityContinuation ] assertEqual "first biconditional link remains proposition equality" Core.TyProp (equalityOperandType (localReasoningTarget biconditionalFirst)) assertDerivedContinuation "biconditional calculation" [0] (localReasoningTarget biconditionalContinuation) biconditionalContinuation assertPairwiseDistinct "biconditional links and endpoint" [ localReasoningTarget biconditionalFirst , localReasoningTarget biconditionalSecond , localReasoningTarget biconditionalContinuation ] assertEqual "quantified calculation closes both binders" 2 (leadingForalls (localReasoningTarget quantifiedLink)) assertQuantifiedCalculationGuard (localReasoningTarget quantifiedLink) assertDerivedContinuation "quantified calculation" [0] (localReasoningTarget quantifiedLink) quantifiedContinuation assertEqual "quantified source goal and derived local retain the same guard shape" (quantifiedCalculationShape (localReasoningTarget quantifiedContinuation)) (quantifiedCalculationShape (localReasoningTarget quantifiedLink)) assertQuantifiedCalculationGuard (localReasoningTarget quantifiedContinuation) assertEqual "structural Since submits no premise discharge" [0] (localReasoningLocalOrdinals sinceStructuralClaim) assertEqual "structural Since does not duplicate its premise" [0, 1] (localReasoningLocalOrdinals sinceStructuralContinuation) assertEqual "ATP-backed Since starts from existing locals only" [0] (localReasoningLocalOrdinals sinceDischarge) assertEqual "Since claim sees the admitted discourse premise" [0, 1] (localReasoningLocalOrdinals sinceClaim) assertEqual "Since continuation sees premise then claim" [0, 1, 2] (localReasoningLocalOrdinals sinceContinuation) assertEqual "local-only Since requests select no globals" [0, 0, 0] (localReasoningGlobalCount <$> [sinceDischarge, sinceClaim, sinceContinuation]) assertEqual "biconditional second link keeps local-only policy" 0 (localReasoningGlobalCount biconditionalSecond) _ -> assertFailure ("unexpected local-reasoning observations: " <> show observed) omittedBatch <- sole "omitted Suffices batch" (take 1 (reverse (Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix fresh)))) omittedFact <- sole "omitted Suffices fact" (Semantic.declarationDeltaFacts (Declaration.committedBatchDelta omittedBatch)) assertEqual "Suffices continuation omission reaches final authority" (Authority.authoritySafety (Authority.singletonEscapeKind Authority.Omitted)) (Authority.factAuthoritySafety (Semantic.semanticFactAuthority omittedFact)) bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) Store.closeStore \store -> do expectRightIO (Store.writePendingModulePrefix store (Module.sealedTypedModulePrefix fresh)) let validation = Declaration.WarmValidation (Declaration.validationLookup (expectRightIO . Store.loadProofValidation store) (expectRightIO . Store.loadDeclarationValidation store)) warmRuns <- newIORef (0 :: Int) warm <- sole "warm local-reasoning module" =<< compileParsedWorkspaceWithValidation foundation bootstrap (countingAcceptedResolver executable warmRuns) validation workspace assertEqual "warm local-reasoning validation skips Vampire" 0 =<< readIORef warmRuns assertEqual "fresh and warm local-reasoning validations" (validationRecords fresh) (validationRecords warm) assertRejectedPrefix "Suffices implication failure" foundation bootstrap workspace executable 0 0 1 assertRejectedPrefix "Suffices reduction failure" foundation bootstrap workspace executable 1 0 2 assertRejectedPrefix "middle calculation link failure" foundation bootstrap workspace executable 3 1 4 where observingResolver executable observations = Declaration.vampireResolver \prepared -> do let problem = Provers.preparedTypedProverLogicalProblem prepared claim = Backend.typedProblemClaim problem locals = Backend.typedProblemLocalPremises problem observation = LocalReasoningObservation { localReasoningTarget = Backend.supportedPropositionTerm claim , localReasoningGlobalCount = Vector.length (Backend.typedProblemGlobalPremises problem) , localReasoningLocalOrdinals = [ Backend.localPremiseOrdinalValue (Backend.typedLocalPremiseOrdinal premise) | premise <- Vector.toList locals ] , localReasoningLocalTerms = [ Backend.supportedPropositionTerm (Backend.typedLocalPremiseProposition premise) | premise <- Vector.toList locals ] , localReasoningAuxiliaries = Backend.typedProblemAuxiliaryTag <$> Vector.toList (Backend.typedProblemAuxiliaries problem) } modifyIORef' observations (<> [observation]) (Provers.runPreparedTypedProver (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) requestCounts sealed = [ case Declaration.committedBatchProofValidations batch of [record] -> case Authority.validationDirectAuthorization (Semantic.proofValidationRecordCertificate record) of Authority.CheckedSourceProof requests -> length requests Authority.OmittedAuthorization -> 1 direct -> error ("unexpected local-reasoning authority: " <> show direct) records -> error ("unexpected local-reasoning validation count: " <> show (length records)) | batch <- Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix sealed) ] validationRecords = concatMap Declaration.committedBatchProofValidations . Declaration.pendingModulePrefixBatches . Module.sealedTypedModulePrefix assertDerivedContinuation label expectedOrdinals expectedEndpoint continuation = do assertEqual (label <> " local source ordinals") expectedOrdinals (localReasoningLocalOrdinals continuation) case reverse (localReasoningLocalTerms continuation) of derived : _ -> assertEqual (label <> " derived endpoint") expectedEndpoint derived [] -> assertFailure (label <> ": continuation has no derived endpoint") assertPairwiseDistinct label terms = assertEqual (label <> ": " <> show terms) (length terms) (Set.size (Set.fromList terms)) assertQuantifiedCalculationGuard proposition = case dropForalls 2 proposition of Core.CImp constraint endpoint -> do assertEqual "quantified guard retains both membership bounds" 2 (countIntrinsic Core.Member constraint) assertEqual "quantified guard retains its such-that equality" 1 (countSetEqualities constraint) case endpoint of Core.CEq Core.TySet (Core.CBound left) (Core.CBound right) -> assertBool "quantified endpoint keeps asymmetric binders" (left /= right) _ -> assertFailure ("unexpected quantified endpoint: " <> show endpoint) target -> assertFailure ("expected quantified guarded implication, found " <> show target) quantifiedCalculationShape proposition = case dropForalls 2 proposition of Core.CImp constraint endpoint -> Just ( countIntrinsic Core.Member constraint , countSetEqualities constraint , endpoint ) _ -> Nothing dropForalls :: Int -> Core.CanonicalTerm Identity.ObjectId -> Core.CanonicalTerm Identity.ObjectId dropForalls 0 term = term dropForalls remaining (Core.CForall _binder body) = dropForalls (remaining - 1) body dropForalls _remaining term = term countIntrinsic :: Core.CoreIntrinsicTag -> Core.CanonicalTerm Identity.ObjectId -> Int countIntrinsic intrinsic = \case Core.CBound{} -> 0 Core.CGlobal{} -> 0 Core.CIntrinsic found -> fromEnum (found == intrinsic) Core.COpaqueInteger{} -> 0 Core.CApp function argument -> countIntrinsic intrinsic function + countIntrinsic intrinsic argument Core.CLam _binder body -> countIntrinsic intrinsic body Core.CFalsum -> 0 Core.CImp premise conclusion -> countIntrinsic intrinsic premise + countIntrinsic intrinsic conclusion Core.CEq _operand left right -> countIntrinsic intrinsic left + countIntrinsic intrinsic right Core.CForall _binder body -> countIntrinsic intrinsic body countSetEqualities :: Core.CanonicalTerm Identity.ObjectId -> Int countSetEqualities = \case Core.CBound{} -> 0 Core.CGlobal{} -> 0 Core.CIntrinsic{} -> 0 Core.COpaqueInteger{} -> 0 Core.CApp function argument -> countSetEqualities function + countSetEqualities argument Core.CLam _binder body -> countSetEqualities body Core.CFalsum -> 0 Core.CImp premise conclusion -> countSetEqualities premise + countSetEqualities conclusion Core.CEq operand left right -> fromEnum (operand == Core.TySet) + countSetEqualities left + countSetEqualities right Core.CForall _binder body -> countSetEqualities body equalityOperandType = \case Core.CEq operandType _left _right -> operandType term -> error ("expected checked equality, found " <> show term) leadingForalls :: Core.CanonicalTerm Identity.ObjectId -> Int leadingForalls = \case Core.CForall _binder body -> 1 + leadingForalls body _ -> 0 assertRejectedPrefix label foundation bootstrap workspace executable rejectedIndex expectedPrefix expectedRuns = do runs <- newIORef (0 :: Int) parsed <- sole (label <> " parsed module") (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) let resolver = Declaration.vampireResolver \prepared -> do index <- atomicModifyIORef' runs \current -> (current + 1, current) if index == rejectedIndex then pure (Right (Provers.CounterSatisfiable "focused deterministic rejection")) else (Provers.runPreparedTypedProver (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) input <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) resolver Declaration.FreshValidation parsed []) Module.runTypedModule input >>= \case Module.TypedModuleFailed _failure prefix -> assertEqual (label <> " publishes only the prior prefix") expectedPrefix (length (Declaration.pendingModulePrefixBatches prefix)) Module.TypedModuleSucceeded{} -> assertFailure (label <> " unexpectedly succeeded") Module.TypedModuleOpenFailed failure -> assertFailure (label <> " did not open: " <> show failure) assertEqual (label <> " selects the first rejected request") expectedRuns =<< readIORef runs data LocalReasoningObservation = LocalReasoningObservation { localReasoningTarget :: !(Core.CanonicalTerm Identity.ObjectId) , localReasoningGlobalCount :: !Int , localReasoningLocalOrdinals :: ![Natural] , localReasoningLocalTerms :: ![Core.CanonicalTerm Identity.ObjectId] , localReasoningAuxiliaries :: ![Foundation.FoundationAxiomTag] } deriving (Show) selectsCalculationLinkFailureBySourceOrder :: Assertion selectsCalculationLinkFailureBySourceOrder = do foundation <- expectRight Foundation.checkedFoundation Temp.withSystemTempDirectory "felix-calculation-link-order" \root -> do let executable = root Posix. "vampire" storePath = root Posix. "store.sqlite" source = "test/phase7/calculation-link-order.tex" laterCompleted = root Posix. "later-completed" firstRun = root Posix. "first-run" secondRun = root Posix. "second-run" prover = Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit writeAcceptedFixtureVampire executable (_startup, store) <- Store.openStore storePath (Identity.theoryId foundation) >>= expectRight bracket (pure store) Store.closeStore \openStore -> do let ignored = Verification.verificationRequestObserver (\_position _request -> pure ()) void ( (checkFileWithStore openStore Verification.WarmStoreValidation ignored prover "test/phase3/typed-unsupported.tex") >>= expectRight) writeFile executable (unlines [ "#!/bin/sh" , "cat >/dev/null" , "if mkdir \"" <> firstRun <> "\" 2>/dev/null; then" , " printf '%s\\n' '% SZS status Theorem for calculation-link-order'" , "elif mkdir \"" <> secondRun <> "\" 2>/dev/null; then" , " : > \"" <> laterCompleted <> "\"" , " printf '%s\\n' '% SZS status Theorem for calculation-link-order'" , "else" , " printf '%s\\n' '% SZS status CounterSatisfiable for calculation-link-order'" , "fi" ]) permissions <- getPermissions executable setPermissions executable (setOwnerExecutable True permissions) jobs <- Provers.selectEffectiveJobs (Provers.effectiveJobs 2) (fail "explicit jobs unexpectedly detected processors") positions <- newIORef [] middleStarted <- newEmptyTMVarIO laterStarted <- newEmptyTMVarIO releaseMiddle <- newEmptyTMVarIO let observer = Verification.verificationRequestObserver \position _request -> do let ordinal = Provers.workPositionLocalRequestOrdinal position modifyIORef' positions (position :) case ordinal of 1 -> pure () 2 -> do atomically (putTMVar middleStarted ()) atomically (takeTMVar releaseMiddle) 3 -> atomically (putTMVar laterStarted ()) _ -> assertFailure ("unexpected calculation request ordinal: " <> show ordinal) withAsync ( (checkFileWithStoreAndJobs openStore Verification.WarmStoreValidation jobs observer prover source) >>= expectRight) \verification -> do void (awaitTmvar "middle calculation link" middleStarted) void (awaitTmvar "later calculation continuation" laterStarted) waitForFileSignal "later calculation continuation" laterCompleted atomically (putTMVar releaseMiddle ()) (result, _slowReport) <- wait verification case result of Verification.VerificationFailure report failed -> do assertEqual "middle link failure location" (source, 10) ( locFile (Verification.failedVerificationLocation failed) , locLine (Verification.failedVerificationLocation failed) ) assertEqual "failed calculation admits no source fact" [] (Verification.verificationDirectEscapes report) other -> assertFailure ("calculation link order did not reject: " <> show other) observedPositions <- fmap (\position -> ( Provers.workPositionModuleOrdinal position , Provers.workPositionLocalRequestOrdinal position )) <$> readIORef positions assertEqual "all calculation requests executed" [(1, 1), (1, 2), (1, 3)] (sort observedPositions) writeAcceptedFixtureVampire executable retryPositions <- newIORef [] let retryObserver = Verification.verificationRequestObserver \position _request -> modifyIORef' retryPositions (position :) (retry, _retrySlowReport) <- (checkFileWithStoreAndJobs openStore Verification.WarmStoreValidation jobs retryObserver prover source) >>= expectRight case retry of Verification.VerificationCompleted{} -> pure () other -> assertFailure ("calculation rollback retry failed: " <> show other) retryObserved <- readIORef retryPositions assertEqual "retry executes the complete calculation proof" 3 (length retryObserved) where awaitTmvar label variable = do result <- Timeout.timeout 10000000 (atomically (takeTMVar variable)) maybe (assertFailure (label <> " was not observed") >> fail "unreachable") pure result assertProofParityFailure :: Foundation.CheckedFoundation -> Module.BootstrapPreludeFixture -> SourceMounts -> FilePath -> (ExactProof.ExactProofError -> Bool) -> Assertion assertProofParityFailure foundation bootstrap mounts relative matches = do workspace <- parseExactWorkspace bootstrap mounts relative parsed <- sole "invalid proof-parity module" (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) input <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) unusedResolver Declaration.FreshValidation parsed []) Module.runTypedModule input >>= \case Module.TypedModuleFailed (Module.TypedActionFailed (Module.TypedExactProofFailed failure)) prefix -> do assertBool ("unexpected proof failure: " <> show failure) (matches failure) assertBool "failing proof publishes no declaration" (null (Declaration.pendingModulePrefixBatches prefix)) Module.TypedModuleSucceeded{} -> assertFailure "invalid proof-parity module succeeded" Module.TypedModuleOpenFailed failure -> assertFailure ("invalid proof-parity module did not open: " <> show failure) Module.TypedModuleFailed failure _prefix -> assertFailure ("unexpected proof-parity module failure: " <> show failure) compilesExactSeparationComprehensions :: Assertion compilesExactSeparationComprehensions = Temp.withSystemTempDirectory "felix-exact-separation" \root -> do let relative = "test/phase5/exact-separation.tex" executable = root Posix. "vampire" failedSource = root Posix. relative repository <- getCurrentDirectory foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts repository workspace <- parseExactWorkspace bootstrap mounts relative writeFile executable (unlines [ "#!/bin/sh" , "cat >/dev/null" , "printf '%s\\n' '% SZS status Theorem for exact-separation'" ]) permissions <- getPermissions executable setPermissions executable (setOwnerExecutable True permissions) observations <- newIORef [] let resolver = Declaration.vampireResolver \prepared -> do let problem = Provers.preparedTypedProverLogicalProblem prepared request = Provers.preparedTypedProverRequest prepared globals = Backend.typedProblemGlobalPremises problem modifyIORef' observations (<> [ ( Backend.typedProblemRoute problem , Backend.typedBackendFactReference <$> globals , all (\fact -> case Backend.typedBackendFactCapability fact of Backend.FofProjectable{} -> True Backend.RequiresTh0{} -> False) globals , Backend.localPremiseOrdinalValue . Backend.typedLocalPremiseOrdinal <$> Vector.toList (Backend.typedProblemLocalPremises problem) , Backend.typedProblemAuxiliaryTag <$> Vector.toList (Backend.typedProblemAuxiliaries problem) , Provers.preparedVerificationRequestId request , Provers.preparedVerificationByteCount request ) ]) (Provers.runPreparedTypedProver (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) modules <- compileParsedWorkspaceWithResolver foundation bootstrap resolver workspace sealed <- sole "exact separation module" modules assertExactSeparationModule "fresh" sealed definition <- batchByAlias (Module.sealedTypedModulePrefix sealed) "phase5_separation_definition" let definitionFacts = Semantic.declarationDeltaFacts (Declaration.committedBatchDelta definition) extensional <- sole "searchable separation view" [ Semantic.semanticFactFingerprint occurrence | occurrence <- definitionFacts , Semantic.semanticFactSearchEligibility occurrence == Semantic.SearchEligible ] equation <- sole "explicit separation equation" [ Semantic.semanticFactFingerprint occurrence | occurrence <- definitionFacts , Semantic.semanticFactSearchEligibility occurrence == Semantic.SearchIneligible ] readIORef observations >>= \case [ ( Backend.RouteFof , selectedGlobals , True , [0] , [] , _requestId , requestBytes ) ] -> do assertBool "searchable separation view is selected" (extensional `elem` selectedGlobals) assertBool "exact separation equation is not selected" (equation `notElem` selectedGlobals) assertBool "separation exact request has bytes" (requestBytes > 0) observed -> assertFailure ("unexpected implicit separation problem: " <> show observed) createDirectoryIfMissing True (Posix.takeDirectory failedSource) original <- ByteString.readFile relative let invalid = Text.encodeUtf8 (StrictText.replace "x \\in A \\mid x = x" "x \\in x \\mid x = x" (Text.decodeUtf8 original)) ByteString.writeFile failedSource invalid failedMounts <- exactFixtureMounts root failedWorkspace <- parseExactWorkspace bootstrap failedMounts relative let parsed = Parse.parsedWorkspaceRootModule failedWorkspace input <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) unusedResolver Declaration.FreshValidation parsed []) Module.runTypedModule input >>= \case Module.TypedModuleFailed (Module.TypedActionFailed (Module.TypedExactCompileFailed (Exact.ExactFreeVariable location (Raw.NamedVar "x")))) prefix -> do assertEqual "invalid separation bound line" 2 (locLine location) assertEqual "invalid separation publishes none of its declaration" 0 (length (Declaration.pendingModulePrefixBatches prefix)) Module.TypedModuleSucceeded{} -> assertFailure "invalid separation was accepted" Module.TypedModuleOpenFailed failure -> assertFailure ("invalid separation module did not open: " <> show failure) Module.TypedModuleFailed failure _prefix -> assertFailure ("unexpected invalid separation failure: " <> show failure) compilesAndReusesProofLocalSetDefinitions :: Assertion compilesAndReusesProofLocalSetDefinitions = Temp.withSystemTempDirectory "felix-exact-local-definition" \root -> do let relative = "test/phase5/exact-local-definition.tex" failedRelative = "test/phase5/exact-local-definition-failure.tex" sourcePath = root Posix. relative failedSourcePath = root Posix. failedRelative executable = root Posix. "vampire" storePath = root Posix. "store.sqlite" createDirectoryIfMissing True (Posix.takeDirectory sourcePath) ByteString.readFile relative >>= ByteString.writeFile sourcePath createDirectoryIfMissing True (Posix.takeDirectory failedSourcePath) ByteString.readFile failedRelative >>= ByteString.writeFile failedSourcePath writeAcceptedFixtureVampire executable foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts root workspace <- parseExactWorkspace bootstrap mounts relative freshRuns <- newIORef (0 :: Int) observations <- newIORef [] let freshResolver = Declaration.vampireResolver \prepared -> do modifyIORef' freshRuns (+ 1) let problem = Provers.preparedTypedProverLogicalProblem prepared premises = Backend.typedProblemLocalPremises problem definition = Vector.find ((== Backend.localPremiseOrdinal 0) . Backend.typedLocalPremiseOrdinal) premises modifyIORef' observations (<> [ ( Backend.typedProblemRoute problem , Backend.localPremiseOrdinalValue . Backend.typedLocalPremiseOrdinal <$> Vector.toList premises , fmap localDefinitionShape definition ) ]) (Provers.runPreparedTypedProver (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) freshModules <- compileParsedWorkspaceWithValidation foundation bootstrap freshResolver Declaration.FreshValidation workspace assertEqual "fresh local-definition discharge count" 2 =<< readIORef freshRuns assertEqual "implicit and local-only definition views" [ (Backend.RouteFof, [0, 2], Just expectedLocalDefinitionShape) , (Backend.RouteTh0, [0, 1, 3], Just expectedLocalDefinitionShape) ] =<< readIORef observations fresh <- sole "fresh local-definition module" freshModules localDefinitionBatch <- sole "proof-local definition publishes one declaration" (Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix fresh)) assertEqual "proof-local definition publishes no object" [] (Declaration.committedBatchObjects localDefinitionBatch) assertEqual "proof-local definition publishes only its theorem" 1 (length (Declaration.committedBatchPropositions localDefinitionBatch)) localDefinitionFact <- sole "proof-local definition theorem" (Semantic.declarationDeltaFacts (Declaration.committedBatchDelta localDefinitionBatch)) assertEqual "proof-local definition remains clean" Authority.cleanAuthoritySafety (Authority.factAuthoritySafety (Semantic.semanticFactAuthority localDefinitionFact)) bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) Store.closeStore \store -> do expectRightIO (Store.writePendingModulePrefix store (Module.sealedTypedModulePrefix fresh)) let validation = Declaration.WarmValidation (Declaration.validationLookup (expectRightIO . Store.loadProofValidation store) (expectRightIO . Store.loadDeclarationValidation store)) warmRuns <- newIORef (0 :: Int) warmModules <- compileParsedWorkspaceWithValidation foundation bootstrap (countingAcceptedResolver executable warmRuns) validation workspace assertEqual "warm local-definition proof skips Vampire" 0 =<< readIORef warmRuns warm <- sole "warm local-definition module" warmModules assertEqual "warm local-definition semantic interface" (Module.sealedTypedModuleSemantic fresh) (Module.sealedTypedModuleSemantic warm) assertEqual "warm local-definition prefix" (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix fresh)) (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix warm)) failedWorkspace <- parseExactWorkspace bootstrap mounts failedRelative let failedParsed = Parse.parsedWorkspaceRootModule failedWorkspace failedInput <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) unusedResolver Declaration.FreshValidation failedParsed []) Module.runTypedModule failedInput >>= \case Module.TypedModuleFailed (Module.TypedActionFailed (Module.TypedExactProofFailed (ExactProof.ExactProofElaborationFailed (Exact.ExactFreeVariable location (Raw.NamedVar "B"))))) prefix -> do assertEqual "self-reference rejection line" 6 (locLine location) assertBool "failed local definition publishes no theorem" (null (Declaration.pendingModulePrefixBatches prefix)) Module.TypedModuleSucceeded{} -> assertFailure "self-referential local definition was accepted" Module.TypedModuleOpenFailed failure -> assertFailure ("local-definition failure fixture did not open: " <> show failure) Module.TypedModuleFailed failure _prefix -> assertFailure ("unexpected local-definition failure: " <> show failure) where localDefinitionShape premise = let proposition = Backend.typedLocalPremiseProposition premise in ( fmap snd (Vector.toList (Backend.supportedPropositionSupport proposition)) , Backend.supportedPropositionTerm proposition ) expectedLocalDefinitionShape = ( [Core.TySet, Core.TySet] , Core.CForall Core.TySet (Core.CEq Core.TyProp (member (Core.CBound 0) (Core.CBound 1)) (andP (member (Core.CBound 0) (Core.CBound 2)) (Core.CEq Core.TySet (Core.CBound 0) (Core.CBound 0)))) ) member element set = Core.CApp (Core.CApp (Core.CIntrinsic Core.Member) element) set andP left right = Core.CImp (Core.CImp left (Core.CImp right Core.CFalsum)) Core.CFalsum compilesAndReusesProofLocalFunctionGraphs :: Assertion compilesAndReusesProofLocalFunctionGraphs = Temp.withSystemTempDirectory "felix-exact-local-function" \root -> do let relative = "test/phase5/exact-local-function.tex" failedRelative = "test/phase5/exact-local-function-failure.tex" executable = root Posix. "vampire" storePath = root Posix. "store.sqlite" writeAcceptedFixtureVampire executable foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts =<< getCurrentDirectory workspace <- parseExactWorkspace bootstrap mounts relative observations <- newIORef [] let resolver = Declaration.vampireResolver \prepared -> do let problem = Provers.preparedTypedProverLogicalProblem prepared premises = [ ( Backend.typedProblemRoute problem , fmap snd (Vector.toList (Backend.supportedPropositionSupport proposition)) , Backend.supportedPropositionTerm proposition ) | premise <- Vector.toList (Backend.typedProblemLocalPremises problem) , let proposition = Backend.typedLocalPremiseProposition premise ] modifyIORef' observations (<> premises) (Provers.runPreparedTypedProver (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) freshModules <- compileParsedWorkspaceWithValidation foundation bootstrap resolver Declaration.FreshValidation workspace allObserved <- readIORef observations let observed = [ (route, proposition) | (route, support, proposition) <- allObserved , support == [Core.TySet, Core.TySet] , isJust (localFunctionPair proposition) ] assertBool ("the local graph characteristic reaches a discharge: " <> show allObserved) (not (null observed)) for_ observed \(route, proposition) -> do assertEqual "local function characteristic stays on FOF" Backend.RouteFof route assertExactLocalFunctionCharacteristic proposition freshRoot <- sole "fresh local-function root" (take 1 (reverse freshModules)) rootBatch <- sole "local function publishes only its theorem" (drop 1 (Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix freshRoot))) assertEqual "local function publishes no object" [] (Declaration.committedBatchObjects rootBatch) assertEqual "local function publishes only its theorem" 1 (length (Declaration.committedBatchPropositions rootBatch)) assertEqual "local function publishes no semantic binding" [] (Semantic.semanticEnvironmentBindings (Semantic.declarationDeltaEnvironment (Declaration.committedBatchDelta rootBatch))) rootFact <- sole "local-function theorem" (Semantic.declarationDeltaFacts (Declaration.committedBatchDelta rootBatch)) assertEqual "local-function theorem remains clean" Authority.cleanAuthoritySafety (Authority.factAuthoritySafety (Semantic.semanticFactAuthority rootFact)) bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) Store.closeStore \store -> do traverse_ (expectRightIO . Store.writePendingModulePrefix store . Module.sealedTypedModulePrefix) freshModules let validation = Declaration.WarmValidation (Declaration.validationLookup (expectRightIO . Store.loadProofValidation store) (expectRightIO . Store.loadDeclarationValidation store)) warmRuns <- newIORef (0 :: Int) warmModules <- compileParsedWorkspaceWithValidation foundation bootstrap (countingAcceptedResolver executable warmRuns) validation workspace assertEqual "warm local-function graph skips Vampire" 0 =<< readIORef warmRuns warmRoot <- sole "warm local-function root" (take 1 (reverse warmModules)) assertEqual "warm local-function semantic interface" (Module.sealedTypedModuleSemantic freshRoot) (Module.sealedTypedModuleSemantic warmRoot) assertEqual "warm local-function prefix" (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix freshRoot)) (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix warmRoot)) failedWorkspace <- parseExactWorkspace bootstrap mounts failedRelative failedInput <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) unusedResolver Declaration.FreshValidation (Parse.parsedWorkspaceRootModule failedWorkspace) []) Module.runTypedModule failedInput >>= \case Module.TypedModuleFailed (Module.TypedActionFailed (Module.TypedExactProofFailed (ExactProof.ExactProofElaborationFailed (Exact.ExactFreeVariable location (Raw.NamedVar "f"))))) prefix -> do assertEqual "self-reference rejection line" 6 (locLine location) assertBool "failed local function publishes no theorem" (null (Declaration.pendingModulePrefixBatches prefix)) Module.TypedModuleSucceeded{} -> assertFailure "self-referential local function was accepted" Module.TypedModuleOpenFailed failure -> assertFailure ("local-function failure fixture did not open: " <> show failure) Module.TypedModuleFailed failure _prefix -> assertFailure ("unexpected local-function failure: " <> show failure) where assertExactLocalFunctionCharacteristic proposition = do pair <- maybe (assertFailure "local function characteristic has wrong shape") pure (localFunctionPair proposition) assertEqual "local function uses the exact replacement characteristic" (expectedLocalFunctionCharacteristic pair) proposition localFunctionPair proposition = case Set.toList (Core.canonicalTermGlobals proposition) of [pair] | proposition == expectedLocalFunctionCharacteristic pair -> Just pair _ -> Nothing expectedLocalFunctionCharacteristic pair = Core.CForall Core.TySet (Core.CEq Core.TyProp (member (Core.CBound 0) (Core.CBound 1)) (existsP (andP (member (Core.CBound 0) (Core.CBound 3)) (Core.CEq Core.TySet (Core.CBound 1) (Core.CApp (Core.CApp (Core.CGlobal pair) (Core.CBound 0)) (Core.CBound 0)))))) member element set = Core.CApp (Core.CApp (Core.CIntrinsic Core.Member) element) set andP left right = notP (Core.CImp left (notP right)) existsP proposition = notP (Core.CForall Core.TySet (notP proposition)) notP proposition = Core.CImp proposition Core.CFalsum confinesTerminalExactContradiction :: Assertion confinesTerminalExactContradiction = Temp.withSystemTempDirectory "felix-exact-contradiction" \directory -> do let acceptedExecutable = directory Posix. "accepted-vampire" contradictoryExecutable = directory Posix. "contradictory-vampire" storePath = directory Posix. "store.sqlite" writeAcceptedFixtureVampire acceptedExecutable writeFile contradictoryExecutable (unlines [ "#!/bin/sh" , "cat >/dev/null" , "printf '%s\\n' '% SZS status ContradictoryAxioms for exact-contradiction'" ]) permissions <- getPermissions contradictoryExecutable setPermissions contradictoryExecutable (setOwnerExecutable True permissions) foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts =<< getCurrentDirectory workspace <- parseExactWorkspace bootstrap mounts "test/phase5/exact-cases-contradiction.tex" assertEmptyCaseAstRejected foundation bootstrap workspace observations <- newIORef [] fresh <- sole "cases and contradiction module" =<< compileParsedWorkspaceWithValidation foundation bootstrap (observingResolver acceptedExecutable contradictoryExecutable observations) Declaration.FreshValidation workspace observed <- readIORef observations assertEqual "cases and contradiction request count" 8 (length observed) case observed of branchOne : branchTwo : branchThree : exhaustive : byContradiction : arbitraryContradiction : omittedLaterBranch : omittedExhaustive : [] -> do assertEqual "case branches have isolated local ordinals" [[0], [1], [2]] (localReasoningLocalOrdinals <$> [branchOne, branchTwo, branchThree]) assertEqual "exhaustiveness sees pre-case locals only" [] (localReasoningLocalOrdinals exhaustive) case ( localReasoningLocalTerms branchOne , localReasoningLocalTerms branchTwo , localReasoningLocalTerms branchThree ) of ([caseOne], [caseTwo], [caseThree]) -> assertEqual "case exhaustiveness is left-associated in source order" (orP (orP caseOne caseTwo) caseThree) (localReasoningTarget exhaustive) branchTerms -> assertFailure ("unexpected branch-local premises: " <> show branchTerms) assertEqual "proof by contradiction targets falsum" Core.CFalsum (localReasoningTarget byContradiction) assertBool "double-negation elimination is not an ATP auxiliary" (Foundation.DoubleNegationElim `notElem` localReasoningAuxiliaries byContradiction) case localReasoningLocalTerms byContradiction of [Core.CImp negatedGoal Core.CFalsum] -> assertEqual "proof by contradiction assumes the exact negated goal" (localReasoningTarget branchOne) negatedGoal locals -> assertFailure ("unexpected contradiction locals: " <> show locals) assertEqual "arbitrary terminal contradiction targets falsum" Core.CFalsum (localReasoningTarget arbitraryContradiction) assertEqual "omitted case does not leak into its sibling" [1] (localReasoningLocalOrdinals omittedLaterBranch) assertEqual "omitted exhaustiveness sees no branch local" [] (localReasoningLocalOrdinals omittedExhaustive) _ -> assertFailure ("unexpected cases/contradiction observations: " <> show observed) case Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix fresh) of [caseBatch, byContradictionBatch, terminalBatch, omittedBatch] -> do traverse_ (assertBatchSafety Authority.cleanAuthoritySafety) [caseBatch, byContradictionBatch, terminalBatch] assertBatchSafety (Authority.authoritySafety (Authority.singletonEscapeKind Authority.Omitted)) omittedBatch batches -> assertFailure ("unexpected cases/contradiction declaration count: " <> show (length batches)) bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) Store.closeStore \store -> do expectRightIO (Store.writePendingModulePrefix store (Module.sealedTypedModulePrefix fresh)) let validation = Declaration.WarmValidation (Declaration.validationLookup (expectRightIO . Store.loadProofValidation store) (expectRightIO . Store.loadDeclarationValidation store)) warmRuns <- newIORef (0 :: Int) warm <- sole "warm cases and contradiction module" =<< compileParsedWorkspaceWithValidation foundation bootstrap (countingAcceptedResolver acceptedExecutable warmRuns) validation workspace assertEqual "warm structural proofs skip Vampire" 0 =<< readIORef warmRuns assertEqual "fresh and warm structural proof validations" (proofValidations fresh) (proofValidations warm) failureWorkspace <- parseExactWorkspace bootstrap mounts "test/phase5/exact-case-failure.tex" assertCaseFailure "middle case branch" foundation bootstrap failureWorkspace acceptedExecutable 1 2 assertCaseFailure "case exhaustiveness" foundation bootstrap failureWorkspace acceptedExecutable 3 4 directWorkspace <- parseExactWorkspace bootstrap mounts "test/phase5/exact-direct-contradictory.tex" directParsed <- sole "direct contradictory parsed module" (toList (Parse.parsedWorkspaceImportedBeforeImporter directWorkspace)) directInput <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) (Declaration.vampireResolver (runWith contradictoryExecutable)) Declaration.FreshValidation directParsed []) Module.runTypedModule directInput >>= \case Module.TypedModuleFailed (Module.TypedDeclarationFailed (Declaration.ProofObligationFailedAt _location Declaration.VampireObligationRejected{})) prefix -> assertBool "direct contradictory input publishes no theorem" (null (Declaration.pendingModulePrefixBatches prefix)) _result -> assertFailure "direct contradictory input was accepted" where observingResolver acceptedExecutable contradictoryExecutable observations = Declaration.vampireResolver \prepared -> do let problem = Provers.preparedTypedProverLogicalProblem prepared claim = Backend.typedProblemClaim problem locals = Backend.typedProblemLocalPremises problem target = Backend.supportedPropositionTerm claim modifyIORef' observations (<> [ LocalReasoningObservation { localReasoningTarget = target , localReasoningGlobalCount = Vector.length (Backend.typedProblemGlobalPremises problem) , localReasoningLocalOrdinals = [ Backend.localPremiseOrdinalValue (Backend.typedLocalPremiseOrdinal premise) | premise <- Vector.toList locals ] , localReasoningLocalTerms = Backend.supportedPropositionTerm . Backend.typedLocalPremiseProposition <$> Vector.toList locals , localReasoningAuxiliaries = Backend.typedProblemAuxiliaryTag <$> Vector.toList (Backend.typedProblemAuxiliaries problem) } ]) runWith (if target == Core.CFalsum then contradictoryExecutable else acceptedExecutable) prepared runWith executable prepared = (Provers.runPreparedTypedProver (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) assertEmptyCaseAstRejected foundation bootstrap workspace = do parsed <- sole "cases parsed module" (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) let blocks = Parse.identifiedParsedModuleBlocks (Parse.parsedModuleIdentified parsed) claim <- sole "cases source claim" [ candidate | candidate@Raw.BlockClaim{} <- take 1 blocks ] location <- case [ found | Raw.BlockProof _ (Raw.ByCase found _cases) _ <- blocks ] of found : _ -> pure found [] -> assertFailure "cases source proof is absent" >> fail "unreachable" let preludeModule = Module.bootstrapPreludeModule bootstrap outcome <- Declaration.runModuleDriver foundation (moduleName (Parse.parsedModuleAddress parsed)) [ Semantic.semanticInterfaceAssertedId (Module.sealedTypedModuleSemantic preludeModule) ] unusedResolver Declaration.FreshValidation do Declaration.importSealedModuleDriver (Module.sealedTypedModuleEvidence preludeModule) Declaration.runProspectiveLoweringDriver (ExactProof.prepareExactProof claim (Just (Raw.ByCase location []))) case outcome of Right (Declaration.DriverSucceeded (Left (ExactProof.ExactProofEmptyCaseSplit found)) _semantic prefix _closure) -> do assertEqual "empty case AST failure location" location found assertBool "empty case AST publishes no declaration" (null (Declaration.pendingModulePrefixBatches prefix)) _ -> assertFailure "empty programmatic case split was not rejected" assertBatchSafety expected batch = do fact <- sole "structural proof fact" (Semantic.declarationDeltaFacts (Declaration.committedBatchDelta batch)) assertEqual "structural proof authority safety" expected (Authority.factAuthoritySafety (Semantic.semanticFactAuthority fact)) proofValidations = concatMap Declaration.committedBatchProofValidations . Declaration.pendingModulePrefixBatches . Module.sealedTypedModulePrefix assertCaseFailure label foundation bootstrap workspace executable rejectedIndex expectedRuns = do runs <- newIORef (0 :: Int) parsed <- sole (label <> " parsed module") (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) let resolver = Declaration.vampireResolver \prepared -> do index <- atomicModifyIORef' runs \current -> (current + 1, current) if index == rejectedIndex then pure (Right (Provers.CounterSatisfiable "focused case rejection")) else runWith executable prepared input <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) resolver Declaration.FreshValidation parsed []) Module.runTypedModule input >>= \case Module.TypedModuleFailed _failure prefix -> assertBool (label <> " publishes no declaration") (null (Declaration.pendingModulePrefixBatches prefix)) _result -> assertFailure (label <> " unexpectedly succeeded") assertEqual (label <> " selects failures in source order") expectedRuns =<< readIORef runs orP left right = Core.CImp (Core.CImp left Core.CFalsum) right compilesExactReplacementComprehensions :: Assertion compilesExactReplacementComprehensions = Temp.withSystemTempDirectory "felix-exact-replacement" \root -> do let relative = "test/phase5/exact-replacement.tex" executable = root Posix. "vampire" repository <- getCurrentDirectory foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts repository workspace <- parseExactWorkspace bootstrap mounts relative writeFile executable (unlines [ "#!/bin/sh" , "cat >/dev/null" , "printf '%s\\n' '% SZS status Theorem for exact-replacement'" ]) permissions <- getPermissions executable setPermissions executable (setOwnerExecutable True permissions) observations <- newIORef [] let resolver = Declaration.vampireResolver \prepared -> do let problem = Provers.preparedTypedProverLogicalProblem prepared modifyIORef' observations (<> [ ( Backend.typedProblemRoute problem , Backend.typedProblemAuxiliaryTag <$> Vector.toList (Backend.typedProblemAuxiliaries problem) ) ]) (Provers.runPreparedTypedProver (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) modules <- compileParsedWorkspaceWithResolver foundation bootstrap resolver workspace sealed <- sole "exact replacement module" modules assertExactReplacementModule sealed assertEqual "replacement proof uses its checked characteristic on TH0" [( Backend.RouteTh0 , [Foundation.ReplacementCharacteristic] )] =<< readIORef observations assertExactReplacementModule :: Module.SealedTypedModule -> Assertion assertExactReplacementModule sealed = case Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix sealed) of [definitionBatch, theoremBatch] -> do definitionObject <- sole "replacement definition object" (Declaration.committedBatchObjects definitionBatch) case Identity.assertedObjectContent definitionObject of Identity.TransparentObjectContent _theory coreType body -> do assertEqual "replacement definition type" (Core.TyArrow Core.TySet Core.TySet) coreType assertEqual "replacement definition body" expectedBody body assertEqual "replacement definition foundation helpers" (Set.fromList [ Foundation.FamilyUnionCharacteristic , Foundation.SeparationCharacteristic , Foundation.ReplacementCharacteristic ]) (Foundation.foundationAxiomDependencies body) content -> assertFailure ("unexpected replacement object " <> show content) let definitionDelta = Declaration.committedBatchDelta definitionBatch definitionFacts = Semantic.declarationDeltaFacts definitionDelta assertEqual "replacement definition fact count" 2 (length definitionFacts) assertEqual "replacement equation/search view eligibility" [Semantic.SearchIneligible, Semantic.SearchEligible] (Semantic.semanticFactSearchEligibility <$> definitionFacts) assertEqual "replacement generated view is unaliased" 1 (length (Semantic.declarationDeltaAliases definitionDelta)) assertEqual "replacement definition proposition count" 2 (length (Declaration.committedBatchPropositions definitionBatch)) assertEqual "replacement definition proof validations" [] (Declaration.committedBatchProofValidations definitionBatch) definitionValidation <- maybe (assertFailure "replacement validation is absent" >> fail "unreachable") pure (Declaration.committedBatchDeclarationValidation definitionBatch) case Authority.validationDirectAuthorization <$> Semantic.declarationValidationRecordCertificates definitionValidation of [ Authority.CheckedKernelConstruction (Authority.CheckedDefinitionEquation target) , Authority.CheckedKernelConstruction (Authority.CheckedSetConstructionExtensionality generatedTarget _descriptor) ] -> assertEqual "replacement construction authority object" target generatedTarget authorizations -> assertFailure ("unexpected replacement definition authorities " <> show authorizations) assertEqual "replacement theorem adds no object" [] (Declaration.committedBatchObjects theoremBatch) assertEqual "replacement theorem fact count" 1 (length (Semantic.declarationDeltaFacts (Declaration.committedBatchDelta theoremBatch))) assertEqual "replacement theorem proposition count" 1 (length (Declaration.committedBatchPropositions theoremBatch)) theoremValidation <- sole "replacement theorem validation" (Declaration.committedBatchProofValidations theoremBatch) case Authority.validationDirectAuthorization (Semantic.proofValidationRecordCertificate theoremValidation) of Authority.CheckedSourceProof [_request] -> pure () authorization -> assertFailure ("unexpected replacement theorem authority " <> show authorization) batches -> assertFailure ("expected replacement definition and theorem, found " <> show (length batches)) where app1 intrinsic argument = Core.CApp (Core.CIntrinsic intrinsic) argument app2 intrinsic first second = Core.CApp (app1 intrinsic first) second expectedBody = Core.CLam Core.TySet $ app1 Core.FamilyUnion $ app2 Core.Repl (Core.CBound 0) $ Core.CLam Core.TySet $ app2 Core.Repl (app2 Core.Sep (Core.CBound 0) (Core.CLam Core.TySet $ Core.CEq Core.TySet (Core.CBound 1) (Core.CBound 0))) (Core.CLam Core.TySet (Core.CBound 0)) compilesAndReusesRelationalReplacement :: Assertion compilesAndReusesRelationalReplacement = Temp.withSystemTempDirectory "felix-exact-relational-replacement" \root -> do let relative = "test/phase5/exact-relational-replacement.tex" failureRelative = "test/phase5/exact-relational-replacement-failure.tex" localFailureRelative = "test/phase5/exact-relational-replacement-local-failure.tex" executable = root Posix. "vampire" storePath = root Posix. "store.sqlite" writeAcceptedFixtureVampire executable foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts =<< getCurrentDirectory workspace <- parseExactWorkspace bootstrap mounts relative observed <- newIORef [] runs <- newIORef (0 :: Int) let resolver = Declaration.vampireResolver \prepared -> do modifyIORef' runs (+ 1) let problem = Provers.preparedTypedProverLogicalProblem prepared modifyIORef' observed (<> [ ( Backend.typedProblemRoute problem , Backend.localPremiseOrdinalValue . Backend.typedLocalPremiseOrdinal <$> Vector.toList (Backend.typedProblemLocalPremises problem) , Backend.typedProblemAuxiliaryTag <$> Vector.toList (Backend.typedProblemAuxiliaries problem) ) ]) (Provers.runPreparedTypedProver (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) freshModules <- compileParsedWorkspaceWithValidation foundation bootstrap resolver Declaration.FreshValidation workspace fresh <- sole "fresh relational replacement module" freshModules assertRelationalReplacementModule fresh problems <- readIORef observed assertEqual "relational replacement request count" 3 (length problems) firstProblem <- sole "module functionality request" (take 1 problems) assertEqual "module functionality uses FOF" Backend.RouteFof (case firstProblem of (route, _, _) -> route) assertEqual "module functionality has no local premises" [] (case firstProblem of (_, ordinals, _) -> ordinals) assertEqual "relational equivalence creates no ATP obligation or auxiliary" [ (Backend.RouteFof, [], []) , (Backend.RouteFof, [], []) , (Backend.RouteFof, [0], []) ] problems bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) Store.closeStore \store -> do expectRightIO (Store.writePendingModulePrefix store (Module.sealedTypedModulePrefix fresh)) let validation = Declaration.WarmValidation (Declaration.validationLookup (expectRightIO . Store.loadProofValidation store) (expectRightIO . Store.loadDeclarationValidation store)) warmRuns <- newIORef (0 :: Int) warmModules <- compileParsedWorkspaceWithValidation foundation bootstrap (countingAcceptedResolver executable warmRuns) validation workspace assertEqual "warm relational replacement skips Vampire" 0 =<< readIORef warmRuns warm <- sole "warm relational replacement module" warmModules assertEqual "warm relational replacement interface" (Module.sealedTypedModuleSemantic fresh) (Module.sealedTypedModuleSemantic warm) assertEqual "warm relational replacement prefix" (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix fresh)) (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix warm)) let rejectingResolver = Declaration.vampireResolver \_prepared -> pure (Right (Provers.CounterSatisfiable "relational functionality rejected")) runRejected relativePath = do failedWorkspace <- parseExactWorkspace bootstrap mounts relativePath input <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) rejectingResolver Declaration.FreshValidation (Parse.parsedWorkspaceRootModule failedWorkspace) []) Module.runTypedModule input runRejected failureRelative >>= \case Module.TypedModuleFailed _failure prefix -> do batches <- pure (Declaration.pendingModulePrefixBatches prefix) assertEqual "failed relational definition keeps its prefix" 1 (length batches) prefixBatch <- sole "relational prefix declaration" batches assertEqual "failed relational definition publishes no object" 1 (length (Declaration.committedBatchObjects prefixBatch)) _result -> assertFailure "nonfunctional relational definition did not fail" runRejected localFailureRelative >>= \case Module.TypedModuleFailed _failure prefix -> assertBool "failed local functionality publishes no theorem" (null (Declaration.pendingModulePrefixBatches prefix)) _result -> assertFailure "nonfunctional local definition did not fail" assertRelationalReplacementModule :: Module.SealedTypedModule -> Assertion assertRelationalReplacementModule sealed = case Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix sealed) of [_axiomBatch, definitionBatch, proofBatch] -> do _object <- sole "relational replacement object" (Declaration.committedBatchObjects definitionBatch) let definitionFacts = Semantic.declarationDeltaFacts (Declaration.committedBatchDelta definitionBatch) assertEqual "relational replacement fact eligibility" [ Semantic.SearchIneligible , Semantic.SearchIneligible , Semantic.SearchEligible ] (Semantic.semanticFactSearchEligibility <$> definitionFacts) let sourceSafety = Authority.authoritySafety (Authority.singletonEscapeKind Authority.SourceAxiom) assertEqual "relational extensionality inherits functionality safety" [ Authority.cleanAuthoritySafety , sourceSafety , sourceSafety ] ( Authority.factAuthoritySafety . Semantic.semanticFactAuthority <$> definitionFacts ) assertEqual "relational replacement has only its equation alias" 1 (length (Semantic.declarationDeltaAliases (Declaration.committedBatchDelta definitionBatch))) validation <- maybe (assertFailure "relational replacement validation absent" >> fail "unreachable") pure (Declaration.committedBatchDeclarationValidation definitionBatch) case Authority.validationDirectAuthorization <$> Semantic.declarationValidationRecordCertificates validation of [ Authority.CheckedKernelConstruction (Authority.CheckedDefinitionEquation equationObject) , Authority.CheckedSourceProof [_functionalityRequest] , Authority.CheckedKernelConstruction (Authority.CheckedSetConstructionExtensionality extensionalObject _descriptor) ] -> assertEqual "relational facts target one object" equationObject extensionalObject authorizations -> assertFailure ("unexpected relational authorities " <> show authorizations) assertEqual "module construction generates no proof row" [] (Declaration.committedBatchProofValidations definitionBatch) proofValidation <- sole "proof-local relational validation" (Declaration.committedBatchProofValidations proofBatch) case Authority.validationDirectAuthorization (Semantic.proofValidationRecordCertificate proofValidation) of Authority.CheckedSourceProof requests -> assertEqual "local functionality precedes its continuation" 2 (length requests) authorization -> assertFailure ("unexpected proof-local relational authority " <> show authorization) proofFact <- sole "proof-local relational theorem" (Semantic.declarationDeltaFacts (Declaration.committedBatchDelta proofBatch)) assertEqual "local extensional premise retains discharge safety" sourceSafety (Authority.factAuthoritySafety (Semantic.semanticFactAuthority proofFact)) batches -> assertFailure ("expected relational axiom, definition, and proof, found " <> show (length batches)) compilesAndReusesExactFiniteSets :: Assertion compilesAndReusesExactFiniteSets = Temp.withSystemTempDirectory "felix-exact-finite-set" \root -> do let relative = "test/phase5/exact-finite-set.tex" sourcePath = root Posix. relative executable = root Posix. "vampire" storePath = root Posix. "store.sqlite" createDirectoryIfMissing True (Posix.takeDirectory sourcePath) ByteString.readFile relative >>= ByteString.writeFile sourcePath writeFile executable (unlines [ "#!/bin/sh" , "cat >/dev/null" , "printf '%s\\n' '% SZS status Theorem for exact-finite-set'" ]) permissions <- getPermissions executable setPermissions executable (setOwnerExecutable True permissions) foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts root workspace <- parseExactWorkspace bootstrap mounts relative observations <- newIORef [] let resolver = Declaration.vampireResolver \prepared -> do let problem = Provers.preparedTypedProverLogicalProblem prepared modifyIORef' observations (<> [ ( Backend.typedProblemRoute problem , Backend.typedProblemAuxiliaryTag <$> Vector.toList (Backend.typedProblemAuxiliaries problem) ) ]) (Provers.runPreparedTypedProver (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) freshModules <- compileParsedWorkspaceWithValidation foundation bootstrap resolver Declaration.FreshValidation workspace fresh <- sole "fresh finite-set module" freshModules assertExactFiniteSetModule "fresh" fresh assertEqual "finite-set proof uses exactly its FOF characteristics" [( Backend.RouteFof , [ Foundation.EmptyCharacteristic , Foundation.PairSetCharacteristic , Foundation.FamilyUnionCharacteristic ] )] =<< readIORef observations bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) Store.closeStore \store -> do expectRightIO (Store.writePendingModulePrefix store (Module.sealedTypedModulePrefix fresh)) let validation = Declaration.WarmValidation (Declaration.validationLookup (expectRightIO . Store.loadProofValidation store) (expectRightIO . Store.loadDeclarationValidation store)) warmRuns <- newIORef (0 :: Int) warmModules <- compileParsedWorkspaceWithValidation foundation bootstrap (countingAcceptedResolver executable warmRuns) validation workspace assertEqual "warm finite-set proof skips Vampire" 0 =<< readIORef warmRuns warm <- sole "warm finite-set module" warmModules assertExactFiniteSetModule "warm" warm assertEqual "warm finite-set semantic interface" (Module.sealedTypedModuleSemantic fresh) (Module.sealedTypedModuleSemantic warm) assertEqual "warm finite-set final prefix" (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix fresh)) (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix warm)) preparesExactDirectInductives :: Assertion preparesExactDirectInductives = do foundation <- expectRight Foundation.checkedFoundation prepared <- expectRight =<< prepareExactInductiveFixture "test/phase5/exact-inductive.tex" assertEqual "exact inductive carrier type" (Core.TyArrow Core.TySet Core.TySet) (ExactInductive.preparedExactInductiveCarrierType prepared) assertEqual "exact inductive carrier body" expectedCarrier (Core.frozenCoreTerm (ExactInductive.preparedExactInductiveCarrierBody prepared)) assertEqual "foundation guard needs no imported fact" [] (Vector.toList (ExactInductive.preparedExactInductiveGuardTargets prepared)) let facts = toList (ExactInductive.preparedExactInductiveFacts prepared) assertEqual "generated fact order" [ Raw.Marker "phase5_fin_intro_1" , Raw.Marker "phase5_fin_dom_subset" , Raw.Marker "phase5_fin_cases" , Raw.Marker "phase5_fin_induct" ] (TypedInductive.typedInductiveFactMarker <$> facts) assertEqual "generated guarded-rule descriptors" [ Set.singleton Foundation.SetLfpFixed , Set.singleton Foundation.SetLfpBound , Set.singleton Foundation.SetLfpFixed , Set.singleton Foundation.SetLfpInduct ] ( Set.fromList . toList . TypedInductive.typedInductiveFactRules <$> facts ) assertBool "generated targets are closed propositions" (all (\fact -> let target = TypedInductive.typedInductiveFactTarget fact in Core.frozenCoreType target == Core.TyProp && Set.null (Core.frozenCoreGlobals target)) facts) let singleton = Internal.finiteSet Nowhere (Internal.EmptySet Nowhere :| []) noGlobalType :: Void -> Core.CoreType noGlobalType = absurd noGlobal :: Internal.Symbol -> Maybe (TypedInductive.SourceGlobal Void) noGlobal = const Nothing finite <- expectRight (TypedInductive.prepareTypedInductive noGlobalType foundation noGlobal (Internal.Marker "finite_internal") (TypedInductive.DirectInductive [] singleton (TypedInductive.DirectInductiveClause [] [] (Internal.EmptySet Nowhere) :| []))) finiteGuard <- sole "finite-set inductive guard" (Vector.toList (TypedInductive.typedInductiveGuardTargets finite)) assertEqual "typed inductive path uses intrinsic finite-set adjunction" (member (Core.CIntrinsic Core.Empty) (Core.canonicalSetInsert (Core.CIntrinsic Core.Empty) (Core.CIntrinsic Core.Empty))) (Core.frozenCoreTerm finiteGuard) where apply1 intrinsic argument = Core.CApp (Core.CIntrinsic intrinsic) argument member element set = Core.CApp (Core.CApp (Core.CIntrinsic Core.Member) element) set expectedCarrier = Core.CLam Core.TySet (Core.CApp (Core.CApp (Core.CIntrinsic Core.ISetLfp) (apply1 Core.UnivOf (Core.CBound 0))) (Core.CLam Core.TySet (Core.CApp (Core.CApp (Core.CIntrinsic Core.Sep) (apply1 Core.UnivOf (Core.CBound 1))) (Core.CLam Core.TySet (Core.CEq Core.TySet (Core.CBound 0) (Core.CBound 2)))))) preparesExactDatatypes :: Assertion preparesExactDatatypes = do (foundation, owner, prepared) <- expectRight =<< prepareExactDatatypeFixture "test/phase5/exact-datatype.tex" let objects = toList (ExactDatatype.preparedExactDatatypeObjects prepared) objectIds = fst <$> objects objectTypes = snd <$> objects expectedTypes = [ Core.TySet , Core.TySet , Core.TyArrow Core.TySet Core.TySet , Core.TyArrow Core.TySet (Core.TyArrow Core.TySet Core.TySet) ] theory = Identity.theoryId foundation expectedIds = [ Identity.opaqueObjectId theory (Identity.opaqueDeclarationSeed owner (localDeclarationOrdinal 0) DatatypeDeclaration (generatedObjectSlot index)) coreType | (index, coreType) <- zip [0 ..] expectedTypes ] assertEqual "datatype opaque object types" expectedTypes objectTypes assertEqual "datatype opaque object slots" expectedIds objectIds assertBool "datatype objects are opaque" (all ((== Identity.OpaqueObject) . Identity.objectIdFamily) objectIds) (carrierId, zeroId, atomId, joinId, constructorIds) <- case expectedIds of [carrier, zero, atom, join] -> pure ( carrier , zero , atom , join , zero :| [atom, join] ) _ -> assertFailure "datatype object inventory is incomplete" >> fail "unreachable" let facts = toList (ExactDatatype.preparedExactDatatypeFacts prepared) markers = ExactDatatype.preparedExactDatatypeFactMarker <$> facts assertEqual "datatype generated fact order" [ Internal.Marker "phase5_data_phasefivezero_intro" , Internal.Marker "phase5_data_phasefiveatom_intro" , Internal.Marker "phase5_data_phasefivejoin_intro" , Internal.Marker "phase5_data_phasefivezero_phasefiveatom_distinct" , Internal.Marker "phase5_data_phasefivezero_phasefivejoin_distinct" , Internal.Marker "phase5_data_phasefiveatom_phasefivejoin_distinct" , Internal.Marker "phase5_data_phasefiveatom_injective" , Internal.Marker "phase5_data_phasefivejoin_injective" , Internal.Marker "phase5_data_cases" , Internal.Marker "phase5_data_induct" ] markers assertBool "datatype generated targets are checked propositions" (all (\fact -> Core.frozenCoreType (ExactDatatype.preparedExactDatatypeFactTarget fact) == Core.TyProp) facts) atomIntroduction <- sole "domain-bearing datatype introduction" [ fact | fact <- facts , ExactDatatype.preparedExactDatatypeFactMarker fact == Internal.Marker "phase5_data_phasefiveatom_intro" ] assertEqual "domain-bearing datatype introduction target" (Core.CForall Core.TySet (Core.CImp (member (Core.CBound 0) singletonEmpty) (member (Core.CApp (Core.CGlobal atomId) (Core.CBound 0)) (Core.CGlobal carrierId)))) (Core.frozenCoreTerm (ExactDatatype.preparedExactDatatypeFactTarget atomIntroduction)) induction <- sole "datatype induction law" [ fact | fact <- facts , ExactDatatype.preparedExactDatatypeFactMarker fact == Internal.Marker "phase5_data_induct" ] assertEqual "datatype induction target" (Core.CForall Core.TySet (Core.CImp (conjunctions [ member (Core.CGlobal zeroId) (Core.CBound 0) , Core.CForall Core.TySet (Core.CImp (member (Core.CBound 0) singletonEmpty) (member (Core.CApp (Core.CGlobal atomId) (Core.CBound 0)) (Core.CBound 1))) , Core.CForall Core.TySet (Core.CForall Core.TySet (Core.CImp (conjunction (member (Core.CBound 1) (Core.CBound 2)) (member (Core.CBound 0) (Core.CBound 2))) (member (Core.CApp (Core.CApp (Core.CGlobal joinId) (Core.CBound 1)) (Core.CBound 0)) (Core.CBound 2)))) ]) (Core.CForall Core.TySet (Core.CImp (member (Core.CBound 0) (Core.CGlobal carrierId)) (member (Core.CBound 0) (Core.CBound 1)))))) (Core.frozenCoreTerm (ExactDatatype.preparedExactDatatypeFactTarget induction)) assertEqual "datatype descriptor membership" (Authority.datatypeCompilationDescriptor carrierId constructorIds (ExactDatatype.preparedExactDatatypeFactReference <$> facts)) (ExactDatatype.preparedExactDatatypeDescriptor prepared) where singletonEmpty = Core.canonicalSetInsert (Core.CIntrinsic Core.Empty) (Core.CIntrinsic Core.Empty) member element set = Core.CApp (Core.CApp (Core.CIntrinsic Core.Member) element) set conjunction left right = Core.CImp (Core.CImp left (Core.CImp right Core.CFalsum)) Core.CFalsum conjunctions = \case [] -> Core.CImp Core.CFalsum Core.CFalsum first : remaining -> foldl' conjunction first remaining rejectsNestedExactDatatypeRecursion :: Assertion rejectsNestedExactDatatypeRecursion = do result <- prepareExactDatatypeFixture "test/phase5/exact-datatype-nested.tex" case result of Left ExactDatatype.ExactDatatypeInvalid{} -> pure () Left failure -> assertFailure ("unexpected nested datatype failure: " <> show failure) Right _prepared -> assertFailure "nested exact datatype recursion was accepted" compilesAndReusesExactDatatypes :: Assertion compilesAndReusesExactDatatypes = Temp.withSystemTempDirectory "felix-exact-datatype" \directory -> do let relative = "test/phase5/exact-datatype.tex" storePath = directory Posix. "store.sqlite" (foundation, bootstrap, workspace, freshModules) <- compileExactFixture relative fresh <- sole "fresh exact datatype module" freshModules assertExactDatatypeModule "fresh" fresh parsed <- sole "exact datatype parsed module" (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) let artifact sealed = do key <- expectRight (Semantic.moduleArtifactKey (moduleName (Parse.parsedModuleAddress parsed)) (Parse.parsedModuleId parsed) [ Semantic.semanticInterfaceAssertedId (Module.sealedTypedModuleSemantic (Module.bootstrapPreludeModule bootstrap)) ] (Identity.theoryId foundation)) pure (Semantic.moduleArtifactResult key (Syntax.moduleSyntaxAssertedId (Module.sealedTypedModuleSyntax sealed)) (Semantic.semanticInterfaceAssertedId (Module.sealedTypedModuleSemantic sealed))) freshArtifact <- artifact fresh bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) Store.closeStore \store -> do expectRightIO (Store.writePendingModulePrefix store (Module.sealedTypedModulePrefix fresh)) let validation = Declaration.WarmValidation (Declaration.validationLookup (expectRightIO . Store.loadProofValidation store) (expectRightIO . Store.loadDeclarationValidation store)) warmModules <- compileParsedWorkspaceWithValidation foundation bootstrap unusedResolver validation workspace warm <- sole "warm exact datatype module" warmModules assertExactDatatypeModule "warm" warm assertEqual "warm exact datatype semantic interface" (Module.sealedTypedModuleSemantic fresh) (Module.sealedTypedModuleSemantic warm) assertEqual "warm exact datatype final prefix" (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix fresh)) (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix warm)) assertEqual "warm exact datatype module artifact" freshArtifact =<< artifact warm mounts <- exactFixtureMounts =<< getCurrentDirectory nestedWorkspace <- parseExactWorkspace bootstrap mounts "test/phase5/exact-datatype-nested.tex" nestedParsed <- sole "nested exact datatype module" (toList (Parse.parsedWorkspaceImportedBeforeImporter nestedWorkspace)) nestedInput <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) unusedResolver Declaration.FreshValidation nestedParsed []) Module.runTypedModule nestedInput >>= \case Module.TypedModuleFailed (Module.TypedActionFailed (Module.TypedExactDatatypeFailed (ExactDatatype.ExactDatatypeInvalid location _message))) prefix -> do assertEqual "nested datatype failure line" 4 (locLine location) assertBool "nested datatype publishes no prefix" (null (Declaration.pendingModulePrefixBatches prefix)) _result -> assertFailure "unexpected nested datatype result" preparesNestedExactInductiveRecursion :: Assertion preparesNestedExactInductiveRecursion = withAcceptedFixtureVampire "felix-nested-inductive" \vampire -> do root <- getCurrentDirectory foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts root workspace <- parseExactWorkspace bootstrap mounts "test/phase5/exact-inductive-nested.tex" parsed <- sole "nested exact inductive parsed module" (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) observed <- newIORef [] let resolver = Declaration.vampireResolver \prepared -> do let problem = Provers.preparedTypedProverLogicalProblem prepared modifyIORef' observed (<> [ ( Backend.typedProblemRoute problem , Backend.supportedPropositionTerm (Backend.typedProblemClaim problem) ) ]) (Provers.runPreparedTypedProver vampire prepared) modules <- compileParsedWorkspaceWithValidation foundation bootstrap resolver Declaration.FreshValidation workspace sealed <- sole "nested exact inductive module" modules observations <- readIORef observed assertEqual "guard proof plus nested monotonicity request count" 2 (length observations) (route, target) <- sole "nested monotonicity request" [ observation | observation@(_route, candidate) <- observations , candidate == expectedPowerMonotonicity ] assertEqual "nested monotonicity target" expectedPowerMonotonicity target assertEqual "nested monotonicity request is first-order" Backend.RouteFof route case Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix sealed) of [_guardBatch, _unsafeBatch, inductiveBatch] -> do let facts = Semantic.declarationDeltaFacts (Declaration.committedBatchDelta inductiveBatch) aliases = Semantic.declarationDeltaAliases (Declaration.committedBatchDelta inductiveBatch) sourceSafety = Authority.authoritySafety (Authority.singletonEscapeKind Authority.SourceAxiom) assertEqual "nested inductive fact eligibility" ( Semantic.SearchEligible : Semantic.SearchIneligible : replicate 4 Semantic.SearchEligible ) (Semantic.semanticFactSearchEligibility <$> facts) monotonicityFact <- case facts of _definition : fact : _laws -> pure fact _ -> assertFailure "nested inductive fact inventory" >> fail "unreachable" assertEqual "nested monotonicity fact is unaliased" False (Semantic.semanticFactFingerprint monotonicityFact `elem` (Semantic.semanticAliasTarget <$> aliases)) assertEqual "nested authority safety reaches generated laws" [ Authority.cleanAuthoritySafety , sourceSafety , sourceSafety , Authority.cleanAuthoritySafety , sourceSafety , sourceSafety ] ( Authority.factAuthoritySafety . Semantic.semanticFactAuthority <$> facts ) validation <- maybe (assertFailure "nested inductive validation is absent" >> fail "unreachable") pure (Declaration.committedBatchDeclarationValidation inductiveBatch) assertEqual "nested inductive candidate authority shape" [ "definition" , "source-proof" , "kernel" , "kernel" , "kernel" , "kernel" ] (authorizationKind . Authority.validationDirectAuthorization <$> Semantic.declarationValidationRecordCertificates validation) requestId <- nestedRequestId inductiveBatch Temp.withSystemTempDirectory "felix-nested-inductive-cache" \temporary -> do let storePath = temporary Posix. "store.sqlite" bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) Store.closeStore \store -> do expectRightIO (Store.writePendingModulePrefix store (Module.sealedTypedModulePrefix sealed)) let warmValidation = Declaration.WarmValidation (Declaration.validationLookup (expectRightIO . Store.loadProofValidation store) (expectRightIO . Store.loadDeclarationValidation store)) warmModules <- compileParsedWorkspaceWithValidation foundation bootstrap unusedResolver warmValidation workspace warm <- sole "warm nested exact inductive module" warmModules warmBatch <- case Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix warm) of [_warmGuard, _warmUnsafe, batch] -> pure batch batches -> assertFailure ("warm nested batch count: " <> show (length batches)) >> fail "unreachable" assertEqual "warm nested exact request" requestId =<< nestedRequestId warmBatch assertEqual "warm nested semantic interface" (Module.sealedTypedModuleSemantic sealed) (Module.sealedTypedModuleSemantic warm) assertEqual "warm nested admitted prefix" (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix sealed)) (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix warm)) freshArtifact <- moduleArtifact foundation bootstrap parsed sealed warmArtifact <- moduleArtifact foundation bootstrap parsed warm assertEqual "warm nested module artifact" freshArtifact warmArtifact batches -> assertFailure ("expected guard and nested inductive batches, found " <> show (length batches)) failureWorkspace <- parseExactWorkspace bootstrap mounts "test/phase5/exact-inductive-nested-failure.tex" successfulRequests <- newIORef [] let successfulResolver = Declaration.vampireResolver \prepared -> do let problem = Provers.preparedTypedProverLogicalProblem prepared modifyIORef' successfulRequests (<> [Backend.supportedPropositionTerm (Backend.typedProblemClaim problem)]) (Provers.runPreparedTypedProver vampire prepared) successfulModules <- compileParsedWorkspaceWithValidation foundation bootstrap successfulResolver Declaration.FreshValidation failureWorkspace successful <- sole "successful repeated/distinct nested inductive module" successfulModules assertEqual "repeated and distinct contexts use two monotonicity requests" [ expectedPowerMonotonicity , expectedDoublePowerMonotonicity ] =<< readIORef successfulRequests case Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix successful) of [_guardOne, _guardTwo, batch] -> do validation <- maybe (assertFailure "successful multi-context validation absent" >> fail "unreachable") pure (Declaration.committedBatchDeclarationValidation batch) assertEqual "deduplicated monotonicities precede all kernel laws" ( ["definition", "source-proof", "source-proof"] <> replicate 6 "kernel" ) (authorizationKind . Authority.validationDirectAuthorization <$> Semantic.declarationValidationRecordCertificates validation) batches -> assertFailure ("successful multi-context batch count: " <> show (length batches)) attempts <- newIORef (0 :: Int) let rejectingResolver = Declaration.vampireResolver \prepared -> do index <- atomicModifyIORef' attempts \current -> (current + 1, current) if index == 0 then pure (Right (Provers.CounterSatisfiable "first monotonicity rejected")) else (Provers.runPreparedTypedProver vampire prepared) failureInput <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) rejectingResolver Declaration.FreshValidation (Parse.parsedWorkspaceRootModule failureWorkspace) []) Module.runTypedModule failureInput >>= \case Module.TypedModuleFailed (Module.TypedDeclarationFailed (Declaration.ProofObligationFailedAt location Declaration.VampireObligationRejected{})) prefix -> do assertEqual "earliest monotonicity failure location" 14 (locLine location) assertEqual "later monotonicity still resolves before first rejection" 2 =<< readIORef attempts assertEqual "rejected monotonicity preserves only earlier declarations" 2 (length (Declaration.pendingModulePrefixBatches prefix)) _result -> assertFailure "nested monotonicity rejection unexpectedly succeeded" where authorizationKind = \case Authority.CheckedKernelConstruction Authority.CheckedDefinitionEquation{} -> "definition" Authority.CheckedKernelConstruction{} -> "kernel" Authority.CheckedSourceProof{} -> "source-proof" authorization -> show authorization nestedRequestId batch = do validation <- maybe (assertFailure "nested declaration validation absent" >> fail "unreachable") pure (Declaration.committedBatchDeclarationValidation batch) certificate <- case Semantic.declarationValidationRecordCertificates validation of _definition : monotonicity : _laws -> pure monotonicity certificates -> assertFailure ("nested declaration certificate count: " <> show (length certificates)) >> fail "unreachable" case Authority.validationDirectAuthorization certificate of Authority.CheckedSourceProof [request] -> pure request authorization -> assertFailure ("unexpected nested proof authorization " <> show authorization) >> fail "unreachable" moduleArtifact foundation bootstrap parsed sealed = do key <- expectRight (Semantic.moduleArtifactKey (moduleName (Parse.parsedModuleAddress parsed)) (Parse.parsedModuleId parsed) [ Semantic.semanticInterfaceAssertedId (Module.sealedTypedModuleSemantic (Module.bootstrapPreludeModule bootstrap)) ] (Identity.theoryId foundation)) pure (Semantic.moduleArtifactResult key (Syntax.moduleSyntaxAssertedId (Module.sealedTypedModuleSyntax sealed)) (Semantic.semanticInterfaceAssertedId (Module.sealedTypedModuleSemantic sealed))) expectedPowerMonotonicity = Core.CForall Core.TySet (Core.CForall Core.TySet (Core.CForall Core.TySet (Core.CForall Core.TySet (Core.CImp (subset (Core.CBound 1) (Core.CBound 0)) (subset (power (Core.CBound 1)) (power (Core.CBound 0))))))) expectedDoublePowerMonotonicity = Core.CForall Core.TySet (Core.CForall Core.TySet (Core.CForall Core.TySet (Core.CForall Core.TySet (Core.CImp (subset (Core.CBound 1) (Core.CBound 0)) (subset (power (power (Core.CBound 1))) (power (power (Core.CBound 0)))))))) power argument = Core.CApp (Core.CIntrinsic Core.PowerSet) argument subset left right = Core.CForall Core.TySet (Core.CImp (member (Core.CBound 0) (Core.shiftCanonical 1 0 left)) (member (Core.CBound 0) (Core.shiftCanonical 1 0 right))) member element set = Core.CApp (Core.CApp (Core.CIntrinsic Core.Member) element) set compilesTransparentNestedInductiveWrappers :: Assertion compilesTransparentNestedInductiveWrappers = withAcceptedFixtureVampire "felix-nested-wrapper" \vampire -> do repository <- getCurrentDirectory foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts repository workspace <- parseExactWorkspace bootstrap mounts "test/phase5/exact-inductive-wrapper.tex" observed <- newIORef [] let resolver = Declaration.vampireResolver \prepared -> do let problem = Provers.preparedTypedProverLogicalProblem prepared modifyIORef' observed (<> [ ( Backend.typedProblemRoute problem , Backend.supportedPropositionTerm (Backend.typedProblemClaim problem) ) ]) (Provers.runPreparedTypedProver vampire prepared) modules <- compileParsedWorkspaceWithValidation foundation bootstrap resolver Declaration.FreshValidation workspace sealed <- sole "transparent-wrapper nested module" modules observations <- readIORef observed assertEqual "wrapper guard plus monotonicity request count" 2 (length observations) (route, target) <- case [ observation | observation@(_route, candidate) <- observations , candidate == expectedPowerMonotonicity ] of [observation] -> pure observation matches -> assertFailure ("normalized wrapper monotonicity matches: " <> show matches <> "; observed: " <> show observations) >> fail "unreachable" assertEqual "transparent-wrapper monotonicity is FOF" Backend.RouteFof route assertEqual "transparent-wrapper monotonicity target" expectedPowerMonotonicity target case Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix sealed) of [_wrapperDefinition, _guardProof, inductiveBatch] -> do let facts = Semantic.declarationDeltaFacts (Declaration.committedBatchDelta inductiveBatch) assertEqual "transparent-wrapper inductive stays clean" (replicate 6 Authority.cleanAuthoritySafety) ( Authority.factAuthoritySafety . Semantic.semanticFactAuthority <$> facts ) validation <- maybe (assertFailure "transparent-wrapper declaration validation absent" >> fail "unreachable") pure (Declaration.committedBatchDeclarationValidation inductiveBatch) assertEqual "transparent-wrapper staged authority" [ "definition" , "source-proof" , "kernel" , "kernel" , "kernel" , "kernel" ] (authorizationKind . Authority.validationDirectAuthorization <$> Semantic.declarationValidationRecordCertificates validation) batches -> assertFailure ("transparent-wrapper declaration count: " <> show (length batches)) where authorizationKind = \case Authority.CheckedKernelConstruction Authority.CheckedDefinitionEquation{} -> "definition" Authority.CheckedKernelConstruction{} -> "kernel" Authority.CheckedSourceProof{} -> "source-proof" authorization -> show authorization expectedPowerMonotonicity = Core.CForall Core.TySet (Core.CForall Core.TySet (Core.CForall Core.TySet (Core.CForall Core.TySet (Core.CImp (subset (Core.CBound 1) (Core.CBound 0)) (subset (power (Core.CBound 1)) (power (Core.CBound 0))))))) power argument = Core.CApp (Core.CIntrinsic Core.PowerSet) argument subset left right = Core.CForall Core.TySet (Core.CImp (member (Core.CBound 0) (Core.shiftCanonical 1 0 left)) (member (Core.CBound 0) (Core.shiftCanonical 1 0 right))) member element set = Core.CApp (Core.CApp (Core.CIntrinsic Core.Member) element) set normalizesNestedExactInductiveContexts :: Assertion normalizesNestedExactInductiveContexts = do foundation <- expectRight Foundation.checkedFoundation powerSymbol <- fixedFunctionSymbol "pow" carrierSymbol <- fixedFunctionSymbol "cumul" let a = Internal.NamedVar "A" x = Internal.NamedVar "x" y = Internal.NamedVar "y" z = Internal.NamedVar "z" carrier = Internal.TermOp Nowhere carrierSymbol [Internal.TermVar a] powerCarrier = Internal.TermOp Nowhere powerSymbol [carrier] doublePowerCarrier = Internal.TermOp Nowhere powerSymbol [powerCarrier] parameterizedCarrier = Internal.TermOp Nowhere powerSymbol [ Internal.TermOp Nowhere Lexicon.UpairSymbol [carrier, Internal.TermVar x] ] powerContext <- expectRight (TypedInductive.prepareRecursiveCarrierContext carrierSymbol [a] powerCarrier) doublePowerContext <- expectRight (TypedInductive.prepareRecursiveCarrierContext carrierSymbol [a] doublePowerCarrier) parameterizedContext <- expectRight (TypedInductive.prepareRecursiveCarrierContext carrierSymbol [a] parameterizedCarrier) deduplicated <- expectRight (TypedInductive.prepareTypedInductive (const Core.TySet) foundation (const Nothing) (Internal.Marker "nested_dedup") (TypedInductive.DirectInductive [a] (Internal.EmptySet Nowhere) (TypedInductive.DirectInductiveClause [x, y, z] [ TypedInductive.DirectRecursiveCondition (Internal.TermVar x) powerContext , TypedInductive.DirectRecursiveCondition (Internal.TermVar y) powerContext , TypedInductive.DirectRecursiveCondition (Internal.TermVar z) doublePowerContext , TypedInductive.DirectRecursiveCondition (Internal.TermVar z) parameterizedContext ] (Internal.TermVar a) :| []))) assertEqual "equal contexts deduplicate in first-occurrence order" [ monotonicityTarget 4 power , monotonicityTarget 4 (power . power) , monotonicityTarget 4 (\hole -> power (pair hole (Core.CBound 4))) ] ( Core.frozenCoreTerm . TypedInductive.typedInductiveMonotonicityTarget <$> Vector.toList (TypedInductive.typedInductiveMonotonicities deduplicated) ) let wrapperSymbol = Raw.mkMixfixItem [ Just (Internal.Command "phasefivecheckedwrapper") , Just Internal.InvisibleBraceL , Nothing , Just Internal.InvisibleBraceR ] (Internal.Marker "phasefivecheckedwrapper") Raw.NonAssoc wrapperCarrier = Internal.TermOp Nowhere wrapperSymbol [carrier] wrapperContext <- expectRight (TypedInductive.prepareRecursiveCarrierContext carrierSymbol [a] wrapperCarrier) wrapperBody <- expectRight (Core.checkCanonicalCore (const Nothing) (Core.CLam Core.TySet (power (Core.CBound 0)))) let wrapperId = Identity.transparentObjectId (Identity.theoryId foundation) (Core.TyArrow Core.TySet Core.TySet) (Core.frozenCoreTerm wrapperBody) wrapped <- expectRight (TypedInductive.prepareTypedInductive (const (Core.TyArrow Core.TySet Core.TySet)) foundation (\symbol -> if symbol == Internal.SymbolMixfix wrapperSymbol then Just (TypedInductive.SourceGlobal wrapperId (Just wrapperBody)) else Nothing) (Internal.Marker "nested_wrapper") (TypedInductive.DirectInductive [a] (Internal.EmptySet Nowhere) (TypedInductive.DirectInductiveClause [x] [TypedInductive.DirectRecursiveCondition (Internal.TermVar x) wrapperContext] (Internal.TermVar a) :| []))) assertEqual "transparent content, not a primitive-name whitelist, owns context semantics" [monotonicityTarget 2 power] ( Core.frozenCoreTerm . TypedInductive.typedInductiveMonotonicityTarget <$> Vector.toList (TypedInductive.typedInductiveMonotonicities wrapped) ) assertBool "transparent context target contains no wrapper global" (all (Set.null . Core.frozenCoreGlobals . TypedInductive.typedInductiveMonotonicityTarget) (Vector.toList (TypedInductive.typedInductiveMonotonicities wrapped))) assertExactFailure "test/phase5/exact-inductive-wrong-arguments.tex" 4 (\case ExactInductive.ExactInductiveRecursiveCarrierWrongArguments{} -> True _ -> False) assertExactFailure "test/phase5/exact-inductive-outside-membership.tex" 4 (\case ExactInductive.ExactInductiveRecursiveCarrierOutsideMembership{} -> True _ -> False) assertExactFailure "test/phase5/exact-inductive-recursive-element.tex" 4 (\case ExactInductive.ExactInductiveRecursiveTermMentionsCarrier{} -> True _ -> False) assertExactFailure "test/phase5/exact-inductive-recursive-domain.tex" 2 (\case ExactInductive.ExactInductiveDomainMentionsCarrier{} -> True _ -> False) assertExactFailure "test/phase5/exact-inductive-recursive-result.tex" 4 (\case ExactInductive.ExactInductiveResultMentionsCarrier{} -> True _ -> False) assertExactFailure "test/phase5/exact-inductive-unsupported-context.tex" 4 (\case ExactInductive.ExactInductiveUnsupportedRecursiveCarrierContext{} -> True _ -> False) where fixedFunctionSymbol marker = sole ("fixed function " <> StrictText.unpack marker) [ symbol | symbol <- Lexicon.prefixOps , Raw.mixfixMarker symbol == Internal.Marker marker ] assertExactFailure relative expectedLine expected = prepareExactInductiveFixture relative >>= \case Left failure | expected failure -> assertEqual ("nested-context failure line for " <> relative) expectedLine (locLine (ExactInductive.exactInductiveErrorLocation failure)) | otherwise -> assertFailure ("unexpected nested-context failure for " <> relative <> ": " <> show failure) Right{} -> assertFailure ("unsupported nested context was accepted: " <> relative) monotonicityTarget :: Int -> (Core.CanonicalTerm Identity.ObjectId -> Core.CanonicalTerm Identity.ObjectId) -> Core.CanonicalTerm Identity.ObjectId monotonicityTarget sourceBinders context = foldr (const (Core.CForall Core.TySet)) (Core.CForall Core.TySet (Core.CForall Core.TySet (Core.CImp (subset (Core.CBound 1) (Core.CBound 0)) (subset (context (Core.CBound 1)) (context (Core.CBound 0)))))) [1 .. sourceBinders] power argument = Core.CApp (Core.CIntrinsic Core.PowerSet) argument pair left right = Core.CApp (Core.CApp (Core.CIntrinsic Core.PairSet) left) right subset left right = Core.CForall Core.TySet (Core.CImp (member (Core.CBound 0) (Core.shiftCanonical 1 0 left)) (member (Core.CBound 0) (Core.shiftCanonical 1 0 right))) member element set = Core.CApp (Core.CApp (Core.CIntrinsic Core.Member) element) set compilesAndReusesExactInductives :: Assertion compilesAndReusesExactInductives = Temp.withSystemTempDirectory "felix-exact-inductive" \directory -> do let relative = "test/phase5/exact-inductive.tex" storePath = directory Posix. "store.sqlite" (foundation, bootstrap, workspace, freshModules) <- compileExactFixture relative fresh <- sole "fresh exact inductive module" freshModules assertExactInductiveModule foundation "fresh" fresh parsed <- sole "exact inductive parsed module" (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) let artifact sealed = do key <- expectRight (Semantic.moduleArtifactKey (moduleName (Parse.parsedModuleAddress parsed)) (Parse.parsedModuleId parsed) [ Semantic.semanticInterfaceAssertedId (Module.sealedTypedModuleSemantic (Module.bootstrapPreludeModule bootstrap)) ] (Identity.theoryId foundation)) pure (Semantic.moduleArtifactResult key (Syntax.moduleSyntaxAssertedId (Module.sealedTypedModuleSyntax sealed)) (Semantic.semanticInterfaceAssertedId (Module.sealedTypedModuleSemantic sealed))) freshArtifact <- artifact fresh bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) Store.closeStore \store -> do expectRightIO (Store.writePendingModulePrefix store (Module.sealedTypedModulePrefix fresh)) let validation = Declaration.WarmValidation (Declaration.validationLookup (expectRightIO . Store.loadProofValidation store) (expectRightIO . Store.loadDeclarationValidation store)) warmModules <- compileParsedWorkspaceWithValidation foundation bootstrap unusedResolver validation workspace warm <- sole "warm exact inductive module" warmModules assertExactInductiveModule foundation "warm" warm assertEqual "warm exact inductive semantic interface" (Module.sealedTypedModuleSemantic fresh) (Module.sealedTypedModuleSemantic warm) assertEqual "warm exact inductive final prefix" (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix fresh)) (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix warm)) assertEqual "warm exact inductive module artifact" freshArtifact =<< artifact warm authorizesRecursiveExactInductives :: Assertion authorizesRecursiveExactInductives = Temp.withSystemTempDirectory "felix-recursive-inductive" \directory -> do let relative = "test/phase5/exact-inductive-recursive.tex" storePath = directory Posix. "store.sqlite" (foundation, bootstrap, workspace, freshModules) <- compileExactFixture relative fresh <- sole "fresh recursive inductive module" freshModules assertRecursiveExactInductiveModule "fresh" fresh bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) Store.closeStore \store -> do expectRightIO (Store.writePendingModulePrefix store (Module.sealedTypedModulePrefix fresh)) let validation = Declaration.WarmValidation (Declaration.validationLookup (expectRightIO . Store.loadProofValidation store) (expectRightIO . Store.loadDeclarationValidation store)) warmModules <- compileParsedWorkspaceWithValidation foundation bootstrap unusedResolver validation workspace warm <- sole "warm recursive inductive module" warmModules assertRecursiveExactInductiveModule "warm" warm assertEqual "warm recursive inductive semantic interface" (Module.sealedTypedModuleSemantic fresh) (Module.sealedTypedModuleSemantic warm) assertEqual "warm recursive inductive final prefix" (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix fresh)) (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix warm)) assertRecursiveExactInductiveModule :: String -> Module.SealedTypedModule -> Assertion assertRecursiveExactInductiveModule label sealed = case Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix sealed) of [_axiomBatch, inductiveBatch] -> do object <- sole (label <> " recursive inductive carrier") (Declaration.committedBatchObjects inductiveBatch) let facts = Semantic.declarationDeltaFacts (Declaration.committedBatchDelta inductiveBatch) sourceSafety = Authority.authoritySafety (Authority.singletonEscapeKind Authority.SourceAxiom) assertEqual (label <> " recursive inductive safety") (Authority.cleanAuthoritySafety : replicate 4 sourceSafety) ( Authority.factAuthoritySafety . Semantic.semanticFactAuthority <$> facts ) validation <- maybe (assertFailure (label <> ": recursive validation is absent") >> fail "unreachable") pure (Declaration.committedBatchDeclarationValidation inductiveBatch) assertEqual (label <> " recursive inductive descriptors") [ Authority.CheckedKernelConstruction (Authority.CheckedDefinitionEquation (Identity.assertedObjectId object)) , guardedRules (Foundation.SetLfpBound :| [Foundation.SetLfpFixed]) , guardedRules (Foundation.SetLfpBound :| []) , guardedRules (Foundation.SetLfpFixed :| []) , guardedRules (Foundation.SetLfpInduct :| []) ] ( Authority.validationDirectAuthorization <$> Semantic.declarationValidationRecordCertificates validation ) batches -> assertFailure (label <> ": expected axiom and inductive batches, found " <> show (length batches)) where guardedRules rules = Authority.CheckedKernelConstruction (Authority.GuardedFoundationRules (Authority.guardedRuleSet rules)) assertExactDatatypeModule :: String -> Module.SealedTypedModule -> Assertion assertExactDatatypeModule label sealed = do assertEqual (label <> " datatype semantic declaration count") 1 (length (Semantic.semanticInterfaceDeclarations (Module.sealedTypedModuleSemantic sealed))) batch <- sole (label <> " datatype declaration batch") (Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix sealed)) let objects = Declaration.committedBatchObjects batch objectIds = Identity.assertedObjectId <$> objects delta = Declaration.committedBatchDelta batch facts = Semantic.declarationDeltaFacts delta aliases = Semantic.declarationDeltaAliases delta bindings = Semantic.semanticEnvironmentBindings (Semantic.declarationDeltaEnvironment delta) boundIds = Semantic.semanticGlobalTargetObject . Semantic.semanticGlobalBindingTarget <$> bindings assertEqual (label <> " datatype object count") 4 (length objects) assertBool (label <> " datatype objects are opaque") (all ((== Identity.OpaqueObject) . Identity.objectIdFamily . Identity.assertedObjectId) objects) assertEqual (label <> " datatype global binding count") 4 (length bindings) assertBool (label <> " datatype globals are references") (all (\binding -> case Semantic.semanticGlobalBindingTarget binding of Semantic.GlobalReference{} -> True Semantic.TransparentExpansion{} -> False Semantic.ContextualTransparentExpansion{} -> False) bindings) assertEqual (label <> " datatype global targets") (Set.fromList objectIds) (Set.fromList boundIds) assertEqual (label <> " datatype fact count") 10 (length facts) assertEqual (label <> " datatype aliases") (Semantic.semanticName <$> [ "phase5_data_phasefivezero_intro" , "phase5_data_phasefiveatom_intro" , "phase5_data_phasefivejoin_intro" , "phase5_data_phasefivezero_phasefiveatom_distinct" , "phase5_data_phasefivezero_phasefivejoin_distinct" , "phase5_data_phasefiveatom_phasefivejoin_distinct" , "phase5_data_phasefiveatom_injective" , "phase5_data_phasefivejoin_injective" , "phase5_data_cases" , "phase5_data_induct" ]) (Semantic.semanticAliasName <$> aliases) assertBool (label <> " datatype facts are clean") (all ((== Authority.cleanAuthoritySafety) . Authority.factAuthoritySafety . Semantic.semanticFactAuthority) facts) assertEqual (label <> " datatype proof validations") [] (Declaration.committedBatchProofValidations batch) validation <- maybe (assertFailure (label <> ": datatype validation is absent") >> fail "unreachable") pure (Declaration.committedBatchDeclarationValidation batch) descriptor <- case objectIds of carrier : firstConstructor : remainingConstructors -> pure (Authority.datatypeCompilationDescriptor carrier (firstConstructor :| remainingConstructors) ( Authority.factAuthorityTheorem . Semantic.semanticFactAuthority <$> facts )) _ -> assertFailure (label <> ": datatype object family is absent") >> fail "unreachable" assertEqual (label <> " datatype validation descriptors") (replicate 10 (Authority.TrustedCompilation (Authority.DatatypeCompilation descriptor))) ( Authority.validationDirectAuthorization <$> Semantic.declarationValidationRecordCertificates validation ) assertExactInductiveModule :: Foundation.CheckedFoundation -> String -> Module.SealedTypedModule -> Assertion assertExactInductiveModule foundation label sealed = case Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix sealed) of [batch] -> do object <- sole (label <> " inductive carrier") (Declaration.committedBatchObjects batch) case Identity.assertedObjectContent object of Identity.TransparentObjectContent _theory coreType body -> do assertEqual (label <> " inductive carrier type") (Core.TyArrow Core.TySet Core.TySet) coreType assertEqual (label <> " inductive carrier identity") (Identity.transparentObjectId (Identity.theoryId foundation) coreType body) (Identity.assertedObjectId object) content -> assertFailure (label <> ": unexpected inductive carrier " <> show content) let delta = Declaration.committedBatchDelta batch facts = Semantic.declarationDeltaFacts delta aliases = Semantic.declarationDeltaAliases delta assertEqual (label <> " inductive fact count") 5 (length facts) assertEqual (label <> " inductive aliases") (Semantic.semanticName <$> [ "phase5_fin" , "phase5_fin_intro_1" , "phase5_fin_dom_subset" , "phase5_fin_cases" , "phase5_fin_induct" ]) (Semantic.semanticAliasName <$> aliases) assertBool (label <> " inductive facts are clean") (all ((== Authority.cleanAuthoritySafety) . Authority.factAuthoritySafety . Semantic.semanticFactAuthority) facts) assertEqual (label <> " inductive proof validations") [] (Declaration.committedBatchProofValidations batch) validation <- maybe (assertFailure (label <> ": inductive validation is absent") >> fail "unreachable") pure (Declaration.committedBatchDeclarationValidation batch) assertEqual (label <> " inductive validation descriptors") [ Authority.CheckedKernelConstruction (Authority.CheckedDefinitionEquation (Identity.assertedObjectId object)) , guardedRules (Foundation.SetLfpFixed :| []) , guardedRules (Foundation.SetLfpBound :| []) , guardedRules (Foundation.SetLfpFixed :| []) , guardedRules (Foundation.SetLfpInduct :| []) ] ( Authority.validationDirectAuthorization <$> Semantic.declarationValidationRecordCertificates validation ) batches -> assertFailure (label <> ": expected one inductive batch, found " <> show (length batches)) where guardedRules rules = Authority.CheckedKernelConstruction (Authority.GuardedFoundationRules (Authority.guardedRuleSet rules)) assertExactFiniteSetModule :: String -> Module.SealedTypedModule -> Assertion assertExactFiniteSetModule label sealed = do assertEqual (label <> " finite-set semantic declarations") 2 (length (Semantic.semanticInterfaceDeclarations (Module.sealedTypedModuleSemantic sealed))) case Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix sealed) of [definitionBatch, theoremBatch] -> do definitionObject <- sole (label <> " finite-set definition object") (Declaration.committedBatchObjects definitionBatch) case Identity.assertedObjectContent definitionObject of Identity.TransparentObjectContent _theory coreType body -> do assertEqual (label <> " finite-set definition type") (Core.TyArrow Core.TySet (Core.TyArrow Core.TySet Core.TySet)) coreType assertEqual (label <> " finite-set definition body") expectedBody body content -> assertFailure (label <> ": unexpected finite-set object " <> show content) assertEqual (label <> " finite-set definition fact count") 1 (length (Semantic.declarationDeltaFacts (Declaration.committedBatchDelta definitionBatch))) assertEqual (label <> " finite-set definition proof validations") [] (Declaration.committedBatchProofValidations definitionBatch) assertEqual (label <> " finite-set theorem adds no object") [] (Declaration.committedBatchObjects theoremBatch) theoremFact <- sole (label <> " finite-set theorem fact") (Semantic.declarationDeltaFacts (Declaration.committedBatchDelta theoremBatch)) assertEqual (label <> " finite-set theorem safety") Authority.cleanAuthoritySafety (Authority.factAuthoritySafety (Semantic.semanticFactAuthority theoremFact)) theoremValidation <- sole (label <> " finite-set theorem validation") (Declaration.committedBatchProofValidations theoremBatch) case Authority.validationDirectAuthorization (Semantic.proofValidationRecordCertificate theoremValidation) of Authority.CheckedSourceProof [_request] -> pure () authorization -> assertFailure (label <> ": unexpected finite-set theorem authority " <> show authorization) batches -> assertFailure (label <> ": expected finite-set definition and theorem, found " <> show (length batches)) where expectedBody = Core.CLam Core.TySet (Core.CLam Core.TySet (Core.canonicalSetInsert (Core.CBound 1) (Core.canonicalSetInsert (Core.CBound 0) (Core.CIntrinsic Core.Empty)))) assertExactSeparationModule :: String -> Module.SealedTypedModule -> Assertion assertExactSeparationModule label sealed = do case Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix sealed) of [definitionBatch, theoremBatch] -> do assertEqual (label <> " separation definition object count") 1 (length (Declaration.committedBatchObjects definitionBatch)) definitionObject <- sole (label <> " separation definition object") (Declaration.committedBatchObjects definitionBatch) case Identity.assertedObjectContent definitionObject of Identity.TransparentObjectContent _theory coreType body -> do assertEqual (label <> " separation definition type") (Core.TyArrow Core.TySet Core.TySet) coreType assertEqual (label <> " separation definition body") (Core.CLam Core.TySet (Core.CApp (Core.CApp (Core.CIntrinsic Core.Sep) (Core.CBound 0)) (Core.CLam Core.TySet (Core.CEq Core.TySet (Core.CBound 0) (Core.CBound 0))))) body content -> assertFailure (label <> ": unexpected separation object " <> show content) let definitionDelta = Declaration.committedBatchDelta definitionBatch definitionFacts = Semantic.declarationDeltaFacts definitionDelta assertEqual (label <> " definition fact count") 2 (length definitionFacts) assertEqual (label <> " defining equation is explicit-only") [Semantic.SearchIneligible, Semantic.SearchEligible] (Semantic.semanticFactSearchEligibility <$> definitionFacts) assertEqual (label <> " generated view is unaliased") 1 (length (Semantic.declarationDeltaAliases definitionDelta)) assertEqual (label <> " definition proposition count") 2 (length (Declaration.committedBatchPropositions definitionBatch)) assertEqual (label <> " definition proof validations") [] (Declaration.committedBatchProofValidations definitionBatch) definitionValidation <- maybe (assertFailure (label <> ": definition validation is absent") >> fail "unreachable") pure (Declaration.committedBatchDeclarationValidation definitionBatch) case Authority.validationDirectAuthorization <$> Semantic.declarationValidationRecordCertificates definitionValidation of [ Authority.CheckedKernelConstruction (Authority.CheckedDefinitionEquation target) , Authority.CheckedKernelConstruction (Authority.CheckedSetConstructionExtensionality generatedTarget _descriptor) ] -> assertEqual (label <> " construction authority object") target generatedTarget authorizations -> assertFailure (label <> ": unexpected definition authorities " <> show authorizations) assertEqual (label <> " theorem adds no object") [] (Declaration.committedBatchObjects theoremBatch) theoremFact <- sole (label <> " separation theorem fact") (Semantic.declarationDeltaFacts (Declaration.committedBatchDelta theoremBatch)) assertEqual (label <> " theorem safety") Authority.cleanAuthoritySafety (Authority.factAuthoritySafety (Semantic.semanticFactAuthority theoremFact)) theoremValidation <- sole (label <> " separation theorem validation") (Declaration.committedBatchProofValidations theoremBatch) case Authority.validationDirectAuthorization (Semantic.proofValidationRecordCertificate theoremValidation) of Authority.CheckedSourceProof [_request] -> pure () authorization -> assertFailure (label <> ": unexpected theorem authority " <> show authorization) batches -> assertFailure (label <> ": expected definition and theorem, found " <> show (length batches)) reusesExactSeparationValidation :: Assertion reusesExactSeparationValidation = Temp.withSystemTempDirectory "felix-exact-separation-cache" \root -> do let relative = "test/phase5/exact-separation.tex" sourcePath = root Posix. relative executable = root Posix. "vampire" storePath = root Posix. "store.sqlite" createDirectoryIfMissing True (Posix.takeDirectory sourcePath) ByteString.readFile relative >>= ByteString.writeFile sourcePath writeFile executable (unlines [ "#!/bin/sh" , "cat >/dev/null" , "printf '%s\\n' '% SZS status Theorem for exact-separation-cache'" ]) permissions <- getPermissions executable setPermissions executable (setOwnerExecutable True permissions) foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts root workspace <- parseExactWorkspace bootstrap mounts relative freshRequests <- newIORef [] let freshResolver = Declaration.vampireResolver \prepared -> do modifyIORef' freshRequests (<> [Provers.preparedTypedProverRequest prepared]) (Provers.runPreparedTypedProver (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) freshModules <- compileParsedWorkspaceWithValidation foundation bootstrap freshResolver Declaration.FreshValidation workspace assertEqual "fresh separation proof runs Vampire once" 1 . length =<< readIORef freshRequests fresh <- sole "fresh exact separation module" freshModules assertExactSeparationModule "fresh cached" fresh freshDefinitionBatch <- case Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix fresh) of batch : _theorem : [] -> pure batch batches -> assertFailure ("fresh separation declaration count: " <> show (length batches)) >> fail "unreachable" freshDefinitionValidation <- maybe (assertFailure "fresh separation definition validation absent" >> fail "unreachable") pure (Declaration.committedBatchDeclarationValidation freshDefinitionBatch) corruptedDefinitionValidation <- case Semantic.declarationValidationRecordCertificates freshDefinitionValidation of [equation, extensional] -> do corruptedExtensional <- expectRight (Authority.validationCertificate (Authority.validationTarget extensional) (Authority.validationDirectAuthorization equation)) pure (Semantic.declarationValidationRecord (Semantic.declarationValidationRecordKey freshDefinitionValidation) [equation, corruptedExtensional]) certificates -> assertFailure ("fresh separation certificate count: " <> show (length certificates)) >> fail "unreachable" freshRequest <- sole "fresh separation request" =<< readIORef freshRequests freshAcceptedRequest <- acceptedRequestId "fresh separation" fresh assertEqual "fresh authority binds the exact request bytes" freshAcceptedRequest (Provers.preparedVerificationRequestId freshRequest) assertBool "fresh separation request bytes are retained by the caller" (Provers.preparedVerificationByteCount freshRequest > 0) bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) Store.closeStore \store -> do expectRightIO (Store.writePendingModulePrefix store (Module.sealedTypedModulePrefix fresh)) let validation = Declaration.WarmValidation (Declaration.validationLookup (expectRightIO . Store.loadProofValidation store) (expectRightIO . Store.loadDeclarationValidation store)) warmRuns <- newIORef (0 :: Int) warmModules <- compileParsedWorkspaceWithValidation foundation bootstrap (countingAcceptedResolver executable warmRuns) validation workspace assertEqual "warm separation proof skips Vampire" 0 =<< readIORef warmRuns warm <- sole "warm exact separation module" warmModules assertExactSeparationModule "warm cached" warm warmAcceptedRequest <- acceptedRequestId "warm separation" warm assertEqual "warm validation retains the fresh request-byte identity" freshAcceptedRequest warmAcceptedRequest assertEqual "warm separation semantic interface" (Module.sealedTypedModuleSemantic fresh) (Module.sealedTypedModuleSemantic warm) assertEqual "warm separation final prefix" (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix fresh)) (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix warm)) let components sealed = let batches = Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix sealed) in ( concatMap Declaration.committedBatchObjects batches , concatMap (fmap Identity.checkedPropositionId . Declaration.committedBatchPropositions) batches , concatMap Declaration.committedBatchProofValidations batches , Declaration.committedBatchDeclarationValidation <$> batches ) assertEqual "warm separation checked artifacts" (components fresh) (components warm) corruptRuns <- newIORef (0 :: Int) let corruptedValidation = Declaration.WarmValidation (Declaration.validationLookup (expectRightIO . Store.loadProofValidation store) (\key -> if key == Semantic.declarationValidationRecordKey corruptedDefinitionValidation then pure (Just corruptedDefinitionValidation) else expectRightIO (Store.loadDeclarationValidation store key))) corrupted <- Exception.try (compileParsedWorkspaceWithValidation foundation bootstrap (countingAcceptedResolver executable corruptRuns) corruptedValidation workspace) :: IO (Either Declaration.ValidationIntegrityError [Module.SealedTypedModule]) case corrupted of Left Declaration.CachedValidationIntegrityError{} -> pure () Right _ -> assertFailure "mismatched generated authority replay succeeded" assertEqual "mismatched generated authority does not invoke Vampire" 0 =<< readIORef corruptRuns where acceptedRequestId label sealed = do theoremBatch <- case Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix sealed) of [_definitionBatch, batch] -> pure batch batches -> assertFailure (label <> ": unexpected declaration count " <> show (length batches)) >> fail "unreachable" validation <- sole (label <> " proof validation") (Declaration.committedBatchProofValidations theoremBatch) case Authority.validationDirectAuthorization (Semantic.proofValidationRecordCertificate validation) of Authority.CheckedSourceProof [request] -> pure request authorization -> assertFailure (label <> ": unexpected direct authorization " <> show authorization) >> fail "unreachable" compilesExactSourceAxioms :: Assertion compilesExactSourceAxioms = Temp.withSystemTempDirectory "felix-exact-source-axiom" \root -> do let storePath = root Posix. "store.sqlite" (foundation, bootstrap, workspace, freshModules) <- compileExactFixture "test/phase5/exact-source-axiom-assumptions.tex" fresh <- sole "fresh source-axiom module" freshModules assertSourceAxiom "fresh" fresh bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) Store.closeStore \store -> do expectRightIO (Store.writePendingModulePrefix store (Module.sealedTypedModulePrefix fresh)) let validation = Declaration.WarmValidation (Declaration.validationLookup (expectRightIO . Store.loadProofValidation store) (expectRightIO . Store.loadDeclarationValidation store)) warmModules <- compileParsedWorkspaceWithValidation foundation bootstrap unusedResolver validation workspace warm <- sole "warm source-axiom module" warmModules assertSourceAxiom "warm" warm assertEqual "warm source axiom preserves semantics" (Module.sealedTypedModuleSemantic fresh) (Module.sealedTypedModuleSemantic warm) assertEqual "warm source axiom preserves prefix" (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix fresh)) (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix warm)) where assertSourceAxiom label sealed = do batch <- sole (label <> " source-axiom batch") (Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix sealed)) fact <- sole (label <> " source-axiom fact") (Semantic.declarationDeltaFacts (Declaration.committedBatchDelta batch)) alias <- sole (label <> " source-axiom alias") (Semantic.declarationDeltaAliases (Declaration.committedBatchDelta batch)) assertEqual (label <> " source-axiom search eligibility") Semantic.SearchEligible (Semantic.semanticFactSearchEligibility fact) assertEqual (label <> " source-axiom marker alias") (Semantic.semanticName "phase5_exact_source_axiom_assumptions") (Semantic.semanticAliasName alias) proposition <- sole (label <> " source-axiom proposition") (Declaration.committedBatchPropositions batch) assertEqual (label <> " source-axiom closed target") (Core.CForall Core.TySet (Core.CForall Core.TySet (Core.CImp (member (Core.CBound 0) (Core.CBound 1)) (Core.CImp (Core.CEq Core.TySet (Core.CBound 0) (Core.CBound 0)) (member (Core.CBound 0) (Core.CBound 1)))))) (Core.frozenCoreTerm (Identity.checkedPropositionTerm proposition)) assertEqual (label <> " source-axiom safety") (Authority.authoritySafety (Authority.singletonEscapeKind Authority.SourceAxiom)) (Authority.factAuthoritySafety (Semantic.semanticFactAuthority fact)) validation <- maybe (assertFailure (label <> " source-axiom validation is absent") >> fail "unreachable") pure (Declaration.committedBatchDeclarationValidation batch) certificate <- sole (label <> " source-axiom certificate") (Semantic.declarationValidationRecordCertificates validation) assertEqual (label <> " source-axiom direct authority") Authority.SourceAxiomAuthorization (Authority.validationDirectAuthorization certificate) assertEqual (label <> " source axiom has no proof validations") [] (Declaration.committedBatchProofValidations batch) member element set = Core.CApp (Core.CApp (Core.CIntrinsic Core.Member) element) set rejectsProofLocalGeneralization :: Assertion rejectsProofLocalGeneralization = do foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver repository <- getCurrentDirectory mounts <- exactFixtureMounts repository workspace <- parseExactWorkspace bootstrap mounts "test/phase5/exact-proof-local-free.tex" input <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) unusedResolver Declaration.FreshValidation (Parse.parsedWorkspaceRootModule workspace) []) Module.runTypedModule input >>= \case Module.TypedModuleFailed (Module.TypedActionFailed (Module.TypedExactProofFailed (ExactProof.ExactProofElaborationFailed (Exact.ExactFreeVariable location (Raw.NamedVar "y"))))) prefix -> do assertEqual "proof-local free variable line" 6 (locLine location) assertEqual "proof-local failure commits nothing" 0 (length (Declaration.pendingModulePrefixBatches prefix)) Module.TypedModuleSucceeded{} -> assertFailure "proof-local variable was generalized" Module.TypedModuleOpenFailed failure -> assertFailure ("proof-local generalization module did not open: " <> show failure) Module.TypedModuleFailed failure _prefix -> assertFailure ("unexpected proof-local generalization failure: " <> show failure) doesNotTreatMarkerOnlyNounAsSet :: Assertion doesNotTreatMarkerOnlyNounAsSet = do foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver repository <- getCurrentDirectory mounts <- exactFixtureMounts repository workspace <- parseExactWorkspace bootstrap mounts "test/phase5/exact-set-marker.tex" Temp.withSystemTempDirectory "felix-exact-set-marker" \root -> do let executable = root Posix. "vampire" writeFile executable (unlines [ "#!/bin/sh" , "cat >/dev/null" , "printf '%s\\n' '% SZS status Theorem for set-marker'" ]) permissions <- getPermissions executable setPermissions executable (setOwnerExecutable True permissions) observed <- newIORef [] let resolver = Declaration.vampireResolver \prepared -> do let problem = Provers.preparedTypedProverLogicalProblem prepared claim = Backend.typedProblemClaim problem locals = Backend.typedProblemLocalPremises problem modifyIORef' observed (<> [ [ Backend.supportedPropositionTerm (Backend.typedLocalPremiseProposition premise) == Backend.supportedPropositionTerm claim | premise <- Vector.toList locals ] ]) (Provers.runPreparedTypedProver (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) input <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) resolver Declaration.FreshValidation (Parse.parsedWorkspaceRootModule workspace) []) Module.runTypedModule input >>= \case Module.TypedModuleSucceeded{} -> assertEqual "the source noun supplies the local proof premise" [[True]] =<< readIORef observed Module.TypedModuleOpenFailed failure -> assertFailure ("marker-only set noun module did not open: " <> show failure) Module.TypedModuleFailed failure _prefix -> assertFailure ("unexpected marker-only set noun failure: " <> show failure) compilesExactOmittedProofs :: Assertion compilesExactOmittedProofs = Temp.withSystemTempDirectory "felix-exact-omitted" \root -> do repository <- getCurrentDirectory foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts repository workspace <- parseExactWorkspace bootstrap mounts "test/phase5/exact-omitted.tex" let executable = root Posix. "vampire" writeFile executable (unlines [ "#!/bin/sh" , "cat >/dev/null" , "printf '%s\\n' '% SZS status Theorem for exact-omitted'" ]) permissions <- getPermissions executable setPermissions executable (setOwnerExecutable True permissions) calls <- newIORef (0 :: Int) let resolver = Declaration.vampireResolver \prepared -> do modifyIORef' calls (+ 1) (Provers.runPreparedTypedProver (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) modules <- compileParsedWorkspaceWithResolver foundation bootstrap resolver workspace sealed <- sole "exact omitted module" modules assertEqual "only the non-omitted continuation invokes Vampire" 1 =<< readIORef calls let batches = Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix sealed) assertEqual "top-level and nested omitted declarations" 2 (length batches) for_ (zip ["top-level", "nested"] batches) \(label, batch) -> do fact <- sole (label <> " omitted fact") (Semantic.declarationDeltaFacts (Declaration.committedBatchDelta batch)) assertEqual (label <> " omitted safety") (Authority.authoritySafety (Authority.singletonEscapeKind Authority.Omitted)) (Authority.factAuthoritySafety (Semantic.semanticFactAuthority fact)) record <- sole (label <> " omitted validation") (Declaration.committedBatchProofValidations batch) assertEqual (label <> " omitted direct authority") Authority.OmittedAuthorization (Authority.validationDirectAuthorization (Semantic.proofValidationRecordCertificate record)) assertEqual (label <> " publishes only its final theorem") 1 (length (Semantic.declarationDeltaFacts (Declaration.committedBatchDelta batch))) reusesExactEscapeAuthority :: Assertion reusesExactEscapeAuthority = Temp.withSystemTempDirectory "felix-exact-escape-cache" \root -> do let consumerRelative = "test/phase5/exact-escape-consumer.tex" producerRelative = "test/phase5/exact-escape-producer.tex" consumerPath = root Posix. consumerRelative producerPath = root Posix. producerRelative executable = root Posix. "vampire" storePath = root Posix. "store.sqlite" createDirectoryIfMissing True (Posix.takeDirectory consumerPath) consumerSource <- ByteString.readFile consumerRelative producerSource <- ByteString.readFile producerRelative ByteString.writeFile consumerPath consumerSource ByteString.writeFile producerPath producerSource writeFile executable (unlines [ "#!/bin/sh" , "cat >/dev/null" , "printf '%s\\n' '% SZS status Theorem for exact-escape'" ]) permissions <- getPermissions executable setPermissions executable (setOwnerExecutable True permissions) foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts root freshWorkspace <- parseExactWorkspace bootstrap mounts consumerRelative freshRuns <- newIORef (0 :: Int) freshModules <- compileParsedWorkspaceWithValidation foundation bootstrap (acceptedResolver executable freshRuns) Declaration.FreshValidation freshWorkspace assertEqual "fresh escape graph Vampire requests" 5 =<< readIORef freshRuns assertEscapeGraph "fresh" freshModules bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) Store.closeStore \store -> do traverse_ (expectRightIO . Store.writePendingModulePrefix store . Module.sealedTypedModulePrefix) freshModules let validation = Declaration.WarmValidation (Declaration.validationLookup (expectRightIO . Store.loadProofValidation store) (expectRightIO . Store.loadDeclarationValidation store)) compileWarm workspace = do runs <- newIORef (0 :: Int) modules <- compileParsedWorkspaceWithValidation foundation bootstrap (acceptedResolver executable runs) validation workspace runCount <- readIORef runs pure (modules, runCount) (warmModules, warmRuns) <- compileWarm freshWorkspace assertEqual "exact escape warm hit skips Vampire" 0 warmRuns assertEscapeGraph "warm" warmModules assertEqual "warm escape graph preserves module semantics" (moduleSemantics freshModules) (moduleSemantics warmModules) assertEqual "warm escape graph preserves module prefixes" (modulePrefixes freshModules) (modulePrefixes warmModules) let formattingOnly = Text.encodeUtf8 ("% shifted exact escape source\n" <> Text.decodeUtf8 consumerSource) ByteString.writeFile consumerPath formattingOnly formattedWorkspace <- parseExactWorkspace bootstrap mounts consumerRelative assertBool "formatting changes the escape parsed identity" (Parse.parsedModuleId (Parse.parsedWorkspaceRootModule freshWorkspace) /= Parse.parsedModuleId (Parse.parsedWorkspaceRootModule formattedWorkspace)) (formattedModules, formattedRuns) <- compileWarm formattedWorkspace assertEqual "formatting-only escape edit reuses validation" 0 formattedRuns assertEqual "formatting-only escape edit preserves semantics" (moduleSemantics freshModules) (moduleSemantics formattedModules) let omittedGoalEdit = Text.encodeUtf8 (StrictText.replace " Show $x = x$." " Show if $x = x$, then $x = x$." (Text.decodeUtf8 consumerSource)) ByteString.writeFile consumerPath omittedGoalEdit editedWorkspace <- parseExactWorkspace bootstrap mounts consumerRelative (editedModules, editedRuns) <- compileWarm editedWorkspace assertEqual "changed omitted goal misses its proof validation" 1 editedRuns assertEqual "changed omitted goal preserves public semantics" (moduleSemantics freshModules) (moduleSemantics editedModules) where acceptedResolver executable runs = Declaration.vampireResolver \prepared -> do modifyIORef' runs (+ 1) (Provers.runPreparedTypedProver (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) moduleSemantics = fmap Module.sealedTypedModuleSemantic modulePrefixes = fmap (Declaration.pendingModulePrefixCurrent . Module.sealedTypedModulePrefix) assertEscapeGraph label = \case [producer, consumer] -> do let producerBatches = Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix producer) consumerBatches = Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix consumer) case producerBatches of [sourceAxiom, omitted] -> do assertEscapeSafety (label <> " source axiom") [Authority.SourceAxiom] sourceAxiom assertDeclarationDirect (label <> " source axiom") Authority.SourceAxiomAuthorization sourceAxiom assertEscapeSafety (label <> " omitted theorem") [Authority.Omitted] omitted assertProofDirectOmitted (label <> " omitted theorem") omitted batches -> assertFailure (label <> " producer batch count: " <> show (length batches)) case consumerBatches of [fromAxiom, fromOmitted, throughLocal, ownOmission] -> do assertEscapeSafety (label <> " source-axiom consumer") [Authority.SourceAxiom] fromAxiom assertProofDirectChecked (label <> " source-axiom consumer") 1 fromAxiom assertEscapeSafety (label <> " omitted consumer") [Authority.Omitted] fromOmitted assertProofDirectChecked (label <> " omitted consumer") 1 fromOmitted assertEscapeSafety (label <> " local source-axiom consumer") [Authority.SourceAxiom] throughLocal assertProofDirectChecked (label <> " local source-axiom consumer") 2 throughLocal assertEscapeSafety (label <> " own omission") [Authority.SourceAxiom, Authority.Omitted] ownOmission assertProofDirectOmitted (label <> " own omission") ownOmission batches -> assertFailure (label <> " consumer batch count: " <> show (length batches)) modules -> assertFailure (label <> " escape module count: " <> show (length modules)) assertEscapeSafety label expected batch = do fact <- sole (label <> " fact") (Semantic.declarationDeltaFacts (Declaration.committedBatchDelta batch)) assertEqual (label <> " public escape kinds") expected (Authority.escapeKindsToList (Authority.authoritySafetyEscapeKinds (Authority.factAuthoritySafety (Semantic.semanticFactAuthority fact)))) assertDeclarationDirect label expected batch = do validation <- maybe (assertFailure (label <> " declaration validation is absent") >> fail "unreachable") pure (Declaration.committedBatchDeclarationValidation batch) certificate <- sole (label <> " declaration certificate") (Semantic.declarationValidationRecordCertificates validation) assertEqual (label <> " direct authorization") expected (Authority.validationDirectAuthorization certificate) assertProofDirectChecked label expectedCount batch = do authorization <- proofDirect label batch case authorization of Authority.CheckedSourceProof requests -> assertEqual (label <> " accepted request count") expectedCount (length requests) direct -> assertFailure (label <> " has unexpected direct authority: " <> show direct) assertProofDirectOmitted label batch = do authorization <- proofDirect label batch assertEqual (label <> " direct authorization") Authority.OmittedAuthorization authorization proofDirect label batch = do record <- sole (label <> " proof validation") (Declaration.committedBatchProofValidations batch) pure (Authority.validationDirectAuthorization (Semantic.proofValidationRecordCertificate record)) rejectsAfterExactOmittedSubclaim :: Assertion rejectsAfterExactOmittedSubclaim = Temp.withSystemTempDirectory "felix-exact-omitted-rollback" \root -> do repository <- getCurrentDirectory foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts repository workspace <- parseExactWorkspace bootstrap mounts "test/phase5/exact-escape-consumer.tex" parsedModules <- pure (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) (producerParsed, consumerParsed) <- case parsedModules of [producer, consumer] -> pure (producer, consumer) modules -> assertFailure ("unexpected rollback graph size: " <> show (length modules)) >> fail "unreachable" producerInput <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) unusedResolver Declaration.FreshValidation producerParsed []) producer <- Module.runTypedModule producerInput >>= \case Module.TypedModuleSucceeded sealed -> pure sealed _ -> assertFailure "escape producer did not seal" >> fail "unreachable" let executable = root Posix. "vampire" writeFile executable (unlines [ "#!/bin/sh" , "cat >/dev/null" , "printf '%s\\n' '% SZS status Theorem for omitted-rollback'" ]) permissions <- getPermissions executable setPermissions executable (setOwnerExecutable True permissions) calls <- newIORef (0 :: Int) let resolver = Declaration.vampireResolver \prepared -> do runCount <- readIORef calls modifyIORef' calls (+ 1) if runCount < 4 then (Provers.runPreparedTypedProver (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) else pure (Right (Provers.CounterSatisfiable "rejected continuation")) consumerInput <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) resolver Declaration.FreshValidation consumerParsed [producer]) Module.runTypedModule consumerInput >>= \case Module.TypedModuleFailed (Module.TypedDeclarationFailed (Declaration.ProofObligationFailedAt location Declaration.VampireObligationRejected{})) prefix -> do assertEqual "the continuation is the fifth request" 5 =<< readIORef calls assertEqual "rejected continuation location" 37 (locLine location) assertEqual "omitted declaration rolls back atomically" 3 (length (Declaration.pendingModulePrefixBatches prefix)) Module.TypedModuleSucceeded{} -> assertFailure "rejected omitted continuation was accepted" Module.TypedModuleOpenFailed failure -> assertFailure ("omitted rollback module did not open: " <> show failure) Module.TypedModuleFailed failure _prefix -> assertFailure ("unexpected omitted rollback failure: " <> show failure) reusesExactProofValidationAcrossModuleMisses :: Assertion reusesExactProofValidationAcrossModuleMisses = Temp.withSystemTempDirectory "felix-exact-proof-cache" \root -> do let relative = "test/phase5/exact-proofs.tex" producerRelative = "test/phase5/exact-producer.tex" sourcePath = root Posix. relative producerPath = root Posix. producerRelative executable = root Posix. "vampire" storePath = root Posix. "store.sqlite" createDirectoryIfMissing True (Posix.takeDirectory sourcePath) original <- ByteString.readFile relative producer <- ByteString.readFile producerRelative ByteString.writeFile sourcePath original ByteString.writeFile producerPath producer writeFile executable (unlines [ "#!/bin/sh" , "cat >/dev/null" , "printf '%s\\n' '% SZS status Theorem for exact-cache'" ]) permissions <- getPermissions executable setPermissions executable (setOwnerExecutable True permissions) foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts root freshWorkspace <- parseExactWorkspace bootstrap mounts relative freshRuns <- newIORef (0 :: Int) freshModules <- compileParsedWorkspaceWithValidation foundation bootstrap (countingAcceptedResolver executable freshRuns) Declaration.FreshValidation freshWorkspace assertEqual "fresh proof obligations run Vampire" 7 =<< readIORef freshRuns freshRoot <- sole "fresh exact proof root" (drop 1 freshModules) bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) Store.closeStore \store -> do traverse_ (expectRightIO . Store.writePendingModulePrefix store . Module.sealedTypedModulePrefix) freshModules let validation = Declaration.WarmValidation (Declaration.validationLookup (expectRightIO . Store.loadProofValidation store) (expectRightIO . Store.loadDeclarationValidation store)) compileWarm workspace = do runs <- newIORef (0 :: Int) modules <- compileParsedWorkspaceWithValidation foundation bootstrap (countingAcceptedResolver executable runs) validation workspace rootModule <- sole "warm exact proof root" (drop 1 modules) runCount <- readIORef runs pure (rootModule, runCount) (unchangedRoot, unchangedRuns) <- compileWarm freshWorkspace assertEqual "exact warm hit skips Vampire" 0 unchangedRuns assertEqual "exact warm hit preserves public semantics" (Module.sealedTypedModuleSemantic freshRoot) (Module.sealedTypedModuleSemantic unchangedRoot) let formattingOnly = Text.encodeUtf8 (StrictText.replace "\\begin{proposition}\\label{phase5_structural_proof}" ("% shifted source location\n" <> "\\begin{proposition}\\label{phase5_structural_proof}") (Text.decodeUtf8 original)) ByteString.writeFile sourcePath formattingOnly formattedWorkspace <- parseExactWorkspace bootstrap mounts relative assertBool "formatting changes parsed module identity" (Parse.parsedModuleId (Parse.parsedWorkspaceRootModule freshWorkspace) /= Parse.parsedModuleId (Parse.parsedWorkspaceRootModule formattedWorkspace)) (formattedRoot, formattedRuns) <- compileWarm formattedWorkspace assertEqual "formatting-only module miss reuses proof validation" 0 formattedRuns assertEqual "formatting-only miss preserves public semantics" (Module.sealedTypedModuleSemantic freshRoot) (Module.sealedTypedModuleSemantic formattedRoot) let semanticEdit = Text.encodeUtf8 (StrictText.replace " We have $x = x$ by assumption." (StrictText.intercalate "\n" [ " Show $x = x$." , " \\begin{subproof}" , " Follows by assumption." , " \\end{subproof}" ]) (Text.decodeUtf8 original)) ByteString.writeFile sourcePath semanticEdit editedWorkspace <- parseExactWorkspace bootstrap mounts relative (editedRoot, editedRuns) <- compileWarm editedWorkspace assertEqual "semantic proof edit reruns its obligations" 2 editedRuns assertEqual "request-equivalent proof preserves public semantics" (Module.sealedTypedModuleSemantic freshRoot) (Module.sealedTypedModuleSemantic editedRoot) rejectsFixedSemanticDeclaration :: Assertion rejectsFixedSemanticDeclaration = Temp.withSystemTempDirectory "felix-fixed-semantic" \root -> do let relative = "entry.tex" path = root Posix. relative source = "\\begin{signature}\\label{source_unions}\n" <> " $\\unions{X}$ is a set.\n" <> "\\end{signature}\n" ByteString.writeFile path (Text.encodeUtf8 (StrictText.pack source)) foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts root workspace <- parseExactWorkspace bootstrap mounts relative let parsed = Parse.parsedWorkspaceRootModule workspace input <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) unusedResolver Declaration.FreshValidation parsed []) Module.runTypedModule input >>= \case Module.TypedModuleFailed (Module.TypedActionFailed (Module.TypedExactCompileFailed (Exact.ExactFixedSemanticCollision location key))) prefix -> do assertEqual "fixed collision line" 1 (locLine location) assertEqual "fixed collision key" (Semantic.SemanticExpressionFunction (Raw.TokenCons (Raw.Command "unions") (Raw.TokenCons Raw.InvisibleBraceL (Raw.HoleCons (Raw.TokenCons Raw.InvisibleBraceR Raw.End))))) key assertEqual "fixed collision commits no prefix" 0 (length (Declaration.pendingModulePrefixBatches prefix)) Module.TypedModuleSucceeded{} -> assertFailure "fixed semantic declaration was accepted" Module.TypedModuleOpenFailed failure -> assertFailure ("fixed semantic module did not open: " <> show failure) Module.TypedModuleFailed failure _prefix -> assertFailure ("unexpected fixed semantic failure: " <> show failure) rejectsFixedSemanticInductive :: Assertion rejectsFixedSemanticInductive = Temp.withSystemTempDirectory "felix-fixed-inductive" \root -> do let relative = "entry.tex" path = root Posix. relative source = "\\begin{inductive}\\label{source_pow}\n" <> " Define $\\pow{A}\\subseteq\\cumul{A}$ inductively as follows.\n" <> " \\begin{enumerate}\n" <> " \\item $A\\in\\pow{A}$.\n" <> " \\end{enumerate}\n" <> "\\end{inductive}\n" ByteString.writeFile path (Text.encodeUtf8 (StrictText.pack source)) foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts root workspace <- parseExactWorkspace bootstrap mounts relative let parsed = Parse.parsedWorkspaceRootModule workspace input <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) unusedResolver Declaration.FreshValidation parsed []) Module.runTypedModule input >>= \case Module.TypedModuleFailed (Module.TypedActionFailed (Module.TypedExactInductiveFailed (ExactInductive.ExactInductiveFixedSemanticCollision location key))) prefix -> do assertEqual "fixed inductive collision line" 1 (locLine location) assertEqual "fixed inductive collision key" (Semantic.SemanticExpressionFunction (Raw.TokenCons (Raw.Command "pow") (Raw.TokenCons Raw.InvisibleBraceL (Raw.HoleCons (Raw.TokenCons Raw.InvisibleBraceR Raw.End))))) key assertEqual "fixed inductive collision commits no prefix" 0 (length (Declaration.pendingModulePrefixBatches prefix)) Module.TypedModuleSucceeded{} -> assertFailure "fixed semantic inductive was accepted" Module.TypedModuleOpenFailed failure -> assertFailure ("fixed semantic inductive did not open: " <> show failure) Module.TypedModuleFailed failure _prefix -> assertFailure ("unexpected fixed inductive failure: " <> show failure) keepsExactSemanticsIndependentOfFixity :: Assertion keepsExactSemanticsIndependentOfFixity = Temp.withSystemTempDirectory "felix-exact-fixity" \root -> do let relative = "test/phase5/exact-producer.tex" path = root Posix. relative createDirectoryIfMissing True (Posix.takeDirectory path) original <- ByteString.readFile relative let changed = Text.encodeUtf8 (StrictText.replace "infixl 2" "infixr 6" (Text.decodeUtf8 original)) ByteString.writeFile path original first <- compileExactRootAt root relative ByteString.writeFile path changed second <- compileExactRootAt root relative let firstParsed = Parse.parsedWorkspaceRootModule (fst first) secondParsed = Parse.parsedWorkspaceRootModule (fst second) firstSealed = snd first secondSealed = snd second assertBool "fixity changes syntax identity" (Syntax.moduleSyntaxAssertedId (Parse.parsedModuleSyntaxInterface firstParsed) /= Syntax.moduleSyntaxAssertedId (Parse.parsedModuleSyntaxInterface secondParsed)) assertBool "fixity changes parsed identity" (Parse.parsedModuleId firstParsed /= Parse.parsedModuleId secondParsed) assertEqual "fixity preserves semantic interface" (Module.sealedTypedModuleSemantic firstSealed) (Module.sealedTypedModuleSemantic secondSealed) assertEqual "fixity preserves semantic prefix" (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix firstSealed)) (Declaration.pendingModulePrefixCurrent (Module.sealedTypedModulePrefix secondSealed)) loadsCachedExactProducerForFreshImporter :: Assertion loadsCachedExactProducerForFreshImporter = do foundation <- expectRight Foundation.checkedFoundation Temp.withSystemTempDirectory "felix-exact-cache" \root -> do let path = root Posix. "store.sqlite" executable = root Posix. "vampire" writeAcceptedFixtureVampire executable (_startup, store) <- Store.openStore path (Identity.theoryId foundation) >>= expectRight let observer = Verification.verificationRequestObserver \_ordinal _request -> pure () prover = Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit verify mode source = (checkResultWithStore store mode observer prover source) >>= expectRight producer <- verify Verification.FreshStoreValidation "test/phase5/exact-producer.tex" importer <- verify Verification.WarmStoreValidation "test/phase5/exact-importer.tex" assertTypedSuccess "fresh producer" producer assertTypedSuccess "warm producer/fresh importer" importer memo <- Store.newStoreMemo store prelude <- expectRight =<< Module.acquireFinalPreludeSession memo store foundation unusedResolver preludeVisits <- Store.storeMemoVisits memo repository <- getCurrentDirectory mounts <- exactFixtureMounts repository workspace <- parseFinalExactWorkspace prelude mounts "test/phase5/exact-importer.tex" let parsedModules = toList (Parse.parsedWorkspaceImportedBeforeImporter workspace) preludeSemantic = Module.sealedTypedModuleSemantic (Module.finalPreludeModule prelude) preludeId = Semantic.semanticInterfaceAssertedId preludeSemantic theory = Identity.theoryId foundation loadInstallation parsed direct = do key <- expectRight (Semantic.moduleArtifactKey (moduleName (Parse.parsedModuleAddress parsed)) (Parse.parsedModuleId parsed) direct theory) loaded <- expectRight =<< Store.loadCachedModuleInstallation memo store key (Syntax.moduleSyntaxAssertedId (Parse.parsedModuleSyntaxInterface parsed)) maybe (assertFailure "exact cached installation is absent" >> fail "unreachable") pure loaded environmentBindings installation = [ binding | delta <- Semantic.semanticInterfaceDeclarations (Store.cachedInstallationSemantic installation) , binding <- Semantic.semanticEnvironmentBindings (Semantic.declarationDeltaEnvironment delta) ] case parsedModules of [producerParsed, importerParsed] -> do producerInstallation <- loadInstallation producerParsed [preludeId] producerVisits <- Store.storeMemoVisits memo assertEqual "ordinary root adds one artifact validation" (Store.storeArtifactsValidated preludeVisits + 1) (Store.storeArtifactsValidated producerVisits) assertEqual "ordinary root reuses prelude syntax validation" (Store.storeSyntaxRowsValidated preludeVisits + 1) (Store.storeSyntaxRowsValidated producerVisits) assertEqual "ordinary root reuses prelude semantic validation" (Store.storeSemanticRowsValidated preludeVisits + 1) (Store.storeSemanticRowsValidated producerVisits) let producerSemanticId = Semantic.semanticInterfaceAssertedId (Store.cachedInstallationSemantic producerInstallation) importerInstallation <- loadInstallation importerParsed [preludeId, producerSemanticId] case ( environmentBindings producerInstallation , environmentBindings importerInstallation ) of (seedBinding : aliasBinding : _definitionBinding : [], [importerBinding]) -> do let seedTarget = Semantic.semanticGlobalTargetObject (Semantic.semanticGlobalBindingTarget seedBinding) aliasTarget = Semantic.semanticGlobalTargetObject (Semantic.semanticGlobalBindingTarget aliasBinding) importerTarget = Semantic.semanticGlobalTargetObject (Semantic.semanticGlobalBindingTarget importerBinding) assertEqual "cached importer reuses expanded content" aliasTarget importerTarget assertEqual "cached importer adds no object" [] (Store.cachedInstallationObjects importerInstallation) expandedObject <- maybe (assertFailure "cached expanded object is absent" >> fail "unreachable") pure (find ((== aliasTarget) . Identity.assertedObjectId) (Store.cachedInstallationObjects producerInstallation)) case Identity.assertedObjectContent expandedObject of Identity.TransparentObjectContent _identity _coreType body -> assertEqual "cached expansion retains the opaque seed" (Set.singleton seedTarget) (Core.canonicalTermGlobals body) content -> assertFailure ("cached expansion is not transparent: " <> show content) (producerBindings, importerBindings) -> assertFailure ("unexpected cached exact bindings: " <> show ( length producerBindings , length importerBindings )) modules -> assertFailure ("unexpected cached exact module count: " <> show (length modules)) Store.closeStore store selectsConcurrentModuleFailureDeterministically :: Assertion selectsConcurrentModuleFailureDeterministically = do foundation <- expectRight Foundation.checkedFoundation Temp.withSystemTempDirectory "felix-concurrent-module-failure" \root -> do let executable = root Posix. "vampire" source = "test/phase7/concurrent-failure-root.tex" prover = Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit ignored = Verification.verificationRequestObserver (\_position _request -> pure ()) select amount = Provers.selectEffectiveJobs (Provers.effectiveJobs amount) (fail "explicit jobs unexpectedly detected processors") reportEntry escape = ( Verification.reportedEscapeKind escape , locFile (Verification.reportedEscapeLocation escape) , locLine (Verification.reportedEscapeLocation escape) ) inspect label expectedPositions (result, _slowReport, positions) = do case result of Verification.VerificationFailure report failed -> do assertEqual (label <> " selected earlier failure") "test/phase7/concurrent-earlier.tex" (locFile (Verification.failedVerificationLocation failed)) assertEqual (label <> " admitted source prefix") [ ( Verification.ReportedSourceAxiom , "test/phase7/concurrent-earlier.tex" , 1 ) ] (reportEntry <$> Verification.verificationDirectEscapes report) other -> assertFailure (label <> " did not reject deterministically: " <> show other) assertEqual (label <> " executed only sibling obligations") expectedPositions (sort [ ( Provers.workPositionModuleOrdinal position , Provers.workPositionLocalRequestOrdinal position ) | position <- positions ]) runCase label jobsAmount = do let storePath = root Posix. (label <> ".sqlite") processLock = root Posix. (label <> ".process-lock") processStarted = root Posix. (label <> ".process-started") writeAcceptedFixtureVampire executable (_startup, store) <- Store.openStore storePath (Identity.theoryId foundation) >>= expectRight bracket (pure store) Store.closeStore \openStore -> do -- Seed only the final prelude. The unsupported ordinary -- module cannot publish a root. void ( (checkFileWithStore openStore Verification.WarmStoreValidation ignored prover "test/phase3/typed-unsupported.tex") >>= expectRight) writeFile executable (unlines [ "#!/bin/sh" , "while ! mkdir \"" <> processLock <> "\" 2>/dev/null; do sleep 0.01; done" , "trap 'rmdir \"" <> processLock <> "\"' EXIT" , ": > \"" <> processStarted <> "\"" , "cat >/dev/null" , "printf '%s\\n' '% SZS status CounterSatisfiable for concurrent-fixture'" ]) permissions <- getPermissions executable setPermissions executable (setOwnerExecutable True permissions) positionsRef <- newIORef [] let observer = Verification.verificationRequestObserver (\position _request -> do atomicModifyIORef' positionsRef (\positions -> (position : positions, ())) when (jobsAmount > 1 && Provers.workPositionModuleOrdinal position == 1) (waitForFileSignal "later module process" processStarted)) jobs <- select jobsAmount (result, slowReport) <- (checkFileWithStoreAndJobs openStore Verification.WarmStoreValidation jobs observer prover source) >>= expectRight positions <- readIORef positionsRef pure (result, slowReport, positions) void $ runCase "parallel" 2 >>= inspect "parallel" [(1, 1), (2, 1)] void $ runCase "sequential" 1 >>= inspect "sequential" [(1, 1)] waitForFileSignal :: String -> FilePath -> Assertion waitForFileSignal label path = do guarded <- Timeout.timeout 10000000 loop case guarded of Just () -> pure () Nothing -> assertFailure (label <> " was not observed") where loop = do exists <- doesFileExist path if exists then pure () else do threadDelay 10000 loop batchesStructureObligationsAtomically :: Assertion batchesStructureObligationsAtomically = do foundation <- expectRight Foundation.checkedFoundation Temp.withSystemTempDirectory "felix-structure-obligation-batch" \root -> do let storePath = root Posix. "store.sqlite" executable = root Posix. "vampire" unavailable = root Posix. "must-not-run-vampire" source = "test/phase7/structure-obligation-batch.tex" prover path = Provers.vampire path Provers.defaultTimeLimit Provers.defaultMemoryLimit select amount = Provers.selectEffectiveJobs (Provers.effectiveJobs amount) (fail "explicit jobs unexpectedly detected processors") run openStore jobs observer vampireCommand = (checkFileWithStoreAndJobs openStore Verification.WarmStoreValidation jobs observer vampireCommand source) >>= expectRight inspectFailure label positions (result, _slowReport) = do case result of Verification.VerificationFailure report failed -> do assertEqual (label <> " selects first consequence") (source, 12) ( locFile (Verification.failedVerificationLocation failed) , locLine (Verification.failedVerificationLocation failed) ) assertEqual (label <> " retains preceding prefix") [(Verification.ReportedSourceAxiom, source, 1)] [ ( Verification.reportedEscapeKind escape , locFile (Verification.reportedEscapeLocation escape) , locLine (Verification.reportedEscapeLocation escape) ) | escape <- Verification.verificationDirectEscapes report ] other -> assertFailure (label <> " did not reject its structure batch: " <> show other) assertEqual (label <> " assigns consecutive positions") [(1, 1), (1, 2)] (sort positions) writeAcceptedFixtureVampire executable (_startup, store) <- Store.openStore storePath (Identity.theoryId foundation) >>= expectRight bracket (pure store) Store.closeStore \openStore -> do let ignored = Verification.verificationRequestObserver (\_position _request -> pure ()) -- Seed only the confined prelude so this fixture observes exactly -- the ordinary structure module's ready batch. void ( (checkFileWithStore openStore Verification.WarmStoreValidation ignored (prover executable) "test/phase3/typed-unsupported.tex") >>= expectRight) parallelJobs <- select 2 parallelPositions <- newIORef [] firstStarted <- newEmptyTMVarIO secondStarted <- newEmptyTMVarIO releaseFirst <- newEmptyTMVarIO let laterCompleted = root Posix. "later-completed" writeLaterAcceptingVampire executable laterCompleted let parallelObserver = Verification.verificationRequestObserver \position _request -> do let ordinal = Provers.workPositionLocalRequestOrdinal position atomicModifyIORef' parallelPositions (\positions -> ( ( Provers.workPositionModuleOrdinal position , ordinal ) : positions , () )) case ordinal of 1 -> do atomically (putTMVar firstStarted ()) atomically (takeTMVar releaseFirst) 2 -> atomically (putTMVar secondStarted ()) _ -> assertFailure ("unexpected structure request ordinal: " <> show ordinal) withAsync (run openStore parallelJobs parallelObserver (prover executable)) \verification -> do void (awaitSignal "first structure request" (atomically (takeTMVar firstStarted))) void (awaitSignal "second structure request" (atomically (takeTMVar secondStarted))) -- Only the later member can reach the subprocess while -- the first observer is gated. Its completed signal -- therefore establishes reversed wall-clock completion. waitForFileSignal "later structure consequence" laterCompleted atomically (putTMVar releaseFirst ()) parallelResult <- wait verification positions <- readIORef parallelPositions inspectFailure "parallel" positions parallelResult sequentialJobs <- select 1 sequentialPositions <- newIORef [] let sequentialCompleted = root Posix. "sequential-completed" writeRejectingVampire executable sequentialCompleted let sequentialObserver = Verification.verificationRequestObserver \position _request -> atomicModifyIORef' sequentialPositions (\positions -> ( ( Provers.workPositionModuleOrdinal position , Provers.workPositionLocalRequestOrdinal position ) : positions , () )) sequentialResult <- run openStore sequentialJobs sequentialObserver (prover executable) sequentialObserved <- readIORef sequentialPositions inspectFailure "sequential" sequentialObserved sequentialResult -- A rejected sibling wrote neither validation nor a module root: -- the complete batch executes again, while the earlier source -- axiom remains the admitted prefix. A subsequent hit executes -- no request at all. writeAcceptedFixtureVampire executable acceptedPositions <- newIORef [] let acceptedObserver = Verification.verificationRequestObserver \position _request -> modifyIORef' acceptedPositions (position :) (accepted, _acceptedSlowReport) <- run openStore parallelJobs acceptedObserver (prover executable) case accepted of Verification.VerificationCompleted report _presentation -> assertEqual "successful retry retains only source axiom" [Verification.ReportedSourceAxiom] (Verification.reportedEscapeKind <$> Verification.verificationDirectEscapes report) other -> assertFailure ("successful structure retry failed: " <> show other) acceptedObserved <- readIORef acceptedPositions assertEqual "successful retry executes the complete batch" 2 (length acceptedObserved) let forbiddenObserver = Verification.verificationRequestObserver \position _request -> assertFailure ("warm structure batch invoked Vampire at " <> show position) (warm, _warmSlowReport) <- run openStore parallelJobs forbiddenObserver (prover unavailable) case warm of Verification.VerificationCompleted{} -> pure () other -> assertFailure ("warm structure batch did not install: " <> show other) where awaitSignal label action = do result <- Timeout.timeout 10000000 action maybe (assertFailure (label <> " was not observed") >> fail "unreachable") pure result writeRejectingVampire executable completed = do writeFile executable (unlines [ "#!/bin/sh" , "cat >/dev/null" , ": > \"" <> completed <> "\"" , "printf '%s\\n' '% SZS status CounterSatisfiable for structure-batch-fixture'" ]) permissions <- getPermissions executable setPermissions executable (setOwnerExecutable True permissions) writeLaterAcceptingVampire executable completed = do let firstProcess = completed <> ".first-process" writeFile executable (unlines [ "#!/bin/sh" , "cat >/dev/null" , ": > \"" <> completed <> "\"" , "if mkdir \"" <> firstProcess <> "\" 2>/dev/null; then" , " printf '%s\\n' '% SZS status Theorem for structure-batch-fixture'" , "else" , " printf '%s\\n' '% SZS status CounterSatisfiable for structure-batch-fixture'" , "fi" ]) permissions <- getPermissions executable setPermissions executable (setOwnerExecutable True permissions) speculatesDependentProofObligationsWithoutAdmittingAhead :: Assertion speculatesDependentProofObligationsWithoutAdmittingAhead = do foundation <- expectRight Foundation.checkedFoundation Temp.withSystemTempDirectory "felix-dependent-proof-chain" \root -> do let executable = root Posix. "vampire" unavailable = root Posix. "must-not-run-vampire" storePath = root Posix. "store.sqlite" source = "test/phase7/dependent-proof-chain.tex" prover path = Provers.vampire path Provers.defaultTimeLimit Provers.defaultMemoryLimit ignored = Verification.verificationRequestObserver (\_position _request -> pure ()) writeAcceptedFixtureVampire executable (_startup, store) <- Store.openStore storePath (Identity.theoryId foundation) >>= expectRight bracket (pure store) Store.closeStore \openStore -> do -- Seed only the final prelude so the observed work belongs to the -- ordinary proof module. void ( (checkFileWithStore openStore Verification.WarmStoreValidation ignored (prover executable) "test/phase3/typed-unsupported.tex") >>= expectRight) jobs <- Provers.selectEffectiveJobs (Provers.effectiveJobs 2) (fail "explicit jobs unexpectedly detected processors") firstStarted <- newEmptyTMVarIO secondStarted <- newEmptyTMVarIO releaseFirst <- newEmptyTMVarIO positionsRef <- newIORef [] let observer = Verification.verificationRequestObserver \position _request -> do let ordinal = Provers.workPositionLocalRequestOrdinal position atomicModifyIORef' positionsRef (\positions -> ( ( Provers.workPositionModuleOrdinal position , ordinal ) : positions , () )) case ordinal of 1 -> do atomically (putTMVar firstStarted ()) atomically (takeTMVar releaseFirst) 2 -> atomically (putTMVar secondStarted ()) _ -> assertFailure ("unexpected dependent proof request: " <> show ordinal) withAsync ( (checkFileWithStoreAndJobs openStore Verification.WarmStoreValidation jobs observer (prover executable) source) >>= expectRight) \checking -> do void (awaitSignal "local subclaim request" (atomically (takeTMVar firstStarted))) -- The continuation is semantically dependent, but its -- already checked request may execute prospectively. It -- cannot be admitted until the local claim succeeds. void (awaitSignal "dependent continuation request" (atomically (takeTMVar secondStarted))) atomically (putTMVar releaseFirst ()) (result, _slowReport) <- wait checking case result of Verification.VerificationCompleted report _presentation -> assertEqual "only the preceding axiom is reported" [Verification.ReportedSourceAxiom] (Verification.reportedEscapeKind <$> Verification.verificationDirectEscapes report) other -> assertFailure ("dependent proof module did not seal: " <> show other) positions <- readIORef positionsRef assertEqual "dependent requests retain source positions" [(1, 1), (1, 2)] (sort positions) let forbiddenObserver = Verification.verificationRequestObserver \position _request -> assertFailure ("warm dependent proof invoked Vampire at " <> show position) (warm, _warmSlowReport) <- (checkFileWithStoreAndJobs openStore Verification.WarmStoreValidation jobs forbiddenObserver (prover unavailable) source) >>= expectRight case warm of Verification.VerificationCompleted{} -> pure () other -> assertFailure ("warm dependent proof did not install: " <> show other) where awaitSignal label action = do result <- Timeout.timeout 10000000 action maybe (assertFailure (label <> " was not observed") >> fail "unreachable") pure result schedulesDiamondAfterSealedImports :: Assertion schedulesDiamondAfterSealedImports = do foundation <- expectRight Foundation.checkedFoundation Temp.withSystemTempDirectory "felix-concurrent-diamond" \root -> do let storePath = root Posix. "store.sqlite" executable = root Posix. "vampire" unavailable = root Posix. "must-not-run-vampire" source = "test/phase7/diamond-root.tex" prover path = Provers.vampire path Provers.defaultTimeLimit Provers.defaultMemoryLimit ignored = Verification.verificationRequestObserver (\_position _request -> pure ()) writeAcceptedFixtureVampire executable (_startup, store) <- Store.openStore storePath (Identity.theoryId foundation) >>= expectRight bracket (pure store) Store.closeStore \openStore -> do -- Acquire the final prelude before introducing scheduler gates. void ( (checkFileWithStore openStore Verification.WarmStoreValidation ignored (prover executable) "test/phase3/typed-unsupported.tex") >>= expectRight) jobs <- Provers.selectEffectiveJobs (Provers.effectiveJobs 2) (fail "explicit jobs unexpectedly detected processors") baseStarted <- newEmptyTMVarIO branchStarted <- newTQueueIO rootStarted <- newEmptyTMVarIO releaseBase <- newTVarIO False releaseBranches <- newTVarIO False let awaitRelease released = atomically (readTVar released >>= check) observer = Verification.verificationRequestObserver (\position _request -> case Provers.workPositionModuleOrdinal position of 1 -> do atomically (putTMVar baseStarted ()) awaitRelease releaseBase ordinal@2 -> do atomically (writeTQueue branchStarted ordinal) awaitRelease releaseBranches ordinal@3 -> do atomically (writeTQueue branchStarted ordinal) awaitRelease releaseBranches 4 -> atomically (putTMVar rootStarted ()) _ -> pure ()) verify vampireCommand requestObserver = (checkFileWithStoreAndJobs openStore Verification.WarmStoreValidation jobs requestObserver vampireCommand source) >>= expectRight await label action = do result <- Timeout.timeout 10000000 action maybe (assertFailure (label <> " was not observed") >> fail "unreachable") pure result withAsync (verify (prover executable) observer) \verification -> do void (await "base request" (atomically (takeTMVar baseStarted))) threadDelay 50000 atomically (tryReadTQueue branchStarted) >>= \case Nothing -> pure () Just ordinal -> assertFailure ("dependent module started before base seal: " <> show ordinal) atomically (writeTVar releaseBase True) firstBranch <- await "first branch" (atomically (readTQueue branchStarted)) secondBranch <- await "second branch" (atomically (readTQueue branchStarted)) assertEqual "both diamond branches became ready together" [2, 3] (sort [firstBranch, secondBranch]) atomically (tryReadTMVar rootStarted) >>= \case Nothing -> pure () Just () -> assertFailure "diamond root started before both branch seals" atomically (writeTVar releaseBranches True) void (await "diamond root" (atomically (takeTMVar rootStarted))) (coldResult, _coldSlowReport) <- wait verification case coldResult of Verification.VerificationCompleted{} -> pure () other -> assertFailure ("cold diamond did not complete: " <> show other) let forbiddenObserver = Verification.verificationRequestObserver (\position _request -> assertFailure ("warm diamond invoked Vampire at " <> show position)) (warmResult, _warmSlowReport) <- verify (prover unavailable) forbiddenObserver case warmResult of Verification.VerificationCompleted{} -> pure () other -> assertFailure ("warm diamond did not install: " <> show other) reportsAdmittedSourceEscapes :: Assertion reportsAdmittedSourceEscapes = do foundation <- expectRight Foundation.checkedFoundation Temp.withSystemTempDirectory "felix-admitted-source-report" \root -> do let storePath = root Posix. "store.sqlite" executable = root Posix. "vampire" unavailable = root Posix. "must-not-run-vampire" observer = Verification.verificationRequestObserver \_ordinal _request -> pure () prover path = Provers.vampire path Provers.defaultTimeLimit Provers.defaultMemoryLimit writeAcceptedFixtureVampire executable (_startup, store) <- Store.openStore storePath (Identity.theoryId foundation) >>= expectRight bracket (pure store) Store.closeStore \openStore -> do let verify mode vampirePath source = (checkFileWithStore openStore mode observer (prover vampirePath) source) >>= expectRight reportEntries = fmap (\escape -> ( Verification.reportedEscapeKind escape , locFile (Verification.reportedEscapeLocation escape) , locLine (Verification.reportedEscapeLocation escape) )) . Verification.verificationDirectEscapes expectedConsumer = [ ( Verification.ReportedSourceAxiom , "test/phase5/exact-escape-producer.tex" , 1 ) , ( Verification.ReportedOmitted , "test/phase5/exact-escape-producer.tex" , 9 ) , ( Verification.ReportedOmitted , "test/phase5/exact-escape-consumer.tex" , 35 ) ] (freshResult, _freshSlowReport) <- verify Verification.FreshStoreValidation executable "test/phase5/exact-escape-consumer.tex" freshReport <- case freshResult of Verification.CompletedWithExplicitGaps report _presentation -> pure report other -> assertFailure ("fresh escape report did not complete with gaps: " <> show other) >> fail "unreachable" assertEqual "fresh direct escapes" expectedConsumer (reportEntries freshReport) (warmResult, _warmSlowReport) <- verify Verification.WarmStoreValidation unavailable "test/phase5/exact-escape-consumer.tex" warmReport <- case warmResult of Verification.CompletedWithExplicitGaps report _presentation -> pure report other -> assertFailure ("warm escape report did not complete with gaps: " <> show other) >> fail "unreachable" assertEqual "warm report uses rebound current locations" freshReport warmReport void (verify Verification.FreshStoreValidation executable "test/phase5/exact-source-axiom.tex") (failedResult, _failedSlowReport) <- verify Verification.WarmStoreValidation unavailable "test/phase6/admitted-prefix-failure.tex" failedReport <- case failedResult of Verification.VerificationCheckingFailure report _failure -> pure report other -> assertFailure ("typed suffix failure was not report-bearing: " <> show other) >> fail "unreachable" assertEqual "failure report retains only admitted source prefix" (take 2 expectedConsumer <> [ ( Verification.ReportedOmitted , "test/phase6/admitted-prefix-failure.tex" , 7 ) ]) (reportEntries failedReport) classifiesTypedVampireFailures :: Assertion classifiesTypedVampireFailures = do foundation <- expectRight Foundation.checkedFoundation Temp.withSystemTempDirectory "felix-typed-failure-classification" \root -> do let storePath = root Posix. "store.sqlite" executable = root Posix. "vampire" observer = Verification.verificationRequestObserver \_ordinal _request -> pure () prover = Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit writeAcceptedFixtureVampire executable (_startup, store) <- Store.openStore storePath (Identity.theoryId foundation) >>= expectRight bracket (pure store) Store.closeStore \openStore -> do let verify source = (checkFileWithStore openStore Verification.WarmStoreValidation observer prover source) >>= expectRight writeProtocol lines = do writeFile executable (unlines (["#!/bin/sh", "cat >/dev/null"] <> lines)) permissions <- getPermissions executable setPermissions executable (setOwnerExecutable True permissions) expectTypedFailure classify = do (result, slowReport) <- verify "test/phase5/exact-runtime-failure.tex" case result of Verification.VerificationFailure report failed -> do assertEqual "typed failure has no direct escapes" [] (Verification.verificationDirectEscapes report) assertEqual "typed failure retains source location" "test/phase5/exact-runtime-failure.tex" (locFile (Verification.failedVerificationLocation failed)) classify (Verification.failedVerificationReason failed) (CommandLine.verificationCommandOutcome result slowReport) other -> assertFailure ("typed prover outcome was misclassified: " <> show other) -- Populate only the confined prelude. The selected ordinary -- module then remains a miss for each classified live failure. (_preludeResult, _preludeSlowReport) <- verify "test/phase3/typed-unsupported.tex" writeProtocol [ "printf '%s\\n' '% SZS status CounterSatisfiable for typed-failure'" , "exit 0" ] expectTypedFailure \reason outcome -> do case reason of Verification.CountermodelFailure{} -> pure () other -> assertFailure ("expected countermodel: " <> show other) case outcome of CommandLine.VerificationRejected{} -> pure () other -> assertFailure ("expected rejection: " <> show other) writeProtocol [ "printf '%s\\n' '% SZS status Timeout for typed-failure'" , "exit 0" ] expectTypedFailure \reason outcome -> do case reason of Verification.IndeterminateFailure{} -> pure () other -> assertFailure ("expected indeterminate result: " <> show other) case outcome of CommandLine.VerificationRejected{} -> pure () other -> assertFailure ("expected prover failure: " <> show other) writeProtocol [ "printf '%s\\n' '% SZS status Theorem for typed-failure'" , "exit 7" ] expectTypedFailure \reason outcome -> do case reason of Verification.ProtocolFailure{} -> pure () other -> assertFailure ("expected protocol failure: " <> show other) case outcome of CommandLine.VerificationRejected{} -> pure () other -> assertFailure ("expected prover failure: " <> show other) writeFile executable "not executable" permissions <- getPermissions executable setPermissions executable (setOwnerExecutable False permissions) expectTypedFailure \reason outcome -> do case reason of Verification.TransportFailure{} -> pure () other -> assertFailure ("expected transport failure: " <> show other) case outcome of CommandLine.VerificationRejected{} -> pure () other -> assertFailure ("expected prover failure: " <> show other) retainsExactPrefixBeforeFailure :: Assertion retainsExactPrefixBeforeFailure = do result <- withAcceptedFixtureVampire "felix-exact-failure" \prover -> (checkFileFresh prover "test/phase5/exact-failure.tex") case result of Right ( Verification.VerificationCheckingFailure _report (Verification.VerificationTypedModuleError source (Module.TypedActionFailed (Module.TypedExactCompileFailed (Exact.ExactGuardedOpaqueSignature location))) prefix) , _slowReport ) -> do assertEqual "failed exact source" "test/phase5/exact-failure.tex" (safeRelativePathFilePath (resolvedSourceRelativePath source)) assertEqual "unsupported declaration line" 6 (locLine location) assertEqual "earlier exact declaration remains committed" 1 (length (Declaration.pendingModulePrefixBatches prefix)) Left err -> assertFailure ("unexpected exact failure: " <> show err) Right{} -> assertFailure "unsupported declaration was admitted" proofFailure <- withAcceptedFixtureVampire "felix-exact-proof-failure" \prover -> (checkFileFresh prover "test/phase5/exact-proof-failure.tex") case proofFailure of Right ( Verification.VerificationCheckingFailure _report (Verification.VerificationTypedModuleError _source (Module.TypedActionFailed (Module.TypedExactProofFailed (ExactProof.ExactProofGoalStatementMismatch location))) prefix) , _slowReport ) -> do assertEqual "mismatched assumption line" 10 (locLine location) assertEqual "failed proof publishes no theorem" 1 (length (Declaration.pendingModulePrefixBatches prefix)) Left err -> assertFailure ("unexpected exact proof failure: " <> show err) Right{} -> assertFailure "mismatched exact proof was admitted" unmatched <- withAcceptedFixtureVampire "felix-unmatched-proof" \prover -> (checkFileFresh prover "test/phase5/unmatched-proof.tex") case unmatched of Right ( Verification.VerificationCheckingFailure _report (Verification.VerificationTypedModuleError _source (Module.TypedActionFailed (Module.TypedUnmatchedProof location)) prefix) , _slowReport ) -> do assertEqual "unmatched proof line" 1 (locLine location) assertEqual "unmatched proof publishes no declaration" 0 (length (Declaration.pendingModulePrefixBatches prefix)) Left err -> assertFailure ("unexpected unmatched-proof failure: " <> show err) Right{} -> assertFailure "unmatched proof was admitted" runtimeFailure <- Temp.withSystemTempDirectory "felix-runtime-proof-failure" \root -> do foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver repository <- getCurrentDirectory mounts <- exactFixtureMounts repository workspace <- parseExactWorkspace bootstrap mounts "test/phase5/exact-runtime-failure.tex" let executable = root Posix. "vampire" writeFile executable (unlines [ "#!/bin/sh" , "cat >/dev/null" , "printf '%s\\n' '% SZS status Theorem for located-proof'" ]) permissions <- getPermissions executable setPermissions executable (setOwnerExecutable True permissions) runs <- newIORef (0 :: Int) let resolver = Declaration.vampireResolver \prepared -> do runNumber <- readIORef runs modifyIORef' runs (+ 1) if runNumber == 0 then (Provers.runPreparedTypedProver (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) else pure (Right (Provers.CounterSatisfiable "later exact obligation")) parsed = Parse.parsedWorkspaceRootModule workspace input <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) resolver Declaration.FreshValidation parsed []) Module.runTypedModule input case runtimeFailure of Module.TypedModuleFailed failure@(Module.TypedDeclarationFailed (Declaration.ProofObligationFailedAt location Declaration.VampireObligationRejected{})) prefix -> do assertEqual "later rejected obligation line" 11 (locLine location) assertEqual "typed failure retains obligation location" (Just location) (Module.typedModuleFailureLocation failure) assertEqual "runtime proof failure publishes no theorem" 1 (length (Declaration.pendingModulePrefixBatches prefix)) _result -> assertFailure "unexpected runtime proof failure" restoresCheckedSetInduction :: Assertion restoresCheckedSetInduction = Temp.withSystemTempDirectory "felix-checked-set-induction" \root -> do let executable = root Posix. "vampire" storePath = root Posix. "store.sqlite" writeAcceptedFixtureVampire executable foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts =<< getCurrentDirectory initialWorkspace <- parseExactWorkspace bootstrap mounts "test/phase5/exact-induction-initial.tex" initialObservations <- newIORef [] initial <- sole "initial set-induction module" =<< compileParsedWorkspaceWithValidation foundation bootstrap (observingResolver executable initialObservations) Declaration.FreshValidation initialWorkspace [initialRequest] <- expectCount "initial set-induction request" 1 =<< readIORef initialObservations assertEqual "initial induction retains header then hypothesis ordinals" [0, 1] (localReasoningLocalOrdinals initialRequest) let initialTarget = Core.CEq Core.TySet (Core.CBound 0) (Core.CBound 0) initialAntecedent = member (Core.CBound 1) (Core.CBound 0) initialHypothesis = Core.CForall Core.TySet (Core.CImp (member (Core.CBound 0) (Core.CBound 2)) (Core.CImp (member (Core.CBound 0) (Core.CBound 1)) (Core.CEq Core.TySet (Core.CBound 0) (Core.CBound 0)))) assertEqual "initial induction child target" initialTarget (localReasoningTarget initialRequest) assertEqual "initial induction uses the complete guarded property" [initialAntecedent, initialHypothesis] (localReasoningLocalTerms initialRequest) nestedWorkspace <- parseExactWorkspace bootstrap mounts "test/phase5/exact-induction-nested.tex" nestedObservations <- newIORef [] nested <- sole "nested set-induction module" =<< compileParsedWorkspaceWithValidation foundation bootstrap (observingResolver executable nestedObservations) Declaration.FreshValidation nestedWorkspace [nestedChild, nestedContinuation] <- expectCount "nested set-induction requests" 2 =<< readIORef nestedObservations let x = Core.CBound 0 a = Core.CBound 1 y = Core.CBound 0 xUnderY = Core.CBound 1 aUnderY = Core.CBound 2 guardAtX = andP (member x a) (notP (Core.CEq Core.TySet x a)) guardAtY = andP (member y aUnderY) (notP (Core.CEq Core.TySet y aUnderY)) nestedHypothesis = Core.CForall Core.TySet (Core.CImp (member y xUnderY) (Core.CImp guardAtY (Core.CEq Core.TySet y y))) nestedTarget = Core.CEq Core.TySet x x assertEqual "omitted leading induction retains its source binder and guard" ([0, 1], [nestedHypothesis, guardAtX], nestedTarget) ( localReasoningLocalOrdinals nestedChild , localReasoningLocalTerms nestedChild , localReasoningTarget nestedChild ) case localReasoningLocalTerms nestedContinuation of [derived] -> do assertEqual "subproof continuation uses one derived local" [2] (localReasoningLocalOrdinals nestedContinuation) assertEqual "subproof closes the exact binder-level result" derived (localReasoningTarget nestedContinuation) locals -> assertFailure ("unexpected induction continuation locals: " <> show locals) formulaWorkspace <- parseExactWorkspace bootstrap mounts "test/phase5/exact-induction-formula-quantified.tex" formulaObservations <- newIORef [] _formula <- sole "formula-quantified set-induction module" =<< compileParsedWorkspaceWithValidation foundation bootstrap (observingResolver executable formulaObservations) Declaration.FreshValidation formulaWorkspace [formulaChild, formulaContinuation] <- expectCount "formula-quantified set-induction requests" 2 =<< readIORef formulaObservations assertEqual "formula-quantified omitted induction retains its written binder" (Core.CEq Core.TySet (Core.CBound 0) (Core.CBound 0)) (localReasoningTarget formulaChild) assertEqual "formula-quantified continuation retains hypothesis and derived local" [0, 1] (localReasoningLocalOrdinals formulaContinuation) anchorWorkspace <- parseExactWorkspace bootstrap mounts "test/examples/no-reflexive-set.tex" anchorObservations <- newIORef [] _anchor <- sole "omitted-focus set-induction module" =<< compileParsedWorkspaceWithValidation foundation bootstrap (observingResolver executable anchorObservations) Declaration.FreshValidation anchorWorkspace [anchorRequest] <- expectCount "omitted-focus set-induction request" 1 =<< readIORef anchorObservations anchorLocal <- case localReasoningLocalTerms anchorRequest of [term] -> pure term terms -> assertFailure ("unexpected omitted-focus locals: " <> show terms) >> fail "unreachable" assertEqual "omitted focus retains its source binder in the child" ([0], Core.CForall Core.TySet (Core.CImp (member (Core.CBound 0) (Core.CBound 1)) (notP (member (Core.CBound 0) (Core.CBound 0))))) ( localReasoningLocalOrdinals anchorRequest , anchorLocal ) assertProofParityFailure foundation bootstrap mounts "test/phase5/exact-induction-ambiguous.tex" (\case ExactProof.ExactProofSetInductionFocusAmbiguous location -> locLine location == 5 _failure -> False) assertProofParityFailure foundation bootstrap mounts "test/phase5/exact-induction-fixed.tex" (\case ExactProof.ExactProofSetInductionActiveBinderIneligible location (Raw.NamedVar "x") -> locLine location == 7 _failure -> False) failedInput <- moduleInput foundation bootstrap initialWorkspace (Declaration.vampireResolver \_prepared -> pure (Right (Provers.CounterSatisfiable "focused induction child rejection"))) Declaration.FreshValidation Module.runTypedModule failedInput >>= \case Module.TypedModuleFailed _failure prefix -> assertBool "failed induction child publishes no theorem" (null (Declaration.pendingModulePrefixBatches prefix)) _result -> assertFailure "rejected induction child unexpectedly succeeded" bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) Store.closeStore \store -> do expectRightIO (Store.writePendingModulePrefix store (Module.sealedTypedModulePrefix nested)) let validation = Declaration.WarmValidation (Declaration.validationLookup (expectRightIO . Store.loadProofValidation store) (expectRightIO . Store.loadDeclarationValidation store)) warmRuns <- newIORef (0 :: Int) warm <- sole "warm nested set-induction module" =<< compileParsedWorkspaceWithValidation foundation bootstrap (countingAcceptedResolver executable warmRuns) validation nestedWorkspace assertEqual "warm set induction skips Vampire" 0 =<< readIORef warmRuns assertEqual "fresh and warm induction proof validations" (proofValidations nested) (proofValidations warm) assertBool "initial induction publishes one theorem" (not (null (Declaration.pendingModulePrefixBatches (Module.sealedTypedModulePrefix initial)))) where observingResolver executable observations = Declaration.vampireResolver \prepared -> do let problem = Provers.preparedTypedProverLogicalProblem prepared locals = Backend.typedProblemLocalPremises problem modifyIORef' observations (<> [ LocalReasoningObservation { localReasoningTarget = Backend.supportedPropositionTerm (Backend.typedProblemClaim problem) , localReasoningGlobalCount = Vector.length (Backend.typedProblemGlobalPremises problem) , localReasoningLocalOrdinals = Backend.localPremiseOrdinalValue . Backend.typedLocalPremiseOrdinal <$> Vector.toList locals , localReasoningLocalTerms = Backend.supportedPropositionTerm . Backend.typedLocalPremiseProposition <$> Vector.toList locals , localReasoningAuxiliaries = Backend.typedProblemAuxiliaryTag <$> Vector.toList (Backend.typedProblemAuxiliaries problem) } ]) (Provers.runPreparedTypedProver (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) expectCount label expected values = do assertEqual label expected (length values) pure values member element set = Core.CApp (Core.CApp (Core.CIntrinsic Core.Member) element) set notP proposition = Core.CImp proposition Core.CFalsum andP left right = notP (Core.CImp left (notP right)) moduleInput foundation bootstrap workspace resolver validation = do parsed <- sole "set-induction parsed module" (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) resolver validation parsed []) proofValidations = concatMap Declaration.committedBatchProofValidations . Declaration.pendingModulePrefixBatches . Module.sealedTypedModulePrefix routesProductionVerification :: Assertion routesProductionVerification = Temp.withSystemTempDirectory "felix-production-route" \directory -> do let executable = directory Posix. "vampire" counter = directory Posix. "runs" writeFile executable (unlines [ "#!/bin/sh" , "cat >/dev/null" , "printf '%s\\n' run >> " <> show counter , "printf '%s\\n' '% SZS status Theorem for production-route'" ]) permissions <- getPermissions executable setPermissions executable (setOwnerExecutable True permissions) producer <- verifyFixture executable "test/phase3/typed-producer.tex" assertTypedSuccess "exact producer" producer selectedRuns <- runCount counter assertBool "ordinary roots construct the final prelude" (selectedRuns > 0) importer <- verifyFixture executable "test/phase3/typed-importer.tex" assertTypedSuccess "ordinary importer" importer assertBool "every root constructs the final prelude" . (> selectedRuns) =<< runCount counter where verifyFixture executable path = fst <$> ( (checkFileFresh (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) path) >>= expectRight) runCount path = length . StrictText.lines . StrictText.pack <$> readFile path installsNonemptyImplicitPreludeEvidence :: Assertion installsNonemptyImplicitPreludeEvidence = do foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver closure <- expectRight (Identity.validateObjectClosure (Identity.theoryId foundation) []) proposition <- expectRight (Identity.validatePropositionContent closure Core.CFalsum) preludeDriver <- Declaration.runModuleDriver foundation preludeModuleName [] unusedResolver Declaration.FreshValidation do Declaration.commitProofDeclaration (Semantic.proofSyntaxId "nonempty-prelude") do candidate <- Declaration.reserveCandidate (Declaration.candidateSpec proposition Semantic.SearchEligible [Semantic.semanticName "prelude-fact"]) Declaration.authorizeSourceAxiomCandidate candidate preludeResult <- expectRight preludeDriver (preludeSemantic, preludePrefix) <- case preludeResult of Declaration.DriverSucceeded _value semantic prefix _closure -> pure (semantic, prefix) _ -> assertFailure "nonempty prelude fixture did not seal" >> fail "unreachable" preludeFingerprint <- case concatMap Semantic.declarationDeltaFacts (Semantic.semanticInterfaceDeclarations preludeSemantic) of [occurrence] -> pure (Semantic.semanticFactFingerprint occurrence) facts -> assertFailure ("unexpected prelude fact count: " <> show (length facts)) >> fail "unreachable" let preludeSyntax = Module.sealedTypedModuleSyntax (Module.bootstrapPreludeModule bootstrap) nonemptyPrelude <- Temp.withSystemTempDirectory "felix-nonempty-prelude" \directory -> do let path = directory Posix. "store.sqlite" theory = Identity.theoryId foundation parsed = Module.identifiedModuleParsed (Module.bootstrapPreludeInput bootstrap) (_startup, store) <- Store.openStore path theory >>= expectRight artifactKey <- expectRight (Semantic.moduleArtifactKey preludeModuleName (Parse.identifiedParsedModuleId parsed) [] theory) let artifact = Semantic.moduleArtifactResult artifactKey (Syntax.moduleSyntaxAssertedId preludeSyntax) (Semantic.semanticInterfaceAssertedId preludeSemantic) _ <- expectRight =<< Store.writeSealedModule store preludePrefix [preludeSyntax] [preludeSemantic] artifact memo <- Store.newStoreMemo store loaded <- expectRight =<< Store.loadCachedModuleInstallation memo store artifactKey (Syntax.moduleSyntaxAssertedId preludeSyntax) installation <- maybe (assertFailure "nonempty prelude was not installed" >> fail "unreachable") pure loaded sealed <- expectRight (Module.cachedSealedTypedModule foundation [] installation) Store.closeStore store pure sealed root <- getCurrentDirectory mounts <- expectRight =<< prepareSourceMounts [ (sourceMountId "project", root) , (sourceMountId "library", root Posix. "library") , (sourceMountId "debug", root Posix. "debug") ] request <- expectRight (searchedRoot "test/phase3/typed-producer.tex") workspace <- expectRight =<< Parse.parseSourceWorkspaceWithSyntaxInputs mounts request (const [preludeSyntax]) let parsed = Parse.parsedWorkspaceRootModule workspace input <- expectRight (Module.typedModuleInput foundation (Module.fixtureFinalPreludeReadinessFromSealed nonemptyPrelude) unusedResolver Declaration.FreshValidation parsed []) ordinary <- Module.runTypedModule input >>= \case Module.TypedModuleSucceeded sealed -> pure sealed _ -> assertFailure "ordinary module rejected the nonempty prelude" >> fail "unreachable" consumerDigest <- expectRight (hashCanonicalFields "implicit-prelude-consumer" ["consumer"]) consumerPath <- expectRight (safeRelativePath "consumer.tex") let consumerOwner = moduleNameFromParts (sourceNamespaceIdFromDigest consumerDigest) consumerPath consumed <- Declaration.runModuleDriver foundation consumerOwner [Semantic.semanticInterfaceAssertedId (Module.sealedTypedModuleSemantic ordinary)] unusedResolver Declaration.FreshValidation do Declaration.importSealedModuleDriver (Module.sealedTypedModuleEvidence ordinary) Declaration.commitProofDeclaration (Semantic.proofSyntaxId "use-implicit-prelude") do candidate <- Declaration.reserveCandidate (Declaration.candidateSpec proposition Semantic.SearchIneligible []) Declaration.authorizeOmittedCandidate candidate do void (Declaration.useAuthorizedFact preludeFingerprint) Declaration.recordOmittedUse consumedResult <- expectRight consumed case consumedResult of Declaration.DriverSucceeded{} -> pure () _ -> assertFailure "implicit prelude fact was not transitively visible" unusedResolver :: Declaration.VampireResolver unusedResolver = Declaration.vampireResolver \_prepared -> fail "empty bootstrap invoked Vampire" writeAcceptedFixtureVampire :: FilePath -> IO () writeAcceptedFixtureVampire executable = do writeFile executable (unlines [ "#!/bin/sh" , "cat >/dev/null" , "printf '%s\\n' '% SZS status Theorem for typed-fixture'" ]) permissions <- getPermissions executable setPermissions executable (setOwnerExecutable True permissions) withAcceptedFixtureVampire :: String -> (Provers.Vampire -> IO value) -> IO value withAcceptedFixtureVampire label action = Temp.withSystemTempDirectory label \directory -> do let executable = directory Posix. "vampire" writeAcceptedFixtureVampire executable action (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) finalPreludeResolver :: Declaration.VampireResolver finalPreludeResolver = Declaration.vampireResolver \prepared -> (Provers.runPreparedTypedProver (Provers.vampire "vampire" Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) countingAcceptedResolver :: FilePath -> IORef Int -> Declaration.VampireResolver countingAcceptedResolver executable runs = Declaration.vampireResolver \prepared -> do modifyIORef' runs (+ 1) (Provers.runPreparedTypedProver (Provers.vampire executable Provers.defaultTimeLimit Provers.defaultMemoryLimit) prepared) prepareExactInductiveFixture :: FilePath -> IO (Either ExactInductive.ExactInductiveError ExactInductive.PreparedExactInductive) prepareExactInductiveFixture relative = do root <- getCurrentDirectory foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts root workspace <- parseExactWorkspace bootstrap mounts relative parsed <- sole "exact inductive parsed module" (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) let identified = Module.identifiedPhysicalModule parsed owner = Module.identifiedModuleOwner identified parsedModule = Module.identifiedModuleParsed identified (blockIndex, block) <- sole "exact inductive block" [ (index, candidate) | (index, candidate@Raw.BlockInductive{}) <- zip [0..] (Parse.identifiedParsedModuleBlocks parsedModule) ] let entries = [ Parse.parsedSyntaxOccurrenceEntry occurrence | occurrence <- Parse.identifiedParsedModuleSyntaxOccurrences parsedModule , Parse.parsedSyntaxOccurrenceBlockIndex occurrence == blockIndex ] action :: Declaration.ModuleDriver Void (Either ExactInductive.ExactInductiveError ExactInductive.PreparedExactInductive) action = Declaration.runProspectiveLoweringDriver (ExactInductive.prepareExactInductive foundation block entries) result <- Declaration.runModuleDriver foundation owner [] unusedResolver Declaration.FreshValidation action driver <- expectRight result case driver of Declaration.DriverSucceeded prepared _semantic _prefix _closure -> pure prepared Declaration.DriverFailed failure _prefix -> assertFailure ("exact inductive preparation driver failed: " <> show failure) >> fail "unreachable" Declaration.DriverSealFailed failure _prefix -> assertFailure ("exact inductive preparation driver did not seal: " <> show failure) >> fail "unreachable" prepareExactDatatypeFixture :: FilePath -> IO (Either ExactDatatype.ExactDatatypeError ( Foundation.CheckedFoundation , ModuleName , ExactDatatype.PreparedExactDatatype )) prepareExactDatatypeFixture relative = do root <- getCurrentDirectory foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts root workspace <- parseExactWorkspace bootstrap mounts relative parsed <- sole "exact datatype parsed module" (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) let identified = Module.identifiedPhysicalModule parsed owner = Module.identifiedModuleOwner identified parsedModule = Module.identifiedModuleParsed identified block <- sole "exact datatype block" (Parse.identifiedParsedModuleBlocks parsedModule) let occurrences = [ ( Parse.parsedSyntaxOccurrenceLocation occurrence , Parse.parsedSyntaxOccurrenceMarker occurrence , Parse.parsedSyntaxOccurrenceEntry occurrence ) | occurrence <- Parse.identifiedParsedModuleSyntaxOccurrences parsedModule , Parse.parsedSyntaxOccurrenceBlockIndex occurrence == 0 ] action :: Declaration.ModuleDriver Void (Either ExactDatatype.ExactDatatypeError ExactDatatype.PreparedExactDatatype) action = Declaration.runProspectiveLoweringDriver (ExactDatatype.prepareExactDatatype block occurrences) result <- Declaration.runModuleDriver foundation owner [] unusedResolver Declaration.FreshValidation action driver <- expectRight result case driver of Declaration.DriverSucceeded prepared _semantic _prefix _closure -> pure ((\datatype -> (foundation, owner, datatype)) <$> prepared) Declaration.DriverFailed failure _prefix -> assertFailure ("exact datatype preparation driver failed: " <> show failure) >> fail "unreachable" Declaration.DriverSealFailed failure _prefix -> assertFailure ("exact datatype preparation driver did not seal: " <> show failure) >> fail "unreachable" compileExactFixture :: FilePath -> IO ( Foundation.CheckedFoundation , Module.BootstrapPreludeFixture , Parse.ParsedSourceWorkspace , [Module.SealedTypedModule] ) compileExactFixture relative = do root <- getCurrentDirectory foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts root workspace <- parseExactWorkspace bootstrap mounts relative sealed <- compileParsedWorkspace foundation bootstrap workspace pure (foundation, bootstrap, workspace, sealed) compileExactRootAt :: FilePath -> FilePath -> IO (Parse.ParsedSourceWorkspace, Module.SealedTypedModule) compileExactRootAt projectRoot relative = do foundation <- expectRight Foundation.checkedFoundation bootstrap <- expectRight =<< Module.buildBootstrapPreludeFixture foundation unusedResolver mounts <- exactFixtureMounts projectRoot workspace <- parseExactWorkspace bootstrap mounts relative sealed <- compileParsedWorkspace foundation bootstrap workspace rootModule <- sole "exact root module" (reverse sealed) pure (workspace, rootModule) exactFixtureMounts :: FilePath -> IO SourceMounts exactFixtureMounts projectRoot = do repository <- getCurrentDirectory expectRight =<< prepareSourceMounts [ (sourceMountId "project", projectRoot) , (sourceMountId "library", repository Posix. "library") , (sourceMountId "debug", repository Posix. "debug") ] parseExactWorkspace :: Module.BootstrapPreludeFixture -> SourceMounts -> FilePath -> IO Parse.ParsedSourceWorkspace parseExactWorkspace bootstrap mounts relative = parseExactWorkspaceWithPrelude (Module.bootstrapPreludeModule bootstrap) mounts relative parseFinalExactWorkspace :: Module.FinalPreludeSession -> SourceMounts -> FilePath -> IO Parse.ParsedSourceWorkspace parseFinalExactWorkspace prelude mounts relative = parseExactWorkspaceWithPrelude (Module.finalPreludeModule prelude) mounts relative parseExactWorkspaceWithPrelude :: Module.SealedTypedModule -> SourceMounts -> FilePath -> IO Parse.ParsedSourceWorkspace parseExactWorkspaceWithPrelude prelude mounts relative = do request <- expectRight (searchedRoot relative) let preludeSyntax = Module.sealedTypedModuleSyntax prelude expectRight =<< Parse.parseSourceWorkspaceWithSyntaxInputs mounts request (const [preludeSyntax]) compileParsedWorkspace :: Foundation.CheckedFoundation -> Module.BootstrapPreludeFixture -> Parse.ParsedSourceWorkspace -> IO [Module.SealedTypedModule] compileParsedWorkspace foundation bootstrap workspace = compileParsedWorkspaceWithResolver foundation bootstrap unusedResolver workspace compileParsedWorkspaceWithResolver :: Foundation.CheckedFoundation -> Module.BootstrapPreludeFixture -> Declaration.VampireResolver -> Parse.ParsedSourceWorkspace -> IO [Module.SealedTypedModule] compileParsedWorkspaceWithResolver foundation bootstrap resolver workspace = compileParsedWorkspaceWithValidation foundation bootstrap resolver Declaration.FreshValidation workspace compileParsedWorkspaceWithValidation :: Foundation.CheckedFoundation -> Module.BootstrapPreludeFixture -> Declaration.VampireResolver -> Declaration.ValidationRun -> Parse.ParsedSourceWorkspace -> IO [Module.SealedTypedModule] compileParsedWorkspaceWithValidation foundation bootstrap resolver validation workspace = compileParsedWorkspaceWithReadiness foundation (Module.bootstrapPreludeReadiness bootstrap) resolver validation workspace compileFinalParsedWorkspaceWithResolver :: Foundation.CheckedFoundation -> Module.FinalPreludeSession -> Declaration.VampireResolver -> Parse.ParsedSourceWorkspace -> IO [Module.SealedTypedModule] compileFinalParsedWorkspaceWithResolver foundation prelude resolver workspace = compileParsedWorkspaceWithReadiness foundation (Module.finalPreludeReadiness prelude) resolver Declaration.FreshValidation workspace compileParsedWorkspaceWithReadiness :: Foundation.CheckedFoundation -> Module.FinalPreludeReadiness -> Declaration.VampireResolver -> Declaration.ValidationRun -> Parse.ParsedSourceWorkspace -> IO [Module.SealedTypedModule] compileParsedWorkspaceWithReadiness foundation readiness resolver validation workspace = snd <$> foldM compileOne (Map.empty, []) (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) where compileOne (admitted, ordered) parsed = do direct <- traverse (\address -> maybe (assertFailure ("missing exact direct module: " <> show address) >> fail "unreachable") pure (Map.lookup address admitted)) (nubOrd (Parse.parsedImportedAddress <$> Parse.parsedModuleImports parsed)) input <- expectRight (Module.typedModuleInput foundation readiness resolver validation parsed direct) sealed <- Module.runTypedModule input >>= \case Module.TypedModuleSucceeded module' -> pure module' Module.TypedModuleOpenFailed failure -> assertFailure ("exact module did not open: " <> show failure) >> fail "unreachable" Module.TypedModuleFailed failure _prefix -> assertFailure ("exact module did not seal: " <> show failure) >> fail "unreachable" pure ( Map.insert (Parse.parsedModuleAddress parsed) sealed admitted , ordered <> [sealed] ) checkFileFresh :: Provers.Vampire -> FilePath -> IO (Either Verification.VerificationDriverError (Verification.VerificationResult, Provers.SlowAtpReport)) checkFileFresh prover source = do plan <- Store.planStore Store.FreshTemporaryStore >>= expectRight Store.withStoreLease plan \lease -> do opened <- Verification.withVerificationSession lease (\session -> checkFileWithSession session Verification.FreshStoreValidation testSequentialJobs ignoredVerificationRequests prover source) case opened of Left failure -> assertFailure ("test verification session failed: " <> show failure) >> fail "unreachable" Right result -> pure result checkFileWithStore :: Store.Store -> Verification.StoreValidationMode -> Verification.VerificationRequestObserver -> Provers.Vampire -> FilePath -> IO (Either Verification.VerificationDriverError (Verification.VerificationResult, Provers.SlowAtpReport)) checkFileWithStore store mode = checkFileWithStoreAndJobs store mode testSequentialJobs checkFileWithStoreAndJobs :: Store.Store -> Verification.StoreValidationMode -> Provers.EffectiveJobs -> Verification.VerificationRequestObserver -> Provers.Vampire -> FilePath -> IO (Either Verification.VerificationDriverError (Verification.VerificationResult, Provers.SlowAtpReport)) checkFileWithStoreAndJobs store mode jobs observer prover source = do opened <- Verification.withVerificationSessionUsingStore store (\session -> checkFileWithSession session mode jobs observer prover source) case opened of Left failure -> assertFailure ("test verification session failed: " <> show failure) >> fail "unreachable" Right result -> pure result checkResultWithStore :: Store.Store -> Verification.StoreValidationMode -> Verification.VerificationRequestObserver -> Provers.Vampire -> FilePath -> IO (Either Verification.VerificationDriverError Verification.VerificationResult) checkResultWithStore store mode observer prover source = fmap (fmap fst) (checkFileWithStore store mode observer prover source) checkFileWithSession :: Verification.VerificationSession -> Verification.StoreValidationMode -> Provers.EffectiveJobs -> Verification.VerificationRequestObserver -> Provers.Vampire -> FilePath -> IO (Either Verification.VerificationDriverError (Verification.VerificationResult, Provers.SlowAtpReport)) checkFileWithSession session mode jobs observer prover source = Workspace.prepareDefaultSourceGraph source >>= \case Left failure -> pure (Left (Verification.VerificationWorkspaceError failure)) Right graph -> fmap (fmap (\outcome -> ( Verification.checkVerificationResult outcome , Verification.checkSlowAtpReport outcome ))) (Verification.checkWorkspace session Verification.CheckRequest { Verification.checkSourceGraph = graph , Verification.checkStoreValidationMode = mode , Verification.checkEffectiveJobs = jobs , Verification.checkVampire = prover , Verification.checkRequestObserver = observer }) ignoredVerificationRequests :: Verification.VerificationRequestObserver ignoredVerificationRequests = Verification.verificationRequestObserver (\_position _request -> pure ()) testSequentialJobs :: Provers.EffectiveJobs testSequentialJobs = fromMaybe (impossible "one is a positive worker count") (Provers.effectiveJobs 1) assertTypedSuccess :: String -> Verification.VerificationResult -> Assertion assertTypedSuccess label = \case Verification.VerificationCompleted _report _presentation -> pure () Verification.CompletedWithExplicitGaps _report _presentation -> assertFailure (label <> " completed with gaps") Verification.VerificationFailure _report failure -> assertFailure (label <> " failed: " <> show failure) Verification.VerificationCheckingFailure _report failure -> assertFailure (label <> " failed: " <> show failure) sole :: String -> [value] -> IO value sole label = \case [value] -> pure value values -> assertFailure (label <> ": expected one value, found " <> show (length values)) >> fail "unreachable" expectRight :: Show error => Either error value -> IO value expectRight = \case Left err -> assertFailure (show err) >> fail "unreachable" Right value -> pure value expectRightIO :: Show error => IO (Either error value) -> IO value expectRightIO action = action >>= expectRight acquireFinalPreludeSession :: Store.Store -> Foundation.CheckedFoundation -> Declaration.VampireResolver -> IO (Either Module.FinalPreludeReadinessError Module.FinalPreludeSession) acquireFinalPreludeSession store foundation resolver = do memo <- Store.newStoreMemo store Module.acquireFinalPreludeSession memo store foundation resolver