{-# 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 " 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