diff options
Diffstat (limited to 'source/Checking/Declaration.hs')
| -rw-r--r-- | source/Checking/Declaration.hs | 6543 |
1 files changed, 0 insertions, 6543 deletions
diff --git a/source/Checking/Declaration.hs b/source/Checking/Declaration.hs deleted file mode 100644 index 65b7675..0000000 --- a/source/Checking/Declaration.hs +++ /dev/null @@ -1,6543 +0,0 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE NoImplicitPrelude #-} -{-# LANGUAGE RankNTypes #-} - --- | Builder-confined authorization and atomic typed declaration append. -module Checking.Declaration - ( ModuleDriver - , DriverFailure(..) - , DriverResult(..) - , ImportedModuleEvidence - , ImportedAliasOrigin(..) - , freshImportedModuleEvidence - , validateImportedModuleEvidence - , importSealedModule - , importSealedModuleDriver - , nextDeclarationSlotDriver - , currentTheoryDriver - , currentFoundationAxiomDriver - , resolveVisibleFactAliasDriver - , resolveVisibleFactTargetsDriver - , resolveVisibleGlobalDriver - , resolveVisibleGlobalContentDriver - , ResolvedStructure - , resolvedStructureDescriptor - , resolvedStructurePredicate - , resolvedStructureOperation - , resolvedStructureOperations - , resolveVisibleStructureDriver - , resolveVisibleStructureOperationObjectsDriver - , objectAvailableDriver - , objectTypeDriver - , LoweringDriver - , runProspectiveLoweringDriver - , nextDeclarationSlotLowering - , currentTheoryLowering - , currentFoundationAxiomLowering - , resolveVisibleFactAliasLowering - , resolveVisibleFactTargetsLowering - , resolveVisibleGlobalLowering - , resolveVisibleGlobalContentLowering - , resolveVisibleStructureLowering - , resolveVisibleStructureOperationObjectsLowering - , objectAvailableLowering - , objectTypeLowering - , runModuleDriver - , ValidationLookup - , validationLookup - , ValidationRun(..) - , failModuleDriver - , failDeclarationDriver - , VampireResolver - , vampireBatchResolver - , vampireBatchResolverWithPreparationObserver - , vampireResolver - , vampireSubmissionResolver - , Declaration - , failDeclaration - , addDeclarationObject - , addDeclarationProposition - , resolveVisibleGlobal - , stageSemanticGlobalBinding - , stageSemanticStructureDescriptor - , CandidateSpec - , candidateSpec - , CandidatePlanningSpec - , CheckedCandidate - , checkedCandidate - , checkedDefinitionEquationPlanning - , checkedSourceAxiomPlanning - , checkedDatatypePlanning - , checkedKernelPlanning - , checkedSourceProofPlanning - , checkedOmittedPlanning - , CheckedPlannedVampireRequest - , checkedPlannedVampireRequest - , plannedEarlierCandidate - , CheckedDeclaration - , checkedProofDeclaration - , checkedCompiledDeclaration - , admitCheckedDeclaration - , PlannedDeclaration - , planCheckedDeclaration - , admitPlannedCheckedDeclaration - , plannedDeclarationPreviousPrefix - , plannedDeclarationNextPrefix - , plannedDeclarationDelta - , PlanningIntegrityError(..) - , prepareCandidateSpecDriver - , prepareFrozenCandidateSpecDriver - , prepareDefinitionEquationSpecDriver - , preparePointwiseDefinitionEquationSpecDriver - , prepareStagedCandidateVampireDriver - , prepareCandidateSpecLowering - , prepareFrozenCandidateSpecLowering - , prepareDefinitionEquationSpecLowering - , preparePointwiseDefinitionEquationSpecLowering - , prepareStagedCandidateVampireLowering - , ReservedCandidate - , reserveCandidate - , reserveCandidateBatch - , reservePropositionCandidate - , reserveFrozenPropositionCandidateBatch - , reserveDefinitionEquationCandidate - , reservePointwiseDefinitionEquationCandidate - , reserveDefinitionEquationCandidateBatch - , reservedCandidateSlot - , reservedCandidateStage - , CandidateProof - , locateProofObligation - , recordOmittedUse - , VampirePremiseSelection(..) - , VampireObligationPreparationError(..) - , ScopedVampirePremise - , scopedVampirePremise - , PreparedVampireObligation - , prepareScopedVampireObligationDriver - , prepareScopedContradictionObligationDriver - , prepareScopedVampireObligationLowering - , prepareScopedContradictionObligationLowering - , useAuthorizedFact - , useStagedCandidate - , LocalClaim - , proveLocalKernelClaim - , useLocalClaim - , authorizeKernelProofCandidate - , authorizeKernelConstructionCandidate - , authorizeDefinitionEquationCandidate - , acceptVampireObligation - , acceptPreparedVampireObligation - , acceptCurrentCandidateVampire - , prepareCurrentCandidateVampire - , authorizeVampireCandidate - , authorizeVampireCandidateBatch - , authorizeSourceAxiomCandidate - , authorizeOmittedCandidate - , authorizeDatatypeCompilationCandidates - , authorizeCompiledDeclaration - , commitProofDeclaration - , commitCompiledDeclaration - , CommittedDeclarationBatch - , committedBatchOwner - , committedBatchSlot - , committedBatchPreviousPrefix - , committedBatchNextPrefix - , committedBatchDelta - , committedBatchObjects - , committedBatchPropositions - , committedBatchProofValidations - , committedBatchDeclarationValidation - , PendingModulePrefix - , emptyPendingModulePrefix - , pendingModulePrefixBatches - , pendingModulePrefixCurrent - , ValidationIntegrityError(..) - , renderValidationIntegrityError - , DeclarationError(..) - , declarationErrorLocation - , renderDeclarationError - , DriverOpenError(..) - , renderDriverOpenError - ) where - -import Base -import Checking.Authority -import Checking.Backend.Problem qualified as Backend -import Checking.Backend.Tptp qualified as Tptp -import Checking.Core -import Checking.Foundation -import Checking.Identity -import Checking.Kernel.Derivation -import Checking.Semantic -import Checking.Materialization qualified as Materialization -import Felix.Cache.Codec (encodeCache) -import Felix.Module -import Provers qualified -import Report.Location -import Syntax.Abstract (StructSymbol) - -import Control.Exception qualified as Exception -import Control.DeepSeq (deepseq) -import Control.Monad.Except (ExceptT) -import Control.Monad.Except qualified as Except -import Control.Monad (foldM, unless, when) -import Control.Monad.State.Strict (StateT) -import Control.Monad.State.Strict qualified as State -import Data.Bifunctor (first) -import Data.ByteString qualified as ByteString -import Data.List qualified as List -import Data.List.NonEmpty qualified as NonEmpty -import Data.Map.Strict qualified as Map -import Data.Maybe (catMaybes, mapMaybe) -import Data.Set qualified as Set -import Data.Text qualified as Text -import Data.Unique (Unique, newUnique) -import Data.IORef (IORef, atomicModifyIORef', newIORef, readIORef) -import Data.Vector (Vector) -import Data.Vector qualified as Vector -import Numeric.Natural (Natural) - - -newtype BuilderIdentity = BuilderIdentity Unique - deriving stock (Eq) - -newtype DeclarationInvocation = DeclarationInvocation Natural - deriving stock (Eq) - -newtype CandidateStage = CandidateStage Natural - deriving stock (Show, Eq, Ord) - -data ValidationLookup = ValidationLookup - !(ProofValidationKey -> IO (Maybe ProofValidationRecord)) - !(DeclarationValidationKey - -> IO (Maybe DeclarationValidationRecord)) - -validationLookup - :: (ProofValidationKey -> IO (Maybe ProofValidationRecord)) - -> (DeclarationValidationKey - -> IO (Maybe DeclarationValidationRecord)) - -> ValidationLookup -validationLookup = - ValidationLookup - -data ValidationRun - = FreshValidation - | WarmValidation !ValidationLookup - -data ValidationIntegrityError - = CachedValidationIntegrityError - !Materialization.MaterializationError - deriving stock (Show, Eq) - -instance Exception.Exception ValidationIntegrityError - -renderValidationIntegrityError :: ValidationIntegrityError -> Text -renderValidationIntegrityError = \case - CachedValidationIntegrityError failure -> - "cached validation does not match its exact contextual input: " - <> Text.pack (show failure) - - -data BuilderFactAuthorization = BuilderFactAuthorization - !BuilderIdentity - !FactSlot - !FactAuthority - -data PendingFactAuthorization = PendingFactAuthorization - !BuilderIdentity - !PrefixContextId - !DeclarationInvocation - !FactSlot - !FactAuthority - !CandidateStage - --- | Checked fact semantics paired with caller-selected evidence. Semantic --- lookup and request preparation deliberately ignore the evidence parameter; --- only the admitted builder instantiation may consume capabilities. -data FactEntry evidence = FactEntry - !CheckedPropositionContent - !SemanticFactOccurrence - !evidence - --- | The shared checked semantic state. The evidence parameter makes the --- distinction between admitted authority and future inert planning data --- visible without duplicating lookup, collision, closure, or delta logic. -data BuilderState evidence = BuilderState - { logicalBuilderIdentity :: !BuilderIdentity - , logicalBuilderFoundation :: !CheckedFoundation - , logicalBuilderTheory :: !TheoryId - , logicalBuilderOwner :: !ModuleName - , logicalBuilderDirectSemanticInputs :: ![SemanticInterfaceId] - , logicalBuilderPrefix :: !PrefixContextId - , logicalBuilderObjectClosure :: !CheckedObjectClosure - , logicalBuilderFacts - :: !(Map - SemanticFactOccurrenceFingerprint - (FactEntry evidence)) - , logicalBuilderAliases - :: !(Map SemanticName ImportedAliasBinding) - , logicalBuilderGlobals - :: !(Map SemanticGlobalKey SemanticGlobalTarget) - , logicalBuilderStructures - :: !(Map SemanticStructurePhrase ResolvedStructure) - , logicalBuilderImportedInterfaces :: !(Set SemanticInterfaceId) - , logicalBuilderDeltas :: ![DeclarationInterfaceDelta] - , logicalBuilderNextDeclaration :: !Natural - , logicalBuilderNextFact :: !Natural - , logicalBuilderNextInvocation :: !Natural - } - --- | The only production builder in this milestone. Capability-consuming --- operations below accept this admitted instantiation, never a polymorphic --- 'BuilderState'. -type LogicalBuilder = BuilderState BuilderFactAuthorization - --- | Public semantic contract and strict declaration-stage provenance for a --- prospective fact. It deliberately contains no builder identity, prefix, --- declaration invocation, pending authorization, or minting capability. -data PlanningProvenance = PlanningProvenance - !DeclarationSlot - !CandidateStage - !FactSlot - deriving stock (Eq) - -data PlanningEvidence = PlanningEvidence - !FactAuthority - !(Maybe PlanningProvenance) - -data ResolvedStructureOperation = ResolvedStructureOperation - !ObjectId - !SemanticStructurePhrase - deriving stock (Show, Eq) - -data ResolvedStructure = ResolvedStructure - !SemanticStructureDescriptor - !(Set SemanticStructurePhrase) - !(Map StructSymbol ResolvedStructureOperation) - deriving stock (Show, Eq) - -resolvedStructureDescriptor - :: ResolvedStructure - -> SemanticStructureDescriptor -resolvedStructureDescriptor (ResolvedStructure descriptor _ _) = - descriptor - -resolvedStructurePredicate :: ResolvedStructure -> Maybe ObjectId -resolvedStructurePredicate = - semanticStructureDescriptorPredicate . resolvedStructureDescriptor - -resolvedStructureOperation - :: StructSymbol - -> ResolvedStructure - -> Maybe ObjectId -resolvedStructureOperation symbol (ResolvedStructure _ _ operations) = - operationObject <$> Map.lookup symbol operations - where - operationObject (ResolvedStructureOperation object _origin) = object - -resolvedStructureOperations - :: ResolvedStructure - -> Map StructSymbol ObjectId -resolvedStructureOperations (ResolvedStructure _ _ operations) = - operationObject <$> operations - where - operationObject (ResolvedStructureOperation object _origin) = object - -structureOperationBindings - :: Map SemanticStructurePhrase ResolvedStructure - -> Set (StructSymbol, ObjectId) -structureOperationBindings structures = - Set.fromList - [ (symbol, object) - | structure <- Map.elems structures - , (symbol, object) <- - Map.toAscList (resolvedStructureOperations structure) - ] - - -data CommittedDeclarationBatch = CommittedDeclarationBatch - !ModuleName - !DeclarationSlot - !PrefixContextId - !PrefixContextId - !DeclarationInterfaceDelta - ![AssertedObject] - ![CheckedPropositionContent] - ![ProofValidationRecord] - !(Maybe DeclarationValidationRecord) - -committedBatchOwner :: CommittedDeclarationBatch -> ModuleName -committedBatchOwner - (CommittedDeclarationBatch owner _ _ _ _ _ _ _ _) = - owner - -committedBatchSlot - :: CommittedDeclarationBatch - -> DeclarationSlot -committedBatchSlot - (CommittedDeclarationBatch _ slot _ _ _ _ _ _ _) = - slot - -committedBatchPreviousPrefix - :: CommittedDeclarationBatch - -> PrefixContextId -committedBatchPreviousPrefix - (CommittedDeclarationBatch _ _ previous _ _ _ _ _ _) = - previous - -committedBatchNextPrefix - :: CommittedDeclarationBatch - -> PrefixContextId -committedBatchNextPrefix - (CommittedDeclarationBatch _ _ _ next _ _ _ _ _) = - next - -committedBatchDelta - :: CommittedDeclarationBatch - -> DeclarationInterfaceDelta -committedBatchDelta - (CommittedDeclarationBatch _ _ _ _ delta _ _ _ _) = - delta - -committedBatchObjects - :: CommittedDeclarationBatch - -> [AssertedObject] -committedBatchObjects - (CommittedDeclarationBatch _ _ _ _ _ objects _ _ _) = - objects - -committedBatchPropositions - :: CommittedDeclarationBatch - -> [CheckedPropositionContent] -committedBatchPropositions - (CommittedDeclarationBatch _ _ _ _ _ _ propositions _ _) = - propositions - -committedBatchProofValidations - :: CommittedDeclarationBatch - -> [ProofValidationRecord] -committedBatchProofValidations - (CommittedDeclarationBatch _ _ _ _ _ _ _ validations _) = - validations - -committedBatchDeclarationValidation - :: CommittedDeclarationBatch - -> Maybe DeclarationValidationRecord -committedBatchDeclarationValidation - (CommittedDeclarationBatch _ _ _ _ _ _ _ _ validation) = - validation - - -data PendingModulePrefix = PendingModulePrefix - !PrefixContextId - ![CommittedDeclarationBatch] - -emptyPendingModulePrefix - :: PrefixContextId - -> PendingModulePrefix -emptyPendingModulePrefix prefix = - PendingModulePrefix prefix [] - -instance Show PendingModulePrefix where - show prefix = - "PendingModulePrefix {pendingModulePrefixCurrent = " - <> show (pendingModulePrefixCurrent prefix) - <> ", pendingModulePrefixBatchCount = " - <> show (length (pendingModulePrefixBatches prefix)) - <> "}" - -pendingModulePrefixBatches - :: PendingModulePrefix - -> [CommittedDeclarationBatch] -pendingModulePrefixBatches - (PendingModulePrefix _ batchesReversed) = - reverse batchesReversed - -pendingModulePrefixCurrent - :: PendingModulePrefix - -> PrefixContextId -pendingModulePrefixCurrent - (PendingModulePrefix prefix _batches) = - prefix - -appendPendingBatch - :: CommittedDeclarationBatch - -> PendingModulePrefix - -> PendingModulePrefix -appendPendingBatch batch (PendingModulePrefix _ batches) = - forceCommittedBatch batch `seq` - PendingModulePrefix - (committedBatchNextPrefix batch) - (batch : batches) - -forceCommittedBatch :: CommittedDeclarationBatch -> () -forceCommittedBatch - (CommittedDeclarationBatch - owner slot previous next delta objects propositions - proofValidations declarationValidation) = - owner `seq` - slot `seq` - previous `seq` - next `seq` - ByteString.length - (encodeCache (putDeclarationInterfaceDeltaCache delta)) `seq` - objects `deepseq` - propositions `deepseq` - forceProofValidations proofValidations `seq` - forceDeclarationValidation declarationValidation - where - forceProofValidations = - foldl' - (\() record -> - proofValidationRecordKey record `seq` - ByteString.length - (encodeCache - (putValidationCertificateCache - (proofValidationRecordCertificate - record))) `seq` ()) - () - - forceDeclarationValidation = \case - Nothing -> () - Just record -> - declarationValidationRecordKey record `seq` - foldl' - (\() certificate -> - ByteString.length - (encodeCache - (putValidationCertificateCache - certificate)) `seq` ()) - () - (declarationValidationRecordCertificates record) - - -data VampireResolverMode - = SynchronousVampireResolution - (forall local origin. - NonEmpty - (Provers.PreparedTypedProverTask - SemanticFactOccurrenceFingerprint - local - origin - ObjectId) - -> IO - (NonEmpty - (Either - Provers.ProverProcessError - Provers.ProverAnswer))) - | AsynchronousVampireSubmission - (NonEmpty Provers.PreparedVerificationRequest - -> IO (NonEmpty Provers.VampireHandle)) - -data VampireResolver = VampireResolver - !VampireResolverMode - !(Word64 -> IO ()) - -vampireBatchResolver - :: (forall local origin. - NonEmpty - (Provers.PreparedTypedProverTask - SemanticFactOccurrenceFingerprint - local - origin - ObjectId) - -> IO - (NonEmpty - (Either - Provers.ProverProcessError - Provers.ProverAnswer))) - -> VampireResolver -vampireBatchResolver resolve = - vampireBatchResolverWithPreparationObserver resolve (const (pure ())) - -vampireBatchResolverWithPreparationObserver - :: (forall local origin. - NonEmpty - (Provers.PreparedTypedProverTask - SemanticFactOccurrenceFingerprint - local - origin - ObjectId) - -> IO - (NonEmpty - (Either - Provers.ProverProcessError - Provers.ProverAnswer))) - -> (Word64 -> IO ()) - -> VampireResolver -vampireBatchResolverWithPreparationObserver resolve observe = - VampireResolver (SynchronousVampireResolution resolve) observe - --- | Production submission-only resolver. Retained-plan admission consumes --- the submitted handles through its private synchronous replay resolver. -vampireSubmissionResolver - :: (NonEmpty Provers.PreparedVerificationRequest - -> IO (NonEmpty Provers.VampireHandle)) - -> (Word64 -> IO ()) - -> VampireResolver -vampireSubmissionResolver submit observe = - VampireResolver (AsynchronousVampireSubmission submit) observe - -vampireResolver - :: (forall local origin. - Provers.PreparedTypedProverTask - SemanticFactOccurrenceFingerprint - local - origin - ObjectId - -> IO - (Either - Provers.ProverProcessError - Provers.ProverAnswer)) - -> VampireResolver -vampireResolver resolve = - vampireBatchResolver (traverse resolve) - -resolveOneVampire - :: VampireResolver - -> Provers.PreparedTypedProverTask - SemanticFactOccurrenceFingerprint - local - origin - ObjectId - -> ExceptT DeclarationError IO - (Either - Provers.ProverProcessError - Provers.ProverAnswer) -resolveOneVampire resolver prepared = do - results@(result :| _) <- - liftIO (resolveSynchronousVampireBatch resolver (prepared :| [])) - void - (Except.liftEither - (validateVampireResolverResultCount 1 results)) - pure result - -resolveSynchronousVampireBatch - :: VampireResolver - -> NonEmpty - (Provers.PreparedTypedProverTask - SemanticFactOccurrenceFingerprint - local - origin - ObjectId) - -> IO - (NonEmpty - (Either - Provers.ProverProcessError - Provers.ProverAnswer)) -resolveSynchronousVampireBatch - (VampireResolver mode _observe) tasks = - case mode of - SynchronousVampireResolution resolve -> resolve tasks - AsynchronousVampireSubmission{} -> - throwIO - (PlanningIntegrityError - "asynchronous Vampire resolver reached synchronous admission") - -observeVampirePreparation - :: VampireResolver - -> Word64 - -> IO () -observeVampirePreparation (VampireResolver _mode observe) = observe - -validateVampireResolverResultCount - :: Int - -> NonEmpty value - -> Either DeclarationError [value] -validateVampireResolverResultCount expected results - | expected == actual = - Right (NonEmpty.toList results) - | otherwise = - Left (VampireResolverBatchSizeMismatch expected actual) - where - actual = NonEmpty.length results - -data DriverState = DriverState - !VampireResolver - !LogicalBuilder - !PendingModulePrefix - !ValidationRun - --- | Authority-free semantic state used while lowering checked declarations. --- Existing admitted facts are projected to their public contracts; no --- builder-local authorization capability crosses this boundary. -newtype ProspectiveBuilder = ProspectiveBuilder - (BuilderState PlanningEvidence) - -data LoweringState = LoweringState - !VampireResolver - !ProspectiveBuilder - !ValidationRun - -newtype LoweringDriver value = LoweringDriver - { runLoweringStep :: StateT LoweringState IO value - } - deriving newtype (Functor, Applicative, Monad) - -newtype ModuleDriver failure value = ModuleDriver - { runDriverStep - :: ExceptT - (DriverFailure failure) - (StateT DriverState IO) - value - } - deriving newtype (Functor, Applicative, Monad) - --- | Run one complete authority-free planning action from the current admitted --- input projection. The prospective state advances throughout the action but --- never mutates the authoritative module builder. -runProspectiveLoweringDriver - :: LoweringDriver value - -> ModuleDriver failure value -runProspectiveLoweringDriver action = ModuleDriver do - DriverState resolver builder _prefix validation <- State.get - State.lift - (liftIO - (State.evalStateT - (runLoweringStep action) - (LoweringState resolver - (projectLogicalBuilder builder) - validation))) - -projectLogicalBuilder :: LogicalBuilder -> ProspectiveBuilder -projectLogicalBuilder builder = - ProspectiveBuilder - builder - { logicalBuilderFacts = - fmap projectFact (logicalBuilderFacts builder) - } - where - projectFact (FactEntry proposition occurrence _authorization) = - FactEntry proposition occurrence - (PlanningEvidence - (semanticFactAuthority occurrence) - Nothing) - -data DriverFailure failure - = DriverDeclarationFailed !DeclarationError - | DriverActionFailed !failure - deriving stock (Show, Eq) - -data DriverResult failure value - = DriverSucceeded - !value - !SemanticInterface - !PendingModulePrefix - !CheckedObjectClosure - | DriverFailed - !(DriverFailure failure) - !PendingModulePrefix - | DriverSealFailed - !SemanticInterfaceError - !PendingModulePrefix - -data ImportedAliasOrigin = ImportedAliasOrigin - !DeclarationSlot - !SemanticFactOccurrenceFingerprint - deriving stock (Show, Eq) - -data ImportedAliasBinding = ImportedAliasBinding - !SemanticFactOccurrenceFingerprint - !ImportedAliasOrigin - --- | Opaque evidence produced from a successfully sealed producer. Direct --- parents retain the semantic DAG; importing folds it deterministically and --- mints fresh authority for the consuming builder. -data ImportedModuleEvidence = ImportedModuleEvidence - !SemanticInterface - ![ImportedModuleEvidence] - !(Map - SemanticFactOccurrenceFingerprint - (SemanticFactOccurrence, CheckedPropositionContent)) - ![AssertedObject] - -freshImportedModuleEvidence - :: [ImportedModuleEvidence] - -> SemanticInterface - -> PendingModulePrefix - -> ImportedModuleEvidence -freshImportedModuleEvidence parents interface prefix = - ImportedModuleEvidence - interface - parents - (Map.fromList - [ ( semanticFactFingerprint occurrence - , (occurrence, requireProposition occurrence) - ) - | occurrence <- occurrences - ]) - objects - where - batches = pendingModulePrefixBatches prefix - objects = concatMap committedBatchObjects batches - propositions = concatMap committedBatchPropositions batches - propositionMap = - Map.fromList - [ (checkedPropositionId proposition, proposition) - | proposition <- propositions - ] - occurrences = - concatMap - declarationDeltaFacts - (semanticInterfaceDeclarations interface) - - requireProposition occurrence = - case Map.lookup - (semanticFactProposition occurrence) - propositionMap of - Just proposition -> - proposition - Nothing -> - impossible - ("sealed fact occurrence references absent proposition " - <> show (semanticFactProposition occurrence)) - --- | Construct import evidence after a trusted producer or validated store --- installation has supplied the complete canonical proposition payloads. -validateImportedModuleEvidence - :: TheoryId - -> [ImportedModuleEvidence] - -> SemanticInterface - -> [AssertedObject] - -> [CheckedPropositionContent] - -> Either DeclarationError ImportedModuleEvidence -validateImportedModuleEvidence - theory parents interface objects propositions = do - _ <- first ImportedEvidenceInterfaceFailed - (validateSemanticInterface - (semanticInterfaceOwner interface) - (semanticInterfaceDirectInputs interface) - (semanticInterfaceDeclarations interface) - (semanticInterfaceAssertedId interface)) - unless - (semanticInterfaceDirectInputs interface == parentIds) - (Left - (ImportedEvidenceDirectMismatch - (semanticInterfaceDirectInputs interface) - parentIds)) - let propositionMap = - Map.fromList - [ (checkedPropositionId proposition, proposition) - | proposition <- propositions - ] - objectMap = - Map.fromList - [ (assertedObjectId object, object) - | object <- objects - ] - localObjectIds = - concatMap - declarationDeltaObjects - (semanticInterfaceDeclarations interface) - parentObjectMap = - foldl' - (Map.unionWith const) - Map.empty - (evidenceObjectMap <$> parents) - localObjects <- traverse - (\identity -> - maybe - (Left (ImportedEvidenceObjectMissing identity)) - Right - (Map.lookup identity objectMap)) - localObjectIds - closure <- first DeclarationObjectValidationFailed - (validateObjectClosure - theory - (Map.elems parentObjectMap <> localObjects)) - let occurrences = - concatMap - declarationDeltaFacts - (semanticInterfaceDeclarations interface) - pairs <- traverse - (\occurrence -> do - proposition <- maybe - (Left - (ImportedEvidencePropositionMissing - (semanticFactProposition occurrence))) - Right - (Map.lookup - (semanticFactProposition occurrence) - propositionMap) - _ <- first DeclarationPropositionValidationFailed - (validateAssertedPropositionContent - closure - (checkedPropositionId proposition) - (frozenCoreTerm - (checkedPropositionTerm proposition))) - _ <- first ImportedFactMaterializationFailed - (Materialization.checkImportedOccurrence - theory - (semanticFactFingerprint occurrence) - occurrence - proposition - (semanticFactAuthority occurrence)) - pure - ( semanticFactFingerprint occurrence - , (occurrence, proposition) - )) - occurrences - let evidence = - ImportedModuleEvidence - interface - parents - (Map.fromList pairs) - localObjects - _ <- validateEvidenceInventory theory closure evidence - pure evidence - where - parentIds = - semanticInterfaceAssertedId . evidenceInterface <$> parents - -validateEvidenceInventory - :: TheoryId - -> CheckedObjectClosure - -> ImportedModuleEvidence - -> Either DeclarationError () -validateEvidenceInventory theory closure evidence = - do - void (foldEvidence Set.empty Map.empty Map.empty evidence) - (_seen, structures) <- - foldStructures Set.empty Map.empty evidence - void (foldGlobals structures Set.empty Map.empty evidence) - where - foldEvidence seen facts aliases current - | identity `Set.member` seen = - Right (seen, facts, aliases) - | otherwise = do - unless - (semanticInterfaceDirectInputs interface == parentIds) - (Left - (ImportedEvidenceDirectMismatch - (semanticInterfaceDirectInputs interface) - parentIds)) - (parentsSeen, parentFacts, parentAliases) <- - foldM - (\(seen', facts', aliases') parent -> - foldEvidence seen' facts' aliases' parent) - (seen, facts, aliases) - parents - localFacts <- foldM insertFact parentFacts (Map.elems entries) - localAliases <- foldM - (insertAlias localFacts) - parentAliases - [ ( alias - , ImportedAliasOrigin - (declarationDeltaSlot delta) - (semanticAliasTarget alias) - ) - | delta <- semanticInterfaceDeclarations interface - , alias <- declarationDeltaAliases delta - ] - pure - ( Set.insert identity parentsSeen - , localFacts - , localAliases - ) - where - ImportedModuleEvidence interface parents entries _objects = current - identity = semanticInterfaceAssertedId interface - parentIds = - semanticInterfaceAssertedId . evidenceInterface <$> parents - - insertFact facts pair@(occurrence, proposition) = do - let fingerprint = semanticFactFingerprint occurrence - _ <- first ImportedFactMaterializationFailed - (Materialization.checkImportedOccurrence - theory - fingerprint - occurrence - proposition - (semanticFactAuthority occurrence)) - case Map.lookup fingerprint facts of - Nothing -> - Right (Map.insert fingerprint pair facts) - Just (existingOccurrence, existingProposition) - | existingOccurrence == occurrence - && checkedPropositionId existingProposition - == checkedPropositionId proposition -> - Right facts - | otherwise -> - Left (ImportedFactCollision fingerprint) - - insertAlias facts aliases (alias, origin) = do - let name = semanticAliasName alias - target = semanticAliasTarget alias - unless - (Map.member target facts) - (Left (ImportedAliasTargetMissing target)) - case Map.lookup name aliases of - Nothing -> - Right - (Map.insert - name - (ImportedAliasBinding target origin) - aliases) - Just (ImportedAliasBinding existingTarget existingOrigin) - | existingTarget == target -> - Right aliases - | otherwise -> - Left - (ImportedAliasCollision - name existingOrigin origin) - - foldGlobals structures seen globals current - | identity `Set.member` seen = - Right (seen, globals) - | otherwise = do - (parentsSeen, parentGlobals) <- - foldM - (\(seen', globals') parent -> - foldGlobals structures seen' globals' parent) - (seen, globals) - parents - globals' <- - foldM - (insertGlobal - (structureOperationBindings structures)) - parentGlobals - [ binding - | delta <- semanticInterfaceDeclarations interface - , binding <- semanticEnvironmentBindings - (declarationDeltaEnvironment delta) - ] - pure (Set.insert identity parentsSeen, globals') - where - ImportedModuleEvidence interface parents _entries _objects = current - identity = semanticInterfaceAssertedId interface - - insertGlobal operationBindings globals binding = do - let key = semanticGlobalBindingKey binding - target = semanticGlobalBindingTarget binding - _ <- - first - (ImportedGlobalTargetInvalid key target) - (validateSemanticGlobalBindingTarget - operationBindings - closure binding) - case Map.lookup key globals of - Nothing -> Right (Map.insert key target globals) - Just existing - | existing == target -> Right globals - | otherwise -> - Left (ImportedGlobalCollision key existing target) - - foldStructures seen structures current - | identity `Set.member` seen = - Right (seen, structures) - | otherwise = do - (parentsSeen, parentStructures) <- - foldM - (\(seen', structures') parent -> - foldStructures seen' structures' parent) - (seen, structures) - parents - structures' <- - foldM - (insertSemanticStructure closure) - parentStructures - [ descriptor - | delta <- semanticInterfaceDeclarations interface - , descriptor <- semanticEnvironmentStructures - (declarationDeltaEnvironment delta) - ] - pure (Set.insert identity parentsSeen, structures') - where - ImportedModuleEvidence interface parents _entries _objects = current - identity = semanticInterfaceAssertedId interface - -evidenceInterface :: ImportedModuleEvidence -> SemanticInterface -evidenceInterface - (ImportedModuleEvidence interface _parents _entries _objects) = - interface - -evidenceObjectMap - :: ImportedModuleEvidence - -> Map ObjectId AssertedObject -evidenceObjectMap - (ImportedModuleEvidence _interface parents _entries objects) = - foldl' - (Map.unionWith const) - (Map.fromList - [ (assertedObjectId object, object) - | object <- objects - ]) - (evidenceObjectMap <$> parents) - -data DriverOpenError - = DriverInitialPrefixError !PrefixContextError - | DriverInitialObjectError !ObjectValidationError - deriving stock (Show, Eq) - -renderDriverOpenError :: DriverOpenError -> Text -renderDriverOpenError = \case - DriverInitialPrefixError{} -> - "the initial semantic prefix is inconsistent" - DriverInitialObjectError{} -> - "the initial object closure is inconsistent" - -runModuleDriver - :: CheckedFoundation - -> ModuleName - -> [SemanticInterfaceId] - -> VampireResolver - -> ValidationRun - -> ModuleDriver failure value - -> IO - (Either - DriverOpenError - (DriverResult failure value)) -runModuleDriver - foundation owner direct resolver validationRun action = do - unique <- BuilderIdentity <$> newUnique - let theory = theoryId foundation - case (,) <$> - first DriverInitialPrefixError - (initialPrefixContextId theory owner direct) - <*> - first DriverInitialObjectError - (validateObjectClosure theory []) of - Left err -> - pure (Left err) - Right (prefix, closure) -> do - let builder = - BuilderState - { logicalBuilderIdentity = unique - , logicalBuilderFoundation = foundation - , logicalBuilderTheory = theory - , logicalBuilderOwner = owner - , logicalBuilderDirectSemanticInputs = direct - , logicalBuilderPrefix = prefix - , logicalBuilderObjectClosure = closure - , logicalBuilderFacts = Map.empty - , logicalBuilderAliases = Map.empty - , logicalBuilderGlobals = Map.empty - , logicalBuilderStructures = Map.empty - , logicalBuilderImportedInterfaces = Set.empty - , logicalBuilderDeltas = [] - , logicalBuilderNextDeclaration = 0 - , logicalBuilderNextFact = 0 - , logicalBuilderNextInvocation = 0 - } - initialState = - DriverState - resolver - builder - (PendingModulePrefix prefix []) - validationRun - (result, DriverState _ finalBuilder finalPrefix _) <- - State.runStateT - (Except.runExceptT - (runDriverStep action)) - initialState - case result of - Left err -> - pure (Right (DriverFailed err finalPrefix)) - Right value -> do - case semanticInterface - owner - direct - (reverse - (logicalBuilderDeltas - finalBuilder)) of - Left err -> - pure - (Right - (DriverSealFailed - err - finalPrefix)) - Right interface -> - pure - (Right - (DriverSucceeded - value - interface - finalPrefix - (logicalBuilderObjectClosure - finalBuilder))) - -failModuleDriver :: failure -> ModuleDriver failure value -failModuleDriver err = - ModuleDriver - (Except.throwError - (DriverActionFailed err)) - -failDeclarationDriver :: DeclarationError -> ModuleDriver failure value -failDeclarationDriver err = - ModuleDriver (Except.throwError (DriverDeclarationFailed err)) - -nextDeclarationSlotDriver - :: ModuleDriver failure DeclarationSlot -nextDeclarationSlotDriver = ModuleDriver do - DriverState _resolver builder _prefix _validation <- State.get - pure - (declarationSlot - (logicalBuilderOwner builder) - (localDeclarationOrdinal - (logicalBuilderNextDeclaration builder))) - -currentTheoryDriver :: ModuleDriver failure TheoryId -currentTheoryDriver = - ModuleDriver - (State.gets - (\(DriverState _resolver builder _prefix _validation) -> - logicalBuilderTheory builder)) - -currentFoundationAxiomDriver - :: FoundationAxiomTag - -> ModuleDriver failure (FrozenCheckedCore Void) -currentFoundationAxiomDriver tag = - ModuleDriver - (State.gets - (\(DriverState _resolver builder _prefix _validation) -> - foundationAxiomFrozen - (logicalBuilderFoundation builder) - tag)) - -resolveVisibleFactAliasDriver - :: SemanticName - -> ModuleDriver failure - (Maybe SemanticFactOccurrenceFingerprint) -resolveVisibleFactAliasDriver alias = ModuleDriver do - DriverState _resolver builder _prefix _validation <- State.get - pure do - ImportedAliasBinding fingerprint _origin <- - Map.lookup alias (logicalBuilderAliases builder) - pure fingerprint - -resolveVisibleFactTargetsDriver - :: FrozenCheckedCore ObjectId - -> ModuleDriver failure - [SemanticFactOccurrenceFingerprint] -resolveVisibleFactTargetsDriver target = ModuleDriver do - DriverState _resolver builder _prefix _validation <- State.get - pure - [ fingerprint - | (fingerprint, FactEntry proposition _occurrence _authorization) <- - Map.toAscList (logicalBuilderFacts builder) - , checkedPropositionTerm proposition == target - ] - -resolveVisibleGlobalDriver - :: SemanticGlobalKey - -> ModuleDriver failure (Maybe (SemanticGlobalTarget, CoreType)) -resolveVisibleGlobalDriver key = ModuleDriver do - DriverState _resolver builder _prefix _validation <- State.get - pure - ( (\(target, _content, _dependencies) -> - ( target - , fromMaybe - (impossible "visible semantic key has no source type") - (semanticGlobalKeyType key) - )) - <$> resolveVisibleGlobalContent builder key - ) - -resolveVisibleGlobalContentDriver - :: SemanticGlobalKey - -> ModuleDriver failure - (Maybe - ( SemanticGlobalTarget - , ObjectContent - , Map ObjectId CoreType - )) -resolveVisibleGlobalContentDriver key = ModuleDriver do - DriverState _resolver builder _prefix _validation <- State.get - pure (resolveVisibleGlobalContent builder key) - -resolveVisibleStructureDriver - :: SemanticStructurePhrase - -> ModuleDriver failure (Maybe ResolvedStructure) -resolveVisibleStructureDriver structurePhrase = ModuleDriver do - DriverState _resolver builder _prefix _validation <- State.get - pure (Map.lookup structurePhrase (logicalBuilderStructures builder)) - -resolveVisibleStructureOperationObjectsDriver - :: StructSymbol - -> ModuleDriver failure [ObjectId] -resolveVisibleStructureOperationObjectsDriver symbol = ModuleDriver do - DriverState _resolver builder _prefix _validation <- State.get - pure - ( Set.toAscList - (Set.fromList - (mapMaybe - (resolvedStructureOperation symbol) - (Map.elems (logicalBuilderStructures builder)))) - ) - -resolveVisibleGlobalContent - :: BuilderState evidence - -> SemanticGlobalKey - -> Maybe - ( SemanticGlobalTarget - , ObjectContent - , Map ObjectId CoreType - ) -resolveVisibleGlobalContent builder key = do - target <- Map.lookup key (logicalBuilderGlobals builder) - content <- - lookupCheckedObjectContent - (semanticGlobalTargetObject target) - closure - let dependencies = - Map.fromList - [ (identity, requireDependency identity) - | identity <- case content of - TransparentObjectContent _theory _coreType body -> - Set.toAscList (canonicalTermGlobals body) - _ -> [] - ] - pure - ( target - , content - , dependencies - ) - where - closure = logicalBuilderObjectClosure builder - - requireDependency identity = - case lookupCheckedObjectType identity closure of - Just coreType -> coreType - Nothing -> - impossible "checked object dependency is absent" - -objectAvailableDriver - :: ObjectId - -> ModuleDriver failure Bool -objectAvailableDriver identity = - ModuleDriver - (State.gets - (\(DriverState _resolver builder _prefix _validation) -> - isJust - (lookupCheckedObjectType - identity - (logicalBuilderObjectClosure builder)))) - -objectTypeDriver - :: ObjectId - -> ModuleDriver failure (Maybe CoreType) -objectTypeDriver identity = - ModuleDriver - (State.gets - (\(DriverState _resolver builder _prefix _validation) -> - lookupCheckedObjectType - identity - (logicalBuilderObjectClosure builder))) - -nextDeclarationSlotLowering :: LoweringDriver DeclarationSlot -nextDeclarationSlotLowering = - withLoweringBuilder \builder -> - declarationSlot - (logicalBuilderOwner builder) - (localDeclarationOrdinal - (logicalBuilderNextDeclaration builder)) - -currentTheoryLowering :: LoweringDriver TheoryId -currentTheoryLowering = - withLoweringBuilder logicalBuilderTheory - -currentFoundationAxiomLowering - :: FoundationAxiomTag - -> LoweringDriver (FrozenCheckedCore Void) -currentFoundationAxiomLowering tag = - withLoweringBuilder - (\builder -> - foundationAxiomFrozen - (logicalBuilderFoundation builder) - tag) - -resolveVisibleFactAliasLowering - :: SemanticName - -> LoweringDriver (Maybe SemanticFactOccurrenceFingerprint) -resolveVisibleFactAliasLowering alias = - withLoweringBuilder \builder -> do - ImportedAliasBinding fingerprint _origin <- - Map.lookup alias (logicalBuilderAliases builder) - pure fingerprint - -resolveVisibleFactTargetsLowering - :: FrozenCheckedCore ObjectId - -> LoweringDriver [SemanticFactOccurrenceFingerprint] -resolveVisibleFactTargetsLowering target = - withLoweringBuilder \builder -> - [ fingerprint - | (fingerprint, FactEntry proposition _occurrence _evidence) <- - Map.toAscList (logicalBuilderFacts builder) - , checkedPropositionTerm proposition == target - ] - -resolveVisibleGlobalLowering - :: SemanticGlobalKey - -> LoweringDriver (Maybe (SemanticGlobalTarget, CoreType)) -resolveVisibleGlobalLowering key = - withLoweringBuilder \builder -> - ( (\(target, _content, _dependencies) -> - ( target - , fromMaybe - (impossible "visible semantic key has no source type") - (semanticGlobalKeyType key) - )) - <$> resolveVisibleGlobalContent builder key - ) - -resolveVisibleGlobalContentLowering - :: SemanticGlobalKey - -> LoweringDriver - (Maybe - ( SemanticGlobalTarget - , ObjectContent - , Map ObjectId CoreType - )) -resolveVisibleGlobalContentLowering key = - withLoweringBuilder (\builder -> resolveVisibleGlobalContent builder key) - -resolveVisibleStructureLowering - :: SemanticStructurePhrase - -> LoweringDriver (Maybe ResolvedStructure) -resolveVisibleStructureLowering phrase = - withLoweringBuilder (Map.lookup phrase . logicalBuilderStructures) - -resolveVisibleStructureOperationObjectsLowering - :: StructSymbol - -> LoweringDriver [ObjectId] -resolveVisibleStructureOperationObjectsLowering symbol = - withLoweringBuilder \builder -> - Set.toAscList - (Set.fromList - (mapMaybe - (resolvedStructureOperation symbol) - (Map.elems (logicalBuilderStructures builder)))) - -objectAvailableLowering :: ObjectId -> LoweringDriver Bool -objectAvailableLowering identity = - withLoweringBuilder - (isJust - . lookupCheckedObjectType identity - . logicalBuilderObjectClosure) - -objectTypeLowering :: ObjectId -> LoweringDriver (Maybe CoreType) -objectTypeLowering identity = - withLoweringBuilder - (lookupCheckedObjectType identity - . logicalBuilderObjectClosure) - -withLoweringBuilder - :: (BuilderState PlanningEvidence -> value) - -> LoweringDriver value -withLoweringBuilder action = LoweringDriver do - LoweringState _resolver (ProspectiveBuilder builder) _validation <- State.get - pure (action builder) - - -data CandidateSpec = CandidateSpec - !CheckedPropositionContent - !FactSearchEligibility - ![SemanticName] - -candidateSpec - :: CheckedPropositionContent - -> FactSearchEligibility - -> [SemanticName] - -> CandidateSpec -candidateSpec = - CandidateSpec - --- | One strictly earlier candidate in the same checked declaration. The --- position is structural and becomes a concrete fact slot only while the --- declaration is planned. -data PlannedCandidatePosition = PlannedCandidatePosition - !Natural - !Natural - deriving stock (Show, Eq, Ord) - -data CandidatePlanningDirect - = PlanningDefinitionEquation !ObjectId - | PlanningSourceAxiom - | PlanningTrustedDatatype !DatatypeCompilationDescriptor - | PlanningKernelConstruction !KernelConstructionDescriptor - | PlanningCheckedSourceProof - | PlanningOmitted - deriving stock (Show, Eq) - --- | Erased exact request data needed by scheduling and public-contract --- planning. The family body retains the typed obligation used by admission; --- this projection carries only its one canonical request and exact global --- premise fingerprints. -data CheckedPlannedVampireRequest = CheckedPlannedVampireRequest - !Location - !Provers.PreparedVerificationRequest - ![SemanticFactOccurrenceFingerprint] - -data CandidatePlanningSpec = CandidatePlanningSpec - !CandidatePlanningDirect - ![SemanticFactOccurrenceFingerprint] - ![PlannedCandidatePosition] - ![CheckedPlannedVampireRequest] - --- | One authority-free checked candidate and its exact planning contract. --- The two parts are constructed together by the declaration-family lowerer --- and retain no builder capability or publication path. -data CheckedCandidate = CheckedCandidate - !CandidateSpec - !CandidatePlanningSpec - -checkedCandidate - :: CandidateSpec - -> CandidatePlanningSpec - -> CheckedCandidate -checkedCandidate = CheckedCandidate - -checkedDefinitionEquationPlanning :: ObjectId -> CandidatePlanningSpec -checkedDefinitionEquationPlanning identity = - CandidatePlanningSpec - (PlanningDefinitionEquation identity) [] [] [] - -checkedSourceAxiomPlanning :: CandidatePlanningSpec -checkedSourceAxiomPlanning = - CandidatePlanningSpec PlanningSourceAxiom [] [] [] - -checkedDatatypePlanning - :: DatatypeCompilationDescriptor - -> CandidatePlanningSpec -checkedDatatypePlanning descriptor = - CandidatePlanningSpec (PlanningTrustedDatatype descriptor) [] [] [] - -checkedKernelPlanning - :: KernelConstructionDescriptor - -> [SemanticFactOccurrenceFingerprint] - -> CandidatePlanningSpec -checkedKernelPlanning descriptor facts = - CandidatePlanningSpec - (PlanningKernelConstruction descriptor) - facts - [] - [] - -checkedSourceProofPlanning - :: [CheckedPlannedVampireRequest] - -> [PlannedCandidatePosition] - -> CandidatePlanningSpec -checkedSourceProofPlanning requests staged = - CandidatePlanningSpec - PlanningCheckedSourceProof [] staged requests - -checkedOmittedPlanning - :: [CheckedPlannedVampireRequest] - -> [PlannedCandidatePosition] - -> CandidatePlanningSpec -checkedOmittedPlanning requests staged = - CandidatePlanningSpec PlanningOmitted [] staged requests - -checkedPlannedVampireRequest - :: Location - -> PreparedVampireObligation local origin - -> CheckedPlannedVampireRequest -checkedPlannedVampireRequest location - (PreparedVampireObligation expected task) = - CheckedPlannedVampireRequest - location - (Provers.preparedTypedProverRequest task) - ( Backend.typedBackendFactReference - <$> Vector.toList - (Backend.typedProblemGlobalPremises expected) - ) - -plannedEarlierCandidate - :: Natural - -> Natural - -> PlannedCandidatePosition -plannedEarlierCandidate = - PlannedCandidatePosition - -data CheckedDeclarationMode - = CheckedProofMode !ProofSyntaxId - | CheckedCompiledMode !DeclarationSyntaxId - --- | One completely lowered, authority-free declaration transaction. The --- family body is a closed checked authorization recipe owned by its exact --- lowerer; structural effects and stable source-ordered candidate stages are --- common. This value is invocation-local and never serialized. -data CheckedDeclaration body = CheckedDeclaration - !CheckedDeclarationMode - ![AssertedObject] - ![CheckedPropositionContent] - ![SemanticGlobalBinding] - ![SemanticStructureDescriptor] - ![NonEmpty CheckedCandidate] - !body - -checkedProofDeclaration - :: ProofSyntaxId - -> [AssertedObject] - -> [CheckedPropositionContent] - -> [SemanticGlobalBinding] - -> [SemanticStructureDescriptor] - -> [NonEmpty CheckedCandidate] - -> body - -> CheckedDeclaration body -checkedProofDeclaration - syntax objects propositions globals structures stages = - CheckedDeclaration - (CheckedProofMode syntax) objects propositions globals structures - stages - -checkedCompiledDeclaration - :: DeclarationSyntaxId - -> [AssertedObject] - -> [CheckedPropositionContent] - -> [SemanticGlobalBinding] - -> [SemanticStructureDescriptor] - -> [NonEmpty CheckedCandidate] - -> body - -> CheckedDeclaration body -checkedCompiledDeclaration - syntax objects propositions globals structures stages = - CheckedDeclaration - (CheckedCompiledMode syntax) objects propositions globals structures - stages - -prepareCandidateSpecDriver - :: [AssertedObject] - -> ScopedCheckedCore ObjectId - -> FactSearchEligibility - -> [SemanticName] - -> ModuleDriver failure (Either DeclarationError CandidateSpec) -prepareCandidateSpecDriver objects scoped eligibility aliases = - prepareCandidateSpecWithDriverClosure objects - (\closure -> - prepareScopedCandidateSpec - closure scoped eligibility aliases) - -prepareFrozenCandidateSpecDriver - :: [AssertedObject] - -> FrozenCheckedCore ObjectId - -> FactSearchEligibility - -> [SemanticName] - -> ModuleDriver failure (Either DeclarationError CandidateSpec) -prepareFrozenCandidateSpecDriver objects frozen eligibility aliases = - prepareCandidateSpecWithDriverClosure objects - (\closure -> - prepareFrozenCandidateSpec - closure frozen eligibility aliases) - -prepareDefinitionEquationSpecDriver - :: [AssertedObject] - -> ObjectId - -> SemanticName - -> ModuleDriver failure (Either DeclarationError CandidateSpec) -prepareDefinitionEquationSpecDriver objects identity alias = - prepareCandidateSpecWithDriverClosure objects - (\closure -> - prepareDefinitionEquationSpec closure identity alias) - -preparePointwiseDefinitionEquationSpecDriver - :: [AssertedObject] - -> ObjectId - -> SemanticName - -> ModuleDriver failure (Either DeclarationError CandidateSpec) -preparePointwiseDefinitionEquationSpecDriver objects identity alias = - prepareCandidateSpecWithDriverClosure objects - (\closure -> - preparePointwiseDefinitionEquationSpec closure identity alias) - -prepareCandidateSpecLowering - :: [AssertedObject] - -> ScopedCheckedCore ObjectId - -> FactSearchEligibility - -> [SemanticName] - -> LoweringDriver (Either DeclarationError CandidateSpec) -prepareCandidateSpecLowering objects scoped eligibility aliases = - prepareCandidateSpecWithLoweringClosure objects - (\closure -> - prepareScopedCandidateSpec - closure scoped eligibility aliases) - -prepareFrozenCandidateSpecLowering - :: [AssertedObject] - -> FrozenCheckedCore ObjectId - -> FactSearchEligibility - -> [SemanticName] - -> LoweringDriver (Either DeclarationError CandidateSpec) -prepareFrozenCandidateSpecLowering objects frozen eligibility aliases = - prepareCandidateSpecWithLoweringClosure objects - (\closure -> - prepareFrozenCandidateSpec - closure frozen eligibility aliases) - -prepareDefinitionEquationSpecLowering - :: [AssertedObject] - -> ObjectId - -> SemanticName - -> LoweringDriver (Either DeclarationError CandidateSpec) -prepareDefinitionEquationSpecLowering objects identity alias = - prepareCandidateSpecWithLoweringClosure objects - (\closure -> - prepareDefinitionEquationSpec closure identity alias) - -preparePointwiseDefinitionEquationSpecLowering - :: [AssertedObject] - -> ObjectId - -> SemanticName - -> LoweringDriver (Either DeclarationError CandidateSpec) -preparePointwiseDefinitionEquationSpecLowering objects identity alias = - prepareCandidateSpecWithLoweringClosure objects - (\closure -> - preparePointwiseDefinitionEquationSpec closure identity alias) - --- | Prepare one closed Vampire obligation whose only premise is a --- conditionally available fact from a strictly earlier candidate stage of --- the same declaration. The temporary checked stage contains public fact --- semantics and structural provenance only; admission must still consume the --- corresponding real reserved candidate before accepting this request. -prepareStagedCandidateVampireDriver - :: Location - -> [AssertedObject] - -> CandidateSpec - -> CandidateSpec - -> ModuleDriver failure - (Either - DeclarationError - (PreparedVampireObligation Void ())) -prepareStagedCandidateVampireDriver - location objects premiseSpec targetSpec = - ModuleDriver do - DriverState resolver builder _prefix _validation <- State.get - State.lift - (liftIO - (prepareStagedCandidateVampireWith - resolver builder location objects premiseSpec targetSpec)) - -prepareStagedCandidateVampireLowering - :: Location - -> [AssertedObject] - -> CandidateSpec - -> CandidateSpec - -> LoweringDriver - (Either - DeclarationError - (PreparedVampireObligation Void ())) -prepareStagedCandidateVampireLowering - location objects premiseSpec targetSpec = - LoweringDriver do - LoweringState resolver (ProspectiveBuilder builder) _validation <- - State.get - liftIO - (prepareStagedCandidateVampireWith - resolver builder location objects premiseSpec targetSpec) - -prepareStagedCandidateVampireWith - :: VampireResolver - -> BuilderState evidence - -> Location - -> [AssertedObject] - -> CandidateSpec - -> CandidateSpec - -> IO - (Either - DeclarationError - (PreparedVampireObligation Void ())) -prepareStagedCandidateVampireWith - resolver builder location objects premiseSpec targetSpec = do - let staged = do - closure <- - first DeclarationObjectValidationFailed - (extendObjectClosure - (logicalBuilderObjectClosure builder) - objects) - premise <- - prospectiveStagePremise - builder closure premiseSpec targetSpec - pure (closure, premise) - case staged of - Left failure -> pure (Left failure) - Right (closure, premise) -> do - prepared <- - measureVampirePreparation resolver - (prepareClosedCandidateVampire - builder closure - (candidateSpecProposition targetSpec) - [premise]) - pure - (first - (ProofObligationFailedAt location - . CurrentCandidateVampirePreparationFailed) - prepared) - -candidateSpecProposition :: CandidateSpec -> CheckedPropositionContent -candidateSpecProposition (CandidateSpec proposition _eligibility _aliases) = - proposition - -prospectiveStagePremise - :: BuilderState evidence - -> CheckedObjectClosure - -> CandidateSpec - -> CandidateSpec - -> Either DeclarationError CheckedPropositionContent -prospectiveStagePremise builder closure premiseSpec targetSpec = do - let owner = logicalBuilderOwner builder - declaration = - declarationSlot owner - (localDeclarationOrdinal - (logicalBuilderNextDeclaration builder)) - premiseSlot = - factSlot owner - (localFactOrdinal (logicalBuilderNextFact builder)) - targetSlot = - factSlot owner - (localFactOrdinal (logicalBuilderNextFact builder + 1)) - premiseStage = CandidateStage 0 - targetStage = CandidateStage 1 - proposition = candidateSpecProposition premiseSpec - authority = - factAuthority - (theoremRef - (logicalBuilderTheory builder) - (checkedPropositionId proposition)) - cleanAuthoritySafety - CandidateSpec _ eligibility _aliases = premiseSpec - occurrence = - semanticFactOccurrence premiseSlot authority eligibility - stage = - CheckedDeclarationStage declaration closure - (Map.singleton premiseSlot - (FactEntry proposition occurrence - (PlanningEvidence - authority - (Just - (PlanningProvenance - declaration premiseStage premiseSlot))))) - unless - (propositionMatchesClosure closure - (candidateSpecProposition targetSpec)) - (Left (PlanningFactContractMismatch targetSlot)) - useProspectiveStageFact - stage targetStage targetSlot premiseStage premiseSlot - -useProspectiveStageFact - :: CheckedDeclarationStage - -> CandidateStage - -> FactSlot - -> CandidateStage - -> FactSlot - -> Either DeclarationError CheckedPropositionContent -useProspectiveStageFact - (CheckedDeclarationStage ownSlot closure entries) - currentStage currentSlot expectedStage premiseSlot = do - FactEntry proposition occurrence - (PlanningEvidence authority provenance) <- - maybe - (Left (PlanningFactContractMismatch premiseSlot)) - Right - (Map.lookup premiseSlot entries) - unless - ( provenance - == Just - (PlanningProvenance - ownSlot expectedStage premiseSlot) - && expectedStage < currentStage - && semanticFactSlot occurrence == premiseSlot - && semanticFactAuthority occurrence == authority - && propositionMatchesClosure closure proposition - ) - (Left (PlanningFactContractMismatch currentSlot)) - pure proposition - -prepareCandidateSpecWithDriverClosure - :: [AssertedObject] - -> (CheckedObjectClosure -> Either DeclarationError CandidateSpec) - -> ModuleDriver failure (Either DeclarationError CandidateSpec) -prepareCandidateSpecWithDriverClosure objects prepare = ModuleDriver do - DriverState _resolver builder _prefix _validation <- State.get - pure do - closure <- - first DeclarationObjectValidationFailed - (extendObjectClosure - (logicalBuilderObjectClosure builder) - objects) - prepare closure - -prepareCandidateSpecWithLoweringClosure - :: [AssertedObject] - -> (CheckedObjectClosure -> Either DeclarationError CandidateSpec) - -> LoweringDriver (Either DeclarationError CandidateSpec) -prepareCandidateSpecWithLoweringClosure objects prepare = - withLoweringBuilder \builder -> do - closure <- - first DeclarationObjectValidationFailed - (extendObjectClosure - (logicalBuilderObjectClosure builder) - objects) - prepare closure - -data ReservedCandidate = ReservedCandidate - !BuilderIdentity - !PrefixContextId - !DeclarationInvocation - !CandidateStage - !FactSlot - !CandidateSpec - -reservedCandidateSlot :: ReservedCandidate -> FactSlot -reservedCandidateSlot - (ReservedCandidate _ _ _ _ slot _) = - slot - -reservedCandidateStage :: ReservedCandidate -> Natural -reservedCandidateStage - (ReservedCandidate _ _ _ (CandidateStage stage) _ _) = - stage - -candidateCheckedProposition - :: ReservedCandidate - -> CheckedPropositionContent -candidateCheckedProposition - (ReservedCandidate _ _ _ _ _ (CandidateSpec proposition _ _)) = - proposition - -candidateTheoremReference - :: BuilderState evidence - -> ReservedCandidate - -> TheoremRef -candidateTheoremReference builder candidate = - theoremRef - (logicalBuilderTheory builder) - (checkedPropositionId - (candidateCheckedProposition candidate)) - - -data PendingCandidate = PendingCandidate - !ReservedCandidate - !ValidationCertificate - !PendingFactAuthorization - -data DeclarationValidationSelection - = DeclarationValidationUnselected - | FreshDeclarationValidation - | CachedDeclarationValidation - !DeclarationSyntaxId - ![ObjectId] - ![TheoremId] - !DeclarationValidationRecord - !(Map FactSlot Natural) - -data DeclarationState = DeclarationState - { declarationVampireResolver :: !VampireResolver - , declarationValidationRun :: !ValidationRun - , declarationValidationMode :: !ValidationMode - , declarationValidationSelection - :: !DeclarationValidationSelection - , declarationBuilder :: !LogicalBuilder - , declarationOwnSlot :: !DeclarationSlot - , declarationInvocation :: !DeclarationInvocation - , declarationObjectsReversed :: ![AssertedObject] - , declarationObjectClosure :: !(Maybe CheckedObjectClosure) - , declarationPropositionsReversed - :: ![CheckedPropositionContent] - , declarationGlobalBindingsReversed - :: ![SemanticGlobalBinding] - , declarationStructureDescriptorsReversed - :: ![SemanticStructureDescriptor] - , declarationReservations - :: !(Map FactSlot ReservedCandidate) - , declarationPending :: !(Map FactSlot PendingCandidate) - , declarationNextFact :: !Natural - , declarationNextStage :: !Natural - , declarationAuthorizationFrontier :: !Natural - } - --- | Authority-free view of checked declaration-local semantics. This is the --- narrow staging substrate for later lowerers: it carries the exact object --- closure and conditional public fact contracts, but no builder identity, --- prefix, invocation, pending authorization, admitted alias, or published --- occurrence. -data CheckedDeclarationStage = CheckedDeclarationStage - !DeclarationSlot - !CheckedObjectClosure - !(Map FactSlot (FactEntry PlanningEvidence)) - -newtype Declaration value = Declaration - { runDeclaration - :: StateT - DeclarationState - (ExceptT DeclarationError IO) - value - } - deriving newtype (Functor, Applicative, Monad) - -failDeclaration :: DeclarationError -> Declaration value -failDeclaration = - Declaration . State.lift . Except.throwError - -addDeclarationObject :: AssertedObject -> Declaration () -addDeclarationObject asserted = Declaration do - state <- State.get - case declarationValidationSelection state of - DeclarationValidationUnselected -> pure () - _ -> - State.lift - (Except.throwError - DeclarationShapeChangedAfterValidationLookup) - when - (isJust (declarationObjectClosure state)) - (State.lift - (Except.throwError - DeclarationObjectAddedAfterAuthorization)) - State.put - state - { declarationObjectsReversed = - asserted : declarationObjectsReversed state - } - -addDeclarationProposition - :: CheckedPropositionContent - -> Declaration () -addDeclarationProposition proposition = - Declaration - (State.modify' \state -> - state - { declarationPropositionsReversed = - proposition - : declarationPropositionsReversed state - }) - -resolveVisibleGlobal - :: SemanticGlobalKey - -> Declaration (Maybe (SemanticGlobalTarget, CoreType)) -resolveVisibleGlobal key = Declaration do - state <- State.get - let builder = declarationBuilder state - pure do - target <- Map.lookup key (logicalBuilderGlobals builder) - coreType <- semanticGlobalKeyType key - pure (target, coreType) - -stageSemanticGlobalBinding - :: SemanticGlobalKey - -> SemanticGlobalTarget - -> Declaration () -stageSemanticGlobalBinding key target = Declaration do - state <- State.get - case declarationValidationSelection state of - DeclarationValidationUnselected -> pure () - _ -> - State.lift - (Except.throwError - DeclarationShapeChangedAfterValidationLookup) - when - (any - ((== key) . semanticGlobalBindingKey) - (declarationGlobalBindingsReversed state)) - (State.lift - (Except.throwError - (DeclarationGlobalAlreadyStaged key))) - State.put - state - { declarationGlobalBindingsReversed = - semanticGlobalBinding key target - : declarationGlobalBindingsReversed state - } - -stageSemanticStructureDescriptor - :: SemanticStructureDescriptor - -> Declaration () -stageSemanticStructureDescriptor descriptor = Declaration do - state <- State.get - case declarationValidationSelection state of - DeclarationValidationUnselected -> pure () - _ -> - State.lift - (Except.throwError - DeclarationShapeChangedAfterValidationLookup) - let structurePhrase = semanticStructureDescriptorPhrase descriptor - when - (any - ((== structurePhrase) . semanticStructureDescriptorPhrase) - (declarationStructureDescriptorsReversed state)) - (State.lift - (Except.throwError - (DeclarationStructureAlreadyStaged structurePhrase))) - State.put - state - { declarationStructureDescriptorsReversed = - descriptor - : declarationStructureDescriptorsReversed state - } - -prepareScopedCandidateSpec - :: CheckedObjectClosure - -> ScopedCheckedCore ObjectId - -> FactSearchEligibility - -> [SemanticName] - -> Either DeclarationError CandidateSpec -prepareScopedCandidateSpec closure scoped eligibility aliases = do - frozen <- - maybe (Left CandidatePropositionNotClosed) Right - (closeScopedCore scoped) - prepareFrozenCandidateSpec closure frozen eligibility aliases - -prepareFrozenCandidateSpec - :: CheckedObjectClosure - -> FrozenCheckedCore ObjectId - -> FactSearchEligibility - -> [SemanticName] - -> Either DeclarationError CandidateSpec -prepareFrozenCandidateSpec closure frozen eligibility aliases = do - unless - (frozenCoreType frozen == TyProp) - (Left - (CandidatePropositionNotProposition - (frozenCoreType frozen))) - proposition <- - first DeclarationPropositionValidationFailed - (validatePropositionContent closure (frozenCoreTerm frozen)) - pure (candidateSpec proposition eligibility aliases) - -prepareDefinitionEquationSpec - :: CheckedObjectClosure - -> ObjectId - -> SemanticName - -> Either DeclarationError CandidateSpec -prepareDefinitionEquationSpec closure identity alias = do - content <- - maybe - (Left (DefinitionEquationObjectMissing identity)) - Right - (lookupCheckedObjectContent identity closure) - (coreType, body) <- - case content of - TransparentObjectContent _theory objectType objectBody -> - Right (objectType, objectBody) - _ -> - Left (DefinitionEquationObjectNotTransparent identity) - proposition <- - first DeclarationPropositionValidationFailed - (validatePropositionContent - closure - (CEq coreType (CGlobal identity) body)) - pure (candidateSpec proposition SearchEligible [alias]) - -preparePointwiseDefinitionEquationSpec - :: CheckedObjectClosure - -> ObjectId - -> SemanticName - -> Either DeclarationError CandidateSpec -preparePointwiseDefinitionEquationSpec closure identity alias = do - content <- - maybe - (Left (DefinitionEquationObjectMissing identity)) - Right - (lookupCheckedObjectContent identity closure) - body <- - case content of - TransparentObjectContent _theory - (TyArrow TySet TyProp) (CLam TySet predicate) -> - Right predicate - _ -> - Left - (DefinitionEquationObjectNotPointwisePredicate identity) - proposition <- - first DeclarationPropositionValidationFailed - (validatePropositionContent - closure - (CForall TySet - (CEq TyProp - (CApp (CGlobal identity) (CBound 0)) - body))) - pure (candidateSpec proposition SearchEligible [alias]) - -reserveCandidate - :: CandidateSpec - -> Declaration ReservedCandidate -reserveCandidate spec = - NonEmpty.head <$> reserveCandidateBatch (spec :| []) - --- | Validate and reserve one closed checked proposition in the current --- declaration closure. -reservePropositionCandidate - :: ScopedCheckedCore ObjectId - -> FactSearchEligibility - -> [SemanticName] - -> Declaration ReservedCandidate -reservePropositionCandidate scoped eligibility aliases = Declaration do - unprepared <- State.get - prepared <- - State.lift - (Except.liftEither - (prepareDeclarationClosure unprepared)) - spec <- - State.lift - (Except.liftEither - (prepareScopedCandidateSpec - (fromMaybe - (impossible - "prepared proposition closure is absent") - (declarationObjectClosure prepared)) - scoped eligibility aliases)) - State.put prepared - runDeclaration (reserveCandidate spec) - --- | Validate and reserve one stage of already closed checked propositions in --- the current declaration closure. -reserveFrozenPropositionCandidateBatch - :: NonEmpty - ( FrozenCheckedCore ObjectId - , FactSearchEligibility - , [SemanticName] - ) - -> Declaration (NonEmpty ReservedCandidate) -reserveFrozenPropositionCandidateBatch inputs = Declaration do - unprepared <- State.get - prepared <- - State.lift - (Except.liftEither - (prepareDeclarationClosure unprepared)) - let closure = - maybe - (impossible "prepared proposition closure is absent") - id - (declarationObjectClosure prepared) - specs <- traverse (prepareInput closure) inputs - State.put prepared - runDeclaration (reserveCandidateBatch specs) - where - prepareInput closure (frozen, eligibility, aliases) = - State.lift - (Except.liftEither - (prepareFrozenCandidateSpec - closure frozen eligibility aliases)) - -reserveCandidateBatch - :: NonEmpty CandidateSpec - -> Declaration (NonEmpty ReservedCandidate) -reserveCandidateBatch specs = Declaration do - state <- State.get - case declarationValidationSelection state of - DeclarationValidationUnselected -> pure () - _ -> - State.lift - (Except.throwError - DeclarationShapeChangedAfterValidationLookup) - let builder = declarationBuilder state - stage = CandidateStage (declarationNextStage state) - firstFact = declarationNextFact state - candidates = - NonEmpty.zipWith - (makeReserved builder state stage) - (0 :| [1 ..]) - specs - reservations' = - foldl' - (\reservations candidate -> - Map.insert - (reservedCandidateSlot candidate) - candidate - reservations) - (declarationReservations state) - candidates - candidateCount = fromIntegral (NonEmpty.length specs) - State.put - state - { declarationReservations = reservations' - , declarationNextFact = firstFact + candidateCount - , declarationNextStage = - declarationNextStage state + 1 - } - pure candidates - where - makeReserved builder state stage offset spec = - ReservedCandidate - (logicalBuilderIdentity builder) - (logicalBuilderPrefix builder) - (declarationInvocation state) - stage - (factSlot - (logicalBuilderOwner builder) - (localFactOrdinal - (declarationNextFact state + offset))) - spec - --- | Construct the one defining equation owned by a checked transparent --- object. The equation is derived from authoritative object content, not from --- a caller-supplied proposition. -reserveDefinitionEquationCandidate - :: ObjectId - -> SemanticName - -> Declaration ReservedCandidate -reserveDefinitionEquationCandidate identity alias = Declaration do - unprepared <- State.get - prepared <- - State.lift - (Except.liftEither - (prepareDeclarationClosure unprepared)) - spec <- - State.lift - (Except.liftEither - (prepareDefinitionEquationSpec - (fromMaybe - (impossible - "prepared definition closure is absent") - (declarationObjectClosure prepared)) - identity alias)) - State.put prepared - runDeclaration (reserveCandidate spec) - --- | Construct the pointwise presentation of one unary transparent predicate --- definition. The candidate remains tied to the object's checked content. -reservePointwiseDefinitionEquationCandidate - :: ObjectId - -> SemanticName - -> Declaration ReservedCandidate -reservePointwiseDefinitionEquationCandidate identity alias = Declaration do - unprepared <- State.get - prepared <- - State.lift - (Except.liftEither - (prepareDeclarationClosure unprepared)) - spec <- - State.lift - (Except.liftEither - (preparePointwiseDefinitionEquationSpec - (fromMaybe - (impossible "prepared predicate closure is absent") - (declarationObjectClosure prepared)) - identity alias)) - State.put prepared - runDeclaration (reserveCandidate spec) - --- | Reserve one defining equation and a nonempty generated-fact batch at the --- same declaration stage. No candidate in the batch can cite a sibling. -reserveDefinitionEquationCandidateBatch - :: ObjectId - -> SemanticName - -> NonEmpty - ( ScopedCheckedCore ObjectId - , FactSearchEligibility - , [SemanticName] - ) - -> Declaration - ( ReservedCandidate - , NonEmpty ReservedCandidate - ) -reserveDefinitionEquationCandidateBatch identity alias generated = - Declaration do - unprepared <- State.get - prepared <- - State.lift - (Except.liftEither - (prepareDeclarationClosure unprepared)) - let closure = - maybe - (impossible - "prepared declaration closure is absent") - id - (declarationObjectClosure prepared) - definition <- - State.lift - (Except.liftEither - (prepareDefinitionEquationSpec closure identity alias)) - generatedSpecs <- - traverse - (prepareGeneratedSpec closure) - generated - State.put prepared - candidates <- - runDeclaration - (reserveCandidateBatch - (definition :| toList generatedSpecs)) - case candidates of - definitionCandidate :| firstGenerated : remainingGenerated -> - pure - ( definitionCandidate - , firstGenerated :| remainingGenerated - ) - _ -> - impossible - "a nonempty generated batch produced no candidate" - where - prepareGeneratedSpec closure (scoped, eligibility, aliases) = - State.lift - (Except.liftEither - (prepareScopedCandidateSpec - closure scoped eligibility aliases)) - --- | Resolve one complete compiled declaration against its exact validation --- key, then run the source-level authorization action under that selection. --- Objects and candidates must already be prepared so the lookup key cannot --- change after a hit or miss is chosen. -authorizeCompiledDeclaration - :: Declaration value - -> Declaration value -authorizeCompiledDeclaration action = Declaration do - unprepared <- State.get - (syntax, objects, theorems, ordinals, prepared) <- - State.lift - (Except.liftEither - (prepareCompiledValidation unprepared)) - let key = - declarationValidationKey - syntax - (logicalBuilderPrefix - (declarationBuilder prepared)) - objects - theorems - cached <- - case declarationValidationRun prepared of - FreshValidation -> - pure Nothing - WarmValidation - (ValidationLookup _lookupProof lookupDeclaration) -> - liftIO (lookupDeclaration key) - traverse_ - (\record -> - case Materialization.checkDeclarationValidationRecord - (logicalBuilderPrefix - (declarationBuilder prepared)) - syntax - objects - theorems - record of - Left failure -> - liftIO - (throwIO - (CachedValidationIntegrityError failure)) - Right () -> - pure ()) - cached - let selection = - case cached of - Nothing -> - FreshDeclarationValidation - Just record -> - CachedDeclarationValidation - syntax objects theorems record ordinals - State.put - prepared - { declarationValidationSelection = selection - } - runDeclaration action - -prepareCompiledValidation - :: DeclarationState - -> Either - DeclarationError - ( DeclarationSyntaxId - , [ObjectId] - , [TheoremId] - , Map FactSlot Natural - , DeclarationState - ) -prepareCompiledValidation declaration = do - syntax <- - case declarationValidationMode declaration of - DeclarationValidationMode value -> - Right value - _ -> - Left DeclarationValidationOutsideCompiledDeclaration - case declarationValidationSelection declaration of - DeclarationValidationUnselected -> pure () - _ -> Left DeclarationValidationAlreadySelected - closure <- declarationClosure declaration - let builder = declarationBuilder declaration - candidates = Map.elems (declarationReservations declaration) - objects = - assertedObjectId - <$> reverse - (declarationObjectsReversed declaration) - theorems = - theoremId . candidateTheoremReference builder - <$> candidates - ordinals = - Map.fromList - (zip - (reservedCandidateSlot <$> candidates) - [0 ..]) - pure - ( syntax - , objects - , theorems - , ordinals - , declaration - { declarationObjectClosure = Just closure - } - ) - -lookupProofValidation - :: ReservedCandidate - -> Declaration (ProofSyntaxId, Maybe ProofValidationRecord) -lookupProofValidation candidate = Declaration do - state <- State.get - syntax <- - case declarationValidationMode state of - EnvironmentImportMode -> - State.lift - (Except.throwError - ProofValidationOutsideProofDeclaration) - ProofValidationMode proofSyntax -> - pure proofSyntax - DeclarationValidationMode{} -> - State.lift - (Except.throwError - ProofValidationOutsideProofDeclaration) - let builder = declarationBuilder state - reference = candidateTheoremReference builder candidate - key = - proofValidationKey - (theoremId - (factAuthorityTheorem - (factAuthority - reference - cleanAuthoritySafety))) - syntax - (logicalBuilderPrefix builder) - record <- - case declarationValidationRun state of - FreshValidation -> - pure Nothing - WarmValidation (ValidationLookup lookupProof _lookupDeclaration) -> - State.lift - (liftIO - (lookupProof key)) - pure (syntax, record) -data CandidatePremise = CandidatePremise - !CheckedPropositionContent - -data CandidateProofState = CandidateProofState - { candidateProofDeclaration :: !DeclarationState - , candidateProofObjectClosure :: !CheckedObjectClosure - , candidateProofCandidate :: !ReservedCandidate - , candidateProofCachedValidation - :: !(Maybe Materialization.CandidateValidation) - , candidateProofPremisesReversed :: ![CandidatePremise] - , candidateProofPremiseCount :: !Natural - , candidateProofSafety :: !CandidateSafety - , candidateProofAcceptedRequestsReversed - :: ![PreparedRequestId] - } - -candidateProofBuilder :: CandidateProofState -> LogicalBuilder -candidateProofBuilder = - declarationBuilder . candidateProofDeclaration - -newtype CandidateProof value = CandidateProof - { runCandidateProof - :: StateT - CandidateProofState - (ExceptT DeclarationError IO) - value - } - deriving newtype (Functor, Applicative, Monad) - --- | Attach source trivia to a proof-obligation failure. The location does --- not participate in validation or request identity. -locateProofObligation - :: Location - -> CandidateProof value - -> CandidateProof value -locateProofObligation location (CandidateProof action) = - CandidateProof - (State.mapStateT - (Except.withExceptT - (ProofObligationFailedAt location)) - action) - --- | Record that the current exact proof discharged one goal with @Omitted@. -recordOmittedUse :: CandidateProof () -recordOmittedUse = CandidateProof do - state <- State.get - State.put - state - { candidateProofSafety = - addCandidateEscape - Omitted - (candidateProofSafety state) - } - -data VampirePremiseSelection - = VampireImplicitPremises - | VampireExplicitPremises - !(NonEmpty SemanticFactOccurrenceFingerprint) - | VampireLocalPremises - deriving stock (Show, Eq) - -data VampireObligationPreparationError local - = VampireObligationIndirectTargetNotFalsum - | VampireObligationClaimProjectionFailed - !(Backend.SupportedPropositionProjectionError local) - | VampireObligationLocalProjectionFailed - !Backend.LocalPremiseOrdinal - !(Backend.SupportedPropositionProjectionError local) - | VampireObligationLocalClassificationFailed - !Backend.LocalPremiseOrdinal - !(Backend.BackendClassificationError ObjectId) - | VampireObligationFactNotVisible - !SemanticFactOccurrenceFingerprint - | VampireObligationFactInvalid - !SemanticFactOccurrenceFingerprint - | VampireObligationPlanningFailed - !(Backend.TypedProblemError local ObjectId) - | VampireObligationEncodingFailed - !(Tptp.TypedTptpPreparationError local ObjectId) - deriving stock (Show, Eq) - -data ScopedVampirePremise local origin = ScopedVampirePremise - !Backend.LocalPremiseOrdinal - !origin - !(Vector (local, CoreType)) - !(ScopedCheckedCore ObjectId) - -scopedVampirePremise - :: Backend.LocalPremiseOrdinal - -> origin - -> Vector (local, CoreType) - -> ScopedCheckedCore ObjectId - -> ScopedVampirePremise local origin -scopedVampirePremise = - ScopedVampirePremise - -data PreparedVampireObligation local origin = - PreparedVampireObligation - !(Backend.TypedProblem - SemanticFactOccurrenceFingerprint - local - origin - ObjectId) - !(Provers.PreparedTypedProverTask - SemanticFactOccurrenceFingerprint - local - origin - ObjectId) - --- | Prepare a scoped task for a trusted structural proof checker. This --- validates the typed problem but does not establish how its local judgments --- derive from the enclosing theorem. 'Checking.Exact.Proof' owns that --- composition on the production path. -prepareScopedVampireObligationDriver - :: Ord local - => Vector (local, CoreType) - -> ScopedCheckedCore ObjectId - -> [ScopedVampirePremise local origin] - -> [FoundationAxiomTag] - -> VampirePremiseSelection - -> ModuleDriver failure - (Either - (VampireObligationPreparationError local) - (PreparedVampireObligation local origin)) -prepareScopedVampireObligationDriver - claimSupport claim scopedLocals auxiliaryTags selection = - prepareScopedVampireObligationForMode - Provers.DirectTask - claimSupport - claim - scopedLocals - auxiliaryTags - selection - --- | Prepare the one indirect task admitted by the exact proof compiler. --- The target check keeps contradictory input from authorizing another goal. -prepareScopedContradictionObligationDriver - :: Ord local - => Vector (local, CoreType) - -> ScopedCheckedCore ObjectId - -> [ScopedVampirePremise local origin] - -> [FoundationAxiomTag] - -> VampirePremiseSelection - -> ModuleDriver failure - (Either - (VampireObligationPreparationError local) - (PreparedVampireObligation local origin)) -prepareScopedContradictionObligationDriver - claimSupport claim scopedLocals auxiliaryTags selection - | scopedCoreType claim /= TyProp || scopedCoreTerm claim /= CFalsum = - pure (Left VampireObligationIndirectTargetNotFalsum) - | otherwise = - prepareScopedVampireObligationForMode - Provers.IndirectTask - claimSupport - claim - scopedLocals - auxiliaryTags - selection - -prepareScopedVampireObligationLowering - :: Ord local - => Vector (local, CoreType) - -> ScopedCheckedCore ObjectId - -> [ScopedVampirePremise local origin] - -> [FoundationAxiomTag] - -> VampirePremiseSelection - -> LoweringDriver - (Either - (VampireObligationPreparationError local) - (PreparedVampireObligation local origin)) -prepareScopedVampireObligationLowering - claimSupport claim scopedLocals auxiliaryTags selection = - prepareScopedVampireObligationForModeLowering - Provers.DirectTask - claimSupport claim scopedLocals auxiliaryTags selection - -prepareScopedContradictionObligationLowering - :: Ord local - => Vector (local, CoreType) - -> ScopedCheckedCore ObjectId - -> [ScopedVampirePremise local origin] - -> [FoundationAxiomTag] - -> VampirePremiseSelection - -> LoweringDriver - (Either - (VampireObligationPreparationError local) - (PreparedVampireObligation local origin)) -prepareScopedContradictionObligationLowering - claimSupport claim scopedLocals auxiliaryTags selection - | scopedCoreType claim /= TyProp || scopedCoreTerm claim /= CFalsum = - pure (Left VampireObligationIndirectTargetNotFalsum) - | otherwise = - prepareScopedVampireObligationForModeLowering - Provers.IndirectTask - claimSupport claim scopedLocals auxiliaryTags selection - -prepareScopedVampireObligationForModeLowering - :: Ord local - => Provers.VampireTaskMode - -> Vector (local, CoreType) - -> ScopedCheckedCore ObjectId - -> [ScopedVampirePremise local origin] - -> [FoundationAxiomTag] - -> VampirePremiseSelection - -> LoweringDriver - (Either - (VampireObligationPreparationError local) - (PreparedVampireObligation local origin)) -prepareScopedVampireObligationForModeLowering - taskMode claimSupport claim scopedLocals auxiliaryTags selection = - LoweringDriver do - LoweringState resolver (ProspectiveBuilder builder) _validation <- - State.get - liftIO - (prepareScopedVampireObligationWith - resolver builder taskMode claimSupport claim scopedLocals - auxiliaryTags selection) - -prepareScopedVampireObligationForMode - :: Ord local - => Provers.VampireTaskMode - -> Vector (local, CoreType) - -> ScopedCheckedCore ObjectId - -> [ScopedVampirePremise local origin] - -> [FoundationAxiomTag] - -> VampirePremiseSelection - -> ModuleDriver failure - (Either - (VampireObligationPreparationError local) - (PreparedVampireObligation local origin)) -prepareScopedVampireObligationForMode - taskMode claimSupport claim scopedLocals auxiliaryTags selection = - ModuleDriver do - DriverState resolver builder _prefix _validation <- State.get - State.lift - (Except.liftIO - (prepareScopedVampireObligationWith - resolver builder taskMode claimSupport claim scopedLocals - auxiliaryTags selection)) - -prepareScopedVampireObligationWith - :: (Ord local) - => VampireResolver - -> BuilderState evidence - -> Provers.VampireTaskMode - -> Vector (local, CoreType) - -> ScopedCheckedCore ObjectId - -> [ScopedVampirePremise local origin] - -> [FoundationAxiomTag] - -> VampirePremiseSelection - -> IO - (Either - (VampireObligationPreparationError local) - (PreparedVampireObligation local origin)) -prepareScopedVampireObligationWith - resolver builder taskMode claimSupport claim scopedLocals - auxiliaryTags selection = - measureVampirePreparation resolver preparation - where - closure = logicalBuilderObjectClosure builder - globalType = (`lookupCheckedObjectType` closure) - preparation = do - supportedClaim <- - first VampireObligationClaimProjectionFailed - (Backend.projectSupportedProposition - globalType - claimSupport - claim) - locals <- traverse prepareLocal scopedLocals - prepareVampireObligationWith - taskMode - builder - closure - supportedClaim - locals - auxiliaryTags - selection - - prepareLocal - (ScopedVampirePremise - ordinal origin support proposition) = do - supported <- - first - (VampireObligationLocalProjectionFailed ordinal) - (Backend.projectSupportedProposition - globalType - support - proposition) - first - (VampireObligationLocalClassificationFailed ordinal) - (Backend.typedLocalPremise - globalType - ordinal - origin - supported) - -prepareVampireObligationWith - :: Ord local - => Provers.VampireTaskMode - -> BuilderState evidence - -> CheckedObjectClosure - -> Backend.SupportedProposition local ObjectId - -> [Backend.TypedLocalPremise local origin ObjectId] - -> [FoundationAxiomTag] - -> VampirePremiseSelection - -> Either - (VampireObligationPreparationError local) - (PreparedVampireObligation local origin) -prepareVampireObligationWith - taskMode builder closure claim locals auxiliaryTags selection = do - let globalType = (`lookupCheckedObjectType` closure) - selected <- - selectVampireFacts - globalType - builder - selection - let (globalMode, localPolicy) = - case selection of - VampireImplicitPremises -> - ( Backend.ImplicitFofPremises - , Backend.FirstOrderLocals - ) - VampireExplicitPremises{} -> - ( Backend.ExplicitGlobalPremises - , Backend.FirstOrderLocals - ) - VampireLocalPremises -> - ( Backend.NoGlobalPremises - , Backend.AllLocals - ) - propositionDependencies = - foundationAxiomDependencies - . Backend.supportedPropositionTerm - requiredAuxiliaryTags = - Set.toAscList - ( Set.fromList auxiliaryTags - <> propositionDependencies claim - <> foldMap - (propositionDependencies - . Backend.typedBackendFactProposition) - selected - <> foldMap - (propositionDependencies - . Backend.typedLocalPremiseProposition) - (Backend.selectTypedLocalPremises - localPolicy - locals) - ) - auxiliaries = - Backend.typedFoundationAuxiliaryInput - (logicalBuilderFoundation builder) - <$> requiredAuxiliaryTags - problem <- - first VampireObligationPlanningFailed - (Backend.planTypedProblem - globalType - selected - claim - locals - auxiliaries - globalMode - localPolicy) - task <- - first VampireObligationEncodingFailed - (Provers.prepareTypedProverTask - taskMode - problem) - pure (PreparedVampireObligation problem task) - -measureVampirePreparation - :: VampireResolver - -> Either - (VampireObligationPreparationError local) - (PreparedVampireObligation local origin) - -> IO - (Either - (VampireObligationPreparationError local) - (PreparedVampireObligation local origin)) -measureVampirePreparation resolver preparation = do - started <- getMonotonicTimeNSec - prepared <- Exception.evaluate (forcePrepared preparation) - finished <- getMonotonicTimeNSec - observeVampirePreparation resolver (finished - started) - pure prepared - where - forcePrepared result = - case result of - Left err -> err `seq` result - Right prepared@(PreparedVampireObligation _ task) -> - let request = Provers.preparedTypedProverRequest task - in Provers.preparedVerificationByteCount request `seq` - Provers.preparedVerificationRequestId request `seq` - prepared `seq` - result - -selectVampireFacts - :: (ObjectId -> Maybe CoreType) - -> BuilderState evidence - -> VampirePremiseSelection - -> Either - (VampireObligationPreparationError local) - (Vector - (Backend.TypedBackendFact - SemanticFactOccurrenceFingerprint - ObjectId)) -selectVampireFacts globalType builder selection = - Vector.fromList <$> case selection of - VampireImplicitPremises -> - mapMaybeM prepareImplicit - (Map.toAscList (logicalBuilderFacts builder)) - VampireExplicitPremises fingerprints -> - traverse prepareExplicit - (stableUniqueBy id (toList fingerprints)) - VampireLocalPremises -> - Right [] - where - prepareImplicit (fingerprint, authorized@(FactEntry - _proposition occurrence _authorization)) - | semanticFactSearchEligibility occurrence - /= SearchEligible = - Right Nothing - | otherwise = do - fact <- prepareFact fingerprint authorized - pure case Backend.typedBackendFactCapability fact of - Backend.FofProjectable{} -> Just fact - Backend.RequiresTh0{} -> Nothing - - prepareExplicit fingerprint = - case Map.lookup fingerprint (logicalBuilderFacts builder) of - Nothing -> - Left (VampireObligationFactNotVisible fingerprint) - Just authorized -> - prepareFact fingerprint authorized - - prepareFact fingerprint - (FactEntry proposition occurrence _authorization) - | semanticFactFingerprint occurrence /= fingerprint = - Left (VampireObligationFactInvalid fingerprint) - | otherwise = do - supported <- - first - (const - (VampireObligationFactInvalid fingerprint)) - (Backend.supportedProposition - Vector.empty - (embedClosedCore - [] - (checkedPropositionTerm proposition))) - capability <- - first - (const - (VampireObligationFactInvalid fingerprint)) - (Backend.classifySupportedProposition - globalType - supported) - pure - (Backend.typedBackendFact - fingerprint - supported - capability) - - mapMaybeM action = - fmap catMaybes . traverse action - -data LocalClaim = LocalClaim - !BuilderIdentity - !DeclarationInvocation - !FactSlot - !CheckedPropositionContent - -useAuthorizedFact - :: SemanticFactOccurrenceFingerprint - -> CandidateProof ImportIx -useAuthorizedFact fingerprint = do - proposition <- consumeAuthorizedFact fingerprint - registerKernelImport proposition - --- | Validate one fact capability and accumulate only its safety effect. --- Backend use does not register a kernel import. -consumeAuthorizedFact - :: SemanticFactOccurrenceFingerprint - -> CandidateProof CheckedPropositionContent -consumeAuthorizedFact fingerprint = CandidateProof do - state <- State.get - let builder = candidateProofBuilder state - declaration = candidateProofDeclaration state - staged = - findPendingByFingerprint - fingerprint - (declarationPending declaration) - case staged of - Just pending -> - consumePendingFact pending state - Nothing -> - case Map.lookup - fingerprint - (logicalBuilderFacts builder) of - Nothing -> - State.lift - (Except.throwError - (AuthorizedFactNotVisible fingerprint)) - Just authorized -> - consumeBuilderAuthorizedFact authorized state - --- | Materialize one sealed direct import and its transitive parents. The --- interface DAG is folded imported-before-importer and each producer --- occurrence receives a fresh capability for this consuming builder. -importSealedModule - :: ImportedModuleEvidence - -> Declaration () -importSealedModule evidence = Declaration do - state <- State.get - when - (isJust (declarationObjectClosure state)) - (State.lift - (Except.throwError ImportedModuleAfterAuthorization)) - let builder = declarationBuilder state - interfaceId = - semanticInterfaceAssertedId - (evidenceInterface evidence) - unless - (interfaceId `elem` - logicalBuilderDirectSemanticInputs builder) - (State.lift - (Except.throwError - (ImportedModuleNotDirect interfaceId))) - imported <- - State.lift - (Except.liftEither - (foldImportedEvidence evidence builder)) - State.put - state - { declarationBuilder = imported - , declarationObjectClosure = Nothing - } - --- The walking path keeps complete aggregate maps. Measure long chains before --- replacing this representation. -foldImportedEvidence - :: ImportedModuleEvidence - -> LogicalBuilder - -> Either DeclarationError LogicalBuilder -foldImportedEvidence evidence builder - | interfaceId - `Set.member` logicalBuilderImportedInterfaces builder = - Right builder - | otherwise = do - unless - (semanticInterfaceDirectInputs interface - == (semanticInterfaceAssertedId . evidenceInterface - <$> parents)) - (Left - (ImportedEvidenceDirectMismatch - (semanticInterfaceDirectInputs interface) - (semanticInterfaceAssertedId . evidenceInterface - <$> parents))) - withParents <- foldM - (flip foldImportedEvidence) - builder - parents - objectClosure <- - first - DeclarationObjectValidationFailed - (extendImportedObjectClosure - (logicalBuilderObjectClosure withParents) - objects) - importedFacts <- foldM - (insertImportedFact withParents) - (logicalBuilderFacts withParents) - (Map.elems entries) - importedAliases <- foldM - (insertImportedAlias importedFacts) - (logicalBuilderAliases withParents) - [ ( alias - , ImportedAliasOrigin - (declarationDeltaSlot delta) - (semanticAliasTarget alias) - ) - | delta <- semanticInterfaceDeclarations interface - , alias <- declarationDeltaAliases delta - ] - importedStructures <- foldM - (insertSemanticStructure objectClosure) - (logicalBuilderStructures withParents) - [ descriptor - | delta <- semanticInterfaceDeclarations interface - , descriptor <- semanticEnvironmentStructures - (declarationDeltaEnvironment delta) - ] - importedGlobals <- foldM - (insertImportedGlobal objectClosure importedStructures) - (logicalBuilderGlobals withParents) - [ binding - | delta <- semanticInterfaceDeclarations interface - , binding <- semanticEnvironmentBindings - (declarationDeltaEnvironment delta) - ] - pure - withParents - { logicalBuilderFacts = importedFacts - , logicalBuilderAliases = importedAliases - , logicalBuilderGlobals = importedGlobals - , logicalBuilderStructures = importedStructures - , logicalBuilderObjectClosure = objectClosure - , logicalBuilderImportedInterfaces = - Set.insert - interfaceId - (logicalBuilderImportedInterfaces withParents) - } - where - ImportedModuleEvidence interface parents entries objects = evidence - interfaceId = semanticInterfaceAssertedId interface - - extendImportedObjectClosure closure asserted = - extendObjectClosure - closure - [ object - | object <- asserted - , assertedObjectId object - `Set.notMember` checkedObjectIds closure - ] - - insertImportedFact - current facts pair = do - let (occurrence, proposition) = pair - fingerprint = semanticFactFingerprint occurrence - authority = semanticFactAuthority occurrence - _ <- - first ImportedFactMaterializationFailed - (Materialization.checkImportedOccurrence - (logicalBuilderTheory current) - fingerprint - occurrence - proposition - authority) - let authorization = - BuilderFactAuthorization - (logicalBuilderIdentity current) - (semanticFactSlot occurrence) - authority - authorized = - FactEntry proposition occurrence authorization - case Map.lookup fingerprint facts of - Nothing -> - pure (Map.insert fingerprint authorized facts) - Just existing - | equivalentAuthorizedFact existing authorized -> - pure facts - | otherwise -> - Left (ImportedFactCollision fingerprint) - - insertImportedAlias facts aliases (alias, origin) = do - let name = semanticAliasName alias - target = semanticAliasTarget alias - unless - (Map.member target facts) - (Left (ImportedAliasTargetMissing target)) - case Map.lookup name aliases of - Nothing -> - pure - (Map.insert - name - (ImportedAliasBinding target origin) - aliases) - Just (ImportedAliasBinding existingTarget existingOrigin) - | existingTarget == target -> - pure aliases - | otherwise -> - Left - (ImportedAliasCollision - name existingOrigin origin) - - insertImportedGlobal closure structures globals binding = do - let key = semanticGlobalBindingKey binding - target = semanticGlobalBindingTarget binding - _ <- - first - (ImportedGlobalTargetInvalid key target) - (validateSemanticGlobalBindingTarget - (structureOperationBindings structures) - closure binding) - case Map.lookup key globals of - Nothing -> pure (Map.insert key target globals) - Just existing - | existing == target -> pure globals - | otherwise -> - Left (ImportedGlobalCollision key existing target) - -insertSemanticStructure - :: CheckedObjectClosure - -> Map SemanticStructurePhrase ResolvedStructure - -> SemanticStructureDescriptor - -> Either - DeclarationError - (Map SemanticStructurePhrase ResolvedStructure) -insertSemanticStructure closure structures descriptor = do - validateSemanticStructureTargets closure descriptor - let structurePhrase = semanticStructureDescriptorPhrase descriptor - case Map.lookup structurePhrase structures of - Just (ResolvedStructure existing _ _) - | existing == descriptor -> Right structures - | otherwise -> - Left - (ImportedStructureCollision - structurePhrase existing descriptor) - Nothing -> do - parents <- traverse resolveParent - (semanticStructureDescriptorParents descriptor) - inherited <- foldM mergeParentOperations Map.empty parents - complete <- foldM insertOwnOperation inherited - (semanticStructureDescriptorOperations descriptor) - let ancestors = - Set.unions - [ Set.insert - (semanticStructureDescriptorPhrase - (resolvedStructureDescriptor parent)) - parentAncestors - | parent@(ResolvedStructure _ parentAncestors _) <- parents - ] - resolved = ResolvedStructure descriptor ancestors complete - Right (Map.insert structurePhrase resolved structures) - where - resolveParent parentPhrase = - maybe - (Left - (SemanticStructureParentMissing - (semanticStructureDescriptorPhrase descriptor) - parentPhrase)) - Right - (Map.lookup parentPhrase structures) - - mergeParentOperations operations - (ResolvedStructure _descriptor _ancestors parentOperations) = - foldM insertInheritedOperation operations - (Map.toAscList parentOperations) - - insertInheritedOperation operations (symbol, operation) = - insertResolvedOperation symbol operation operations - - insertOwnOperation operations operation = - insertResolvedOperation - (semanticStructureOperationSymbol operation) - (ResolvedStructureOperation - (semanticStructureOperationObject operation) - (semanticStructureDescriptorPhrase descriptor)) - operations - - insertResolvedOperation symbol incoming operations = - case Map.lookup symbol operations of - Nothing -> Right (Map.insert symbol incoming operations) - Just (ResolvedStructureOperation existingObject existingOrigin) -> - case incoming of - ResolvedStructureOperation incomingObject incomingOrigin - | existingObject == incomingObject -> Right operations - | otherwise -> - Left - (SemanticStructureOperationConflict - symbol existingOrigin incomingOrigin) - -validateSemanticStructureTargets - :: CheckedObjectClosure - -> SemanticStructureDescriptor - -> Either DeclarationError () -validateSemanticStructureTargets closure descriptor = do - traverse_ validatePredicate - (semanticStructureDescriptorPredicate descriptor) - traverse_ validateOperation - (semanticStructureDescriptorOperations descriptor) - where - validatePredicate object = - validateObjectType - (SemanticStructurePredicateTargetInvalid - (semanticStructureDescriptorPhrase descriptor)) - object - (TyArrow TySet TyProp) - - validateOperation operation = - validateObjectType - (SemanticStructureOperationTargetInvalid - (semanticStructureDescriptorPhrase descriptor) - (semanticStructureOperationSymbol operation)) - (semanticStructureOperationObject operation) - (TyArrow TySet TySet) - - validateObjectType failure object expected = - case lookupCheckedObjectType object closure of - Nothing -> Left (failure object Nothing expected) - Just actual - | actual == expected -> Right () - | otherwise -> Left (failure object (Just actual) expected) - -equivalentAuthorizedFact - :: FactEntry BuilderFactAuthorization - -> FactEntry BuilderFactAuthorization - -> Bool -equivalentAuthorizedFact - (FactEntry leftProposition leftOccurrence - (BuilderFactAuthorization leftIdentity leftSlot leftAuthority)) - (FactEntry rightProposition rightOccurrence - (BuilderFactAuthorization rightIdentity rightSlot rightAuthority)) = - checkedPropositionId leftProposition - == checkedPropositionId rightProposition - && leftOccurrence == rightOccurrence - && leftIdentity == rightIdentity - && leftSlot == rightSlot - && leftAuthority == rightAuthority - --- | Driver-level form used before the first declaration of a consuming --- module. It changes only the private builder's imported fact environment; --- no declaration prefix or durable envelope is emitted. -importSealedModuleDriver - :: ImportedModuleEvidence - -> ModuleDriver failure () -importSealedModuleDriver evidence = ModuleDriver do - DriverState resolver builder prefix validationRun <- - State.get - let declaration = - initialDeclarationState - resolver - validationRun - EnvironmentImportMode - builder - result <- - liftIO - (Except.runExceptT - (State.runStateT - (runDeclaration - (importSealedModule evidence)) - declaration)) - case result of - Left failure -> - Except.throwError (DriverDeclarationFailed failure) - Right (_value, importedState) -> - State.put - (DriverState - resolver - (declarationBuilder importedState) - prefix - validationRun) - -useStagedCandidate - :: ReservedCandidate - -> CandidateProof ImportIx -useStagedCandidate premise = CandidateProof do - state <- State.get - let current = candidateProofCandidate state - declaration = candidateProofDeclaration state - State.lift - (Except.liftEither - (validateReservedCandidate - declaration - premise)) - State.lift - (Except.liftEither - (validateStrictCandidateStage premise current)) - pending <- - maybe - (State.lift - (Except.throwError - (StagedPremiseNotAuthorized - (reservedCandidateSlot premise)))) - pure - (Map.lookup - (reservedCandidateSlot premise) - (declarationPending declaration)) - let proposedAuthority = - validationTarget (pendingCandidateCertificate pending) - checkedStage <- - State.lift - (Except.liftEither - (prepareCheckedDeclarationStage - declaration - (candidateProofObjectClosure state) - [(premise, proposedAuthority)])) - stagedProposition <- - State.lift - (Except.liftEither - (useCheckedStageFact checkedStage current premise)) - proposition <- consumePendingFact pending state - unless - (checkedPropositionId stagedProposition - == checkedPropositionId proposition) - (State.lift - (Except.throwError - (PlanningFactContractMismatch - (reservedCandidateSlot premise)))) - updated <- State.get - appendCandidatePremise proposition updated - -validateStrictCandidateStage - :: ReservedCandidate - -> ReservedCandidate - -> Either DeclarationError () -validateStrictCandidateStage premise current = - unless - (reservedStage premise < reservedStage current) - (Left - (StagedPremiseNotEarlier - (reservedCandidateSlot premise) - (reservedCandidateStage premise) - (reservedCandidateSlot current) - (reservedCandidateStage current))) - -prepareCheckedDeclarationStage - :: DeclarationState - -> CheckedObjectClosure - -> [(ReservedCandidate, FactAuthority)] - -> Either DeclarationError CheckedDeclarationStage -prepareCheckedDeclarationStage declaration closure candidates = do - entries <- foldM insertCandidate Map.empty candidates - pure (CheckedDeclarationStage ownSlot closure entries) - where - builder = declarationBuilder declaration - ownSlot = declarationOwnSlot declaration - - insertCandidate entries (candidate, authority) = do - validateReservedCandidate declaration candidate - let slot = reservedCandidateSlot candidate - unless - (factAuthorityTheorem authority - == candidateTheoremReference builder candidate) - (Left (PlanningFactContractMismatch slot)) - when - (Map.member slot entries) - (Left (PlanningFactContractMismatch slot)) - let occurrence = candidateOccurrence candidate authority - evidence = PlanningEvidence - authority - (Just - (PlanningProvenance - ownSlot - (reservedStage candidate) - slot)) - pure - (Map.insert - slot - (FactEntry - (candidateCheckedProposition candidate) - occurrence - evidence) - entries) - -useCheckedStageFact - :: CheckedDeclarationStage - -> ReservedCandidate - -> ReservedCandidate - -> Either DeclarationError CheckedPropositionContent -useCheckedStageFact - (CheckedDeclarationStage ownSlot closure entries) - current - premise = do - validateStrictCandidateStage premise current - let slot = reservedCandidateSlot premise - FactEntry proposition occurrence - (PlanningEvidence authority provenance) <- - maybe - (Left (PlanningFactContractMismatch slot)) - Right - (Map.lookup slot entries) - unless - ( provenance - == Just - (PlanningProvenance - ownSlot - (reservedStage premise) - slot) - && semanticFactSlot occurrence == slot - && semanticFactAuthority occurrence == authority - && checkedPropositionId proposition - == checkedPropositionId - (candidateCheckedProposition premise) - && propositionMatchesClosure closure proposition - ) - (Left (PlanningFactContractMismatch slot)) - pure proposition - -propositionMatchesClosure - :: CheckedObjectClosure - -> CheckedPropositionContent - -> Bool -propositionMatchesClosure closure proposition = - case validateAssertedPropositionContent - closure - (checkedPropositionId proposition) - (frozenCoreTerm (checkedPropositionTerm proposition)) of - Right _ -> True - Left _ -> False - -candidateOccurrence - :: ReservedCandidate - -> FactAuthority - -> SemanticFactOccurrence -candidateOccurrence - (ReservedCandidate _ _ _ _ slot - (CandidateSpec _ eligibility _aliases)) - authority = - semanticFactOccurrence slot authority eligibility - -candidateAliases :: ReservedCandidate -> [SemanticName] -candidateAliases - (ReservedCandidate _ _ _ _ _ - (CandidateSpec _ _ aliases)) = - aliases - -proveLocalKernelClaim - :: CheckedPropositionContent - -> KernelDerivation ObjectId - -> CandidateProof LocalClaim -proveLocalKernelClaim proposition derivation = CandidateProof do - state <- State.get - void - (State.lift - (Except.liftEither - (replayCandidateKernel proposition derivation state))) - let candidate = candidateProofCandidate state - declaration = candidateProofDeclaration state - pure - (LocalClaim - (logicalBuilderIdentity - (candidateProofBuilder state)) - (declarationInvocation declaration) - (reservedCandidateSlot candidate) - proposition) - -useLocalClaim :: LocalClaim -> CandidateProof ImportIx -useLocalClaim - (LocalClaim identity invocation slot proposition) = - CandidateProof do - state <- State.get - let builder = candidateProofBuilder state - declaration = candidateProofDeclaration state - candidate = candidateProofCandidate state - unless - ( identity == logicalBuilderIdentity builder - && invocation == declarationInvocation declaration - && slot == reservedCandidateSlot candidate - ) - (State.lift - (Except.throwError LocalClaimOutsideCandidate)) - appendCandidatePremise proposition state - - -authorizeKernelProofCandidate - :: ReservedCandidate - -> CandidateProof (KernelDerivation ObjectId) - -> Declaration () -authorizeKernelProofCandidate candidate proof = - authorizeOneCandidate candidate \initial -> do - (derivation, final) <- - State.runStateT (runCandidateProof proof) initial - when - (isNothing (candidateProofCachedValidation final)) - (void - (Except.liftEither - (replayCandidateKernel - (candidateCheckedProposition candidate) - derivation - final))) - completeCandidateWithValidation - candidate - (CheckedSourceProof - (acceptedRequestIds final)) - (candidateProofSafety final) - final - -authorizeKernelConstructionCandidate - :: KernelConstructionDescriptor - -> ReservedCandidate - -> CandidateProof (KernelDerivation ObjectId) - -> Declaration () -authorizeKernelConstructionCandidate descriptor candidate proof = - authorizeOneCandidate candidate \initial -> do - (derivation, final) <- - State.runStateT (runCandidateProof proof) initial - when - (isNothing (candidateProofCachedValidation final)) do - replayed <- - Except.liftEither - (replayCandidateKernel - (candidateCheckedProposition candidate) - derivation - final) - Except.liftEither - (validateKernelConstruction - descriptor - (candidateCheckedProposition candidate) - replayed - final) - completeCandidateWithValidation - candidate - (CheckedKernelConstruction descriptor) - (candidateProofSafety final) - final - -authorizeDefinitionEquationCandidate - :: ObjectId - -> ReservedCandidate - -> Declaration () -authorizeDefinitionEquationCandidate identity candidate = - authorizeOneCandidate candidate \initial -> do - when - (isNothing (candidateProofCachedValidation initial)) - (unless - (matchesDefinitionEquation - identity - (candidateCheckedProposition candidate) - initial) - (Except.throwError - DefinitionEquationCandidateMismatch)) - completeCandidateWithValidation - candidate - (CheckedKernelConstruction - (CheckedDefinitionEquation identity)) - (candidateProofSafety initial) - initial - -authorizeSourceAxiomCandidate - :: ReservedCandidate - -> Declaration () -authorizeSourceAxiomCandidate candidate = - authorizeOneCandidate candidate \initial -> - let safety = - addCandidateEscape - SourceAxiom - initialCandidateSafety - in completeCandidateWithValidation - candidate - SourceAxiomAuthorization - safety - initial - --- | Complete one exact deterministic datatype as a single trusted family. --- The descriptor, objects, and complete candidate batch must agree exactly. --- Law semantics are trusted to the sole production compiler in --- "Checking.Exact.Datatype"; this boundary validates its complete inventory, --- not the meaning of each generated proposition. -authorizeDatatypeCompilationCandidates - :: DatatypeCompilationDescriptor - -> ObjectId - -> NonEmpty ObjectId - -> NonEmpty ReservedCandidate - -> Declaration () -authorizeDatatypeCompilationCandidates - suppliedDescriptor carrier constructors candidates = - Declaration do - state <- State.get - let builder = declarationBuilder state - objectInventory = carrier : NonEmpty.toList constructors - declaredObjects = - assertedObjectId - <$> reverse (declarationObjectsReversed state) - reservedCandidates = - Map.elems (declarationReservations state) - theoremInventory = - candidateTheoremReference builder - <$> NonEmpty.toList candidates - expectedDescriptor = - datatypeCompilationDescriptor - carrier - constructors - theoremInventory - stages = - nubOrd - (reservedCandidateStage - <$> NonEmpty.toList candidates) - unless - ( suppliedDescriptor == expectedDescriptor - && declaredObjects == objectInventory - && reservedCandidates == NonEmpty.toList candidates - && length stages == 1 - ) - (State.lift - (Except.throwError - DatatypeCompilationDescriptorMismatch)) - runDeclaration - (traverse_ - (authorizeDatatypeCandidate suppliedDescriptor) - candidates) - -authorizeDatatypeCandidate - :: DatatypeCompilationDescriptor - -> ReservedCandidate - -> Declaration () -authorizeDatatypeCandidate descriptor candidate = - authorizeOneCandidate candidate \initial -> - completeCandidateWithValidation - candidate - (TrustedCompilation - (DatatypeCompilation descriptor)) - initialCandidateSafety - initial - -authorizeOmittedCandidate - :: ReservedCandidate - -> CandidateProof () - -> Declaration () -authorizeOmittedCandidate candidate proof = - authorizeOneCandidate candidate \initial -> do - cached <- - selectProofCandidateValidation candidate initial - let preparedInitial = - initial - { candidateProofCachedValidation = cached - } - ((), final) <- - State.runStateT (runCandidateProof proof) preparedInitial - let safety = candidateProofSafety final - unless - (Omitted - `elem` escapeKindsToList - (authoritySafetyEscapeKinds - (candidateSafetyAuthority safety))) - (Except.throwError OmittedProofDidNotRecordUse) - completeCandidateWithValidation - candidate - OmittedAuthorization - safety - final - --- | Retain the closed candidate-target path while scoped proof composition is --- introduced. It uses the same environment validation as local obligations. -acceptVampireObligation - :: Provers.PreparedTypedProverTask - SemanticFactOccurrenceFingerprint - Void - origin - ObjectId - -> CandidateProof () -acceptVampireObligation prepared = - acceptValidatedVampireTask - (validateCandidateVampireProblem prepared) - prepared - --- | Validate one internally prepared scoped obligation, then retain its exact --- accepted request. The trusted caller remains responsible for structural --- local-proof composition. -acceptPreparedVampireObligation - :: (Eq local, Eq origin) - => PreparedVampireObligation local origin - -> CandidateProof () -acceptPreparedVampireObligation - (PreparedVampireObligation expected prepared) = - acceptValidatedVampireTask - (validatePreparedVampireProblem expected prepared) - prepared - --- | Prepare and execute the current closed candidate using exactly the --- staged premises already consumed by its trusted declaration compiler. -acceptCurrentCandidateVampire :: CandidateProof () -acceptCurrentCandidateVampire = - prepareCurrentCandidateVampire - >>= acceptPreparedVampireObligation - --- | Prepare the current closed candidate without executing its request. The --- declaration-owned batch authorizer uses this seam only after all strictly --- earlier staged premises have been consumed. -prepareCurrentCandidateVampire - :: CandidateProof (PreparedVampireObligation Void ()) -prepareCurrentCandidateVampire = CandidateProof do - initial <- State.get - let builder = candidateProofBuilder initial - closure = candidateProofObjectClosure initial - target = candidateCheckedProposition - (candidateProofCandidate initial) - premises = - [ proposition - | CandidatePremise proposition <- - reverse (candidateProofPremisesReversed initial) - ] - resolver = - declarationVampireResolver - (candidateProofDeclaration initial) - preparation = - prepareClosedCandidateVampire - builder closure target premises - preparedResult <- - State.lift - (liftIO - (measureVampirePreparation resolver preparation)) - prepared <- - State.lift - (Except.liftEither - (first - CurrentCandidateVampirePreparationFailed - preparedResult)) - pure prepared - -prepareClosedCandidateVampire - :: BuilderState evidence - -> CheckedObjectClosure - -> CheckedPropositionContent - -> [CheckedPropositionContent] - -> Either - (VampireObligationPreparationError Void) - (PreparedVampireObligation Void ()) -prepareClosedCandidateVampire builder closure target premises = do - supportedTarget <- - first - VampireObligationClaimProjectionFailed - (Backend.projectSupportedProposition - globalType - (Vector.empty :: Vector (Void, CoreType)) - (closed target)) - locals <- - traverse - prepareLocal - (zip [0 :: Natural ..] premises) - prepareVampireObligationWith - Provers.DirectTask - builder - closure - supportedTarget - locals - [] - VampireLocalPremises - where - globalType = (`lookupCheckedObjectType` closure) - closed proposition = - embedClosedCore [] - (checkedPropositionTerm proposition) - - prepareLocal (index, proposition) = do - let ordinal = Backend.localPremiseOrdinal index - supported <- - first - (VampireObligationLocalProjectionFailed ordinal) - (Backend.projectSupportedProposition - globalType - (Vector.empty :: Vector (Void, CoreType)) - (closed proposition)) - first - (VampireObligationLocalClassificationFailed ordinal) - (Backend.typedLocalPremise - globalType ordinal () supported) - -acceptValidatedVampireTask - :: (CandidateProofState - -> ExceptT DeclarationError IO CandidateProofState) - -> Provers.PreparedTypedProverTask - SemanticFactOccurrenceFingerprint - local - origin - ObjectId - -> CandidateProof () -acceptValidatedVampireTask validate prepared = CandidateProof do - initial <- State.get - validated <- State.lift (validate initial) - result <- - case candidateProofCachedValidation initial of - Nothing -> do - let resolver = - declarationVampireResolver - (candidateProofDeclaration initial) - Just <$> State.lift (resolveOneVampire resolver prepared) - Just _validation -> - pure Nothing - final <- - State.lift - (acceptVampireBatchMemberResult - prepared result validated) - State.put final - --- | Complete one checked source candidate after all of its obligations have --- been accepted in source order. The enclosing proof declaration owns the --- exact syntax key and selects live or cached execution before this action. -authorizeVampireCandidate - :: ReservedCandidate - -> CandidateProof () - -> Declaration () -authorizeVampireCandidate candidate proof = - authorizeOneCandidate candidate \initial -> do - cached <- - selectProofCandidateValidation candidate initial - let preparedInitial = - initial - { candidateProofCachedValidation = cached - } - ((), final) <- - State.runStateT (runCandidateProof proof) preparedInitial - case acceptedRequestIds final of - [] -> - Except.throwError - VampireProofHasNoAcceptedObligations - requests -> - completeCandidateWithValidation - candidate - (CheckedSourceProof requests) - (candidateProofSafety final) - final - -data PreparedVampireCandidateBatchMember = - PreparedVampireCandidateBatchMember - !Location - !ReservedCandidate - !(Provers.PreparedTypedProverTask - SemanticFactOccurrenceFingerprint - Void - () - ObjectId) - !CandidateProofState - -data ResolvedVampireCandidateBatchMember = - ResolvedVampireCandidateBatchMember - !PreparedVampireCandidateBatchMember - !(Maybe - (Either - Provers.ProverProcessError - Provers.ProverAnswer)) - --- | Authorize one complete, source-ordered candidate stage whose members are --- mutually independent and each require exactly one closed Vampire request. --- Every member is prepared and validated against the same declaration --- baseline. Results are applied only after the complete live batch returns, --- so no same-stage sibling can become authority for another member. -authorizeVampireCandidateBatch - :: NonEmpty - ( Location - , ReservedCandidate - , CandidateProof (PreparedVampireObligation Void ()) - ) - -> Declaration () -authorizeVampireCandidateBatch inputs = Declaration do - unprepared <- State.get - baseline <- - State.lift - (Except.liftEither - (prepareDeclarationClosure unprepared)) - let supplied = - [ candidate - | (_location, candidate, _prepare) <- NonEmpty.toList inputs - ] - frontier = declarationAuthorizationFrontier baseline - expected = - List.filter - ((== CandidateStage frontier) . reservedStage) - (Map.elems (declarationReservations baseline)) - traverse_ - (State.lift - . Except.liftEither - . validateReservedCandidate baseline) - supplied - traverse_ - (\candidate -> - when - (Map.member - (reservedCandidateSlot candidate) - (declarationPending baseline)) - (State.lift - (Except.throwError - (CandidateAlreadyAuthorized - (reservedCandidateSlot candidate))))) - supplied - unless (supplied == expected) - (State.lift - (Except.throwError - (VampireCandidateBatchMismatch - (reservedCandidateSlot <$> expected) - (reservedCandidateSlot <$> supplied)))) - prepared <- - State.lift - (traverse - (prepareVampireCandidateBatchMember baseline) - inputs) - State.lift - (validateCachedVampireCandidateBatch - (NonEmpty.toList prepared)) - let live = - [ task - | PreparedVampireCandidateBatchMember - _location _candidate task final <- - NonEmpty.toList prepared - , isNothing (candidateProofCachedValidation final) - ] - liveResults <- - case NonEmpty.nonEmpty live of - Nothing -> pure [] - Just nonempty -> do - let resolver = - declarationVampireResolver baseline - results <- - liftIO - (resolveSynchronousVampireBatch resolver nonempty) - State.lift - (Except.liftEither - (validateVampireResolverResultCount - (length live) - results)) - pending <- - State.lift - (completeVampireCandidateBatch - (NonEmpty.toList prepared) - liveResults) - let withPending = - baseline - { declarationPending = - foldl' - (\entries item@(PendingCandidate candidate _ _) -> - Map.insert - (reservedCandidateSlot - candidate) - item - entries) - (declarationPending baseline) - pending - } - State.put (advanceAuthorizationFrontier withPending) - -prepareVampireCandidateBatchMember - :: DeclarationState - -> ( Location - , ReservedCandidate - , CandidateProof (PreparedVampireObligation Void ()) - ) - -> ExceptT DeclarationError IO PreparedVampireCandidateBatchMember -prepareVampireCandidateBatchMember - baseline (location, candidate, prepare) = do - initial <- - Except.liftEither - (initialCandidateProofState baseline candidate) - cached <- selectProofCandidateValidation candidate initial - let selected = - initial{candidateProofCachedValidation = cached} - (obligation, preparedState) <- - State.runStateT - (runCandidateProof - (locateProofObligation location prepare)) - selected - unless (null (acceptedRequestIds preparedState)) - (Except.throwError - (VampireCandidateBatchProofShapeMismatch - (reservedCandidateSlot candidate))) - let PreparedVampireObligation expected task = obligation - validated <- - Except.withExceptT - (ProofObligationFailedAt location) - (validatePreparedVampireProblem - expected task preparedState) - pure - (PreparedVampireCandidateBatchMember - location candidate task validated) - -completeVampireCandidateBatch - :: [PreparedVampireCandidateBatchMember] - -> [Either Provers.ProverProcessError Provers.ProverAnswer] - -> ExceptT DeclarationError IO [PendingCandidate] -completeVampireCandidateBatch members liveResults = do - resolved <- - Except.liftEither - (associateVampireCandidateBatchResults - members liveResults) - -- Integrity dominates ranked proof failure: validate every accepted run - -- before inspecting any ordinary process or prover rejection. - traverse_ validateAcceptedVampireBatchMember resolved - traverse_ rejectOrdinaryVampireBatchMember resolved - traverse completeVampireCandidateBatchMember resolved - -validateCachedVampireCandidateBatch - :: [PreparedVampireCandidateBatchMember] - -> ExceptT DeclarationError IO () -validateCachedVampireCandidateBatch = - traverse_ \member -> - when - (preparedVampireCandidateBatchMemberIsCached member) - (void - (completeVampireCandidateBatchMember - (ResolvedVampireCandidateBatchMember member Nothing))) - -associateVampireCandidateBatchResults - :: [PreparedVampireCandidateBatchMember] - -> [Either Provers.ProverProcessError Provers.ProverAnswer] - -> Either - DeclarationError - [ResolvedVampireCandidateBatchMember] -associateVampireCandidateBatchResults members = - go members - where - go [] [] = Right [] - go [] results = - Left - (VampireResolverBatchSizeMismatch - 0 - (length results)) - go (member : remaining) results - | preparedVampireCandidateBatchMemberIsCached member = - (ResolvedVampireCandidateBatchMember member Nothing :) - <$> go remaining results - | otherwise = - case results of - [] -> - Left (VampireResolverBatchSizeMismatch 1 0) - current : later -> - (ResolvedVampireCandidateBatchMember - member (Just current) :) - <$> go remaining later - -preparedVampireCandidateBatchMemberIsCached - :: PreparedVampireCandidateBatchMember - -> Bool -preparedVampireCandidateBatchMemberIsCached - (PreparedVampireCandidateBatchMember - _location _candidate _task state) = - isJust (candidateProofCachedValidation state) - -validateAcceptedVampireBatchMember - :: ResolvedVampireCandidateBatchMember - -> ExceptT DeclarationError IO () -validateAcceptedVampireBatchMember - (ResolvedVampireCandidateBatchMember - (PreparedVampireCandidateBatchMember - location _candidate task _validated) - result) = - Except.withExceptT - (ProofObligationFailedAt location) - (validateAcceptedVampireResult task result) - -rejectOrdinaryVampireBatchMember - :: ResolvedVampireCandidateBatchMember - -> ExceptT DeclarationError IO () -rejectOrdinaryVampireBatchMember - (ResolvedVampireCandidateBatchMember - (PreparedVampireCandidateBatchMember - location _candidate _task _validated) - result) = - traverse_ - (Except.throwError . ProofObligationFailedAt location) - (result >>= vampireResultFailure) - -completeVampireCandidateBatchMember - :: ResolvedVampireCandidateBatchMember - -> ExceptT DeclarationError IO PendingCandidate -completeVampireCandidateBatchMember - (ResolvedVampireCandidateBatchMember - (PreparedVampireCandidateBatchMember - location candidate task validated) - result) = do - final <- - Except.withExceptT - (ProofObligationFailedAt location) - (applyAcceptedVampireResult task result validated) - completeCandidateWithValidation - candidate - (CheckedSourceProof (acceptedRequestIds final)) - (candidateProofSafety final) - final - -acceptVampireBatchMemberResult - :: Provers.PreparedTypedProverTask - SemanticFactOccurrenceFingerprint - local - origin - ObjectId - -> Maybe (Either Provers.ProverProcessError Provers.ProverAnswer) - -> CandidateProofState - -> ExceptT DeclarationError IO CandidateProofState -acceptVampireBatchMemberResult prepared result validated = do - validateAcceptedVampireResult prepared result - traverse_ Except.throwError (result >>= vampireResultFailure) - applyAcceptedVampireResult prepared result validated - -validateAcceptedVampireResult - :: Provers.PreparedTypedProverTask - SemanticFactOccurrenceFingerprint - local - origin - ObjectId - -> Maybe (Either Provers.ProverProcessError Provers.ProverAnswer) - -> ExceptT DeclarationError IO () -validateAcceptedVampireResult prepared result = do - let request = Provers.preparedTypedProverRequest prepared - traverse_ - (\resolved -> - traverse_ - (\accepted -> - unless - (Provers.acceptedVampireRequestId accepted - == Provers.preparedVerificationRequestId request) - (Except.throwError VampireRequestMismatch)) - (either (const Nothing) Provers.provedVampireRun resolved)) - result - -vampireResultFailure - :: Either Provers.ProverProcessError Provers.ProverAnswer - -> Maybe DeclarationError -vampireResultFailure = \case - Left failure -> - Just (VampireProcessFailed failure) - Right answer -> - case Provers.provedVampireRun answer of - Nothing -> - Just (VampireObligationRejected answer) - Just _accepted -> - Nothing - -applyAcceptedVampireResult - :: Provers.PreparedTypedProverTask - SemanticFactOccurrenceFingerprint - local - origin - ObjectId - -> Maybe (Either Provers.ProverProcessError Provers.ProverAnswer) - -> CandidateProofState - -> ExceptT DeclarationError IO CandidateProofState -applyAcceptedVampireResult prepared result validated = do - traverse_ - (\resolved -> - case vampireResultFailure resolved of - Just failure -> - Except.throwError failure - Nothing -> - pure ()) - result - let request = Provers.preparedTypedProverRequest prepared - requestId = Provers.preparedVerificationRequestId request - pure - validated - { candidateProofAcceptedRequestsReversed = - requestId - : candidateProofAcceptedRequestsReversed validated - } - -selectProofCandidateValidation - :: ReservedCandidate - -> CandidateProofState - -> ExceptT - DeclarationError - IO - (Maybe Materialization.CandidateValidation) -selectProofCandidateValidation candidate initial = - case declarationValidationMode - (candidateProofDeclaration initial) of - EnvironmentImportMode -> - Except.throwError - ProofValidationOutsideProofDeclaration - ProofValidationMode{} -> do - (syntax, cached) <- - runDeclarationLookup - (lookupProofValidation candidate) - initial - pure - ((\record -> - Materialization.candidateProofValidation - record syntax) - <$> cached) - DeclarationValidationMode{} -> - pure (candidateProofCachedValidation initial) - -completeCandidateWithValidation - :: ReservedCandidate - -> DirectAuthorization - -> CandidateSafety - -> CandidateProofState - -> ExceptT DeclarationError IO PendingCandidate -completeCandidateWithValidation candidate direct safety final = do - pending <- - Except.liftEither - (freshCompletion - candidate - direct - safety - final) - traverse_ - (\validation -> - case Materialization.checkCandidateValidation - (logicalBuilderTheory - (candidateProofBuilder final)) - (logicalBuilderPrefix - (candidateProofBuilder final)) - (candidateCheckedProposition candidate) - (validationTarget - (pendingCandidateCertificate pending)) - direct - validation of - Left failure -> - liftIO - (throwIO - (CachedValidationIntegrityError failure)) - Right () -> - pure ()) - (candidateProofCachedValidation final) - pure pending - -runDeclarationLookup - :: Declaration value - -> CandidateProofState - -> ExceptT DeclarationError IO value -runDeclarationLookup action initial = - fst - <$> State.runStateT - (runDeclaration action) - (candidateProofDeclaration initial) - -pendingCandidateCertificate :: PendingCandidate -> ValidationCertificate -pendingCandidateCertificate - (PendingCandidate _ certificate _) = - certificate - -acceptedRequestIds :: CandidateProofState -> [PreparedRequestId] -acceptedRequestIds = - reverse . candidateProofAcceptedRequestsReversed - -freshCompletion - :: ReservedCandidate - -> DirectAuthorization - -> CandidateSafety - -> CandidateProofState - -> Either DeclarationError PendingCandidate -freshCompletion candidate direct safety proofState = do - let builder = candidateProofBuilder proofState - declaration = candidateProofDeclaration proofState - reference = candidateTheoremReference builder candidate - authority = candidateFactAuthority reference safety - void - (first DeclarationPropositionValidationFailed - (validateAssertedPropositionContent - (candidateProofObjectClosure proofState) - (checkedPropositionId - (candidateCheckedProposition candidate)) - (frozenCoreTerm - (checkedPropositionTerm - (candidateCheckedProposition candidate))))) - certificate <- - first ValidationCertificateFailed - (validationCertificate authority direct) - let authorization = - PendingFactAuthorization - (logicalBuilderIdentity builder) - (logicalBuilderPrefix builder) - (declarationInvocation declaration) - (reservedCandidateSlot candidate) - authority - (reservedStage candidate) - pure - (PendingCandidate - candidate - certificate - authorization) - -authorizeOneCandidate - :: ReservedCandidate - -> (CandidateProofState - -> ExceptT DeclarationError IO PendingCandidate) - -> Declaration () -authorizeOneCandidate candidate complete = Declaration do - unprepared <- State.get - state <- - State.lift - (Except.liftEither - (prepareDeclarationClosure unprepared)) - State.lift - (Except.liftEither - (validateReservedCandidate state candidate)) - when - (Map.member - (reservedCandidateSlot candidate) - (declarationPending state)) - (State.lift - (Except.throwError - (CandidateAlreadyAuthorized - (reservedCandidateSlot candidate)))) - unless - (reservedStage candidate - == CandidateStage - (declarationAuthorizationFrontier state)) - (State.lift - (Except.throwError - (CandidateOutsideAuthorizationFrontier - (reservedCandidateSlot candidate) - (reservedCandidateStage candidate) - (declarationAuthorizationFrontier state)))) - initial <- State.lift - (Except.liftEither - (initialCandidateProofState state candidate)) - pending <- State.lift (complete initial) - let state' = - state - { declarationPending = - Map.insert - (reservedCandidateSlot candidate) - pending - (declarationPending state) - } - State.put (advanceAuthorizationFrontier state') - -advanceAuthorizationFrontier - :: DeclarationState - -> DeclarationState -advanceAuthorizationFrontier state - | all stageCompleted currentCandidates = - state - { declarationAuthorizationFrontier = - frontier + 1 - } - | otherwise = - state - where - frontier = declarationAuthorizationFrontier state - currentCandidates = - List.filter - ((== CandidateStage frontier) . reservedStage) - (Map.elems (declarationReservations state)) - stageCompleted candidate = - Map.member - (reservedCandidateSlot candidate) - (declarationPending state) - -initialCandidateProofState - :: DeclarationState - -> ReservedCandidate - -> Either DeclarationError CandidateProofState -initialCandidateProofState declaration candidate = do - closure <- declarationClosure declaration - cached <- - cachedDeclarationCandidateValidation declaration candidate - pure CandidateProofState - { candidateProofDeclaration = declaration - , candidateProofObjectClosure = closure - , candidateProofCandidate = candidate - , candidateProofCachedValidation = cached - , candidateProofPremisesReversed = [] - , candidateProofPremiseCount = 0 - , candidateProofSafety = initialCandidateSafety - , candidateProofAcceptedRequestsReversed = [] - } - -cachedDeclarationCandidateValidation - :: DeclarationState - -> ReservedCandidate - -> Either - DeclarationError - (Maybe Materialization.CandidateValidation) -cachedDeclarationCandidateValidation declaration candidate = - case declarationValidationSelection declaration of - DeclarationValidationUnselected -> - Right Nothing - FreshDeclarationValidation -> - Right Nothing - CachedDeclarationValidation - syntax objects theorems record ordinals -> - maybe - (Left - (CachedDeclarationCandidateMissing - (reservedCandidateSlot candidate))) - (Right - . Just - . Materialization.candidateDeclarationValidation - record syntax objects theorems) - (Map.lookup - (reservedCandidateSlot candidate) - ordinals) - -reservedStage :: ReservedCandidate -> CandidateStage -reservedStage - (ReservedCandidate _ _ _ stage _ _) = - stage - -validateReservedCandidate - :: DeclarationState - -> ReservedCandidate - -> Either DeclarationError () -validateReservedCandidate declaration candidate = do - let builder = declarationBuilder declaration - ReservedCandidate - identity prefix invocation _stage slot _spec = candidate - unless - ( identity == logicalBuilderIdentity builder - && prefix == logicalBuilderPrefix builder - && invocation == declarationInvocation declaration - && Map.lookup slot - (declarationReservations declaration) - == Just candidate - ) - (Left (CandidateOutsideDeclaration slot)) - -instance Eq ReservedCandidate where - left == right = - reservedCandidateKey left == reservedCandidateKey right - -reservedCandidateKey - :: ReservedCandidate - -> (BuilderIdentity, PrefixContextId, DeclarationInvocation, CandidateStage, FactSlot) -reservedCandidateKey - (ReservedCandidate identity prefix invocation stage slot _spec) = - (identity, prefix, invocation, stage, slot) - - -consumeBuilderAuthorizedFact - :: FactEntry BuilderFactAuthorization - -> CandidateProofState - -> StateT - CandidateProofState - (ExceptT DeclarationError IO) - CheckedPropositionContent -consumeBuilderAuthorizedFact - (FactEntry proposition occurrence authorization) - state = do - let builder = candidateProofBuilder state - BuilderFactAuthorization - identity slot authority = authorization - unless - ( identity == logicalBuilderIdentity builder - && slot == semanticFactSlot occurrence - && authority == semanticFactAuthority occurrence - ) - (State.lift - (Except.throwError BuilderFactAuthorizationMismatch)) - accumulateAuthorizedSafety - proposition - authority - state - pure proposition - -consumePendingFact - :: PendingCandidate - -> CandidateProofState - -> StateT - CandidateProofState - (ExceptT DeclarationError IO) - CheckedPropositionContent -consumePendingFact - (PendingCandidate premise certificate authorization) - state = do - let builder = candidateProofBuilder state - declaration = candidateProofDeclaration state - PendingFactAuthorization - identity prefix invocation slot authority - premiseStageValue = authorization - current = candidateProofCandidate state - unless - ( identity == logicalBuilderIdentity builder - && prefix == logicalBuilderPrefix builder - && invocation == declarationInvocation declaration - && slot == reservedCandidateSlot premise - && authority == validationTarget certificate - && premiseStageValue == reservedStage premise - ) - (State.lift - (Except.throwError PendingFactAuthorizationMismatch)) - unless - (reservedStage premise < reservedStage current) - (State.lift - (Except.throwError - (StagedPremiseNotEarlier - (reservedCandidateSlot premise) - (reservedCandidateStage premise) - (reservedCandidateSlot current) - (reservedCandidateStage current)))) - let proposition = candidateCheckedProposition premise - accumulateAuthorizedSafety - proposition - authority - state - pure proposition - -accumulateAuthorizedSafety - :: CheckedPropositionContent - -> FactAuthority - -> CandidateProofState - -> StateT - CandidateProofState - (ExceptT DeclarationError IO) - () -accumulateAuthorizedSafety proposition authority state = do - let expected = - theoremRef - (logicalBuilderTheory - (candidateProofBuilder state)) - (checkedPropositionId proposition) - safety <- - State.lift - (Except.liftEither - (first FactSafetyFailed - (accumulateFactSafety - expected - authority - (candidateProofSafety state)))) - State.put state{candidateProofSafety = safety} - -registerKernelImport - :: CheckedPropositionContent - -> CandidateProof ImportIx -registerKernelImport proposition = CandidateProof do - state <- State.get - appendCandidatePremise proposition state - -appendCandidatePremise - :: CheckedPropositionContent - -> CandidateProofState - -> StateT - CandidateProofState - (ExceptT DeclarationError IO) - ImportIx -appendCandidatePremise proposition state = do - let index = candidateProofPremiseCount state - State.put - state - { candidateProofPremisesReversed = - CandidatePremise proposition - : candidateProofPremisesReversed state - , candidateProofPremiseCount = index + 1 - } - pure (importIx index) - -findPendingByFingerprint - :: SemanticFactOccurrenceFingerprint - -> Map FactSlot PendingCandidate - -> Maybe PendingCandidate -findPendingByFingerprint fingerprint = - find - (\(PendingCandidate candidate certificate _authorization) -> - semanticFactOccurrenceFingerprint - (reservedCandidateSlot candidate) - (validationTarget certificate) - == fingerprint) - . Map.elems - -candidateImportJudgments - :: CandidateProofState - -> Either DeclarationError (Vector (DerivationImportJudgment ObjectId)) -candidateImportJudgments state = - Vector.fromList - <$> traverse - (\(CandidatePremise proposition) -> - first DerivationImportFailed - (derivationImportJudgment - (checkedPropositionTerm proposition))) - (reverse - (candidateProofPremisesReversed state)) - -replayCandidateKernel - :: CheckedPropositionContent - -> KernelDerivation ObjectId - -> CandidateProofState - -> Either - DeclarationError - (ReplayedKernelDerivation ObjectId) -replayCandidateKernel proposition derivation state = do - imports <- candidateImportJudgments state - let builder = candidateProofBuilder state - closure = candidateProofObjectClosure state - first KernelCompletionFailed - (replayKernelDerivation - (logicalBuilderFoundation builder) - defaultKernelReplayLimits - (`lookupCheckedObjectType` closure) - imports - (checkedPropositionTerm proposition) - derivation) - -validateKernelConstruction - :: KernelConstructionDescriptor - -> CheckedPropositionContent - -> ReplayedKernelDerivation ObjectId - -> CandidateProofState - -> Either DeclarationError () -validateKernelConstruction descriptor proposition replayed proofState = - unless matches - (Left KernelConstructionDescriptorMismatch) - where - builder = candidateProofBuilder proofState - noImports = Set.null (replayedKernelImportUses replayed) - noFoundation = Set.null (replayedKernelFoundationUses replayed) - noRules = Set.null (replayedKernelRuleUses replayed) - - matches = - case descriptor of - FoundationLeaf tag -> - noImports - && replayedKernelFoundationUses replayed - == Set.singleton tag - && noRules - && checkedPropositionTerm proposition - == mapFrozenGlobals - absurd - (foundationAxiomFrozen - (logicalBuilderFoundation builder) - tag) - GuardedFoundationRules rules -> - replayedKernelRuleUses replayed - == guardedRuleTags rules - CheckedDefinitionEquation identity -> - noImports - && noFoundation - && noRules - && matchesDefinitionEquation identity proposition proofState - -matchesDefinitionEquation - :: ObjectId - -> CheckedPropositionContent - -> CandidateProofState - -> Bool -matchesDefinitionEquation identity proposition proofState = - case lookupCheckedObjectContent - identity - (candidateProofObjectClosure proofState) of - Just - (TransparentObjectContent - contentTheory coreType body) -> - contentTheory - == logicalBuilderTheory - (candidateProofBuilder proofState) - && frozenCoreTerm (checkedPropositionTerm proposition) - `elem` definitionEquationTargets identity coreType body - _ -> - False - -definitionEquationTargets - :: ObjectId - -> CoreType - -> CanonicalTerm ObjectId - -> [CanonicalTerm ObjectId] -definitionEquationTargets identity coreType body = - CEq coreType (CGlobal identity) body - : case (coreType, body) of - (TyArrow TySet TyProp, CLam TySet predicate) -> - [ CForall TySet - (CEq TyProp - (CApp (CGlobal identity) (CBound 0)) - predicate) - ] - _ -> [] - - -validateCandidateVampireProblem - :: Provers.PreparedTypedProverTask - SemanticFactOccurrenceFingerprint - Void - origin - ObjectId - -> CandidateProofState - -> ExceptT DeclarationError IO CandidateProofState -validateCandidateVampireProblem prepared initial = do - let problem = Provers.preparedTypedProverLogicalProblem prepared - claim = Backend.typedProblemClaim problem - target = candidateCheckedProposition - (candidateProofCandidate initial) - Except.liftEither do - unless - ( Vector.null (Backend.supportedPropositionSupport claim) - && Backend.supportedPropositionTerm claim - == frozenCoreTerm (checkedPropositionTerm target) - ) - (Left VampireTargetMismatch) - unless - (Vector.null (Backend.typedProblemLocalPremises problem)) - (Left VampireLocalPremisesNotSupported) - validateVampireProblemEnvironment prepared initial - -validatePreparedVampireProblem - :: (Eq local, Eq origin) - => Backend.TypedProblem - SemanticFactOccurrenceFingerprint - local - origin - ObjectId - -> Provers.PreparedTypedProverTask - SemanticFactOccurrenceFingerprint - local - origin - ObjectId - -> CandidateProofState - -> ExceptT DeclarationError IO CandidateProofState -validatePreparedVampireProblem expectedProblem prepared initial = do - let problem = Provers.preparedTypedProverLogicalProblem prepared - Except.liftEither - (unless (problem == expectedProblem) - (Left VampireTargetMismatch) - ) - validateVampireProblemEnvironment prepared initial - -validateVampireProblemEnvironment - :: Provers.PreparedTypedProverTask - SemanticFactOccurrenceFingerprint - local - origin - ObjectId - -> CandidateProofState - -> ExceptT DeclarationError IO CandidateProofState -validateVampireProblemEnvironment prepared initial = do - let problem = Provers.preparedTypedProverLogicalProblem prepared - builder = candidateProofBuilder initial - closure = candidateProofObjectClosure initial - Except.liftEither do - traverse_ - (\(identity, reportedType) -> - unless - (lookupCheckedObjectType identity closure - == Just reportedType) - (Left (VampireGlobalTypeMismatch identity))) - (Map.toList (Backend.typedProblemGlobalTypes problem)) - traverse_ - (validateFoundationAuxiliary builder) - (Backend.typedProblemAuxiliaries problem) - execCandidateProof initial do - traverse_ - validatePremise - (Backend.typedProblemGlobalPremises problem) - where - validatePremise selected = do - let fingerprint = Backend.typedBackendFactReference selected - proposition <- consumeAuthorizedFact fingerprint - state <- CandidateProof State.get - unless - ( Backend.supportedPropositionTerm - (Backend.typedBackendFactProposition selected) - == frozenCoreTerm - (checkedPropositionTerm proposition) - ) - (failCandidateProof - (VampirePremiseMismatch fingerprint)) - let closure = - candidateProofObjectClosure state - supported <- - either - (const - (failCandidateProof - (VampirePremiseCapabilityMismatch - fingerprint))) - pure - (Backend.supportedProposition - Vector.empty - (embedClosedCore - [] - (checkedPropositionTerm proposition))) - capability <- - either - (const - (failCandidateProof - (VampirePremiseCapabilityMismatch - fingerprint))) - pure - (Backend.classifySupportedProposition - (`lookupCheckedObjectType` closure) - supported) - unless - (capability - == Backend.typedBackendFactCapability selected) - (failCandidateProof - (VampirePremiseCapabilityMismatch fingerprint)) - - validateFoundationAuxiliary builder auxiliary = do - let tag = Backend.typedProblemAuxiliaryTag auxiliary - actual = - Backend.supportedPropositionTerm - (Backend.typedProblemAuxiliaryProposition auxiliary) - expectedTerm = - frozenCoreTerm - (mapFrozenGlobals - absurd - (foundationAxiomFrozen - (logicalBuilderFoundation builder) - tag)) - unless (actual == expectedTerm) - (Left (VampireFoundationMismatch tag)) - -execCandidateProof - :: CandidateProofState - -> CandidateProof value - -> ExceptT DeclarationError IO CandidateProofState -execCandidateProof initial action = - snd <$> State.runStateT (runCandidateProof action) initial - -failCandidateProof - :: DeclarationError - -> CandidateProof value -failCandidateProof = - CandidateProof . State.lift . Except.throwError - -data ValidationMode - = EnvironmentImportMode - | ProofValidationMode !ProofSyntaxId - | DeclarationValidationMode !DeclarationSyntaxId - -data PlannedVampireDisposition - = PlannedCachedRequest !Provers.PreparedVerificationRequest - | PlannedLiveRequest - !Provers.PreparedVerificationRequest - !Provers.VampireHandle - | PlannedSynchronousRequest !Provers.PreparedVerificationRequest - -data PlannedCandidate = PlannedCandidate - !ReservedCandidate - !FactAuthority - !DirectAuthorization - ![PlannedVampireDisposition] - -data PlannedReplayRequest - = ReplayLive - !Provers.PreparedVerificationRequest - !Provers.VampireHandle - | ReplaySynchronous !Provers.PreparedVerificationRequest - -data PlannedValidationSelection - = PlannedFreshValidation - | PlannedProofValidation - !ProofValidationKey - !ProofValidationRecord - | PlannedCompiledValidation - !DeclarationValidationKey - !DeclarationValidationRecord - --- | One completely lowered and submitted declaration. It carries no --- builder authorization or materialized certificate; all authority is --- reconstructed by the source-ordered admission cursor. -data PlannedDeclaration body = PlannedDeclaration - !(CheckedDeclaration body) - !PrefixContextId - !PrefixContextId - !DeclarationInterfaceDelta - ![AssertedObject] - ![CheckedPropositionContent] - ![NonEmpty PlannedCandidate] - !PlannedValidationSelection - -plannedDeclarationPreviousPrefix - :: PlannedDeclaration body - -> PrefixContextId -plannedDeclarationPreviousPrefix - (PlannedDeclaration _checked previous _next _delta - _objects _propositions _candidates _validation) = - previous - -plannedDeclarationNextPrefix - :: PlannedDeclaration body - -> PrefixContextId -plannedDeclarationNextPrefix - (PlannedDeclaration _checked _previous next _delta - _objects _propositions _candidates _validation) = - next - -plannedDeclarationDelta - :: PlannedDeclaration body - -> DeclarationInterfaceDelta -plannedDeclarationDelta - (PlannedDeclaration _checked _previous _next delta - _objects _propositions _candidates _validation) = - delta - -newtype PlanningIntegrityError = PlanningIntegrityError Text - deriving stock (Show) - -instance Exception.Exception PlanningIntegrityError - --- | Advance the authority-free semantic projection through one complete --- checked declaration. Validation selection and every deterministic check --- finish before the first live request is submitted. -planCheckedDeclaration - :: CheckedDeclaration body - -> LoweringDriver (Either DeclarationError (PlannedDeclaration body)) -planCheckedDeclaration checked@(CheckedDeclaration - mode objects explicitPropositions globals descriptors stages - _body) = LoweringDriver do - state@(LoweringState resolver (ProspectiveBuilder builder) validationRun) <- - State.get - prepared <- liftIO (Except.runExceptT do - closure <- - Except.liftEither - (first DeclarationObjectValidationFailed - (extendObjectClosure - (logicalBuilderObjectClosure builder) - objects)) - let reservedStages = - reservePlanningStages builder stages - plannedWithoutDisposition <- - Except.liftEither - (preparePlannedCandidates builder closure reservedStages) - let orderedCandidates = fmap (fmap fst) plannedWithoutDisposition - occurrences = - [ candidateOccurrence reserved authority - | stage <- plannedWithoutDisposition - , (PlannedCandidate reserved authority _direct _requests, - _requestValues) <- toList stage - ] - aliases = - [ semanticAlias alias - (semanticFactFingerprint - (candidateOccurrence reserved authority)) - | stage <- plannedWithoutDisposition - , (PlannedCandidate reserved authority _direct _requests, - _requestValues) <- toList stage - , alias <- candidateAliases reserved - ] - allCandidatePropositions = - candidateCheckedProposition . fst - <$> concatMap toList reservedStages - propositions = - stableUniqueBy checkedPropositionId - (explicitPropositions <> allCandidatePropositions) - objectIds = assertedObjectId <$> objects - propositionIds = checkedPropositionId <$> propositions - ownSlot = declarationSlot - (logicalBuilderOwner builder) - (localDeclarationOrdinal - (logicalBuilderNextDeclaration builder)) - traverse_ - (\proposition -> - void - (Except.liftEither - (first DeclarationPropositionValidationFailed - (validateAssertedPropositionContent - closure - (checkedPropositionId proposition) - (frozenCoreTerm - (checkedPropositionTerm proposition)))))) - propositions - (resolvedStructures, delta, next) <- - Except.liftEither - (buildCheckedDeclarationDelta - builder closure ownSlot occurrences aliases objectIds - propositionIds (reverse globals) (reverse descriptors)) - selection <- - selectPlannedValidation - validationRun mode builder objects orderedCandidates - planned <- - submitPlannedCandidates resolver selection - plannedWithoutDisposition - let nextBuilder = - appendProspectiveBuilder - closure resolvedStructures delta next planned builder - declaration = - PlannedDeclaration checked - (logicalBuilderPrefix builder) - next delta objects propositions planned selection - pure (declaration, nextBuilder)) - case prepared of - Left failure -> pure (Left failure) - Right (declaration, nextBuilder) -> do - let LoweringState currentResolver _current currentValidation = state - State.put - (LoweringState - currentResolver - (ProspectiveBuilder nextBuilder) - currentValidation) - pure (Right declaration) - -reservePlanningStages - :: BuilderState PlanningEvidence - -> [NonEmpty CheckedCandidate] - -> [NonEmpty (ReservedCandidate, CandidatePlanningSpec)] -reservePlanningStages builder = - snd . mapAccumPlanning reserveStage (logicalBuilderNextFact builder) - where - invocation = DeclarationInvocation (logicalBuilderNextInvocation builder) - reserveStage nextFact (stageIndex, specs) = - let candidates = - NonEmpty.zipWith - (\offset (CheckedCandidate spec planning) -> - ( ReservedCandidate - (logicalBuilderIdentity builder) - (logicalBuilderPrefix builder) - invocation - (CandidateStage stageIndex) - (factSlot - (logicalBuilderOwner builder) - (localFactOrdinal (nextFact + offset))) - spec - , planning - )) - (0 :| [1..]) - specs - in ( nextFact + fromIntegral (NonEmpty.length specs) - , candidates - ) - - mapAccumPlanning action initial values = - go initial (zip [0..] values) - where - go accumulator [] = (accumulator, []) - go accumulator (value : remaining) = - let (next, result) = action accumulator value - (final, results) = go next remaining - in (final, result : results) - -preparePlannedCandidates - :: BuilderState PlanningEvidence - -> CheckedObjectClosure - -> [NonEmpty (ReservedCandidate, CandidatePlanningSpec)] - -> Either - DeclarationError - [NonEmpty (PlannedCandidate, [CheckedPlannedVampireRequest])] -preparePlannedCandidates builder closure stages = - snd <$> mapAccumM prepareStage Map.empty (zip [0..] stages) - where - prepareStage earlier (stageIndex, stage) = do - (sameStage, planned) <- - mapAccumM - (prepareCandidate stageIndex earlier) - Map.empty - (zip [0..] (toList stage)) - pure (Map.union earlier sameStage, NonEmpty.fromList planned) - - prepareCandidate stageIndex earlier sameStage - (candidateIndex, (candidate, contract)) = do - let position = PlannedCandidatePosition stageIndex candidateIndex - (direct, safety, requests) <- - prepareCandidatePlanningContract - builder closure earlier position candidate contract - let authority = - candidateFactAuthority - (candidateTheoremReference builder candidate) - safety - planned = PlannedCandidate candidate authority direct [] - pure - ( Map.insert position (candidate, authority) sameStage - , (planned, requests) - ) - - mapAccumM action initial values = - go initial [] values - where - go accumulator outputs = \case - [] -> pure (accumulator, reverse outputs) - value : remaining -> do - (next, output) <- action accumulator value - go next (output : outputs) remaining - -prepareCandidatePlanningContract - :: BuilderState PlanningEvidence - -> CheckedObjectClosure - -> Map PlannedCandidatePosition (ReservedCandidate, FactAuthority) - -> PlannedCandidatePosition - -> ReservedCandidate - -> CandidatePlanningSpec - -> Either - DeclarationError - ( DirectAuthorization - , CandidateSafety - , [CheckedPlannedVampireRequest] - ) -prepareCandidatePlanningContract builder closure earlier current candidate - (CandidatePlanningSpec direct extraFacts staged requests) = do - safetyWithFacts <- - foldM (accumulatePlanningFact builder closure) - initialCandidateSafety - (stableUniqueBy id - ( extraFacts - <> concatMap requestFacts requests - )) - safetyWithStages <- - foldM consumeStage safetyWithFacts staged - let safety = case direct of - PlanningSourceAxiom -> - addCandidateEscape SourceAxiom safetyWithStages - PlanningOmitted -> - addCandidateEscape Omitted safetyWithStages - _ -> safetyWithStages - requestIds = requestIdentity <$> requests - directAuthorization = case direct of - PlanningDefinitionEquation identity -> - CheckedKernelConstruction - (CheckedDefinitionEquation identity) - PlanningSourceAxiom -> SourceAxiomAuthorization - PlanningTrustedDatatype descriptor -> - TrustedCompilation (DatatypeCompilation descriptor) - PlanningKernelConstruction descriptor -> - CheckedKernelConstruction descriptor - PlanningCheckedSourceProof -> - CheckedSourceProof requestIds - PlanningOmitted -> OmittedAuthorization - validatePlanningDirect directAuthorization safety - pure (directAuthorization, safety, requests) - where - requestFacts - (CheckedPlannedVampireRequest _location _request facts) = facts - requestIdentity - (CheckedPlannedVampireRequest _location request _facts) = - Provers.preparedVerificationRequestId request - - consumeStage safety position = do - (premise, authority) <- - maybe - (Left - (PlanningFactContractMismatch - (reservedCandidateSlot candidate))) - Right - (Map.lookup position earlier) - let PlannedCandidatePosition premiseStage _premiseIndex = position - PlannedCandidatePosition currentStage _currentIndex = current - unless (premiseStage < currentStage) - (Left - (StagedPremiseNotEarlier - (reservedCandidateSlot premise) - premiseStage - (reservedCandidateSlot candidate) - currentStage)) - first FactSafetyFailed - (accumulateFactSafety - (candidateTheoremReference builder premise) - authority - safety) - -accumulatePlanningFact - :: BuilderState PlanningEvidence - -> CheckedObjectClosure - -> CandidateSafety - -> SemanticFactOccurrenceFingerprint - -> Either DeclarationError CandidateSafety -accumulatePlanningFact builder closure safety fingerprint = do - FactEntry proposition occurrence (PlanningEvidence authority _provenance) <- - maybe - (Left (AuthorizedFactNotVisible fingerprint)) - Right - (Map.lookup fingerprint (logicalBuilderFacts builder)) - unless - ( semanticFactFingerprint occurrence == fingerprint - && semanticFactAuthority occurrence == authority - && propositionMatchesClosure closure proposition - ) - (Left (PlanningFactContractMismatch (semanticFactSlot occurrence))) - first FactSafetyFailed - (accumulateFactSafety - (theoremRef - (logicalBuilderTheory builder) - (checkedPropositionId proposition)) - authority - safety) - -validatePlanningDirect - :: DirectAuthorization - -> CandidateSafety - -> Either DeclarationError () -validatePlanningDirect direct safety = - case direct of - SourceAxiomAuthorization -> - unless - (candidateSafetyAuthority safety - == authoritySafety (singletonEscapeKind SourceAxiom)) - (Left - (ValidationCertificateFailed - (SourceAxiomSafetyMismatch - (candidateSafetyAuthority safety)))) - OmittedAuthorization -> - unless - (Omitted `elem` escapeKindsToList - (authoritySafetyEscapeKinds - (candidateSafetyAuthority safety))) - (Left - (ValidationCertificateFailed - (OmittedSafetyMissing - (candidateSafetyAuthority safety)))) - _ -> pure () - -selectPlannedValidation - :: ValidationRun - -> CheckedDeclarationMode - -> BuilderState PlanningEvidence - -> [AssertedObject] - -> [NonEmpty PlannedCandidate] - -> ExceptT DeclarationError IO PlannedValidationSelection -selectPlannedValidation validationRun mode builder objects stages = - case mode of - CheckedProofMode syntax -> - case concatMap toList stages of - [planned@(PlannedCandidate _candidate authority _direct _)] -> do - let key = proofValidationKey - (theoremId (factAuthorityTheorem authority)) - syntax - (logicalBuilderPrefix builder) - cached <- case validationRun of - FreshValidation -> pure Nothing - WarmValidation (ValidationLookup lookupProof _) -> - liftIO (lookupProof key) - traverse_ - (validateProof planned syntax) - cached - pure case cached of - Nothing -> PlannedFreshValidation - Just record -> PlannedProofValidation key record - candidates -> - Except.throwError - (CheckedProofCandidateCountMismatch - (length candidates)) - CheckedCompiledMode syntax -> do - let planned = concatMap toList stages - objectIds = assertedObjectId <$> objects - theorems = - theoremId . factAuthorityTheorem . plannedAuthority - <$> planned - key = declarationValidationKey syntax - (logicalBuilderPrefix builder) objectIds theorems - cached <- case validationRun of - FreshValidation -> pure Nothing - WarmValidation (ValidationLookup _ lookupDeclaration) -> - liftIO (lookupDeclaration key) - traverse_ - (validateCompiled planned syntax objectIds theorems) - cached - pure case cached of - Nothing -> PlannedFreshValidation - Just record -> PlannedCompiledValidation key record - where - plannedAuthority (PlannedCandidate _ authority _ _) = authority - - validateProof - (PlannedCandidate candidate authority direct _) - syntax record = - case Materialization.checkCandidateValidation - (logicalBuilderTheory builder) - (logicalBuilderPrefix builder) - (candidateCheckedProposition candidate) - authority direct - (Materialization.candidateProofValidation record syntax) of - Left failure -> - liftIO - (throwIO (CachedValidationIntegrityError failure)) - Right () -> pure () - - validateCompiled planned syntax objectIds theorems record = do - case Materialization.checkDeclarationValidationRecord - (logicalBuilderPrefix builder) - syntax objectIds theorems record of - Left failure -> - liftIO - (throwIO (CachedValidationIntegrityError failure)) - Right () -> pure () - traverse_ - (\(ordinal, - PlannedCandidate candidate authority direct _) -> - case Materialization.checkCandidateValidation - (logicalBuilderTheory builder) - (logicalBuilderPrefix builder) - (candidateCheckedProposition candidate) - authority direct - (Materialization.candidateDeclarationValidation - record syntax objectIds theorems ordinal) of - Left failure -> - liftIO - (throwIO - (CachedValidationIntegrityError failure)) - Right () -> pure ()) - (zip [0..] planned) - -submitPlannedCandidates - :: VampireResolver - -> PlannedValidationSelection - -> [NonEmpty (PlannedCandidate, [CheckedPlannedVampireRequest])] - -> ExceptT DeclarationError IO [NonEmpty PlannedCandidate] -submitPlannedCandidates resolver selection candidates - | cached = - pure (fmap (fmap cachedCandidate) candidates) - | otherwise = do - let requests = - [ request - | stage <- candidates - , (_candidate, plannedRequests) <- toList stage - , CheckedPlannedVampireRequest - _location request _facts <- plannedRequests - ] - case resolver of - VampireResolver SynchronousVampireResolution{} _observe -> - pure (fmap (fmap synchronousCandidate) candidates) - VampireResolver - (AsynchronousVampireSubmission submit) _observe -> do - handles <- case NonEmpty.nonEmpty requests of - Nothing -> pure [] - Just nonempty -> do - submitted <- liftIO (submit nonempty) - unless - (NonEmpty.length submitted == length requests) - (Except.throwError - (VampireResolverBatchSizeMismatch - (length requests) - (NonEmpty.length submitted))) - pure (toList submitted) - let (planned, remaining) = - State.runState - (traverse (traverse liveCandidate) candidates) - handles - unless (null remaining) - (Except.throwError - (VampireResolverBatchSizeMismatch - (length requests) - (length requests + length remaining))) - pure planned - where - cached = case selection of - PlannedFreshValidation -> False - PlannedProofValidation{} -> True - PlannedCompiledValidation{} -> True - - cachedCandidate - (PlannedCandidate candidate authority direct _dispositions, - requests) = - PlannedCandidate candidate authority direct - [ PlannedCachedRequest request - | CheckedPlannedVampireRequest - _location request _facts <- requests - ] - - liveCandidate - (PlannedCandidate candidate authority direct _dispositions, - requests) = do - dispositions <- traverse takeHandle requests - pure (PlannedCandidate candidate authority direct dispositions) - - synchronousCandidate - (PlannedCandidate candidate authority direct _dispositions, - requests) = - PlannedCandidate candidate authority direct - [ PlannedSynchronousRequest request - | CheckedPlannedVampireRequest - _location request _facts <- requests - ] - - takeHandle - (CheckedPlannedVampireRequest _location request _facts) = do - remaining <- State.get - case remaining of - [] -> - impossible - "validated prospective handle count became exhausted" - handle : later -> do - State.put later - pure (PlannedLiveRequest request handle) - -appendProspectiveBuilder - :: CheckedObjectClosure - -> Map SemanticStructurePhrase ResolvedStructure - -> DeclarationInterfaceDelta - -> PrefixContextId - -> [NonEmpty PlannedCandidate] - -> BuilderState PlanningEvidence - -> BuilderState PlanningEvidence -appendProspectiveBuilder closure structures delta next planned builder = - builder - { logicalBuilderPrefix = next - , logicalBuilderObjectClosure = closure - , logicalBuilderFacts = - foldl' insertPlanningFact - (logicalBuilderFacts builder) - (concatMap toList planned) - , logicalBuilderAliases = - foldl' - (\entries alias -> - Map.insert - (semanticAliasName alias) - (ImportedAliasBinding - (semanticAliasTarget alias) - (ImportedAliasOrigin - (declarationDeltaSlot delta) - (semanticAliasTarget alias))) - entries) - (logicalBuilderAliases builder) - (declarationDeltaAliases delta) - , logicalBuilderGlobals = - foldl' - (\entries binding -> - Map.insert - (semanticGlobalBindingKey binding) - (semanticGlobalBindingTarget binding) - entries) - (logicalBuilderGlobals builder) - (semanticEnvironmentBindings - (declarationDeltaEnvironment delta)) - , logicalBuilderStructures = structures - , logicalBuilderDeltas = delta : logicalBuilderDeltas builder - , logicalBuilderNextDeclaration = - logicalBuilderNextDeclaration builder + 1 - , logicalBuilderNextFact = - logicalBuilderNextFact builder - + fromIntegral (sum (fmap NonEmpty.length planned)) - , logicalBuilderNextInvocation = - logicalBuilderNextInvocation builder + 1 - } - where - insertPlanningFact entries - (PlannedCandidate candidate authority _direct _requests) = - let occurrence = candidateOccurrence candidate authority - fingerprint = semanticFactFingerprint occurrence - evidence = PlanningEvidence authority - (Just - (PlanningProvenance - (declarationDeltaSlot delta) - (reservedStageValue candidate) - (reservedCandidateSlot candidate))) - in Map.insert fingerprint - (FactEntry - (candidateCheckedProposition candidate) - occurrence - evidence) - entries - - -- Keep the constructor match private while storing exact stage provenance. - reservedStageValue - (ReservedCandidate _identity _prefix _invocation stage _slot _spec) = - stage - --- | Admit one checked declaration through the existing authoritative --- source-order cursor. The callback interprets a closed family recipe over --- freshly reserved stage slots; it is not retained in the checked value. -admitCheckedDeclaration - :: CheckedDeclaration body - -> (body -> [NonEmpty ReservedCandidate] -> Declaration ()) - -> ModuleDriver failure CommittedDeclarationBatch -admitCheckedDeclaration - (CheckedDeclaration - mode objects propositions globals structures stages body) - authorize = - snd <$> do - case mode of - CheckedProofMode syntax -> - commitProofDeclaration syntax do - reserved <- installCheckedStructure - authorize body reserved - CheckedCompiledMode syntax -> - commitCompiledDeclaration syntax do - reserved <- installCheckedStructure - authorizeCompiledDeclaration - (authorize body reserved) - where - installCheckedStructure = do - traverse_ addDeclarationObject objects - traverse_ addDeclarationProposition propositions - traverse_ - (\binding -> - stageSemanticGlobalBinding - (semanticGlobalBindingKey binding) - (semanticGlobalBindingTarget binding)) - globals - traverse_ stageSemanticStructureDescriptor structures - traverse - (reserveCandidateBatch . fmap checkedCandidateSemanticSpec) - stages - - checkedCandidateSemanticSpec - (CheckedCandidate spec _planning) = spec - --- | Admit one retained plan against the real authorized builder. The family --- callback performs the existing authority checks, but every live resolver --- result comes from the handle submitted during planning and every validation --- lookup is the inert selection retained by the plan. -admitPlannedCheckedDeclaration - :: PlannedDeclaration body - -> (body -> [NonEmpty ReservedCandidate] -> Declaration ()) - -> ModuleDriver failure CommittedDeclarationBatch -admitPlannedCheckedDeclaration planned@(PlannedDeclaration - checked previous _expectedNext _expectedDelta _objects _propositions - candidates selection) authorize = ModuleDriver do - DriverState originalResolver builder prefix originalValidation <- - State.get - unless (logicalBuilderPrefix builder == previous) - (liftIO - (throwIO - (PlanningIntegrityError - "planned declaration predecessor does not match the admitted builder"))) - liveRef <- liftIO - (newIORef - [ replay - | stage <- candidates - , PlannedCandidate _candidate _authority _direct dispositions <- - toList stage - , disposition <- dispositions - , replay <- case disposition of - PlannedCachedRequest{} -> [] - PlannedLiveRequest request handle -> - [ReplayLive request handle] - PlannedSynchronousRequest request -> - [ReplaySynchronous request] - ]) - replay <- liftIO (plannedReplayResolver originalResolver liveRef) - let validation = plannedAdmissionValidation selection - State.put (DriverState replay builder prefix validation) - batch <- runDriverStep (admitCheckedDeclaration checked authorize) - remaining <- liftIO (readIORef liveRef) - unless (null remaining) - (liftIO - (throwIO - (PlanningIntegrityError - "admission did not consume every planned live request"))) - liftIO (validateAdmittedPlan planned batch) - DriverState _replay admittedBuilder admittedPrefix _plannedValidation <- - State.get - State.put - (DriverState - originalResolver admittedBuilder admittedPrefix originalValidation) - pure batch - -plannedReplayResolver - :: VampireResolver - -> IORef [PlannedReplayRequest] - -> IO VampireResolver -plannedReplayResolver original liveRef = - pure - (vampireBatchResolverWithPreparationObserver resolve - (observeVampirePreparation original)) - where - resolve - :: forall local origin. - NonEmpty - (Provers.PreparedTypedProverTask - SemanticFactOccurrenceFingerprint - local - origin - ObjectId) - -> IO - (NonEmpty - (Either - Provers.ProverProcessError - Provers.ProverAnswer)) - resolve tasks = do - expected <- atomicModifyIORef' liveRef \remaining -> - let amount = NonEmpty.length tasks - (selected, later) = splitAt amount remaining - in (later, selected) - unless (length expected == NonEmpty.length tasks) - (throwIO - (PlanningIntegrityError - "admission requested a different number of live Vampire results")) - traverse_ validateExpected (zip (toList tasks) expected) - case expected of - ReplayLive{} : _ -> do - unless (all isLive expected) - (throwIO - (PlanningIntegrityError - "planned resolver batch mixed execution modes")) - results <- traverse awaitOne expected - maybe - (throwIO - (PlanningIntegrityError - "an admission resolver batch was unexpectedly empty")) - pure - (NonEmpty.nonEmpty results) - ReplaySynchronous{} : _ -> - resolveSynchronousVampireBatch original tasks - [] -> - throwIO - (PlanningIntegrityError - "an admission resolver batch was unexpectedly empty") - - validateExpected (task, replay) = do - let actual = Provers.preparedTypedProverRequest task - expected = replayRequest replay - unless (actual == expected) - (throwIO - (PlanningIntegrityError - "admission request differs from its planned exact request")) - - awaitOne (ReplayLive expected handle) = - Provers.awaitPreparedVampireRequest expected handle - awaitOne ReplaySynchronous{} = - impossible "validated live resolver batch changed execution mode" - - replayRequest = \case - ReplayLive request _handle -> request - ReplaySynchronous request -> request - - isLive = \case - ReplayLive{} -> True - ReplaySynchronous{} -> False - -plannedAdmissionValidation - :: PlannedValidationSelection - -> ValidationRun -plannedAdmissionValidation = \case - PlannedFreshValidation -> FreshValidation - PlannedProofValidation expected record -> - WarmValidation - (validationLookup - (\actual -> - if actual == expected - then pure (Just record) - else throwIO - (PlanningIntegrityError - "proof validation key changed during admission")) - (\_actual -> pure Nothing)) - PlannedCompiledValidation expected record -> - WarmValidation - (validationLookup - (\_actual -> pure Nothing) - (\actual -> - if actual == expected - then pure (Just record) - else throwIO - (PlanningIntegrityError - "declaration validation key changed during admission"))) - -validateAdmittedPlan - :: PlannedDeclaration body - -> CommittedDeclarationBatch - -> IO () -validateAdmittedPlan - (PlannedDeclaration _checked expectedPrevious expectedNext expectedDelta - expectedObjects expectedPropositions candidates selection) - batch = do - let expectedContracts = - [ (authority, direct) - | stage <- candidates - , PlannedCandidate _candidate authority direct _requests <- - toList stage - ] - actualCertificates = - (proofValidationRecordCertificate - <$> committedBatchProofValidations batch) - <> maybe - [] - declarationValidationRecordCertificates - (committedBatchDeclarationValidation batch) - actualContracts = - [ ( validationTarget certificate - , validationDirectAuthorization certificate - ) - | certificate <- actualCertificates - ] - validationAgrees = case selection of - PlannedFreshValidation -> True - PlannedProofValidation _ record -> - committedBatchProofValidations batch == [record] - PlannedCompiledValidation _ record -> - committedBatchDeclarationValidation batch == Just record - unless - ( committedBatchPreviousPrefix batch == expectedPrevious - && committedBatchNextPrefix batch == expectedNext - && committedBatchDelta batch == expectedDelta - && committedBatchObjects batch == expectedObjects - && fmap propositionContract (committedBatchPropositions batch) - == fmap propositionContract expectedPropositions - && actualContracts == expectedContracts - && validationAgrees - ) - (throwIO - (PlanningIntegrityError - "admitted declaration differs from its prospective contract")) - where - propositionContract proposition = - ( checkedPropositionId proposition - , checkedPropositionTerm proposition - ) - -commitProofDeclaration - :: ProofSyntaxId - -> Declaration value - -> ModuleDriver failure - (value, CommittedDeclarationBatch) -commitProofDeclaration syntax = - commitDeclaration (ProofValidationMode syntax) - -commitCompiledDeclaration - :: DeclarationSyntaxId - -> Declaration value - -> ModuleDriver failure - (value, CommittedDeclarationBatch) -commitCompiledDeclaration syntax = - commitDeclaration (DeclarationValidationMode syntax) - -commitDeclaration - :: ValidationMode - -> Declaration value - -> ModuleDriver failure - (value, CommittedDeclarationBatch) -commitDeclaration mode action = ModuleDriver do - DriverState resolver builder pendingPrefix validationRun <- - State.get - let - declaration = - initialDeclarationState - resolver - validationRun - mode - builder - result <- - liftIO - (Except.runExceptT - (State.runStateT - (runDeclaration action) - declaration)) - case result of - Left err -> - Except.throwError (DriverDeclarationFailed err) - Right (value, prepared) -> - case appendDeclaration mode prepared of - Left err -> - Except.throwError (DriverDeclarationFailed err) - Right (builder', batch) -> - let prefix' = appendPendingBatch batch pendingPrefix - in do - State.put - (DriverState - resolver - builder' - prefix' - validationRun) - pure (value, batch) - -initialDeclarationState - :: VampireResolver - -> ValidationRun - -> ValidationMode - -> LogicalBuilder - -> DeclarationState -initialDeclarationState resolver validationRun validationMode builder = - DeclarationState - { declarationVampireResolver = resolver - , declarationValidationRun = validationRun - , declarationValidationMode = validationMode - , declarationValidationSelection = - DeclarationValidationUnselected - , declarationBuilder = builder - , declarationOwnSlot = - declarationSlot - (logicalBuilderOwner builder) - (localDeclarationOrdinal - (logicalBuilderNextDeclaration builder)) - , declarationInvocation = - DeclarationInvocation - (logicalBuilderNextInvocation builder) - , declarationObjectsReversed = [] - , declarationObjectClosure = Nothing - , declarationPropositionsReversed = [] - , declarationGlobalBindingsReversed = [] - , declarationStructureDescriptorsReversed = [] - , declarationReservations = Map.empty - , declarationPending = Map.empty - , declarationNextFact = logicalBuilderNextFact builder - , declarationNextStage = 0 - , declarationAuthorizationFrontier = 0 - } - -appendDeclaration - :: ValidationMode - -> DeclarationState - -> Either - DeclarationError - (LogicalBuilder, CommittedDeclarationBatch) -appendDeclaration mode declaration = do - let builder = declarationBuilder declaration - reservations = Map.elems (declarationReservations declaration) - pending = declarationPending declaration - unless - (Map.keysSet pending - == Map.keysSet (declarationReservations declaration)) - (Left DeclarationHasUnauthorizedCandidates) - unless - (declarationAuthorizationFrontier declaration - == declarationNextStage declaration) - (Left DeclarationAuthorizationFrontierIncomplete) - case mode of - DeclarationValidationMode{} -> - case declarationValidationSelection declaration of - DeclarationValidationUnselected -> - Left DeclarationValidationNotSelected - _ -> pure () - _ -> pure () - closure <- declarationClosure declaration - propositions <- validateDeclarationPropositions closure declaration - traverse_ (validatePendingAuthorization declaration) (Map.elems pending) - let orderedPending = - [ pendingCandidate - | reservation <- reservations - , let slot = reservedCandidateSlot reservation - , Just pendingCandidate <- [Map.lookup slot pending] - ] - occurrences = occurrenceFromPending <$> orderedPending - aliases = concatMap aliasesFromPending orderedPending - objectIds = - assertedObjectId - <$> reverse - (declarationObjectsReversed declaration) - propositionIds = - checkedPropositionId <$> propositions - (structures, delta, next) <- - buildCheckedDeclarationDelta - builder - closure - (declarationOwnSlot declaration) - occurrences - aliases - objectIds - propositionIds - (declarationGlobalBindingsReversed declaration) - (declarationStructureDescriptorsReversed declaration) - let previous = logicalBuilderPrefix builder - (proofValidations, declarationValidation) <- - buildValidationRecords - mode previous objectIds orderedPending - let builder' = - appendBuilderState - closure - structures - delta - next - orderedPending - builder - declaration - batch = - CommittedDeclarationBatch - (logicalBuilderOwner builder) - (declarationOwnSlot declaration) - previous - next - delta - (reverse - (declarationObjectsReversed declaration)) - propositions - proofValidations - declarationValidation - pure (builder', batch) - --- | Construct and collision-check one canonical semantic delta without --- inspecting fact evidence. This remains the admitted append path now and --- is the shared delta seam for the later prospective builder. -buildCheckedDeclarationDelta - :: BuilderState evidence - -> CheckedObjectClosure - -> DeclarationSlot - -> [SemanticFactOccurrence] - -> [SemanticAlias] - -> [ObjectId] - -> [PropositionId] - -> [SemanticGlobalBinding] - -> [SemanticStructureDescriptor] - -> Either - DeclarationError - ( Map SemanticStructurePhrase ResolvedStructure - , DeclarationInterfaceDelta - , PrefixContextId - ) -buildCheckedDeclarationDelta - builder closure slot occurrences aliases objectIds propositionIds - reversedBindings reversedDescriptors = do - let bindings = - List.sortOn - semanticGlobalBindingKey - (reverse reversedBindings) - descriptors = - List.sortOn - semanticStructureDescriptorPhrase - (reverse reversedDescriptors) - traverse_ - (\binding -> - first - (DeclarationGlobalTargetInvalid - (semanticGlobalBindingKey binding) - (semanticGlobalBindingTarget binding)) - (validateSemanticGlobalBindingTarget - (structureOperationBindings - (logicalBuilderStructures builder)) - closure binding)) - bindings - traverse_ - (\descriptor -> - let structurePhrase = semanticStructureDescriptorPhrase descriptor - in when - (Map.member structurePhrase - (logicalBuilderStructures builder)) - (Left (BuilderStructureCollision structurePhrase))) - descriptors - structures <- foldM - (insertSemanticStructure closure) - (logicalBuilderStructures builder) - descriptors - environment <- - first DeclarationEnvironmentFailed - (semanticEnvironmentWithStructures bindings descriptors) - delta <- - first DeclarationInterfaceFailed - (declarationInterfaceDelta - slot - occurrences - aliases - objectIds - propositionIds - environment) - validateBuilderCollisions builder delta - pure - ( structures - , delta - , nextPrefixContextId (logicalBuilderPrefix builder) delta - ) - -declarationClosure - :: DeclarationState - -> Either DeclarationError CheckedObjectClosure -declarationClosure declaration = - case declarationObjectClosure declaration of - Just closure -> - Right closure - Nothing -> - first DeclarationObjectValidationFailed - (extendObjectClosure - (logicalBuilderObjectClosure - (declarationBuilder declaration)) - (reverse - (declarationObjectsReversed declaration))) - -prepareDeclarationClosure - :: DeclarationState - -> Either DeclarationError DeclarationState -prepareDeclarationClosure declaration = do - closure <- declarationClosure declaration - pure declaration{declarationObjectClosure = Just closure} - -validateDeclarationPropositions - :: CheckedObjectClosure - -> DeclarationState - -> Either DeclarationError [CheckedPropositionContent] -validateDeclarationPropositions closure declaration = do - let explicit = - reverse - (declarationPropositionsReversed declaration) - reserved = - candidateCheckedProposition - <$> Map.elems - (declarationReservations declaration) - propositions = stableUniqueBy checkedPropositionId (explicit <> reserved) - traverse_ - (\proposition -> - void - (first DeclarationPropositionValidationFailed - (validateAssertedPropositionContent - closure - (checkedPropositionId proposition) - (frozenCoreTerm - (checkedPropositionTerm proposition))))) - propositions - pure propositions - -validatePendingAuthorization - :: DeclarationState - -> PendingCandidate - -> Either DeclarationError () -validatePendingAuthorization declaration - (PendingCandidate candidate certificate authorization) = do - validateReservedCandidate declaration candidate - let builder = declarationBuilder declaration - PendingFactAuthorization - identity prefix invocation slot authority stage = - authorization - unless - ( identity == logicalBuilderIdentity builder - && prefix == logicalBuilderPrefix builder - && invocation == declarationInvocation declaration - && slot == reservedCandidateSlot candidate - && authority == validationTarget certificate - && stage == reservedStage candidate - ) - (Left PendingFactAuthorizationMismatch) - -occurrenceFromPending - :: PendingCandidate - -> SemanticFactOccurrence -occurrenceFromPending - (PendingCandidate candidate certificate _authorization) = - candidateOccurrence candidate (validationTarget certificate) - -aliasesFromPending :: PendingCandidate -> [SemanticAlias] -aliasesFromPending pending@(PendingCandidate - candidate _certificate _authorization) = - let occurrence = occurrenceFromPending pending - fingerprint = semanticFactFingerprint occurrence - in (`semanticAlias` fingerprint) <$> candidateAliases candidate - -buildValidationRecords - :: ValidationMode - -> PrefixContextId - -> [ObjectId] - -> [PendingCandidate] - -> Either - DeclarationError - ([ProofValidationRecord], Maybe DeclarationValidationRecord) -buildValidationRecords mode prefix objects pending = - case mode of - EnvironmentImportMode -> - impossible - "environment import produced declaration validation records" - ProofValidationMode syntax -> - case pending of - [PendingCandidate _ certificate _] -> - let authority = validationTarget certificate - key = - proofValidationKey - (theoremId - (factAuthorityTheorem authority)) - syntax - prefix - in Right - ( [proofValidationRecord key certificate] - , Nothing - ) - _ -> - Left ProofDeclarationMustProduceOneFact - DeclarationValidationMode syntax -> - let certificates = - [ certificate - | PendingCandidate _ certificate _ <- pending - ] - theorems = - theoremId - . factAuthorityTheorem - . validationTarget - <$> certificates - key = - declarationValidationKey - syntax prefix objects theorems - in Right - ( [] - , Just - (declarationValidationRecord - key certificates) - ) - -validateBuilderCollisions - :: BuilderState evidence - -> DeclarationInterfaceDelta - -> Either DeclarationError () -validateBuilderCollisions builder delta = do - traverse_ - (\occurrence -> - when - (Map.member - (semanticFactFingerprint occurrence) - (logicalBuilderFacts builder)) - (Left - (BuilderFactCollision - (semanticFactFingerprint occurrence)))) - (declarationDeltaFacts delta) - traverse_ - (\alias -> - when - (Map.member - (semanticAliasName alias) - (logicalBuilderAliases builder)) - (Left - (BuilderAliasCollision - (semanticAliasName alias)))) - (declarationDeltaAliases delta) - traverse_ - (\identity -> - when - (identity - `Set.member` checkedObjectIds - (logicalBuilderObjectClosure builder)) - (Left (BuilderObjectCollision identity))) - (declarationDeltaObjects delta) - traverse_ - (\binding -> - case Map.lookup - (semanticGlobalBindingKey binding) - (logicalBuilderGlobals builder) of - Nothing -> pure () - Just existing -> - Left - (BuilderGlobalCollision - (semanticGlobalBindingKey binding) - existing)) - (semanticEnvironmentBindings - (declarationDeltaEnvironment delta)) - -appendBuilderState - :: CheckedObjectClosure - -> Map SemanticStructurePhrase ResolvedStructure - -> DeclarationInterfaceDelta - -> PrefixContextId - -> [PendingCandidate] - -> LogicalBuilder - -> DeclarationState - -> LogicalBuilder -appendBuilderState closure structures delta next pending builder declaration = - builder - { logicalBuilderPrefix = next - , logicalBuilderObjectClosure = closure - , logicalBuilderFacts = - foldl' - (insertAuthorizedFact builder) - (logicalBuilderFacts builder) - pending - , logicalBuilderAliases = - foldl' - (\entries alias -> - Map.insert - (semanticAliasName alias) - (ImportedAliasBinding - (semanticAliasTarget alias) - (ImportedAliasOrigin - (declarationDeltaSlot delta) - (semanticAliasTarget alias))) - entries) - (logicalBuilderAliases builder) - (declarationDeltaAliases delta) - , logicalBuilderGlobals = - foldl' - (\entries binding -> - Map.insert - (semanticGlobalBindingKey binding) - (semanticGlobalBindingTarget binding) - entries) - (logicalBuilderGlobals builder) - (semanticEnvironmentBindings - (declarationDeltaEnvironment delta)) - , logicalBuilderStructures = structures - , logicalBuilderDeltas = - delta : logicalBuilderDeltas builder - , logicalBuilderNextDeclaration = - logicalBuilderNextDeclaration builder + 1 - , logicalBuilderNextFact = - declarationNextFact declaration - , logicalBuilderNextInvocation = - logicalBuilderNextInvocation builder + 1 - } - -insertAuthorizedFact - :: LogicalBuilder - -> Map - SemanticFactOccurrenceFingerprint - (FactEntry BuilderFactAuthorization) - -> PendingCandidate - -> Map - SemanticFactOccurrenceFingerprint - (FactEntry BuilderFactAuthorization) -insertAuthorizedFact builder entries pending@(PendingCandidate - candidate certificate _pendingAuthorization) = - let occurrence = occurrenceFromPending pending - fingerprint = semanticFactFingerprint occurrence - authority = validationTarget certificate - authorization = - BuilderFactAuthorization - (logicalBuilderIdentity builder) - (reservedCandidateSlot candidate) - authority - in Map.insert - fingerprint - (FactEntry - (candidateCheckedProposition candidate) - occurrence - authorization) - entries - -stableUniqueBy :: Ord key => (value -> key) -> [value] -> [value] -stableUniqueBy key = - reverse . snd - . foldl' - (\(seen, values) value -> - let identity = key value - in if identity `Set.member` seen - then (seen, values) - else - ( Set.insert identity seen - , value : values - )) - (Set.empty, []) - - -data DeclarationError - = CandidateOutsideDeclaration !FactSlot - | CandidateAlreadyAuthorized !FactSlot - | CandidateOutsideAuthorizationFrontier - !FactSlot !Natural !Natural - | DeclarationHasUnauthorizedCandidates - | DeclarationAuthorizationFrontierIncomplete - | CandidatePropositionNotClosed - | CandidatePropositionNotProposition !CoreType - | StagedPremiseNotEarlier - !FactSlot !Natural !FactSlot !Natural - | StagedPremiseNotAuthorized !FactSlot - | AuthorizedFactNotVisible - !SemanticFactOccurrenceFingerprint - | BuilderFactAuthorizationMismatch - | PendingFactAuthorizationMismatch - | PlanningFactContractMismatch !FactSlot - | CheckedAuthorizationCandidateShapeMismatch !Int !Int - | CheckedProofCandidateCountMismatch !Int - | LocalClaimOutsideCandidate - | FactSafetyFailed !FactSafetyError - | ValidationCertificateFailed !ValidationCertificateError - | DerivationImportFailed !DerivationImportError - | KernelCompletionFailed !KernelReplayError - | KernelConstructionDescriptorMismatch - | DefinitionEquationObjectMissing !ObjectId - | DefinitionEquationObjectNotTransparent !ObjectId - | DefinitionEquationObjectNotPointwisePredicate !ObjectId - | DefinitionEquationCandidateMismatch - | DatatypeCompilationDescriptorMismatch - | ProofObligationFailedAt !Location !DeclarationError - | VampireProcessFailed !Provers.ProverProcessError - | VampireObligationRejected !Provers.ProverAnswer - | VampireProofHasNoAcceptedObligations - | VampireCandidateBatchMismatch ![FactSlot] ![FactSlot] - | VampireCandidateBatchProofShapeMismatch !FactSlot - | VampireResolverBatchSizeMismatch !Int !Int - | OmittedProofDidNotRecordUse - | VampireRequestMismatch - | VampireTargetMismatch - | VampireLocalPremisesNotSupported - | VampireGlobalTypeMismatch !ObjectId - | VampirePremiseMismatch - !SemanticFactOccurrenceFingerprint - | VampirePremiseCapabilityMismatch - !SemanticFactOccurrenceFingerprint - | VampireFoundationMismatch !FoundationAxiomTag - | CurrentCandidateVampirePreparationFailed - !(VampireObligationPreparationError Void) - | ProofValidationOutsideProofDeclaration - | DeclarationValidationOutsideCompiledDeclaration - | DeclarationValidationAlreadySelected - | DeclarationValidationNotSelected - | DeclarationShapeChangedAfterValidationLookup - | CachedDeclarationCandidateMissing !FactSlot - | ImportedModuleNotDirect !SemanticInterfaceId - | ImportedFactMaterializationFailed - !Materialization.MaterializationError - | ImportedFactCollision - !SemanticFactOccurrenceFingerprint - | ImportedAliasCollision - !SemanticName !ImportedAliasOrigin !ImportedAliasOrigin - | ImportedAliasTargetMissing - !SemanticFactOccurrenceFingerprint - | ImportedGlobalCollision - !SemanticGlobalKey !SemanticGlobalTarget !SemanticGlobalTarget - | ImportedGlobalTargetInvalid - !SemanticGlobalKey - !SemanticGlobalTarget - !SemanticGlobalTargetError - | ImportedStructureCollision - !SemanticStructurePhrase - !SemanticStructureDescriptor - !SemanticStructureDescriptor - | SemanticStructureParentMissing - !SemanticStructurePhrase !SemanticStructurePhrase - | SemanticStructureOperationConflict - !StructSymbol !SemanticStructurePhrase !SemanticStructurePhrase - | SemanticStructurePredicateTargetInvalid - !SemanticStructurePhrase !ObjectId !(Maybe CoreType) !CoreType - | SemanticStructureOperationTargetInvalid - !SemanticStructurePhrase !StructSymbol !ObjectId !(Maybe CoreType) !CoreType - | ImportedEvidenceDirectMismatch - ![SemanticInterfaceId] ![SemanticInterfaceId] - | ImportedEvidenceInterfaceFailed !SemanticInterfaceError - | ImportedEvidenceObjectMissing !ObjectId - | ImportedEvidencePropositionMissing !PropositionId - | ImportedModuleAfterAuthorization - | DeclarationObjectAddedAfterAuthorization - | DeclarationObjectValidationFailed !ObjectValidationError - | DeclarationPropositionValidationFailed - !PropositionValidationError - | DeclarationInterfaceFailed !DeclarationInterfaceError - | DeclarationEnvironmentFailed !SemanticEnvironmentError - | DeclarationGlobalAlreadyStaged !SemanticGlobalKey - | DeclarationStructureAlreadyStaged !SemanticStructurePhrase - | DeclarationGlobalTargetInvalid - !SemanticGlobalKey - !SemanticGlobalTarget - !SemanticGlobalTargetError - | ProofDeclarationMustProduceOneFact - | BuilderFactCollision - !SemanticFactOccurrenceFingerprint - | BuilderAliasCollision !SemanticName - | BuilderObjectCollision !ObjectId - | BuilderGlobalCollision !SemanticGlobalKey !SemanticGlobalTarget - | BuilderStructureCollision !SemanticStructurePhrase - deriving stock (Show, Eq) - -declarationErrorLocation :: DeclarationError -> Maybe Location -declarationErrorLocation = \case - ProofObligationFailedAt location _failure -> - Just location - _failure -> - Nothing - -renderDeclarationError :: DeclarationError -> Text -renderDeclarationError = \case - CandidateOutsideDeclaration slot -> - "candidate " <> shown slot <> " does not belong to this declaration" - CandidateAlreadyAuthorized slot -> - "candidate " <> shown slot <> " was authorized more than once" - CandidateOutsideAuthorizationFrontier slot expected actual -> - "candidate " <> shown slot <> " is outside authorization frontier " - <> shown expected <> " (found " <> shown actual <> ")" - DeclarationHasUnauthorizedCandidates -> - "the declaration has unauthorized candidates" - DeclarationAuthorizationFrontierIncomplete -> - "the declaration authorization frontier is incomplete" - CandidatePropositionNotClosed -> - "the candidate proposition still has open local binders" - CandidatePropositionNotProposition actual -> - "the candidate has type " <> shown actual <> " instead of Prop" - StagedPremiseNotEarlier candidate candidateOrdinal premise premiseOrdinal -> - "candidate " <> shown candidate <> " at stage " <> shown candidateOrdinal - <> " depends on non-earlier premise " <> shown premise - <> " at stage " <> shown premiseOrdinal - StagedPremiseNotAuthorized slot -> - "staged premise " <> shown slot <> " is not authorized" - AuthorizedFactNotVisible fingerprint -> - "authorized fact " <> shown fingerprint <> " is not visible" - BuilderFactAuthorizationMismatch -> - "builder fact authority does not match the checked declaration" - PendingFactAuthorizationMismatch -> - "pending fact authority does not match the checked declaration" - PlanningFactContractMismatch slot -> - "checked declaration-stage fact " <> shown slot - <> " has inconsistent semantic provenance" - CheckedAuthorizationCandidateShapeMismatch expected actual -> - "checked declaration recipe expected " <> shown expected - <> " candidate stages but received " <> shown actual - CheckedProofCandidateCountMismatch actual -> - "checked proof declaration requires exactly one candidate but received " - <> shown actual - LocalClaimOutsideCandidate -> - "proof-local claim was used outside a candidate proof" - FactSafetyFailed{} -> - "fact-safety validation failed" - ValidationCertificateFailed{} -> - "validation-certificate checking failed" - DerivationImportFailed{} -> - "kernel derivation import failed" - KernelCompletionFailed{} -> - "kernel replay failed" - KernelConstructionDescriptorMismatch -> - "kernel construction does not match its checked descriptor" - DefinitionEquationObjectMissing identity -> - "definition equation references missing object " <> shown identity - DefinitionEquationObjectNotTransparent identity -> - "definition equation references non-transparent object " <> shown identity - DefinitionEquationObjectNotPointwisePredicate identity -> - "definition equation object " <> shown identity - <> " is not a unary predicate definition" - DefinitionEquationCandidateMismatch -> - "definition equation does not match its checked object content" - DatatypeCompilationDescriptorMismatch -> - "datatype compilation does not match its complete checked family" - ProofObligationFailedAt location failure -> - locationToText location <> ": " <> renderDeclarationError failure - VampireProcessFailed{} -> - "Vampire process failed while authorizing the declaration" - VampireObligationRejected{} -> - "Vampire did not accept a declaration obligation" - VampireProofHasNoAcceptedObligations -> - "Vampire proof contains no accepted obligations" - VampireCandidateBatchMismatch expected actual -> - "Vampire candidate batch does not match the complete authorization " - <> "stage (expected " <> shown expected - <> ", found " <> shown actual <> ")" - VampireCandidateBatchProofShapeMismatch slot -> - "Vampire candidate " <> shown slot - <> " performed execution before its ready batch" - VampireResolverBatchSizeMismatch expected actual -> - "Vampire resolver returned " <> shown actual - <> " results for " <> shown expected <> " requests" - OmittedProofDidNotRecordUse -> - "omitted proof completion did not record an omission" - VampireRequestMismatch -> - "accepted Vampire run does not match the prepared request" - VampireTargetMismatch -> - "Vampire request target does not match the candidate theorem" - VampireLocalPremisesNotSupported -> - "typed Vampire requests do not yet support local premises" - VampireGlobalTypeMismatch object -> - "Vampire request has the wrong type for global object " <> shown object - VampirePremiseMismatch fingerprint -> - "Vampire request premise does not match visible fact " <> shown fingerprint - VampirePremiseCapabilityMismatch fingerprint -> - "Vampire request lacks authority for premise " <> shown fingerprint - VampireFoundationMismatch tag -> - "Vampire request has inconsistent foundation axiom " <> shown tag - CurrentCandidateVampirePreparationFailed failure -> - "the staged Vampire obligation could not be prepared: " <> shown failure - ProofValidationOutsideProofDeclaration -> - "proof validation requires a proof declaration" - DeclarationValidationOutsideCompiledDeclaration -> - "declaration validation requires a compiled declaration" - DeclarationValidationAlreadySelected -> - "compiled declaration validation was selected more than once" - DeclarationValidationNotSelected -> - "compiled declaration validation was not selected" - DeclarationShapeChangedAfterValidationLookup -> - "compiled declaration shape changed after validation lookup" - CachedDeclarationCandidateMissing slot -> - "cached declaration validation has no candidate for " <> shown slot - ImportedModuleNotDirect interface -> - "sealed semantic interface is not a direct import: " <> shown interface - ImportedFactMaterializationFailed{} -> - "imported fact failed materialization checks" - ImportedFactCollision fingerprint -> - "imported fact " <> shown fingerprint <> " is already registered" - ImportedAliasCollision alias earlier later -> - "imported semantic alias " <> shown alias - <> " conflicts between " <> shown earlier - <> " and " <> shown later - ImportedAliasTargetMissing fingerprint -> - "imported alias targets missing fact " <> shown fingerprint - ImportedGlobalCollision key earlier later -> - "imported global " <> shown key - <> " has conflicting targets " <> shown earlier - <> " and " <> shown later - ImportedGlobalTargetInvalid key target _failure -> - "imported global " <> shown key - <> " has invalid target " <> shown target - ImportedEvidenceDirectMismatch expected actual -> - "imported semantic parents differ: expected " <> shown expected - <> ", found " <> shown actual - ImportedStructureCollision structurePhrase _existing _incoming -> - "structure " <> shown structurePhrase <> " has conflicting descriptors" - SemanticStructureParentMissing structurePhrase parent -> - "structure " <> shown structurePhrase <> " has unknown parent " <> shown parent - SemanticStructureOperationConflict symbol firstOrigin secondOrigin -> - "structure operation " <> shown symbol <> " conflicts between " - <> shown firstOrigin <> " and " <> shown secondOrigin - SemanticStructurePredicateTargetInvalid structurePhrase object _actual expected -> - "structure " <> shown structurePhrase <> " has invalid predicate object " - <> shown object <> " (expected " <> shown expected <> ")" - SemanticStructureOperationTargetInvalid structurePhrase symbol object _actual expected -> - "structure " <> shown structurePhrase <> " has invalid operation " - <> shown symbol <> " object " <> shown object - <> " (expected " <> shown expected <> ")" - ImportedEvidenceInterfaceFailed{} -> - "imported semantic interface failed validation" - ImportedEvidenceObjectMissing identity -> - "imported semantic interface is missing object " <> shown identity - ImportedEvidencePropositionMissing identity -> - "imported semantic interface is missing proposition " <> shown identity - ImportedModuleAfterAuthorization -> - "a sealed module was imported after candidate authorization" - DeclarationObjectAddedAfterAuthorization -> - "the declaration added an object after candidate authorization" - DeclarationObjectValidationFailed{} -> - "declaration object validation failed" - DeclarationPropositionValidationFailed{} -> - "declaration proposition validation failed" - DeclarationInterfaceFailed{} -> - "declaration interface validation failed" - DeclarationEnvironmentFailed{} -> - "declaration environment delta is inconsistent" - DeclarationGlobalAlreadyStaged key -> - "global " <> shown key <> " was staged more than once" - DeclarationStructureAlreadyStaged structurePhrase -> - "structure " <> shown structurePhrase <> " was staged more than once" - DeclarationGlobalTargetInvalid key target _failure -> - "global " <> shown key <> " has invalid target " <> shown target - ProofDeclarationMustProduceOneFact -> - "a proof declaration must produce exactly one fact" - BuilderFactCollision fingerprint -> - "fact " <> shown fingerprint <> " is already registered" - BuilderAliasCollision alias -> - "semantic alias " <> shown alias <> " is already registered" - BuilderObjectCollision object -> - "object " <> shown object <> " is already registered" - BuilderGlobalCollision key object -> - "global " <> shown key <> " is already bound to " <> shown object - BuilderStructureCollision structurePhrase -> - "structure " <> shown structurePhrase <> " is already registered" - where - shown :: Show value => value -> Text - shown = Text.pack . show |