diff options
Diffstat (limited to 'source/Api.hs')
| -rw-r--r-- | source/Api.hs | 2074 |
1 files changed, 1053 insertions, 1021 deletions
diff --git a/source/Api.hs b/source/Api.hs index 430eb41..2220434 100644 --- a/source/Api.hs +++ b/source/Api.hs @@ -10,17 +10,21 @@ module Api , scan , parse , parseWorkspace + , AuthorityFreeParseError(..) + , renderAuthorityFreeParseError , simpleStream , builtins , ParseException(..) - , gloss, GlossError(..) - , generateTasks - , encodeTasks , verify, verifyMeasured , verifyWithObserverAndStoreMode + , verifyMeasuredWithObserverAndStoreMode + , verifyWithObserverAndStoreModeAndJobs + , verifyMeasuredWithObserverAndStoreModeAndJobs , StoreValidationMode(..) - , VerificationRequestOrdinal - , verificationRequestOrdinalValue + , WorkPosition + , workPosition + , workPositionModuleOrdinal + , workPositionLocalRequestOrdinal , VerificationRequestObserver , verificationRequestObserver , ProverAnswer @@ -31,69 +35,58 @@ module Api ) , pattern Yes , VerificationResult(..) - , VerificationRoute(..) + , VerificationPresentation + , ReportedEscapeKind(..) + , ReportedEscape(..) , VerificationReport(..) , VerificationMeasurements(..) , VerificationDriverError(..) , FailedVerification(..) , VerificationFailureReason(..) - , exportHtml - , prepareHtmlExport - , prepareHtmlExportResult + , prepareVerifiedHtmlExportResult , prepareDefaultSourceGraph , defaultHtmlMountPrefixes ) where import Base -import Checking import Checking.Declaration qualified as Declaration import Checking.Foundation qualified as Foundation import Checking.Identity qualified as Identity -import Checking.Legacy qualified as Legacy import Checking.Module qualified as Typed -import Checking.Obligation import Checking.Semantic qualified as Semantic -import Checking.Transition qualified as Transition -import Encoding -import Felix.Migration qualified as Migration +import Felix.Module (localDeclarationOrdinal) import Felix.Parse (ParseException(..), ParseWorkspaceError(..), ParsedSourceWorkspace) import Felix.Parse qualified as Felix +import Felix.Prelude qualified as Prelude import Felix.Source import Felix.Store qualified as Store import Felix.Source.Graph (ResolvedSourceGraph) import Felix.Source.Graph qualified as SourceGraph -import Meaning - ( GlossError(..) - , meaning - ) import Provers import Render.Html.Export qualified as HtmlExport -import Render.Html.Output (PreparedHtmlBundle) +import Render.Html.Output (PreparedHtmlArtifact) import Report.Location import Syntax.Abstract qualified as Raw import Syntax.Adapt (scanChunk, ScannedLexicalItem) -import Syntax.Internal qualified as Internal import Syntax.Interface qualified as Syntax import Syntax.Lexicon (builtins) import Syntax.Token -import Tptp.UnsortedFirstOrder qualified as Tptp import Control.Exception qualified as Exception import Control.Monad.Logger -import Control.Monad (foldM, unless) +import Control.Monad (unless) import Data.Bifunctor (first) import Data.List.NonEmpty qualified as NonEmpty import Data.Map.Strict qualified as Map -import Data.Set qualified as Set import Data.Text qualified as StrictText import Data.Text.Encoding.Error (UnicodeException) import Data.Text.IO qualified as Text -import Data.Vector qualified as Vector import Numeric.Natural (Natural) import System.FilePath.Posix import Text.Megaparsec hiding (failure, parse, Token, try) import UnliftIO +import UnliftIO.Async qualified as Async import UnliftIO.Directory import UnliftIO.Environment @@ -234,31 +227,74 @@ scan input = do (unTokStream tokenStream) --- | Parse a file. Throws a 'ParseException' when tokenizing, scanning, or --- parsing fails. +-- | Parse a file. Throws an 'AuthorityFreeParseError' when packaged-prelude +-- loading/parsing or ordinary workspace parsing fails. parse :: MonadIO io => FilePath -> io [Raw.Block] parse file = do result <- parseWorkspace file - either throwWorkspaceError pure result + either throwIO pure result + +data AuthorityFreeParseError + = AuthorityFreePreludeLoadFailed !Prelude.PreludeLoadError + | AuthorityFreePreludeParseFailed !Prelude.PreludeParseError + | AuthorityFreeWorkspaceFailed !ParseWorkspaceError + deriving (Show) + +instance Exception AuthorityFreeParseError + +renderAuthorityFreeParseError :: AuthorityFreeParseError -> Text +renderAuthorityFreeParseError = \case + AuthorityFreePreludeLoadFailed failure -> + "packaged final prelude loading failed: " + <> Prelude.renderPreludeLoadError failure + AuthorityFreePreludeParseFailed failure -> + "packaged final prelude parsing failed: " + <> Prelude.renderPreludeParseError failure + AuthorityFreeWorkspaceFailed failure -> + Felix.renderParseWorkspaceError failure parseWorkspace :: MonadIO io => FilePath - -> io (Either ParseWorkspaceError [Raw.Block]) + -> io (Either AuthorityFreeParseError [Raw.Block]) parseWorkspace file = fmap Felix.importedBeforeImporterBlocks - <$> liftIO (parseDefaultWorkspace file) + <$> liftIO (parseDefaultWorkspaceWithPrelude file) -parseDefaultWorkspace +parseDefaultWorkspaceWithPrelude :: FilePath - -> IO (Either ParseWorkspaceError ParsedSourceWorkspace) -parseDefaultWorkspace file = do - prepared <- prepareDefaultSourceRequest file - case prepared of - Left err -> - pure (Left err) - Right (mounts, request) -> - Felix.parseSourceWorkspace mounts request + -> IO + (Either + AuthorityFreeParseError + ParsedSourceWorkspace) +parseDefaultWorkspaceWithPrelude file = + Prelude.loadReservedPreludeSourceInput >>= \case + Left failure -> + pure (Left (AuthorityFreePreludeLoadFailed failure)) + Right source -> + Prelude.parseReservedPreludeSource source >>= \case + Left failure -> + pure (Left (AuthorityFreePreludeParseFailed failure)) + Right prelude -> do + prepared <- prepareDefaultSourceRequest file + case prepared of + Left failure -> + pure + (Left + (AuthorityFreeWorkspaceFailed failure)) + Right (mounts, request) -> do + let syntax = + Felix.identifiedParsedModuleSyntaxInterface + (Prelude.reservedParsedPreludeModule + prelude) + fmap + (first AuthorityFreeWorkspaceFailed . fmap fst) + (Felix.parseSourceWorkspaceMeasuredWithSyntaxInputsAndGraphValidation + mounts + request + (const [syntax]) + (Prelude.rejectOrdinaryPreludeSourceGraph + source)) prepareDefaultSourceRequest :: FilePath @@ -326,81 +362,45 @@ throwWorkspaceError = \case simpleStream :: TokStream -> [[Token]] simpleStream TokStream{unTokStream=chunks} = [unLocated <$> ch | ch <- chunks] --- | Parse the workspace, then gloss each module independently in --- imported-before-importer order. -gloss :: MonadIO io => FilePath -> io [Internal.Block] -gloss file = do - result <- liftIO (parseDefaultWorkspace file) - workspace <- either throwWorkspaceError pure result - liftIO - (concat - <$> traverse - (\parsed -> - either throwIO pure - (meaning - (Felix.parsedModuleBlocks parsed))) - (toList - (Felix.parsedWorkspaceImportedBeforeImporter - workspace))) - +data VerificationResult + = VerificationCompleted + !VerificationReport + !VerificationPresentation + | CompletedWithExplicitGaps + !VerificationReport + !VerificationPresentation + | VerificationFailure !VerificationReport !FailedVerification + | VerificationCheckingFailure + !VerificationReport + !VerificationDriverError + deriving (Show) -generateTasks :: MonadIO io => FilePath -> io [Internal.Task] -generateTasks file = do - obligations <- - prepareCheckingTasks - contractionTask - file - pure (preparedObligationTask <$> obligations) +-- | Strict owner-independent source presentation retained only after the +-- complete typed workspace succeeds. +data VerificationPresentation = VerificationPresentation + !HtmlExport.HtmlPresentation -prepareCheckingTasks - :: MonadIO io - => (Internal.Task -> Internal.Task) - -> FilePath - -> io [PreparedObligation] -prepareCheckingTasks prepareTask file = do - blocks <- gloss file - liftIO - (checkPrepared - WithoutDumpPremselTraining - prepareTask - blocks) - -encodeTasks :: MonadIO io => FilePath -> io [Tptp.Task] -encodeTasks file = do - obligations <- - prepareCheckingTasks - contractionTask - file - pure - [ preparedTptpSyntax - (preparedProverTptpTask - (preparedObligationProverTask obligation)) - | obligation <- obligations - ] +instance Show VerificationPresentation where + show _presentation = + "VerificationPresentation <HTML presentation>" -data VerificationResult - = VerifiedWithTrustedVampire !VerificationReport - | CompletedWithExplicitGaps !VerificationReport - | VerificationFailure !FailedVerification - deriving (Show) +data ReportedEscapeKind + = ReportedSourceAxiom + | ReportedOmitted + deriving (Show, Eq) -data VerificationRoute - = LegacyVerificationRoute - | TypedVerificationRoute +data ReportedEscape = ReportedEscape + { reportedEscapeKind :: !ReportedEscapeKind + , reportedEscapeLocation :: !Location + } deriving (Show, Eq) data VerificationReport = VerificationReport - { verificationRoute :: !VerificationRoute - , verificationLegacyDeclaredAssumptionCount :: !Int - , verificationTypedDeclaredAssumptionCount :: !Int - , verificationTrustedVampireCount :: !Int - , verificationExplicitGapLocations :: ![Location] - , verificationTrustedLegacyRuleCount :: !Int - , verificationKernelProofCount :: !Int + { verificationDirectEscapes :: ![ReportedEscape] } deriving (Show, Eq) --- | Invocation-local observation of the sequential verification pipeline. +-- | Invocation-local observation of the verification pipeline. -- -- Durations use the monotonic clock and are never part of fact authority or -- deterministic verification results. @@ -410,73 +410,76 @@ data VerificationMeasurements = VerificationMeasurements , verificationInvocationNanoseconds :: !Word64 , verificationCheckingNanoseconds :: !Word64 , verificationModuleCount :: !Int + , verificationDetectedProcessorCount :: !(Maybe Int) + , verificationEffectiveJobs :: !Int + , verificationJobsOverridden :: !Bool + , verificationMaximumLiveModuleCheckers :: !Int + , verificationMaximumLiveVampireProcesses :: !Int , verificationMaximumReadyModuleCount :: !Int - , verificationReadyModuleWaitNanoseconds :: !Word64 , verificationObligationBatchCount :: !Int , verificationPreparedObligationCount :: !Int , verificationMaximumObligationBatchSize :: !Int , verificationPreparedRequestBytes :: !Word64 , verificationVampireRunCount :: !Int + , verificationModuleRootHitCount :: !Int + , verificationModuleRootMissCount :: !Int , verificationFirstVampireStartNanoseconds :: !(Maybe Word64) , verificationVampireExecutionNanoseconds :: !Word64 - , verificationReplayMeasurements - :: !Transition.TransitionReplayMeasurements } deriving (Show, Eq) data VerificationObservation = VerificationObservation { observedModuleCount :: !Int - , observedReadyAt - :: !(Map ResolvedSourceAddress Word64) + , observedDetectedProcessorCount :: !(Maybe Int) + , observedEffectiveJobs :: !Int + , observedJobsOverridden :: !Bool + , observedLiveModuleCheckers :: !Int + , observedMaximumLiveModuleCheckers :: !Int + , observedMaximumLiveVampireProcesses :: !Int , observedMaximumReadyModuleCount :: !Int - , observedReadyModuleWaitNanoseconds :: !Word64 , observedObligationBatchCount :: !Int , observedPreparedObligationCount :: !Int , observedMaximumObligationBatchSize :: !Int , observedPreparedRequestBytes :: !Word64 , observedVampireRunCount :: !Int + , observedModuleRootHitCount :: !Int + , observedModuleRootMissCount :: !Int , observedFirstVampireStart :: !(Maybe Word64) , observedVampireExecutionNanoseconds :: !Word64 - , observedNextRequestOrdinal :: !Natural } initialVerificationObservation :: VerificationObservation initialVerificationObservation = VerificationObservation { observedModuleCount = 0 - , observedReadyAt = Map.empty + , observedDetectedProcessorCount = Nothing + , observedEffectiveJobs = 1 + , observedJobsOverridden = False + , observedLiveModuleCheckers = 0 + , observedMaximumLiveModuleCheckers = 0 + , observedMaximumLiveVampireProcesses = 0 , observedMaximumReadyModuleCount = 0 - , observedReadyModuleWaitNanoseconds = 0 , observedObligationBatchCount = 0 , observedPreparedObligationCount = 0 , observedMaximumObligationBatchSize = 0 , observedPreparedRequestBytes = 0 , observedVampireRunCount = 0 + , observedModuleRootHitCount = 0 + , observedModuleRootMissCount = 0 , observedFirstVampireStart = Nothing , observedVampireExecutionNanoseconds = 0 - , observedNextRequestOrdinal = 1 } -newtype VerificationRequestOrdinal = VerificationRequestOrdinal Natural - deriving (Show, Eq, Ord) - -verificationRequestOrdinalValue - :: VerificationRequestOrdinal - -> Natural -verificationRequestOrdinalValue - (VerificationRequestOrdinal value) = - value - newtype VerificationRequestObserver = VerificationRequestObserver { observeVerificationRequest - :: VerificationRequestOrdinal + :: WorkPosition -> PreparedVerificationRequest -> IO () } verificationRequestObserver - :: (VerificationRequestOrdinal + :: (WorkPosition -> PreparedVerificationRequest -> IO ()) -> VerificationRequestObserver @@ -489,7 +492,6 @@ ignoreVerificationRequests = data FailedVerification = FailedVerification { failedVerificationLocation :: !Location - , failedVerificationFormula :: !Internal.Formula , failedVerificationReason :: !VerificationFailureReason } deriving (Show) @@ -502,58 +504,32 @@ data VerificationFailureReason | TransportFailure !ProverProcessError deriving (Show) -failedVerification - :: ( Location - , Internal.Formula - , Either ProverProcessError ProverAnswer - ) - -> Maybe FailedVerification -failedVerification (location, formula, result) = - FailedVerification location formula <$> case result of - 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) - -newtype VerificationAborted = - VerificationAborted FailedVerification - deriving (Show) - -instance Exception VerificationAborted +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 - | VerificationGlossError - !ResolvedSource - !GlossError - | VerificationCheckingError - !ResolvedSource - !CheckingError - | VerificationObligationResolutionError - !ObligationResolutionError - | VerificationLegacyModuleError - !Legacy.LegacyModuleStageError - | VerificationTransitionModuleError - !Transition.TransitionModuleError | VerificationFoundationManifestError !(NonEmpty Foundation.FoundationManifestError) | VerificationMissingImportedModule !ResolvedSourceAddress | VerificationMissingRootModule !ResolvedSourceAddress - | VerificationMigrationManifestError - !Migration.MigrationManifestError - | VerificationMigrationRouteMismatch - !Migration.MigrationGraphRoute | VerificationFinalPreludeReadinessError !Typed.FinalPreludeReadinessError | VerificationTypedInputError @@ -572,6 +548,9 @@ data VerificationDriverError | VerificationValidationIntegrityError !ResolvedSource !Declaration.ValidationIntegrityError + | VerificationAdmittedViewError + !ResolvedSource + !AdmittedViewError | VerificationParsedArtifactIntegrityError !ResolvedSource !Felix.ParsedArtifactIntegrityError @@ -579,13 +558,119 @@ data VerificationDriverError | VerificationStorePlanningFailure !Store.StorePlanningError | VerificationStoreLifecycleFailure !Store.StoreLifecycleError | VerificationModuleArtifactKeyError !Semantic.ModuleArtifactKeyError + | VerificationModuleSchedulerInvariant !Text deriving (Show) instance Exception VerificationDriverError -data CheckedWorkspace - = CheckedLegacyWorkspace !Transition.TransitionAdmittedModule - | CheckedTypedWorkspace !Typed.SealedTypedModule +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 @@ -601,14 +686,68 @@ verifyWithObserverAndStoreMode -> FilePath -> io (Either VerificationDriverError VerificationResult) verifyWithObserverAndStoreMode store validationMode observer prover file = - fmap fst - <$> try - (verifyMeasuredThrowingWithStore - store - validationMode - observer - prover - file) + verifyWithObserverAndStoreModeAndJobs + store validationMode sequentialJobs observer prover file + +verifyWithObserverAndStoreModeAndJobs + :: (MonadUnliftIO io, MonadLogger io) + => Store.Store + -> StoreValidationMode + -> JobsSelection + -> VerificationRequestObserver + -> Vampire + -> FilePath + -> io (Either VerificationDriverError VerificationResult) +verifyWithObserverAndStoreModeAndJobs + store validationMode jobs observer prover file = + fmap (fmap fst) + (verifyMeasuredWithObserverAndStoreModeAndJobs + store validationMode jobs observer prover file) + +verifyMeasuredWithObserverAndStoreMode + :: (MonadUnliftIO io, MonadLogger io) + => Store.Store + -> StoreValidationMode + -> VerificationRequestObserver + -> Vampire + -> FilePath + -> io + (Either + VerificationDriverError + (VerificationResult, VerificationMeasurements)) +verifyMeasuredWithObserverAndStoreMode + store validationMode observer prover file = + verifyMeasuredWithObserverAndStoreModeAndJobs + store validationMode sequentialJobs observer prover file + +verifyMeasuredWithObserverAndStoreModeAndJobs + :: (MonadUnliftIO io, MonadLogger io) + => Store.Store + -> StoreValidationMode + -> JobsSelection + -> VerificationRequestObserver + -> Vampire + -> FilePath + -> io + (Either + VerificationDriverError + (VerificationResult, VerificationMeasurements)) +verifyMeasuredWithObserverAndStoreModeAndJobs + store validationMode jobs observer prover file = + try + (verifyMeasuredThrowingWithStore + store validationMode jobs observer prover file) + +sequentialJobs :: JobsSelection +sequentialJobs = + JobsSelection + { jobsSelectionDetectedProcessors = Nothing + , jobsSelectionEffectiveJobs = + fromMaybe + (impossible "one is not a positive worker count") + (effectiveJobs 1) + , jobsSelectionWasOverridden = True + } verifyMeasured :: (MonadUnliftIO io, MonadLogger io) @@ -663,6 +802,7 @@ verifyMeasuredThrowing requestObserver prover file = do (verifyMeasuredThrowingWithStore store FreshStoreValidation + sequentialJobs requestObserver prover file)) @@ -675,35 +815,52 @@ verifyMeasuredThrowingWithStore :: (MonadUnliftIO io, MonadLogger io) => Store.Store -> StoreValidationMode + -> JobsSelection -> VerificationRequestObserver -> Vampire -> FilePath -> io (VerificationResult, VerificationMeasurements) verifyMeasuredThrowingWithStore - store validationMode requestObserver prover file = do + store validationMode jobsSelection requestObserver prover file = do invocationStart <- liftIO getMonotonicTimeNSec + memo <- liftIO (Store.newStoreMemo store) + storeCoordinator <- liftIO Store.newStoreCoordinator ( admittedResult , parseMeasurements , sourcePreparation , checkingStart , checkingEnd , observation + , parsedPresentation ) <- - withRunInIO \runInIO -> do - observationRef <- - newIORef initialVerificationObservation + withRunInIO \runInIO -> + withVampireExecutor + (jobsSelectionEffectiveJobs jobsSelection) + prover + (observeVerificationRequest requestObserver) + \executor -> do + observationRef <- newIORef + initialVerificationObservation + { observedDetectedProcessorCount = + jobsSelectionDetectedProcessors jobsSelection + , observedEffectiveJobs = + effectiveJobsValue + (jobsSelectionEffectiveJobs jobsSelection) + , observedJobsOverridden = + jobsSelectionWasOverridden jobsSelection + } foundation <- either (throwIO . VerificationFoundationManifestError) pure Foundation.checkedFoundation - let resolver = - typedVampireResolver - runInIO - prover - requestObserver - observationRef + preludeResolver <- + typedVampireResolver + runInIO + executor + 0 + observationRef preparationStart <- getMonotonicTimeNSec prepared <- prepareDefaultSourceRequest file @@ -711,102 +868,72 @@ verifyMeasuredThrowingWithStore (throwIO . VerificationWorkspaceError) pure let (mounts, request) = prepared - selection <- - either - (throwIO . VerificationMigrationManifestError) - pure - (Migration.resolveMigrationSelection - mounts - Migration.typedMigrationModules) - root <- - resolveRoot mounts request + preparationEnd <- getMonotonicTimeNSec + prelude <- + Typed.acquireFinalPreludeSession + memo store foundation preludeResolver >>= either (throwIO - . VerificationWorkspaceError - . SourceWorkspaceError) + . VerificationFinalPreludeReadinessError) pure - preparationEnd <- getMonotonicTimeNSec - prelude <- - if Migration.migrationSelectionContains selection root - then - Just - <$> (Typed.buildFinalPreludeSession - store foundation resolver - >>= either - (throwIO - . VerificationFinalPreludeReadinessError) - pure) - else - pure Nothing + observeModuleRootAcquisition observationRef + (Typed.finalPreludeAcquisition prelude) let preludeSyntax = Typed.sealedTypedModuleSyntax - . Typed.migrationPreludeModule - syntaxInputs source - | Migration.migrationSelectionContains selection source = - maybeToList (preludeSyntax <$> prelude) - | otherwise = [] + (Typed.finalPreludeModule prelude) + syntaxInputs _source = [preludeSyntax] (parsed, measured) <- - Felix.parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputs + Felix.parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndGraphValidation store mounts request syntaxInputs + (Prelude.rejectOrdinaryPreludeSourceGraph + (Typed.finalPreludeSource prelude)) >>= either throwParseExecutionError pure checkingStart <- getMonotonicTimeNSec - admitted <- - (Right <$> case - ( prelude - , Migration.classifyMigrationGraph selection parsed - ) of - (Nothing, Migration.LegacyMigrationGraph) -> - CheckedLegacyWorkspace - <$> checkParsedWorkspace - foundation - runInIO - prover - requestObserver - observationRef - parsed - (Just finalPrelude, Migration.TypedMigrationGraph) -> - CheckedTypedWorkspace - <$> checkTypedWorkspace - foundation - finalPrelude - resolver - validationMode - observationRef - parsed - store - (_, route) -> - throwIO - (VerificationMigrationRouteMismatch route)) - `catch` - \(VerificationAborted failed) -> - pure (Left failed) + outcome <- + checkTypedWorkspace + memo + storeCoordinator + foundation + prelude + runInIO + executor + (jobsSelectionEffectiveJobs jobsSelection) + validationMode + observationRef + parsed + store checkingEnd <- getMonotonicTimeNSec + executorObserved <- vampireExecutorObservation executor + mergeExecutorObservation observationRef executorObserved observed <- readIORef observationRef pure - ( admitted + ( outcome , measured , preparationEnd - preparationStart , checkingStart , checkingEnd , observed + , parsed ) let result = case admittedResult of - Left failed -> - VerificationFailure failed - Right admitted -> - let report = - checkedWorkspaceReport admitted - in - if null - (verificationExplicitGapLocations report) - then - VerifiedWithTrustedVampire report - else - CompletedWithExplicitGaps report + 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 + parsedPresentation)) measurements = finalizeVerificationMeasurements invocationStart @@ -815,7 +942,6 @@ verifyMeasuredThrowingWithStore parseMeasurements sourcePreparation observation - (either (const Nothing) Just admittedResult) logInfoN (renderVerificationMeasurements measurements) pure (result, measurements) @@ -829,187 +955,205 @@ verifyMeasuredThrowingWithStore throwIO (VerificationParsedArtifactIntegrityError source failure) -checkParsedWorkspace +checkTypedWorkspace :: forall io . (MonadIO io, MonadLogger io) - => Foundation.CheckedFoundation - -> (forall a. io a -> IO a) - -> Vampire - -> VerificationRequestObserver - -> IORef VerificationObservation - -> ParsedSourceWorkspace - -> IO Transition.TransitionAdmittedModule -checkParsedWorkspace - checkedFoundationValue - runInIO - prover - requestObserver - observationRef - workspace = do - assignments <- - driverLegacy - (Legacy.assignLegacyModuleOrdinals workspace) - initializeModuleObservation - observationRef - assignments - admittedByAddress <- - foldM - (checkModule - checkedFoundationValue - assignments) - Map.empty - (toList assignments) - let rootAddress = - Felix.parsedModuleAddress - (Felix.parsedWorkspaceRootModule workspace) - maybe - (throwIO - (VerificationMissingRootModule rootAddress)) - pure - (Map.lookup rootAddress admittedByAddress) - where - foundation = - initialLegacyCheckingEnvironment - - checkModule - :: Foundation.CheckedFoundation - -> NonEmpty Legacy.LegacyModuleAssignment - -> Map - ResolvedSourceAddress - Transition.TransitionAdmittedModule - -> Legacy.LegacyModuleAssignment - -> IO - (Map - ResolvedSourceAddress - Transition.TransitionAdmittedModule) - checkModule - moduleFoundation - assignments - admittedByAddress - assignment = do - let parsedModule = - Legacy.assignedParsedModule assignment - source = - Felix.parsedModuleResolved parsedModule - address = - Felix.parsedModuleAddress parsedModule - moduleStart <- getMonotonicTimeNSec - observeModuleStart - observationRef - assignments - admittedByAddress - address - moduleStart - directImports <- - traverse - (lookupImportedModule admittedByAddress - . Felix.parsedImportedAddress) - (Felix.parsedModuleImports parsedModule) - builder <- - driverTransition - (Transition.openTransitionModuleBuilder - moduleFoundation - foundation - assignment - directImports) - blocks <- - glossModule - source - (Felix.parsedModuleBlocks parsedModule) - checked <- do - checkedResult <- try - (runCheckingBlocks - blocks - (initialTransitionCheckingState - builder - (resolvePreparedBatch - runInIO - prover - requestObserver - observationRef))) - either - (throwIO . VerificationCheckingError source) - pure - checkedResult - finalBuilder <- - maybe - (impossible - "checking lost its transition module builder") - pure - (checkingTransitionModuleBuilder checked) - admitted <- - driverTransition - (Transition.sealTransitionModule - (checkingStateEnvironment checked) - finalBuilder) - moduleEnd <- getMonotonicTimeNSec - let admittedByAddress' = - Map.insert address admitted admittedByAddress - observeModuleAdmission - observationRef - assignments - admittedByAddress' - moduleEnd - pure admittedByAddress' - -checkTypedWorkspace - :: Foundation.CheckedFoundation - -> Typed.MigrationPreludeSession - -> Declaration.VampireResolver + => Store.StoreMemo + -> Store.StoreCoordinator + -> Foundation.CheckedFoundation + -> Typed.FinalPreludeSession + -> (forall value. io value -> IO value) + -> VampireExecutor + -> EffectiveJobs -> StoreValidationMode -> IORef VerificationObservation -> ParsedSourceWorkspace -> Store.Store - -> IO Typed.SealedTypedModule + -> IO TypedWorkspaceOutcome checkTypedWorkspace - foundation prelude resolver validationMode observationRef workspace + memo + storeCoordinator + foundation + prelude + runInIO + executor + selectedJobs + validationMode + observationRef + workspace store = do - memo <- Store.newStoreMemo store let modules = - toList (Felix.parsedWorkspaceImportedBeforeImporter workspace) - modifyIORef' observationRef \observation -> - observation - { observedModuleCount = length modules - , observedMaximumReadyModuleCount = - if null modules then 0 else 1 - } - admittedByAddress <- - foldM (checkModule memo) Map.empty modules - let root = Felix.parsedWorkspaceRootModule workspace - rootAddress = Felix.parsedModuleAddress root - maybe - (throwIO (VerificationMissingRootModule rootAddress)) - pure - (Map.lookup rootAddress admittedByAddress) + zipWith + makeTask + [1..] + (toList + (Felix.parsedWorkspaceImportedBeforeImporter workspace)) + rootAddress = + Felix.parsedModuleAddress + (Felix.parsedWorkspaceRootModule workspace) + atomicModifyIORef' observationRef + (\observation -> + ( observation + { observedModuleCount = length modules + } + , () + )) + scheduleModules + rootAddress + modules + Map.empty + Map.empty + Map.empty + Nothing where - storeValidationLookup lookupStore = - Declaration.validationLookup - (\key -> - Store.loadProofValidation lookupStore key - >>= either - (throwIO . VerificationStoreFailure) - pure) - (\key -> - Store.loadDeclarationValidation lookupStore key - >>= either - (throwIO . VerificationStoreFailure) - pure) + workerBound = effectiveJobsValue selectedJobs - validationRun = - case validationMode of - FreshStoreValidation -> - Declaration.FreshValidation - WarmStoreValidation -> - Declaration.WarmValidation - (storeValidationLookup store) - - checkModule memo admittedByAddress parsed = do - let source = Felix.parsedModuleResolved parsed - address = Felix.parsedModuleAddress parsed - directAddresses = + makeTask ordinal parsed = + ModuleTask + { moduleTaskOrdinal = ordinal + , moduleTaskParsed = parsed + , moduleTaskDirectAddresses = nubOrd (Felix.parsedImportedAddress <$> Felix.parsedModuleImports parsed) + } + + scheduleModules + rootAddress + pending + running + sealedByAddress + admittedByOrdinal + candidate = do + let readyCount = + length + [ () + | task <- pending + , taskMayStart candidate sealedByAddress task + ] + observeReadyModules observationRef readyCount + (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 + (observeModuleChecker observationRef + (checkModule task sealedByAddress)) + :: IO + (Either + SomeException + ModuleCheckResult)) + pure (moduleTaskOrdinal task, completed) + startReadyModules + remaining + (Map.insert + (moduleTaskOrdinal task) + checker + running) + sealedByAddress + candidate + + checkModule task sealedByAddress = do + let parsed = moduleTaskParsed task + source = Felix.parsedModuleResolved parsed + address = Felix.parsedModuleAddress parsed direct <- traverse (\directAddress -> @@ -1018,8 +1162,14 @@ checkTypedWorkspace (VerificationMissingImportedModule directAddress)) pure - (Map.lookup directAddress admittedByAddress)) - directAddresses + (Map.lookup directAddress sealedByAddress)) + (moduleTaskDirectAddresses task) + resolver <- + typedVampireResolver + runInIO + executor + (moduleTaskOrdinal task) + observationRef input <- either (throwIO . VerificationTypedInputError source) @@ -1031,9 +1181,16 @@ checkTypedWorkspace validationRun parsed direct) - loadCachedModule memo parsed direct >>= \case - Just sealed -> - pure (Map.insert address sealed admittedByAddress) + loadCachedModule parsed direct >>= \case + Just sealed -> do + observeModuleRootAcquisition + observationRef Typed.ModuleRootHit + pure + (ModuleCheckSucceeded + address + sealed + (completeAdmittedModule + (Typed.identifiedPhysicalModule parsed))) Nothing -> do typedResult <- Exception.catch @@ -1046,21 +1203,88 @@ checkTypedWorkspace case typedResult of Typed.TypedModuleOpenFailed err -> throwIO (VerificationTypedOpenError source err) - Typed.TypedModuleFailed err prefix -> - flushPrefix prefix - >>= either - (throwIO . VerificationStoreFailure) - (const - (throwIO - (VerificationTypedModuleError - source - err - prefix))) + 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 (Map.insert address sealed admittedByAddress) + observeModuleRootAcquisition + observationRef Typed.ModuleRootMiss + 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 @@ -1080,22 +1304,24 @@ checkTypedWorkspace (Typed.sealedTypedModuleSyntax sealed)) (Semantic.semanticInterfaceAssertedId (Typed.sealedTypedModuleSemantic sealed)) - Store.writeSealedModule - store - (Typed.sealedTypedModulePrefix sealed) - [Typed.sealedTypedModuleSyntax sealed] - [Typed.sealedTypedModuleSemantic sealed] - artifact - >>= either - (throwIO . VerificationStoreFailure) - (\acknowledged -> - unless - (acknowledged == artifact) - (throwIO - (VerificationStoreFailure - Store.StoreModuleArtifactIdMismatch))) + 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 memo parsed direct = + loadCachedModule parsed direct = case validationMode of WarmStoreValidation -> do let owner = @@ -1104,7 +1330,7 @@ checkTypedWorkspace directSemantic = Semantic.semanticInterfaceAssertedId (Typed.sealedTypedModuleSemantic - (Typed.migrationPreludeModule prelude)) + (Typed.finalPreludeModule prelude)) : ( Semantic.semanticInterfaceAssertedId . Typed.sealedTypedModuleSemantic <$> direct @@ -1120,386 +1346,275 @@ checkTypedWorkspace (Typed.identifiedPhysicalModule parsed))) directSemantic (Identity.theoryId foundation)) - Store.loadCachedModuleInstallation - memo - store - artifactKey - (Syntax.moduleSyntaxAssertedId - (Felix.parsedModuleSyntaxInterface parsed)) - >>= \case + 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) -> do - cached <- - either - (throwIO - . VerificationTypedCachedModuleError - (Felix.parsedModuleResolved parsed)) - pure - (Typed.cachedSealedTypedModule - foundation - (Typed.migrationPreludeModule prelude - : direct) - installation) - pure (Just cached) + Right (Just installation) -> + either + (throwIO + . VerificationTypedCachedModuleError + (Felix.parsedModuleResolved parsed)) + (pure . Just) + (Typed.cachedSealedTypedModule + foundation + (Typed.finalPreludeModule prelude : direct) + installation) FreshStoreValidation -> pure Nothing - flushPrefix prefix = - Store.writePendingModulePrefix store prefix + 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 :: forall io . (MonadIO io, MonadLogger io) => (forall value. io value -> IO value) - -> Vampire - -> VerificationRequestObserver + -> VampireExecutor + -> Natural -> IORef VerificationObservation - -> Declaration.VampireResolver -typedVampireResolver runInIO prover requestObserver observationRef = - Declaration.vampireResolver \prepared -> do - started <- getMonotonicTimeNSec - observeVampireStart observationRef started - let request = preparedTypedProverRequest prepared - modifyIORef' observationRef \observation -> - observation + -> IO Declaration.VampireResolver +typedVampireResolver + runInIO executor moduleOrdinal observationRef = do + localOrdinalRef <- newIORef 1 + pure (Declaration.vampireBatchResolver \prepared -> do + let batchSize = NonEmpty.length prepared + ordinalCount = fromIntegral batchSize + firstOrdinal <- atomicModifyIORef' localOrdinalRef + (\current -> (current + ordinalCount, current)) + let positions = + NonEmpty.fromList + [ workPosition moduleOrdinal ordinal + | ordinal <- + [firstOrdinal .. firstOrdinal + ordinalCount - 1] + ] + positioned = + NonEmpty.zip positions prepared + preparedBytes = + foldl' + (\total task -> + total + + fromIntegral + (preparedVerificationByteCount + (preparedTypedProverRequest task))) + 0 + prepared + atomicModifyIORef' observationRef \observation -> + ( observation { observedObligationBatchCount = observedObligationBatchCount observation + 1 , observedPreparedObligationCount = - observedPreparedObligationCount observation + 1 + observedPreparedObligationCount observation + batchSize , observedMaximumObligationBatchSize = max - 1 + batchSize (observedMaximumObligationBatchSize observation) , observedPreparedRequestBytes = observedPreparedRequestBytes observation - + fromIntegral - (preparedVerificationByteCount request) + + preparedBytes } - result <- runInIO - (runPreparedTypedProverWithObserver - (observeRequest observationRef requestObserver) - prover - prepared) - finished <- getMonotonicTimeNSec - observeVampireFinish observationRef (finished - started) - pure result - -initializeModuleObservation - :: IORef VerificationObservation - -> NonEmpty Legacy.LegacyModuleAssignment - -> IO () -initializeModuleObservation observationRef assignments = do - now <- getMonotonicTimeNSec - let ready = - readyModuleAssignments - assignments - Map.empty - modifyIORef' - observationRef - (\observation -> - observation - { observedModuleCount = - NonEmpty.length assignments - , observedReadyAt = - Map.fromList - [ (legacyAssignmentAddress assignment, now) - | assignment <- ready - ] - , observedMaximumReadyModuleCount = - length ready - }) - -observeModuleStart + , () + ) + results <- + Async.mapConcurrently + (\(position, task) -> + runInIO + (runPreparedTypedProverWithExecutor + executor + position + task)) + (NonEmpty.toList positioned) + pure (NonEmpty.fromList results)) + +observeModuleRootAcquisition :: IORef VerificationObservation - -> NonEmpty Legacy.LegacyModuleAssignment - -> Map - ResolvedSourceAddress - Transition.TransitionAdmittedModule - -> ResolvedSourceAddress - -> Word64 + -> Typed.ModuleRootAcquisition -> IO () -observeModuleStart - observationRef - assignments - admittedByAddress - address - now = - modifyIORef' - observationRef - (\observation -> - let - ready = - readyModuleAssignments - assignments - admittedByAddress - readySince = - Map.findWithDefault - now - address - (observedReadyAt observation) - in +observeModuleRootAcquisition observationRef acquisition = + atomicModifyIORef' observationRef \observation -> + ( case acquisition of + Typed.ModuleRootHit -> observation - { observedMaximumReadyModuleCount = - max - (observedMaximumReadyModuleCount - observation) - (length ready) - , observedReadyModuleWaitNanoseconds = - observedReadyModuleWaitNanoseconds - observation - + (now - readySince) - }) - -observeModuleAdmission - :: IORef VerificationObservation - -> NonEmpty Legacy.LegacyModuleAssignment - -> Map - ResolvedSourceAddress - Transition.TransitionAdmittedModule - -> Word64 - -> IO () -observeModuleAdmission - observationRef - assignments - admittedByAddress - now = - modifyIORef' - observationRef - (\observation -> - let - ready = - readyModuleAssignments - assignments - admittedByAddress - readyAt = - foldl' - (\known assignment -> - Map.insertWith - (\_new old -> old) - (legacyAssignmentAddress assignment) - now - known) - (observedReadyAt observation) - ready - in + { observedModuleRootHitCount = + observedModuleRootHitCount observation + 1 + } + Typed.ModuleRootMiss -> observation - { observedReadyAt = readyAt - , observedMaximumReadyModuleCount = - max - (observedMaximumReadyModuleCount - observation) - (length ready) - }) - -readyModuleAssignments - :: NonEmpty Legacy.LegacyModuleAssignment - -> Map - ResolvedSourceAddress - Transition.TransitionAdmittedModule - -> [Legacy.LegacyModuleAssignment] -readyModuleAssignments assignments admittedByAddress = - [ assignment - | assignment <- NonEmpty.toList assignments - , legacyAssignmentAddress assignment - `Map.notMember` admittedByAddress - , all - (`Map.member` admittedByAddress) - (legacyAssignmentImportAddresses assignment) - ] - -legacyAssignmentAddress - :: Legacy.LegacyModuleAssignment - -> ResolvedSourceAddress -legacyAssignmentAddress = - Felix.parsedModuleAddress - . Legacy.assignedParsedModule - -legacyAssignmentImportAddresses - :: Legacy.LegacyModuleAssignment - -> [ResolvedSourceAddress] -legacyAssignmentImportAddresses = - fmap Felix.parsedImportedAddress - . Felix.parsedModuleImports - . Legacy.assignedParsedModule - -lookupImportedModule - :: Map - ResolvedSourceAddress - Transition.TransitionAdmittedModule - -> ResolvedSourceAddress - -> IO Transition.TransitionAdmittedModule -lookupImportedModule admittedByAddress address = - maybe - (throwIO - (VerificationMissingImportedModule address)) - pure - (Map.lookup address admittedByAddress) - -glossModule - :: ResolvedSource - -> [Raw.Block] - -> IO [Internal.Block] -glossModule source rawBlocks = - either - (throwIO . VerificationGlossError source) - pure - (meaning rawBlocks) + { observedModuleRootMissCount = + observedModuleRootMissCount observation + 1 + } + , () + ) -resolvePreparedBatch - :: forall io - . (MonadIO io, MonadLogger io) - => (forall a. io a -> IO a) - -> Vampire - -> VerificationRequestObserver - -> IORef VerificationObservation - -> PreparedObligationBatch - -> IO ResolvedObligationBatch -resolvePreparedBatch - runInIO prover requestObserver observationRef batch = do - observePreparedBatch observationRef batch - resolved <- - traverse - resolveObligation - (preparedBatchObligations batch) - driverResolution - (resolveObligationBatch batch resolved) - where - resolveObligation obligation = - case preparedObligationMethod obligation of - RecordExplicitGap{} -> - driverResolution - (resolveObligationAsGap obligation) - ProveWithVampire -> do - started <- getMonotonicTimeNSec - observeVampireStart - observationRef - started - result <- - runInIO - (runPreparedProverWithObserver - (observeRequest - observationRef - requestObserver) - prover - (preparedObligationProverTask - obligation)) - finished <- getMonotonicTimeNSec - observeVampireFinish - observationRef - (finished - started) - case failedVerification result of - Just failed -> - throwIO (VerificationAborted failed) - Nothing -> - case result of - ( _location - , _formula - , Right answer - ) - | Just accepted <- - provedVampireRun answer -> - driverResolution - (resolveObligationWithVampire - obligation - accepted) - _ -> - impossible - "successful prover result has no accepted Vampire run" - -observeRequest +observeReadyModules :: IORef VerificationObservation - -> VerificationRequestObserver - -> PreparedVerificationRequest + -> Int -> IO () -observeRequest observationRef observer request = do - ordinal <- atomicModifyIORef' observationRef \observation -> - let current = observedNextRequestOrdinal observation +observeReadyModules observationRef readyCount = + atomicModifyIORef' observationRef \observation -> + ( observation + { observedMaximumReadyModuleCount = + max readyCount + (observedMaximumReadyModuleCount observation) + } + , () + ) + +observeModuleChecker + :: IORef VerificationObservation + -> IO value + -> IO value +observeModuleChecker observationRef action = do + atomicModifyIORef' observationRef \observation -> + let live = observedLiveModuleCheckers observation + 1 in ( observation - { observedNextRequestOrdinal = current + 1 + { observedLiveModuleCheckers = live + , observedMaximumLiveModuleCheckers = + max live + (observedMaximumLiveModuleCheckers observation) } - , VerificationRequestOrdinal current + , () ) - observeVerificationRequest observer ordinal request - -observePreparedBatch + action `Exception.finally` + atomicModifyIORef' observationRef + (\observation -> + ( observation + { observedLiveModuleCheckers = + observedLiveModuleCheckers observation - 1 + } + , () + )) + +mergeExecutorObservation :: IORef VerificationObservation - -> PreparedObligationBatch + -> VampireExecutorObservation -> IO () -observePreparedBatch observationRef batch = - modifyIORef' - observationRef - (\observation -> - observation - { observedObligationBatchCount = - observedObligationBatchCount observation - + 1 - , observedPreparedObligationCount = - observedPreparedObligationCount observation - + obligationCount - , observedMaximumObligationBatchSize = - max - (observedMaximumObligationBatchSize - observation) - obligationCount - , observedPreparedRequestBytes = - observedPreparedRequestBytes observation - + requestBytes - }) - where - obligations = - preparedBatchObligations batch - obligationCount = - Vector.length obligations - requestBytes = - Vector.foldl' - (\total obligation -> - total - + fromIntegral - (preparedVerificationByteCount - (preparedProverRequest - (preparedObligationProverTask - obligation)))) - 0 - obligations - -observeVampireStart - :: IORef VerificationObservation - -> Word64 - -> IO () -observeVampireStart observationRef started = - modifyIORef' - observationRef - (\observation -> - observation - { observedVampireRunCount = - observedVampireRunCount observation - + 1 - , observedFirstVampireStart = - case observedFirstVampireStart observation of - Nothing -> - Just started - firstStart -> - firstStart - }) - -observeVampireFinish - :: IORef VerificationObservation - -> Word64 - -> IO () -observeVampireFinish observationRef duration = - modifyIORef' - observationRef - (\observation -> - observation - { observedVampireExecutionNanoseconds = - observedVampireExecutionNanoseconds - observation - + duration - }) +mergeExecutorObservation observationRef executorObserved = + atomicModifyIORef' observationRef \observation -> + ( observation + { observedVampireRunCount = + vampireExecutorRunCount executorObserved + , observedMaximumLiveVampireProcesses = + vampireExecutorMaximumLiveCount executorObserved + , observedFirstVampireStart = + vampireExecutorFirstStartNanoseconds executorObserved + , observedVampireExecutionNanoseconds = + vampireExecutorExecutionNanoseconds executorObserved + } + , () + ) finalizeVerificationMeasurements :: Word64 @@ -1508,7 +1623,6 @@ finalizeVerificationMeasurements -> Felix.ParseMeasurements -> Word64 -> VerificationObservation - -> Maybe CheckedWorkspace -> VerificationMeasurements finalizeVerificationMeasurements invocationStart @@ -1516,8 +1630,7 @@ finalizeVerificationMeasurements checkingEnd parseMeasurements sourcePreparation - observation - admitted = + observation = VerificationMeasurements { verificationParseMeasurements = parseMeasurements @@ -1529,10 +1642,18 @@ finalizeVerificationMeasurements checkingEnd - checkingStart , verificationModuleCount = observedModuleCount observation + , verificationDetectedProcessorCount = + observedDetectedProcessorCount observation + , verificationEffectiveJobs = + observedEffectiveJobs observation + , verificationJobsOverridden = + observedJobsOverridden observation + , verificationMaximumLiveModuleCheckers = + observedMaximumLiveModuleCheckers observation + , verificationMaximumLiveVampireProcesses = + observedMaximumLiveVampireProcesses observation , verificationMaximumReadyModuleCount = observedMaximumReadyModuleCount observation - , verificationReadyModuleWaitNanoseconds = - observedReadyModuleWaitNanoseconds observation , verificationObligationBatchCount = observedObligationBatchCount observation , verificationPreparedObligationCount = @@ -1543,20 +1664,16 @@ finalizeVerificationMeasurements observedPreparedRequestBytes observation , verificationVampireRunCount = observedVampireRunCount observation + , verificationModuleRootHitCount = + observedModuleRootHitCount observation + , verificationModuleRootMissCount = + observedModuleRootMissCount observation , verificationFirstVampireStartNanoseconds = fmap (\started -> started - invocationStart) (observedFirstVampireStart observation) , verificationVampireExecutionNanoseconds = observedVampireExecutionNanoseconds observation - , verificationReplayMeasurements = - case admitted of - Just (CheckedLegacyWorkspace legacy) -> - Transition.transitionAdmittedReplayMeasurements legacy - Just (CheckedTypedWorkspace _typed) -> - emptyReplayMeasurements - Nothing -> - emptyReplayMeasurements } renderVerificationMeasurements @@ -1607,6 +1724,21 @@ renderVerificationMeasurements measurements = parseMeasurements) , "modules=" <> renderIntegral (verificationModuleCount measurements) + , "detected_processors=" + <> maybe + "unavailable" + renderIntegral + (verificationDetectedProcessorCount measurements) + , "effective_jobs=" <> renderIntegral + (verificationEffectiveJobs measurements) + , "jobs_overridden=" + <> if verificationJobsOverridden measurements + then "yes" + else "no" + , "max_module_checkers=" <> renderIntegral + (verificationMaximumLiveModuleCheckers measurements) + , "max_vampire_processes=" <> renderIntegral + (verificationMaximumLiveVampireProcesses measurements) , "files_read=" <> renderIntegral (Felix.parseMeasurementModuleCount parseMeasurements) @@ -1634,6 +1766,10 @@ renderVerificationMeasurements measurements = (verificationPreparedRequestBytes measurements) , "vampire_runs=" <> renderIntegral (verificationVampireRunCount measurements) + , "module_root_hits=" <> renderIntegral + (verificationModuleRootHitCount measurements) + , "module_root_misses=" <> renderIntegral + (verificationModuleRootMissCount measurements) , "first_vampire_ms=" <> maybe "none" @@ -1644,43 +1780,9 @@ renderVerificationMeasurements measurements = <> renderNanoseconds (verificationVampireExecutionNanoseconds measurements) - , "vampire_idle_ms=" - <> renderNanoseconds - (verificationVampireIdleNanoseconds - measurements) - , "vampire_utilization_permille=" - <> renderIntegral - (verificationVampireUtilizationPermille - measurements) , "max_ready_modules=" <> renderIntegral (verificationMaximumReadyModuleCount measurements) - , "ready_wait_sum_ms=" - <> renderNanoseconds - (verificationReadyModuleWaitNanoseconds - measurements) - , "kernel_replays=" <> renderIntegral - (Transition.transitionKernelReplayCount replay) - , "kernel_replay_nodes=" <> renderIntegral - (Transition.transitionKernelReplayNodeCount replay) - , "kernel_replay_max_depth=" <> renderIntegral - (Transition.transitionKernelReplayMaximumDepth replay) - , "reconstructions=" <> renderIntegral - (Transition.transitionReconstructionCount replay) - , "connection_search_work=" <> renderIntegral - (Transition.transitionReconstructionSearchWork - replay) - , "connection_derived_atoms=" <> renderIntegral - (Transition.transitionReconstructionDerivedAtomCount - replay) - , "connection_max_candidate_depth=" <> renderIntegral - (Transition.transitionReconstructionMaximumCandidateDepth - replay) - , "connection_replay_nodes=" <> renderIntegral - (Transition.transitionConnectionReplayNodeCount replay) - , "connection_replay_max_depth=" <> renderIntegral - (Transition.transitionConnectionReplayMaximumDepth - replay) , "total_ms=" <> renderNanoseconds (verificationInvocationNanoseconds @@ -1689,52 +1791,6 @@ renderVerificationMeasurements measurements = where parseMeasurements = verificationParseMeasurements measurements - replay = - verificationReplayMeasurements measurements - -emptyReplayMeasurements - :: Transition.TransitionReplayMeasurements -emptyReplayMeasurements = - Transition.TransitionReplayMeasurements - { Transition.transitionKernelReplayCount = 0 - , Transition.transitionKernelReplayNodeCount = 0 - , Transition.transitionKernelReplayMaximumDepth = 0 - , Transition.transitionReconstructionCount = 0 - , Transition.transitionReconstructionSearchWork = 0 - , Transition.transitionReconstructionDerivedAtomCount = 0 - , Transition.transitionReconstructionMaximumCandidateDepth = 0 - , Transition.transitionConnectionReplayNodeCount = 0 - , Transition.transitionConnectionReplayMaximumDepth = 0 - } - -verificationVampireIdleNanoseconds - :: VerificationMeasurements - -> Word64 -verificationVampireIdleNanoseconds measurements = - checking - min checking execution - where - checking = - verificationCheckingNanoseconds measurements - execution = - verificationVampireExecutionNanoseconds - measurements - -verificationVampireUtilizationPermille - :: VerificationMeasurements - -> Word64 -verificationVampireUtilizationPermille measurements - | checking == 0 = - 0 - | otherwise = - min - 1000 - (execution * 1000 `div` checking) - where - checking = - verificationCheckingNanoseconds measurements - execution = - verificationVampireExecutionNanoseconds - measurements renderNanoseconds :: Word64 -> Text renderNanoseconds nanoseconds = @@ -1744,78 +1800,93 @@ renderIntegral :: Show number => number -> Text renderIntegral = StrictText.pack . show -driverLegacy - :: Either Legacy.LegacyModuleStageError value - -> IO value -driverLegacy = - either - (throwIO . VerificationLegacyModuleError) - pure - -driverTransition - :: Either Transition.TransitionModuleError value - -> IO value -driverTransition = - either - (throwIO . VerificationTransitionModuleError) - pure - -driverResolution - :: Either ObligationResolutionError value - -> IO value -driverResolution = - either - (throwIO . VerificationObligationResolutionError) - pure - -checkedWorkspaceReport :: CheckedWorkspace -> VerificationReport -checkedWorkspaceReport = \case - CheckedLegacyWorkspace admitted -> - legacyVerificationReport admitted - CheckedTypedWorkspace _admitted -> - VerificationReport - { verificationRoute = TypedVerificationRoute - , verificationLegacyDeclaredAssumptionCount = 0 - , verificationTypedDeclaredAssumptionCount = 0 - , verificationTrustedVampireCount = 0 - , verificationExplicitGapLocations = [] - , verificationTrustedLegacyRuleCount = 0 - , verificationKernelProofCount = 0 - } - -legacyVerificationReport - :: Transition.TransitionAdmittedModule +admittedWorkspaceReport + :: AdmittedTypedWorkspace -> VerificationReport -legacyVerificationReport admitted = +admittedWorkspaceReport (AdmittedTypedWorkspace modules) = VerificationReport - { verificationRoute = LegacyVerificationRoute - , verificationLegacyDeclaredAssumptionCount = - Set.size - (Legacy.legacyDeclaredAssumptionUses trust) - , verificationTypedDeclaredAssumptionCount = - Set.size - (Transition.typedDeclaredAssumptionUses - (Transition.transitionAdmittedTypedTrustDependencies - admitted)) - , verificationTrustedVampireCount = - Set.size - (Legacy.legacyTrustedVampireUses trust) - + Transition.transitionAdmittedTypedTrustedVampireCount - admitted - , verificationExplicitGapLocations = - Legacy.legacyGapLocations trust - , verificationTrustedLegacyRuleCount = - Set.size - (Legacy.trustedLegacyRuleUses trust) - , verificationKernelProofCount = - Transition.transitionAdmittedKernelProofCount - admitted + { verificationDirectEscapes = + concatMap admittedModuleEscapes modules } + +admittedModuleEscapes + :: AdmittedTypedModule + -> [ReportedEscape] +admittedModuleEscapes (AdmittedTypedModule declarations) = + concatMap admittedDeclarationEscapes declarations + +admittedDeclarationEscapes + :: AdmittedTypedDeclaration + -> [ReportedEscape] +admittedDeclarationEscapes + (AdmittedTypedDeclaration _slot declaration) = + axiomEscape <> proofEscapes where - trust = - Legacy.legacyAdmittedTrustDependencies - (Transition.transitionAdmittedLegacyModule - admitted) + 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 verify :: (MonadUnliftIO io, MonadLogger io) @@ -1825,58 +1896,19 @@ verify verify prover file = fmap fst <$> verifyMeasured prover file -exportHtml :: MonadUnliftIO io => FilePath -> io Text -exportHtml file = - HtmlExport.preparedHtmlRootDocument - <$> prepareDefaultHtmlExport file - -prepareHtmlExport - :: MonadUnliftIO io - => FilePath - -> io PreparedHtmlBundle -prepareHtmlExport file = - prepareHtmlExportResult file - >>= either throwIO pure - -prepareHtmlExportResult - :: MonadUnliftIO io - => FilePath - -> io (Either HtmlExport.HtmlExportError PreparedHtmlBundle) -prepareHtmlExportResult file = - fmap HtmlExport.preparedHtmlOutputBundle - <$> prepareDefaultHtmlExportResult file - -prepareDefaultHtmlExport - :: MonadUnliftIO io - => FilePath - -> io HtmlExport.PreparedHtmlExport -prepareDefaultHtmlExport file = do - result <- prepareDefaultHtmlExportResult file - either throwIO pure result - -prepareDefaultHtmlExportResult - :: MonadUnliftIO io - => FilePath - -> io (Either HtmlExport.HtmlExportError HtmlExport.PreparedHtmlExport) -prepareDefaultHtmlExportResult file = do - hintsResult <- liftIO (findAndReadRendererFile "lexicon.tsv") - case hintsResult of - Left failure -> - pure (Left failure) - Right hints -> do - prepared <- liftIO (prepareDefaultSourceRequest file) - case prepared of - Left parseFailure -> - pure - (Left - (HtmlExport.HtmlExportParseError parseFailure)) - Right (mounts, request) -> - liftIO - (HtmlExport.prepareHtmlExport - defaultHtmlMountPrefixes - mounts - request - hints) +prepareVerifiedHtmlExportResult + :: MonadIO io + => VerificationPresentation + -> io (Either HtmlExport.HtmlExportError [PreparedHtmlArtifact]) +prepareVerifiedHtmlExportResult + (VerificationPresentation workspace) = liftIO do + hintsResult <- findAndReadRendererFile "lexicon.tsv" + pure do + hints <- hintsResult + HtmlExport.prepareHtmlExport + defaultHtmlMountPrefixes + workspace + hints defaultHtmlMountPrefixes :: [(SourceMountId, [Text])] defaultHtmlMountPrefixes = |