diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2026-08-06 17:54:00 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2026-08-06 17:54:00 +0200 |
| commit | 82328890108bae64b372b8d58620ebc62699de76 (patch) | |
| tree | 575404c6b425c19259c0ded296f1c8ffb7ff0e2b /source/Felix/Test/Unit/Module.hs | |
| parent | 1a25421c2a168d420581358c8733fcd8f36f379b (diff) | |
Diffstat (limited to 'source/Felix/Test/Unit/Module.hs')
| -rw-r--r-- | source/Felix/Test/Unit/Module.hs | 9759 |
1 files changed, 9759 insertions, 0 deletions
diff --git a/source/Felix/Test/Unit/Module.hs b/source/Felix/Test/Unit/Module.hs new file mode 100644 index 0000000..44f0ccb --- /dev/null +++ b/source/Felix/Test/Unit/Module.hs @@ -0,0 +1,9759 @@ +{-# 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" + "<felix-prelude>: syntax pragma location is out of range at 7:3" + (Prelude.renderPreludeParseError parseFailure) + assertEqual "authority-free API presentation" + ("packaged final prelude parsing failed: " + <> "<felix-prelude>: 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 |
