Aggregate typed Vampire obligations

1 files changed, 249 insertions, 133 deletions

diff --git a/source/Checking/Declaration.hs b/source/Checking/Declaration.hs
index 94163cb..ab7b33c 100644
--- a/source/Checking/Declaration.hs
+++ b/source/Checking/Declaration.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE RankNTypes #-}
 
 -- | Builder-confined authorization and atomic typed declaration append.
 module Checking.Declaration
@@ -10,6 +11,8 @@ module Checking.Declaration
     , DriverResult(..)
     , runModuleDriver
     , failModuleDriver
+    , VampireResolver
+    , vampireResolver
     , Declaration
     , failDeclaration
     , addDeclarationObject
@@ -29,6 +32,7 @@ module Checking.Declaration
     , useLocalClaim
     , authorizeKernelProofCandidate
     , authorizeKernelConstructionCandidate
+    , acceptVampireObligation
     , authorizeVampireCandidate
     , authorizeSourceAxiomCandidate
     , authorizeOmittedCandidate
@@ -276,7 +280,37 @@ forceCommittedBatch
                 (declarationValidationRecordCertificates record)
 
 
+newtype VampireResolver = VampireResolver
+    { resolveVampire
+        :: forall origin.
+            Provers.PreparedTypedProverTask
+                SemanticFactOccurrenceFingerprint
+                Void
+                origin
+                ObjectId
+            -> IO
+                (Either
+                    Provers.ProverProcessError
+                    Provers.ProverAnswer)
+    }
+
+vampireResolver
+    :: (forall origin.
+        Provers.PreparedTypedProverTask
+            SemanticFactOccurrenceFingerprint
+            Void
+            origin
+            ObjectId
+        -> IO
+            (Either
+                Provers.ProverProcessError
+                Provers.ProverAnswer))
+    -> VampireResolver
+vampireResolver =
+    VampireResolver
+
 data DriverState = DriverState
+    !VampireResolver
     !LogicalBuilder
     !PendingModulePrefix
 
@@ -315,12 +349,13 @@ runModuleDriver
     :: CheckedFoundation
     -> ModuleName
     -> [SemanticInterfaceId]
+    -> VampireResolver
     -> ModuleDriver failure value
     -> IO
         (Either
             DriverOpenError
             (DriverResult failure value))
-runModuleDriver foundation owner direct action = do
+runModuleDriver foundation owner direct resolver action = do
     unique <- BuilderIdentity <$> newUnique
     let theory = theoryId foundation
     case (,) <$>
@@ -352,9 +387,10 @@ runModuleDriver foundation owner direct action = do
                         }
                 initialState =
                     DriverState
+                        resolver
                         builder
                         (PendingModulePrefix prefix [])
-            (result, DriverState finalBuilder finalPrefix) <-
+            (result, DriverState _ finalBuilder finalPrefix) <-
                 State.runStateT
                     (Except.runExceptT
                         (runDriverStep action))
@@ -445,7 +481,8 @@ data PendingCandidate = PendingCandidate
     !PendingFactAuthorization
 
 data DeclarationState = DeclarationState
