Separate ATP premises from kernel imports

2 files changed, 85 insertions, 45 deletions

diff --git a/source/Checking/Declaration.hs b/source/Checking/Declaration.hs
index c9e2173..1968657 100644
--- a/source/Checking/Declaration.hs
+++ b/source/Checking/Declaration.hs
@@ -1672,7 +1672,16 @@ data LocalClaim = LocalClaim
 useAuthorizedFact
     :: SemanticFactOccurrenceFingerprint
     -> CandidateProof ImportIx
-useAuthorizedFact fingerprint = CandidateProof do
+useAuthorizedFact fingerprint = do
+    proposition <- consumeAuthorizedFact fingerprint
+    registerKernelImport proposition
+
+-- | Validate one fact capability and accumulate only its safety effect.
+-- Backend use does not register a kernel import.
+consumeAuthorizedFact
+    :: SemanticFactOccurrenceFingerprint
+    -> CandidateProof CheckedPropositionContent
+consumeAuthorizedFact fingerprint = CandidateProof do
     state <- State.get
     let builder = candidateProofBuilder state
         declaration = candidateProofDeclaration state
@@ -1682,7 +1691,7 @@ useAuthorizedFact fingerprint = CandidateProof do
                 (declarationPending declaration)
     case staged of
         Just pending ->
-            usePendingFact pending state
+            consumePendingFact pending state
         Nothing ->
             case Map.lookup
                     fingerprint
@@ -1692,7 +1701,7 @@ useAuthorizedFact fingerprint = CandidateProof do
                         (Except.throwError
                             (AuthorizedFactNotVisible fingerprint))
                 Just authorized ->
-                    useBuilderAuthorizedFact authorized state
+                    consumeBuilderAuthorizedFact authorized state
 
 -- | Materialize one sealed direct import and its transitive parents.  The
 -- interface DAG is folded imported-before-importer and each producer
@@ -1944,7 +1953,9 @@ useStagedCandidate premise = CandidateProof do
                 (reservedCandidateSlot premise)
                 (declarationPending
                     (candidateProofDeclaration state)))
-    usePendingFact pending state
+    proposition <- consumePendingFact pending state
+    updated <- State.get
+    appendCandidatePremise proposition updated
 
 proveLocalKernelClaim
     :: CheckedPropositionContent
@@ -2457,14 +2468,14 @@ reservedCandidateKey
     (identity, prefix, invocation, stage, slot)
 
 
-useBuilderAuthorizedFact
+consumeBuilderAuthorizedFact
     :: AuthorizedFact
     -> CandidateProofState
     -> StateT
         CandidateProofState
         (ExceptT DeclarationError IO)
-        ImportIx
-useBuilderAuthorizedFact
+        CheckedPropositionContent
+consumeBuilderAuthorizedFact
         (AuthorizedFact proposition occurrence authorization)
         state = do
     let builder = candidateProofBuilder state
@@ -2477,19 +2488,20 @@ useBuilderAuthorizedFact
         )
         (State.lift
             (Except.throwError BuilderFactAuthorizationMismatch))
-    accumulateAuthorizedPremise
+    accumulateAuthorizedSafety
         proposition
         authority
         state
+    pure proposition
 
-usePendingFact
+consumePendingFact
     :: PendingCandidate
     -> CandidateProofState
     -> StateT
         CandidateProofState
         (ExceptT DeclarationError IO)
-        ImportIx
-usePendingFact
+        CheckedPropositionContent
+consumePendingFact
         (PendingCandidate premise certificate authorization)
         state = do
     let builder = candidateProofBuilder state
@@ -2517,20 +2529,22 @@ usePendingFact
                     (reservedCandidateStage premise)
                     (reservedCandidateSlot current)
                     (reservedCandidateStage current))))
-    accumulateAuthorizedPremise
-        (candidateCheckedProposition premise)
+    let proposition = candidateCheckedProposition premise
+    accumulateAuthorizedSafety
+        proposition
         authority
         state
+    pure proposition
 
-accumulateAuthorizedPremise
+accumulateAuthorizedSafety
     :: CheckedPropositionContent
     -> FactAuthority
     -> CandidateProofState
     -> StateT
         CandidateProofState
         (ExceptT DeclarationError IO)
-        ImportIx
-accumulateAuthorizedPremise proposition authority state = do
+        ()
+accumulateAuthorizedSafety proposition authority state = do
     let expected =
             theoremRef
                 (logicalBuilderTheory
@@ -2545,7 +2559,13 @@ accumulateAuthorizedPremise proposition authority state = do
                         authority
                         (candidateProofSafety state))))
     State.put state{candidateProofSafety = safety}
