diff options
Diffstat (limited to 'source/Checking/Declaration.hs')
| -rw-r--r-- | source/Checking/Declaration.hs | 115 |
1 files changed, 109 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{} -> |