-    { declarationBuilder :: !LogicalBuilder
+    { declarationVampireResolver :: !VampireResolver
+    , declarationBuilder :: !LogicalBuilder
     , declarationOwnSlot :: !DeclarationSlot
     , declarationInvocation :: !DeclarationInvocation
     , declarationObjectsReversed :: ![AssertedObject]
@@ -463,14 +500,14 @@ newtype Declaration value = Declaration
     { runDeclaration
         :: StateT
             DeclarationState
-            (Either DeclarationError)
+            (ExceptT DeclarationError IO)
             value
     }
     deriving newtype (Functor, Applicative, Monad)
 
 failDeclaration :: DeclarationError -> Declaration value
 failDeclaration =
-    Declaration . State.lift . Left
+    Declaration . State.lift . Except.throwError
 
 addDeclarationObject :: AssertedObject -> Declaration ()
 addDeclarationObject asserted =
@@ -555,13 +592,15 @@ data CandidateProofState = CandidateProofState
     , candidateProofPremisesReversed :: ![CandidatePremise]
     , candidateProofPremiseCount :: !Natural
     , candidateProofSafety :: !CandidateSafety
+    , candidateProofAcceptedRequestsReversed
+        :: ![PreparedRequestId]
     }
 
 newtype CandidateProof value = CandidateProof
     { runCandidateProof
         :: StateT
             CandidateProofState
-            (Either DeclarationError)
+            (ExceptT DeclarationError IO)
             value
     }
     deriving newtype (Functor, Applicative, Monad)
@@ -592,7 +631,7 @@ useAuthorizedFact fingerprint = CandidateProof do
                     (logicalBuilderFacts builder) of
                 Nothing ->
                     State.lift
-                        (Left
+                        (Except.throwError
                             (AuthorizedFactNotVisible fingerprint))
                 Just authorized ->
                     useBuilderAuthorizedFact authorized state
@@ -603,13 +642,15 @@ useStagedCandidate
 useStagedCandidate premise = CandidateProof do
     state <- State.get
     let current = candidateProofCandidate state
-    validateReservedCandidate
-        (candidateProofDeclaration state)
-        premise
+    State.lift
+        (Except.liftEither
+            (validateReservedCandidate
+                (candidateProofDeclaration state)
+                premise))
     unless
         (reservedStage premise < reservedStage current)
         (State.lift
-            (Left
+            (Except.throwError
                 (StagedPremiseNotEarlier
                     (reservedCandidateSlot premise)
                     (reservedCandidateStage premise)
@@ -618,7 +659,7 @@ useStagedCandidate premise = CandidateProof do
     pending <-
         maybe
             (State.lift
-                (Left
+                (Except.throwError
                     (StagedPremiseNotAuthorized
                         (reservedCandidateSlot premise))))
             pure
@@ -636,7 +677,8 @@ proveLocalKernelClaim proposition derivation = CandidateProof do
     state <- State.get
     void
         (State.lift
-            (replayCandidateKernel proposition derivation state))
+            (Except.liftEither
+                (replayCandidateKernel proposition derivation state)))
     let candidate = candidateProofCandidate state
         declaration = candidateProofDeclaration state
     pure
@@ -660,7 +702,8 @@ useLocalClaim
               && invocation == declarationInvocation declaration
               && slot == reservedCandidateSlot candidate
             )
-            (State.lift (Left LocalClaimOutsideCandidate))
+            (State.lift
+                (Except.throwError LocalClaimOutsideCandidate))
         appendCandidatePremise proposition state
 
 
@@ -673,15 +716,18 @@ authorizeKernelProofCandidate candidate proof =
         (derivation, final) <-
             State.runStateT (runCandidateProof proof) initial
         void
-            (replayCandidateKernel
-                (candidateCheckedProposition candidate)
-                derivation
+            (Except.liftEither
+                (replayCandidateKernel
+                    (candidateCheckedProposition candidate)
+                    derivation
+                    final))
+        Except.liftEither
+            (freshCompletion
+                candidate
+                (CheckedSourceProof
+                    (acceptedRequestIds final))
+                (candidateProofSafety final)
                 final)
-        freshCompletion
-            candidate
-            (CheckedSourceProof [])
-            (candidateProofSafety final)
-            final
 
 authorizeKernelConstructionCandidate
     :: KernelConstructionDescriptor
@@ -693,20 +739,23 @@ authorizeKernelConstructionCandidate descriptor candidate proof =
         (derivation, final) <-
             State.runStateT (runCandidateProof proof) initial
         replayed <-
-            replayCandidateKernel
+            Except.liftEither
+                (replayCandidateKernel
+                    (candidateCheckedProposition candidate)
+                    derivation
+                    final)
+        Except.liftEither
+            (validateKernelConstruction
+                descriptor
                 (candidateCheckedProposition candidate)
-                derivation
-                final
-        validateKernelConstruction
-            descriptor
-            (candidateCheckedProposition candidate)
-            replayed
-            final
-        freshCompletion
-            candidate
-            (CheckedKernelConstruction descriptor)
-            (candidateProofSafety final)
-            final
+                replayed
+                final)
+        Except.liftEither
+            (freshCompletion
+                candidate
+                (CheckedKernelConstruction descriptor)
+                (candidateProofSafety final)
+                final)
 
 authorizeSourceAxiomCandidate
     :: ReservedCandidate
@@ -717,11 +766,12 @@ authorizeSourceAxiomCandidate candidate =
                 addCandidateEscape
                     SourceAxiom
                     initialCandidateSafety
-        in freshCompletion
-            candidate
-            SourceAxiomAuthorization
-            safety
-            initial
+        in Except.liftEither
+            (freshCompletion
+                candidate
+                SourceAxiomAuthorization
+                safety
+                initial)
 
 authorizeOmittedCandidate
     :: ReservedCandidate
@@ -735,36 +785,86 @@ authorizeOmittedCandidate candidate proof =
                 addCandidateEscape
                     Omitted
                     (candidateProofSafety final)
-        freshCompletion
-            candidate
-            OmittedAuthorization
-            safety
-            final
+        Except.liftEither
+            (freshCompletion
+                candidate
+                OmittedAuthorization
+                safety
+                final)
 
--- | Complete one candidate only from an accepted run of its exact prepared
--- request. Every selected global or staged premise passes through the same
--- builder-authorized lookup used by kernel completion.
-authorizeVampireCandidate
-    :: ReservedCandidate
-    -> Provers.PreparedTypedProverTask
+-- | Validate one closed obligation before invoking Vampire, then retain its
+-- exact accepted request. Typed local obligations remain a Phase 5 consumer;
+-- this walking subset rejects local premises.
+acceptVampireObligation
+    :: Provers.PreparedTypedProverTask
         SemanticFactOccurrenceFingerprint
         Void
         origin
         ObjectId
-    -> Provers.AcceptedVampireRun
+    -> CandidateProof ()
+acceptVampireObligation prepared = CandidateProof do
+    initial <- State.get
+    let resolver =
+            declarationVampireResolver
+                (candidateProofDeclaration initial)
+    validated <-
+        State.lift
+            (validatePreparedVampireProblem
+                (candidateProofCandidate initial)
+                prepared
+                initial)
+    result <- liftIO (resolveVampire resolver prepared)
+    accepted <-
+        case result of
+            Left err ->
+                State.lift
+                    (Except.throwError
+                        (VampireProcessFailed err))
+            Right answer ->
+                maybe
+                    (State.lift
+                        (Except.throwError
+                            (VampireObligationRejected answer)))
+                    pure
+                    (Provers.provedVampireRun answer)
+    let request = Provers.preparedTypedProverRequest prepared
+    unless
+        (Provers.acceptedVampireRequest accepted == request)
+        (State.lift
+            (Except.throwError VampireRequestMismatch))
+    let requestId = Provers.preparedVerificationRequestId request
+    State.put
+        validated
+            { candidateProofAcceptedRequestsReversed =
+                requestId
+                    : candidateProofAcceptedRequestsReversed validated
+            }
+
+-- | Complete one checked source candidate after all of its obligations have
+-- been accepted in source order.
+authorizeVampireCandidate
+    :: ReservedCandidate
+    -> CandidateProof ()
     -> Declaration ()
-authorizeVampireCandidate candidate prepared accepted =
+authorizeVampireCandidate candidate proof =
     authorizeOneCandidate candidate \initial -> do
-        final <- validatePreparedVampire candidate prepared accepted initial
-        let request = Provers.preparedTypedProverRequest prepared
-            direct =
-                CheckedSourceProof
-                    [Provers.preparedVerificationRequestId request]
-        freshCompletion
-            candidate
-            direct
-            (candidateProofSafety final)
-            final
+        ((), final) <-
+            State.runStateT (runCandidateProof proof) initial
+        case acceptedRequestIds final of
+            [] ->
+                Except.throwError
+                    VampireProofHasNoAcceptedObligations
+            requests ->
+                Except.liftEither
+                    (freshCompletion
+                        candidate
+                        (CheckedSourceProof requests)
+                        (candidateProofSafety final)
+                        final)
+
+acceptedRequestIds :: CandidateProofState -> [PreparedRequestId]
+acceptedRequestIds =
+    reverse . candidateProofAcceptedRequestsReversed
 
 freshCompletion
     :: ReservedCandidate
@@ -808,17 +908,19 @@ freshCompletion candidate direct safety proofState = do
 authorizeOneCandidate
     :: ReservedCandidate
     -> (CandidateProofState
-        -> Either DeclarationError PendingCandidate)
+        -> ExceptT DeclarationError IO PendingCandidate)
     -> Declaration ()
 authorizeOneCandidate candidate complete = Declaration do
     state <- State.get
-    validateReservedCandidate state candidate
+    State.lift
+        (Except.liftEither
+            (validateReservedCandidate state candidate))
     when
         (Map.member
             (reservedCandidateSlot candidate)
             (declarationPending state))
         (State.lift
-            (Left
+            (Except.throwError
                 (CandidateAlreadyAuthorized
                     (reservedCandidateSlot candidate))))
     unless
@@ -826,13 +928,14 @@ authorizeOneCandidate candidate complete = Declaration do
             == CandidateStage
                 (declarationAuthorizationFrontier state))
         (State.lift
-            (Left
+            (Except.throwError
                 (CandidateOutsideAuthorizationFrontier
                     (reservedCandidateSlot candidate)
                     (reservedCandidateStage candidate)
                     (declarationAuthorizationFrontier state))))
     initial <- State.lift
-        (initialCandidateProofState state candidate)
+        (Except.liftEither
+            (initialCandidateProofState state candidate))
     pending <- State.lift (complete initial)
     let state' =
             state
@@ -883,6 +986,7 @@ initialCandidateProofState declaration candidate = do
         , candidateProofPremisesReversed = []
         , candidateProofPremiseCount = 0
         , candidateProofSafety = initialCandidateSafety
+        , candidateProofAcceptedRequestsReversed = []
         }
 
 reservedStage :: ReservedCandidate -> CandidateStage
@@ -893,7 +997,7 @@ reservedStage
 validateReservedCandidate
     :: DeclarationState
     -> ReservedCandidate
-    -> StateT state (Either DeclarationError) ()
+    -> Either DeclarationError ()
 validateReservedCandidate declaration candidate = do
     let builder = declarationBuilder declaration
         ReservedCandidate
@@ -906,9 +1010,7 @@ validateReservedCandidate declaration candidate = do
                 (declarationReservations declaration)
                 == Just candidate
         )
-        (State.lift
-            (Left
-                (CandidateOutsideDeclaration slot)))
+        (Left (CandidateOutsideDeclaration slot))
 
 instance Eq ReservedCandidate where
     left == right =
@@ -925,7 +1027,10 @@ reservedCandidateKey
 useBuilderAuthorizedFact
     :: AuthorizedFact
     -> CandidateProofState
-    -> StateT CandidateProofState (Either DeclarationError) ImportIx
+    -> StateT
+        CandidateProofState
+        (ExceptT DeclarationError IO)
+        ImportIx
 useBuilderAuthorizedFact
         (AuthorizedFact proposition occurrence authorization)
         state = do
@@ -937,7 +1042,8 @@ useBuilderAuthorizedFact
           && slot == semanticFactSlot occurrence
           && authority == semanticFactAuthority occurrence
         )
-        (State.lift (Left BuilderFactAuthorizationMismatch))
+        (State.lift
+            (Except.throwError BuilderFactAuthorizationMismatch))
     accumulateAuthorizedPremise
         proposition
         authority
@@ -946,7 +1052,10 @@ useBuilderAuthorizedFact
 usePendingFact
     :: PendingCandidate
     -> CandidateProofState
-    -> StateT CandidateProofState (Either DeclarationError) ImportIx
+    -> StateT
+        CandidateProofState
+        (ExceptT DeclarationError IO)
+        ImportIx
 usePendingFact
         (PendingCandidate premise certificate authorization)
         state = do
@@ -965,11 +1074,12 @@ usePendingFact
           && premiseStageValue == reservedStage premise
           && frontier <= reservedStage current
         )
-        (State.lift (Left PendingFactAuthorizationMismatch))
+        (State.lift
+            (Except.throwError PendingFactAuthorizationMismatch))
     unless
         (reservedStage premise < reservedStage current)
         (State.lift
-            (Left
+            (Except.throwError
                 (StagedPremiseNotEarlier
                     (reservedCandidateSlot premise)
                     (reservedCandidateStage premise)
@@ -984,7 +1094,10 @@ accumulateAuthorizedPremise
     :: CheckedPropositionContent
     -> FactAuthority
     -> CandidateProofState
-    -> StateT CandidateProofState (Either DeclarationError) ImportIx
+    -> StateT
+        CandidateProofState
+        (ExceptT DeclarationError IO)
+        ImportIx
 accumulateAuthorizedPremise proposition authority state = do
     let expected =
             theoremRef
@@ -993,18 +1106,22 @@ accumulateAuthorizedPremise proposition authority state = do
                 (checkedPropositionId proposition)
     safety <-
         State.lift
-            (first FactSafetyFailed
-                (accumulateFactSafety
-                    expected
-                    authority
-                    (candidateProofSafety state)))
+            (Except.liftEither
+                (first FactSafetyFailed
+                    (accumulateFactSafety
+                        expected
+                        authority
+                        (candidateProofSafety state))))
     State.put state{candidateProofSafety = safety}
     appendCandidatePremise proposition state{candidateProofSafety = safety}
 
 appendCandidatePremise
     :: CheckedPropositionContent
     -> CandidateProofState
-    -> StateT CandidateProofState (Either DeclarationError) ImportIx
+    -> StateT
+        CandidateProofState
+        (ExceptT DeclarationError IO)
+        ImportIx
 appendCandidatePremise proposition state = do
     let index = candidateProofPremiseCount state
     State.put
@@ -1117,45 +1234,41 @@ validateKernelConstruction descriptor proposition replayed proofState =
                 False
 
 
-validatePreparedVampire
+validatePreparedVampireProblem
     :: ReservedCandidate
     -> Provers.PreparedTypedProverTask
         SemanticFactOccurrenceFingerprint
         Void
         origin
         ObjectId
-    -> Provers.AcceptedVampireRun
     -> CandidateProofState
-    -> Either DeclarationError CandidateProofState
-validatePreparedVampire candidate prepared accepted initial = do
-    let request = Provers.preparedTypedProverRequest prepared
-        problem = Provers.preparedTypedProverLogicalProblem prepared
+    -> ExceptT DeclarationError IO CandidateProofState
+validatePreparedVampireProblem candidate prepared initial = do
+    let problem = Provers.preparedTypedProverLogicalProblem prepared
         claim = Backend.typedProblemClaim problem
         target = candidateCheckedProposition candidate
         builder = candidateProofBuilder initial
         closure = logicalBuilderObjectClosure builder
-    unless
-        (Provers.acceptedVampireRequest accepted == request)
-        (Left VampireRequestMismatch)
-    unless
-        ( Vector.null (Backend.supportedPropositionSupport claim)
-          && Backend.supportedPropositionTerm claim
-                == frozenCoreTerm (checkedPropositionTerm target)
-        )
-        (Left VampireTargetMismatch)
-    unless
-        (Vector.null (Backend.typedProblemLocalPremises problem))
-        (Left VampireLocalPremisesNotSupported)
-    traverse_
-        (\(identity, reportedType) ->
-            unless
-                (lookupCheckedObjectType identity closure
-                    == Just reportedType)
-                (Left (VampireGlobalTypeMismatch identity)))
-        (Map.toList (Backend.typedProblemGlobalTypes problem))
-    traverse_
-        (validateFoundationAuxiliary builder)
-        (Backend.typedProblemAuxiliaries problem)
+    Except.liftEither do
+        unless
+            ( Vector.null (Backend.supportedPropositionSupport claim)
+              && Backend.supportedPropositionTerm claim
+                    == frozenCoreTerm (checkedPropositionTerm target)
+            )
+            (Left VampireTargetMismatch)
+        unless
+            (Vector.null (Backend.typedProblemLocalPremises problem))
+            (Left VampireLocalPremisesNotSupported)
+        traverse_
+            (\(identity, reportedType) ->
+                unless
+                    (lookupCheckedObjectType identity closure
+                        == Just reportedType)
+                    (Left (VampireGlobalTypeMismatch identity)))
+            (Map.toList (Backend.typedProblemGlobalTypes problem))
+        traverse_
+            (validateFoundationAuxiliary builder)
+            (Backend.typedProblemAuxiliaries problem)
     execCandidateProof initial do
         traverse_
             validatePremise
@@ -1228,7 +1341,7 @@ validatePreparedVampire candidate prepared accepted initial = do
 execCandidateProof
     :: CandidateProofState
     -> CandidateProof value
-    -> Either DeclarationError CandidateProofState
+    -> ExceptT DeclarationError IO CandidateProofState
 execCandidateProof initial action =
     snd <$> State.runStateT (runCandidateProof action) initial
 
@@ -1236,7 +1349,7 @@ failCandidateProof
     :: DeclarationError
     -> CandidateProof value
 failCandidateProof =
-    CandidateProof . State.lift . Left
+    CandidateProof . State.lift . Except.throwError
 
 lookupAuthorizedProposition
     :: SemanticFactOccurrenceFingerprint
@@ -1285,10 +1398,16 @@ commitDeclaration
     -> ModuleDriver failure
         (value, CommittedDeclarationBatch)
 commitDeclaration mode action = ModuleDriver do
-    DriverState builder pendingPrefix <- State.get
+    DriverState resolver builder pendingPrefix <- State.get
     let
-        declaration = initialDeclarationState builder
-    case State.runStateT (runDeclaration action) declaration of
+        declaration = initialDeclarationState resolver builder
+    result <-
+        liftIO
+            (Except.runExceptT
+                (State.runStateT
+                    (runDeclaration action)
+                    declaration))
+    case result of
         Left err ->
             Except.throwError (DriverDeclarationFailed err)
         Right (value, prepared) ->
@@ -1298,13 +1417,18 @@ commitDeclaration mode action = ModuleDriver do
                 Right (builder', batch) ->
                     let prefix' = appendPendingBatch batch pendingPrefix
                     in do
-                        State.put (DriverState builder' prefix')
+                        State.put
+                            (DriverState resolver builder' prefix')
                         pure (value, batch)
 
-initialDeclarationState :: LogicalBuilder -> DeclarationState
-initialDeclarationState builder =
+initialDeclarationState
+    :: VampireResolver
+    -> LogicalBuilder
+    -> DeclarationState
+initialDeclarationState resolver builder =
     DeclarationState
-        { declarationBuilder = builder
+        { declarationVampireResolver = resolver
+        , declarationBuilder = builder
         , declarationOwnSlot =
             declarationSlot
                 (logicalBuilderOwner builder)
@@ -1440,7 +1564,7 @@ validatePendingAuthorization
     -> Either DeclarationError ()
 validatePendingAuthorization declaration
         (PendingCandidate candidate certificate authorization) = do
-    validateReservedCandidatePure declaration candidate
+    validateReservedCandidate declaration candidate
     let builder = declarationBuilder declaration
         PendingFactAuthorization
             identity prefix invocation slot authority stage frontier =
@@ -1456,17 +1580,6 @@ validatePendingAuthorization declaration
         )
         (Left PendingFactAuthorizationMismatch)
 
-validateReservedCandidatePure
-    :: DeclarationState
-    -> ReservedCandidate
-    -> Either DeclarationError ()
-validateReservedCandidatePure declaration candidate =
-    case State.runStateT
-            (validateReservedCandidate declaration candidate)
-            () of
-        Left err -> Left err
-        Right _ -> Right ()
-
 occurrenceFromPending
     :: PendingCandidate
     -> SemanticFactOccurrence
@@ -1681,6 +1794,9 @@ data DeclarationError
     | DerivationImportFailed !DerivationImportError
     | KernelCompletionFailed !KernelReplayError
     | KernelConstructionDescriptorMismatch
+    | VampireProcessFailed !Provers.ProverProcessError
+    | VampireObligationRejected !Provers.ProverAnswer
+    | VampireProofHasNoAcceptedObligations
     | VampireRequestMismatch
     | VampireTargetMismatch
     | VampireLocalPremisesNotSupported