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