diff options
Diffstat (limited to 'source/Test/Unit/Module.hs')
| -rw-r--r-- | source/Test/Unit/Module.hs | 6672 |
1 files changed, 0 insertions, 6672 deletions
diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs deleted file mode 100644 index 267a9ad..0000000 --- a/source/Test/Unit/Module.hs +++ /dev/null @@ -1,6672 +0,0 @@ -{-# LANGUAGE NoImplicitPrelude #-} - -module Test.Unit.Module (unitTests) where - -import Base -import Api qualified -import Checking.Authority qualified as Authority -import Checking.Backend.Problem qualified as Backend -import Checking.Core qualified as Core -import Checking.Declaration qualified as Declaration -import Checking.Exact qualified as Exact -import Checking.Exact.Datatype qualified as ExactDatatype -import Checking.Exact.Inductive qualified as ExactInductive -import Checking.Exact.Proof qualified as ExactProof -import Checking.FinalPrelude qualified as FinalPrelude -import Checking.Foundation qualified as Foundation -import Checking.Identity qualified as Identity -import Checking.Module qualified as Module -import Checking.Semantic qualified as Semantic -import Checking.Typed.Inductive qualified as TypedInductive -import CommandLine qualified -import Felix.Module -import Felix.Math.Codec -import Felix.Parse qualified as Parse -import Felix.Prelude qualified as Prelude -import Felix.Source -import Felix.Source.Content qualified as Content -import Felix.Store qualified as Store -import Report.Location -import Provers qualified -import Paths_felix qualified as Paths -import Syntax.Abstract qualified as Raw -import Syntax.Internal qualified as Internal -import Syntax.Interface qualified as Syntax -import Syntax.Pragma qualified as Pragma - -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.Monad (foldM, when) -import Data.ByteString qualified as ByteString -import Data.Text qualified as StrictText -import Data.Text.Encoding qualified as Text -import Control.Monad.Logger (runNoLoggingT) -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 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 "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 "confines quantified terms to exact statement subjects" - confinesExactQuantifiedTerms - , testCase "compiles exact ordinary proofs" - compilesExactOrdinaryProofs - , testCase "compiles and reuses proof-local set definitions" - compilesAndReusesProofLocalSetDefinitions - , testCase "compiles and reuses proof-local function graphs" - compilesAndReusesProofLocalFunctionGraphs - , testCase "confines terminal exact contradiction" - confinesTerminalExactContradiction - , testCase "compiles exact separation comprehensions" - compilesExactSeparationComprehensions - , testCase "compiles exact replacement comprehensions" - compilesExactReplacementComprehensions - , 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 "rejects nested exact inductive recursion" - rejectsNestedExactInductiveRecursion - , 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 "rejects nested exact set induction" - rejectsNestedExactSetInduction - , 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") - (Api.renderAuthorityFreeParseError - (Api.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 - 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) - -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) - -assertCleanFactAlias - :: Module.SealedTypedModule - -> Text - -> Assertion -assertCleanFactAlias sealed name = do - delta <- localDeltaByAlias sealed name - alias <- sole - ("semantic alias " <> StrictText.unpack name) - [ candidate - | candidate <- Semantic.declarationDeltaAliases delta - , Semantic.semanticAliasName candidate - == Semantic.semanticName name - ] - fact <- sole - ("semantic fact " <> StrictText.unpack name) - [ candidate - | candidate <- Semantic.declarationDeltaFacts delta - , Semantic.semanticFactFingerprint candidate - == Semantic.semanticAliasTarget alias - ] - assertEqual - ("clean authority for " <> StrictText.unpack name) - Authority.cleanAuthoritySafety - (Authority.factAuthoritySafety - (Semantic.semanticFactAuthority fact)) - -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, _measurements) <- - expectRight - =<< Parse.parseSourceWorkspaceMeasuredWithSyntaxInputs - 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 <- - runNoLoggingT - (Api.verifyMeasured - (Provers.vampire - "vampire" - Provers.defaultTimeLimit - Provers.defaultMemoryLimit) - "test/phase3/typed-unsupported.tex") - case result of - Right - ( Api.VerificationCheckingFailure _report - (failure@(Api.VerificationTypedModuleError - source - (Module.TypedActionFailed - (Module.TypedExactCompileFailed - (Exact.ExactUnsupportedDeclarationBody location))) - prefix)) - , _measurements - ) -> do - assertEqual "failed source" - "test/phase3/typed-unsupported.tex" - (safeRelativePathFilePath - (resolvedSourceRelativePath source)) - assertEqual "unsupported source location line" - 1 - (locLine location) - assertEqual "failure retains the initial module prefix" - 0 - (length - (Declaration.pendingModulePrefixBatches prefix)) - let diagnostic = - CommandLine.verificationDriverFailureMessage failure - assertBool "diagnostic retains resolved source" - ("project:test/phase3/typed-unsupported.tex" - `StrictText.isInfixOf` diagnostic) - assertBool "diagnostic retains best location" - ("typed-unsupported.tex 1:1" - `StrictText.isInfixOf` diagnostic) - assertBool "diagnostic explains the typed failure" - ("not yet supported by exact elaboration" - `StrictText.isInfixOf` diagnostic) - Left err -> - assertFailure ("unexpected verification driver error: " <> show err) - Right{} -> - assertFailure "unsupported typed source was admitted" - -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) - - 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 - ] - ]) - runNoLoggingT - (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 -> - runNoLoggingT - (Api.verifyMeasured - prover - "test/phase5/exact-relation-expression-missing-pair.tex") - case missingPair of - Right - ( Api.VerificationCheckingFailure _report - (Api.VerificationTypedModuleError - _source - (Module.TypedActionFailed - (Module.TypedExactProofFailed - (ExactProof.ExactProofElaborationFailed - (Exact.ExactGlobalNotVisible location key)))) - prefix) - , _measurements - ) -> 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 - (runNoLoggingT . 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 -> - runNoLoggingT - (Api.verifyMeasured - prover - "test/phase5/exact-application-missing.tex") - case missing of - Right - ( Api.VerificationCheckingFailure _report - (Api.VerificationTypedModuleError - _source - (Module.TypedActionFailed - (Module.TypedExactProofFailed - (ExactProof.ExactProofElaborationFailed - (Exact.ExactGlobalNotVisible location key)))) - prefix) - , _measurements - ) -> 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 - (runNoLoggingT . 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 - - negative <- - withAcceptedFixtureVampire "felix-exact-quantified-subject-nested" - \prover -> - runNoLoggingT - (Api.verifyMeasured - prover - "test/phase5/exact-quantified-subject-nested.tex") - case negative of - Right - ( Api.VerificationCheckingFailure _report - (Api.VerificationTypedModuleError - _source - (Module.TypedActionFailed - (Module.TypedExactProofFailed - (ExactProof.ExactProofElaborationFailed - (Exact.ExactQuantifiedTermRequiresStatementSubject - location)))) - prefix) - , _measurements - ) -> do - assertEqual "nested quantified term line" 8 (locLine location) - assertEqual "earlier exact definition remains committed" - 1 - (length (Declaration.pendingModulePrefixBatches prefix)) - Left failure -> - assertFailure - ("unexpected nested quantified-term failure: " - <> show failure) - Right{} -> - assertFailure "nested quantified exact term was admitted" -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 - ] - ) - ]) - runNoLoggingT - (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 - -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 - modifyIORef' observations - (<> [ ( Backend.typedProblemRoute problem - , Backend.typedProblemAuxiliaryTag - <$> Vector.toList - (Backend.typedProblemAuxiliaries problem) - ) - ]) - runNoLoggingT - (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 - assertEqual - "separation proof uses its checked characteristic on TH0" - [( Backend.RouteTh0 - , [Foundation.SeparationCharacteristic] - )] - =<< readIORef observations - - 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 - , Vector.length premises - , fmap localDefinitionShape definition - ) - ]) - runNoLoggingT - (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 "local definitions remain on the FOF route" - [ (Backend.RouteFof, 2, Just expectedLocalDefinitionShape) - , (Backend.RouteFof, 2, 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) - runNoLoggingT - (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 executable = directory Posix.</> "vampire" - writeFile executable - (unlines - [ "#!/bin/sh" - , "cat >/dev/null" - , "printf '%s\\n' '% SZS status ContradictoryAxioms for exact-contradiction'" - ]) - permissions <- getPermissions executable - setPermissions executable - (setOwnerExecutable True permissions) - foundation <- expectRight Foundation.checkedFoundation - bootstrap <- - expectRight - =<< Module.buildBootstrapPreludeFixture - foundation unusedResolver - mounts <- exactFixtureMounts =<< getCurrentDirectory - workspace <- parseExactWorkspace bootstrap mounts - "test/phase5/exact-contradiction.tex" - runs <- newIORef (0 :: Int) - modules <- - compileParsedWorkspaceWithResolver - foundation - bootstrap - (countingAcceptedResolver executable runs) - workspace - accepted <- sole "terminal contradiction module" modules - assertEqual "one indirect contradiction obligation" - 1 =<< readIORef runs - assertCleanFactAlias accepted "phase5_contradiction" - - invalidWorkspace <- parseExactWorkspace bootstrap mounts - "test/phase5/exact-contradiction-goal.tex" - invalidParsed <- - sole "invalid contradiction module" - (toList - (Parse.parsedWorkspaceImportedBeforeImporter - invalidWorkspace)) - invalidInput <- expectRight - (Module.typedModuleInput - foundation - (Module.bootstrapPreludeReadiness bootstrap) - unusedResolver - Declaration.FreshValidation - invalidParsed - []) - Module.runTypedModule invalidInput >>= \case - Module.TypedModuleFailed - (Module.TypedActionFailed - (Module.TypedExactProofFailed - (ExactProof.ExactProofContradictionGoalMismatch - location))) - prefix -> do - assertEqual "invalid contradiction line" - 6 (locLine location) - assertBool "invalid contradiction publishes no declaration" - (null - (Declaration.pendingModulePrefixBatches prefix)) - _result -> - assertFailure "unexpected invalid contradiction result" - -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) - ) - ]) - runNoLoggingT - (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 - content -> - assertFailure - ("unexpected replacement object " <> show content) - assertEqual "replacement definition fact count" - 1 - (length - (Semantic.declarationDeltaFacts - (Declaration.committedBatchDelta definitionBatch))) - assertEqual "replacement definition proposition count" - 1 - (length - (Declaration.committedBatchPropositions definitionBatch)) - assertEqual "replacement definition proof validations" - [] - (Declaration.committedBatchProofValidations definitionBatch) - - 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)) - -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) - ) - ]) - runNoLoggingT - (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 - 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) - where - apply1 intrinsic argument = - Core.CApp (Core.CIntrinsic intrinsic) argument - 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) - (apply1 Core.FamilyUnion - (Core.CIntrinsic Core.Empty))) - (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) - (apply1 Core.FamilyUnion - (Core.CIntrinsic Core.Empty))) - (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 - apply1 intrinsic argument = - Core.CApp (Core.CIntrinsic intrinsic) argument - - 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" - -rejectsNestedExactInductiveRecursion :: Assertion -rejectsNestedExactInductiveRecursion = do - result <- - prepareExactInductiveFixture - "test/phase5/exact-inductive-nested.tex" - case result of - Left (ExactInductive.ExactInductiveNestedRecursion location) -> - assertEqual "nested recursive occurrence line" - 6 - (locLine location) - Left failure -> - assertFailure - ("unexpected exact inductive failure: " <> show failure) - Right{} -> - assertFailure "nested inductive recursion was accepted" - -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 - - mounts <- exactFixtureMounts =<< getCurrentDirectory - nestedWorkspace <- - parseExactWorkspace bootstrap mounts - "test/phase5/exact-inductive-nested.tex" - nestedParsed <- - sole "nested exact inductive 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.TypedExactInductiveFailed - (ExactInductive.ExactInductiveNestedRecursion - location))) - prefix -> do - assertEqual "nested failure line" 6 (locLine location) - assertBool "nested declaration publishes no prefix" - (null (Declaration.pendingModulePrefixBatches prefix)) - _result -> - assertFailure "unexpected nested inductive result" - -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) - assertEqual (label <> " definition fact count") - 1 - (length - (Semantic.declarationDeltaFacts - (Declaration.committedBatchDelta definitionBatch))) - assertEqual (label <> " definition proposition count") - 1 - (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) - definitionCertificate <- sole - (label <> " definition certificate") - (Semantic.declarationValidationRecordCertificates - definitionValidation) - case Authority.validationDirectAuthorization - definitionCertificate of - Authority.CheckedKernelConstruction - (Authority.CheckedDefinitionEquation _target) -> - pure () - authorization -> - assertFailure - (label <> ": unexpected definition authority " - <> show authorization) - - 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 - freshRuns <- newIORef (0 :: Int) - freshModules <- - compileParsedWorkspaceWithValidation - foundation - bootstrap - (countingAcceptedResolver executable freshRuns) - Declaration.FreshValidation - workspace - assertEqual "fresh separation proof runs Vampire once" - 1 - =<< readIORef freshRuns - fresh <- sole "fresh exact separation module" freshModules - assertExactSeparationModule "fresh cached" 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) - 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 - 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) - -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 - ] - ]) - runNoLoggingT - (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) - runNoLoggingT - (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) - runNoLoggingT - (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 - runNoLoggingT - (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 = Api.verificationRequestObserver \_ordinal _request -> - pure () - prover = - Provers.vampire - executable - Provers.defaultTimeLimit - Provers.defaultMemoryLimit - verify mode source = - runNoLoggingT - (Api.verifyWithObserverAndStoreMode - store mode observer prover source) - >>= expectRight - producer <- - verify Api.FreshStoreValidation - "test/phase5/exact-producer.tex" - importer <- - verify Api.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 = - Api.verificationRequestObserver - (\_position _request -> pure ()) - select amount = - Provers.selectEffectiveJobs - (Provers.effectiveJobs amount) - (fail "explicit jobs unexpectedly detected processors") - reportEntry escape = - ( Api.reportedEscapeKind escape - , locFile (Api.reportedEscapeLocation escape) - , locLine (Api.reportedEscapeLocation escape) - ) - inspect label expectedPositions - (result, measurements, positions) = do - case result of - Api.VerificationFailure report failed -> do - assertEqual (label <> " selected earlier failure") - "test/phase7/concurrent-earlier.tex" - (locFile (Api.failedVerificationLocation failed)) - assertEqual (label <> " admitted source prefix") - [ ( Api.ReportedSourceAxiom - , "test/phase7/concurrent-earlier.tex" - , 1 - ) - ] - (reportEntry - <$> Api.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 - ]) - pure measurements - 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 - (runNoLoggingT - (Api.verifyMeasuredWithObserverAndStoreMode - openStore - Api.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 = - Api.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, measurements) <- - runNoLoggingT - (Api.verifyMeasuredWithObserverAndStoreModeAndJobs - openStore - Api.WarmStoreValidation - jobs - observer - prover - source) - >>= expectRight - positions <- readIORef positionsRef - pure (result, measurements, positions) - parallel <- - runCase "parallel" 2 - >>= inspect "parallel" [(1, 1), (2, 1)] - sequential <- - runCase "sequential" 1 - >>= inspect "sequential" [(1, 1)] - assertEqual "parallel module checker bound" - 2 - (Api.verificationMaximumLiveModuleCheckers parallel) - assertEqual "parallel Vampire bound" - 2 - (Api.verificationMaximumLiveVampireProcesses parallel) - assertEqual "sequential module checker reference" - 1 - (Api.verificationMaximumLiveModuleCheckers sequential) - assertEqual "sequential Vampire reference" - 1 - (Api.verificationMaximumLiveVampireProcesses sequential) - -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 = - runNoLoggingT - (Api.verifyMeasuredWithObserverAndStoreModeAndJobs - openStore - Api.WarmStoreValidation - jobs - observer - vampireCommand - source) - >>= expectRight - inspectFailure label positions (result, measurements) = do - case result of - Api.VerificationFailure report failed -> do - assertEqual (label <> " selects first consequence") - (source, 12) - ( locFile (Api.failedVerificationLocation failed) - , locLine (Api.failedVerificationLocation failed) - ) - assertEqual (label <> " retains preceding prefix") - [(Api.ReportedSourceAxiom, source, 1)] - [ ( Api.reportedEscapeKind escape - , locFile (Api.reportedEscapeLocation escape) - , locLine (Api.reportedEscapeLocation escape) - ) - | escape <- Api.verificationDirectEscapes report - ] - other -> - assertFailure - (label <> " did not reject its structure batch: " - <> show other) - assertEqual (label <> " assigns consecutive positions") - [(1, 1), (1, 2)] - (sort positions) - assertEqual (label <> " observes one two-member batch") - (1, 2, 2) - ( Api.verificationObligationBatchCount measurements - , Api.verificationPreparedObligationCount measurements - , Api.verificationMaximumObligationBatchSize measurements - ) - pure measurements - writeAcceptedFixtureVampire executable - (_startup, store) <- - Store.openStore storePath (Identity.theoryId foundation) - >>= expectRight - bracket (pure store) Store.closeStore \openStore -> do - let ignored = - Api.verificationRequestObserver - (\_position _request -> pure ()) - -- Seed only the confined prelude so this fixture observes exactly - -- the ordinary structure module's ready batch. - void - (runNoLoggingT - (Api.verifyMeasuredWithObserverAndStoreMode - openStore - Api.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 = - Api.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 - parallelMeasurements <- - inspectFailure "parallel" - positions parallelResult - assertEqual "parallel obligations overlap" - 2 - (Api.verificationMaximumLiveVampireProcesses - parallelMeasurements) - - sequentialJobs <- select 1 - sequentialPositions <- newIORef [] - let sequentialCompleted = root Posix.</> "sequential-completed" - writeRejectingVampire executable sequentialCompleted - let sequentialObserver = - Api.verificationRequestObserver \position _request -> - atomicModifyIORef' sequentialPositions - (\positions -> - ( ( Provers.workPositionModuleOrdinal position - , Provers.workPositionLocalRequestOrdinal - position - ) : positions - , () - )) - sequentialResult <- - run openStore sequentialJobs sequentialObserver - (prover executable) - sequentialObserved <- readIORef sequentialPositions - sequentialMeasurements <- - inspectFailure "sequential" - sequentialObserved sequentialResult - assertEqual "sequential batch is the semantic reference" - 1 - (Api.verificationMaximumLiveVampireProcesses - sequentialMeasurements) - - -- 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 = - Api.verificationRequestObserver \position _request -> - modifyIORef' acceptedPositions - (position :) - (accepted, acceptedMeasurements) <- - run openStore parallelJobs acceptedObserver - (prover executable) - case accepted of - Api.VerificationCompleted report _presentation -> - assertEqual "successful retry retains only source axiom" - [Api.ReportedSourceAxiom] - (Api.reportedEscapeKind - <$> Api.verificationDirectEscapes report) - other -> - assertFailure - ("successful structure retry failed: " <> show other) - acceptedObserved <- readIORef acceptedPositions - assertEqual "successful retry executes the complete batch" - 2 - (length acceptedObserved) - assertEqual "failed declaration published no root" - (1, 1) - ( Api.verificationModuleRootHitCount acceptedMeasurements - , Api.verificationModuleRootMissCount acceptedMeasurements - ) - let forbiddenObserver = - Api.verificationRequestObserver \position _request -> - assertFailure - ("warm structure batch invoked Vampire at " - <> show position) - (warm, warmMeasurements) <- - run openStore parallelJobs forbiddenObserver - (prover unavailable) - case warm of - Api.VerificationCompleted{} -> pure () - other -> - assertFailure - ("warm structure batch did not install: " <> show other) - assertEqual "warm module hit executes no batch" - (2, 0, 0) - ( Api.verificationModuleRootHitCount warmMeasurements - , Api.verificationModuleRootMissCount warmMeasurements - , Api.verificationVampireRunCount warmMeasurements - ) - 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 = - Api.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 - (runNoLoggingT - (Api.verifyMeasuredWithObserverAndStoreMode - openStore - Api.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 = - Api.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 - (runNoLoggingT - (Api.verifyMeasuredWithObserverAndStoreModeAndJobs - openStore - Api.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, measurements) <- wait checking - case result of - Api.VerificationCompleted report _presentation -> - assertEqual "only the preceding axiom is reported" - [Api.ReportedSourceAxiom] - (Api.reportedEscapeKind - <$> Api.verificationDirectEscapes report) - other -> - assertFailure - ("dependent proof module did not seal: " - <> show other) - assertEqual "dependent proof obligations overlap" - 2 - (Api.verificationMaximumLiveVampireProcesses - measurements) - positions <- readIORef positionsRef - assertEqual "dependent requests retain source positions" - [(1, 1), (1, 2)] - (sort positions) - - let forbiddenObserver = - Api.verificationRequestObserver \position _request -> - assertFailure - ("warm dependent proof invoked Vampire at " - <> show position) - (warm, warmMeasurements) <- - runNoLoggingT - (Api.verifyMeasuredWithObserverAndStoreModeAndJobs - openStore - Api.WarmStoreValidation - jobs - forbiddenObserver - (prover unavailable) - source) - >>= expectRight - case warm of - Api.VerificationCompleted{} -> pure () - other -> - assertFailure - ("warm dependent proof did not install: " <> show other) - assertEqual "warm plan executes no live request" - 0 - (Api.verificationVampireRunCount warmMeasurements) - 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 = - Api.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 - (runNoLoggingT - (Api.verifyMeasuredWithObserverAndStoreMode - openStore - Api.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 = - Api.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 = - runNoLoggingT - (Api.verifyMeasuredWithObserverAndStoreModeAndJobs - openStore - Api.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, coldMeasurements) <- wait verification - case coldResult of - Api.VerificationCompleted{} -> pure () - other -> - assertFailure - ("cold diamond did not complete: " <> show other) - assertEqual "cold diamond module misses plus prelude hit" - (1, 4) - ( Api.verificationModuleRootHitCount coldMeasurements - , Api.verificationModuleRootMissCount coldMeasurements - ) - let forbiddenObserver = - Api.verificationRequestObserver - (\position _request -> - assertFailure - ("warm diamond invoked Vampire at " - <> show position)) - (warmResult, warmMeasurements) <- - verify (prover unavailable) forbiddenObserver - case warmResult of - Api.VerificationCompleted{} -> pure () - other -> - assertFailure - ("warm diamond did not install: " <> show other) - assertEqual "warm diamond installs each distinct root" - (5, 0) - ( Api.verificationModuleRootHitCount warmMeasurements - , Api.verificationModuleRootMissCount warmMeasurements - ) - assertEqual "warm diamond runs no prover" - 0 - (Api.verificationVampireRunCount warmMeasurements) - -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 = - Api.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 = - runNoLoggingT - (Api.verifyMeasuredWithObserverAndStoreMode - openStore - mode - observer - (prover vampirePath) - source) - >>= expectRight - reportEntries = - fmap - (\escape -> - ( Api.reportedEscapeKind escape - , locFile (Api.reportedEscapeLocation escape) - , locLine (Api.reportedEscapeLocation escape) - )) - . Api.verificationDirectEscapes - expectedConsumer = - [ ( Api.ReportedSourceAxiom - , "test/phase5/exact-escape-producer.tex" - , 1 - ) - , ( Api.ReportedOmitted - , "test/phase5/exact-escape-producer.tex" - , 9 - ) - , ( Api.ReportedOmitted - , "test/phase5/exact-escape-consumer.tex" - , 35 - ) - ] - (freshResult, freshMeasurements) <- - verify - Api.FreshStoreValidation - executable - "test/phase5/exact-escape-consumer.tex" - freshReport <- case freshResult of - Api.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) - assertEqual "cold acquisition includes prelude and two modules" - (0, 3) - ( Api.verificationModuleRootHitCount freshMeasurements - , Api.verificationModuleRootMissCount freshMeasurements - ) - - (warmResult, warmMeasurements) <- - verify - Api.WarmStoreValidation - unavailable - "test/phase5/exact-escape-consumer.tex" - warmReport <- case warmResult of - Api.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 - assertEqual "warm acquisition includes prelude and two modules" - (3, 0) - ( Api.verificationModuleRootHitCount warmMeasurements - , Api.verificationModuleRootMissCount warmMeasurements - ) - assertEqual "warm root hit invokes no Vampire process" - 0 - (Api.verificationVampireRunCount warmMeasurements) - - void - (verify - Api.FreshStoreValidation - executable - "test/phase5/exact-source-axiom.tex") - (failedResult, failedMeasurements) <- - verify - Api.WarmStoreValidation - unavailable - "test/phase6/admitted-prefix-failure.tex" - failedReport <- case failedResult of - Api.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 - <> [ ( Api.ReportedOmitted - , "test/phase6/admitted-prefix-failure.tex" - , 7 - ) - ]) - (reportEntries failedReport) - assertEqual "failed root is not counted as acquired" - (2, 0) - ( Api.verificationModuleRootHitCount failedMeasurements - , Api.verificationModuleRootMissCount failedMeasurements - ) - assertEqual "cached prefix failure invokes no Vampire process" - 0 - (Api.verificationVampireRunCount failedMeasurements) - -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 = - Api.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 = - runNoLoggingT - (Api.verifyMeasuredWithObserverAndStoreMode - openStore - Api.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, _measurements) <- - verify "test/phase5/exact-runtime-failure.tex" - case result of - Api.VerificationFailure report failed -> do - assertEqual "typed failure has no direct escapes" - [] - (Api.verificationDirectEscapes report) - assertEqual "typed failure retains source location" - "test/phase5/exact-runtime-failure.tex" - (locFile - (Api.failedVerificationLocation failed)) - classify - (Api.failedVerificationReason failed) - (CommandLine.verificationCommandOutcome result) - 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, _preludeMeasurements) <- - 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 - Api.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 - Api.IndeterminateFailure{} -> pure () - other -> assertFailure ("expected indeterminate result: " <> show other) - case outcome of - CommandLine.ProverFailed - _report _location CommandLine.ProverIndeterminate{} -> - 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 - Api.ProtocolFailure{} -> pure () - other -> assertFailure ("expected protocol failure: " <> show other) - case outcome of - CommandLine.ProverFailed - _report _location CommandLine.ProverProtocolFailure{} -> - 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 - Api.TransportFailure{} -> pure () - other -> assertFailure ("expected transport failure: " <> show other) - case outcome of - CommandLine.ProverFailed - _report _location CommandLine.ProverTransportFailure{} -> - pure () - other -> assertFailure ("expected prover failure: " <> show other) - -retainsExactPrefixBeforeFailure :: Assertion -retainsExactPrefixBeforeFailure = do - result <- - withAcceptedFixtureVampire "felix-exact-failure" \prover -> - runNoLoggingT - (Api.verifyMeasured - prover - "test/phase5/exact-failure.tex") - case result of - Right - ( Api.VerificationCheckingFailure _report - (Api.VerificationTypedModuleError - source - (Module.TypedActionFailed - (Module.TypedExactCompileFailed - (Exact.ExactUnsupportedDeclarationBody location))) - prefix) - , _measurements - ) -> do - assertEqual "failed exact source" - "test/phase5/exact-failure.tex" - (safeRelativePathFilePath - (resolvedSourceRelativePath source)) - assertEqual "unsupported declaration line" 5 (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 -> - runNoLoggingT - (Api.verifyMeasured - prover - "test/phase5/exact-proof-failure.tex") - case proofFailure of - Right - ( Api.VerificationCheckingFailure _report - (Api.VerificationTypedModuleError - _source - (Module.TypedActionFailed - (Module.TypedExactProofFailed - (ExactProof.ExactProofGoalStatementMismatch - location))) - prefix) - , _measurements - ) -> 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 -> - runNoLoggingT - (Api.verifyMeasured - prover - "test/phase5/unmatched-proof.tex") - case unmatched of - Right - ( Api.VerificationCheckingFailure _report - (Api.VerificationTypedModuleError - _source - (Module.TypedActionFailed - (Module.TypedUnmatchedProof location)) - prefix) - , _measurements - ) -> 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 - runNoLoggingT - (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" - -rejectsNestedExactSetInduction :: Assertion -rejectsNestedExactSetInduction = do - result <- - withAcceptedFixtureVampire "felix-nested-set-induction" \prover -> - runNoLoggingT - (Api.verifyMeasured - prover - "test/phase5/exact-induction-nested.tex") - case result of - Right - ( Api.VerificationCheckingFailure _report - (Api.VerificationTypedModuleError - _source - (Module.TypedActionFailed - (Module.TypedExactProofFailed - (ExactProof.ExactProofSetInductionNotOutermost - location))) - prefix) - , _measurements - ) -> do - assertEqual "nested induction line" 7 (locLine location) - assertBool "failed proof publishes no theorem" - (null (Declaration.pendingModulePrefixBatches prefix)) - Left err -> - assertFailure - ("unexpected nested-induction failure: " <> show err) - Right{} -> - assertFailure "nested exact set induction was admitted" - -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 - <$> (runNoLoggingT - (Api.verifyMeasured - (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 <- - fst - <$> (expectRight - =<< Parse.parseSourceWorkspaceMeasuredWithSyntaxInputs - 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 -> - runNoLoggingT - (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) - runNoLoggingT - (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 - block <- - sole "exact inductive block" - (Parse.identifiedParsedModuleBlocks parsedModule) - let entries = - [ Parse.parsedSyntaxOccurrenceEntry occurrence - | occurrence <- - Parse.identifiedParsedModuleSyntaxOccurrences parsedModule - , Parse.parsedSyntaxOccurrenceBlockIndex occurrence == 0 - ] - 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 - fst - <$> (expectRight - =<< Parse.parseSourceWorkspaceMeasuredWithSyntaxInputs - 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] - ) - -assertTypedSuccess :: String -> Api.VerificationResult -> Assertion -assertTypedSuccess label = \case - Api.VerificationCompleted _report _presentation -> - pure () - Api.CompletedWithExplicitGaps _report _presentation -> - assertFailure (label <> " completed with gaps") - Api.VerificationFailure _report failure -> - assertFailure (label <> " failed: " <> show failure) - Api.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 |