path: root/source/Checking/Declaration.hs

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE RankNTypes #-}

-- | Builder-confined authorization and atomic typed declaration append.
module Checking.Declaration
    ( ModuleDriver
    , DriverFailure(..)
    , DriverResult(..)
    , ImportedModuleEvidence
    , ImportedAliasOrigin(..)
    , freshImportedModuleEvidence
    , validateImportedModuleEvidence
    , importSealedModule
    , importSealedModuleDriver
    , nextDeclarationSlotDriver
    , currentTheoryDriver
    , currentFoundationAxiomDriver
    , resolveVisibleFactAliasDriver
    , resolveVisibleFactTargetsDriver
    , resolveVisibleGlobalDriver
    , resolveVisibleGlobalContentDriver
    , ResolvedStructure
    , resolvedStructureDescriptor
    , resolvedStructurePredicate
    , resolvedStructureOperation
    , resolvedStructureOperations
    , resolveVisibleStructureDriver
    , resolveVisibleStructureOperationObjectsDriver
    , objectAvailableDriver
    , objectTypeDriver
    , LoweringDriver
    , runProspectiveLoweringDriver
    , nextDeclarationSlotLowering
    , currentTheoryLowering
    , currentFoundationAxiomLowering
    , resolveVisibleFactAliasLowering
    , resolveVisibleFactTargetsLowering
    , resolveVisibleGlobalLowering
    , resolveVisibleGlobalContentLowering
    , resolveVisibleStructureLowering
    , resolveVisibleStructureOperationObjectsLowering
    , objectAvailableLowering
    , objectTypeLowering
    , runModuleDriver
    , ValidationLookup
    , validationLookup
    , ValidationRun(..)
    , failModuleDriver
    , failDeclarationDriver
    , VampireResolver
    , vampireBatchResolver
    , vampireBatchResolverWithPreparationObserver
    , vampireResolver
    , vampireSubmissionResolver
    , Declaration
    , failDeclaration
    , addDeclarationObject
    , addDeclarationProposition
    , resolveVisibleGlobal
    , stageSemanticGlobalBinding
    , stageSemanticStructureDescriptor
    , CandidateSpec
    , candidateSpec
    , CandidatePlanningSpec
    , CheckedCandidate
    , checkedCandidate
    , checkedDefinitionEquationPlanning
    , checkedSourceAxiomPlanning
    , checkedDatatypePlanning
    , checkedKernelPlanning
    , checkedSourceProofPlanning
    , checkedOmittedPlanning
    , CheckedPlannedVampireRequest
    , checkedPlannedVampireRequest
    , plannedEarlierCandidate
    , CheckedDeclaration
    , checkedProofDeclaration
    , checkedCompiledDeclaration
    , admitCheckedDeclaration
    , PlannedDeclaration
    , planCheckedDeclaration
    , admitPlannedCheckedDeclaration
    , plannedDeclarationPreviousPrefix
    , plannedDeclarationNextPrefix
    , plannedDeclarationDelta
    , PlanningIntegrityError(..)
    , prepareCandidateSpecDriver
    , prepareFrozenCandidateSpecDriver
    , prepareDefinitionEquationSpecDriver
    , preparePointwiseDefinitionEquationSpecDriver
    , prepareStagedCandidateVampireDriver
    , prepareCandidateSpecLowering
    , prepareFrozenCandidateSpecLowering
    , prepareDefinitionEquationSpecLowering
    , preparePointwiseDefinitionEquationSpecLowering
    , prepareStagedCandidateVampireLowering
    , ReservedCandidate
    , reserveCandidate
    , reserveCandidateBatch
    , reservePropositionCandidate
    , reserveFrozenPropositionCandidateBatch
    , reserveDefinitionEquationCandidate
    , reservePointwiseDefinitionEquationCandidate
    , reserveDefinitionEquationCandidateBatch
    , reservedCandidateSlot
    , reservedCandidateStage
    , CandidateProof
    , locateProofObligation
    , recordOmittedUse
    , VampirePremiseSelection(..)
    , VampireObligationPreparationError(..)
    , ScopedVampirePremise
    , scopedVampirePremise
    , PreparedVampireObligation
    , prepareScopedVampireObligationDriver
    , prepareScopedContradictionObligationDriver
    , prepareScopedVampireObligationLowering
    , prepareScopedContradictionObligationLowering
    , useAuthorizedFact
    , useStagedCandidate
    , LocalClaim
    , proveLocalKernelClaim
    , useLocalClaim
    , authorizeKernelProofCandidate
    , authorizeKernelConstructionCandidate
    , authorizeDefinitionEquationCandidate
    , acceptVampireObligation
    , acceptPreparedVampireObligation
    , acceptCurrentCandidateVampire
    , prepareCurrentCandidateVampire
    , authorizeVampireCandidate
    , authorizeVampireCandidateBatch
    , authorizeSourceAxiomCandidate
    , authorizeOmittedCandidate
    , authorizeDatatypeCompilationCandidates
    , authorizeCompiledDeclaration
    , commitProofDeclaration
    , commitCompiledDeclaration
    , CommittedDeclarationBatch
    , committedBatchOwner
    , committedBatchSlot
    , committedBatchPreviousPrefix
    , committedBatchNextPrefix
    , committedBatchDelta
    , committedBatchObjects
    , committedBatchPropositions
    , committedBatchProofValidations
    , committedBatchDeclarationValidation
    , PendingModulePrefix
    , emptyPendingModulePrefix
    , pendingModulePrefixBatches
    , pendingModulePrefixCurrent
    , ValidationIntegrityError(..)
    , renderValidationIntegrityError
    , DeclarationError(..)
    , declarationErrorLocation
    , renderDeclarationError
    , DriverOpenError(..)
    , renderDriverOpenError
    ) where

import Base
import Checking.Authority
import Checking.Backend.Problem qualified as Backend
import Checking.Backend.Tptp qualified as Tptp
import Checking.Core
import Checking.Foundation
import Checking.Identity
import Checking.Kernel.Derivation
import Checking.Semantic
import Checking.Materialization qualified as Materialization
import Felix.Cache.Codec (encodeCache)
import Felix.Module
import Provers qualified
import Report.Location
import Syntax.Abstract (StructSymbol)

