summaryrefslogtreecommitdiff
path: root/source/Felix/Checking/Declaration.hs
diff options
context:
space:
mode:
authoradelon <22380201+adelon@users.noreply.github.com>2026-08-06 17:54:00 +0200
committeradelon <22380201+adelon@users.noreply.github.com>2026-08-06 17:54:00 +0200
commit82328890108bae64b372b8d58620ebc62699de76 (patch)
tree575404c6b425c19259c0ded296f1c8ffb7ff0e2b /source/Felix/Checking/Declaration.hs
parent1a25421c2a168d420581358c8733fcd8f36f379b (diff)
Migrate to `Felix` namespaceHEADhotg
Diffstat (limited to 'source/Felix/Checking/Declaration.hs')
-rw-r--r--source/Felix/Checking/Declaration.hs6770
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
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 20:17:39 +0000