diff options
Diffstat (limited to 'source/Felix/Verification.hs')
| -rw-r--r-- | source/Felix/Verification.hs | 1157 |
1 files changed, 1157 insertions, 0 deletions
diff --git a/source/Felix/Verification.hs b/source/Felix/Verification.hs new file mode 100644 index 0000000..716beea --- /dev/null +++ b/source/Felix/Verification.hs @@ -0,0 +1,1157 @@ +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE RankNTypes #-} + +module Felix.Verification + ( VerificationSession + , VerificationSessionError(..) + , withVerificationSession + , withVerificationSessionUsingStore + , CheckRequest(..) + , CheckOutcome(..) + , checkWorkspace + , StoreValidationMode(..) + , WorkPosition + , workPosition + , workPositionModuleOrdinal + , workPositionLocalRequestOrdinal + , VerificationRequestObserver + , verificationRequestObserver + , PreparedVerificationRequest + , SlowAtpOutcome(..) + , SlowAtpTask(..) + , SlowAtpReport(..) + , slowAtpOmittedTaskCount + , ProverAnswer + ( CounterSatisfiable + , ContradictoryAxioms + , Uncertain + , Error + ) + , pattern Yes + , VerificationResult(..) + , VerificationPresentation + , verificationHtmlPresentation + , ReportedEscapeKind(..) + , ReportedEscape(..) + , VerificationReport(..) + , VerificationDriverError(..) + , VerificationDriverErrorKind(..) + , verificationDriverErrorKind + , renderVerificationDriverError + , FailedVerification(..) + , VerificationFailureReason(..) + ) where + + +import Base +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Foundation qualified as Foundation +import Felix.Checking.Identity qualified as Identity +import Felix.Checking.Module qualified as Typed +import Felix.Checking.Semantic qualified as Semantic +import Felix.Module (localDeclarationOrdinal) +import Felix.Parse (ParseWorkspaceError(..), ParsedSourceWorkspace) +import Felix.Parse qualified as Felix +import Felix.Prelude qualified as Prelude +import Felix.Provers +import Felix.Source +import Felix.Source.Graph (ResolvedSourceGraph) +import Felix.Store qualified as Store +import Felix.Render.Html.Export qualified as HtmlExport +import Felix.Report.Location +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Interface qualified as Syntax + +import Control.Exception qualified as Exception +import Control.Monad (unless) +import Data.Bifunctor (first) +import Data.IORef (atomicModifyIORef', newIORef) +import Data.List.NonEmpty qualified as NonEmpty +import Data.Map.Strict qualified as Map +import Data.Text qualified as Text +import Numeric.Natural (Natural) +import UnliftIO.Async qualified as Async + +data VerificationResult + = VerificationCompleted + !VerificationReport + !VerificationPresentation + | CompletedWithExplicitGaps + !VerificationReport + !VerificationPresentation + | VerificationFailure !VerificationReport !FailedVerification + | VerificationCheckingFailure + !VerificationReport + !VerificationDriverError + deriving (Show) + +-- | Strict owner-independent source presentation retained only after the +-- complete typed workspace succeeds. +data VerificationPresentation = VerificationPresentation + !HtmlExport.HtmlPresentation + +instance Show VerificationPresentation where + show _presentation = + "VerificationPresentation <HTML presentation>" + +verificationHtmlPresentation + :: VerificationPresentation + -> HtmlExport.HtmlPresentation +verificationHtmlPresentation (VerificationPresentation presentation) = + presentation + +data ReportedEscapeKind + = ReportedSourceAxiom + | ReportedOmitted + deriving (Show, Eq) + +data ReportedEscape = ReportedEscape + { reportedEscapeKind :: !ReportedEscapeKind + , reportedEscapeLocation :: !Location + } + deriving (Show, Eq) + +data VerificationReport = VerificationReport + { verificationDirectEscapes :: ![ReportedEscape] + } + deriving (Show, Eq) + +newtype VerificationRequestObserver = VerificationRequestObserver + { observeVerificationRequest + :: WorkPosition + -> PreparedVerificationRequest + -> IO () + } + +verificationRequestObserver + :: (WorkPosition + -> PreparedVerificationRequest + -> IO ()) + -> VerificationRequestObserver +verificationRequestObserver = + VerificationRequestObserver + +data FailedVerification = FailedVerification + { failedVerificationLocation :: !Location + , failedVerificationReason :: !VerificationFailureReason + } + deriving (Show) + +data VerificationFailureReason + = CountermodelFailure !Text + | ContradictoryInputFailure !Text + | IndeterminateFailure !Text + | ProtocolFailure !Text !Text + | TransportFailure !ProverProcessError + deriving (Show) + +verificationFailureReason + :: Either ProverProcessError ProverAnswer + -> Maybe VerificationFailureReason +verificationFailureReason = \case + Left processError -> + Just (TransportFailure processError) + Right Yes -> + Nothing + Right (CounterSatisfiable tptp) -> + Just (CountermodelFailure tptp) + Right (ContradictoryAxioms tptp) -> + Just (ContradictoryInputFailure tptp) + Right (Uncertain tptp) -> + Just (IndeterminateFailure tptp) + Right (Error taskLabel message) -> + Just (ProtocolFailure taskLabel message) + +data VerificationDriverError + = VerificationWorkspaceError + !ParseWorkspaceError + | VerificationMissingImportedModule + !ResolvedSourceAddress + | VerificationMissingRootModule + !ResolvedSourceAddress + | VerificationFinalPreludeReadinessError + !Typed.FinalPreludeReadinessError + | VerificationTypedInputError + !ResolvedSource + !Typed.TypedModuleInputError + | VerificationTypedOpenError + !ResolvedSource + !Declaration.DriverOpenError + | VerificationTypedCachedModuleError + !ResolvedSource + !Typed.CachedTypedModuleError + | VerificationTypedModuleError + !ResolvedSource + !Typed.TypedModuleFailure + !Declaration.PendingModulePrefix + | VerificationValidationIntegrityError + !ResolvedSource + !Declaration.ValidationIntegrityError + | VerificationAdmittedViewError + !ResolvedSource + !AdmittedViewError + | VerificationParsedArtifactIntegrityError + !ResolvedSource + !Felix.ParsedArtifactIntegrityError + | VerificationStoreFailure !Store.StoreFailure + | VerificationModuleArtifactKeyError !Semantic.ModuleArtifactKeyError + | VerificationModuleSchedulerInvariant !Text + deriving (Show) + +instance Exception.Exception VerificationDriverError + +data VerificationDriverErrorKind + = VerificationSourceFailure + | VerificationInfrastructureFailure + deriving (Show, Eq) + +verificationDriverErrorKind + :: VerificationDriverError + -> VerificationDriverErrorKind +verificationDriverErrorKind = \case + VerificationWorkspaceError{} -> VerificationSourceFailure + VerificationTypedInputError{} -> VerificationSourceFailure + VerificationTypedModuleError _source failure _prefix -> + case failure of + Typed.TypedActionFailed{} -> VerificationSourceFailure + _ -> VerificationInfrastructureFailure + VerificationMissingImportedModule{} -> VerificationInfrastructureFailure + VerificationMissingRootModule{} -> VerificationInfrastructureFailure + VerificationFinalPreludeReadinessError{} -> + VerificationInfrastructureFailure + VerificationTypedOpenError{} -> VerificationInfrastructureFailure + VerificationTypedCachedModuleError{} -> VerificationInfrastructureFailure + VerificationValidationIntegrityError{} -> + VerificationInfrastructureFailure + VerificationAdmittedViewError{} -> VerificationInfrastructureFailure + VerificationParsedArtifactIntegrityError{} -> + VerificationInfrastructureFailure + VerificationStoreFailure{} -> VerificationInfrastructureFailure + VerificationModuleArtifactKeyError{} -> + VerificationInfrastructureFailure + VerificationModuleSchedulerInvariant{} -> + VerificationInfrastructureFailure + +renderVerificationDriverError :: VerificationDriverError -> Text +renderVerificationDriverError = \case + VerificationWorkspaceError failure -> + "Verification input failed: " + <> Felix.renderParseWorkspaceError failure + VerificationTypedInputError source failure -> + "Typed module input failed in " + <> resolvedSourceDisplay source + <> ": " <> Typed.renderTypedModuleInputError failure + VerificationTypedOpenError source failure -> + "Typed module startup failed in " + <> resolvedSourceDisplay source + <> ": " <> Declaration.renderDriverOpenError failure + VerificationTypedCachedModuleError source failure -> + "Cached typed module is invalid in " + <> resolvedSourceDisplay source + <> ": " <> Typed.renderCachedTypedModuleError failure + VerificationTypedModuleError source failure _prefix -> + "Typed module checking failed in " + <> resolvedSourceDisplay source + <> ": " <> Typed.renderTypedModuleFailure failure + VerificationValidationIntegrityError source failure -> + "Typed module validation store is inconsistent in " + <> resolvedSourceDisplay source + <> ": " <> Declaration.renderValidationIntegrityError failure + VerificationAdmittedViewError source failure -> + "Typed admitted-source association is inconsistent in " + <> resolvedSourceDisplay source + <> ": " <> Text.pack (show failure) + VerificationParsedArtifactIntegrityError source failure -> + "Parsed artifact is inconsistent in " + <> resolvedSourceDisplay source + <> ": " <> Text.pack (show failure) + VerificationStoreFailure failure -> + "Verification store failed: " <> Store.renderStoreFailure failure + VerificationModuleArtifactKeyError{} -> + "Typed module artifact inputs are inconsistent." + VerificationModuleSchedulerInvariant message -> + "Typed module scheduler invariant failed: " <> message + VerificationMissingImportedModule address -> + "Verification could not find checked imported module " + <> Text.pack (show address) <> "." + VerificationMissingRootModule address -> + "Verification could not find checked root module " + <> Text.pack (show address) <> "." + VerificationFinalPreludeReadinessError{} -> + "The packaged final prelude failed." + +resolvedSourceDisplay :: ResolvedSource -> Text +resolvedSourceDisplay source = + sourceMountIdText (resolvedSourceMount source) + <> ":" + <> Text.pack (resolvedSourceLocationPath source) + +data TypedWorkspaceOutcome + = TypedWorkspaceSucceeded + !AdmittedTypedWorkspace + | TypedWorkspaceRejected + !AdmittedTypedWorkspace + !TypedWorkspaceFailure + +data TypedWorkspaceFailure + = TypedWorkspaceCheckingRejected !VerificationDriverError + | TypedWorkspaceProverRejected !FailedVerification + +data ModuleTask = ModuleTask + { moduleTaskOrdinal :: !Natural + , moduleTaskParsed :: !Felix.ParsedModule + , moduleTaskDirectAddresses :: ![ResolvedSourceAddress] + } + +data ModuleCheckResult + = ModuleCheckSucceeded + !ResolvedSourceAddress + !Typed.SealedTypedModule + !AdmittedTypedModule + | ModuleCheckRejected + !AdmittedTypedModule + !TypedWorkspaceFailure + +data ModuleFailureCandidate = ModuleFailureCandidate + !Natural + !AdmittedTypedModule + !TypedWorkspaceFailure + +data AdmittedTypedDeclaration = AdmittedTypedDeclaration + !Semantic.DeclarationSlot + !Typed.TypedSourceDeclaration + +newtype AdmittedTypedModule = AdmittedTypedModule + [AdmittedTypedDeclaration] + +newtype AdmittedTypedWorkspace = AdmittedTypedWorkspace + [AdmittedTypedModule] + +data AdmittedViewError + = AdmittedDeclarationCountMismatch + !Int + !Int + | AdmittedDeclarationSlotMismatch + ![Semantic.DeclarationSlot] + ![Semantic.DeclarationSlot] + deriving (Show, Eq) + +completeAdmittedModule + :: Typed.IdentifiedModuleInput + -> AdmittedTypedModule +completeAdmittedModule input = + AdmittedTypedModule + (uncurry AdmittedTypedDeclaration <$> expectedDeclarations input) + +checkedAdmittedModule + :: Bool + -> Typed.IdentifiedModuleInput + -> Declaration.PendingModulePrefix + -> Either AdmittedViewError AdmittedTypedModule +checkedAdmittedModule requireComplete input prefix = do + let expected = expectedDeclarations input + expectedSlots = fst <$> expected + actualSlots = + Declaration.committedBatchSlot + <$> Declaration.pendingModulePrefixBatches prefix + admittedCount = length actualSlots + if requireComplete + then unless + (admittedCount == length expected) + (Left + (AdmittedDeclarationCountMismatch + (length expected) + admittedCount)) + else unless + (admittedCount <= length expected) + (Left + (AdmittedDeclarationCountMismatch + (length expected) + admittedCount)) + unless + (actualSlots == take admittedCount expectedSlots) + (Left + (AdmittedDeclarationSlotMismatch + (take admittedCount expectedSlots) + actualSlots)) + pure + (AdmittedTypedModule + [ AdmittedTypedDeclaration slot declaration + | (slot, declaration) <- take admittedCount expected + ]) + +expectedDeclarations + :: Typed.IdentifiedModuleInput + -> [(Semantic.DeclarationSlot, Typed.TypedSourceDeclaration)] +expectedDeclarations input = + zipWith + (\ordinal declaration -> + ( Semantic.declarationSlot + (Typed.identifiedModuleOwner input) + (localDeclarationOrdinal ordinal) + , declaration + )) + [0..] + (Typed.typedSourceDeclarations + (Typed.identifiedModuleParsed input)) + +data StoreValidationMode + = FreshStoreValidation + | WarmStoreValidation + deriving (Show, Eq) + +data VerificationSession = VerificationSession + !Foundation.CheckedFoundation + !Store.Store + +data VerificationSessionError + = VerificationSessionFoundationError + !(NonEmpty Foundation.FoundationManifestError) + | VerificationSessionStoreError !Store.StoreLifecycleError + | VerificationSessionTheoryMismatch !Identity.TheoryId !Identity.TheoryId + deriving (Show) + +withVerificationSession + :: Store.StoreLease + -> (VerificationSession -> IO value) + -> IO (Either VerificationSessionError value) +withVerificationSession lease action = + case Foundation.checkedFoundation of + Left failure -> + pure (Left (VerificationSessionFoundationError failure)) + Right foundation -> do + opened <- Store.withOpenStore + lease + (Identity.theoryId foundation) + (\_startup store -> + action (VerificationSession foundation store)) + pure (first VerificationSessionStoreError opened) + +-- | Borrow an already-open store while preserving the session's +-- foundation/store identity invariant. The caller retains ownership of the +-- store lifetime; ordinary hosts should prefer 'withVerificationSession'. +withVerificationSessionUsingStore + :: Store.Store + -> (VerificationSession -> IO value) + -> IO (Either VerificationSessionError value) +withVerificationSessionUsingStore store action = + case Foundation.checkedFoundation of + Left failure -> + pure (Left (VerificationSessionFoundationError failure)) + Right foundation -> + let expected = Identity.theoryId foundation + actual = Store.storeTheoryId store + in if expected == actual + then Right <$> action (VerificationSession foundation store) + else pure + (Left + (VerificationSessionTheoryMismatch expected actual)) + +data CheckRequest = CheckRequest + { checkSourceGraph :: !ResolvedSourceGraph + , checkStoreValidationMode :: !StoreValidationMode + , checkEffectiveJobs :: !EffectiveJobs + , checkVampire :: !Vampire + , checkRequestObserver :: !VerificationRequestObserver + } + +data CheckOutcome = CheckOutcome + { checkVerificationResult :: !VerificationResult + , checkSlowAtpReport :: !SlowAtpReport + } + deriving (Show) + +checkWorkspace + :: VerificationSession + -> CheckRequest + -> IO (Either VerificationDriverError CheckOutcome) +checkWorkspace session request = + Exception.try (checkWorkspaceThrowing session request) + +checkWorkspaceThrowing + :: VerificationSession + -> CheckRequest + -> IO CheckOutcome +checkWorkspaceThrowing + (VerificationSession foundation store) + request = do + memo <- Store.newStoreMemo store + storeCoordinator <- Store.newStoreCoordinator + withVampireExecutor + (checkEffectiveJobs request) + (checkVampire request) + (observeVerificationRequest (checkRequestObserver request)) + \executor -> do + prelude <- withVampireRequestOwner executor \owner -> do + preludeResolver <- typedVampireResolver owner 0 + Typed.acquireFinalPreludeSession + memo store foundation preludeResolver + >>= either + (throwIO . VerificationFinalPreludeReadinessError) + pure + let preludeSyntax = + Typed.sealedTypedModuleSyntax + (Typed.finalPreludeModule prelude) + syntaxInputs _source = [preludeSyntax] + parsed <- + Felix.parseResolvedSourceGraphWithStoreAndSyntaxInputsAndGraphValidation + store + (checkSourceGraph request) + syntaxInputs + (Prelude.rejectOrdinaryPreludeSourceGraph + (Typed.finalPreludeSource prelude)) + >>= either throwParseExecutionError pure + admittedResult <- + checkTypedWorkspace + memo + storeCoordinator + foundation + prelude + executor + (checkEffectiveJobs request) + (checkStoreValidationMode request) + parsed + store + slowReport <- vampireExecutorSlowAtpReport executor + let result = + case admittedResult of + TypedWorkspaceRejected admitted failure -> + let report = admittedWorkspaceReport admitted + in case failure of + TypedWorkspaceCheckingRejected checkingFailure -> + VerificationCheckingFailure + report checkingFailure + TypedWorkspaceProverRejected proverFailure -> + VerificationFailure report proverFailure + TypedWorkspaceSucceeded admitted -> + completedResult + (admittedWorkspaceReport admitted) + (VerificationPresentation + (HtmlExport.htmlPresentationFromParsedWorkspace + parsed)) + pure (CheckOutcome result slowReport) + where + throwParseExecutionError = \case + Felix.ParseExecutionWorkspaceError failure -> + throwIO (VerificationWorkspaceError failure) + Felix.ParseExecutionStoreFailure failure -> + throwIO (VerificationStoreFailure failure) + Felix.ParseExecutionArtifactIntegrityFailure source failure -> + throwIO + (VerificationParsedArtifactIntegrityError source failure) + +checkTypedWorkspace + :: Store.StoreMemo + -> Store.StoreCoordinator + -> Foundation.CheckedFoundation + -> Typed.FinalPreludeSession + -> VampireExecutor + -> EffectiveJobs + -> StoreValidationMode + -> ParsedSourceWorkspace + -> Store.Store + -> IO TypedWorkspaceOutcome +checkTypedWorkspace + memo + storeCoordinator + foundation + prelude + executor + selectedJobs + validationMode + workspace + store = do + let modules = + zipWith + makeTask + [1..] + (toList + (Felix.parsedWorkspaceImportedBeforeImporter workspace)) + rootAddress = + Felix.parsedModuleAddress + (Felix.parsedWorkspaceRootModule workspace) + scheduleModules + rootAddress + modules + Map.empty + Map.empty + Map.empty + Nothing + where + workerBound = effectiveJobsValue selectedJobs + + makeTask ordinal parsed = + ModuleTask + { moduleTaskOrdinal = ordinal + , moduleTaskParsed = parsed + , moduleTaskDirectAddresses = + nubOrd + (Felix.parsedImportedAddress + <$> Felix.parsedModuleImports parsed) + } + + scheduleModules + rootAddress + pending + running + sealedByAddress + admittedByOrdinal + candidate = do + (pending', running') <- + startReadyModules + pending + running + sealedByAddress + candidate + Exception.onException + (if Map.null running' + then case candidate of + Just selected + | any + (\task -> + moduleTaskOrdinal task + < candidateOrdinal selected) + pending' -> + throwIO + (VerificationModuleSchedulerInvariant + "an earlier module is not terminal") + | otherwise -> + pure + (TypedWorkspaceRejected + (admittedWorkspaceThrough + admittedByOrdinal + selected) + (candidateFailure selected)) + Nothing + | null pending' -> do + unless + (Map.member rootAddress sealedByAddress) + (throwIO + (VerificationMissingRootModule + rootAddress)) + pure + (TypedWorkspaceSucceeded + (completeAdmittedWorkspace + admittedByOrdinal)) + | otherwise -> + throwIO + (VerificationModuleSchedulerInvariant + "no ready module and no running module") + else do + (_completedAsync, (ordinal, completed)) <- + Async.waitAny (Map.elems running') + let runningWithoutCompleted = + Map.delete ordinal running' + case completed of + Left fatal -> do + cancelModuleCheckers runningWithoutCompleted + Exception.throwIO fatal + Right (ModuleCheckSucceeded + address sealed admittedModule) -> + scheduleModules + rootAddress + pending' + runningWithoutCompleted + (Map.insert address sealed sealedByAddress) + (Map.insert + ordinal + admittedModule + admittedByOrdinal) + candidate + Right (ModuleCheckRejected + admittedModule failure) -> do + let selected = + chooseEarlierFailure + candidate + (ModuleFailureCandidate + ordinal + admittedModule + failure) + cutoff = candidateOrdinal selected + (later, retained) = + Map.partitionWithKey + (\runningOrdinal _async -> + runningOrdinal > cutoff) + runningWithoutCompleted + cancelModuleCheckers later + scheduleModules + rootAddress + pending' + retained + sealedByAddress + admittedByOrdinal + (Just selected) + ) + (cancelModuleCheckers running') + + startReadyModules + pending + running + sealedByAddress + candidate + | Map.size running >= workerBound = + pure (pending, running) + | otherwise = + case extractFirstReady candidate sealedByAddress pending of + Nothing -> + pure (pending, running) + Just (task, remaining) -> do + checker <- Async.async do + completed <- + (Exception.try + (checkModule task sealedByAddress) + :: IO + (Either + Exception.SomeException + ModuleCheckResult)) + pure (moduleTaskOrdinal task, completed) + startReadyModules + remaining + (Map.insert + (moduleTaskOrdinal task) + checker + running) + sealedByAddress + candidate + + checkModule task sealedByAddress = + withVampireRequestOwner executor \requestOwner -> do + let parsed = moduleTaskParsed task + source = Felix.parsedModuleResolved parsed + address = Felix.parsedModuleAddress parsed + direct <- + traverse + (\directAddress -> + maybe + (throwIO + (VerificationMissingImportedModule + directAddress)) + pure + (Map.lookup directAddress sealedByAddress)) + (moduleTaskDirectAddresses task) + resolver <- + typedVampireResolver + requestOwner + (moduleTaskOrdinal task) + input <- + either + (throwIO . VerificationTypedInputError source) + pure + (Typed.typedModuleInput + foundation + (Typed.finalPreludeReadiness prelude) + resolver + validationRun + parsed + direct) + loadCachedModule parsed direct >>= \case + Just sealed -> do + pure + (ModuleCheckSucceeded + address + sealed + (completeAdmittedModule + (Typed.identifiedPhysicalModule parsed))) + Nothing -> do + typedResult <- + Exception.catch + (Typed.runTypedModule input) + (\failure -> + throwIO + (VerificationValidationIntegrityError + source + failure)) + case typedResult of + Typed.TypedModuleOpenFailed err -> + throwIO (VerificationTypedOpenError source err) + Typed.TypedModuleFailed err prefix -> do + let driverFailure = + VerificationTypedModuleError + source err prefix + case classifyTypedModuleFailure err of + TypedIntegrityFailure -> + throwIO driverFailure + TypedCheckingRejection -> + reportFailure + parsed + prefix + (TypedWorkspaceCheckingRejected + driverFailure) + TypedVerificationRejection failed -> + reportFailure + parsed + prefix + (TypedWorkspaceProverRejected failed) + TypedProverFailure failed -> + reportFailure + parsed + prefix + (TypedWorkspaceProverRejected failed) + Typed.TypedModuleSucceeded sealed -> do + admittedModule <- + either + (throwIO + . VerificationAdmittedViewError source) + pure + (checkedAdmittedModule + True + (Typed.identifiedPhysicalModule parsed) + (Typed.sealedTypedModulePrefix sealed)) + persistSealed + (Typed.identifiedPhysicalModule parsed) + sealed + pure + (ModuleCheckSucceeded + address sealed admittedModule) + + reportFailure parsed prefix failure = do + let source = Felix.parsedModuleResolved parsed + admittedModule <- + either + (throwIO . VerificationAdmittedViewError source) + pure + (checkedAdmittedModule + False + (Typed.identifiedPhysicalModule parsed) + prefix) + Store.withStoreCoordinator storeCoordinator + (Store.writePendingModulePrefix store prefix) + >>= either + (throwIO . VerificationStoreFailure) + pure + pure (ModuleCheckRejected admittedModule failure) + + storeValidationLookup lookupStore = + Declaration.validationLookup + (\key -> + Store.withStoreCoordinator storeCoordinator + (Store.loadProofValidation lookupStore key) + >>= either + (throwIO . VerificationStoreFailure) + pure) + (\key -> + Store.withStoreCoordinator storeCoordinator + (Store.loadDeclarationValidation lookupStore key) + >>= either + (throwIO . VerificationStoreFailure) + pure) + + validationRun = + case validationMode of + FreshStoreValidation -> + Declaration.FreshValidation + WarmStoreValidation -> + Declaration.WarmValidation + (storeValidationLookup store) + + persistSealed input sealed = do + artifactKey <- + either + (throwIO . VerificationModuleArtifactKeyError) + pure + (Semantic.moduleArtifactKey + (Typed.identifiedModuleOwner input) + (Felix.identifiedParsedModuleId + (Typed.identifiedModuleParsed input)) + (Semantic.semanticInterfaceDirectInputs + (Typed.sealedTypedModuleSemantic sealed)) + (Identity.theoryId foundation)) + let artifact = + Semantic.moduleArtifactResult + artifactKey + (Syntax.moduleSyntaxAssertedId + (Typed.sealedTypedModuleSyntax sealed)) + (Semantic.semanticInterfaceAssertedId + (Typed.sealedTypedModuleSemantic sealed)) + acknowledged <- + Store.withStoreCoordinator storeCoordinator + (Store.writeSealedModule + store + (Typed.sealedTypedModulePrefix sealed) + [Typed.sealedTypedModuleSyntax sealed] + [Typed.sealedTypedModuleSemantic sealed] + artifact) + >>= either + (throwIO . VerificationStoreFailure) + pure + unless + (acknowledged == artifact) + (throwIO + (VerificationStoreFailure + Store.StoreModuleArtifactIdMismatch)) + + loadCachedModule parsed direct = + case validationMode of + WarmStoreValidation -> do + let owner = + Typed.identifiedModuleOwner + (Typed.identifiedPhysicalModule parsed) + directSemantic = + Semantic.semanticInterfaceAssertedId + (Typed.sealedTypedModuleSemantic + (Typed.finalPreludeModule prelude)) + : ( Semantic.semanticInterfaceAssertedId + . Typed.sealedTypedModuleSemantic + <$> direct + ) + artifactKey <- + either + (throwIO . VerificationModuleArtifactKeyError) + pure + (Semantic.moduleArtifactKey + owner + (Felix.identifiedParsedModuleId + (Typed.identifiedModuleParsed + (Typed.identifiedPhysicalModule parsed))) + directSemantic + (Identity.theoryId foundation)) + loaded <- + Store.withStoreCoordinator storeCoordinator + (Store.loadCachedModuleInstallation + memo + store + artifactKey + (Syntax.moduleSyntaxAssertedId + (Felix.parsedModuleSyntaxInterface parsed))) + case loaded of + Left failure -> + throwIO (VerificationStoreFailure failure) + Right Nothing -> + pure Nothing + Right (Just installation) -> + either + (throwIO + . VerificationTypedCachedModuleError + (Felix.parsedModuleResolved parsed)) + (pure . Just) + (Typed.cachedSealedTypedModule + foundation + (Typed.finalPreludeModule prelude : direct) + installation) + FreshStoreValidation -> + pure Nothing + + taskMayStart candidate sealedByAddress task = + maybe True + (moduleTaskOrdinal task <) + (candidateOrdinal <$> candidate) + && all + (`Map.member` sealedByAddress) + (moduleTaskDirectAddresses task) + + extractFirstReady candidate sealedByAddress = go [] + where + go _before [] = Nothing + go before (task : after) + | taskMayStart candidate sealedByAddress task = + Just (task, reverse before <> after) + | otherwise = + go (task : before) after + + chooseEarlierFailure Nothing incoming = incoming + chooseEarlierFailure (Just current) incoming + | candidateOrdinal incoming < candidateOrdinal current = incoming + | otherwise = current + + candidateOrdinal (ModuleFailureCandidate ordinal _admitted _failure) = + ordinal + + candidateFailure (ModuleFailureCandidate _ordinal _admitted failure) = + failure + + candidateAdmitted (ModuleFailureCandidate _ordinal admitted _failure) = + admitted + + completeAdmittedWorkspace admittedByOrdinal = + AdmittedTypedWorkspace + ( completeAdmittedModule (Typed.finalPreludeInput prelude) + : fmap snd (Map.toAscList admittedByOrdinal) + ) + + admittedWorkspaceThrough admittedByOrdinal selected = + let cutoff = candidateOrdinal selected + earlier = Map.filterWithKey + (\ordinal _admitted -> ordinal < cutoff) + admittedByOrdinal + in AdmittedTypedWorkspace + ( completeAdmittedModule (Typed.finalPreludeInput prelude) + : ( fmap snd (Map.toAscList earlier) + <> [candidateAdmitted selected] + ) + ) + + cancelModuleCheckers running = do + traverse_ Async.cancel (Map.elems running) + traverse_ Async.waitCatch (Map.elems running) + +data TypedFailureClassification + = TypedCheckingRejection + | TypedVerificationRejection !FailedVerification + | TypedProverFailure !FailedVerification + | TypedIntegrityFailure + +-- | Classify failures at the typed checking boundary conservatively. +-- +-- Only source elaboration and recognized prover outcomes may retain an +-- admitted source report. Every declaration/sealing invariant, including a +-- future constructor not explicitly recognized below, remains fatal. +classifyTypedModuleFailure + :: Typed.TypedModuleFailure + -> TypedFailureClassification +classifyTypedModuleFailure = \case + Typed.TypedActionFailed{} -> + TypedCheckingRejection + Typed.TypedDeclarationFailed + (Declaration.ProofObligationFailedAt + location + (Declaration.VampireProcessFailed processError)) -> + classifyTypedProverResult location (Left processError) + Typed.TypedDeclarationFailed + (Declaration.ProofObligationFailedAt + location + (Declaration.VampireObligationRejected answer)) -> + classifyTypedProverResult location (Right answer) + _failure -> + TypedIntegrityFailure + +classifyTypedProverResult + :: Location + -> Either ProverProcessError ProverAnswer + -> TypedFailureClassification +classifyTypedProverResult location result = + case verificationFailureReason result of + Nothing -> + TypedIntegrityFailure + Just reason -> + let failed = FailedVerification location reason + in case reason of + CountermodelFailure{} -> + TypedVerificationRejection failed + ContradictoryInputFailure{} -> + TypedVerificationRejection failed + IndeterminateFailure{} -> + TypedProverFailure failed + ProtocolFailure{} -> + TypedProverFailure failed + TransportFailure{} -> + TypedProverFailure failed + +typedVampireResolver + :: VampireRequestOwner + -> Natural + -> IO Declaration.VampireResolver +typedVampireResolver + requestOwner moduleOrdinal = do + localOrdinalRef <- newIORef 1 + let reserve requests = do + let batchSize = NonEmpty.length requests + ordinalCount = fromIntegral batchSize + firstOrdinal <- atomicModifyIORef' localOrdinalRef + (\current -> (current + ordinalCount, current)) + let positions = + NonEmpty.fromList + [ workPosition moduleOrdinal ordinal + | ordinal <- + [firstOrdinal .. firstOrdinal + ordinalCount - 1] + ] + pure positions + submit requests = do + positions <- reserve requests + traverse + (\(position, Declaration.VampireSubmission location request) -> + submitVampireRequest + requestOwner position location request) + (NonEmpty.zip positions requests) + pure (Declaration.vampireSubmissionResolver submit) + +admittedWorkspaceReport + :: AdmittedTypedWorkspace + -> VerificationReport +admittedWorkspaceReport (AdmittedTypedWorkspace modules) = + VerificationReport + { verificationDirectEscapes = + concatMap admittedModuleEscapes modules + } + +admittedModuleEscapes + :: AdmittedTypedModule + -> [ReportedEscape] +admittedModuleEscapes (AdmittedTypedModule declarations) = + concatMap admittedDeclarationEscapes declarations + +admittedDeclarationEscapes + :: AdmittedTypedDeclaration + -> [ReportedEscape] +admittedDeclarationEscapes + (AdmittedTypedDeclaration _slot declaration) = + axiomEscape <> proofEscapes + where + axiomEscape = + case Typed.typedSourceDeclarationHead declaration of + Raw.BlockAxiom location _title _marker _axiom -> + [ReportedEscape ReportedSourceAxiom location] + _ -> + [] + proofEscapes = + maybe [] omittedProofEscapes + (Typed.typedSourceDeclarationProof declaration) + +omittedProofEscapes :: Raw.Proof -> [ReportedEscape] +omittedProofEscapes = \case + Raw.Omitted location -> + [ReportedEscape ReportedOmitted location] + Raw.Qed{} -> + [] + Raw.Contradiction{} -> + [] + Raw.ByCase _location cases -> + concatMap (omittedProofEscapes . Raw.caseProof) cases + Raw.ByContradiction _location proof -> + omittedProofEscapes proof + Raw.BySetInduction _location _term proof -> + omittedProofEscapes proof + Raw.ByOrdInduction _location proof -> + omittedProofEscapes proof + Raw.Assume _location _statement proof -> + omittedProofEscapes proof + Raw.FixSymbolic _location _variables _bound proof -> + omittedProofEscapes proof + Raw.FixSuchThat _location _variables _statement proof -> + omittedProofEscapes proof + Raw.Calc _location _quantifier _calculation proof -> + omittedProofEscapes proof + Raw.TakeVar _location _variables _bound _statement _justification proof -> + omittedProofEscapes proof + Raw.TakeNoun _location _noun _justification proof -> + omittedProofEscapes proof + Raw.Have _location _condition _statement _justification proof -> + omittedProofEscapes proof + Raw.Suffices _location _statement _justification proof -> + omittedProofEscapes proof + Raw.Subclaim _location _statement subproof continuation -> + omittedProofEscapes subproof <> omittedProofEscapes continuation + Raw.Define _location _variable _expression proof -> + omittedProofEscapes proof + Raw.DefineFunction + _location _function _argument _value _domainVariable _domain + proof -> + omittedProofEscapes proof + Raw.DefineFunctionLocal + _location _function _argument _domain _target _ruleVariable + _rules proof -> + omittedProofEscapes proof + +completedResult + :: VerificationReport + -> VerificationPresentation + -> VerificationResult +completedResult report presentation + | any ((== ReportedOmitted) . reportedEscapeKind) + (verificationDirectEscapes report) = + CompletedWithExplicitGaps report presentation + | otherwise = + VerificationCompleted report presentation |