Add warm proof validation lookup

2 files changed, 180 insertions, 6 deletions

diff --git a/source/Checking/Declaration.hs b/source/Checking/Declaration.hs
index 8e31b8d..ee1b38d 100644
--- a/source/Checking/Declaration.hs
+++ b/source/Checking/Declaration.hs
@@ -10,6 +10,10 @@ module Checking.Declaration
     , DriverFailure(..)
     , DriverResult(..)
     , runModuleDriver
+    , ProofValidationLookup
+    , proofValidationLookup
+    , ProofValidationRunMode(..)
+    , runModuleDriverWithValidation
     , failModuleDriver
     , VampireResolver
     , vampireResolver
@@ -34,6 +38,7 @@ module Checking.Declaration
     , authorizeKernelConstructionCandidate
     , acceptVampireObligation
     , acceptCachedVampireObligation
+    , lookupProofValidation
     , authorizeVampireCandidate
     , authorizeCachedVampireCandidate
     , authorizeSourceAxiomCandidate
@@ -100,6 +105,24 @@ newtype DeclarationInvocation = DeclarationInvocation Natural
 newtype CandidateStage = CandidateStage Natural
     deriving stock (Show, Eq, Ord)
 
+newtype ProofValidationLookup = ProofValidationLookup
+    { runProofValidationLookup
+        :: ProofValidationKey
+        -> IO (Either Text (Maybe ProofValidationRecord))
+    }
+
+proofValidationLookup
+    :: (ProofValidationKey
+        -> IO (Either Text (Maybe ProofValidationRecord)))
+    -> ProofValidationLookup
+proofValidationLookup =
+    ProofValidationLookup
+
+data ProofValidationRunMode
+    = FreshProofValidation
+    | WarmProofValidation
+    deriving stock (Show, Eq)
+
 
 data BuilderFactAuthorization = BuilderFactAuthorization
     !BuilderIdentity
@@ -321,6 +344,8 @@ data DriverState = DriverState
     !VampireResolver
     !LogicalBuilder
     !PendingModulePrefix
+    !(Maybe ProofValidationLookup)
+    !ProofValidationRunMode
 
 newtype ModuleDriver failure value = ModuleDriver
     { runDriverStep
@@ -371,6 +396,29 @@ runModuleDriver
             DriverOpenError
             (DriverResult failure value))
 runModuleDriver foundation owner direct resolver action = do
+    runModuleDriverWithValidation
+        foundation
+        owner
+        direct
+        resolver
+        Nothing
+        FreshProofValidation
+        action
+
+runModuleDriverWithValidation
+    :: CheckedFoundation
+    -> ModuleName
+    -> [SemanticInterfaceId]
+    -> VampireResolver
+    -> Maybe ProofValidationLookup
+    -> ProofValidationRunMode
+    -> ModuleDriver failure value
+    -> IO
+        (Either
+            DriverOpenError
+            (DriverResult failure value))
+runModuleDriverWithValidation
+        foundation owner direct resolver validationLookup validationMode action = do
     unique <- BuilderIdentity <$> newUnique
     let theory = theoryId foundation
     case (,) <$>
@@ -402,7 +450,9 @@ runModuleDriver foundation owner direct resolver action = do
                         resolver
                         builder
                         (PendingModulePrefix prefix [])
-            (result, DriverState _ finalBuilder finalPrefix) <-
+                        validationLookup
+                        validationMode
+            (result, DriverState _ finalBuilder finalPrefix _ _) <-
                 State.runStateT
                     (Except.runExceptT
                         (runDriverStep action))
@@ -494,6 +544,8 @@ data PendingCandidate = PendingCandidate
 
 data DeclarationState = DeclarationState
     { declarationVampireResolver :: !VampireResolver
+    , declarationProofValidationLookup :: !(Maybe ProofValidationLookup)
+    , declarationProofValidationMode :: !ProofValidationRunMode
     , declarationBuilder :: !LogicalBuilder
     , declarationOwnSlot :: !DeclarationSlot
     , declarationInvocation :: !DeclarationInvocation
@@ -598,7 +650,40 @@ reserveCandidateBatch specs = Declaration do
                     (declarationNextFact state + offset)))
             spec
 
