diff options
| -rw-r--r-- | source/Checking/Core.hs | 47 | ||||
| -rw-r--r-- | source/Checking/Exact.hs | 153 | ||||
| -rw-r--r-- | source/Checking/Exact/Proof.hs | 272 | ||||
| -rw-r--r-- | source/Felix/Cache/Codec.hs | 2 | ||||
| -rw-r--r-- | source/Test/Unit/Module.hs | 360 | ||||
| -rw-r--r-- | test/phase5/exact-proof-parity-invalid-assume.tex | 8 | ||||
| -rw-r--r-- | test/phase5/exact-proof-parity-invalid-fix-shape.tex | 8 | ||||
| -rw-r--r-- | test/phase5/exact-proof-parity-invalid-fix.tex | 8 | ||||
| -rw-r--r-- | test/phase5/exact-proof-parity.tex | 107 |
9 files changed, 877 insertions, 88 deletions
diff --git a/source/Checking/Core.hs b/source/Checking/Core.hs index 4b7478f..f8466af 100644 --- a/source/Checking/Core.hs +++ b/source/Checking/Core.hs @@ -58,6 +58,7 @@ module Checking.Core , closeScopedExists , openScopedForall , openScopedImplication + , openScopedAssumption , closeScopedCore , instantiateCanonical , mapCanonicalGlobals @@ -1058,6 +1059,52 @@ openScopedImplication openScopedImplication _scoped = Nothing +-- | Open a checked proof assumption against the current goal. Besides a +-- direct implication antecedent, the source language historically permits +-- either immediate side of one binary conjunction antecedent to be assumed +-- first. The other side remains the next implication antecedent. This is a +-- deliberately shallow structural rule: it neither flattens conjunctions nor +-- treats disjunction as an eliminable assumption. +openScopedAssumption + :: Eq global + => ScopedCheckedCore global + -> ScopedCheckedCore global + -> Maybe + ( ScopedCheckedCore global + , ScopedCheckedCore global + ) +openScopedAssumption supplied goal = do + (antecedent, conclusion) <- openScopedImplication goal + if supplied == antecedent + then pure (antecedent, conclusion) + else do + (left, right) <- splitScopedConjunction antecedent + if supplied == left + then do + remaining <- implyScopedCore right conclusion + pure (left, remaining) + else if supplied == right + then do + remaining <- implyScopedCore left conclusion + pure (right, remaining) + else Nothing + +splitScopedConjunction + :: ScopedCheckedCore global + -> Maybe + ( ScopedCheckedCore global + , ScopedCheckedCore global + ) +splitScopedConjunction + (ScopedCheckedCore context TyProp + (CImp (CImp left (CImp right CFalsum)) CFalsum)) = + Just + ( ScopedCheckedCore context TyProp left + , ScopedCheckedCore context TyProp right + ) +splitScopedConjunction _scoped = + Nothing + closeScopedCore :: ScopedCheckedCore global -> Maybe (FrozenCheckedCore global) diff --git a/source/Checking/Exact.hs b/source/Checking/Exact.hs index c4b90c7..1788224 100644 --- a/source/Checking/Exact.hs +++ b/source/Checking/Exact.hs @@ -9,11 +9,15 @@ module Checking.Exact , ExactBinderContext , emptyExactBinderContext , extendExactBinderContext + , extendExactAnonymousBinderContext , exactBinderContextSupport , exactBinderContextIndex , PreparedExactProposition , preparedExactPropositionCore , prepareExactProposition + , prepareExactSymbolicBoundConstraints + , prepareExactSymbolicWitnessConstraints + , prepareExactNounWitnessConstraints , PreparedExactSetExpression , preparedExactSetExpressionCore , prepareExactSetExpression @@ -95,7 +99,7 @@ exactLocalIdValue (ExactLocalId value) = value data ExactBinder = ExactBinder !ExactLocalId - !Raw.VarSymbol + !(Maybe Raw.VarSymbol) !CoreType !(Maybe ExactStructureAnnotation) @@ -123,14 +127,33 @@ extendExactBinderContext additions (ExactBinderContext initial) = | any (sameIdentity identity) binders = Left (ExactDuplicateLocalIdentity (locate variable) identity) | otherwise = - Right (ExactBinder identity variable TySet Nothing : binders) + Right (ExactBinder identity (Just variable) TySet Nothing : binders) sameVariable variable (ExactBinder _identity existing _coreType _structure) = - existing == variable + existing == Just variable sameIdentity identity (ExactBinder existing _variable _coreType _structure) = existing == identity +-- | Add one proof-owned binder which deliberately has no source-resolvable +-- spelling. This is used for a nameless singular witness; it participates in +-- checked support and de Bruijn weakening but cannot shadow or be looked up by +-- a later source variable. +extendExactAnonymousBinderContext + :: ExactLocalId + -> ExactBinderContext + -> Either ExactCompileError ExactBinderContext +extendExactAnonymousBinderContext identity (ExactBinderContext binders) + | any sameIdentity binders = + Left (ExactDuplicateLocalIdentity Nowhere identity) + | otherwise = + Right + (ExactBinderContext + (ExactBinder identity Nothing TySet Nothing : binders)) + where + sameIdentity (ExactBinder existing _variable _coreType _structure) = + existing == identity + exactBinderContextSupport :: ExactBinderContext -> Vector (ExactLocalId, CoreType) @@ -150,7 +173,7 @@ exactBinderContextIndex variable (ExactBinderContext binders) = go _index [] = Nothing go index (ExactBinder _identity candidate _coreType _structure : rest) - | candidate == variable = Just index + | candidate == Just variable = Just index | otherwise = go (index + 1) rest newtype PreparedExactProposition = PreparedExactProposition @@ -547,16 +570,88 @@ prepareExactProposition -> Declaration.LoweringDriver (Either ExactCompileError PreparedExactProposition) prepareExactProposition context statement = + prepareExactPropositionTerm + context + (locate statement) + (compileStatement statement) + +-- | Compile the source bound of already-opened symbolic binders. This is the +-- shared checked constraint seam used by quantified statements and proof +-- binders, so relation signs, carrier casts, and global occurrences are +-- elaborated exactly once by the ordinary expression compiler. +prepareExactSymbolicBoundConstraints + :: ExactBinderContext + -> NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactProposition) +prepareExactSymbolicBoundConstraints context variables bound = + prepareExactPropositionTerm + context + (case bound of + Raw.Unbounded -> locate (NonEmpty.head variables) + _ -> locate bound) + (logicalConjunction + <$> compileSymbolicBoundConstraintList variables bound) + +-- | Compile the opened body used by a symbolic existential witness. Its +-- grouping is deliberately identical to 'SymbolicExists': all bound +-- constraints form the existential restriction and the stated proposition is +-- its body. +prepareExactSymbolicWitnessConstraints + :: ExactBinderContext + -> NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Raw.Stmt + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactProposition) +prepareExactSymbolicWitnessConstraints context variables bound statement = + prepareExactPropositionTerm context (locate statement) do + constraints <- + logicalConjunction + <$> compileSymbolicBoundConstraintList variables bound + body <- compileStatement statement + pure + (if constraints == logicalTruth + then body + else logicalAnd constraints body) + +-- | Compile the checked constraint of an already-opened noun witness. Named +-- binders are resolved normally; a nameless singular noun uses the nearest +-- anonymous binder and therefore introduces no lookup spelling. +prepareExactNounWitnessConstraints + :: ExactBinderContext + -> Raw.NounPhrase [] + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactProposition) +prepareExactNounWitnessConstraints context nounPhrase = + case nounPhrase of + Raw.NounPhrase left noun variables right suchThat -> + prepareExactPropositionTerm context (locate noun) do + subjects <- + case NonEmpty.nonEmpty variables of + Just binders -> + toList + <$> traverse compileIntroducedVariable binders + Nothing -> + pure [CBound 0] + compileNounPhraseConstraints + subjects left noun right suchThat + +prepareExactPropositionTerm + :: ExactBinderContext + -> Location + -> Elaborate (CanonicalTerm ObjectId) + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactProposition) +prepareExactPropositionTerm context location compile = Except.runExceptT do let initialElaboration = initialElaborationState context (term, finalElaboration) <- - State.runStateT - (compileStatement statement) - initialElaboration + State.runStateT compile initialElaboration checked <- either - (Except.throwError - . ExactCoreCheckFailed (locate statement)) + (Except.throwError . ExactCoreCheckFailed location) pure (checkScopedCanonicalCore (`Map.lookup` elaborationGlobals finalElaboration) @@ -565,7 +660,7 @@ prepareExactProposition context statement = unless (scopedCoreType checked == TyProp) (Except.throwError (ExactFormulaExpectedProposition - (locate statement) + location (scopedCoreType checked))) pure (PreparedExactProposition checked) @@ -786,7 +881,7 @@ binderIndices :: ExactBinderContext -> Map.Map Raw.VarSymbol Natural binderIndices (ExactBinderContext binders) = Map.fromList [ (variable, fromIntegral index) - | (index, ExactBinder _identity variable _coreType _structure) <- + | (index, ExactBinder _identity (Just variable) _coreType _structure) <- zip [0 :: Int ..] binders ] @@ -2275,21 +2370,8 @@ compileSymbolicQuantified -> Elaborate (CanonicalTerm ObjectId) compileSymbolicQuantified quantifier variables bound suchThat compileBody = withSetBinders variables do - subjects <- traverse compileIntroducedVariable variables - boundConstraints <- case bound of - Raw.Unbounded -> - pure [] - Raw.Bounded _location sign relation domain -> do - domain' <- compileExpressionAsSet domain - traverse - (\subject -> do - proposition <- - compileAtomicRelationTerms - subject relation domain' - pure case sign of - Raw.Positive -> proposition - Raw.Negative -> logicalNot proposition) - (toList subjects) + boundConstraints <- + compileSymbolicBoundConstraintList variables bound suchThatConstraints <- maybeToList <$> traverse compileStatement suchThat body <- compileBody @@ -2301,6 +2383,25 @@ compileSymbolicQuantified quantifier variables bound suchThat compileBody = (boundConstraints <> suchThatConstraints)) body) +compileSymbolicBoundConstraintList + :: NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Elaborate [CanonicalTerm ObjectId] +compileSymbolicBoundConstraintList variables = \case + Raw.Unbounded -> + pure [] + Raw.Bounded _location sign relation domain -> do + subjects <- traverse compileIntroducedVariable variables + domain' <- compileExpressionAsSet domain + traverse + (\subject -> do + proposition <- + compileAtomicRelationTerms subject relation domain' + pure case sign of + Raw.Positive -> proposition + Raw.Negative -> logicalNot proposition) + (toList subjects) + compileAtomicRelationTerms :: CanonicalTerm ObjectId -> Raw.Relation diff --git a/source/Checking/Exact/Proof.hs b/source/Checking/Exact/Proof.hs index 40911b0..f3f3b9d 100644 --- a/source/Checking/Exact/Proof.hs +++ b/source/Checking/Exact/Proof.hs @@ -56,8 +56,6 @@ import Numeric.Natural (Natural) data ExactProofError = ExactProofUnsupportedClaim !Location | ExactProofUnsupportedStep !Location - | ExactProofBoundedFixNotSupported !Location - | ExactProofBoundedTakeNotSupported !Location | ExactProofSetInductionVariableRequired !Location | ExactProofSetInductionVariableNotActive !Location !Raw.VarSymbol @@ -86,8 +84,6 @@ exactProofErrorLocation :: ExactProofError -> Location exactProofErrorLocation = \case ExactProofUnsupportedClaim location -> location ExactProofUnsupportedStep location -> location - ExactProofBoundedFixNotSupported location -> location - ExactProofBoundedTakeNotSupported location -> location ExactProofSetInductionVariableRequired location -> location ExactProofSetInductionVariableNotActive location _variable -> location @@ -115,10 +111,6 @@ renderExactProofError = \case at location <> "this claim is not yet supported by the typed checker" ExactProofUnsupportedStep location -> at location <> "this proof step is not yet supported by the typed checker" - ExactProofBoundedFixNotSupported location -> - at location <> "bounded proof binders are not yet supported" - ExactProofBoundedTakeNotSupported location -> - at location <> "bounded proof witnesses are not yet supported" ExactProofSetInductionVariableRequired location -> at location <> "exact set induction requires a named set variable" ExactProofSetInductionVariableNotActive location variable -> @@ -485,34 +477,47 @@ prepareProof fallback context locals inductionAntecedents goal = \case goal justification Raw.FixSymbolic location variables bound continuation -> do - unless (bound == Raw.Unbounded) - (throwProof - (ExactProofBoundedFixNotSupported location)) (context', goal', identities) <- openFixedVariables context goal variables - PreparedFix identities - <$> prepareProof - fallback - context' - locals - Nothing - goal' - continuation + case bound of + Raw.Unbounded -> + PreparedFix identities + <$> prepareProof + fallback + context' + locals + Nothing + goal' + continuation + _ -> do + constraint <- + prepareSymbolicBoundConstraints + context' variables bound + prepareGuardedFix + fallback location context' locals goal' + identities constraint continuation + Raw.FixSuchThat location variables statement continuation -> do + (context', goal', identities) <- + openFixedVariables context goal variables + constraint <- + Exact.preparedExactPropositionCore + <$> prepareStatement context' statement + prepareGuardedFix + fallback location context' locals goal' + identities constraint continuation Raw.Assume location statement continuation -> do - (antecedent, conclusion) <- + supplied <- prepareStatement context statement + when (isNothing (openScopedImplication goal)) + (throwProof (ExactProofExpectedImplicationGoal location)) + (assumption, conclusion) <- maybe - (throwProof - (ExactProofExpectedImplicationGoal location)) + (throwProof (ExactProofGoalStatementMismatch location)) pure - (openScopedImplication goal) - supplied <- prepareStatement context statement - unless - (Exact.preparedExactPropositionCore supplied - == antecedent) - (throwProof - (ExactProofGoalStatementMismatch location)) - local <- allocateLocal ExactAssumption context antecedent - PreparedAssume antecedent + (openScopedAssumption + (Exact.preparedExactPropositionCore supplied) + goal) + local <- allocateLocal ExactAssumption context assumption + PreparedAssume assumption <$> prepareProof fallback context @@ -521,36 +526,13 @@ prepareProof fallback context locals inductionAntecedents goal = \case conclusion continuation Raw.TakeVar location variables bound statement justification continuation -> do - unless (bound == Raw.Unbounded) - (throwProof - (ExactProofBoundedTakeNotSupported location)) - identities <- - traverse (const allocateLocalIdentity) variables - context' <- - either - (throwProof . ExactProofElaborationFailed) - pure - (Exact.extendExactBinderContext - (NonEmpty.zip identities variables) - context) - witness <- - Exact.preparedExactPropositionCore - <$> prepareStatement context' statement - let witnessCount = length (toList variables) - existence = closeTakenWitnesses witnessCount witness - goal' = weakenForTakenWitnesses witnessCount goal - discharge <- - prepareDischarge - location context locals existence justification - local <- allocateLocal ExactAssumption context' witness - PreparedTake (toList identities) witness discharge - <$> prepareProof - fallback - context' - (locals <> [local]) - Nothing - goal' - continuation + prepareSymbolicTake + fallback location context locals goal variables bound statement + justification continuation + Raw.TakeNoun location nounPhrase justification continuation -> + prepareNounTake + fallback location context locals goal nounPhrase + justification continuation Raw.BySetInduction location variable continuation -> case (inductionAntecedents, continuation) of (Nothing, _proof) -> @@ -593,6 +575,12 @@ prepareProof fallback context locals inductionAntecedents goal = \case justification (Just _antecedents, _proof) -> throwProof (ExactProofUnsupportedStep location) + Raw.Have location Nothing + (Raw.SymbolicExists _existential variables bound statement) + justification continuation -> + prepareSymbolicTake + fallback location context locals goal variables bound statement + justification continuation Raw.Have location since statement justification continuation -> do when (isJust since) (throwProof (ExactProofUnsupportedStep location)) @@ -756,6 +744,168 @@ prepareProof fallback context locals inductionAntecedents goal = \case (impossible "an exact claim antecedent changed context") (implyScopedCore antecedent conclusion) +prepareGuardedFix + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> [Exact.ExactLocalId] + -> ScopedCheckedCore ObjectId + -> Raw.Proof + -> Prepare PreparedProof +prepareGuardedFix + fallback location context locals goal identities constraint continuation = do + (antecedent, conclusion) <- + maybe + (throwProof (ExactProofExpectedImplicationGoal location)) + pure + (openScopedImplication goal) + unless (constraint == antecedent) + (throwProof (ExactProofGoalStatementMismatch location)) + local <- allocateLocal ExactAssumption context constraint + prepared <- + prepareProof + fallback + context + (locals <> [local]) + Nothing + conclusion + continuation + pure (PreparedFix identities (PreparedAssume constraint prepared)) + +prepareSymbolicBoundConstraints + :: Exact.ExactBinderContext + -> NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Prepare (ScopedCheckedCore ObjectId) +prepareSymbolicBoundConstraints context variables bound = + Exact.preparedExactPropositionCore + <$> ( liftDriver + (Exact.prepareExactSymbolicBoundConstraints + context variables bound) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + ) + +prepareSymbolicTake + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Raw.Stmt + -> Raw.Justification + -> Raw.Proof + -> Prepare PreparedProof +prepareSymbolicTake + fallback location context locals goal variables bound statement + justification continuation = do + identities <- traverse (const allocateLocalIdentity) variables + context' <- + either + (throwProof . ExactProofElaborationFailed) + pure + (Exact.extendExactBinderContext + (NonEmpty.zip identities variables) + context) + witness <- + Exact.preparedExactPropositionCore + <$> ( liftDriver + (Exact.prepareExactSymbolicWitnessConstraints + context' variables bound statement) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + ) + prepareTake + fallback location context locals goal context' + (toList identities) witness justification continuation + +prepareNounTake + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> Raw.NounPhrase [] + -> Raw.Justification + -> Raw.Proof + -> Prepare PreparedProof +prepareNounTake + fallback location context locals goal nounPhrase + justification continuation = do + (identities, context') <- + case nounPhrase of + Raw.NounPhrase _left _noun variables _right _suchThat -> + case NonEmpty.nonEmpty variables of + Just binders -> do + identities <- + traverse (const allocateLocalIdentity) binders + context' <- + either + (throwProof . ExactProofElaborationFailed) + pure + (Exact.extendExactBinderContext + (NonEmpty.zip identities binders) + context) + pure (toList identities, context') + Nothing -> do + identity <- allocateLocalIdentity + context' <- + either + (throwProof . ExactProofElaborationFailed) + pure + (Exact.extendExactAnonymousBinderContext + identity context) + pure ([identity], context') + witness <- + Exact.preparedExactPropositionCore + <$> ( liftDriver + (Exact.prepareExactNounWitnessConstraints + context' nounPhrase) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + ) + prepareTake + fallback location context locals goal context' + identities witness justification continuation + +prepareTake + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> Exact.ExactBinderContext + -> [Exact.ExactLocalId] + -> ScopedCheckedCore ObjectId + -> Raw.Justification + -> Raw.Proof + -> Prepare PreparedProof +prepareTake + fallback location context locals goal witnessContext + identities witness justification continuation = do + let witnessCount = length identities + existence = closeTakenWitnesses witnessCount witness + goal' = weakenForTakenWitnesses witnessCount goal + discharge <- + prepareDischarge + location context locals existence justification + local <- allocateLocal ExactAssumption witnessContext witness + PreparedTake identities witness discharge + <$> prepareProof + fallback + witnessContext + (locals <> [local]) + Nothing + goal' + continuation + -- The discharged existential and the opened witness premise are the same -- checked proposition viewed on opposite sides of existential elimination. closeTakenWitnesses diff --git a/source/Felix/Cache/Codec.hs b/source/Felix/Cache/Codec.hs index ec7a694..d684b11 100644 --- a/source/Felix/Cache/Codec.hs +++ b/source/Felix/Cache/Codec.hs @@ -75,7 +75,7 @@ newtype CacheEpoch = CacheEpoch Word32 currentCacheEpoch :: CacheEpoch currentCacheEpoch = - CacheEpoch 26 + CacheEpoch 27 cacheEpochValue :: CacheEpoch -> Word32 cacheEpochValue (CacheEpoch value) = diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs index 64f083a..7748dac 100644 --- a/source/Test/Unit/Module.hs +++ b/source/Test/Unit/Module.hs @@ -67,6 +67,7 @@ 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 @@ -122,6 +123,8 @@ unitTests = confinesExactQuantifiedTerms , testCase "compiles exact ordinary proofs" compilesExactOrdinaryProofs + , testCase "restores exact binder and witness proof forms" + restoresExactBinderAndWitnessProofForms , testCase "compiles and reuses proof-local set definitions" compilesAndReusesProofLocalSetDefinitions , testCase "compiles and reuses proof-local function graphs" @@ -2107,6 +2110,363 @@ compilesExactOrdinaryProofs = 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]) + runNoLoggingT + (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)] + } + +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 diff --git a/test/phase5/exact-proof-parity-invalid-assume.tex b/test/phase5/exact-proof-parity-invalid-assume.tex new file mode 100644 index 0000000..3bb04bc --- /dev/null +++ b/test/phase5/exact-proof-parity-invalid-assume.tex @@ -0,0 +1,8 @@ +\begin{proposition}\label{invalid_disjunct_assume} + Let $A,B$ be sets. + $A=A$ or $B=B$. +\end{proposition} +\begin{proof} + Assume $A=A$. + Follows. +\end{proof} diff --git a/test/phase5/exact-proof-parity-invalid-fix-shape.tex b/test/phase5/exact-proof-parity-invalid-fix-shape.tex new file mode 100644 index 0000000..16a58a2 --- /dev/null +++ b/test/phase5/exact-proof-parity-invalid-fix-shape.tex @@ -0,0 +1,8 @@ +\begin{proposition}\label{invalid_fix_shape} + Let $A$ be a set. + $A=A$. +\end{proposition} +\begin{proof} + Fix $x\in A$. + Follows. +\end{proof} diff --git a/test/phase5/exact-proof-parity-invalid-fix.tex b/test/phase5/exact-proof-parity-invalid-fix.tex new file mode 100644 index 0000000..0a2b24c --- /dev/null +++ b/test/phase5/exact-proof-parity-invalid-fix.tex @@ -0,0 +1,8 @@ +\begin{proposition}\label{invalid_bounded_fix} + Let $A$ be a set. + For all $x\in A$ we have $x\in A$. +\end{proposition} +\begin{proof} + Fix $x\notin A$. + Follows. +\end{proof} diff --git a/test/phase5/exact-proof-parity.tex b/test/phase5/exact-proof-parity.tex new file mode 100644 index 0000000..73d849f --- /dev/null +++ b/test/phase5/exact-proof-parity.tex @@ -0,0 +1,107 @@ +\begin{proposition}\label{bounded_fix_single} + Let $A$ be a set. + For all $x\in A$ we have $x\in A$. +\end{proposition} +\begin{proof} + Fix $x\in A$. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{bounded_fix_multiple} + Let $A$ be a set. + For all $x,y\in A$ we have $x\in A$ and $y\in A$. +\end{proposition} +\begin{proof} + Fix $x,y\in A$. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{bounded_fix_negative} + Let $A$ be a set. + For all $x\notin A$ we have $x\notin A$. +\end{proposition} +\begin{proof} + Fix $x\notin A$. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{fix_such_that} + Let $A$ be a set. + For all $x$ such that $x\in A$ we have $x\in A$. +\end{proposition} +\begin{proof} + Fix $x$ such that $x\in A$. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{assume_left_conjunct} + Let $A,B$ be sets. + If $A=A$ and $B=B$, then $A=A$. +\end{proposition} +\begin{proof} + Assume $A=A$. + Assume $B=B$. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{assume_right_conjunct} + Let $A,B$ be sets. + If $A=A$ and $B=B$, then $B=B$. +\end{proposition} +\begin{proof} + Assume $B=B$. + Assume $A=A$. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{take_bounded} + Let $A$ be a set. + Suppose there exists $x\in A$ such that $x=x$. + Then $A=A$. +\end{proposition} +\begin{proof} + Take $x\in A$ such that $x=x$ by assumption. + We have $x\in A$ by assumption. + Follows. +\end{proof} + +\begin{proposition}\label{take_named_noun} + Let $A$ be a set. + Suppose there exist sets $x,y$ such that $x=x$ and $y=y$. + Then $A=A$. +\end{proposition} +\begin{proof} + Take a set $x,y$ such that $x=x$ and $y=y$ by assumption. + Follows. +\end{proof} + +\begin{proposition}\label{take_anonymous_noun} + Let $A$ be a set. + Suppose there exists a set. + Then $A=A$. +\end{proposition} +\begin{proof} + Take a set by assumption. + Follows. +\end{proof} + +\begin{proposition}\label{existential_have_witness} + Let $A$ be a set. + Suppose there exists $x\in A$ such that $x=x$. + Then $A=A$. +\end{proposition} +\begin{proof} + We have there exists $x\in A$ such that $x=x$ by assumption. + We have $x\in A$ by assumption. + Follows. +\end{proof} + +\begin{proposition}\label{take_omitted_continuation} + Let $A$ be a set. + Suppose there exists $x\in A$ such that $x=x$. + Then $A=A$. +\end{proposition} +\begin{proof} + Take $x\in A$ such that $x=x$ by assumption. + Omitted. +\end{proof} |