diff options
Diffstat (limited to 'source/Felix/Checking/Declaration.hs')
| -rw-r--r-- | source/Felix/Checking/Declaration.hs | 6770 |
1 files changed, 6770 insertions, 0 deletions
diff --git a/source/Felix/Checking/Declaration.hs b/source/Felix/Checking/Declaration.hs new file mode 100644 index 0000000..15050c7 --- /dev/null +++ b/source/Felix/Checking/Declaration.hs @@ -0,0 +1,6770 @@ +{-# 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 |