-
+lookupProofValidation
+    :: ProofSyntaxId
+    -> ReservedCandidate
+    -> Declaration (Maybe ProofValidationRecord)
+lookupProofValidation syntax candidate = Declaration do
+    state <- State.get
+    case declarationProofValidationMode state of
+        FreshProofValidation ->
+            pure Nothing
+        WarmProofValidation ->
+            case declarationProofValidationLookup state of
+                Nothing ->
+                    pure Nothing
+                Just (ProofValidationLookup lookupRecord) -> do
+                    let builder = declarationBuilder state
+                        reference = candidateTheoremReference builder candidate
+                        key =
+                            proofValidationKey
+                                (theoremId
+                                    (factAuthorityTheorem
+                                        (factAuthority
+                                            reference
+                                            cleanAuthoritySafety)))
+                                syntax
+                                (logicalBuilderPrefix builder)
+                    result <- State.lift
+                        (liftIO (lookupRecord key))
+                    case result of
+                        Left reason ->
+                            State.lift
+                                (Except.throwError
+                                    (ProofValidationLookupFailed reason))
+                        Right record ->
+                            pure record
 data CandidatePremise = CandidatePremise
     !CheckedPropositionContent
 
@@ -1500,9 +1585,15 @@ commitDeclaration
     -> ModuleDriver failure
         (value, CommittedDeclarationBatch)
 commitDeclaration mode action = ModuleDriver do
-    DriverState resolver builder pendingPrefix <- State.get
+    DriverState resolver builder pendingPrefix validationLookup validationMode <-
+        State.get
     let