-    appendCandidatePremise proposition state{candidateProofSafety = safety}
+
+registerKernelImport
+    :: CheckedPropositionContent
+    -> CandidateProof ImportIx
+registerKernelImport proposition = CandidateProof do
+    state <- State.get
+    appendCandidatePremise proposition state
 
 appendCandidatePremise
     :: CheckedPropositionContent
@@ -2750,14 +2770,8 @@ validateVampireProblemEnvironment prepared initial = do
   where
     validatePremise selected = do
         let fingerprint = Backend.typedBackendFactReference selected
-        _index <- useAuthorizedFact fingerprint
+        proposition <- consumeAuthorizedFact fingerprint
         state <- CandidateProof State.get
-        proposition <-
-            maybe
-                (failCandidateProof
-                    (AuthorizedFactNotVisible fingerprint))
-                pure
-                (lookupAuthorizedProposition fingerprint state)
         unless
             ( Backend.supportedPropositionTerm
                 (Backend.typedBackendFactProposition selected)
@@ -2824,27 +2838,6 @@ failCandidateProof
 failCandidateProof =
     CandidateProof . State.lift . Except.throwError
 
-lookupAuthorizedProposition
-    :: SemanticFactOccurrenceFingerprint
-    -> CandidateProofState
-    -> Maybe CheckedPropositionContent
-lookupAuthorizedProposition fingerprint state =
-    case findPendingByFingerprint
-            fingerprint
-            (declarationPending
-                (candidateProofDeclaration state)) of
-        Just (PendingCandidate candidate _ _) ->
-            Just (candidateCheckedProposition candidate)
-        Nothing ->
-            case Map.lookup
-                    fingerprint
-                    (logicalBuilderFacts
-                        (candidateProofBuilder state)) of
-                Just (AuthorizedFact proposition _ _) ->
-                    Just proposition
-                Nothing ->
-                    Nothing
-
 data ValidationMode
     = EnvironmentImportMode
     | ProofValidationMode !ProofSyntaxId
diff --git a/source/Test/Unit/Declaration.hs b/source/Test/Unit/Declaration.hs
index 975965c..af5af96 100644
--- a/source/Test/Unit/Declaration.hs
+++ b/source/Test/Unit/Declaration.hs
@@ -761,6 +761,53 @@ preservesSourceAxiomSafetyThroughVampireValidation =
             (Authority.factAuthoritySafety
                 (Authority.validationTarget
                     (Semantic.proofValidationRecordCertificate freshRecord)))
+        separationCalls <- IORef.newIORef (0 :: Int)
+        let separationResolver = Declaration.vampireResolver \task -> do
+                IORef.modifyIORef' separationCalls (+ 1)
+                resolveAccepted executable task
+        separated <-
+            (runDriverWithResolver fixture separationResolver do
+                void
+                    (Declaration.commitProofDeclaration
+                        (Semantic.proofSyntaxId "source-axiom") do
+                            candidate <- Declaration.reserveCandidate
+                                (factSpec fixture "source-axiom")
+                            Declaration.authorizeSourceAxiomCandidate candidate)
+                Declaration.commitProofDeclaration
+                    (Semantic.proofSyntaxId "atp-does-not-import") do
+                        candidate <- Declaration.reserveCandidate
+                            (factSpec fixture "atp-does-not-import")
+                        Declaration.authorizeKernelProofCandidate candidate do
+                            Declaration.acceptVampireObligation prepared
+                            pure
+                                (Kernel.importedFactDerivation
+                                    (Kernel.importIx 0))
+                :: IO
+                    (Declaration.DriverResult Text
+                        ((), Declaration.CommittedDeclarationBatch)))
+        assertEqual "mixed proof executes its ATP obligation"
+            1
+            =<< IORef.readIORef separationCalls
+        case separated of
+            Declaration.DriverFailed
+                    (Declaration.DriverDeclarationFailed
+                        (Declaration.KernelCompletionFailed
+                            (Kernel.KernelReplayImportOutOfBounds index)))
+                    prefix -> do
+                assertEqual "ATP premise is absent from kernel imports"
+                    (Kernel.importIx 0)
+                    index
+                assertEqual "failed mixed proof retains only its prefix"
+                    1
+                    (length
+                        (Declaration.pendingModulePrefixBatches prefix))
+            Declaration.DriverFailed failure _prefix ->
+                assertFailure
+                    ("unexpected mixed-proof failure: " <> show failure)
+            Declaration.DriverSucceeded{} ->
+                assertFailure "ATP premise entered the kernel import inventory"
+            Declaration.DriverSealFailed{} ->
+                assertFailure "mixed proof unexpectedly reached sealing"
         withOpenedStore fixture root \store -> do
             freshPrefix <-
                 case freshOutcome of