{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE RankNTypes #-} -- | Builder-confined authorization and atomic typed declaration append. module Felix.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 , currentFoundationLowering , currentFoundationAxiomLowering , resolveVisibleFactAliasLowering , resolveVisibleFactTargetsLowering , resolveVisibleGlobalLowering , resolveVisibleGlobalContentLowering , resolveVisibleStructureLowering , resolveVisibleStructureOperationObjectsLowering , objectAvailableLowering , objectTypeLowering , runModuleDriver , ValidationLookup , validationLookup , ValidationRun(..) , failModuleDriver , failDeclarationDriver , VampireResolver , VampireSubmission(..) , vampireBatchResolver , vampireResolver , vampireSubmissionResolver , Declaration , failDeclaration , addDeclarationObject , addDeclarationProposition , resolveVisibleGlobal , stageSemanticGlobalBinding , stageSemanticStructureDescriptor , CandidateSpec , candidateSpec , CandidatePlanningSpec , CheckedCandidate , checkedCandidate , checkedDefinitionEquationPlanning , checkedSourceAxiomPlanning , checkedDatatypePlanning , checkedKernelPlanning , checkedKernelPlanningWithStaged , checkedStagedKernelPlanning , checkedSourceProofPlanning , checkedOmittedPlanning , CheckedPlannedVampireRequest , checkedPlannedVampireRequest , plannedEarlierCandidate , CheckedDeclaration , checkedProofDeclaration , checkedCompiledDeclaration , admitCheckedDeclaration , PlannedDeclaration , planCheckedDeclaration , admitPlannedCheckedDeclaration , plannedDeclarationPreviousPrefix , plannedDeclarationNextPrefix , plannedDeclarationDelta , PlanningIntegrityError(..) , prepareCandidateSpecDriver , prepareFrozenCandidateSpecDriver , prepareDefinitionEquationSpecDriver , preparePointwiseDefinitionEquationSpecDriver , prepareStagedCandidateVampireDriver , prepareCandidateSpecLowering , prepareFrozenCandidateSpecLowering , prepareDefinitionEquationSpecLowering , prepareDefinitionEquationSpecWithEligibilityLowering , prepareNamedSetConstructionSpecLowering , prepareRelationalSetConstructionSpecLowering , 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 , authorizeNamedSetConstructionCandidate , authorizeRelationalSetConstructionCandidate , 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 Felix.Cache.Codec (encodeCache) import Felix.Checking.Authority import Felix.Checking.Backend.Problem qualified as Backend import Felix.Checking.Backend.Tptp qualified as Tptp import Felix.Checking.Core import Felix.Checking.Foundation import Felix.Checking.Identity import Felix.Checking.Kernel.Derivation import Felix.Checking.Materialization qualified as Materialization import Felix.Checking.Semantic import Felix.Checking.SetConstruction import Felix.Module import Felix.Provers qualified as Provers import Felix.Report.Location import Felix.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 VampireSubmission -> IO (NonEmpty Provers.VampireHandle)) data VampireResolver = VampireResolver !VampireResolverMode data VampireSubmission = VampireSubmission !Location !Provers.PreparedVerificationRequest vampireBatchResolver :: (forall local origin. NonEmpty (Provers.PreparedTypedProverTask SemanticFactOccurrenceFingerprint local origin ObjectId) -> IO (NonEmpty (Either Provers.ProverProcessError Provers.ProverAnswer))) -> VampireResolver vampireBatchResolver resolve = VampireResolver (SynchronousVampireResolution resolve) -- | Production submission-only resolver. Retained-plan admission consumes -- the submitted handles through its private synchronous replay resolver. vampireSubmissionResolver :: (NonEmpty VampireSubmission -> IO (NonEmpty Provers.VampireHandle)) -> VampireResolver vampireSubmissionResolver submit = VampireResolver (AsynchronousVampireSubmission submit) 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) tasks = case mode of SynchronousVampireResolution resolve -> resolve tasks AsynchronousVampireSubmission{} -> throwIO (PlanningIntegrityError "asynchronous Vampire resolver reached synchronous admission") 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 currentFoundationLowering :: LoweringDriver CheckedFoundation currentFoundationLowering = withLoweringBuilder logicalBuilderFoundation 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 [] [] checkedKernelPlanningWithStaged :: KernelConstructionDescriptor -> [SemanticFactOccurrenceFingerprint] -> [PlannedCandidatePosition] -> CandidatePlanningSpec checkedKernelPlanningWithStaged descriptor facts staged = CandidatePlanningSpec (PlanningKernelConstruction descriptor) facts staged [] checkedStagedKernelPlanning :: KernelConstructionDescriptor -> [PlannedCandidatePosition] -> CandidatePlanningSpec checkedStagedKernelPlanning descriptor staged = CandidatePlanningSpec (PlanningKernelConstruction descriptor) [] staged [] 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 = prepareDefinitionEquationSpecWithEligibilityLowering objects identity SearchEligible alias prepareDefinitionEquationSpecWithEligibilityLowering :: [AssertedObject] -> ObjectId -> FactSearchEligibility -> SemanticName -> LoweringDriver (Either DeclarationError CandidateSpec) prepareDefinitionEquationSpecWithEligibilityLowering objects identity eligibility alias = prepareCandidateSpecWithLoweringClosure objects (\closure -> prepareDefinitionEquationSpecWithEligibility closure identity eligibility alias) -- | Prepare the unaliased first-order view of one checked, named set -- construction. The returned descriptor binds direct authorization to the -- transparent object and the complete checked source decomposition. prepareNamedSetConstructionSpecLowering :: [AssertedObject] -> ObjectId -> NamedSetConstruction ObjectId -> LoweringDriver (Either DeclarationError (CandidateSpec, KernelConstructionDescriptor)) prepareNamedSetConstructionSpecLowering objects identity construction = withLoweringBuilder \builder -> do closure <- first DeclarationObjectValidationFailed (extendObjectClosure (logicalBuilderObjectClosure builder) objects) (proposition, descriptor) <- prepareNamedSetConstruction (logicalBuilderFoundation builder) closure identity construction spec <- prepareFrozenCandidateSpec closure proposition SearchEligible [] pure (spec, descriptor) prepareRelationalSetConstructionSpecLowering :: [AssertedObject] -> ObjectId -> CheckedRelationalSetConstruction ObjectId -> FrozenCheckedCore ObjectId -> LoweringDriver (Either DeclarationError (CandidateSpec, KernelConstructionDescriptor)) prepareRelationalSetConstructionSpecLowering objects identity construction functionality = withLoweringBuilder \builder -> do closure <- first DeclarationObjectValidationFailed (extendObjectClosure (logicalBuilderObjectClosure builder) objects) (proposition, descriptor) <- prepareRelationalSetConstruction (logicalBuilderFoundation builder) closure identity construction functionality spec <- prepareFrozenCandidateSpec closure proposition SearchEligible [] pure (spec, descriptor) 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 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 builder location objects premiseSpec targetSpec) prepareStagedCandidateVampireWith :: BuilderState evidence -> Location -> [AssertedObject] -> CandidateSpec -> CandidateSpec -> IO (Either DeclarationError (PreparedVampireObligation Void ())) prepareStagedCandidateVampireWith 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 <- forceVampirePreparation (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 value) -> LoweringDriver (Either DeclarationError value) 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 prepareDefinitionEquationSpecWithEligibility closure identity SearchEligible alias prepareDefinitionEquationSpecWithEligibility :: CheckedObjectClosure -> ObjectId -> FactSearchEligibility -> SemanticName -> Either DeclarationError CandidateSpec prepareDefinitionEquationSpecWithEligibility closure identity eligibility 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 eligibility [alias]) prepareNamedSetConstruction :: CheckedFoundation -> CheckedObjectClosure -> ObjectId -> NamedSetConstruction ObjectId -> Either DeclarationError (FrozenCheckedCore ObjectId, KernelConstructionDescriptor) prepareNamedSetConstruction foundation closure identity construction = do let expectedContent = namedSetConstructionClosedBody construction case lookupCheckedObjectContent identity closure of Just (TransparentObjectContent _theory coreType body) | coreType == frozenCoreType expectedContent , body == frozenCoreTerm expectedContent -> pure () _ -> Left KernelConstructionDescriptorMismatch derived <- maybe (Left KernelConstructionDescriptorMismatch) Right (namedSetConstructionObjectFact (checkedFoundationSetConstruction foundation) identity construction) pure ( namedSetConstructionFactProposition derived , CheckedSetConstructionExtensionality identity (namedSetConstructionFactDescriptor derived) ) prepareRelationalSetConstruction :: CheckedFoundation -> CheckedObjectClosure -> ObjectId -> CheckedRelationalSetConstruction ObjectId -> FrozenCheckedCore ObjectId -> Either DeclarationError (FrozenCheckedCore ObjectId, KernelConstructionDescriptor) prepareRelationalSetConstruction foundation closure identity construction functionality = do let expectedContent = relationalSetConstructionClosedBody construction case lookupCheckedObjectContent identity closure of Just (TransparentObjectContent _theory coreType body) | coreType == frozenCoreType expectedContent , body == frozenCoreTerm expectedContent -> pure () _ -> Left KernelConstructionDescriptorMismatch derived <- maybe (Left KernelConstructionDescriptorMismatch) Right (relationalSetConstructionObjectFact (checkedFoundationSetConstruction foundation) identity construction functionality) pure ( relationalSetConstructionFactProposition derived , CheckedSetConstructionExtensionality identity (relationalSetConstructionFactDescriptor derived) ) 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 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 builder taskMode claimSupport claim scopedLocals auxiliaryTags selection)) prepareScopedVampireObligationWith :: (Ord local) => BuilderState evidence -> Provers.VampireTaskMode -> Vector (local, CoreType) -> ScopedCheckedCore ObjectId -> [ScopedVampirePremise local origin] -> [FoundationAxiomTag] -> VampirePremiseSelection -> IO (Either (VampireObligationPreparationError local) (PreparedVampireObligation local origin)) prepareScopedVampireObligationWith builder taskMode claimSupport claim scopedLocals auxiliaryTags selection = forceVampirePreparation 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 localPremisePolicy = case selection of VampireImplicitPremises -> Backend.FirstOrderLocals VampireExplicitPremises{} | any (\fact -> case Backend.typedBackendFactCapability fact of Backend.FofProjectable{} -> False Backend.RequiresTh0{} -> True) selected -> Backend.CompleteLocals | otherwise -> Backend.FirstOrderLocals VampireLocalPremises -> Backend.CompleteLocals higherOrderPolicy = case selection of VampireImplicitPremises -> Backend.ImplicitConstructionJustification VampireExplicitPremises{} -> Backend.ExplicitHigherOrderJustification VampireLocalPremises -> Backend.ExplicitHigherOrderJustification propositionDependencies = foundationAxiomDependencies . Backend.supportedPropositionTerm requiredAuxiliaryTags = Set.toAscList ( Set.fromList auxiliaryTags <> propositionDependencies claim <> foldMap (propositionDependencies . Backend.typedBackendFactProposition) selected <> foldMap (propositionDependencies . Backend.typedLocalPremiseProposition) (Backend.selectTypedLocalPremises localPremisePolicy locals) ) auxiliaries = Backend.typedFoundationAuxiliaryInput (logicalBuilderFoundation builder) <$> requiredAuxiliaryTags problem <- first VampireObligationPlanningFailed (Backend.planTypedProblem globalType selected claim locals auxiliaries localPremisePolicy higherOrderPolicy) task <- first VampireObligationEncodingFailed (Provers.prepareTypedProverTask taskMode problem) pure (PreparedVampireObligation problem task) forceVampirePreparation :: Either (VampireObligationPreparationError local) (PreparedVampireObligation local origin) -> IO (Either (VampireObligationPreparationError local) (PreparedVampireObligation local origin)) forceVampirePreparation preparation = Exception.evaluate (forcePrepared preparation) 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 -- | Authorize only the extensional fact deterministically derived from the -- checked source construction and its committed transparent object. authorizeNamedSetConstructionCandidate :: ObjectId -> NamedSetConstruction ObjectId -> ReservedCandidate -> Declaration () authorizeNamedSetConstructionCandidate identity construction candidate = authorizeOneCandidate candidate \initial -> do let builder = candidateProofBuilder initial (expected, descriptor) <- Except.liftEither (prepareNamedSetConstruction (logicalBuilderFoundation builder) (candidateProofObjectClosure initial) identity construction) when (isNothing (candidateProofCachedValidation initial)) do unless (frozenCoreTerm expected == frozenCoreTerm (checkedPropositionTerm (candidateCheckedProposition candidate)) ) (Except.throwError KernelConstructionDescriptorMismatch) completeCandidateWithValidation candidate (CheckedKernelConstruction descriptor) (candidateProofSafety initial) initial -- | Authorize the relational extensional view only after consuming the exact -- strictly-earlier functionality candidate. The consumed candidate supplies -- both real authority safety and the proposition rechecked by the confined -- construction schema; a caller cannot substitute an arbitrary theorem. authorizeRelationalSetConstructionCandidate :: ObjectId -> CheckedRelationalSetConstruction ObjectId -> ReservedCandidate -> ReservedCandidate -> Declaration () authorizeRelationalSetConstructionCandidate identity construction functionality candidate = authorizeOneCandidate candidate \initial -> do (_used, final) <- State.runStateT (runCandidateProof (useStagedCandidate functionality)) initial let builder = candidateProofBuilder final functionalityTerm = checkedPropositionTerm (candidateCheckedProposition functionality) (expected, descriptor) <- Except.liftEither (prepareRelationalSetConstruction (logicalBuilderFoundation builder) (candidateProofObjectClosure final) identity construction functionalityTerm) when (isNothing (candidateProofCachedValidation final)) do unless (frozenCoreTerm expected == frozenCoreTerm (checkedPropositionTerm (candidateCheckedProposition candidate))) (Except.throwError KernelConstructionDescriptorMismatch) completeCandidateWithValidation candidate (CheckedKernelConstruction descriptor) (candidateProofSafety final) final 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) ] preparation = prepareClosedCandidateVampire builder closure target premises preparedResult <- State.lift (liftIO (forceVampirePreparation 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 CheckedSetConstructionExtensionality{} -> False 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 = [ VampireSubmission location request | stage <- candidates , (_candidate, plannedRequests) <- toList stage , CheckedPlannedVampireRequest location request _facts <- plannedRequests ] case resolver of VampireResolver SynchronousVampireResolution{} -> pure (fmap (fmap synchronousCandidate) candidates) VampireResolver (AsynchronousVampireSubmission submit) -> 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 (vampireBatchResolver resolve) 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