summaryrefslogtreecommitdiff
path: root/source/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/Test/Unit/Module.hs
parent1a25421c2a168d420581358c8733fcd8f36f379b (diff)
Migrate to `Felix` namespaceHEADhotg
Diffstat (limited to 'source/Test/Unit/Module.hs')
-rw-r--r--source/Test/Unit/Module.hs9759
1 files changed, 0 insertions, 9759 deletions
diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
deleted file mode 100644
index 13fe90d..0000000
--- a/source/Test/Unit/Module.hs
+++ /dev/null
@@ -1,9759 +0,0 @@
-{-# LANGUAGE NoImplicitPrelude #-}
-
-module Test.Unit.Module (unitTests) where
-
-import Base
-import Checking.Authority qualified as Authority
-import Checking.Backend.Problem qualified as Backend
-import Checking.Core qualified as Core
-import Checking.Declaration qualified as Declaration
-import Checking.Exact qualified as Exact
-import Checking.Exact.Datatype qualified as ExactDatatype
-import Checking.Exact.Inductive qualified as ExactInductive
-import Checking.Exact.Proof qualified as ExactProof
-import Checking.FinalPrelude qualified as FinalPrelude
-import Checking.Foundation qualified as Foundation
-import Checking.Identity qualified as Identity
-import Checking.Module qualified as Module
-import Checking.Semantic qualified as Semantic
-import Checking.Typed.Inductive qualified as TypedInductive
-import Felix.CommandLine qualified as CommandLine
-import Felix.Module
-import Felix.Math.Codec
-import Felix.Parse qualified as Parse
-import Felix.Prelude qualified as Prelude
-import Felix.Source
-import Felix.Source.Content qualified as Content
-import Felix.Store qualified as Store
-import Felix.Verification qualified as Verification
-import Felix.Workspace qualified as Workspace
-import Report.Location
-import Felix.Provers qualified as Provers
-import Paths_felix qualified as Paths
-import Syntax.Abstract qualified as Raw
-import Syntax.Internal qualified as Internal
-import Syntax.Interface qualified as Syntax
-import Syntax.Lexicon qualified as Lexicon
-import Syntax.Pragma qualified as Pragma
-
-import Control.Concurrent (threadDelay)
-import Control.Concurrent.STM
- ( atomically
- , check
- , newEmptyTMVarIO
- , newTQueueIO
- , newTVarIO
- , putTMVar
- , readTQueue
- , readTVar
- , takeTMVar
- , tryReadTMVar
- , tryReadTQueue
- , writeTQueue
- , writeTVar
- )
-import Control.Exception (bracket)
-import Control.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
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 19:07:54 +0000