-        declaration = initialDeclarationState resolver builder
+        declaration =
+            initialDeclarationState
+                resolver
+                validationLookup
+                validationMode
+                builder
     result <-
         liftIO
             (Except.runExceptT
@@ -1520,16 +1611,25 @@ commitDeclaration mode action = ModuleDriver do
                     let prefix' = appendPendingBatch batch pendingPrefix
                     in do
                         State.put
-                            (DriverState resolver builder' prefix')
+                            (DriverState
+                                resolver
+                                builder'
+                                prefix'
+                                validationLookup
+                                validationMode)
                         pure (value, batch)
 
 initialDeclarationState
     :: VampireResolver
+    -> Maybe ProofValidationLookup
+    -> ProofValidationRunMode
     -> LogicalBuilder
     -> DeclarationState
-initialDeclarationState resolver builder =
+initialDeclarationState resolver validationLookup validationMode builder =
     DeclarationState
         { declarationVampireResolver = resolver
+        , declarationProofValidationLookup = validationLookup
+        , declarationProofValidationMode = validationMode
         , declarationBuilder = builder
         , declarationOwnSlot =
             declarationSlot
@@ -1901,6 +2001,7 @@ data DeclarationError
     | VampireFoundationMismatch !FoundationAxiomTag
     | CachedValidationMismatch
         !Materialization.MaterializationError
+    | ProofValidationLookupFailed !Text
     | DeclarationObjectAddedAfterAuthorization
     | DeclarationObjectValidationFailed !ObjectValidationError
     | DeclarationPropositionValidationFailed
@@ -1972,6 +2073,8 @@ renderDeclarationError = \case
         "Vampire request has inconsistent foundation axiom " <> shown tag
     CachedValidationMismatch{} ->
         "cached validation does not match the current declaration"
+    ProofValidationLookupFailed reason ->
+        "could not load cached proof validation: " <> reason
     DeclarationObjectAddedAfterAuthorization ->
         "the declaration added an object after candidate authorization"
     DeclarationObjectValidationFailed{} ->
diff --git a/source/Test/Unit/Declaration.hs b/source/Test/Unit/Declaration.hs
index 28f277d..16f4461 100644
--- a/source/Test/Unit/Declaration.hs
+++ b/source/Test/Unit/Declaration.hs
@@ -373,6 +373,46 @@ aggregatesExactVampireObligations =
                         ("unexpected cached validation records: "
                             <> show (length records)))
 
+        warmCalls <- IORef.newIORef (0 :: Int)
+        warm <- runSuccessfulWithValidation fixture
+            (Declaration.proofValidationLookup \_ -> do
+                IORef.modifyIORef' warmCalls (+ 1)
+                pure (Right (Just cachedRecord)))
+            do
+                (_value, committed) <- Declaration.commitProofDeclaration
+                    (Semantic.proofSyntaxId "two-vampire-obligations") do
+                        candidate <- Declaration.reserveCandidate
+                            (factSpec fixture "two-vampire-obligations")
+                        cached <- Declaration.lookupProofValidation
+                            (Semantic.proofSyntaxId "two-vampire-obligations")
+                            candidate
+                        case cached of
+                            Just record ->
+                                Declaration.authorizeCachedVampireCandidate
+                                    (Semantic.proofSyntaxId "two-vampire-obligations")
+                                    record
+                                    candidate do
+                                        Declaration.acceptCachedVampireObligation first
+                                        Declaration.acceptCachedVampireObligation second
+                            Nothing ->
+                                Declaration.failDeclaration
+                                    (Declaration.ProofValidationLookupFailed
+                                        "test cache miss")
+                pure committed
+        assertEqual "warm lookup executes once"
+            1
+            =<< IORef.readIORef warmCalls
+        assertEqual "warm path retains cached request IDs"
+            (Authority.CheckedSourceProof expectedRequests)
+            (case Declaration.committedBatchProofValidations warm of
+                [record] ->
+                    Authority.validationDirectAuthorization
+                        (Semantic.proofValidationRecordCertificate record)
+                records ->
+                    error
+                        ("unexpected warm validation records: "
+                            <> show (length records)))
+
         emptyProof <- runDriver fixture do
             Declaration.commitProofDeclaration
                 (Semantic.proofSyntaxId "empty-vampire-proof") do
@@ -776,6 +816,22 @@ runDriverWithResolver fixture resolver action = do
         action
     expectRight result
 
+runDriverWithValidation
+    :: Fixture
+    -> Declaration.ProofValidationLookup
+    -> Declaration.ModuleDriver failure value
+    -> IO (Declaration.DriverResult failure value)
+runDriverWithValidation fixture lookup action = do
+    result <- Declaration.runModuleDriverWithValidation
+        (fixtureFoundation fixture)
+        (fixtureOwner fixture)
+        []
+        unavailableVampireResolver
+        (Just lookup)
+        Declaration.WarmProofValidation
+        action
+    expectRight result
+
 unavailableVampireResolver :: Declaration.VampireResolver
 unavailableVampireResolver =
     Declaration.vampireResolver \_prepared ->
@@ -807,6 +863,21 @@ runSuccessfulWithResolver fixture resolver action = do
         Declaration.DriverSealFailed failure _prefix ->
             assertFailure (show failure) >> fail "unreachable"
 
+runSuccessfulWithValidation
+    :: Fixture
+    -> Declaration.ProofValidationLookup
+    -> Declaration.ModuleDriver failure value
+    -> IO value
+runSuccessfulWithValidation fixture lookup action = do
+    outcome <- runDriverWithValidation fixture lookup action
+    case outcome of
+        Declaration.DriverSucceeded value _interface _prefix ->
+            pure value
+        Declaration.DriverFailed _failure _prefix ->
+            assertFailure "unexpected driver failure" >> fail "unreachable"
+        Declaration.DriverSealFailed failure _prefix ->
+            assertFailure (show failure) >> fail "unreachable"
+
 requireSingleOccurrence
     :: Declaration.CommittedDeclarationBatch
     -> Declaration.ModuleDriver