import Control.Exception qualified as Exception
import Control.DeepSeq (deepseq)
import Control.Monad.Except (ExceptT)
import Control.Monad.Except qualified as Except
import Control.Monad (foldM, unless, when)
import Control.Monad.State.Strict (StateT)
import Control.Monad.State.Strict qualified as State
import Data.Bifunctor (first)
import Data.ByteString qualified as ByteString
import Data.List qualified as List
import Data.List.NonEmpty qualified as NonEmpty
import Data.Map.Strict qualified as Map
import Data.Maybe (catMaybes, mapMaybe)
import Data.Set qualified as Set
import Data.Text qualified as Text
import Data.Unique (Unique, newUnique)
import Data.IORef (IORef, atomicModifyIORef', newIORef, readIORef)
import Data.Vector (Vector)
import Data.Vector qualified as Vector
import Numeric.Natural (Natural)


newtype BuilderIdentity = BuilderIdentity Unique
    deriving stock (Eq)

newtype DeclarationInvocation = DeclarationInvocation Natural
    deriving stock (Eq)

newtype CandidateStage = CandidateStage Natural
    deriving stock (Show, Eq, Ord)

data ValidationLookup = ValidationLookup
    !(ProofValidationKey -> IO (Maybe ProofValidationRecord))
    !(DeclarationValidationKey
        -> IO (Maybe DeclarationValidationRecord))

validationLookup
    :: (ProofValidationKey -> IO (Maybe ProofValidationRecord))
    -> (DeclarationValidationKey
        -> IO (Maybe DeclarationValidationRecord))
    -> ValidationLookup
validationLookup =
    ValidationLookup

data ValidationRun
    = FreshValidation
    | WarmValidation !ValidationLookup

data ValidationIntegrityError
    = CachedValidationIntegrityError
        !Materialization.MaterializationError
    deriving stock (Show, Eq)

instance Exception.Exception ValidationIntegrityError

renderValidationIntegrityError :: ValidationIntegrityError -> Text
renderValidationIntegrityError = \case
    CachedValidationIntegrityError failure ->
        "cached validation does not match its exact contextual input: "
            <> Text.pack (show failure)


data BuilderFactAuthorization = BuilderFactAuthorization
    !BuilderIdentity
    !FactSlot
    !FactAuthority

data PendingFactAuthorization = PendingFactAuthorization
    !BuilderIdentity
    !PrefixContextId
    !DeclarationInvocation
    !FactSlot
    !FactAuthority
    !CandidateStage

-- | Checked fact semantics paired with caller-selected evidence.  Semantic
-- lookup and request preparation deliberately ignore the evidence parameter;
-- only the admitted builder instantiation may consume capabilities.
data FactEntry evidence = FactEntry
    !CheckedPropositionContent
    !SemanticFactOccurrence
    !evidence

-- | The shared checked semantic state.  The evidence parameter makes the
-- distinction between admitted authority and future inert planning data
-- visible without duplicating lookup, collision, closure, or delta logic.
data BuilderState evidence = BuilderState
    { logicalBuilderIdentity :: !BuilderIdentity
    , logicalBuilderFoundation :: !CheckedFoundation
    , logicalBuilderTheory :: !TheoryId
    , logicalBuilderOwner :: !ModuleName
    , logicalBuilderDirectSemanticInputs :: ![SemanticInterfaceId]
    , logicalBuilderPrefix :: !PrefixContextId
    , logicalBuilderObjectClosure :: !CheckedObjectClosure
    , logicalBuilderFacts
        :: !(Map
            SemanticFactOccurrenceFingerprint
            (FactEntry evidence))
    , logicalBuilderAliases
        :: !(Map SemanticName ImportedAliasBinding)
    , logicalBuilderGlobals
        :: !(Map SemanticGlobalKey SemanticGlobalTarget)
    , logicalBuilderStructures
        :: !(Map SemanticStructurePhrase ResolvedStructure)
    , logicalBuilderImportedInterfaces :: !(Set SemanticInterfaceId)
    , logicalBuilderDeltas :: ![DeclarationInterfaceDelta]
    , logicalBuilderNextDeclaration :: !Natural
    , logicalBuilderNextFact :: !Natural
    , logicalBuilderNextInvocation :: !Natural
    }

-- | The only production builder in this milestone.  Capability-consuming
-- operations below accept this admitted instantiation, never a polymorphic
-- 'BuilderState'.
type LogicalBuilder = BuilderState BuilderFactAuthorization

-- | Public semantic contract and strict declaration-stage provenance for a
-- prospective fact.  It deliberately contains no builder identity, prefix,
-- declaration invocation, pending authorization, or minting capability.
data PlanningProvenance = PlanningProvenance
    !DeclarationSlot
    !CandidateStage
    !FactSlot
    deriving stock (Eq)

data PlanningEvidence = PlanningEvidence
    !FactAuthority
    !(Maybe PlanningProvenance)

data ResolvedStructureOperation = ResolvedStructureOperation
    !ObjectId
    !SemanticStructurePhrase
    deriving stock (Show, Eq)

data ResolvedStructure = ResolvedStructure
    !SemanticStructureDescriptor
    !(Set SemanticStructurePhrase)
    !(Map StructSymbol ResolvedStructureOperation)
    deriving stock (Show, Eq)

resolvedStructureDescriptor
    :: ResolvedStructure
    -> SemanticStructureDescriptor
resolvedStructureDescriptor (ResolvedStructure descriptor _ _) =
    descriptor

resolvedStructurePredicate :: ResolvedStructure -> Maybe ObjectId
resolvedStructurePredicate =
    semanticStructureDescriptorPredicate . resolvedStructureDescriptor

resolvedStructureOperation
    :: StructSymbol
    -> ResolvedStructure
    -> Maybe ObjectId
resolvedStructureOperation symbol (ResolvedStructure _ _ operations) =
    operationObject <$> Map.lookup symbol operations
  where
    operationObject (ResolvedStructureOperation object _origin) = object

resolvedStructureOperations
    :: ResolvedStructure
    -> Map StructSymbol ObjectId
resolvedStructureOperations (ResolvedStructure _ _ operations) =
    operationObject <$> operations
  where
    operationObject (ResolvedStructureOperation object _origin) = object

structureOperationBindings
    :: Map SemanticStructurePhrase ResolvedStructure
    -> Set (StructSymbol, ObjectId)
structureOperationBindings structures =
    Set.fromList
        [ (symbol, object)
        | structure <- Map.elems structures
        , (symbol, object) <-
            Map.toAscList (resolvedStructureOperations structure)
        ]


data CommittedDeclarationBatch = CommittedDeclarationBatch
    !ModuleName
    !DeclarationSlot
    !PrefixContextId
    !PrefixContextId
    !DeclarationInterfaceDelta
    ![AssertedObject]
    ![CheckedPropositionContent]
    ![ProofValidationRecord]
    !(Maybe DeclarationValidationRecord)

committedBatchOwner :: CommittedDeclarationBatch -> ModuleName
committedBatchOwner
        (CommittedDeclarationBatch owner _ _ _ _ _ _ _ _) =
    owner

committedBatchSlot
    :: CommittedDeclarationBatch
    -> DeclarationSlot
committedBatchSlot
        (CommittedDeclarationBatch _ slot _ _ _ _ _ _ _) =
    slot

committedBatchPreviousPrefix
    :: CommittedDeclarationBatch
    -> PrefixContextId
committedBatchPreviousPrefix
        (CommittedDeclarationBatch _ _ previous _ _ _ _ _ _) =
    previous

committedBatchNextPrefix
    :: CommittedDeclarationBatch
    -> PrefixContextId
committedBatchNextPrefix
        (CommittedDeclarationBatch _ _ _ next _ _ _ _ _) =
    next

committedBatchDelta
    :: CommittedDeclarationBatch
    -> DeclarationInterfaceDelta
committedBatchDelta
        (CommittedDeclarationBatch _ _ _ _ delta _ _ _ _) =
    delta

committedBatchObjects
    :: CommittedDeclarationBatch
    -> [AssertedObject]
committedBatchObjects
        (CommittedDeclarationBatch _ _ _ _ _ objects _ _ _) =
    objects

committedBatchPropositions
    :: CommittedDeclarationBatch
    -> [CheckedPropositionContent]
committedBatchPropositions
        (CommittedDeclarationBatch _ _ _ _ _ _ propositions _ _) =
    propositions

committedBatchProofValidations
    :: CommittedDeclarationBatch
    -> [ProofValidationRecord]
committedBatchProofValidations
        (CommittedDeclarationBatch _ _ _ _ _ _ _ validations _) =
    validations

committedBatchDeclarationValidation
    :: CommittedDeclarationBatch
    -> Maybe DeclarationValidationRecord
committedBatchDeclarationValidation
        (CommittedDeclarationBatch _ _ _ _ _ _ _ _ validation) =
    validation


data PendingModulePrefix = PendingModulePrefix
    !PrefixContextId
    ![CommittedDeclarationBatch]

emptyPendingModulePrefix
    :: PrefixContextId
    -> PendingModulePrefix
emptyPendingModulePrefix prefix =
    PendingModulePrefix prefix []

instance Show PendingModulePrefix where
    show prefix =
        "PendingModulePrefix {pendingModulePrefixCurrent = "
            <> show (pendingModulePrefixCurrent prefix)
            <> ", pendingModulePrefixBatchCount = "
            <> show (length (pendingModulePrefixBatches prefix))
            <> "}"

pendingModulePrefixBatches
    :: PendingModulePrefix
    -> [CommittedDeclarationBatch]
pendingModulePrefixBatches
        (PendingModulePrefix _ batchesReversed) =
    reverse batchesReversed

pendingModulePrefixCurrent
    :: PendingModulePrefix
    -> PrefixContextId
pendingModulePrefixCurrent
        (PendingModulePrefix prefix _batches) =
    prefix

appendPendingBatch
    :: CommittedDeclarationBatch
    -> PendingModulePrefix
    -> PendingModulePrefix
appendPendingBatch batch (PendingModulePrefix _ batches) =
    forceCommittedBatch batch `seq`
        PendingModulePrefix
            (committedBatchNextPrefix batch)
            (batch : batches)

forceCommittedBatch :: CommittedDeclarationBatch -> ()
forceCommittedBatch
        (CommittedDeclarationBatch
            owner slot previous next delta objects propositions
            proofValidations declarationValidation) =
    owner `seq`
    slot `seq`
    previous `seq`
    next `seq`
    ByteString.length
        (encodeCache (putDeclarationInterfaceDeltaCache delta)) `seq`
    objects `deepseq`
    propositions `deepseq`
    forceProofValidations proofValidations `seq`
    forceDeclarationValidation declarationValidation
  where
    forceProofValidations =
        foldl'
            (\() record ->
                proofValidationRecordKey record `seq`
                ByteString.length
                    (encodeCache
                        (putValidationCertificateCache
                            (proofValidationRecordCertificate
                                record))) `seq` ())
            ()

    forceDeclarationValidation = \case
        Nothing -> ()
        Just record ->
            declarationValidationRecordKey record `seq`
            foldl'
                (\() certificate ->
                    ByteString.length
                        (encodeCache
                            (putValidationCertificateCache
                                certificate)) `seq` ())
                ()
                (declarationValidationRecordCertificates record)


data VampireResolverMode
    = SynchronousVampireResolution
        (forall local origin.
            NonEmpty
                (Provers.PreparedTypedProverTask
                    SemanticFactOccurrenceFingerprint
                    local
                    origin
                    ObjectId)
            -> IO
                (NonEmpty
                    (Either
                        Provers.ProverProcessError
                        Provers.ProverAnswer)))
    | AsynchronousVampireSubmission
        (NonEmpty Provers.PreparedVerificationRequest
            -> IO (NonEmpty Provers.VampireHandle))

data VampireResolver = VampireResolver
    !VampireResolverMode
    !(Word64 -> IO ())

vampireBatchResolver
    :: (forall local origin.
        NonEmpty
            (Provers.PreparedTypedProverTask
                SemanticFactOccurrenceFingerprint
                local
                origin
                ObjectId)
        -> IO
            (NonEmpty
                (Either
                    Provers.ProverProcessError
                    Provers.ProverAnswer)))
    -> VampireResolver
vampireBatchResolver resolve =
    vampireBatchResolverWithPreparationObserver resolve (const (pure ()))

vampireBatchResolverWithPreparationObserver
    :: (forall local origin.
        NonEmpty
            (Provers.PreparedTypedProverTask
                SemanticFactOccurrenceFingerprint
                local
                origin
                ObjectId)
        -> IO
            (NonEmpty
                (Either
                    Provers.ProverProcessError
                    Provers.ProverAnswer)))
    -> (Word64 -> IO ())
    -> VampireResolver
vampireBatchResolverWithPreparationObserver resolve observe =
    VampireResolver (SynchronousVampireResolution resolve) observe

-- | Production submission-only resolver.  Retained-plan admission consumes
-- the submitted handles through its private synchronous replay resolver.
vampireSubmissionResolver
    :: (NonEmpty Provers.PreparedVerificationRequest
        -> IO (NonEmpty Provers.VampireHandle))
    -> (Word64 -> IO ())
    -> VampireResolver
vampireSubmissionResolver submit observe =
    VampireResolver (AsynchronousVampireSubmission submit) observe

vampireResolver
    :: (forall local origin.
        Provers.PreparedTypedProverTask
            SemanticFactOccurrenceFingerprint
            local
            origin
            ObjectId
        -> IO
            (Either
                Provers.ProverProcessError
                Provers.ProverAnswer))
    -> VampireResolver
vampireResolver resolve =
    vampireBatchResolver (traverse resolve)

resolveOneVampire
    :: VampireResolver
    -> Provers.PreparedTypedProverTask
        SemanticFactOccurrenceFingerprint
        local
        origin
        ObjectId
    -> ExceptT DeclarationError IO
        (Either
            Provers.ProverProcessError
            Provers.ProverAnswer)
resolveOneVampire resolver prepared = do
    results@(result :| _) <-
        liftIO (resolveSynchronousVampireBatch resolver (prepared :| []))
    void
        (Except.liftEither
            (validateVampireResolverResultCount 1 results))
    pure result

resolveSynchronousVampireBatch
    :: VampireResolver
    -> NonEmpty
        (Provers.PreparedTypedProverTask
            SemanticFactOccurrenceFingerprint
            local
            origin
            ObjectId)
    -> IO
        (NonEmpty
            (Either
                Provers.ProverProcessError
                Provers.ProverAnswer))
resolveSynchronousVampireBatch
        (VampireResolver mode _observe) tasks =
    case mode of
        SynchronousVampireResolution resolve -> resolve tasks
        AsynchronousVampireSubmission{} ->
            throwIO
                (PlanningIntegrityError
                    "asynchronous Vampire resolver reached synchronous admission")

observeVampirePreparation
    :: VampireResolver
    -> Word64
    -> IO ()
observeVampirePreparation (VampireResolver _mode observe) = observe

validateVampireResolverResultCount
    :: Int
    -> NonEmpty value
    -> Either DeclarationError [value]
validateVampireResolverResultCount expected results
    | expected == actual =
        Right (NonEmpty.toList results)
    | otherwise =
        Left (VampireResolverBatchSizeMismatch expected actual)
  where
    actual = NonEmpty.length results

data DriverState = DriverState
    !VampireResolver
    !LogicalBuilder
    !PendingModulePrefix
    !ValidationRun

-- | Authority-free semantic state used while lowering checked declarations.
-- Existing admitted facts are projected to their public contracts; no
-- builder-local authorization capability crosses this boundary.
newtype ProspectiveBuilder = ProspectiveBuilder
    (BuilderState PlanningEvidence)

data LoweringState = LoweringState
    !VampireResolver
    !ProspectiveBuilder
    !ValidationRun

newtype LoweringDriver value = LoweringDriver
    { runLoweringStep :: StateT LoweringState IO value
    }
    deriving newtype (Functor, Applicative, Monad)

newtype ModuleDriver failure value = ModuleDriver
    { runDriverStep
        :: ExceptT
            (DriverFailure failure)
            (StateT DriverState IO)
            value
    }
    deriving newtype (Functor, Applicative, Monad)

-- | Run one complete authority-free planning action from the current admitted
-- input projection.  The prospective state advances throughout the action but
-- never mutates the authoritative module builder.
runProspectiveLoweringDriver
    :: LoweringDriver value
    -> ModuleDriver failure value
runProspectiveLoweringDriver action = ModuleDriver do
    DriverState resolver builder _prefix validation <- State.get
    State.lift
        (liftIO
            (State.evalStateT
                (runLoweringStep action)
                (LoweringState resolver
                    (projectLogicalBuilder builder)
                    validation)))

projectLogicalBuilder :: LogicalBuilder -> ProspectiveBuilder
projectLogicalBuilder builder =
    ProspectiveBuilder
        builder
            { logicalBuilderFacts =
                fmap projectFact (logicalBuilderFacts builder)
            }
  where
    projectFact (FactEntry proposition occurrence _authorization) =
        FactEntry proposition occurrence
            (PlanningEvidence
                (semanticFactAuthority occurrence)
                Nothing)

data DriverFailure failure
    = DriverDeclarationFailed !DeclarationError
    | DriverActionFailed !failure
    deriving stock (Show, Eq)

data DriverResult failure value
    = DriverSucceeded
        !value
        !SemanticInterface
        !PendingModulePrefix
        !CheckedObjectClosure
    | DriverFailed
        !(DriverFailure failure)
        !PendingModulePrefix
    | DriverSealFailed
        !SemanticInterfaceError
        !PendingModulePrefix

data ImportedAliasOrigin = ImportedAliasOrigin
    !DeclarationSlot
    !SemanticFactOccurrenceFingerprint
    deriving stock (Show, Eq)

data ImportedAliasBinding = ImportedAliasBinding
    !SemanticFactOccurrenceFingerprint
    !ImportedAliasOrigin

-- | Opaque evidence produced from a successfully sealed producer.  Direct
-- parents retain the semantic DAG; importing folds it deterministically and
-- mints fresh authority for the consuming builder.
data ImportedModuleEvidence = ImportedModuleEvidence
    !SemanticInterface
    ![ImportedModuleEvidence]
    !(Map
        SemanticFactOccurrenceFingerprint
        (SemanticFactOccurrence, CheckedPropositionContent))
    ![AssertedObject]

freshImportedModuleEvidence
    :: [ImportedModuleEvidence]
    -> SemanticInterface
    -> PendingModulePrefix
    -> ImportedModuleEvidence
freshImportedModuleEvidence parents interface prefix =
    ImportedModuleEvidence
        interface
        parents
        (Map.fromList
            [ ( semanticFactFingerprint occurrence
              , (occurrence, requireProposition occurrence)
              )
            | occurrence <- occurrences
            ])
        objects
  where
    batches = pendingModulePrefixBatches prefix
    objects = concatMap committedBatchObjects batches
    propositions = concatMap committedBatchPropositions batches
    propositionMap =
        Map.fromList
            [ (checkedPropositionId proposition, proposition)
            | proposition <- propositions
            ]
    occurrences =
        concatMap
            declarationDeltaFacts
            (semanticInterfaceDeclarations interface)

    requireProposition occurrence =
        case Map.lookup
                (semanticFactProposition occurrence)
                propositionMap of
            Just proposition ->
                proposition
            Nothing ->
                impossible
                    ("sealed fact occurrence references absent proposition "
                        <> show (semanticFactProposition occurrence))

-- | Construct import evidence after a trusted producer or validated store
-- installation has supplied the complete canonical proposition payloads.
validateImportedModuleEvidence
    :: TheoryId
    -> [ImportedModuleEvidence]
    -> SemanticInterface
    -> [AssertedObject]
    -> [CheckedPropositionContent]
    -> Either DeclarationError ImportedModuleEvidence
validateImportedModuleEvidence
        theory parents interface objects propositions = do
    _ <- first ImportedEvidenceInterfaceFailed
        (validateSemanticInterface
            (semanticInterfaceOwner interface)
            (semanticInterfaceDirectInputs interface)
            (semanticInterfaceDeclarations interface)
            (semanticInterfaceAssertedId interface))
    unless
        (semanticInterfaceDirectInputs interface == parentIds)
        (Left
            (ImportedEvidenceDirectMismatch
                (semanticInterfaceDirectInputs interface)
                parentIds))
    let propositionMap =
            Map.fromList
                [ (checkedPropositionId proposition, proposition)
                | proposition <- propositions
                ]
        objectMap =
            Map.fromList
                [ (assertedObjectId object, object)
                | object <- objects
                ]
        localObjectIds =
            concatMap
                declarationDeltaObjects
                (semanticInterfaceDeclarations interface)
        parentObjectMap =
            foldl'
                (Map.unionWith const)
                Map.empty
                (evidenceObjectMap <$> parents)
    localObjects <- traverse
        (\identity ->
            maybe
                (Left (ImportedEvidenceObjectMissing identity))
                Right
                (Map.lookup identity objectMap))
        localObjectIds
    closure <- first DeclarationObjectValidationFailed
        (validateObjectClosure
            theory
            (Map.elems parentObjectMap <> localObjects))
    let occurrences =
            concatMap
                declarationDeltaFacts
                (semanticInterfaceDeclarations interface)
    pairs <- traverse
        (\occurrence -> do
            proposition <- maybe
                (Left
                    (ImportedEvidencePropositionMissing
                        (semanticFactProposition occurrence)))
                Right
                (Map.lookup
                    (semanticFactProposition occurrence)
                    propositionMap)
            _ <- first DeclarationPropositionValidationFailed
                (validateAssertedPropositionContent
                    closure
                    (checkedPropositionId proposition)
                    (frozenCoreTerm
                        (checkedPropositionTerm proposition)))
            _ <- first ImportedFactMaterializationFailed
                (Materialization.checkImportedOccurrence
                    theory
                    (semanticFactFingerprint occurrence)
                    occurrence
                    proposition
                    (semanticFactAuthority occurrence))
            pure
                ( semanticFactFingerprint occurrence
                , (occurrence, proposition)
                ))
        occurrences
    let evidence =
            ImportedModuleEvidence
                interface
                parents
                (Map.fromList pairs)
                localObjects
    _ <- validateEvidenceInventory theory closure evidence
    pure evidence
  where
    parentIds =
        semanticInterfaceAssertedId . evidenceInterface <$> parents

validateEvidenceInventory
    :: TheoryId
    -> CheckedObjectClosure
    -> ImportedModuleEvidence
    -> Either DeclarationError ()
validateEvidenceInventory theory closure evidence =
    do
        void (foldEvidence Set.empty Map.empty Map.empty evidence)
        (_seen, structures) <-
            foldStructures Set.empty Map.empty evidence
        void (foldGlobals structures Set.empty Map.empty evidence)
  where
    foldEvidence seen facts aliases current
        | identity `Set.member` seen =
            Right (seen, facts, aliases)
        | otherwise = do
            unless
                (semanticInterfaceDirectInputs interface == parentIds)
                (Left
                    (ImportedEvidenceDirectMismatch
                        (semanticInterfaceDirectInputs interface)
                        parentIds))
            (parentsSeen, parentFacts, parentAliases) <-
                foldM
                    (\(seen', facts', aliases') parent ->
                        foldEvidence seen' facts' aliases' parent)
                    (seen, facts, aliases)
                    parents
            localFacts <- foldM insertFact parentFacts (Map.elems entries)
            localAliases <- foldM
                (insertAlias localFacts)
                parentAliases
                [ ( alias
                  , ImportedAliasOrigin
                        (declarationDeltaSlot delta)
                        (semanticAliasTarget alias)
                  )
                | delta <- semanticInterfaceDeclarations interface
                , alias <- declarationDeltaAliases delta
                ]
            pure
                ( Set.insert identity parentsSeen
                , localFacts
                , localAliases
                )
      where
        ImportedModuleEvidence interface parents entries _objects = current
        identity = semanticInterfaceAssertedId interface
        parentIds =
            semanticInterfaceAssertedId . evidenceInterface <$> parents

    insertFact facts pair@(occurrence, proposition) = do
        let fingerprint = semanticFactFingerprint occurrence
        _ <- first ImportedFactMaterializationFailed
            (Materialization.checkImportedOccurrence
                theory
                fingerprint
                occurrence
                proposition
                (semanticFactAuthority occurrence))
        case Map.lookup fingerprint facts of
            Nothing ->
                Right (Map.insert fingerprint pair facts)
            Just (existingOccurrence, existingProposition)
                | existingOccurrence == occurrence
                  && checkedPropositionId existingProposition
                    == checkedPropositionId proposition ->
                    Right facts
                | otherwise ->
                    Left (ImportedFactCollision fingerprint)

    insertAlias facts aliases (alias, origin) = do
        let name = semanticAliasName alias
            target = semanticAliasTarget alias
        unless
            (Map.member target facts)
            (Left (ImportedAliasTargetMissing target))
        case Map.lookup name aliases of
            Nothing ->
                Right
                    (Map.insert
                        name
                        (ImportedAliasBinding target origin)
                        aliases)
            Just (ImportedAliasBinding existingTarget existingOrigin)
                | existingTarget == target ->
                    Right aliases
                | otherwise ->
                    Left
                        (ImportedAliasCollision
                            name existingOrigin origin)

    foldGlobals structures seen globals current
        | identity `Set.member` seen =
            Right (seen, globals)
        | otherwise = do
            (parentsSeen, parentGlobals) <-
                foldM
                    (\(seen', globals') parent ->
                        foldGlobals structures seen' globals' parent)
                    (seen, globals)
                    parents
            globals' <-
                foldM
                    (insertGlobal
                        (structureOperationBindings structures))
                    parentGlobals
                    [ binding
                    | delta <- semanticInterfaceDeclarations interface
                    , binding <- semanticEnvironmentBindings
                        (declarationDeltaEnvironment delta)
                    ]
            pure (Set.insert identity parentsSeen, globals')
      where
        ImportedModuleEvidence interface parents _entries _objects = current
        identity = semanticInterfaceAssertedId interface

    insertGlobal operationBindings globals binding = do
        let key = semanticGlobalBindingKey binding
            target = semanticGlobalBindingTarget binding
        _ <-
            first
                (ImportedGlobalTargetInvalid key target)
                (validateSemanticGlobalBindingTarget
                    operationBindings
                    closure binding)
        case Map.lookup key globals of
            Nothing -> Right (Map.insert key target globals)
            Just existing
                | existing == target -> Right globals
                | otherwise ->
                    Left (ImportedGlobalCollision key existing target)

    foldStructures seen structures current
        | identity `Set.member` seen =
            Right (seen, structures)
        | otherwise = do
            (parentsSeen, parentStructures) <-
                foldM
                    (\(seen', structures') parent ->
                        foldStructures seen' structures' parent)
                    (seen, structures)
                    parents
            structures' <-
                foldM
                    (insertSemanticStructure closure)
                    parentStructures
                    [ descriptor
                    | delta <- semanticInterfaceDeclarations interface
                    , descriptor <- semanticEnvironmentStructures
                        (declarationDeltaEnvironment delta)
                    ]
            pure (Set.insert identity parentsSeen, structures')
      where
        ImportedModuleEvidence interface parents _entries _objects = current
        identity = semanticInterfaceAssertedId interface

evidenceInterface :: ImportedModuleEvidence -> SemanticInterface
evidenceInterface
        (ImportedModuleEvidence interface _parents _entries _objects) =
    interface

evidenceObjectMap
    :: ImportedModuleEvidence
    -> Map ObjectId AssertedObject
evidenceObjectMap
        (ImportedModuleEvidence _interface parents _entries objects) =
    foldl'
        (Map.unionWith const)
        (Map.fromList
            [ (assertedObjectId object, object)
            | object <- objects
            ])
        (evidenceObjectMap <$> parents)

data DriverOpenError
    = DriverInitialPrefixError !PrefixContextError
    | DriverInitialObjectError !ObjectValidationError
    deriving stock (Show, Eq)

renderDriverOpenError :: DriverOpenError -> Text
renderDriverOpenError = \case
    DriverInitialPrefixError{} ->
        "the initial semantic prefix is inconsistent"
    DriverInitialObjectError{} ->
        "the initial object closure is inconsistent"

runModuleDriver
    :: CheckedFoundation
    -> ModuleName
    -> [SemanticInterfaceId]
    -> VampireResolver
    -> ValidationRun
    -> ModuleDriver failure value
    -> IO
        (Either
            DriverOpenError
            (DriverResult failure value))
runModuleDriver
        foundation owner direct resolver validationRun action = do
    unique <- BuilderIdentity <$> newUnique
    let theory = theoryId foundation
    case (,) <$>
            first DriverInitialPrefixError
                (initialPrefixContextId theory owner direct)
            <*>
            first DriverInitialObjectError
                (validateObjectClosure theory []) of
        Left err ->
            pure (Left err)
        Right (prefix, closure) -> do
            let builder =
                    BuilderState
                        { logicalBuilderIdentity = unique
                        , logicalBuilderFoundation = foundation
                        , logicalBuilderTheory = theory
                        , logicalBuilderOwner = owner
                        , logicalBuilderDirectSemanticInputs = direct
                        , logicalBuilderPrefix = prefix
                        , logicalBuilderObjectClosure = closure
                        , logicalBuilderFacts = Map.empty
                        , logicalBuilderAliases = Map.empty
                        , logicalBuilderGlobals = Map.empty
                        , logicalBuilderStructures = Map.empty
                        , logicalBuilderImportedInterfaces = Set.empty
                        , logicalBuilderDeltas = []
                        , logicalBuilderNextDeclaration = 0
                        , logicalBuilderNextFact = 0
                        , logicalBuilderNextInvocation = 0
                        }
                initialState =
                    DriverState
                        resolver
                        builder
                        (PendingModulePrefix prefix [])
                        validationRun
            (result, DriverState _ finalBuilder finalPrefix _) <-
                State.runStateT
                    (Except.runExceptT
                        (runDriverStep action))
                    initialState
            case result of
                Left err ->
                    pure (Right (DriverFailed err finalPrefix))
                Right value -> do
                    case semanticInterface
                            owner
                            direct
                            (reverse
                                (logicalBuilderDeltas
                                    finalBuilder)) of
                        Left err ->
                            pure
                                (Right
                                    (DriverSealFailed
                                        err
                                        finalPrefix))
                        Right interface ->
                            pure
                                (Right
                                    (DriverSucceeded
                                        value
                                        interface
                                        finalPrefix
                                        (logicalBuilderObjectClosure
                                            finalBuilder)))

failModuleDriver :: failure -> ModuleDriver failure value
failModuleDriver err =
    ModuleDriver
        (Except.throwError
            (DriverActionFailed err))

failDeclarationDriver :: DeclarationError -> ModuleDriver failure value
failDeclarationDriver err =
    ModuleDriver (Except.throwError (DriverDeclarationFailed err))

nextDeclarationSlotDriver
    :: ModuleDriver failure DeclarationSlot
nextDeclarationSlotDriver = ModuleDriver do
    DriverState _resolver builder _prefix _validation <- State.get
    pure
        (declarationSlot
            (logicalBuilderOwner builder)
            (localDeclarationOrdinal
                (logicalBuilderNextDeclaration builder)))

currentTheoryDriver :: ModuleDriver failure TheoryId
currentTheoryDriver =
    ModuleDriver
        (State.gets
            (\(DriverState _resolver builder _prefix _validation) ->
                logicalBuilderTheory builder))

currentFoundationAxiomDriver
    :: FoundationAxiomTag
    -> ModuleDriver failure (FrozenCheckedCore Void)
currentFoundationAxiomDriver tag =
    ModuleDriver
        (State.gets
            (\(DriverState _resolver builder _prefix _validation) ->
                foundationAxiomFrozen
                    (logicalBuilderFoundation builder)
                    tag))

resolveVisibleFactAliasDriver
    :: SemanticName
    -> ModuleDriver failure
        (Maybe SemanticFactOccurrenceFingerprint)
resolveVisibleFactAliasDriver alias = ModuleDriver do
    DriverState _resolver builder _prefix _validation <- State.get
    pure do
        ImportedAliasBinding fingerprint _origin <-
            Map.lookup alias (logicalBuilderAliases builder)
        pure fingerprint

resolveVisibleFactTargetsDriver
    :: FrozenCheckedCore ObjectId
    -> ModuleDriver failure
        [SemanticFactOccurrenceFingerprint]
resolveVisibleFactTargetsDriver target = ModuleDriver do
    DriverState _resolver builder _prefix _validation <- State.get
    pure
        [ fingerprint
        | (fingerprint, FactEntry proposition _occurrence _authorization) <-
            Map.toAscList (logicalBuilderFacts builder)
        , checkedPropositionTerm proposition == target
        ]

resolveVisibleGlobalDriver
    :: SemanticGlobalKey
    -> ModuleDriver failure (Maybe (SemanticGlobalTarget, CoreType))
resolveVisibleGlobalDriver key = ModuleDriver do
    DriverState _resolver builder _prefix _validation <- State.get
    pure
        ( (\(target, _content, _dependencies) ->
                ( target
                , fromMaybe
                    (impossible "visible semantic key has no source type")
                    (semanticGlobalKeyType key)
                ))
            <$> resolveVisibleGlobalContent builder key
        )

resolveVisibleGlobalContentDriver
    :: SemanticGlobalKey
    -> ModuleDriver failure
        (Maybe
            ( SemanticGlobalTarget
            , ObjectContent
            , Map ObjectId CoreType
            ))
resolveVisibleGlobalContentDriver key = ModuleDriver do
    DriverState _resolver builder _prefix _validation <- State.get
    pure (resolveVisibleGlobalContent builder key)

resolveVisibleStructureDriver
    :: SemanticStructurePhrase
    -> ModuleDriver failure (Maybe ResolvedStructure)
resolveVisibleStructureDriver structurePhrase = ModuleDriver do
    DriverState _resolver builder _prefix _validation <- State.get
    pure (Map.lookup structurePhrase (logicalBuilderStructures builder))

resolveVisibleStructureOperationObjectsDriver
    :: StructSymbol
    -> ModuleDriver failure [ObjectId]
resolveVisibleStructureOperationObjectsDriver symbol = ModuleDriver do
    DriverState _resolver builder _prefix _validation <- State.get
    pure
        ( Set.toAscList
            (Set.fromList
                (mapMaybe
                    (resolvedStructureOperation symbol)
                    (Map.elems (logicalBuilderStructures builder))))
        )

resolveVisibleGlobalContent
    :: BuilderState evidence
    -> SemanticGlobalKey
    -> Maybe
        ( SemanticGlobalTarget
        , ObjectContent
        , Map ObjectId CoreType
        )
resolveVisibleGlobalContent builder key = do
    target <- Map.lookup key (logicalBuilderGlobals builder)
    content <-
        lookupCheckedObjectContent
            (semanticGlobalTargetObject target)
            closure
    let dependencies =
            Map.fromList
                [ (identity, requireDependency identity)
                | identity <- case content of
                    TransparentObjectContent _theory _coreType body ->
                        Set.toAscList (canonicalTermGlobals body)
                    _ -> []
                ]
    pure
        ( target
        , content
        , dependencies
        )
  where
    closure = logicalBuilderObjectClosure builder

    requireDependency identity =
        case lookupCheckedObjectType identity closure of
            Just coreType -> coreType
            Nothing ->
                impossible "checked object dependency is absent"

objectAvailableDriver
    :: ObjectId
    -> ModuleDriver failure Bool
objectAvailableDriver identity =
    ModuleDriver
        (State.gets
            (\(DriverState _resolver builder _prefix _validation) ->
                isJust
                    (lookupCheckedObjectType
                        identity
                        (logicalBuilderObjectClosure builder))))

objectTypeDriver
    :: ObjectId
    -> ModuleDriver failure (Maybe CoreType)
objectTypeDriver identity =
    ModuleDriver
        (State.gets
            (\(DriverState _resolver builder _prefix _validation) ->
                lookupCheckedObjectType
                    identity
                    (logicalBuilderObjectClosure builder)))

nextDeclarationSlotLowering :: LoweringDriver DeclarationSlot
nextDeclarationSlotLowering =
    withLoweringBuilder \builder ->
        declarationSlot
            (logicalBuilderOwner builder)
            (localDeclarationOrdinal
                (logicalBuilderNextDeclaration builder))

currentTheoryLowering :: LoweringDriver TheoryId
currentTheoryLowering =
    withLoweringBuilder logicalBuilderTheory

currentFoundationAxiomLowering
    :: FoundationAxiomTag
    -> LoweringDriver (FrozenCheckedCore Void)
currentFoundationAxiomLowering tag =
    withLoweringBuilder
        (\builder ->
            foundationAxiomFrozen
                (logicalBuilderFoundation builder)
                tag)

resolveVisibleFactAliasLowering
    :: SemanticName
    -> LoweringDriver (Maybe SemanticFactOccurrenceFingerprint)
resolveVisibleFactAliasLowering alias =
    withLoweringBuilder \builder -> do
        ImportedAliasBinding fingerprint _origin <-
            Map.lookup alias (logicalBuilderAliases builder)
        pure fingerprint

resolveVisibleFactTargetsLowering
    :: FrozenCheckedCore ObjectId
    -> LoweringDriver [SemanticFactOccurrenceFingerprint]
resolveVisibleFactTargetsLowering target =
    withLoweringBuilder \builder ->
        [ fingerprint
        | (fingerprint, FactEntry proposition _occurrence _evidence) <-
            Map.toAscList (logicalBuilderFacts builder)
        , checkedPropositionTerm proposition == target
        ]

resolveVisibleGlobalLowering
    :: SemanticGlobalKey
    -> LoweringDriver (Maybe (SemanticGlobalTarget, CoreType))
resolveVisibleGlobalLowering key =
    withLoweringBuilder \builder ->
        ( (\(target, _content, _dependencies) ->
                ( target
                , fromMaybe
                    (impossible "visible semantic key has no source type")
                    (semanticGlobalKeyType key)
                ))
            <$> resolveVisibleGlobalContent builder key
        )

resolveVisibleGlobalContentLowering
    :: SemanticGlobalKey
    -> LoweringDriver
        (Maybe
            ( SemanticGlobalTarget
            , ObjectContent
            , Map ObjectId CoreType
            ))
resolveVisibleGlobalContentLowering key =
    withLoweringBuilder (\builder -> resolveVisibleGlobalContent builder key)

resolveVisibleStructureLowering
    :: SemanticStructurePhrase
    -> LoweringDriver (Maybe ResolvedStructure)
resolveVisibleStructureLowering phrase =
    withLoweringBuilder (Map.lookup phrase . logicalBuilderStructures)

resolveVisibleStructureOperationObjectsLowering
    :: StructSymbol
    -> LoweringDriver [ObjectId]
resolveVisibleStructureOperationObjectsLowering symbol =
    withLoweringBuilder \builder ->
        Set.toAscList
            (Set.fromList
                (mapMaybe
                    (resolvedStructureOperation symbol)
                    (Map.elems (logicalBuilderStructures builder))))

objectAvailableLowering :: ObjectId -> LoweringDriver Bool
objectAvailableLowering identity =
    withLoweringBuilder
        (isJust
            . lookupCheckedObjectType identity
            . logicalBuilderObjectClosure)

objectTypeLowering :: ObjectId -> LoweringDriver (Maybe CoreType)
objectTypeLowering identity =
    withLoweringBuilder
        (lookupCheckedObjectType identity
            . logicalBuilderObjectClosure)

withLoweringBuilder
    :: (BuilderState PlanningEvidence -> value)
    -> LoweringDriver value
withLoweringBuilder action = LoweringDriver do
    LoweringState _resolver (ProspectiveBuilder builder) _validation <- State.get
    pure (action builder)


data CandidateSpec = CandidateSpec
    !CheckedPropositionContent
    !FactSearchEligibility
    ![SemanticName]

candidateSpec
    :: CheckedPropositionContent
    -> FactSearchEligibility
    -> [SemanticName]
    -> CandidateSpec
candidateSpec =
    CandidateSpec

-- | One strictly earlier candidate in the same checked declaration.  The
-- position is structural and becomes a concrete fact slot only while the
-- declaration is planned.
data PlannedCandidatePosition = PlannedCandidatePosition
    !Natural
    !Natural
    deriving stock (Show, Eq, Ord)

data CandidatePlanningDirect
    = PlanningDefinitionEquation !ObjectId
    | PlanningSourceAxiom
    | PlanningTrustedDatatype !DatatypeCompilationDescriptor
    | PlanningKernelConstruction !KernelConstructionDescriptor
    | PlanningCheckedSourceProof
    | PlanningOmitted
    deriving stock (Show, Eq)

-- | Erased exact request data needed by scheduling and public-contract
-- planning.  The family body retains the typed obligation used by admission;
-- this projection carries only its one canonical request and exact global
-- premise fingerprints.
data CheckedPlannedVampireRequest = CheckedPlannedVampireRequest
    !Location
    !Provers.PreparedVerificationRequest
    ![SemanticFactOccurrenceFingerprint]

data CandidatePlanningSpec = CandidatePlanningSpec
    !CandidatePlanningDirect
    ![SemanticFactOccurrenceFingerprint]
    ![PlannedCandidatePosition]
    ![CheckedPlannedVampireRequest]

-- | One authority-free checked candidate and its exact planning contract.
-- The two parts are constructed together by the declaration-family lowerer
-- and retain no builder capability or publication path.
data CheckedCandidate = CheckedCandidate
    !CandidateSpec
    !CandidatePlanningSpec

checkedCandidate
    :: CandidateSpec
    -> CandidatePlanningSpec
    -> CheckedCandidate
checkedCandidate = CheckedCandidate

checkedDefinitionEquationPlanning :: ObjectId -> CandidatePlanningSpec
checkedDefinitionEquationPlanning identity =
    CandidatePlanningSpec
        (PlanningDefinitionEquation identity) [] [] []

checkedSourceAxiomPlanning :: CandidatePlanningSpec
checkedSourceAxiomPlanning =
    CandidatePlanningSpec PlanningSourceAxiom [] [] []

checkedDatatypePlanning
    :: DatatypeCompilationDescriptor
    -> CandidatePlanningSpec
checkedDatatypePlanning descriptor =
    CandidatePlanningSpec (PlanningTrustedDatatype descriptor) [] [] []

checkedKernelPlanning
    :: KernelConstructionDescriptor
    -> [SemanticFactOccurrenceFingerprint]
    -> CandidatePlanningSpec
checkedKernelPlanning descriptor facts =
    CandidatePlanningSpec
        (PlanningKernelConstruction descriptor)
        facts
        []
        []

checkedSourceProofPlanning
    :: [CheckedPlannedVampireRequest]
    -> [PlannedCandidatePosition]
    -> CandidatePlanningSpec
checkedSourceProofPlanning requests staged =
    CandidatePlanningSpec
        PlanningCheckedSourceProof [] staged requests

checkedOmittedPlanning
    :: [CheckedPlannedVampireRequest]
    -> [PlannedCandidatePosition]
    -> CandidatePlanningSpec
checkedOmittedPlanning requests staged =
    CandidatePlanningSpec PlanningOmitted [] staged requests

checkedPlannedVampireRequest
    :: Location
    -> PreparedVampireObligation local origin
    -> CheckedPlannedVampireRequest
checkedPlannedVampireRequest location
        (PreparedVampireObligation expected task) =
    CheckedPlannedVampireRequest
        location
        (Provers.preparedTypedProverRequest task)
        ( Backend.typedBackendFactReference
            <$> Vector.toList
                (Backend.typedProblemGlobalPremises expected)
        )

plannedEarlierCandidate
    :: Natural
    -> Natural
    -> PlannedCandidatePosition
plannedEarlierCandidate =
    PlannedCandidatePosition

data CheckedDeclarationMode
    = CheckedProofMode !ProofSyntaxId
    | CheckedCompiledMode !DeclarationSyntaxId

-- | One completely lowered, authority-free declaration transaction.  The
-- family body is a closed checked authorization recipe owned by its exact
-- lowerer; structural effects and stable source-ordered candidate stages are
-- common.  This value is invocation-local and never serialized.
data CheckedDeclaration body = CheckedDeclaration
    !CheckedDeclarationMode
    ![AssertedObject]
    ![CheckedPropositionContent]
    ![SemanticGlobalBinding]
    ![SemanticStructureDescriptor]
    ![NonEmpty CheckedCandidate]
    !body

checkedProofDeclaration
    :: ProofSyntaxId
    -> [AssertedObject]
    -> [CheckedPropositionContent]
    -> [SemanticGlobalBinding]
    -> [SemanticStructureDescriptor]
    -> [NonEmpty CheckedCandidate]
    -> body
    -> CheckedDeclaration body
checkedProofDeclaration
        syntax objects propositions globals structures stages =
    CheckedDeclaration
        (CheckedProofMode syntax) objects propositions globals structures
        stages

checkedCompiledDeclaration
    :: DeclarationSyntaxId
    -> [AssertedObject]
    -> [CheckedPropositionContent]
    -> [SemanticGlobalBinding]
    -> [SemanticStructureDescriptor]
    -> [NonEmpty CheckedCandidate]
    -> body
    -> CheckedDeclaration body
checkedCompiledDeclaration
        syntax objects propositions globals structures stages =
    CheckedDeclaration
        (CheckedCompiledMode syntax) objects propositions globals structures
        stages

prepareCandidateSpecDriver
    :: [AssertedObject]
    -> ScopedCheckedCore ObjectId
    -> FactSearchEligibility
    -> [SemanticName]
    -> ModuleDriver failure (Either DeclarationError CandidateSpec)
prepareCandidateSpecDriver objects scoped eligibility aliases =
    prepareCandidateSpecWithDriverClosure objects
        (\closure ->
            prepareScopedCandidateSpec
                closure scoped eligibility aliases)

prepareFrozenCandidateSpecDriver
    :: [AssertedObject]
    -> FrozenCheckedCore ObjectId
    -> FactSearchEligibility
    -> [SemanticName]
    -> ModuleDriver failure (Either DeclarationError CandidateSpec)
prepareFrozenCandidateSpecDriver objects frozen eligibility aliases =
    prepareCandidateSpecWithDriverClosure objects
        (\closure ->
            prepareFrozenCandidateSpec
                closure frozen eligibility aliases)

prepareDefinitionEquationSpecDriver
    :: [AssertedObject]
    -> ObjectId
    -> SemanticName
    -> ModuleDriver failure (Either DeclarationError CandidateSpec)
prepareDefinitionEquationSpecDriver objects identity alias =
    prepareCandidateSpecWithDriverClosure objects
        (\closure ->
            prepareDefinitionEquationSpec closure identity alias)

preparePointwiseDefinitionEquationSpecDriver
    :: [AssertedObject]
    -> ObjectId
    -> SemanticName
    -> ModuleDriver failure (Either DeclarationError CandidateSpec)
preparePointwiseDefinitionEquationSpecDriver objects identity alias =
    prepareCandidateSpecWithDriverClosure objects
        (\closure ->
            preparePointwiseDefinitionEquationSpec closure identity alias)

prepareCandidateSpecLowering
    :: [AssertedObject]
    -> ScopedCheckedCore ObjectId
    -> FactSearchEligibility
    -> [SemanticName]
    -> LoweringDriver (Either DeclarationError CandidateSpec)
prepareCandidateSpecLowering objects scoped eligibility aliases =
    prepareCandidateSpecWithLoweringClosure objects
        (\closure ->
            prepareScopedCandidateSpec
                closure scoped eligibility aliases)

prepareFrozenCandidateSpecLowering
    :: [AssertedObject]
    -> FrozenCheckedCore ObjectId
    -> FactSearchEligibility
    -> [SemanticName]
    -> LoweringDriver (Either DeclarationError CandidateSpec)
prepareFrozenCandidateSpecLowering objects frozen eligibility aliases =
    prepareCandidateSpecWithLoweringClosure objects
        (\closure ->
            prepareFrozenCandidateSpec
                closure frozen eligibility aliases)

prepareDefinitionEquationSpecLowering
    :: [AssertedObject]
    -> ObjectId
    -> SemanticName
    -> LoweringDriver (Either DeclarationError CandidateSpec)
prepareDefinitionEquationSpecLowering objects identity alias =
    prepareCandidateSpecWithLoweringClosure objects
        (\closure ->
            prepareDefinitionEquationSpec closure identity alias)

preparePointwiseDefinitionEquationSpecLowering
    :: [AssertedObject]
    -> ObjectId
    -> SemanticName
    -> LoweringDriver (Either DeclarationError CandidateSpec)
preparePointwiseDefinitionEquationSpecLowering objects identity alias =
    prepareCandidateSpecWithLoweringClosure objects
        (\closure ->
            preparePointwiseDefinitionEquationSpec closure identity alias)

-- | Prepare one closed Vampire obligation whose only premise is a
-- conditionally available fact from a strictly earlier candidate stage of
-- the same declaration.  The temporary checked stage contains public fact
-- semantics and structural provenance only; admission must still consume the
-- corresponding real reserved candidate before accepting this request.
prepareStagedCandidateVampireDriver
    :: Location
    -> [AssertedObject]
    -> CandidateSpec
    -> CandidateSpec
    -> ModuleDriver failure
        (Either
            DeclarationError
            (PreparedVampireObligation Void ()))
prepareStagedCandidateVampireDriver
        location objects premiseSpec targetSpec =
    ModuleDriver do
        DriverState resolver builder _prefix _validation <- State.get
        State.lift
            (liftIO
                (prepareStagedCandidateVampireWith
                    resolver builder location objects premiseSpec targetSpec))

prepareStagedCandidateVampireLowering
    :: Location
    -> [AssertedObject]
    -> CandidateSpec
    -> CandidateSpec
    -> LoweringDriver
        (Either
            DeclarationError
            (PreparedVampireObligation Void ()))
prepareStagedCandidateVampireLowering
        location objects premiseSpec targetSpec =
    LoweringDriver do
        LoweringState resolver (ProspectiveBuilder builder) _validation <-
            State.get
        liftIO
            (prepareStagedCandidateVampireWith
                resolver builder location objects premiseSpec targetSpec)

prepareStagedCandidateVampireWith
    :: VampireResolver
    -> BuilderState evidence
    -> Location
    -> [AssertedObject]
    -> CandidateSpec
    -> CandidateSpec
    -> IO
        (Either
            DeclarationError
            (PreparedVampireObligation Void ()))
prepareStagedCandidateVampireWith
        resolver builder location objects premiseSpec targetSpec = do
    let staged = do
            closure <-
                first DeclarationObjectValidationFailed
                    (extendObjectClosure
                        (logicalBuilderObjectClosure builder)
                        objects)
            premise <-
                prospectiveStagePremise
                    builder closure premiseSpec targetSpec
            pure (closure, premise)
    case staged of
        Left failure -> pure (Left failure)
        Right (closure, premise) -> do
            prepared <-
                measureVampirePreparation resolver
                    (prepareClosedCandidateVampire
                        builder closure
                        (candidateSpecProposition targetSpec)
                        [premise])
            pure
                (first
                    (ProofObligationFailedAt location
                        . CurrentCandidateVampirePreparationFailed)
                    prepared)

candidateSpecProposition :: CandidateSpec -> CheckedPropositionContent
candidateSpecProposition (CandidateSpec proposition _eligibility _aliases) =
    proposition

prospectiveStagePremise
    :: BuilderState evidence
    -> CheckedObjectClosure
    -> CandidateSpec
    -> CandidateSpec
    -> Either DeclarationError CheckedPropositionContent
prospectiveStagePremise builder closure premiseSpec targetSpec = do
    let owner = logicalBuilderOwner builder
        declaration =
            declarationSlot owner
                (localDeclarationOrdinal
                    (logicalBuilderNextDeclaration builder))
        premiseSlot =
            factSlot owner
                (localFactOrdinal (logicalBuilderNextFact builder))
        targetSlot =
            factSlot owner
                (localFactOrdinal (logicalBuilderNextFact builder + 1))
        premiseStage = CandidateStage 0
        targetStage = CandidateStage 1
        proposition = candidateSpecProposition premiseSpec
        authority =
            factAuthority
                (theoremRef
                    (logicalBuilderTheory builder)
                    (checkedPropositionId proposition))
                cleanAuthoritySafety
        CandidateSpec _ eligibility _aliases = premiseSpec
        occurrence =
            semanticFactOccurrence premiseSlot authority eligibility
        stage =
            CheckedDeclarationStage declaration closure
                (Map.singleton premiseSlot
                        (FactEntry proposition occurrence
                            (PlanningEvidence
                                authority
                                (Just
                                    (PlanningProvenance
                                        declaration premiseStage premiseSlot)))))
    unless
        (propositionMatchesClosure closure
            (candidateSpecProposition targetSpec))
        (Left (PlanningFactContractMismatch targetSlot))
    useProspectiveStageFact
        stage targetStage targetSlot premiseStage premiseSlot

useProspectiveStageFact
    :: CheckedDeclarationStage
    -> CandidateStage
    -> FactSlot
    -> CandidateStage
    -> FactSlot
    -> Either DeclarationError CheckedPropositionContent
useProspectiveStageFact
        (CheckedDeclarationStage ownSlot closure entries)
        currentStage currentSlot expectedStage premiseSlot = do
    FactEntry proposition occurrence
        (PlanningEvidence authority provenance) <-
            maybe
                (Left (PlanningFactContractMismatch premiseSlot))
                Right
                (Map.lookup premiseSlot entries)
    unless
        ( provenance
            == Just
                (PlanningProvenance
                    ownSlot expectedStage premiseSlot)
          && expectedStage < currentStage
          && semanticFactSlot occurrence == premiseSlot
          && semanticFactAuthority occurrence == authority
          && propositionMatchesClosure closure proposition
        )
        (Left (PlanningFactContractMismatch currentSlot))
    pure proposition

prepareCandidateSpecWithDriverClosure
    :: [AssertedObject]
    -> (CheckedObjectClosure -> Either DeclarationError CandidateSpec)
    -> ModuleDriver failure (Either DeclarationError CandidateSpec)
prepareCandidateSpecWithDriverClosure objects prepare = ModuleDriver do
    DriverState _resolver builder _prefix _validation <- State.get
    pure do
        closure <-
            first DeclarationObjectValidationFailed
                (extendObjectClosure
                    (logicalBuilderObjectClosure builder)
                    objects)
        prepare closure

prepareCandidateSpecWithLoweringClosure
    :: [AssertedObject]
    -> (CheckedObjectClosure -> Either DeclarationError CandidateSpec)
    -> LoweringDriver (Either DeclarationError CandidateSpec)
prepareCandidateSpecWithLoweringClosure objects prepare =
    withLoweringBuilder \builder -> do
        closure <-
            first DeclarationObjectValidationFailed
                (extendObjectClosure
                    (logicalBuilderObjectClosure builder)
                    objects)
        prepare closure

data ReservedCandidate = ReservedCandidate
    !BuilderIdentity
    !PrefixContextId
    !DeclarationInvocation
    !CandidateStage
    !FactSlot
    !CandidateSpec

reservedCandidateSlot :: ReservedCandidate -> FactSlot
reservedCandidateSlot
        (ReservedCandidate _ _ _ _ slot _) =
    slot

reservedCandidateStage :: ReservedCandidate -> Natural
reservedCandidateStage
        (ReservedCandidate _ _ _ (CandidateStage stage) _ _) =
    stage

candidateCheckedProposition
    :: ReservedCandidate
    -> CheckedPropositionContent
candidateCheckedProposition
        (ReservedCandidate _ _ _ _ _ (CandidateSpec proposition _ _)) =
    proposition

candidateTheoremReference
    :: BuilderState evidence
    -> ReservedCandidate
    -> TheoremRef
candidateTheoremReference builder candidate =
    theoremRef
        (logicalBuilderTheory builder)
        (checkedPropositionId
            (candidateCheckedProposition candidate))


data PendingCandidate = PendingCandidate
    !ReservedCandidate
    !ValidationCertificate
    !PendingFactAuthorization

data DeclarationValidationSelection
    = DeclarationValidationUnselected
    | FreshDeclarationValidation
    | CachedDeclarationValidation
        !DeclarationSyntaxId
        ![ObjectId]
        ![TheoremId]
        !DeclarationValidationRecord
        !(Map FactSlot Natural)

data DeclarationState = DeclarationState
    { declarationVampireResolver :: !VampireResolver
    , declarationValidationRun :: !ValidationRun
    , declarationValidationMode :: !ValidationMode
    , declarationValidationSelection
        :: !DeclarationValidationSelection
    , declarationBuilder :: !LogicalBuilder
    , declarationOwnSlot :: !DeclarationSlot
    , declarationInvocation :: !DeclarationInvocation
    , declarationObjectsReversed :: ![AssertedObject]
    , declarationObjectClosure :: !(Maybe CheckedObjectClosure)
    , declarationPropositionsReversed
        :: ![CheckedPropositionContent]
    , declarationGlobalBindingsReversed
        :: ![SemanticGlobalBinding]
    , declarationStructureDescriptorsReversed
        :: ![SemanticStructureDescriptor]
    , declarationReservations
        :: !(Map FactSlot ReservedCandidate)
    , declarationPending :: !(Map FactSlot PendingCandidate)
    , declarationNextFact :: !Natural
    , declarationNextStage :: !Natural
    , declarationAuthorizationFrontier :: !Natural
    }

-- | Authority-free view of checked declaration-local semantics.  This is the
-- narrow staging substrate for later lowerers: it carries the exact object
-- closure and conditional public fact contracts, but no builder identity,
-- prefix, invocation, pending authorization, admitted alias, or published
-- occurrence.
data CheckedDeclarationStage = CheckedDeclarationStage
    !DeclarationSlot
    !CheckedObjectClosure
    !(Map FactSlot (FactEntry PlanningEvidence))

newtype Declaration value = Declaration
    { runDeclaration
        :: StateT
            DeclarationState
            (ExceptT DeclarationError IO)
            value
    }
    deriving newtype (Functor, Applicative, Monad)

failDeclaration :: DeclarationError -> Declaration value
failDeclaration =
    Declaration . State.lift . Except.throwError

addDeclarationObject :: AssertedObject -> Declaration ()
addDeclarationObject asserted = Declaration do
    state <- State.get
    case declarationValidationSelection state of
        DeclarationValidationUnselected -> pure ()
        _ ->
            State.lift
                (Except.throwError
                    DeclarationShapeChangedAfterValidationLookup)
    when
        (isJust (declarationObjectClosure state))
        (State.lift
            (Except.throwError
                DeclarationObjectAddedAfterAuthorization))
    State.put
        state
            { declarationObjectsReversed =
                asserted : declarationObjectsReversed state
            }

addDeclarationProposition
    :: CheckedPropositionContent
    -> Declaration ()
addDeclarationProposition proposition =
    Declaration
        (State.modify' \state ->
            state
                { declarationPropositionsReversed =
                    proposition
                        : declarationPropositionsReversed state
                })

resolveVisibleGlobal
    :: SemanticGlobalKey
    -> Declaration (Maybe (SemanticGlobalTarget, CoreType))
resolveVisibleGlobal key = Declaration do
    state <- State.get
    let builder = declarationBuilder state
    pure do
        target <- Map.lookup key (logicalBuilderGlobals builder)
        coreType <- semanticGlobalKeyType key
        pure (target, coreType)

stageSemanticGlobalBinding
    :: SemanticGlobalKey
    -> SemanticGlobalTarget
    -> Declaration ()
stageSemanticGlobalBinding key target = Declaration do
    state <- State.get
    case declarationValidationSelection state of
        DeclarationValidationUnselected -> pure ()
        _ ->
            State.lift
                (Except.throwError
                    DeclarationShapeChangedAfterValidationLookup)
    when
        (any
            ((== key) . semanticGlobalBindingKey)
            (declarationGlobalBindingsReversed state))
        (State.lift
            (Except.throwError
                (DeclarationGlobalAlreadyStaged key)))
    State.put
        state
            { declarationGlobalBindingsReversed =
                semanticGlobalBinding key target
                    : declarationGlobalBindingsReversed state
            }

stageSemanticStructureDescriptor
    :: SemanticStructureDescriptor
    -> Declaration ()
stageSemanticStructureDescriptor descriptor = Declaration do
    state <- State.get
    case declarationValidationSelection state of
        DeclarationValidationUnselected -> pure ()
        _ ->
            State.lift
                (Except.throwError
                    DeclarationShapeChangedAfterValidationLookup)
    let structurePhrase = semanticStructureDescriptorPhrase descriptor
    when
        (any
            ((== structurePhrase) . semanticStructureDescriptorPhrase)
            (declarationStructureDescriptorsReversed state))
        (State.lift
            (Except.throwError
                (DeclarationStructureAlreadyStaged structurePhrase)))
    State.put
        state
            { declarationStructureDescriptorsReversed =
                descriptor
                    : declarationStructureDescriptorsReversed state
            }

prepareScopedCandidateSpec
    :: CheckedObjectClosure
    -> ScopedCheckedCore ObjectId
    -> FactSearchEligibility
    -> [SemanticName]
    -> Either DeclarationError CandidateSpec
prepareScopedCandidateSpec closure scoped eligibility aliases = do
    frozen <-
        maybe (Left CandidatePropositionNotClosed) Right
            (closeScopedCore scoped)
    prepareFrozenCandidateSpec closure frozen eligibility aliases

prepareFrozenCandidateSpec
    :: CheckedObjectClosure
    -> FrozenCheckedCore ObjectId
    -> FactSearchEligibility
    -> [SemanticName]
    -> Either DeclarationError CandidateSpec
prepareFrozenCandidateSpec closure frozen eligibility aliases = do
    unless
        (frozenCoreType frozen == TyProp)
        (Left
            (CandidatePropositionNotProposition
                (frozenCoreType frozen)))
    proposition <-
        first DeclarationPropositionValidationFailed
            (validatePropositionContent closure (frozenCoreTerm frozen))
    pure (candidateSpec proposition eligibility aliases)

prepareDefinitionEquationSpec
    :: CheckedObjectClosure
    -> ObjectId
    -> SemanticName
    -> Either DeclarationError CandidateSpec
prepareDefinitionEquationSpec closure identity alias = do
    content <-
        maybe
            (Left (DefinitionEquationObjectMissing identity))
            Right
            (lookupCheckedObjectContent identity closure)
    (coreType, body) <-
        case content of
            TransparentObjectContent _theory objectType objectBody ->
                Right (objectType, objectBody)
            _ ->
                Left (DefinitionEquationObjectNotTransparent identity)
    proposition <-
        first DeclarationPropositionValidationFailed
            (validatePropositionContent
                closure
                (CEq coreType (CGlobal identity) body))
    pure (candidateSpec proposition SearchEligible [alias])

preparePointwiseDefinitionEquationSpec
    :: CheckedObjectClosure
    -> ObjectId
    -> SemanticName
    -> Either DeclarationError CandidateSpec
preparePointwiseDefinitionEquationSpec closure identity alias = do
    content <-
        maybe
            (Left (DefinitionEquationObjectMissing identity))
            Right
            (lookupCheckedObjectContent identity closure)
    body <-
        case content of
            TransparentObjectContent _theory
                    (TyArrow TySet TyProp) (CLam TySet predicate) ->
                Right predicate
            _ ->
                Left
                    (DefinitionEquationObjectNotPointwisePredicate identity)
    proposition <-
        first DeclarationPropositionValidationFailed
            (validatePropositionContent
                closure
                (CForall TySet
                    (CEq TyProp
                        (CApp (CGlobal identity) (CBound 0))
                        body)))
    pure (candidateSpec proposition SearchEligible [alias])

reserveCandidate
    :: CandidateSpec
    -> Declaration ReservedCandidate
reserveCandidate spec =
    NonEmpty.head <$> reserveCandidateBatch (spec :| [])

-- | Validate and reserve one closed checked proposition in the current
-- declaration closure.
reservePropositionCandidate
    :: ScopedCheckedCore ObjectId
    -> FactSearchEligibility
    -> [SemanticName]
    -> Declaration ReservedCandidate
reservePropositionCandidate scoped eligibility aliases = Declaration do
    unprepared <- State.get
    prepared <-
        State.lift
            (Except.liftEither
                (prepareDeclarationClosure unprepared))
    spec <-
        State.lift
            (Except.liftEither
                (prepareScopedCandidateSpec
                    (fromMaybe
                        (impossible
                            "prepared proposition closure is absent")
                        (declarationObjectClosure prepared))
                    scoped eligibility aliases))
    State.put prepared
    runDeclaration (reserveCandidate spec)

-- | Validate and reserve one stage of already closed checked propositions in
-- the current declaration closure.
reserveFrozenPropositionCandidateBatch
    :: NonEmpty
        ( FrozenCheckedCore ObjectId
        , FactSearchEligibility
        , [SemanticName]
        )
    -> Declaration (NonEmpty ReservedCandidate)
reserveFrozenPropositionCandidateBatch inputs = Declaration do
    unprepared <- State.get
    prepared <-
        State.lift
            (Except.liftEither
                (prepareDeclarationClosure unprepared))
    let closure =
            maybe
                (impossible "prepared proposition closure is absent")
                id
                (declarationObjectClosure prepared)
    specs <- traverse (prepareInput closure) inputs
    State.put prepared
    runDeclaration (reserveCandidateBatch specs)
  where
    prepareInput closure (frozen, eligibility, aliases) =
        State.lift
            (Except.liftEither
                (prepareFrozenCandidateSpec
                    closure frozen eligibility aliases))

reserveCandidateBatch
    :: NonEmpty CandidateSpec
    -> Declaration (NonEmpty ReservedCandidate)
reserveCandidateBatch specs = Declaration do
    state <- State.get
    case declarationValidationSelection state of
        DeclarationValidationUnselected -> pure ()
        _ ->
            State.lift
                (Except.throwError
                    DeclarationShapeChangedAfterValidationLookup)
    let builder = declarationBuilder state
        stage = CandidateStage (declarationNextStage state)
        firstFact = declarationNextFact state
        candidates =
            NonEmpty.zipWith
                (makeReserved builder state stage)
                (0 :| [1 ..])
                specs
        reservations' =
            foldl'
                (\reservations candidate ->
                    Map.insert
                        (reservedCandidateSlot candidate)
                        candidate
                        reservations)
                (declarationReservations state)
                candidates
        candidateCount = fromIntegral (NonEmpty.length specs)
    State.put
        state
            { declarationReservations = reservations'
            , declarationNextFact = firstFact + candidateCount
            , declarationNextStage =
                declarationNextStage state + 1
            }
    pure candidates
  where
    makeReserved builder state stage offset spec =
        ReservedCandidate
            (logicalBuilderIdentity builder)
            (logicalBuilderPrefix builder)
            (declarationInvocation state)
            stage
            (factSlot
                (logicalBuilderOwner builder)
                (localFactOrdinal
                    (declarationNextFact state + offset)))
            spec

-- | Construct the one defining equation owned by a checked transparent
-- object. The equation is derived from authoritative object content, not from
-- a caller-supplied proposition.
reserveDefinitionEquationCandidate
    :: ObjectId
    -> SemanticName
    -> Declaration ReservedCandidate
reserveDefinitionEquationCandidate identity alias = Declaration do
    unprepared <- State.get
    prepared <-
        State.lift
            (Except.liftEither
                (prepareDeclarationClosure unprepared))
    spec <-
        State.lift
            (Except.liftEither
                (prepareDefinitionEquationSpec
                    (fromMaybe
                        (impossible
                            "prepared definition closure is absent")
                        (declarationObjectClosure prepared))
                    identity alias))
    State.put prepared
    runDeclaration (reserveCandidate spec)

-- | Construct the pointwise presentation of one unary transparent predicate
-- definition. The candidate remains tied to the object's checked content.
reservePointwiseDefinitionEquationCandidate
    :: ObjectId
    -> SemanticName
    -> Declaration ReservedCandidate
reservePointwiseDefinitionEquationCandidate identity alias = Declaration do
    unprepared <- State.get
    prepared <-
        State.lift
            (Except.liftEither
                (prepareDeclarationClosure unprepared))
    spec <-
        State.lift
            (Except.liftEither
                (preparePointwiseDefinitionEquationSpec
                    (fromMaybe
                        (impossible "prepared predicate closure is absent")
                        (declarationObjectClosure prepared))
                    identity alias))
    State.put prepared
    runDeclaration (reserveCandidate spec)

-- | Reserve one defining equation and a nonempty generated-fact batch at the
-- same declaration stage. No candidate in the batch can cite a sibling.
reserveDefinitionEquationCandidateBatch
    :: ObjectId
    -> SemanticName
    -> NonEmpty
        ( ScopedCheckedCore ObjectId
        , FactSearchEligibility
        , [SemanticName]
        )
    -> Declaration
        ( ReservedCandidate
        , NonEmpty ReservedCandidate
        )
reserveDefinitionEquationCandidateBatch identity alias generated =
    Declaration do
        unprepared <- State.get
        prepared <-
            State.lift
                (Except.liftEither
                    (prepareDeclarationClosure unprepared))
        let closure =
                maybe
                    (impossible
                        "prepared declaration closure is absent")
                    id
                    (declarationObjectClosure prepared)
        definition <-
            State.lift
                (Except.liftEither
                    (prepareDefinitionEquationSpec closure identity alias))
        generatedSpecs <-
            traverse
                (prepareGeneratedSpec closure)
                generated
        State.put prepared
        candidates <-
            runDeclaration
                (reserveCandidateBatch
                    (definition :| toList generatedSpecs))
        case candidates of
            definitionCandidate :| firstGenerated : remainingGenerated ->
                pure
                    ( definitionCandidate
                    , firstGenerated :| remainingGenerated
                    )
            _ ->
                impossible
                    "a nonempty generated batch produced no candidate"
  where
    prepareGeneratedSpec closure (scoped, eligibility, aliases) =
        State.lift
            (Except.liftEither
                (prepareScopedCandidateSpec
                    closure scoped eligibility aliases))

-- | Resolve one complete compiled declaration against its exact validation
-- key, then run the source-level authorization action under that selection.
-- Objects and candidates must already be prepared so the lookup key cannot
-- change after a hit or miss is chosen.
authorizeCompiledDeclaration
    :: Declaration value
    -> Declaration value
authorizeCompiledDeclaration action = Declaration do
    unprepared <- State.get
    (syntax, objects, theorems, ordinals, prepared) <-
        State.lift
            (Except.liftEither
                (prepareCompiledValidation unprepared))
    let key =
            declarationValidationKey
                syntax
                (logicalBuilderPrefix
                    (declarationBuilder prepared))
                objects
                theorems
    cached <-
        case declarationValidationRun prepared of
            FreshValidation ->
                pure Nothing
            WarmValidation
                    (ValidationLookup _lookupProof lookupDeclaration) ->
                liftIO (lookupDeclaration key)
    traverse_
        (\record ->
            case Materialization.checkDeclarationValidationRecord
                    (logicalBuilderPrefix
                        (declarationBuilder prepared))
                    syntax
                    objects
                    theorems
                    record of
                Left failure ->
                    liftIO
                        (throwIO
                            (CachedValidationIntegrityError failure))
                Right () ->
                    pure ())
        cached
    let selection =
            case cached of
                Nothing ->
                    FreshDeclarationValidation
                Just record ->
                    CachedDeclarationValidation
                        syntax objects theorems record ordinals
    State.put
        prepared
            { declarationValidationSelection = selection
            }
    runDeclaration action

prepareCompiledValidation
    :: DeclarationState
    -> Either
        DeclarationError
        ( DeclarationSyntaxId
        , [ObjectId]
        , [TheoremId]
        , Map FactSlot Natural
        , DeclarationState
        )
prepareCompiledValidation declaration = do
    syntax <-
        case declarationValidationMode declaration of
            DeclarationValidationMode value ->
                Right value
            _ ->
                Left DeclarationValidationOutsideCompiledDeclaration
    case declarationValidationSelection declaration of
        DeclarationValidationUnselected -> pure ()
        _ -> Left DeclarationValidationAlreadySelected
    closure <- declarationClosure declaration
    let builder = declarationBuilder declaration
        candidates = Map.elems (declarationReservations declaration)
        objects =
            assertedObjectId
                <$> reverse
                    (declarationObjectsReversed declaration)
        theorems =
            theoremId . candidateTheoremReference builder
                <$> candidates
        ordinals =
            Map.fromList
                (zip
                    (reservedCandidateSlot <$> candidates)
                    [0 ..])
    pure
        ( syntax
        , objects
        , theorems
        , ordinals
        , declaration
            { declarationObjectClosure = Just closure
            }
        )

lookupProofValidation
    :: ReservedCandidate
    -> Declaration (ProofSyntaxId, Maybe ProofValidationRecord)
lookupProofValidation candidate = Declaration do
    state <- State.get
    syntax <-
        case declarationValidationMode state of
            EnvironmentImportMode ->
                State.lift
                    (Except.throwError
                        ProofValidationOutsideProofDeclaration)
            ProofValidationMode proofSyntax ->
                pure proofSyntax
            DeclarationValidationMode{} ->
                State.lift
                    (Except.throwError
                        ProofValidationOutsideProofDeclaration)
    let builder = declarationBuilder state
        reference = candidateTheoremReference builder candidate
        key =
            proofValidationKey
                (theoremId
                    (factAuthorityTheorem
                        (factAuthority
                            reference
                            cleanAuthoritySafety)))
                syntax
                (logicalBuilderPrefix builder)
    record <-
        case declarationValidationRun state of
            FreshValidation ->
                pure Nothing
            WarmValidation (ValidationLookup lookupProof _lookupDeclaration) ->
                State.lift
                    (liftIO
                        (lookupProof key))
    pure (syntax, record)
data CandidatePremise = CandidatePremise
    !CheckedPropositionContent

data CandidateProofState = CandidateProofState
    { candidateProofDeclaration :: !DeclarationState
    , candidateProofObjectClosure :: !CheckedObjectClosure
    , candidateProofCandidate :: !ReservedCandidate
    , candidateProofCachedValidation
        :: !(Maybe Materialization.CandidateValidation)
    , candidateProofPremisesReversed :: ![CandidatePremise]
    , candidateProofPremiseCount :: !Natural
    , candidateProofSafety :: !CandidateSafety
    , candidateProofAcceptedRequestsReversed
        :: ![PreparedRequestId]
    }

candidateProofBuilder :: CandidateProofState -> LogicalBuilder
candidateProofBuilder =
    declarationBuilder . candidateProofDeclaration

newtype CandidateProof value = CandidateProof
    { runCandidateProof
        :: StateT
            CandidateProofState
            (ExceptT DeclarationError IO)
            value
    }
    deriving newtype (Functor, Applicative, Monad)

-- | Attach source trivia to a proof-obligation failure.  The location does
-- not participate in validation or request identity.
locateProofObligation
    :: Location
    -> CandidateProof value
    -> CandidateProof value
locateProofObligation location (CandidateProof action) =
    CandidateProof
        (State.mapStateT
            (Except.withExceptT
                (ProofObligationFailedAt location))
            action)

-- | Record that the current exact proof discharged one goal with @Omitted@.
recordOmittedUse :: CandidateProof ()
recordOmittedUse = CandidateProof do
    state <- State.get
    State.put
        state
            { candidateProofSafety =
                addCandidateEscape
                    Omitted
                    (candidateProofSafety state)
            }

data VampirePremiseSelection
    = VampireImplicitPremises
    | VampireExplicitPremises
        !(NonEmpty SemanticFactOccurrenceFingerprint)
    | VampireLocalPremises
    deriving stock (Show, Eq)

data VampireObligationPreparationError local
    = VampireObligationIndirectTargetNotFalsum
    | VampireObligationClaimProjectionFailed
        !(Backend.SupportedPropositionProjectionError local)
    | VampireObligationLocalProjectionFailed
        !Backend.LocalPremiseOrdinal
        !(Backend.SupportedPropositionProjectionError local)
    | VampireObligationLocalClassificationFailed
        !Backend.LocalPremiseOrdinal
        !(Backend.BackendClassificationError ObjectId)
    | VampireObligationFactNotVisible
        !SemanticFactOccurrenceFingerprint
    | VampireObligationFactInvalid
        !SemanticFactOccurrenceFingerprint
    | VampireObligationPlanningFailed
        !(Backend.TypedProblemError local ObjectId)
    | VampireObligationEncodingFailed
        !(Tptp.TypedTptpPreparationError local ObjectId)
    deriving stock (Show, Eq)

data ScopedVampirePremise local origin = ScopedVampirePremise
    !Backend.LocalPremiseOrdinal
    !origin
    !(Vector (local, CoreType))
    !(ScopedCheckedCore ObjectId)

scopedVampirePremise
    :: Backend.LocalPremiseOrdinal
    -> origin
    -> Vector (local, CoreType)
    -> ScopedCheckedCore ObjectId
    -> ScopedVampirePremise local origin
scopedVampirePremise =
    ScopedVampirePremise

data PreparedVampireObligation local origin =
    PreparedVampireObligation
        !(Backend.TypedProblem
            SemanticFactOccurrenceFingerprint
            local
            origin
            ObjectId)
        !(Provers.PreparedTypedProverTask
            SemanticFactOccurrenceFingerprint
            local
            origin
            ObjectId)

-- | Prepare a scoped task for a trusted structural proof checker.  This
-- validates the typed problem but does not establish how its local judgments
-- derive from the enclosing theorem.  'Checking.Exact.Proof' owns that
-- composition on the production path.
prepareScopedVampireObligationDriver
    :: Ord local
    => Vector (local, CoreType)
    -> ScopedCheckedCore ObjectId
    -> [ScopedVampirePremise local origin]
    -> [FoundationAxiomTag]
    -> VampirePremiseSelection
    -> ModuleDriver failure
        (Either
            (VampireObligationPreparationError local)
            (PreparedVampireObligation local origin))
prepareScopedVampireObligationDriver
        claimSupport claim scopedLocals auxiliaryTags selection =
    prepareScopedVampireObligationForMode
        Provers.DirectTask
        claimSupport
        claim
        scopedLocals
        auxiliaryTags
        selection

-- | Prepare the one indirect task admitted by the exact proof compiler.
-- The target check keeps contradictory input from authorizing another goal.
prepareScopedContradictionObligationDriver
    :: Ord local
    => Vector (local, CoreType)
    -> ScopedCheckedCore ObjectId
    -> [ScopedVampirePremise local origin]
    -> [FoundationAxiomTag]
    -> VampirePremiseSelection
    -> ModuleDriver failure
        (Either
            (VampireObligationPreparationError local)
            (PreparedVampireObligation local origin))
prepareScopedContradictionObligationDriver
        claimSupport claim scopedLocals auxiliaryTags selection
    | scopedCoreType claim /= TyProp || scopedCoreTerm claim /= CFalsum =
        pure (Left VampireObligationIndirectTargetNotFalsum)
    | otherwise =
        prepareScopedVampireObligationForMode
            Provers.IndirectTask
            claimSupport
            claim
            scopedLocals
            auxiliaryTags
            selection

prepareScopedVampireObligationLowering
    :: Ord local
    => Vector (local, CoreType)
    -> ScopedCheckedCore ObjectId
    -> [ScopedVampirePremise local origin]
    -> [FoundationAxiomTag]
    -> VampirePremiseSelection
    -> LoweringDriver
        (Either
            (VampireObligationPreparationError local)
            (PreparedVampireObligation local origin))
prepareScopedVampireObligationLowering
        claimSupport claim scopedLocals auxiliaryTags selection =
    prepareScopedVampireObligationForModeLowering
        Provers.DirectTask
        claimSupport claim scopedLocals auxiliaryTags selection

prepareScopedContradictionObligationLowering
    :: Ord local
    => Vector (local, CoreType)
    -> ScopedCheckedCore ObjectId
    -> [ScopedVampirePremise local origin]
    -> [FoundationAxiomTag]
    -> VampirePremiseSelection
    -> LoweringDriver
        (Either
            (VampireObligationPreparationError local)
            (PreparedVampireObligation local origin))
prepareScopedContradictionObligationLowering
        claimSupport claim scopedLocals auxiliaryTags selection
    | scopedCoreType claim /= TyProp || scopedCoreTerm claim /= CFalsum =
        pure (Left VampireObligationIndirectTargetNotFalsum)
    | otherwise =
        prepareScopedVampireObligationForModeLowering
            Provers.IndirectTask
            claimSupport claim scopedLocals auxiliaryTags selection

prepareScopedVampireObligationForModeLowering
    :: Ord local
    => Provers.VampireTaskMode
    -> Vector (local, CoreType)
    -> ScopedCheckedCore ObjectId
    -> [ScopedVampirePremise local origin]
    -> [FoundationAxiomTag]
    -> VampirePremiseSelection
    -> LoweringDriver
        (Either
            (VampireObligationPreparationError local)
            (PreparedVampireObligation local origin))
prepareScopedVampireObligationForModeLowering
        taskMode claimSupport claim scopedLocals auxiliaryTags selection =
    LoweringDriver do
        LoweringState resolver (ProspectiveBuilder builder) _validation <-
            State.get
        liftIO
            (prepareScopedVampireObligationWith
                resolver builder taskMode claimSupport claim scopedLocals
                auxiliaryTags selection)

prepareScopedVampireObligationForMode
    :: Ord local
    => Provers.VampireTaskMode
    -> Vector (local, CoreType)
    -> ScopedCheckedCore ObjectId
    -> [ScopedVampirePremise local origin]
    -> [FoundationAxiomTag]
    -> VampirePremiseSelection
    -> ModuleDriver failure
        (Either
            (VampireObligationPreparationError local)
            (PreparedVampireObligation local origin))
prepareScopedVampireObligationForMode
        taskMode claimSupport claim scopedLocals auxiliaryTags selection =
    ModuleDriver do
        DriverState resolver builder _prefix _validation <- State.get
        State.lift
            (Except.liftIO
                (prepareScopedVampireObligationWith
                    resolver builder taskMode claimSupport claim scopedLocals
                    auxiliaryTags selection))

prepareScopedVampireObligationWith
    :: (Ord local)
    => VampireResolver
    -> BuilderState evidence
    -> Provers.VampireTaskMode
    -> Vector (local, CoreType)
    -> ScopedCheckedCore ObjectId
    -> [ScopedVampirePremise local origin]
    -> [FoundationAxiomTag]
    -> VampirePremiseSelection
    -> IO
        (Either
            (VampireObligationPreparationError local)
            (PreparedVampireObligation local origin))
prepareScopedVampireObligationWith
        resolver builder taskMode claimSupport claim scopedLocals
        auxiliaryTags selection =
    measureVampirePreparation resolver preparation
  where
    closure = logicalBuilderObjectClosure builder
    globalType = (`lookupCheckedObjectType` closure)
    preparation = do
        supportedClaim <-
            first VampireObligationClaimProjectionFailed
                (Backend.projectSupportedProposition
                    globalType
                    claimSupport
                    claim)
        locals <- traverse prepareLocal scopedLocals
        prepareVampireObligationWith
            taskMode
            builder
            closure
            supportedClaim
            locals
            auxiliaryTags
            selection

    prepareLocal
            (ScopedVampirePremise
                ordinal origin support proposition) = do
        supported <-
            first
                (VampireObligationLocalProjectionFailed ordinal)
                (Backend.projectSupportedProposition
                    globalType
                    support
                    proposition)
        first
            (VampireObligationLocalClassificationFailed ordinal)
            (Backend.typedLocalPremise
                globalType
                ordinal
                origin
                supported)

prepareVampireObligationWith
    :: Ord local
    => Provers.VampireTaskMode
    -> BuilderState evidence
    -> CheckedObjectClosure
    -> Backend.SupportedProposition local ObjectId
    -> [Backend.TypedLocalPremise local origin ObjectId]
    -> [FoundationAxiomTag]
    -> VampirePremiseSelection
    -> Either
        (VampireObligationPreparationError local)
        (PreparedVampireObligation local origin)
prepareVampireObligationWith
        taskMode builder closure claim locals auxiliaryTags selection = do
    let globalType = (`lookupCheckedObjectType` closure)
    selected <-
        selectVampireFacts
            globalType
            builder
            selection
    let premiseSelection =
            case selection of
                VampireImplicitPremises ->
                    Backend.ImplicitPremiseSelection
                VampireExplicitPremises{} ->
                    Backend.ExplicitGlobalPremiseSelection
                VampireLocalPremises ->
                    Backend.LocalOnlyPremiseSelection
        propositionDependencies =
            foundationAxiomDependencies
                . Backend.supportedPropositionTerm
        requiredAuxiliaryTags =
            Set.toAscList
                ( Set.fromList auxiliaryTags
                    <> propositionDependencies claim
                    <> foldMap
                        (propositionDependencies
                            . Backend.typedBackendFactProposition)
                        selected
                    <> foldMap
                        (propositionDependencies
                            . Backend.typedLocalPremiseProposition)
                        (Backend.selectTypedLocalPremises
                            premiseSelection
                            locals)
                )
        auxiliaries =
            Backend.typedFoundationAuxiliaryInput
                (logicalBuilderFoundation builder)
                <$> requiredAuxiliaryTags
    problem <-
        first VampireObligationPlanningFailed
            (Backend.planTypedProblem
                globalType
                selected
                claim
                locals
                auxiliaries
                premiseSelection)
    task <-
        first VampireObligationEncodingFailed
            (Provers.prepareTypedProverTask
                taskMode
                problem)
    pure (PreparedVampireObligation problem task)

measureVampirePreparation
    :: VampireResolver
    -> Either
        (VampireObligationPreparationError local)
        (PreparedVampireObligation local origin)
    -> IO
        (Either
            (VampireObligationPreparationError local)
            (PreparedVampireObligation local origin))
measureVampirePreparation resolver preparation = do
    started <- getMonotonicTimeNSec
    prepared <- Exception.evaluate (forcePrepared preparation)
    finished <- getMonotonicTimeNSec
    observeVampirePreparation resolver (finished - started)
    pure prepared
  where
    forcePrepared result =
        case result of
            Left err -> err `seq` result
            Right prepared@(PreparedVampireObligation _ task) ->
                let request = Provers.preparedTypedProverRequest task
                in Provers.preparedVerificationByteCount request `seq`
                    Provers.preparedVerificationRequestId request `seq`
                    prepared `seq`
                    result

selectVampireFacts
    :: (ObjectId -> Maybe CoreType)
    -> BuilderState evidence
    -> VampirePremiseSelection
    -> Either
        (VampireObligationPreparationError local)
        (Vector
            (Backend.TypedBackendFact
                SemanticFactOccurrenceFingerprint
                ObjectId))
selectVampireFacts globalType builder selection =
    Vector.fromList <$> case selection of
        VampireImplicitPremises ->
            mapMaybeM prepareImplicit
                (Map.toAscList (logicalBuilderFacts builder))
        VampireExplicitPremises fingerprints ->
            traverse prepareExplicit
                (stableUniqueBy id (toList fingerprints))
        VampireLocalPremises ->
            Right []
  where
    prepareImplicit (fingerprint, authorized@(FactEntry
            _proposition occurrence _authorization))
        | semanticFactSearchEligibility occurrence
            /= SearchEligible =
                Right Nothing
        | otherwise = do
            fact <- prepareFact fingerprint authorized
            pure case Backend.typedBackendFactCapability fact of
                Backend.FofProjectable{} -> Just fact
                Backend.RequiresTh0{} -> Nothing

    prepareExplicit fingerprint =
        case Map.lookup fingerprint (logicalBuilderFacts builder) of
            Nothing ->
                Left (VampireObligationFactNotVisible fingerprint)
            Just authorized ->
                prepareFact fingerprint authorized

    prepareFact fingerprint
            (FactEntry proposition occurrence _authorization)
        | semanticFactFingerprint occurrence /= fingerprint =
            Left (VampireObligationFactInvalid fingerprint)
        | otherwise = do
            supported <-
                first
                    (const
                        (VampireObligationFactInvalid fingerprint))
                    (Backend.supportedProposition
                        Vector.empty
                        (embedClosedCore
                            []
                            (checkedPropositionTerm proposition)))
            capability <-
                first
                    (const
                        (VampireObligationFactInvalid fingerprint))
                    (Backend.classifySupportedProposition
                        globalType
                        supported)
            pure
                (Backend.typedBackendFact
                    fingerprint
                    supported
                    capability)

    mapMaybeM action =
        fmap catMaybes . traverse action

data LocalClaim = LocalClaim
    !BuilderIdentity
    !DeclarationInvocation
    !FactSlot
    !CheckedPropositionContent

useAuthorizedFact
    :: SemanticFactOccurrenceFingerprint
    -> CandidateProof ImportIx
useAuthorizedFact fingerprint = do
    proposition <- consumeAuthorizedFact fingerprint
    registerKernelImport proposition

-- | Validate one fact capability and accumulate only its safety effect.
-- Backend use does not register a kernel import.
consumeAuthorizedFact
    :: SemanticFactOccurrenceFingerprint
    -> CandidateProof CheckedPropositionContent
consumeAuthorizedFact fingerprint = CandidateProof do
    state <- State.get
    let builder = candidateProofBuilder state
        declaration = candidateProofDeclaration state
        staged =
            findPendingByFingerprint
                fingerprint
                (declarationPending declaration)
    case staged of
        Just pending ->
            consumePendingFact pending state
        Nothing ->
            case Map.lookup
                    fingerprint
                    (logicalBuilderFacts builder) of
                Nothing ->
                    State.lift
                        (Except.throwError
                            (AuthorizedFactNotVisible fingerprint))
                Just authorized ->
                    consumeBuilderAuthorizedFact authorized state

-- | Materialize one sealed direct import and its transitive parents.  The
-- interface DAG is folded imported-before-importer and each producer
-- occurrence receives a fresh capability for this consuming builder.
importSealedModule
    :: ImportedModuleEvidence
    -> Declaration ()
importSealedModule evidence = Declaration do
    state <- State.get
    when
        (isJust (declarationObjectClosure state))
        (State.lift
            (Except.throwError ImportedModuleAfterAuthorization))
    let builder = declarationBuilder state
        interfaceId =
            semanticInterfaceAssertedId
                (evidenceInterface evidence)
    unless
        (interfaceId `elem`
            logicalBuilderDirectSemanticInputs builder)
        (State.lift
            (Except.throwError
                (ImportedModuleNotDirect interfaceId)))
    imported <-
        State.lift
            (Except.liftEither
                (foldImportedEvidence evidence builder))
    State.put
        state
            { declarationBuilder = imported
            , declarationObjectClosure = Nothing
            }

-- The walking path keeps complete aggregate maps. Measure long chains before
-- replacing this representation.
foldImportedEvidence
    :: ImportedModuleEvidence
    -> LogicalBuilder
    -> Either DeclarationError LogicalBuilder
foldImportedEvidence evidence builder
    | interfaceId
        `Set.member` logicalBuilderImportedInterfaces builder =
            Right builder
    | otherwise = do
        unless
            (semanticInterfaceDirectInputs interface
                == (semanticInterfaceAssertedId . evidenceInterface
                        <$> parents))
            (Left
                (ImportedEvidenceDirectMismatch
                    (semanticInterfaceDirectInputs interface)
                    (semanticInterfaceAssertedId . evidenceInterface
                        <$> parents)))
        withParents <- foldM
            (flip foldImportedEvidence)
            builder
            parents
        objectClosure <-
            first
                DeclarationObjectValidationFailed
                (extendImportedObjectClosure
                    (logicalBuilderObjectClosure withParents)
                    objects)
        importedFacts <- foldM
            (insertImportedFact withParents)
            (logicalBuilderFacts withParents)
            (Map.elems entries)
        importedAliases <- foldM
            (insertImportedAlias importedFacts)
            (logicalBuilderAliases withParents)
            [ ( alias
              , ImportedAliasOrigin
                    (declarationDeltaSlot delta)
                    (semanticAliasTarget alias)
              )
            | delta <- semanticInterfaceDeclarations interface
            , alias <- declarationDeltaAliases delta
            ]
        importedStructures <- foldM
            (insertSemanticStructure objectClosure)
            (logicalBuilderStructures withParents)
            [ descriptor
            | delta <- semanticInterfaceDeclarations interface
            , descriptor <- semanticEnvironmentStructures
                (declarationDeltaEnvironment delta)
            ]
        importedGlobals <- foldM
            (insertImportedGlobal objectClosure importedStructures)
            (logicalBuilderGlobals withParents)
            [ binding
            | delta <- semanticInterfaceDeclarations interface
            , binding <- semanticEnvironmentBindings
                (declarationDeltaEnvironment delta)
            ]
        pure
            withParents
                { logicalBuilderFacts = importedFacts
                , logicalBuilderAliases = importedAliases
                , logicalBuilderGlobals = importedGlobals
                , logicalBuilderStructures = importedStructures
                , logicalBuilderObjectClosure = objectClosure
                , logicalBuilderImportedInterfaces =
                    Set.insert
                        interfaceId
                        (logicalBuilderImportedInterfaces withParents)
                }
  where
    ImportedModuleEvidence interface parents entries objects = evidence
    interfaceId = semanticInterfaceAssertedId interface

    extendImportedObjectClosure closure asserted =
        extendObjectClosure
            closure
            [ object
            | object <- asserted
            , assertedObjectId object
                `Set.notMember` checkedObjectIds closure
            ]

    insertImportedFact
        current facts pair = do
            let (occurrence, proposition) = pair
                fingerprint = semanticFactFingerprint occurrence
                authority = semanticFactAuthority occurrence
            _ <-
                first ImportedFactMaterializationFailed
                    (Materialization.checkImportedOccurrence
                        (logicalBuilderTheory current)
                        fingerprint
                        occurrence
                        proposition
                        authority)
            let authorization =
                    BuilderFactAuthorization
                        (logicalBuilderIdentity current)
                        (semanticFactSlot occurrence)
                        authority
                authorized =
                    FactEntry proposition occurrence authorization
            case Map.lookup fingerprint facts of
                Nothing ->
                    pure (Map.insert fingerprint authorized facts)
                Just existing
                    | equivalentAuthorizedFact existing authorized ->
                        pure facts
                    | otherwise ->
                        Left (ImportedFactCollision fingerprint)

    insertImportedAlias facts aliases (alias, origin) = do
        let name = semanticAliasName alias
            target = semanticAliasTarget alias
        unless
            (Map.member target facts)
            (Left (ImportedAliasTargetMissing target))
        case Map.lookup name aliases of
            Nothing ->
                pure
                    (Map.insert
                        name
                        (ImportedAliasBinding target origin)
                        aliases)
            Just (ImportedAliasBinding existingTarget existingOrigin)
                | existingTarget == target ->
                    pure aliases
                | otherwise ->
                    Left
                        (ImportedAliasCollision
                            name existingOrigin origin)

    insertImportedGlobal closure structures globals binding = do
        let key = semanticGlobalBindingKey binding
            target = semanticGlobalBindingTarget binding
        _ <-
            first
                (ImportedGlobalTargetInvalid key target)
                (validateSemanticGlobalBindingTarget
                    (structureOperationBindings structures)
                    closure binding)
        case Map.lookup key globals of
            Nothing -> pure (Map.insert key target globals)
            Just existing
                | existing == target -> pure globals
                | otherwise ->
                    Left (ImportedGlobalCollision key existing target)

insertSemanticStructure
    :: CheckedObjectClosure
    -> Map SemanticStructurePhrase ResolvedStructure
    -> SemanticStructureDescriptor
    -> Either
        DeclarationError
        (Map SemanticStructurePhrase ResolvedStructure)
insertSemanticStructure closure structures descriptor = do
    validateSemanticStructureTargets closure descriptor
    let structurePhrase = semanticStructureDescriptorPhrase descriptor
    case Map.lookup structurePhrase structures of
        Just (ResolvedStructure existing _ _)
            | existing == descriptor -> Right structures
            | otherwise ->
                Left
                    (ImportedStructureCollision
                        structurePhrase existing descriptor)
        Nothing -> do
            parents <- traverse resolveParent
                (semanticStructureDescriptorParents descriptor)
            inherited <- foldM mergeParentOperations Map.empty parents
            complete <- foldM insertOwnOperation inherited
                (semanticStructureDescriptorOperations descriptor)
            let ancestors =
                    Set.unions
                        [ Set.insert
                            (semanticStructureDescriptorPhrase
                                (resolvedStructureDescriptor parent))
                            parentAncestors
                        | parent@(ResolvedStructure _ parentAncestors _) <- parents
                        ]
                resolved = ResolvedStructure descriptor ancestors complete
            Right (Map.insert structurePhrase resolved structures)
  where
    resolveParent parentPhrase =
        maybe
            (Left
                (SemanticStructureParentMissing
                    (semanticStructureDescriptorPhrase descriptor)
                    parentPhrase))
            Right
            (Map.lookup parentPhrase structures)

    mergeParentOperations operations
            (ResolvedStructure _descriptor _ancestors parentOperations) =
        foldM insertInheritedOperation operations
            (Map.toAscList parentOperations)

    insertInheritedOperation operations (symbol, operation) =
        insertResolvedOperation symbol operation operations

    insertOwnOperation operations operation =
        insertResolvedOperation
            (semanticStructureOperationSymbol operation)
            (ResolvedStructureOperation
                (semanticStructureOperationObject operation)
                (semanticStructureDescriptorPhrase descriptor))
            operations

    insertResolvedOperation symbol incoming operations =
        case Map.lookup symbol operations of
            Nothing -> Right (Map.insert symbol incoming operations)
            Just (ResolvedStructureOperation existingObject existingOrigin) ->
                case incoming of
                    ResolvedStructureOperation incomingObject incomingOrigin
                        | existingObject == incomingObject -> Right operations
                        | otherwise ->
                            Left
                                (SemanticStructureOperationConflict
                                    symbol existingOrigin incomingOrigin)

validateSemanticStructureTargets
    :: CheckedObjectClosure
    -> SemanticStructureDescriptor
    -> Either DeclarationError ()
validateSemanticStructureTargets closure descriptor = do
    traverse_ validatePredicate
        (semanticStructureDescriptorPredicate descriptor)
    traverse_ validateOperation
        (semanticStructureDescriptorOperations descriptor)
  where
    validatePredicate object =
        validateObjectType
            (SemanticStructurePredicateTargetInvalid
                (semanticStructureDescriptorPhrase descriptor))
            object
            (TyArrow TySet TyProp)

    validateOperation operation =
        validateObjectType
            (SemanticStructureOperationTargetInvalid
                (semanticStructureDescriptorPhrase descriptor)
                (semanticStructureOperationSymbol operation))
            (semanticStructureOperationObject operation)
            (TyArrow TySet TySet)

    validateObjectType failure object expected =
        case lookupCheckedObjectType object closure of
            Nothing -> Left (failure object Nothing expected)
            Just actual
                | actual == expected -> Right ()
                | otherwise -> Left (failure object (Just actual) expected)

equivalentAuthorizedFact
    :: FactEntry BuilderFactAuthorization
    -> FactEntry BuilderFactAuthorization
    -> Bool
equivalentAuthorizedFact
        (FactEntry leftProposition leftOccurrence
            (BuilderFactAuthorization leftIdentity leftSlot leftAuthority))
        (FactEntry rightProposition rightOccurrence
            (BuilderFactAuthorization rightIdentity rightSlot rightAuthority)) =
    checkedPropositionId leftProposition
        == checkedPropositionId rightProposition
        && leftOccurrence == rightOccurrence
        && leftIdentity == rightIdentity
        && leftSlot == rightSlot
        && leftAuthority == rightAuthority

-- | Driver-level form used before the first declaration of a consuming
-- module.  It changes only the private builder's imported fact environment;
-- no declaration prefix or durable envelope is emitted.
importSealedModuleDriver
    :: ImportedModuleEvidence
    -> ModuleDriver failure ()
importSealedModuleDriver evidence = ModuleDriver do
    DriverState resolver builder prefix validationRun <-
        State.get
    let declaration =
            initialDeclarationState
                resolver
                validationRun
                EnvironmentImportMode
                builder
    result <-
        liftIO
            (Except.runExceptT
                (State.runStateT
                    (runDeclaration
                        (importSealedModule evidence))
                    declaration))
    case result of
        Left failure ->
            Except.throwError (DriverDeclarationFailed failure)
        Right (_value, importedState) ->
            State.put
                (DriverState
                    resolver
                    (declarationBuilder importedState)
                    prefix
                    validationRun)

useStagedCandidate
    :: ReservedCandidate
    -> CandidateProof ImportIx
useStagedCandidate premise = CandidateProof do
    state <- State.get
    let current = candidateProofCandidate state
        declaration = candidateProofDeclaration state
    State.lift
        (Except.liftEither
            (validateReservedCandidate
                declaration
                premise))
    State.lift
        (Except.liftEither
            (validateStrictCandidateStage premise current))
    pending <-
        maybe
            (State.lift
                (Except.throwError
                    (StagedPremiseNotAuthorized
                        (reservedCandidateSlot premise))))
            pure
            (Map.lookup
                (reservedCandidateSlot premise)
                (declarationPending declaration))
    let proposedAuthority =
            validationTarget (pendingCandidateCertificate pending)
    checkedStage <-
        State.lift
            (Except.liftEither
                (prepareCheckedDeclarationStage
                    declaration
                    (candidateProofObjectClosure state)
                    [(premise, proposedAuthority)]))
    stagedProposition <-
        State.lift
            (Except.liftEither
                (useCheckedStageFact checkedStage current premise))
    proposition <- consumePendingFact pending state
    unless
        (checkedPropositionId stagedProposition
            == checkedPropositionId proposition)
        (State.lift
            (Except.throwError
                (PlanningFactContractMismatch
                    (reservedCandidateSlot premise))))
    updated <- State.get
    appendCandidatePremise proposition updated

validateStrictCandidateStage
    :: ReservedCandidate
    -> ReservedCandidate
    -> Either DeclarationError ()
validateStrictCandidateStage premise current =
    unless
        (reservedStage premise < reservedStage current)
        (Left
            (StagedPremiseNotEarlier
                (reservedCandidateSlot premise)
                (reservedCandidateStage premise)
                (reservedCandidateSlot current)
                (reservedCandidateStage current)))

prepareCheckedDeclarationStage
    :: DeclarationState
    -> CheckedObjectClosure
    -> [(ReservedCandidate, FactAuthority)]
    -> Either DeclarationError CheckedDeclarationStage
prepareCheckedDeclarationStage declaration closure candidates = do
    entries <- foldM insertCandidate Map.empty candidates
    pure (CheckedDeclarationStage ownSlot closure entries)
  where
    builder = declarationBuilder declaration
    ownSlot = declarationOwnSlot declaration

    insertCandidate entries (candidate, authority) = do
        validateReservedCandidate declaration candidate
        let slot = reservedCandidateSlot candidate
        unless
            (factAuthorityTheorem authority
                == candidateTheoremReference builder candidate)
            (Left (PlanningFactContractMismatch slot))
        when
            (Map.member slot entries)
            (Left (PlanningFactContractMismatch slot))
        let occurrence = candidateOccurrence candidate authority
            evidence = PlanningEvidence
                authority
                (Just
                    (PlanningProvenance
                        ownSlot
                        (reservedStage candidate)
                        slot))
        pure
            (Map.insert
                slot
                (FactEntry
                    (candidateCheckedProposition candidate)
                    occurrence
                    evidence)
                entries)

useCheckedStageFact
    :: CheckedDeclarationStage
    -> ReservedCandidate
    -> ReservedCandidate
    -> Either DeclarationError CheckedPropositionContent
useCheckedStageFact
        (CheckedDeclarationStage ownSlot closure entries)
        current
        premise = do
    validateStrictCandidateStage premise current
    let slot = reservedCandidateSlot premise
    FactEntry proposition occurrence
        (PlanningEvidence authority provenance) <-
            maybe
                (Left (PlanningFactContractMismatch slot))
                Right
                (Map.lookup slot entries)
    unless
        ( provenance
            == Just
                (PlanningProvenance
                    ownSlot
                    (reservedStage premise)
                    slot)
          && semanticFactSlot occurrence == slot
          && semanticFactAuthority occurrence == authority
          && checkedPropositionId proposition
                == checkedPropositionId
                    (candidateCheckedProposition premise)
          && propositionMatchesClosure closure proposition
        )
        (Left (PlanningFactContractMismatch slot))
    pure proposition

propositionMatchesClosure
    :: CheckedObjectClosure
    -> CheckedPropositionContent
    -> Bool
propositionMatchesClosure closure proposition =
    case validateAssertedPropositionContent
            closure
            (checkedPropositionId proposition)
            (frozenCoreTerm (checkedPropositionTerm proposition)) of
        Right _ -> True
        Left _ -> False

candidateOccurrence
    :: ReservedCandidate
    -> FactAuthority
    -> SemanticFactOccurrence
candidateOccurrence
        (ReservedCandidate _ _ _ _ slot
            (CandidateSpec _ eligibility _aliases))
        authority =
    semanticFactOccurrence slot authority eligibility

candidateAliases :: ReservedCandidate -> [SemanticName]
candidateAliases
        (ReservedCandidate _ _ _ _ _
            (CandidateSpec _ _ aliases)) =
    aliases

proveLocalKernelClaim
    :: CheckedPropositionContent
    -> KernelDerivation ObjectId
    -> CandidateProof LocalClaim
proveLocalKernelClaim proposition derivation = CandidateProof do
    state <- State.get
    void
        (State.lift
            (Except.liftEither
                (replayCandidateKernel proposition derivation state)))
    let candidate = candidateProofCandidate state
        declaration = candidateProofDeclaration state
    pure
        (LocalClaim
            (logicalBuilderIdentity
                (candidateProofBuilder state))
            (declarationInvocation declaration)
            (reservedCandidateSlot candidate)
            proposition)

useLocalClaim :: LocalClaim -> CandidateProof ImportIx
useLocalClaim
        (LocalClaim identity invocation slot proposition) =
    CandidateProof do
        state <- State.get
        let builder = candidateProofBuilder state
            declaration = candidateProofDeclaration state
            candidate = candidateProofCandidate state
        unless
            ( identity == logicalBuilderIdentity builder
              && invocation == declarationInvocation declaration
              && slot == reservedCandidateSlot candidate
            )
            (State.lift
                (Except.throwError LocalClaimOutsideCandidate))
        appendCandidatePremise proposition state


authorizeKernelProofCandidate
    :: ReservedCandidate
    -> CandidateProof (KernelDerivation ObjectId)
    -> Declaration ()
authorizeKernelProofCandidate candidate proof =
    authorizeOneCandidate candidate \initial -> do
        (derivation, final) <-
            State.runStateT (runCandidateProof proof) initial
        when
            (isNothing (candidateProofCachedValidation final))
            (void
                (Except.liftEither
                    (replayCandidateKernel
                        (candidateCheckedProposition candidate)
                        derivation
                        final)))
        completeCandidateWithValidation
                candidate
                (CheckedSourceProof
                    (acceptedRequestIds final))
                (candidateProofSafety final)
                final

authorizeKernelConstructionCandidate
    :: KernelConstructionDescriptor
    -> ReservedCandidate
    -> CandidateProof (KernelDerivation ObjectId)
    -> Declaration ()
authorizeKernelConstructionCandidate descriptor candidate proof =
    authorizeOneCandidate candidate \initial -> do
        (derivation, final) <-
            State.runStateT (runCandidateProof proof) initial
        when
            (isNothing (candidateProofCachedValidation final)) do
                replayed <-
                    Except.liftEither
                        (replayCandidateKernel
                            (candidateCheckedProposition candidate)
                            derivation
                            final)
                Except.liftEither
                    (validateKernelConstruction
                        descriptor
                        (candidateCheckedProposition candidate)
                        replayed
                        final)
        completeCandidateWithValidation
                candidate
                (CheckedKernelConstruction descriptor)
                (candidateProofSafety final)
                final

authorizeDefinitionEquationCandidate
    :: ObjectId
    -> ReservedCandidate
    -> Declaration ()
authorizeDefinitionEquationCandidate identity candidate =
    authorizeOneCandidate candidate \initial -> do
        when
            (isNothing (candidateProofCachedValidation initial))
            (unless
                (matchesDefinitionEquation
                    identity
                    (candidateCheckedProposition candidate)
                    initial)
                (Except.throwError
                    DefinitionEquationCandidateMismatch))
        completeCandidateWithValidation
            candidate
            (CheckedKernelConstruction
                (CheckedDefinitionEquation identity))
            (candidateProofSafety initial)
            initial

authorizeSourceAxiomCandidate
    :: ReservedCandidate
    -> Declaration ()
authorizeSourceAxiomCandidate candidate =
    authorizeOneCandidate candidate \initial ->
        let safety =
                addCandidateEscape
                    SourceAxiom
                    initialCandidateSafety
        in completeCandidateWithValidation
                candidate
                SourceAxiomAuthorization
                safety
                initial

-- | Complete one exact deterministic datatype as a single trusted family.
-- The descriptor, objects, and complete candidate batch must agree exactly.
-- Law semantics are trusted to the sole production compiler in
-- "Checking.Exact.Datatype"; this boundary validates its complete inventory,
-- not the meaning of each generated proposition.
authorizeDatatypeCompilationCandidates
    :: DatatypeCompilationDescriptor
    -> ObjectId
    -> NonEmpty ObjectId
    -> NonEmpty ReservedCandidate
    -> Declaration ()
authorizeDatatypeCompilationCandidates
        suppliedDescriptor carrier constructors candidates =
    Declaration do
        state <- State.get
        let builder = declarationBuilder state
            objectInventory = carrier : NonEmpty.toList constructors
            declaredObjects =
                assertedObjectId
                    <$> reverse (declarationObjectsReversed state)
            reservedCandidates =
                Map.elems (declarationReservations state)
            theoremInventory =
                candidateTheoremReference builder
                    <$> NonEmpty.toList candidates
            expectedDescriptor =
                datatypeCompilationDescriptor
                    carrier
                    constructors
                    theoremInventory
            stages =
                nubOrd
                    (reservedCandidateStage
                        <$> NonEmpty.toList candidates)
        unless
            ( suppliedDescriptor == expectedDescriptor
              && declaredObjects == objectInventory
              && reservedCandidates == NonEmpty.toList candidates
              && length stages == 1
            )
            (State.lift
                (Except.throwError
                    DatatypeCompilationDescriptorMismatch))
        runDeclaration
            (traverse_
                (authorizeDatatypeCandidate suppliedDescriptor)
                candidates)

authorizeDatatypeCandidate
    :: DatatypeCompilationDescriptor
    -> ReservedCandidate
    -> Declaration ()
authorizeDatatypeCandidate descriptor candidate =
    authorizeOneCandidate candidate \initial ->
        completeCandidateWithValidation
            candidate
            (TrustedCompilation
                (DatatypeCompilation descriptor))
            initialCandidateSafety
            initial

authorizeOmittedCandidate
    :: ReservedCandidate
    -> CandidateProof ()
    -> Declaration ()
authorizeOmittedCandidate candidate proof =
    authorizeOneCandidate candidate \initial -> do
        cached <-
            selectProofCandidateValidation candidate initial
        let preparedInitial =
                initial
                    { candidateProofCachedValidation = cached
                    }
        ((), final) <-
            State.runStateT (runCandidateProof proof) preparedInitial
        let safety = candidateProofSafety final
        unless
            (Omitted
                `elem` escapeKindsToList
                    (authoritySafetyEscapeKinds
                        (candidateSafetyAuthority safety)))
            (Except.throwError OmittedProofDidNotRecordUse)
        completeCandidateWithValidation
                candidate
                OmittedAuthorization
                safety
                final

-- | Retain the closed candidate-target path while scoped proof composition is
-- introduced. It uses the same environment validation as local obligations.
acceptVampireObligation
    :: Provers.PreparedTypedProverTask
        SemanticFactOccurrenceFingerprint
        Void
        origin
        ObjectId
    -> CandidateProof ()
acceptVampireObligation prepared =
    acceptValidatedVampireTask
        (validateCandidateVampireProblem prepared)
        prepared

-- | Validate one internally prepared scoped obligation, then retain its exact
-- accepted request.  The trusted caller remains responsible for structural
-- local-proof composition.
acceptPreparedVampireObligation
    :: (Eq local, Eq origin)
    => PreparedVampireObligation local origin
    -> CandidateProof ()
acceptPreparedVampireObligation
        (PreparedVampireObligation expected prepared) =
    acceptValidatedVampireTask
        (validatePreparedVampireProblem expected prepared)
        prepared

-- | Prepare and execute the current closed candidate using exactly the
-- staged premises already consumed by its trusted declaration compiler.
acceptCurrentCandidateVampire :: CandidateProof ()
acceptCurrentCandidateVampire =
    prepareCurrentCandidateVampire
        >>= acceptPreparedVampireObligation

-- | Prepare the current closed candidate without executing its request.  The
-- declaration-owned batch authorizer uses this seam only after all strictly
-- earlier staged premises have been consumed.
prepareCurrentCandidateVampire
    :: CandidateProof (PreparedVampireObligation Void ())
prepareCurrentCandidateVampire = CandidateProof do
    initial <- State.get
    let builder = candidateProofBuilder initial
        closure = candidateProofObjectClosure initial
        target = candidateCheckedProposition
            (candidateProofCandidate initial)
        premises =
            [ proposition
            | CandidatePremise proposition <-
                reverse (candidateProofPremisesReversed initial)
            ]
        resolver =
            declarationVampireResolver
                (candidateProofDeclaration initial)
        preparation =
            prepareClosedCandidateVampire
                builder closure target premises
    preparedResult <-
        State.lift
            (liftIO
                (measureVampirePreparation resolver preparation))
    prepared <-
        State.lift
            (Except.liftEither
                (first
                    CurrentCandidateVampirePreparationFailed
                    preparedResult))
    pure prepared

prepareClosedCandidateVampire
    :: BuilderState evidence
    -> CheckedObjectClosure
    -> CheckedPropositionContent
    -> [CheckedPropositionContent]
    -> Either
        (VampireObligationPreparationError Void)
        (PreparedVampireObligation Void ())
prepareClosedCandidateVampire builder closure target premises = do
    supportedTarget <-
        first
            VampireObligationClaimProjectionFailed
            (Backend.projectSupportedProposition
                globalType
                (Vector.empty :: Vector (Void, CoreType))
                (closed target))
    locals <-
        traverse
            prepareLocal
            (zip [0 :: Natural ..] premises)
    prepareVampireObligationWith
        Provers.DirectTask
        builder
        closure
        supportedTarget
        locals
        []
        VampireLocalPremises
  where
    globalType = (`lookupCheckedObjectType` closure)
    closed proposition =
        embedClosedCore []
            (checkedPropositionTerm proposition)

    prepareLocal (index, proposition) = do
        let ordinal = Backend.localPremiseOrdinal index
        supported <-
            first
                (VampireObligationLocalProjectionFailed ordinal)
                (Backend.projectSupportedProposition
                    globalType
                    (Vector.empty :: Vector (Void, CoreType))
                    (closed proposition))
        first
            (VampireObligationLocalClassificationFailed ordinal)
            (Backend.typedLocalPremise
                globalType ordinal () supported)

acceptValidatedVampireTask
    :: (CandidateProofState
        -> ExceptT DeclarationError IO CandidateProofState)
    -> Provers.PreparedTypedProverTask
        SemanticFactOccurrenceFingerprint
        local
        origin
        ObjectId
    -> CandidateProof ()
acceptValidatedVampireTask validate prepared = CandidateProof do
    initial <- State.get
    validated <- State.lift (validate initial)
    result <-
        case candidateProofCachedValidation initial of
            Nothing -> do
                let resolver =
                        declarationVampireResolver
                            (candidateProofDeclaration initial)
                Just <$> State.lift (resolveOneVampire resolver prepared)
            Just _validation ->
                pure Nothing
    final <-
        State.lift
            (acceptVampireBatchMemberResult
                prepared result validated)
    State.put final

-- | Complete one checked source candidate after all of its obligations have
-- been accepted in source order.  The enclosing proof declaration owns the
-- exact syntax key and selects live or cached execution before this action.
authorizeVampireCandidate
    :: ReservedCandidate
    -> CandidateProof ()
    -> Declaration ()
authorizeVampireCandidate candidate proof =
    authorizeOneCandidate candidate \initial -> do
        cached <-
            selectProofCandidateValidation candidate initial
        let preparedInitial =
                initial
                    { candidateProofCachedValidation = cached
                    }
        ((), final) <-
            State.runStateT (runCandidateProof proof) preparedInitial
        case acceptedRequestIds final of
            [] ->
                Except.throwError
                    VampireProofHasNoAcceptedObligations
            requests ->
                completeCandidateWithValidation
                    candidate
                    (CheckedSourceProof requests)
                    (candidateProofSafety final)
                    final

data PreparedVampireCandidateBatchMember =
    PreparedVampireCandidateBatchMember
        !Location
        !ReservedCandidate
        !(Provers.PreparedTypedProverTask
            SemanticFactOccurrenceFingerprint
            Void
            ()
            ObjectId)
        !CandidateProofState

data ResolvedVampireCandidateBatchMember =
    ResolvedVampireCandidateBatchMember
        !PreparedVampireCandidateBatchMember
        !(Maybe
            (Either
                Provers.ProverProcessError
                Provers.ProverAnswer))

-- | Authorize one complete, source-ordered candidate stage whose members are
-- mutually independent and each require exactly one closed Vampire request.
-- Every member is prepared and validated against the same declaration
-- baseline.  Results are applied only after the complete live batch returns,
-- so no same-stage sibling can become authority for another member.
authorizeVampireCandidateBatch
    :: NonEmpty
        ( Location
        , ReservedCandidate
        , CandidateProof (PreparedVampireObligation Void ())
        )
    -> Declaration ()
authorizeVampireCandidateBatch inputs = Declaration do
    unprepared <- State.get
    baseline <-
        State.lift
            (Except.liftEither
                (prepareDeclarationClosure unprepared))
    let supplied =
            [ candidate
            | (_location, candidate, _prepare) <- NonEmpty.toList inputs
            ]
        frontier = declarationAuthorizationFrontier baseline
        expected =
            List.filter
                ((== CandidateStage frontier) . reservedStage)
                (Map.elems (declarationReservations baseline))
    traverse_
        (State.lift
            . Except.liftEither
            . validateReservedCandidate baseline)
        supplied
    traverse_
        (\candidate ->
            when
                (Map.member
                    (reservedCandidateSlot candidate)
                    (declarationPending baseline))
                (State.lift
                    (Except.throwError
                        (CandidateAlreadyAuthorized
                            (reservedCandidateSlot candidate)))))
        supplied
    unless (supplied == expected)
        (State.lift
            (Except.throwError
                (VampireCandidateBatchMismatch
                    (reservedCandidateSlot <$> expected)
                    (reservedCandidateSlot <$> supplied))))
    prepared <-
        State.lift
            (traverse
                (prepareVampireCandidateBatchMember baseline)
                inputs)
    State.lift
        (validateCachedVampireCandidateBatch
            (NonEmpty.toList prepared))
    let live =
            [ task
            | PreparedVampireCandidateBatchMember
                    _location _candidate task final <-
                        NonEmpty.toList prepared
            , isNothing (candidateProofCachedValidation final)
            ]
    liveResults <-
        case NonEmpty.nonEmpty live of
            Nothing -> pure []
            Just nonempty -> do
                let resolver =
                        declarationVampireResolver baseline
                results <-
                    liftIO
                        (resolveSynchronousVampireBatch resolver nonempty)
                State.lift
                    (Except.liftEither
                        (validateVampireResolverResultCount
                            (length live)
                            results))
    pending <-
        State.lift
            (completeVampireCandidateBatch
                (NonEmpty.toList prepared)
                liveResults)
    let withPending =
            baseline
                { declarationPending =
                    foldl'
                        (\entries item@(PendingCandidate candidate _ _) ->
                            Map.insert
                                (reservedCandidateSlot
                                    candidate)
                                item
                                entries)
                        (declarationPending baseline)
                        pending
                }
    State.put (advanceAuthorizationFrontier withPending)

prepareVampireCandidateBatchMember
    :: DeclarationState
    -> ( Location
       , ReservedCandidate
       , CandidateProof (PreparedVampireObligation Void ())
       )
    -> ExceptT DeclarationError IO PreparedVampireCandidateBatchMember
prepareVampireCandidateBatchMember
        baseline (location, candidate, prepare) = do
    initial <-
        Except.liftEither
            (initialCandidateProofState baseline candidate)
    cached <- selectProofCandidateValidation candidate initial
    let selected =
            initial{candidateProofCachedValidation = cached}
    (obligation, preparedState) <-
        State.runStateT
            (runCandidateProof
                (locateProofObligation location prepare))
            selected
    unless (null (acceptedRequestIds preparedState))
        (Except.throwError
            (VampireCandidateBatchProofShapeMismatch
                (reservedCandidateSlot candidate)))
    let PreparedVampireObligation expected task = obligation
    validated <-
        Except.withExceptT
            (ProofObligationFailedAt location)
            (validatePreparedVampireProblem
                expected task preparedState)
    pure
        (PreparedVampireCandidateBatchMember
            location candidate task validated)

completeVampireCandidateBatch
    :: [PreparedVampireCandidateBatchMember]
    -> [Either Provers.ProverProcessError Provers.ProverAnswer]
    -> ExceptT DeclarationError IO [PendingCandidate]
completeVampireCandidateBatch members liveResults = do
    resolved <-
        Except.liftEither
            (associateVampireCandidateBatchResults
                members liveResults)
    -- Integrity dominates ranked proof failure: validate every accepted run
    -- before inspecting any ordinary process or prover rejection.
    traverse_ validateAcceptedVampireBatchMember resolved
    traverse_ rejectOrdinaryVampireBatchMember resolved
    traverse completeVampireCandidateBatchMember resolved

validateCachedVampireCandidateBatch
    :: [PreparedVampireCandidateBatchMember]
    -> ExceptT DeclarationError IO ()
validateCachedVampireCandidateBatch =
    traverse_ \member ->
        when
            (preparedVampireCandidateBatchMemberIsCached member)
            (void
                (completeVampireCandidateBatchMember
                    (ResolvedVampireCandidateBatchMember member Nothing)))

associateVampireCandidateBatchResults
    :: [PreparedVampireCandidateBatchMember]
    -> [Either Provers.ProverProcessError Provers.ProverAnswer]
    -> Either
        DeclarationError
        [ResolvedVampireCandidateBatchMember]
associateVampireCandidateBatchResults members =
    go members
  where
    go [] [] = Right []
    go [] results =
        Left
            (VampireResolverBatchSizeMismatch
                0
                (length results))
    go (member : remaining) results
        | preparedVampireCandidateBatchMemberIsCached member =
                (ResolvedVampireCandidateBatchMember member Nothing :)
                    <$> go remaining results
        | otherwise =
            case results of
                [] ->
                    Left (VampireResolverBatchSizeMismatch 1 0)
                current : later ->
                    (ResolvedVampireCandidateBatchMember
                        member (Just current) :)
                        <$> go remaining later

preparedVampireCandidateBatchMemberIsCached
    :: PreparedVampireCandidateBatchMember
    -> Bool
preparedVampireCandidateBatchMemberIsCached
        (PreparedVampireCandidateBatchMember
            _location _candidate _task state) =
    isJust (candidateProofCachedValidation state)

validateAcceptedVampireBatchMember
    :: ResolvedVampireCandidateBatchMember
    -> ExceptT DeclarationError IO ()
validateAcceptedVampireBatchMember
        (ResolvedVampireCandidateBatchMember
            (PreparedVampireCandidateBatchMember
                location _candidate task _validated)
            result) =
    Except.withExceptT
        (ProofObligationFailedAt location)
        (validateAcceptedVampireResult task result)

rejectOrdinaryVampireBatchMember
    :: ResolvedVampireCandidateBatchMember
    -> ExceptT DeclarationError IO ()
rejectOrdinaryVampireBatchMember
        (ResolvedVampireCandidateBatchMember
            (PreparedVampireCandidateBatchMember
                location _candidate _task _validated)
            result) =
    traverse_
        (Except.throwError . ProofObligationFailedAt location)
        (result >>= vampireResultFailure)

completeVampireCandidateBatchMember
    :: ResolvedVampireCandidateBatchMember
    -> ExceptT DeclarationError IO PendingCandidate
completeVampireCandidateBatchMember
        (ResolvedVampireCandidateBatchMember
            (PreparedVampireCandidateBatchMember
                location candidate task validated)
            result) = do
    final <-
        Except.withExceptT
            (ProofObligationFailedAt location)
            (applyAcceptedVampireResult task result validated)
    completeCandidateWithValidation
        candidate
        (CheckedSourceProof (acceptedRequestIds final))
        (candidateProofSafety final)
        final

acceptVampireBatchMemberResult
    :: Provers.PreparedTypedProverTask
        SemanticFactOccurrenceFingerprint
        local
        origin
        ObjectId
    -> Maybe (Either Provers.ProverProcessError Provers.ProverAnswer)
    -> CandidateProofState
    -> ExceptT DeclarationError IO CandidateProofState
acceptVampireBatchMemberResult prepared result validated = do
    validateAcceptedVampireResult prepared result
    traverse_ Except.throwError (result >>= vampireResultFailure)
    applyAcceptedVampireResult prepared result validated

validateAcceptedVampireResult
    :: Provers.PreparedTypedProverTask
        SemanticFactOccurrenceFingerprint
        local
        origin
        ObjectId
    -> Maybe (Either Provers.ProverProcessError Provers.ProverAnswer)
    -> ExceptT DeclarationError IO ()
validateAcceptedVampireResult prepared result = do
    let request = Provers.preparedTypedProverRequest prepared
    traverse_
        (\resolved ->
            traverse_
                (\accepted ->
                    unless
                        (Provers.acceptedVampireRequestId accepted
                            == Provers.preparedVerificationRequestId request)
                        (Except.throwError VampireRequestMismatch))
                (either (const Nothing) Provers.provedVampireRun resolved))
        result

vampireResultFailure
    :: Either Provers.ProverProcessError Provers.ProverAnswer
    -> Maybe DeclarationError
vampireResultFailure = \case
    Left failure ->
        Just (VampireProcessFailed failure)
    Right answer ->
        case Provers.provedVampireRun answer of
            Nothing ->
                Just (VampireObligationRejected answer)
            Just _accepted ->
                Nothing

applyAcceptedVampireResult
    :: Provers.PreparedTypedProverTask
        SemanticFactOccurrenceFingerprint
        local
        origin
        ObjectId
    -> Maybe (Either Provers.ProverProcessError Provers.ProverAnswer)
    -> CandidateProofState
    -> ExceptT DeclarationError IO CandidateProofState
applyAcceptedVampireResult prepared result validated = do
    traverse_
        (\resolved ->
            case vampireResultFailure resolved of
                Just failure ->
                    Except.throwError failure
                Nothing ->
                    pure ())
        result
    let request = Provers.preparedTypedProverRequest prepared
        requestId = Provers.preparedVerificationRequestId request
    pure
        validated
            { candidateProofAcceptedRequestsReversed =
                requestId
                    : candidateProofAcceptedRequestsReversed validated
            }

selectProofCandidateValidation
    :: ReservedCandidate
    -> CandidateProofState
    -> ExceptT
        DeclarationError
        IO
        (Maybe Materialization.CandidateValidation)
selectProofCandidateValidation candidate initial =
    case declarationValidationMode
            (candidateProofDeclaration initial) of
        EnvironmentImportMode ->
            Except.throwError
                ProofValidationOutsideProofDeclaration
        ProofValidationMode{} -> do
            (syntax, cached) <-
                runDeclarationLookup
                    (lookupProofValidation candidate)
                    initial
            pure
                ((\record ->
                    Materialization.candidateProofValidation
                        record syntax)
                    <$> cached)
        DeclarationValidationMode{} ->
            pure (candidateProofCachedValidation initial)

completeCandidateWithValidation
    :: ReservedCandidate
    -> DirectAuthorization
    -> CandidateSafety
    -> CandidateProofState
    -> ExceptT DeclarationError IO PendingCandidate
completeCandidateWithValidation candidate direct safety final = do
    pending <-
        Except.liftEither
            (freshCompletion
                candidate
                direct
                safety
                final)
    traverse_
        (\validation ->
            case Materialization.checkCandidateValidation
                    (logicalBuilderTheory
                        (candidateProofBuilder final))
                    (logicalBuilderPrefix
                        (candidateProofBuilder final))
                    (candidateCheckedProposition candidate)
                    (validationTarget
                        (pendingCandidateCertificate pending))
                    direct
                    validation of
                Left failure ->
                    liftIO
                        (throwIO
                            (CachedValidationIntegrityError failure))
                Right () ->
                    pure ())
        (candidateProofCachedValidation final)
    pure pending

runDeclarationLookup
    :: Declaration value
    -> CandidateProofState
    -> ExceptT DeclarationError IO value
runDeclarationLookup action initial =
    fst
        <$> State.runStateT
            (runDeclaration action)
            (candidateProofDeclaration initial)

pendingCandidateCertificate :: PendingCandidate -> ValidationCertificate
pendingCandidateCertificate
        (PendingCandidate _ certificate _) =
    certificate

acceptedRequestIds :: CandidateProofState -> [PreparedRequestId]
acceptedRequestIds =
    reverse . candidateProofAcceptedRequestsReversed

freshCompletion
    :: ReservedCandidate
    -> DirectAuthorization
    -> CandidateSafety
    -> CandidateProofState
    -> Either DeclarationError PendingCandidate
freshCompletion candidate direct safety proofState = do
    let builder = candidateProofBuilder proofState
        declaration = candidateProofDeclaration proofState
        reference = candidateTheoremReference builder candidate
        authority = candidateFactAuthority reference safety
    void
        (first DeclarationPropositionValidationFailed
            (validateAssertedPropositionContent
                (candidateProofObjectClosure proofState)
                (checkedPropositionId
                    (candidateCheckedProposition candidate))
                (frozenCoreTerm
                    (checkedPropositionTerm
                        (candidateCheckedProposition candidate)))))
    certificate <-
        first ValidationCertificateFailed
            (validationCertificate authority direct)
    let authorization =
            PendingFactAuthorization
                (logicalBuilderIdentity builder)
                (logicalBuilderPrefix builder)
                (declarationInvocation declaration)
                (reservedCandidateSlot candidate)
                authority
                (reservedStage candidate)
    pure
        (PendingCandidate
            candidate
            certificate
            authorization)

authorizeOneCandidate
    :: ReservedCandidate
    -> (CandidateProofState
        -> ExceptT DeclarationError IO PendingCandidate)
    -> Declaration ()
authorizeOneCandidate candidate complete = Declaration do
    unprepared <- State.get
    state <-
        State.lift
            (Except.liftEither
                (prepareDeclarationClosure unprepared))
    State.lift
        (Except.liftEither
            (validateReservedCandidate state candidate))
    when
        (Map.member
            (reservedCandidateSlot candidate)
            (declarationPending state))
        (State.lift
            (Except.throwError
                (CandidateAlreadyAuthorized
                    (reservedCandidateSlot candidate))))
    unless
        (reservedStage candidate
            == CandidateStage
                (declarationAuthorizationFrontier state))
        (State.lift
            (Except.throwError
                (CandidateOutsideAuthorizationFrontier
                    (reservedCandidateSlot candidate)
                    (reservedCandidateStage candidate)
                    (declarationAuthorizationFrontier state))))
    initial <- State.lift
        (Except.liftEither
            (initialCandidateProofState state candidate))
    pending <- State.lift (complete initial)
    let state' =
            state
                { declarationPending =
                    Map.insert
                        (reservedCandidateSlot candidate)
                        pending
                        (declarationPending state)
                }
    State.put (advanceAuthorizationFrontier state')

advanceAuthorizationFrontier
    :: DeclarationState
    -> DeclarationState
advanceAuthorizationFrontier state
    | all stageCompleted currentCandidates =
        state
            { declarationAuthorizationFrontier =
                frontier + 1
            }
    | otherwise =
        state
  where
    frontier = declarationAuthorizationFrontier state
    currentCandidates =
        List.filter
            ((== CandidateStage frontier) . reservedStage)
            (Map.elems (declarationReservations state))
    stageCompleted candidate =
        Map.member
            (reservedCandidateSlot candidate)
            (declarationPending state)

initialCandidateProofState
    :: DeclarationState
    -> ReservedCandidate
    -> Either DeclarationError CandidateProofState
initialCandidateProofState declaration candidate = do
    closure <- declarationClosure declaration
    cached <-
        cachedDeclarationCandidateValidation declaration candidate
    pure CandidateProofState
        { candidateProofDeclaration = declaration
        , candidateProofObjectClosure = closure
        , candidateProofCandidate = candidate
        , candidateProofCachedValidation = cached
        , candidateProofPremisesReversed = []
        , candidateProofPremiseCount = 0
        , candidateProofSafety = initialCandidateSafety
        , candidateProofAcceptedRequestsReversed = []
        }

cachedDeclarationCandidateValidation
    :: DeclarationState
    -> ReservedCandidate
    -> Either
        DeclarationError
        (Maybe Materialization.CandidateValidation)
cachedDeclarationCandidateValidation declaration candidate =
    case declarationValidationSelection declaration of
        DeclarationValidationUnselected ->
            Right Nothing
        FreshDeclarationValidation ->
            Right Nothing
        CachedDeclarationValidation
                syntax objects theorems record ordinals ->
            maybe
                (Left
                    (CachedDeclarationCandidateMissing
                        (reservedCandidateSlot candidate)))
                (Right
                    . Just
                    . Materialization.candidateDeclarationValidation
                        record syntax objects theorems)
                (Map.lookup
                    (reservedCandidateSlot candidate)
                    ordinals)

reservedStage :: ReservedCandidate -> CandidateStage
reservedStage
        (ReservedCandidate _ _ _ stage _ _) =
    stage

validateReservedCandidate
    :: DeclarationState
    -> ReservedCandidate
    -> Either DeclarationError ()
validateReservedCandidate declaration candidate = do
    let builder = declarationBuilder declaration
        ReservedCandidate
            identity prefix invocation _stage slot _spec = candidate
    unless
        ( identity == logicalBuilderIdentity builder
          && prefix == logicalBuilderPrefix builder
          && invocation == declarationInvocation declaration
          && Map.lookup slot
                (declarationReservations declaration)
                == Just candidate
        )
        (Left (CandidateOutsideDeclaration slot))

instance Eq ReservedCandidate where
    left == right =
        reservedCandidateKey left == reservedCandidateKey right

reservedCandidateKey
    :: ReservedCandidate
    -> (BuilderIdentity, PrefixContextId, DeclarationInvocation, CandidateStage, FactSlot)
reservedCandidateKey
        (ReservedCandidate identity prefix invocation stage slot _spec) =
    (identity, prefix, invocation, stage, slot)


consumeBuilderAuthorizedFact
    :: FactEntry BuilderFactAuthorization
    -> CandidateProofState
    -> StateT
        CandidateProofState
        (ExceptT DeclarationError IO)
        CheckedPropositionContent
consumeBuilderAuthorizedFact
        (FactEntry proposition occurrence authorization)
        state = do
    let builder = candidateProofBuilder state
        BuilderFactAuthorization
            identity slot authority = authorization
    unless
        ( identity == logicalBuilderIdentity builder
          && slot == semanticFactSlot occurrence
          && authority == semanticFactAuthority occurrence
        )
        (State.lift
            (Except.throwError BuilderFactAuthorizationMismatch))
    accumulateAuthorizedSafety
        proposition
        authority
        state
    pure proposition

consumePendingFact
    :: PendingCandidate
    -> CandidateProofState
    -> StateT
        CandidateProofState
        (ExceptT DeclarationError IO)
        CheckedPropositionContent
consumePendingFact
        (PendingCandidate premise certificate authorization)
        state = do
    let builder = candidateProofBuilder state
        declaration = candidateProofDeclaration state
        PendingFactAuthorization
            identity prefix invocation slot authority
            premiseStageValue = authorization
        current = candidateProofCandidate state
    unless
        ( identity == logicalBuilderIdentity builder
          && prefix == logicalBuilderPrefix builder
          && invocation == declarationInvocation declaration
          && slot == reservedCandidateSlot premise
          && authority == validationTarget certificate
          && premiseStageValue == reservedStage premise
        )
        (State.lift
            (Except.throwError PendingFactAuthorizationMismatch))
    unless
        (reservedStage premise < reservedStage current)
        (State.lift
            (Except.throwError
                (StagedPremiseNotEarlier
                    (reservedCandidateSlot premise)
                    (reservedCandidateStage premise)
                    (reservedCandidateSlot current)
                    (reservedCandidateStage current))))
    let proposition = candidateCheckedProposition premise
    accumulateAuthorizedSafety
        proposition
        authority
        state
    pure proposition

accumulateAuthorizedSafety
    :: CheckedPropositionContent
    -> FactAuthority
    -> CandidateProofState
    -> StateT
        CandidateProofState
        (ExceptT DeclarationError IO)
        ()
accumulateAuthorizedSafety proposition authority state = do
    let expected =
            theoremRef
                (logicalBuilderTheory
                    (candidateProofBuilder state))
                (checkedPropositionId proposition)
    safety <-
        State.lift
            (Except.liftEither
                (first FactSafetyFailed
                    (accumulateFactSafety
                        expected
                        authority
                        (candidateProofSafety state))))
    State.put state{candidateProofSafety = safety}

registerKernelImport
    :: CheckedPropositionContent
    -> CandidateProof ImportIx
registerKernelImport proposition = CandidateProof do
    state <- State.get
    appendCandidatePremise proposition state

appendCandidatePremise
    :: CheckedPropositionContent
    -> CandidateProofState
    -> StateT
        CandidateProofState
        (ExceptT DeclarationError IO)
        ImportIx
appendCandidatePremise proposition state = do
    let index = candidateProofPremiseCount state
    State.put
        state
            { candidateProofPremisesReversed =
                CandidatePremise proposition
                    : candidateProofPremisesReversed state
            , candidateProofPremiseCount = index + 1
            }
    pure (importIx index)

findPendingByFingerprint
    :: SemanticFactOccurrenceFingerprint
    -> Map FactSlot PendingCandidate
    -> Maybe PendingCandidate
findPendingByFingerprint fingerprint =
    find
        (\(PendingCandidate candidate certificate _authorization) ->
            semanticFactOccurrenceFingerprint
                (reservedCandidateSlot candidate)
                (validationTarget certificate)
                == fingerprint)
        . Map.elems

candidateImportJudgments
    :: CandidateProofState
    -> Either DeclarationError (Vector (DerivationImportJudgment ObjectId))
candidateImportJudgments state =
    Vector.fromList
        <$> traverse
            (\(CandidatePremise proposition) ->
                first DerivationImportFailed
                    (derivationImportJudgment
                        (checkedPropositionTerm proposition)))
            (reverse
                (candidateProofPremisesReversed state))

replayCandidateKernel
    :: CheckedPropositionContent
    -> KernelDerivation ObjectId
    -> CandidateProofState
    -> Either
        DeclarationError
        (ReplayedKernelDerivation ObjectId)
replayCandidateKernel proposition derivation state = do
    imports <- candidateImportJudgments state
    let builder = candidateProofBuilder state
        closure = candidateProofObjectClosure state
    first KernelCompletionFailed
        (replayKernelDerivation
            (logicalBuilderFoundation builder)
            defaultKernelReplayLimits
            (`lookupCheckedObjectType` closure)
            imports
            (checkedPropositionTerm proposition)
            derivation)

validateKernelConstruction
    :: KernelConstructionDescriptor
    -> CheckedPropositionContent
    -> ReplayedKernelDerivation ObjectId
    -> CandidateProofState
    -> Either DeclarationError ()
validateKernelConstruction descriptor proposition replayed proofState =
    unless matches
        (Left KernelConstructionDescriptorMismatch)
  where
    builder = candidateProofBuilder proofState
    noImports = Set.null (replayedKernelImportUses replayed)
    noFoundation = Set.null (replayedKernelFoundationUses replayed)
    noRules = Set.null (replayedKernelRuleUses replayed)

    matches =
        case descriptor of
            FoundationLeaf tag ->
                noImports
                    && replayedKernelFoundationUses replayed
                        == Set.singleton tag
                    && noRules
                    && checkedPropositionTerm proposition
                        == mapFrozenGlobals
                            absurd
                            (foundationAxiomFrozen
                                (logicalBuilderFoundation builder)
                                tag)
            GuardedFoundationRules rules ->
                replayedKernelRuleUses replayed
                    == guardedRuleTags rules
            CheckedDefinitionEquation identity ->
                noImports
                    && noFoundation
                    && noRules
                    && matchesDefinitionEquation identity proposition proofState

matchesDefinitionEquation
    :: ObjectId
    -> CheckedPropositionContent
    -> CandidateProofState
    -> Bool
matchesDefinitionEquation identity proposition proofState =
    case lookupCheckedObjectContent
            identity
            (candidateProofObjectClosure proofState) of
        Just
                (TransparentObjectContent
                    contentTheory coreType body) ->
            contentTheory
                == logicalBuilderTheory
                    (candidateProofBuilder proofState)
                && frozenCoreTerm (checkedPropositionTerm proposition)
                    `elem` definitionEquationTargets identity coreType body
        _ ->
            False

definitionEquationTargets
    :: ObjectId
    -> CoreType
    -> CanonicalTerm ObjectId
    -> [CanonicalTerm ObjectId]
definitionEquationTargets identity coreType body =
    CEq coreType (CGlobal identity) body
        : case (coreType, body) of
            (TyArrow TySet TyProp, CLam TySet predicate) ->
                [ CForall TySet
                    (CEq TyProp
                        (CApp (CGlobal identity) (CBound 0))
                        predicate)
                ]
            _ -> []


validateCandidateVampireProblem
    :: Provers.PreparedTypedProverTask
        SemanticFactOccurrenceFingerprint
        Void
        origin
        ObjectId
    -> CandidateProofState
    -> ExceptT DeclarationError IO CandidateProofState
validateCandidateVampireProblem prepared initial = do
    let problem = Provers.preparedTypedProverLogicalProblem prepared
        claim = Backend.typedProblemClaim problem
        target = candidateCheckedProposition
            (candidateProofCandidate initial)
    Except.liftEither do
        unless
            ( Vector.null (Backend.supportedPropositionSupport claim)
              && Backend.supportedPropositionTerm claim
                    == frozenCoreTerm (checkedPropositionTerm target)
            )
            (Left VampireTargetMismatch)
        unless
            (Vector.null (Backend.typedProblemLocalPremises problem))
            (Left VampireLocalPremisesNotSupported)
    validateVampireProblemEnvironment prepared initial

validatePreparedVampireProblem
    :: (Eq local, Eq origin)
    => Backend.TypedProblem
        SemanticFactOccurrenceFingerprint
        local
        origin
        ObjectId
    -> Provers.PreparedTypedProverTask
        SemanticFactOccurrenceFingerprint
        local
        origin
        ObjectId
    -> CandidateProofState
    -> ExceptT DeclarationError IO CandidateProofState
validatePreparedVampireProblem expectedProblem prepared initial = do
    let problem = Provers.preparedTypedProverLogicalProblem prepared
    Except.liftEither
        (unless (problem == expectedProblem)
            (Left VampireTargetMismatch)
        )
    validateVampireProblemEnvironment prepared initial

validateVampireProblemEnvironment
    :: Provers.PreparedTypedProverTask
        SemanticFactOccurrenceFingerprint
        local
        origin
        ObjectId
    -> CandidateProofState
    -> ExceptT DeclarationError IO CandidateProofState
validateVampireProblemEnvironment prepared initial = do
    let problem = Provers.preparedTypedProverLogicalProblem prepared
        builder = candidateProofBuilder initial
        closure = candidateProofObjectClosure initial
    Except.liftEither do
        traverse_
            (\(identity, reportedType) ->
                unless
                    (lookupCheckedObjectType identity closure
                        == Just reportedType)
                    (Left (VampireGlobalTypeMismatch identity)))
            (Map.toList (Backend.typedProblemGlobalTypes problem))
        traverse_
            (validateFoundationAuxiliary builder)
            (Backend.typedProblemAuxiliaries problem)
    execCandidateProof initial do
        traverse_
            validatePremise
            (Backend.typedProblemGlobalPremises problem)
  where
    validatePremise selected = do
        let fingerprint = Backend.typedBackendFactReference selected
        proposition <- consumeAuthorizedFact fingerprint
        state <- CandidateProof State.get
        unless
            ( Backend.supportedPropositionTerm
                (Backend.typedBackendFactProposition selected)
                == frozenCoreTerm
                    (checkedPropositionTerm proposition)
            )
            (failCandidateProof
                (VampirePremiseMismatch fingerprint))
        let closure =
                candidateProofObjectClosure state
        supported <-
            either
                (const
                    (failCandidateProof
                        (VampirePremiseCapabilityMismatch
                            fingerprint)))
                pure
                (Backend.supportedProposition
                    Vector.empty
                    (embedClosedCore
                        []
                        (checkedPropositionTerm proposition)))
        capability <-
            either
                (const
                    (failCandidateProof
                        (VampirePremiseCapabilityMismatch
                            fingerprint)))
                pure
                (Backend.classifySupportedProposition
                    (`lookupCheckedObjectType` closure)
                    supported)
        unless
            (capability
                == Backend.typedBackendFactCapability selected)
            (failCandidateProof
                (VampirePremiseCapabilityMismatch fingerprint))

    validateFoundationAuxiliary builder auxiliary = do
        let tag = Backend.typedProblemAuxiliaryTag auxiliary
            actual =
                Backend.supportedPropositionTerm
                    (Backend.typedProblemAuxiliaryProposition auxiliary)
            expectedTerm =
                frozenCoreTerm
                    (mapFrozenGlobals
                        absurd
                        (foundationAxiomFrozen
                            (logicalBuilderFoundation builder)
                            tag))
        unless (actual == expectedTerm)
            (Left (VampireFoundationMismatch tag))

execCandidateProof
    :: CandidateProofState
    -> CandidateProof value
    -> ExceptT DeclarationError IO CandidateProofState
execCandidateProof initial action =
    snd <$> State.runStateT (runCandidateProof action) initial

failCandidateProof
    :: DeclarationError
    -> CandidateProof value
failCandidateProof =
    CandidateProof . State.lift . Except.throwError

data ValidationMode
    = EnvironmentImportMode
    | ProofValidationMode !ProofSyntaxId
    | DeclarationValidationMode !DeclarationSyntaxId

data PlannedVampireDisposition
    = PlannedCachedRequest !Provers.PreparedVerificationRequest
    | PlannedLiveRequest
        !Provers.PreparedVerificationRequest
        !Provers.VampireHandle
    | PlannedSynchronousRequest !Provers.PreparedVerificationRequest

data PlannedCandidate = PlannedCandidate
    !ReservedCandidate
    !FactAuthority
    !DirectAuthorization
    ![PlannedVampireDisposition]

data PlannedReplayRequest
    = ReplayLive
        !Provers.PreparedVerificationRequest
        !Provers.VampireHandle
    | ReplaySynchronous !Provers.PreparedVerificationRequest

data PlannedValidationSelection
    = PlannedFreshValidation
    | PlannedProofValidation
        !ProofValidationKey
        !ProofValidationRecord
    | PlannedCompiledValidation
        !DeclarationValidationKey
        !DeclarationValidationRecord

-- | One completely lowered and submitted declaration.  It carries no
-- builder authorization or materialized certificate; all authority is
-- reconstructed by the source-ordered admission cursor.
data PlannedDeclaration body = PlannedDeclaration
    !(CheckedDeclaration body)
    !PrefixContextId
    !PrefixContextId
    !DeclarationInterfaceDelta
    ![AssertedObject]
    ![CheckedPropositionContent]
    ![NonEmpty PlannedCandidate]
    !PlannedValidationSelection

plannedDeclarationPreviousPrefix
    :: PlannedDeclaration body
    -> PrefixContextId
plannedDeclarationPreviousPrefix
        (PlannedDeclaration _checked previous _next _delta
            _objects _propositions _candidates _validation) =
    previous

plannedDeclarationNextPrefix
    :: PlannedDeclaration body
    -> PrefixContextId
plannedDeclarationNextPrefix
        (PlannedDeclaration _checked _previous next _delta
            _objects _propositions _candidates _validation) =
    next

plannedDeclarationDelta
    :: PlannedDeclaration body
    -> DeclarationInterfaceDelta
plannedDeclarationDelta
        (PlannedDeclaration _checked _previous _next delta
            _objects _propositions _candidates _validation) =
    delta

newtype PlanningIntegrityError = PlanningIntegrityError Text
    deriving stock (Show)

instance Exception.Exception PlanningIntegrityError

-- | Advance the authority-free semantic projection through one complete
-- checked declaration.  Validation selection and every deterministic check
-- finish before the first live request is submitted.
planCheckedDeclaration
    :: CheckedDeclaration body
    -> LoweringDriver (Either DeclarationError (PlannedDeclaration body))
planCheckedDeclaration checked@(CheckedDeclaration
        mode objects explicitPropositions globals descriptors stages
        _body) = LoweringDriver do
    state@(LoweringState resolver (ProspectiveBuilder builder) validationRun) <-
        State.get
    prepared <- liftIO (Except.runExceptT do
        closure <-
            Except.liftEither
                (first DeclarationObjectValidationFailed
                    (extendObjectClosure
                        (logicalBuilderObjectClosure builder)
                        objects))
        let reservedStages =
                reservePlanningStages builder stages
        plannedWithoutDisposition <-
            Except.liftEither
                (preparePlannedCandidates builder closure reservedStages)
        let orderedCandidates = fmap (fmap fst) plannedWithoutDisposition
            occurrences =
                [ candidateOccurrence reserved authority
                | stage <- plannedWithoutDisposition
                , (PlannedCandidate reserved authority _direct _requests,
                    _requestValues) <- toList stage
                ]
            aliases =
                [ semanticAlias alias
                    (semanticFactFingerprint
                        (candidateOccurrence reserved authority))
                | stage <- plannedWithoutDisposition
                , (PlannedCandidate reserved authority _direct _requests,
                    _requestValues) <- toList stage
                , alias <- candidateAliases reserved
                ]
            allCandidatePropositions =
                candidateCheckedProposition . fst
                    <$> concatMap toList reservedStages
            propositions =
                stableUniqueBy checkedPropositionId
                    (explicitPropositions <> allCandidatePropositions)
            objectIds = assertedObjectId <$> objects
            propositionIds = checkedPropositionId <$> propositions
            ownSlot = declarationSlot
                (logicalBuilderOwner builder)
                (localDeclarationOrdinal
                    (logicalBuilderNextDeclaration builder))
        traverse_
            (\proposition ->
                void
                    (Except.liftEither
                        (first DeclarationPropositionValidationFailed
                            (validateAssertedPropositionContent
                                closure
                                (checkedPropositionId proposition)
                                (frozenCoreTerm
                                    (checkedPropositionTerm proposition))))))
            propositions
        (resolvedStructures, delta, next) <-
            Except.liftEither
                (buildCheckedDeclarationDelta
                    builder closure ownSlot occurrences aliases objectIds
                    propositionIds (reverse globals) (reverse descriptors))
        selection <-
            selectPlannedValidation
                validationRun mode builder objects orderedCandidates
        planned <-
            submitPlannedCandidates resolver selection
                plannedWithoutDisposition
        let nextBuilder =
                appendProspectiveBuilder
                    closure resolvedStructures delta next planned builder
            declaration =
                PlannedDeclaration checked
                    (logicalBuilderPrefix builder)
                    next delta objects propositions planned selection
        pure (declaration, nextBuilder))
    case prepared of
        Left failure -> pure (Left failure)
        Right (declaration, nextBuilder) -> do
            let LoweringState currentResolver _current currentValidation = state
            State.put
                (LoweringState
                    currentResolver
                    (ProspectiveBuilder nextBuilder)
                    currentValidation)
            pure (Right declaration)

reservePlanningStages
    :: BuilderState PlanningEvidence
    -> [NonEmpty CheckedCandidate]
    -> [NonEmpty (ReservedCandidate, CandidatePlanningSpec)]
reservePlanningStages builder =
    snd . mapAccumPlanning reserveStage (logicalBuilderNextFact builder)
  where
    invocation = DeclarationInvocation (logicalBuilderNextInvocation builder)
    reserveStage nextFact (stageIndex, specs) =
        let candidates =
                NonEmpty.zipWith
                    (\offset (CheckedCandidate spec planning) ->
                        ( ReservedCandidate
                            (logicalBuilderIdentity builder)
                            (logicalBuilderPrefix builder)
                            invocation
                            (CandidateStage stageIndex)
                            (factSlot
                                (logicalBuilderOwner builder)
                                (localFactOrdinal (nextFact + offset)))
                            spec
                        , planning
                        ))
                    (0 :| [1..])
                    specs
        in ( nextFact + fromIntegral (NonEmpty.length specs)
           , candidates
           )

    mapAccumPlanning action initial values =
        go initial (zip [0..] values)
      where
        go accumulator [] = (accumulator, [])
        go accumulator (value : remaining) =
            let (next, result) = action accumulator value
                (final, results) = go next remaining
            in (final, result : results)

preparePlannedCandidates
    :: BuilderState PlanningEvidence
    -> CheckedObjectClosure
    -> [NonEmpty (ReservedCandidate, CandidatePlanningSpec)]
    -> Either
        DeclarationError
        [NonEmpty (PlannedCandidate, [CheckedPlannedVampireRequest])]
preparePlannedCandidates builder closure stages =
    snd <$> mapAccumM prepareStage Map.empty (zip [0..] stages)
  where
    prepareStage earlier (stageIndex, stage) = do
        (sameStage, planned) <-
            mapAccumM
                (prepareCandidate stageIndex earlier)
                Map.empty
                (zip [0..] (toList stage))
        pure (Map.union earlier sameStage, NonEmpty.fromList planned)

    prepareCandidate stageIndex earlier sameStage
            (candidateIndex, (candidate, contract)) = do
        let position = PlannedCandidatePosition stageIndex candidateIndex
        (direct, safety, requests) <-
            prepareCandidatePlanningContract
                builder closure earlier position candidate contract
        let authority =
                candidateFactAuthority
                    (candidateTheoremReference builder candidate)
                    safety
            planned = PlannedCandidate candidate authority direct []
        pure
            ( Map.insert position (candidate, authority) sameStage
            , (planned, requests)
            )

    mapAccumM action initial values =
        go initial [] values
      where
        go accumulator outputs = \case
            [] -> pure (accumulator, reverse outputs)
            value : remaining -> do
                (next, output) <- action accumulator value
                go next (output : outputs) remaining

prepareCandidatePlanningContract
    :: BuilderState PlanningEvidence
    -> CheckedObjectClosure
    -> Map PlannedCandidatePosition (ReservedCandidate, FactAuthority)
    -> PlannedCandidatePosition
    -> ReservedCandidate
    -> CandidatePlanningSpec
    -> Either
        DeclarationError
        ( DirectAuthorization
        , CandidateSafety
        , [CheckedPlannedVampireRequest]
        )
prepareCandidatePlanningContract builder closure earlier current candidate
        (CandidatePlanningSpec direct extraFacts staged requests) = do
    safetyWithFacts <-
        foldM (accumulatePlanningFact builder closure)
            initialCandidateSafety
            (stableUniqueBy id
                ( extraFacts
                    <> concatMap requestFacts requests
                ))
    safetyWithStages <-
        foldM consumeStage safetyWithFacts staged
    let safety = case direct of
            PlanningSourceAxiom ->
                addCandidateEscape SourceAxiom safetyWithStages
            PlanningOmitted ->
                addCandidateEscape Omitted safetyWithStages
            _ -> safetyWithStages
        requestIds = requestIdentity <$> requests
        directAuthorization = case direct of
            PlanningDefinitionEquation identity ->
                CheckedKernelConstruction
                    (CheckedDefinitionEquation identity)
            PlanningSourceAxiom -> SourceAxiomAuthorization
            PlanningTrustedDatatype descriptor ->
                TrustedCompilation (DatatypeCompilation descriptor)
            PlanningKernelConstruction descriptor ->
                CheckedKernelConstruction descriptor
            PlanningCheckedSourceProof ->
                CheckedSourceProof requestIds
            PlanningOmitted -> OmittedAuthorization
    validatePlanningDirect directAuthorization safety
    pure (directAuthorization, safety, requests)
  where
    requestFacts
            (CheckedPlannedVampireRequest _location _request facts) = facts
    requestIdentity
            (CheckedPlannedVampireRequest _location request _facts) =
        Provers.preparedVerificationRequestId request

    consumeStage safety position = do
        (premise, authority) <-
            maybe
                (Left
                    (PlanningFactContractMismatch
                        (reservedCandidateSlot candidate)))
                Right
                (Map.lookup position earlier)
        let PlannedCandidatePosition premiseStage _premiseIndex = position
            PlannedCandidatePosition currentStage _currentIndex = current
        unless (premiseStage < currentStage)
            (Left
                (StagedPremiseNotEarlier
                    (reservedCandidateSlot premise)
                    premiseStage
                    (reservedCandidateSlot candidate)
                    currentStage))
        first FactSafetyFailed
            (accumulateFactSafety
                (candidateTheoremReference builder premise)
                authority
                safety)

accumulatePlanningFact
    :: BuilderState PlanningEvidence
    -> CheckedObjectClosure
    -> CandidateSafety
    -> SemanticFactOccurrenceFingerprint
    -> Either DeclarationError CandidateSafety
accumulatePlanningFact builder closure safety fingerprint = do
    FactEntry proposition occurrence (PlanningEvidence authority _provenance) <-
        maybe
            (Left (AuthorizedFactNotVisible fingerprint))
            Right
            (Map.lookup fingerprint (logicalBuilderFacts builder))
    unless
        ( semanticFactFingerprint occurrence == fingerprint
          && semanticFactAuthority occurrence == authority
          && propositionMatchesClosure closure proposition
        )
        (Left (PlanningFactContractMismatch (semanticFactSlot occurrence)))
    first FactSafetyFailed
        (accumulateFactSafety
            (theoremRef
                (logicalBuilderTheory builder)
                (checkedPropositionId proposition))
            authority
            safety)

validatePlanningDirect
    :: DirectAuthorization
    -> CandidateSafety
    -> Either DeclarationError ()
validatePlanningDirect direct safety =
    case direct of
        SourceAxiomAuthorization ->
            unless
                (candidateSafetyAuthority safety
                    == authoritySafety (singletonEscapeKind SourceAxiom))
                (Left
                    (ValidationCertificateFailed
                        (SourceAxiomSafetyMismatch
                            (candidateSafetyAuthority safety))))
        OmittedAuthorization ->
            unless
                (Omitted `elem` escapeKindsToList
                    (authoritySafetyEscapeKinds
                        (candidateSafetyAuthority safety)))
                (Left
                    (ValidationCertificateFailed
                        (OmittedSafetyMissing
                            (candidateSafetyAuthority safety))))
        _ -> pure ()

selectPlannedValidation
    :: ValidationRun
    -> CheckedDeclarationMode
    -> BuilderState PlanningEvidence
    -> [AssertedObject]
    -> [NonEmpty PlannedCandidate]
    -> ExceptT DeclarationError IO PlannedValidationSelection
selectPlannedValidation validationRun mode builder objects stages =
    case mode of
        CheckedProofMode syntax ->
            case concatMap toList stages of
                [planned@(PlannedCandidate _candidate authority _direct _)] -> do
                    let key = proofValidationKey
                            (theoremId (factAuthorityTheorem authority))
                            syntax
                            (logicalBuilderPrefix builder)
                    cached <- case validationRun of
                        FreshValidation -> pure Nothing
                        WarmValidation (ValidationLookup lookupProof _) ->
                            liftIO (lookupProof key)
                    traverse_
                        (validateProof planned syntax)
                        cached
                    pure case cached of
                        Nothing -> PlannedFreshValidation
                        Just record -> PlannedProofValidation key record
                candidates ->
                    Except.throwError
                        (CheckedProofCandidateCountMismatch
                            (length candidates))
        CheckedCompiledMode syntax -> do
            let planned = concatMap toList stages
                objectIds = assertedObjectId <$> objects
                theorems =
                    theoremId . factAuthorityTheorem . plannedAuthority
                        <$> planned
                key = declarationValidationKey syntax
                    (logicalBuilderPrefix builder) objectIds theorems
            cached <- case validationRun of
                FreshValidation -> pure Nothing
                WarmValidation (ValidationLookup _ lookupDeclaration) ->
                    liftIO (lookupDeclaration key)
            traverse_
                (validateCompiled planned syntax objectIds theorems)
                cached
            pure case cached of
                Nothing -> PlannedFreshValidation
                Just record -> PlannedCompiledValidation key record
  where
    plannedAuthority (PlannedCandidate _ authority _ _) = authority

    validateProof
            (PlannedCandidate candidate authority direct _)
            syntax record =
        case Materialization.checkCandidateValidation
                (logicalBuilderTheory builder)
                (logicalBuilderPrefix builder)
                (candidateCheckedProposition candidate)
                authority direct
                (Materialization.candidateProofValidation record syntax) of
            Left failure ->
                liftIO
                    (throwIO (CachedValidationIntegrityError failure))
            Right () -> pure ()

    validateCompiled planned syntax objectIds theorems record = do
        case Materialization.checkDeclarationValidationRecord
                (logicalBuilderPrefix builder)
                syntax objectIds theorems record of
            Left failure ->
                liftIO
                    (throwIO (CachedValidationIntegrityError failure))
            Right () -> pure ()
        traverse_
            (\(ordinal,
                PlannedCandidate candidate authority direct _) ->
                case Materialization.checkCandidateValidation
                        (logicalBuilderTheory builder)
                        (logicalBuilderPrefix builder)
                        (candidateCheckedProposition candidate)
                        authority direct
                        (Materialization.candidateDeclarationValidation
                            record syntax objectIds theorems ordinal) of
                    Left failure ->
                        liftIO
                            (throwIO
                                (CachedValidationIntegrityError failure))
                    Right () -> pure ())
            (zip [0..] planned)

submitPlannedCandidates
    :: VampireResolver
    -> PlannedValidationSelection
    -> [NonEmpty (PlannedCandidate, [CheckedPlannedVampireRequest])]
    -> ExceptT DeclarationError IO [NonEmpty PlannedCandidate]
submitPlannedCandidates resolver selection candidates
    | cached =
        pure (fmap (fmap cachedCandidate) candidates)
    | otherwise = do
        let requests =
                [ request
                | stage <- candidates
                , (_candidate, plannedRequests) <- toList stage
                , CheckedPlannedVampireRequest
                    _location request _facts <- plannedRequests
                ]
        case resolver of
            VampireResolver SynchronousVampireResolution{} _observe ->
                pure (fmap (fmap synchronousCandidate) candidates)
            VampireResolver
                    (AsynchronousVampireSubmission submit) _observe -> do
                handles <- case NonEmpty.nonEmpty requests of
                    Nothing -> pure []
                    Just nonempty -> do
                        submitted <- liftIO (submit nonempty)
                        unless
                            (NonEmpty.length submitted == length requests)
                            (Except.throwError
                                (VampireResolverBatchSizeMismatch
                                    (length requests)
                                    (NonEmpty.length submitted)))
                        pure (toList submitted)
                let (planned, remaining) =
                        State.runState
                            (traverse (traverse liveCandidate) candidates)
                            handles
                unless (null remaining)
                    (Except.throwError
                        (VampireResolverBatchSizeMismatch
                            (length requests)
                            (length requests + length remaining)))
                pure planned
  where
    cached = case selection of
        PlannedFreshValidation -> False
        PlannedProofValidation{} -> True
        PlannedCompiledValidation{} -> True

    cachedCandidate
            (PlannedCandidate candidate authority direct _dispositions,
             requests) =
        PlannedCandidate candidate authority direct
            [ PlannedCachedRequest request
            | CheckedPlannedVampireRequest
                _location request _facts <- requests
            ]

    liveCandidate
            (PlannedCandidate candidate authority direct _dispositions,
             requests) = do
        dispositions <- traverse takeHandle requests
        pure (PlannedCandidate candidate authority direct dispositions)

    synchronousCandidate
            (PlannedCandidate candidate authority direct _dispositions,
             requests) =
        PlannedCandidate candidate authority direct
            [ PlannedSynchronousRequest request
            | CheckedPlannedVampireRequest
                _location request _facts <- requests
            ]

    takeHandle
            (CheckedPlannedVampireRequest _location request _facts) = do
        remaining <- State.get
        case remaining of
            [] ->
                impossible
                    "validated prospective handle count became exhausted"
            handle : later -> do
                State.put later
                pure (PlannedLiveRequest request handle)

appendProspectiveBuilder
    :: CheckedObjectClosure
    -> Map SemanticStructurePhrase ResolvedStructure
    -> DeclarationInterfaceDelta
    -> PrefixContextId
    -> [NonEmpty PlannedCandidate]
    -> BuilderState PlanningEvidence
    -> BuilderState PlanningEvidence
appendProspectiveBuilder closure structures delta next planned builder =
    builder
        { logicalBuilderPrefix = next
        , logicalBuilderObjectClosure = closure
        , logicalBuilderFacts =
            foldl' insertPlanningFact
                (logicalBuilderFacts builder)
                (concatMap toList planned)
        , logicalBuilderAliases =
            foldl'
                (\entries alias ->
                    Map.insert
                        (semanticAliasName alias)
                        (ImportedAliasBinding
                            (semanticAliasTarget alias)
                            (ImportedAliasOrigin
                                (declarationDeltaSlot delta)
                                (semanticAliasTarget alias)))
                        entries)
                (logicalBuilderAliases builder)
                (declarationDeltaAliases delta)
        , logicalBuilderGlobals =
            foldl'
                (\entries binding ->
                    Map.insert
                        (semanticGlobalBindingKey binding)
                        (semanticGlobalBindingTarget binding)
                        entries)
                (logicalBuilderGlobals builder)
                (semanticEnvironmentBindings
                    (declarationDeltaEnvironment delta))
        , logicalBuilderStructures = structures
        , logicalBuilderDeltas = delta : logicalBuilderDeltas builder
        , logicalBuilderNextDeclaration =
            logicalBuilderNextDeclaration builder + 1
        , logicalBuilderNextFact =
            logicalBuilderNextFact builder
                + fromIntegral (sum (fmap NonEmpty.length planned))
        , logicalBuilderNextInvocation =
            logicalBuilderNextInvocation builder + 1
        }
  where
    insertPlanningFact entries
            (PlannedCandidate candidate authority _direct _requests) =
        let occurrence = candidateOccurrence candidate authority
            fingerprint = semanticFactFingerprint occurrence
            evidence = PlanningEvidence authority
                (Just
                    (PlanningProvenance
                        (declarationDeltaSlot delta)
                        (reservedStageValue candidate)
                        (reservedCandidateSlot candidate)))
        in Map.insert fingerprint
            (FactEntry
                (candidateCheckedProposition candidate)
                occurrence
                evidence)
            entries

    -- Keep the constructor match private while storing exact stage provenance.
    reservedStageValue
            (ReservedCandidate _identity _prefix _invocation stage _slot _spec) =
        stage

-- | Admit one checked declaration through the existing authoritative
-- source-order cursor.  The callback interprets a closed family recipe over
-- freshly reserved stage slots; it is not retained in the checked value.
admitCheckedDeclaration
    :: CheckedDeclaration body
    -> (body -> [NonEmpty ReservedCandidate] -> Declaration ())
    -> ModuleDriver failure CommittedDeclarationBatch
admitCheckedDeclaration
        (CheckedDeclaration
            mode objects propositions globals structures stages body)
        authorize =
    snd <$> do
        case mode of
            CheckedProofMode syntax ->
                commitProofDeclaration syntax do
                    reserved <- installCheckedStructure
                    authorize body reserved
            CheckedCompiledMode syntax ->
                commitCompiledDeclaration syntax do
                    reserved <- installCheckedStructure
                    authorizeCompiledDeclaration
                        (authorize body reserved)
  where
    installCheckedStructure = do
        traverse_ addDeclarationObject objects
        traverse_ addDeclarationProposition propositions
        traverse_
            (\binding ->
                stageSemanticGlobalBinding
                    (semanticGlobalBindingKey binding)
                    (semanticGlobalBindingTarget binding))
            globals
        traverse_ stageSemanticStructureDescriptor structures
        traverse
            (reserveCandidateBatch . fmap checkedCandidateSemanticSpec)
            stages

    checkedCandidateSemanticSpec
            (CheckedCandidate spec _planning) = spec

-- | Admit one retained plan against the real authorized builder.  The family
-- callback performs the existing authority checks, but every live resolver
-- result comes from the handle submitted during planning and every validation
-- lookup is the inert selection retained by the plan.
admitPlannedCheckedDeclaration
    :: PlannedDeclaration body
    -> (body -> [NonEmpty ReservedCandidate] -> Declaration ())
    -> ModuleDriver failure CommittedDeclarationBatch
admitPlannedCheckedDeclaration planned@(PlannedDeclaration
        checked previous _expectedNext _expectedDelta _objects _propositions
        candidates selection) authorize = ModuleDriver do
    DriverState originalResolver builder prefix originalValidation <-
        State.get
    unless (logicalBuilderPrefix builder == previous)
        (liftIO
            (throwIO
                (PlanningIntegrityError
                    "planned declaration predecessor does not match the admitted builder")))
    liveRef <- liftIO
        (newIORef
            [ replay
            | stage <- candidates
            , PlannedCandidate _candidate _authority _direct dispositions <-
                toList stage
            , disposition <- dispositions
            , replay <- case disposition of
                PlannedCachedRequest{} -> []
                PlannedLiveRequest request handle ->
                    [ReplayLive request handle]
                PlannedSynchronousRequest request ->
                    [ReplaySynchronous request]
            ])
    replay <- liftIO (plannedReplayResolver originalResolver liveRef)
    let validation = plannedAdmissionValidation selection
    State.put (DriverState replay builder prefix validation)
    batch <- runDriverStep (admitCheckedDeclaration checked authorize)
    remaining <- liftIO (readIORef liveRef)
    unless (null remaining)
        (liftIO
            (throwIO
                (PlanningIntegrityError
                    "admission did not consume every planned live request")))
    liftIO (validateAdmittedPlan planned batch)
    DriverState _replay admittedBuilder admittedPrefix _plannedValidation <-
        State.get
    State.put
        (DriverState
            originalResolver admittedBuilder admittedPrefix originalValidation)
    pure batch

plannedReplayResolver
    :: VampireResolver
    -> IORef [PlannedReplayRequest]
    -> IO VampireResolver
plannedReplayResolver original liveRef =
    pure
        (vampireBatchResolverWithPreparationObserver resolve
            (observeVampirePreparation original))
  where
    resolve
        :: forall local origin.
           NonEmpty
                (Provers.PreparedTypedProverTask
                    SemanticFactOccurrenceFingerprint
                    local
                    origin
                    ObjectId)
        -> IO
            (NonEmpty
                (Either
                    Provers.ProverProcessError
                    Provers.ProverAnswer))
    resolve tasks = do
        expected <- atomicModifyIORef' liveRef \remaining ->
            let amount = NonEmpty.length tasks
                (selected, later) = splitAt amount remaining
            in (later, selected)
        unless (length expected == NonEmpty.length tasks)
            (throwIO
                (PlanningIntegrityError
                    "admission requested a different number of live Vampire results"))
        traverse_ validateExpected (zip (toList tasks) expected)
        case expected of
            ReplayLive{} : _ -> do
                unless (all isLive expected)
                    (throwIO
                        (PlanningIntegrityError
                            "planned resolver batch mixed execution modes"))
                results <- traverse awaitOne expected
                maybe
                    (throwIO
                        (PlanningIntegrityError
                            "an admission resolver batch was unexpectedly empty"))
                    pure
                    (NonEmpty.nonEmpty results)
            ReplaySynchronous{} : _ ->
                resolveSynchronousVampireBatch original tasks
            [] ->
                throwIO
                    (PlanningIntegrityError
                        "an admission resolver batch was unexpectedly empty")

    validateExpected (task, replay) = do
        let actual = Provers.preparedTypedProverRequest task
            expected = replayRequest replay
        unless (actual == expected)
            (throwIO
                (PlanningIntegrityError
                    "admission request differs from its planned exact request"))

    awaitOne (ReplayLive expected handle) =
        Provers.awaitPreparedVampireRequest expected handle
    awaitOne ReplaySynchronous{} =
        impossible "validated live resolver batch changed execution mode"

    replayRequest = \case
        ReplayLive request _handle -> request
        ReplaySynchronous request -> request

    isLive = \case
        ReplayLive{} -> True
        ReplaySynchronous{} -> False

plannedAdmissionValidation
    :: PlannedValidationSelection
    -> ValidationRun
plannedAdmissionValidation = \case
    PlannedFreshValidation -> FreshValidation
    PlannedProofValidation expected record ->
        WarmValidation
            (validationLookup
                (\actual ->
                    if actual == expected
                        then pure (Just record)
                        else throwIO
                            (PlanningIntegrityError
                                "proof validation key changed during admission"))
                (\_actual -> pure Nothing))
    PlannedCompiledValidation expected record ->
        WarmValidation
            (validationLookup
                (\_actual -> pure Nothing)
                (\actual ->
                    if actual == expected
                        then pure (Just record)
                        else throwIO
                            (PlanningIntegrityError
                                "declaration validation key changed during admission")))

validateAdmittedPlan
    :: PlannedDeclaration body
    -> CommittedDeclarationBatch
    -> IO ()
validateAdmittedPlan
        (PlannedDeclaration _checked expectedPrevious expectedNext expectedDelta
            expectedObjects expectedPropositions candidates selection)
        batch = do
    let expectedContracts =
            [ (authority, direct)
            | stage <- candidates
            , PlannedCandidate _candidate authority direct _requests <-
                toList stage
            ]
        actualCertificates =
            (proofValidationRecordCertificate
                <$> committedBatchProofValidations batch)
                <> maybe
                    []
                    declarationValidationRecordCertificates
                    (committedBatchDeclarationValidation batch)
        actualContracts =
            [ ( validationTarget certificate
              , validationDirectAuthorization certificate
              )
            | certificate <- actualCertificates
            ]
        validationAgrees = case selection of
            PlannedFreshValidation -> True
            PlannedProofValidation _ record ->
                committedBatchProofValidations batch == [record]
            PlannedCompiledValidation _ record ->
                committedBatchDeclarationValidation batch == Just record
    unless
        ( committedBatchPreviousPrefix batch == expectedPrevious
          && committedBatchNextPrefix batch == expectedNext
          && committedBatchDelta batch == expectedDelta
          && committedBatchObjects batch == expectedObjects
          && fmap propositionContract (committedBatchPropositions batch)
                == fmap propositionContract expectedPropositions
          && actualContracts == expectedContracts
          && validationAgrees
        )
        (throwIO
            (PlanningIntegrityError
                "admitted declaration differs from its prospective contract"))
  where
    propositionContract proposition =
        ( checkedPropositionId proposition
        , checkedPropositionTerm proposition
        )

commitProofDeclaration
    :: ProofSyntaxId
    -> Declaration value
    -> ModuleDriver failure
        (value, CommittedDeclarationBatch)
commitProofDeclaration syntax =
    commitDeclaration (ProofValidationMode syntax)

commitCompiledDeclaration
    :: DeclarationSyntaxId
    -> Declaration value
    -> ModuleDriver failure
        (value, CommittedDeclarationBatch)
commitCompiledDeclaration syntax =
    commitDeclaration (DeclarationValidationMode syntax)

commitDeclaration
    :: ValidationMode
    -> Declaration value
    -> ModuleDriver failure
        (value, CommittedDeclarationBatch)
commitDeclaration mode action = ModuleDriver do
    DriverState resolver builder pendingPrefix validationRun <-
        State.get
    let
        declaration =
            initialDeclarationState
                resolver
                validationRun
                mode
                builder
    result <-
        liftIO
            (Except.runExceptT
                (State.runStateT
                    (runDeclaration action)
                    declaration))
    case result of
        Left err ->
            Except.throwError (DriverDeclarationFailed err)
        Right (value, prepared) ->
            case appendDeclaration mode prepared of
                Left err ->
                    Except.throwError (DriverDeclarationFailed err)
                Right (builder', batch) ->
                    let prefix' = appendPendingBatch batch pendingPrefix
                    in do
                        State.put
                            (DriverState
                                resolver
                                builder'
                                prefix'
                                validationRun)
                        pure (value, batch)

initialDeclarationState
    :: VampireResolver
    -> ValidationRun
    -> ValidationMode
    -> LogicalBuilder
    -> DeclarationState
initialDeclarationState resolver validationRun validationMode builder =
    DeclarationState
        { declarationVampireResolver = resolver
        , declarationValidationRun = validationRun
        , declarationValidationMode = validationMode
        , declarationValidationSelection =
            DeclarationValidationUnselected
        , declarationBuilder = builder
        , declarationOwnSlot =
            declarationSlot
                (logicalBuilderOwner builder)
                (localDeclarationOrdinal
                    (logicalBuilderNextDeclaration builder))
        , declarationInvocation =
            DeclarationInvocation
                (logicalBuilderNextInvocation builder)
        , declarationObjectsReversed = []
        , declarationObjectClosure = Nothing
        , declarationPropositionsReversed = []
        , declarationGlobalBindingsReversed = []
        , declarationStructureDescriptorsReversed = []
        , declarationReservations = Map.empty
        , declarationPending = Map.empty
        , declarationNextFact = logicalBuilderNextFact builder
        , declarationNextStage = 0
        , declarationAuthorizationFrontier = 0
        }

appendDeclaration
    :: ValidationMode
    -> DeclarationState
    -> Either
        DeclarationError
        (LogicalBuilder, CommittedDeclarationBatch)
appendDeclaration mode declaration = do
    let builder = declarationBuilder declaration
        reservations = Map.elems (declarationReservations declaration)
        pending = declarationPending declaration
    unless
        (Map.keysSet pending
            == Map.keysSet (declarationReservations declaration))
        (Left DeclarationHasUnauthorizedCandidates)
    unless
        (declarationAuthorizationFrontier declaration
            == declarationNextStage declaration)
        (Left DeclarationAuthorizationFrontierIncomplete)
    case mode of
        DeclarationValidationMode{} ->
            case declarationValidationSelection declaration of
                DeclarationValidationUnselected ->
                    Left DeclarationValidationNotSelected
                _ -> pure ()
        _ -> pure ()
    closure <- declarationClosure declaration
    propositions <- validateDeclarationPropositions closure declaration
    traverse_ (validatePendingAuthorization declaration) (Map.elems pending)
    let orderedPending =
            [ pendingCandidate
            | reservation <- reservations
            , let slot = reservedCandidateSlot reservation
            , Just pendingCandidate <- [Map.lookup slot pending]
            ]
        occurrences = occurrenceFromPending <$> orderedPending
        aliases = concatMap aliasesFromPending orderedPending
        objectIds =
            assertedObjectId
                <$> reverse
                    (declarationObjectsReversed declaration)
        propositionIds =
            checkedPropositionId <$> propositions
    (structures, delta, next) <-
        buildCheckedDeclarationDelta
            builder
            closure
            (declarationOwnSlot declaration)
            occurrences
            aliases
            objectIds
            propositionIds
            (declarationGlobalBindingsReversed declaration)
            (declarationStructureDescriptorsReversed declaration)
    let previous = logicalBuilderPrefix builder
    (proofValidations, declarationValidation) <-
        buildValidationRecords
            mode previous objectIds orderedPending
    let builder' =
            appendBuilderState
                closure
                structures
                delta
                next
                orderedPending
                builder
                declaration
        batch =
            CommittedDeclarationBatch
                (logicalBuilderOwner builder)
                (declarationOwnSlot declaration)
                previous
                next
                delta
                (reverse
                    (declarationObjectsReversed declaration))
                propositions
                proofValidations
                declarationValidation
    pure (builder', batch)

-- | Construct and collision-check one canonical semantic delta without
-- inspecting fact evidence.  This remains the admitted append path now and
-- is the shared delta seam for the later prospective builder.
buildCheckedDeclarationDelta
    :: BuilderState evidence
    -> CheckedObjectClosure
    -> DeclarationSlot
    -> [SemanticFactOccurrence]
    -> [SemanticAlias]
    -> [ObjectId]
    -> [PropositionId]
    -> [SemanticGlobalBinding]
    -> [SemanticStructureDescriptor]
    -> Either
        DeclarationError
        ( Map SemanticStructurePhrase ResolvedStructure
        , DeclarationInterfaceDelta
        , PrefixContextId
        )
buildCheckedDeclarationDelta
        builder closure slot occurrences aliases objectIds propositionIds
        reversedBindings reversedDescriptors = do
    let bindings =
            List.sortOn
                semanticGlobalBindingKey
                (reverse reversedBindings)
        descriptors =
            List.sortOn
                semanticStructureDescriptorPhrase
                (reverse reversedDescriptors)
    traverse_
        (\binding ->
            first
                (DeclarationGlobalTargetInvalid
                    (semanticGlobalBindingKey binding)
                    (semanticGlobalBindingTarget binding))
                (validateSemanticGlobalBindingTarget
                    (structureOperationBindings
                        (logicalBuilderStructures builder))
                    closure binding))
        bindings
    traverse_
        (\descriptor ->
            let structurePhrase = semanticStructureDescriptorPhrase descriptor
            in when
                (Map.member structurePhrase
                    (logicalBuilderStructures builder))
                (Left (BuilderStructureCollision structurePhrase)))
        descriptors
    structures <- foldM
        (insertSemanticStructure closure)
        (logicalBuilderStructures builder)
        descriptors
    environment <-
        first DeclarationEnvironmentFailed
            (semanticEnvironmentWithStructures bindings descriptors)
    delta <-
        first DeclarationInterfaceFailed
            (declarationInterfaceDelta
                slot
                occurrences
                aliases
                objectIds
                propositionIds
                environment)
    validateBuilderCollisions builder delta
    pure
        ( structures
        , delta
        , nextPrefixContextId (logicalBuilderPrefix builder) delta
        )

declarationClosure
    :: DeclarationState
    -> Either DeclarationError CheckedObjectClosure
declarationClosure declaration =
    case declarationObjectClosure declaration of
        Just closure ->
            Right closure
        Nothing ->
            first DeclarationObjectValidationFailed
                (extendObjectClosure
                    (logicalBuilderObjectClosure
                        (declarationBuilder declaration))
                    (reverse
                        (declarationObjectsReversed declaration)))

prepareDeclarationClosure
    :: DeclarationState
    -> Either DeclarationError DeclarationState
prepareDeclarationClosure declaration = do
    closure <- declarationClosure declaration
    pure declaration{declarationObjectClosure = Just closure}

validateDeclarationPropositions
    :: CheckedObjectClosure
    -> DeclarationState
    -> Either DeclarationError [CheckedPropositionContent]
validateDeclarationPropositions closure declaration = do
    let explicit =
            reverse
                (declarationPropositionsReversed declaration)
        reserved =
            candidateCheckedProposition
                <$> Map.elems
                    (declarationReservations declaration)
        propositions = stableUniqueBy checkedPropositionId (explicit <> reserved)
    traverse_
        (\proposition ->
            void
                (first DeclarationPropositionValidationFailed
                    (validateAssertedPropositionContent
                        closure
                        (checkedPropositionId proposition)
                        (frozenCoreTerm
                            (checkedPropositionTerm proposition)))))
        propositions
    pure propositions

validatePendingAuthorization
    :: DeclarationState
    -> PendingCandidate
    -> Either DeclarationError ()
validatePendingAuthorization declaration
        (PendingCandidate candidate certificate authorization) = do
    validateReservedCandidate declaration candidate
    let builder = declarationBuilder declaration
        PendingFactAuthorization
            identity prefix invocation slot authority stage =
                authorization
    unless
        ( identity == logicalBuilderIdentity builder
          && prefix == logicalBuilderPrefix builder
          && invocation == declarationInvocation declaration
          && slot == reservedCandidateSlot candidate
          && authority == validationTarget certificate
          && stage == reservedStage candidate
        )
        (Left PendingFactAuthorizationMismatch)

occurrenceFromPending
    :: PendingCandidate
    -> SemanticFactOccurrence
occurrenceFromPending
        (PendingCandidate candidate certificate _authorization) =
    candidateOccurrence candidate (validationTarget certificate)

aliasesFromPending :: PendingCandidate -> [SemanticAlias]
aliasesFromPending pending@(PendingCandidate
        candidate _certificate _authorization) =
    let occurrence = occurrenceFromPending pending
        fingerprint = semanticFactFingerprint occurrence
    in (`semanticAlias` fingerprint) <$> candidateAliases candidate

buildValidationRecords
    :: ValidationMode
    -> PrefixContextId
    -> [ObjectId]
    -> [PendingCandidate]
    -> Either
        DeclarationError
        ([ProofValidationRecord], Maybe DeclarationValidationRecord)
buildValidationRecords mode prefix objects pending =
    case mode of
        EnvironmentImportMode ->
            impossible
                "environment import produced declaration validation records"
        ProofValidationMode syntax ->
            case pending of
                [PendingCandidate _ certificate _] ->
                    let authority = validationTarget certificate
                        key =
                            proofValidationKey
                                (theoremId
                                    (factAuthorityTheorem authority))
                                syntax
                                prefix
                    in Right
                        ( [proofValidationRecord key certificate]
                        , Nothing
                        )
                _ ->
                    Left ProofDeclarationMustProduceOneFact
        DeclarationValidationMode syntax ->
            let certificates =
                    [ certificate
                    | PendingCandidate _ certificate _ <- pending
                    ]
                theorems =
                    theoremId
                        . factAuthorityTheorem
                        . validationTarget
                        <$> certificates
                key =
                    declarationValidationKey
                        syntax prefix objects theorems
            in Right
                ( []
                , Just
                    (declarationValidationRecord
                        key certificates)
                )

validateBuilderCollisions
    :: BuilderState evidence
    -> DeclarationInterfaceDelta
    -> Either DeclarationError ()
validateBuilderCollisions builder delta = do
    traverse_
        (\occurrence ->
            when
                (Map.member
                    (semanticFactFingerprint occurrence)
                    (logicalBuilderFacts builder))
                (Left
                    (BuilderFactCollision
                        (semanticFactFingerprint occurrence))))
        (declarationDeltaFacts delta)
    traverse_
        (\alias ->
            when
                (Map.member
                    (semanticAliasName alias)
                    (logicalBuilderAliases builder))
                (Left
                    (BuilderAliasCollision
                        (semanticAliasName alias))))
        (declarationDeltaAliases delta)
    traverse_
        (\identity ->
            when
                (identity
                    `Set.member` checkedObjectIds
                        (logicalBuilderObjectClosure builder))
                (Left (BuilderObjectCollision identity)))
        (declarationDeltaObjects delta)
    traverse_
        (\binding ->
            case Map.lookup
                    (semanticGlobalBindingKey binding)
                    (logicalBuilderGlobals builder) of
                Nothing -> pure ()
                Just existing ->
                    Left
                        (BuilderGlobalCollision
                            (semanticGlobalBindingKey binding)
                            existing))
        (semanticEnvironmentBindings
            (declarationDeltaEnvironment delta))

appendBuilderState
    :: CheckedObjectClosure
    -> Map SemanticStructurePhrase ResolvedStructure
    -> DeclarationInterfaceDelta
    -> PrefixContextId
    -> [PendingCandidate]
    -> LogicalBuilder
    -> DeclarationState
    -> LogicalBuilder
appendBuilderState closure structures delta next pending builder declaration =
    builder
        { logicalBuilderPrefix = next
        , logicalBuilderObjectClosure = closure
        , logicalBuilderFacts =
            foldl'
                (insertAuthorizedFact builder)
                (logicalBuilderFacts builder)
                pending
        , logicalBuilderAliases =
            foldl'
                (\entries alias ->
                    Map.insert
                        (semanticAliasName alias)
                        (ImportedAliasBinding
                            (semanticAliasTarget alias)
                            (ImportedAliasOrigin
                                (declarationDeltaSlot delta)
                                (semanticAliasTarget alias)))
                        entries)
                (logicalBuilderAliases builder)
                (declarationDeltaAliases delta)
        , logicalBuilderGlobals =
            foldl'
                (\entries binding ->
                    Map.insert
                        (semanticGlobalBindingKey binding)
                        (semanticGlobalBindingTarget binding)
                        entries)
                (logicalBuilderGlobals builder)
                (semanticEnvironmentBindings
                    (declarationDeltaEnvironment delta))
        , logicalBuilderStructures = structures
        , logicalBuilderDeltas =
            delta : logicalBuilderDeltas builder
        , logicalBuilderNextDeclaration =
            logicalBuilderNextDeclaration builder + 1
        , logicalBuilderNextFact =
            declarationNextFact declaration
        , logicalBuilderNextInvocation =
            logicalBuilderNextInvocation builder + 1
        }

insertAuthorizedFact
    :: LogicalBuilder
    -> Map
        SemanticFactOccurrenceFingerprint
        (FactEntry BuilderFactAuthorization)
    -> PendingCandidate
    -> Map
        SemanticFactOccurrenceFingerprint
        (FactEntry BuilderFactAuthorization)
insertAuthorizedFact builder entries pending@(PendingCandidate
        candidate certificate _pendingAuthorization) =
    let occurrence = occurrenceFromPending pending
        fingerprint = semanticFactFingerprint occurrence
        authority = validationTarget certificate
        authorization =
            BuilderFactAuthorization
                (logicalBuilderIdentity builder)
                (reservedCandidateSlot candidate)
                authority
    in Map.insert
        fingerprint
        (FactEntry
            (candidateCheckedProposition candidate)
            occurrence
            authorization)
        entries

stableUniqueBy :: Ord key => (value -> key) -> [value] -> [value]
stableUniqueBy key =
    reverse . snd
        . foldl'
            (\(seen, values) value ->
                let identity = key value
                in if identity `Set.member` seen
                    then (seen, values)
                    else
                        ( Set.insert identity seen
                        , value : values
                        ))
            (Set.empty, [])


data DeclarationError
    = CandidateOutsideDeclaration !FactSlot
    | CandidateAlreadyAuthorized !FactSlot
    | CandidateOutsideAuthorizationFrontier
        !FactSlot !Natural !Natural
    | DeclarationHasUnauthorizedCandidates
    | DeclarationAuthorizationFrontierIncomplete
    | CandidatePropositionNotClosed
    | CandidatePropositionNotProposition !CoreType
    | StagedPremiseNotEarlier
        !FactSlot !Natural !FactSlot !Natural
    | StagedPremiseNotAuthorized !FactSlot
    | AuthorizedFactNotVisible
        !SemanticFactOccurrenceFingerprint
    | BuilderFactAuthorizationMismatch
    | PendingFactAuthorizationMismatch
    | PlanningFactContractMismatch !FactSlot
    | CheckedAuthorizationCandidateShapeMismatch !Int !Int
    | CheckedProofCandidateCountMismatch !Int
    | LocalClaimOutsideCandidate
    | FactSafetyFailed !FactSafetyError
    | ValidationCertificateFailed !ValidationCertificateError
    | DerivationImportFailed !DerivationImportError
    | KernelCompletionFailed !KernelReplayError
    | KernelConstructionDescriptorMismatch
    | DefinitionEquationObjectMissing !ObjectId
    | DefinitionEquationObjectNotTransparent !ObjectId
    | DefinitionEquationObjectNotPointwisePredicate !ObjectId
    | DefinitionEquationCandidateMismatch
    | DatatypeCompilationDescriptorMismatch
    | ProofObligationFailedAt !Location !DeclarationError
    | VampireProcessFailed !Provers.ProverProcessError
    | VampireObligationRejected !Provers.ProverAnswer
    | VampireProofHasNoAcceptedObligations
    | VampireCandidateBatchMismatch ![FactSlot] ![FactSlot]
    | VampireCandidateBatchProofShapeMismatch !FactSlot
    | VampireResolverBatchSizeMismatch !Int !Int
    | OmittedProofDidNotRecordUse
    | VampireRequestMismatch
    | VampireTargetMismatch
    | VampireLocalPremisesNotSupported
    | VampireGlobalTypeMismatch !ObjectId
    | VampirePremiseMismatch
        !SemanticFactOccurrenceFingerprint
    | VampirePremiseCapabilityMismatch
        !SemanticFactOccurrenceFingerprint
    | VampireFoundationMismatch !FoundationAxiomTag
    | CurrentCandidateVampirePreparationFailed
        !(VampireObligationPreparationError Void)
    | ProofValidationOutsideProofDeclaration
    | DeclarationValidationOutsideCompiledDeclaration
    | DeclarationValidationAlreadySelected
    | DeclarationValidationNotSelected
    | DeclarationShapeChangedAfterValidationLookup
    | CachedDeclarationCandidateMissing !FactSlot
    | ImportedModuleNotDirect !SemanticInterfaceId
    | ImportedFactMaterializationFailed
        !Materialization.MaterializationError
    | ImportedFactCollision
        !SemanticFactOccurrenceFingerprint
    | ImportedAliasCollision
        !SemanticName !ImportedAliasOrigin !ImportedAliasOrigin
    | ImportedAliasTargetMissing
        !SemanticFactOccurrenceFingerprint
    | ImportedGlobalCollision
        !SemanticGlobalKey !SemanticGlobalTarget !SemanticGlobalTarget
    | ImportedGlobalTargetInvalid
        !SemanticGlobalKey
        !SemanticGlobalTarget
        !SemanticGlobalTargetError
    | ImportedStructureCollision
        !SemanticStructurePhrase
        !SemanticStructureDescriptor
        !SemanticStructureDescriptor
    | SemanticStructureParentMissing
        !SemanticStructurePhrase !SemanticStructurePhrase
    | SemanticStructureOperationConflict
        !StructSymbol !SemanticStructurePhrase !SemanticStructurePhrase
    | SemanticStructurePredicateTargetInvalid
        !SemanticStructurePhrase !ObjectId !(Maybe CoreType) !CoreType
    | SemanticStructureOperationTargetInvalid
        !SemanticStructurePhrase !StructSymbol !ObjectId !(Maybe CoreType) !CoreType
    | ImportedEvidenceDirectMismatch
        ![SemanticInterfaceId] ![SemanticInterfaceId]
    | ImportedEvidenceInterfaceFailed !SemanticInterfaceError
    | ImportedEvidenceObjectMissing !ObjectId
    | ImportedEvidencePropositionMissing !PropositionId
    | ImportedModuleAfterAuthorization
    | DeclarationObjectAddedAfterAuthorization
    | DeclarationObjectValidationFailed !ObjectValidationError
    | DeclarationPropositionValidationFailed
        !PropositionValidationError
    | DeclarationInterfaceFailed !DeclarationInterfaceError
    | DeclarationEnvironmentFailed !SemanticEnvironmentError
    | DeclarationGlobalAlreadyStaged !SemanticGlobalKey
    | DeclarationStructureAlreadyStaged !SemanticStructurePhrase
    | DeclarationGlobalTargetInvalid
        !SemanticGlobalKey
        !SemanticGlobalTarget
        !SemanticGlobalTargetError
    | ProofDeclarationMustProduceOneFact
    | BuilderFactCollision
        !SemanticFactOccurrenceFingerprint
    | BuilderAliasCollision !SemanticName
    | BuilderObjectCollision !ObjectId
    | BuilderGlobalCollision !SemanticGlobalKey !SemanticGlobalTarget
    | BuilderStructureCollision !SemanticStructurePhrase
    deriving stock (Show, Eq)

declarationErrorLocation :: DeclarationError -> Maybe Location
declarationErrorLocation = \case
    ProofObligationFailedAt location _failure ->
        Just location
    _failure ->
        Nothing

renderDeclarationError :: DeclarationError -> Text
renderDeclarationError = \case
    CandidateOutsideDeclaration slot ->
        "candidate " <> shown slot <> " does not belong to this declaration"
    CandidateAlreadyAuthorized slot ->
        "candidate " <> shown slot <> " was authorized more than once"
    CandidateOutsideAuthorizationFrontier slot expected actual ->
        "candidate " <> shown slot <> " is outside authorization frontier "
            <> shown expected <> " (found " <> shown actual <> ")"
    DeclarationHasUnauthorizedCandidates ->
        "the declaration has unauthorized candidates"
    DeclarationAuthorizationFrontierIncomplete ->
        "the declaration authorization frontier is incomplete"
    CandidatePropositionNotClosed ->
        "the candidate proposition still has open local binders"
    CandidatePropositionNotProposition actual ->
        "the candidate has type " <> shown actual <> " instead of Prop"
    StagedPremiseNotEarlier candidate candidateOrdinal premise premiseOrdinal ->
        "candidate " <> shown candidate <> " at stage " <> shown candidateOrdinal
            <> " depends on non-earlier premise " <> shown premise
            <> " at stage " <> shown premiseOrdinal
    StagedPremiseNotAuthorized slot ->
        "staged premise " <> shown slot <> " is not authorized"
    AuthorizedFactNotVisible fingerprint ->
        "authorized fact " <> shown fingerprint <> " is not visible"
    BuilderFactAuthorizationMismatch ->
        "builder fact authority does not match the checked declaration"
    PendingFactAuthorizationMismatch ->
        "pending fact authority does not match the checked declaration"
    PlanningFactContractMismatch slot ->
        "checked declaration-stage fact " <> shown slot
            <> " has inconsistent semantic provenance"
    CheckedAuthorizationCandidateShapeMismatch expected actual ->
        "checked declaration recipe expected " <> shown expected
            <> " candidate stages but received " <> shown actual
    CheckedProofCandidateCountMismatch actual ->
        "checked proof declaration requires exactly one candidate but received "
            <> shown actual
    LocalClaimOutsideCandidate ->
        "proof-local claim was used outside a candidate proof"
    FactSafetyFailed{} ->
        "fact-safety validation failed"
    ValidationCertificateFailed{} ->
        "validation-certificate checking failed"
    DerivationImportFailed{} ->
        "kernel derivation import failed"
    KernelCompletionFailed{} ->
        "kernel replay failed"
    KernelConstructionDescriptorMismatch ->
        "kernel construction does not match its checked descriptor"
    DefinitionEquationObjectMissing identity ->
        "definition equation references missing object " <> shown identity
    DefinitionEquationObjectNotTransparent identity ->
        "definition equation references non-transparent object " <> shown identity
    DefinitionEquationObjectNotPointwisePredicate identity ->
        "definition equation object " <> shown identity
            <> " is not a unary predicate definition"
    DefinitionEquationCandidateMismatch ->
        "definition equation does not match its checked object content"
    DatatypeCompilationDescriptorMismatch ->
        "datatype compilation does not match its complete checked family"
    ProofObligationFailedAt location failure ->
        locationToText location <> ": " <> renderDeclarationError failure
    VampireProcessFailed{} ->
        "Vampire process failed while authorizing the declaration"
    VampireObligationRejected{} ->
        "Vampire did not accept a declaration obligation"
    VampireProofHasNoAcceptedObligations ->
        "Vampire proof contains no accepted obligations"
    VampireCandidateBatchMismatch expected actual ->
        "Vampire candidate batch does not match the complete authorization "
            <> "stage (expected " <> shown expected
            <> ", found " <> shown actual <> ")"
    VampireCandidateBatchProofShapeMismatch slot ->
        "Vampire candidate " <> shown slot
            <> " performed execution before its ready batch"
    VampireResolverBatchSizeMismatch expected actual ->
        "Vampire resolver returned " <> shown actual
            <> " results for " <> shown expected <> " requests"
    OmittedProofDidNotRecordUse ->
        "omitted proof completion did not record an omission"
    VampireRequestMismatch ->
        "accepted Vampire run does not match the prepared request"
    VampireTargetMismatch ->
        "Vampire request target does not match the candidate theorem"
    VampireLocalPremisesNotSupported ->
        "typed Vampire requests do not yet support local premises"
    VampireGlobalTypeMismatch object ->
        "Vampire request has the wrong type for global object " <> shown object
    VampirePremiseMismatch fingerprint ->
        "Vampire request premise does not match visible fact " <> shown fingerprint
    VampirePremiseCapabilityMismatch fingerprint ->
        "Vampire request lacks authority for premise " <> shown fingerprint
    VampireFoundationMismatch tag ->
        "Vampire request has inconsistent foundation axiom " <> shown tag
    CurrentCandidateVampirePreparationFailed failure ->
        "the staged Vampire obligation could not be prepared: " <> shown failure
    ProofValidationOutsideProofDeclaration ->
        "proof validation requires a proof declaration"
    DeclarationValidationOutsideCompiledDeclaration ->
        "declaration validation requires a compiled declaration"
    DeclarationValidationAlreadySelected ->
        "compiled declaration validation was selected more than once"
    DeclarationValidationNotSelected ->
        "compiled declaration validation was not selected"
    DeclarationShapeChangedAfterValidationLookup ->
        "compiled declaration shape changed after validation lookup"
    CachedDeclarationCandidateMissing slot ->
        "cached declaration validation has no candidate for " <> shown slot
    ImportedModuleNotDirect interface ->
        "sealed semantic interface is not a direct import: " <> shown interface
    ImportedFactMaterializationFailed{} ->
        "imported fact failed materialization checks"
    ImportedFactCollision fingerprint ->
        "imported fact " <> shown fingerprint <> " is already registered"
    ImportedAliasCollision alias earlier later ->
        "imported semantic alias " <> shown alias
            <> " conflicts between " <> shown earlier
            <> " and " <> shown later
    ImportedAliasTargetMissing fingerprint ->
        "imported alias targets missing fact " <> shown fingerprint
    ImportedGlobalCollision key earlier later ->
        "imported global " <> shown key
            <> " has conflicting targets " <> shown earlier
            <> " and " <> shown later
    ImportedGlobalTargetInvalid key target _failure ->
        "imported global " <> shown key
            <> " has invalid target " <> shown target
    ImportedEvidenceDirectMismatch expected actual ->
        "imported semantic parents differ: expected " <> shown expected
            <> ", found " <> shown actual
    ImportedStructureCollision structurePhrase _existing _incoming ->
        "structure " <> shown structurePhrase <> " has conflicting descriptors"
    SemanticStructureParentMissing structurePhrase parent ->
        "structure " <> shown structurePhrase <> " has unknown parent " <> shown parent
    SemanticStructureOperationConflict symbol firstOrigin secondOrigin ->
        "structure operation " <> shown symbol <> " conflicts between "
            <> shown firstOrigin <> " and " <> shown secondOrigin
    SemanticStructurePredicateTargetInvalid structurePhrase object _actual expected ->
        "structure " <> shown structurePhrase <> " has invalid predicate object "
            <> shown object <> " (expected " <> shown expected <> ")"
    SemanticStructureOperationTargetInvalid structurePhrase symbol object _actual expected ->
        "structure " <> shown structurePhrase <> " has invalid operation "
            <> shown symbol <> " object " <> shown object
            <> " (expected " <> shown expected <> ")"
    ImportedEvidenceInterfaceFailed{} ->
        "imported semantic interface failed validation"
    ImportedEvidenceObjectMissing identity ->
        "imported semantic interface is missing object " <> shown identity
    ImportedEvidencePropositionMissing identity ->
        "imported semantic interface is missing proposition " <> shown identity
    ImportedModuleAfterAuthorization ->
        "a sealed module was imported after candidate authorization"
    DeclarationObjectAddedAfterAuthorization ->
        "the declaration added an object after candidate authorization"
    DeclarationObjectValidationFailed{} ->
        "declaration object validation failed"
    DeclarationPropositionValidationFailed{} ->
        "declaration proposition validation failed"
    DeclarationInterfaceFailed{} ->
        "declaration interface validation failed"
    DeclarationEnvironmentFailed{} ->
        "declaration environment delta is inconsistent"
    DeclarationGlobalAlreadyStaged key ->
        "global " <> shown key <> " was staged more than once"
    DeclarationStructureAlreadyStaged structurePhrase ->
        "structure " <> shown structurePhrase <> " was staged more than once"
    DeclarationGlobalTargetInvalid key target _failure ->
        "global " <> shown key <> " has invalid target " <> shown target
    ProofDeclarationMustProduceOneFact ->
        "a proof declaration must produce exactly one fact"
    BuilderFactCollision fingerprint ->
        "fact " <> shown fingerprint <> " is already registered"
    BuilderAliasCollision alias ->
        "semantic alias " <> shown alias <> " is already registered"
    BuilderObjectCollision object ->
        "object " <> shown object <> " is already registered"
    BuilderGlobalCollision key object ->
        "global " <> shown key <> " is already bound to " <> shown object
    BuilderStructureCollision structurePhrase ->
        "structure " <> shown structurePhrase <> " is already registered"
  where
    shown :: Show value => value -> Text
    shown = Text.pack . show