Migrate to `Felix` namespaceHEADhotg

1 files changed, 2639 insertions, 0 deletions

diff --git a/source/Felix/Checking/Exact/Proof.hs b/source/Felix/Checking/Exact/Proof.hs
new file mode 100644
index 0000000..e2149c4
--- /dev/null
+++ b/source/Felix/Checking/Exact/Proof.hs
@@ -0,0 +1,2639 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Exact lowering for the first ordinary theorem/proof fragment.
+--
+-- This module is the trusted owner of structural local-proof composition.  Its
+-- private prepared tree controls when assumptions and proved local claims
+-- become available and executes discharges depth-first.  The declaration
+-- boundary validates typed tasks and authority; it does not reconstruct this
+-- derivation.
+module Felix.Checking.Exact.Proof
+    ( PreparedExactProof
+    , preparedExactProofSyntaxId
+    , preparedExactProofFirstOmission
+    , prepareExactProof
+    , CheckedExactProofAuthorization
+    , lowerPreparedExactProof
+    , authorizeCheckedExactProof
+    , PreparedFinalPreludeFoundationClaim
+    , prepareFinalPreludeFoundationClaim
+    , CheckedFinalPreludeFoundationAuthorization
+    , lowerPreparedFinalPreludeFoundationClaim
+    , authorizeCheckedFinalPreludeFoundationClaim
+    , ExactProofError(..)
+    , exactProofErrorLocation
+    , renderExactProofError
+    ) where
+
+import Base
+import Felix.Checking.Authority qualified as Authority
+import Felix.Checking.Backend.Problem qualified as Backend
+import Felix.Checking.Core
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Exact qualified as Exact
+import Felix.Checking.Foundation
+import Felix.Checking.Identity
+import Felix.Checking.Kernel.Derivation (foundationFactDerivation)
+import Felix.Checking.Kernel.Proof qualified as KernelProof
+import Felix.Checking.SetConstruction
+import Felix.Checking.Semantic
+import Felix.Cache.Codec
+import Felix.Report.Location
+import Felix.Syntax.Abstract qualified as Raw
+
+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.ByteString (ByteString)
+import Data.List.NonEmpty qualified as NonEmpty
+import Data.Map.Strict qualified as Map
+import Data.Set qualified as Set
+import Data.Text qualified as Text
+import Data.Vector (Vector)
+import Data.Vector qualified as Vector
+import Numeric.Natural (Natural)
+
+
+data ExactProofError
+    = ExactProofUnsupportedClaim !Location
+    | ExactProofUnsupportedStep !Location
+    | ExactProofSetInductionVariableRequired !Location
+    | ExactProofSetInductionVariableNotActive
+        !Location !Raw.VarSymbol
+    | ExactProofSetInductionFocusAmbiguous !Location
+    | ExactProofSetInductionActiveBinderIneligible
+        !Location !Raw.VarSymbol
+    | ExactProofSetInductionBinderConflict
+        !Location !Raw.VarSymbol
+    | ExactProofSetInductionGoalMismatch !Location
+    | ExactProofSetExtensionalityGoalMismatch !Location
+    | ExactProofSetExtensionalityDirectionsUnavailable !Location
+    | ExactProofExpectedUniversalGoal !Location
+    | ExactProofExpectedImplicationGoal !Location
+    | ExactProofGoalStatementMismatch !Location
+    | ExactProofEmptyCaseSplit !Location
+    | ExactProofStructuralCompositionFailed
+        !Location !KernelProof.KernelProofBuildError
+    | ExactProofLocalFunctionBinderMismatch !Location
+    | ExactProofLocalFunctionNameConflict !Location
+    | ExactProofUnknownReference !Location !Raw.Marker
+    | ExactProofElaborationFailed !Exact.ExactCompileError
+    | ExactProofObligationPreparationFailed
+        !Location
+        !(Declaration.VampireObligationPreparationError
+            Exact.ExactLocalId)
+    | ExactProofFoundationLeafRequiresImplicitAuto !Location
+    | ExactProofFoundationLeafTargetMismatch !Location
+    | ExactProofFoundationLeafTargetAmbiguous !Location
+    deriving stock (Show, Eq)
+
+exactProofErrorLocation :: ExactProofError -> Location
+exactProofErrorLocation = \case
+    ExactProofUnsupportedClaim location -> location
+    ExactProofUnsupportedStep location -> location
+    ExactProofSetInductionVariableRequired location -> location
+    ExactProofSetInductionVariableNotActive location _variable ->
+        location
+    ExactProofSetInductionFocusAmbiguous location -> location
+    ExactProofSetInductionActiveBinderIneligible location _variable ->
+        location
+    ExactProofSetInductionBinderConflict location _variable ->
+        location
+    ExactProofSetInductionGoalMismatch location -> location
+    ExactProofSetExtensionalityGoalMismatch location -> location
+    ExactProofSetExtensionalityDirectionsUnavailable location -> location
+    ExactProofExpectedUniversalGoal location -> location
+    ExactProofExpectedImplicationGoal location -> location
+    ExactProofGoalStatementMismatch location -> location
+    ExactProofEmptyCaseSplit location -> location
+    ExactProofStructuralCompositionFailed location _failure -> location
+    ExactProofLocalFunctionBinderMismatch location -> location
+    ExactProofLocalFunctionNameConflict location -> location
+    ExactProofUnknownReference location _marker -> location
+    ExactProofElaborationFailed failure ->
+        Exact.exactCompileErrorLocation failure
+    ExactProofObligationPreparationFailed location _failure -> location
+    ExactProofFoundationLeafRequiresImplicitAuto location -> location
+    ExactProofFoundationLeafTargetMismatch location -> location
+    ExactProofFoundationLeafTargetAmbiguous location -> location
+
+renderExactProofError :: ExactProofError -> Text
+renderExactProofError = \case
+    ExactProofUnsupportedClaim location ->
+        at location <> "this claim is not yet supported by the typed checker"
+    ExactProofUnsupportedStep location ->
+        at location <> "this proof step is not yet supported by the typed checker"
+    ExactProofSetInductionVariableRequired location ->
+        at location <> "exact set induction requires a named set variable"
+    ExactProofSetInductionVariableNotActive location variable ->
+        at location <> "the set-induction variable " <> shown variable
+            <> " is not an eligible exact focus"
+    ExactProofSetInductionFocusAmbiguous location ->
+        at location
+            <> "set induction without an explicit variable has no unique focus"
+    ExactProofSetInductionActiveBinderIneligible location variable ->
+        at location <> "the active binder " <> shown variable
+            <> " is not an eligible set-induction focus"
+    ExactProofSetInductionBinderConflict location variable ->
+        at location <> "the leading set-induction binder " <> shown variable
+            <> " conflicts with an active exact binder"
+    ExactProofSetInductionGoalMismatch location ->
+        at location <> "the set-induction variable does not belong to this goal"
+    ExactProofSetExtensionalityGoalMismatch location ->
+        at location <> "set extensionality requires a set-equality goal"
+    ExactProofSetExtensionalityDirectionsUnavailable location ->
+        at location
+            <> "set extensionality requires both directions as proved local claims"
+    ExactProofExpectedUniversalGoal location ->
+        at location <> "this fix step requires a universal goal"
+    ExactProofExpectedImplicationGoal location ->
+        at location <> "this assume step requires an implication goal"
+    ExactProofGoalStatementMismatch location ->
+        at location <> "the proof step does not match the current goal"
+    ExactProofEmptyCaseSplit location ->
+        at location <> "case analysis requires at least one case"
+    ExactProofStructuralCompositionFailed location failure ->
+        at location <> "invalid structural proof composition: " <> shown failure
+    ExactProofLocalFunctionBinderMismatch location ->
+        at location <> "the function argument must match its domain binder"
+    ExactProofLocalFunctionNameConflict location ->
+        at location <> "the function and argument names must be distinct"
+    ExactProofUnknownReference location marker ->
+        at location <> "the cited fact " <> shown marker <> " is not visible"
+    ExactProofElaborationFailed failure ->
+        Exact.renderExactCompileError failure
+    ExactProofObligationPreparationFailed location failure ->
+        at location <> "the exact proof obligation is invalid: " <> shown failure
+    ExactProofFoundationLeafRequiresImplicitAuto location ->
+        at location
+            <> "a confined foundation claim requires an implicit Auto proof"
+    ExactProofFoundationLeafTargetMismatch location ->
+        at location <> "the claim does not exactly match a foundation axiom"
+    ExactProofFoundationLeafTargetAmbiguous location ->
+        at location <> "the claim matches more than one foundation axiom"
+  where
+    at location = locationToText location <> ": "
+    shown :: Show value => value -> Text
+    shown = Text.pack . show
+
+data ExactLocalOrigin
+    = ExactAssumption
+    | ExactDerivedClaim
+    | ExactLocalDefinition
+    | ExactLocalConstructionExtensional
+    | ExactLocalConstructionEquation
+    deriving stock (Show, Eq, Ord)
+
+data PreparedLocal = PreparedLocal
+    !Backend.LocalPremiseOrdinal
+    !ExactLocalOrigin
+    !(Vector (Exact.ExactLocalId, CoreType))
+    !(ScopedCheckedCore ObjectId)
+
+data PreparedJustification
+    = PreparedAuto
+    | PreparedReferences
+        !(NonEmpty SemanticFactOccurrenceFingerprint)
+    | PreparedLocalOnly
+
+data PreparedDischarge
+    = PreparedVampireDischarge
+        !Location
+        !PreparedJustification
+        !(ScopedCheckedCore ObjectId)
+        !(Declaration.PreparedVampireObligation
+            Exact.ExactLocalId
+            ExactLocalOrigin)
+    | PreparedSetExtensionality
+        !Location
+        !(ScopedCheckedCore ObjectId)
+
+data PreparedCalculationLink = PreparedCalculationLink
+    !(ScopedCheckedCore ObjectId)
+    !PreparedDischarge
+
+-- The private constructor stores every destination with the discharge derived
+-- from its immediately preceding endpoint.  Planning and admission can
+-- therefore traverse one immutable sequence without re-associating shapes.
+data PreparedCalculation = PreparedCheckedCalculation
+    !CoreType
+    ![Exact.ExactLocalId]
+    !(Maybe (ScopedCheckedCore ObjectId))
+    !(ScopedCheckedCore ObjectId)
+    !(NonEmpty PreparedCalculationLink)
+    !(ScopedCheckedCore ObjectId)
+
+data PreparedSinceEvidence
+    = PreparedSinceExisting !PreparedLocal
+    | PreparedSinceDischarged !PreparedDischarge !PreparedLocal
+
+data PreparedCase = PreparedCase
+    !(ScopedCheckedCore ObjectId)
+    !PreparedProof
+
+data PreparedCaseAnalysis = PreparedCaseAnalysis
+    !(ScopedCheckedCore ObjectId)
+    !(NonEmpty PreparedCase)
+    !(ScopedCheckedCore ObjectId)
+    !PreparedDischarge
+
+data InitialSetInductionFocus = InitialSetInductionFocus
+    !Raw.VarSymbol
+    !Exact.ExactLocalId
+    !Natural
+
+data InitialSetInductionView = InitialSetInductionView
+    ![InitialSetInductionFocus]
+    !(Vector (Exact.ExactLocalId, CoreType))
+    !(ScopedCheckedCore ObjectId)
+    ![ScopedCheckedCore ObjectId]
+    !(ScopedCheckedCore ObjectId)
+    !(Maybe Raw.VarSymbol)
+
+data SetInductionBoundary
+    = InitialClaimInduction !InitialSetInductionView
+    -- A direct source-statement goal may retain only its leading binder name.
+    -- Recursive proof transformations deliberately discard this hint.
+    | SourceStatementInduction !(Maybe Raw.VarSymbol)
+    | RecursiveProofInduction
+
+data SelectedSetInductionFocus
+    = SelectedInitialSetInduction !InitialSetInductionFocus
+    | SelectedLeadingSetInduction !(Maybe Raw.VarSymbol)
+
+data PreparedSetInductionFocus
+    = PreparedInitialSetInductionFocus
+        !Exact.ExactLocalId
+        !Natural
+    | PreparedLeadingSetInductionFocus
+        !Exact.ExactLocalId
+
+data PreparedSetInduction = PreparedCheckedSetInduction
+    !PreparedSetInductionFocus
+    !(ScopedCheckedCore ObjectId)
+    ![ScopedCheckedCore ObjectId]
+    !(ScopedCheckedCore ObjectId)
+    !(ScopedCheckedCore ObjectId)
+    !(ScopedCheckedCore ObjectId)
+    !PreparedProof
+
+data PreparedProof
+    = PreparedImplicitAuto !PreparedDischarge
+    | PreparedQed !PreparedDischarge
+    | PreparedOmitted
+        !Location
+        !(ScopedCheckedCore ObjectId)
+    | PreparedFix ![Exact.ExactLocalId] !PreparedProof
+    | PreparedAssume
+        !(ScopedCheckedCore ObjectId)
+        !PreparedProof
+    | PreparedTake
+        ![Exact.ExactLocalId]
+        !(ScopedCheckedCore ObjectId)
+        !PreparedDischarge
+        !PreparedProof
+    | PreparedSetInduction !PreparedSetInduction
+    | PreparedHave
+        !(ScopedCheckedCore ObjectId)
+        !PreparedDischarge
+        !PreparedProof
+    | PreparedSuffices
+        !(ScopedCheckedCore ObjectId)
+        !(ScopedCheckedCore ObjectId)
+        !(ScopedCheckedCore ObjectId)
+        !PreparedDischarge
+        !PreparedProof
+    | PreparedCalculate
+        !PreparedCalculation
+        !PreparedProof
+    | PreparedSince
+        !(ScopedCheckedCore ObjectId)
+        !PreparedSinceEvidence
+        !(ScopedCheckedCore ObjectId)
+        !PreparedDischarge
+        !PreparedProof
+    | PreparedSubclaim
+        !(ScopedCheckedCore ObjectId)
+        !PreparedProof
+        !PreparedProof
+    | PreparedDefine
+        !Exact.ExactLocalId
+        !(ScopedCheckedCore ObjectId)
+        !(NonEmpty (ScopedCheckedCore ObjectId))
+        !PreparedProof
+    | PreparedDefineRelational
+        !Exact.ExactLocalId
+        !(ScopedCheckedCore ObjectId)
+        !PreparedDischarge
+        !(NonEmpty (ScopedCheckedCore ObjectId))
+        !PreparedProof
+    | PreparedDefineFunction
+        !Exact.ExactLocalId
+        !(ScopedCheckedCore ObjectId)
+        !(ScopedCheckedCore ObjectId)
+        !PreparedProof
+    | PreparedByCase !PreparedCaseAnalysis
+    | PreparedByContradiction
+        !(ScopedCheckedCore ObjectId)
+        !(ScopedCheckedCore ObjectId)
+        !(ScopedCheckedCore ObjectId)
+        !PreparedProof
+    | PreparedContradiction
+        !(ScopedCheckedCore ObjectId)
+        !(ScopedCheckedCore ObjectId)
+        !PreparedDischarge
+
+data PreparedExactProof = PreparedExactProof
+    !Location
+    !SemanticName
+    !(ScopedCheckedCore ObjectId)
+    !PreparedProof
+    !ProofSyntaxId
+
+data PreparedFinalPreludeFoundationClaim =
+    PreparedFinalPreludeFoundationClaim
+    !Location
+    !SemanticName
+    !(ScopedCheckedCore ObjectId)
+    !FoundationAxiomTag
+    !ProofSyntaxId
+
+preparedExactProofSyntaxId :: PreparedExactProof -> ProofSyntaxId
+preparedExactProofSyntaxId
+        (PreparedExactProof _location _alias _target _proof syntax) =
+    syntax
+
+preparedExactProofFirstOmission :: PreparedExactProof -> Maybe Location
+preparedExactProofFirstOmission
+        (PreparedExactProof _location _alias _target proof _syntax) =
+    preparedProofFirstOmission proof
+
+data PrepareState = PrepareState
+    { prepareNextLocal :: !Natural
+    , prepareNextPremise :: !Natural
+    }
+
+type Prepare =
+    StateT
+        PrepareState
+        (ExceptT ExactProofError (Declaration.LoweringDriver))
+
+prepareExactProof
+    :: Raw.Block
+    -> Maybe Raw.Proof
+    -> Declaration.LoweringDriver
+        (Either ExactProofError PreparedExactProof)
+prepareExactProof block explicitProof =
+    Except.runExceptT
+        (State.evalStateT prepare initialState)
+  where
+    initialState = PrepareState 0 0
+
+    prepare =
+        case block of
+            Raw.BlockClaim
+                    _kind location _title (Raw.Marker marker)
+                    (Raw.Claim assumptions statement) -> do
+                envelope <-
+                    liftDriver
+                        (Exact.prepareExactClaimEnvelope assumptions statement)
+                        >>= either
+                            (throwProof . ExactProofElaborationFailed)
+                            pure
+                let targetCore = Exact.preparedExactClaimTarget envelope
+                unless (null (scopedCoreContext targetCore))
+                    (throwProof
+                        (ExactProofUnsupportedClaim location))
+                (context, openedGoal, identities) <-
+                    openEnvelopeVariables
+                        targetCore
+                        (Exact.preparedExactClaimVariables envelope)
+                        (Exact.preparedExactClaimContext envelope)
+                (locals, bodyGoal, antecedents) <-
+                    openEnvelopeAntecedents
+                        context
+                        openedGoal
+                        (Exact.preparedExactClaimAntecedentCount envelope)
+                initialInduction <-
+                    prepareInitialSetInductionView
+                        statement
+                        context
+                        (Exact.preparedExactClaimVariables envelope)
+                        identities
+                        antecedents
+                        bodyGoal
+                bodyProof <-
+                    case explicitProof of
+                        Nothing ->
+                            PreparedImplicitAuto
+                                <$> prepareDischarge
+                                    location
+                                    context
+                                    locals
+                                    bodyGoal
+                                    Raw.JustificationEmpty
+                        Just sourceProof ->
+                            prepareProof
+                                location
+                                context
+                                locals
+                                (InitialClaimInduction initialInduction)
+                                bodyGoal
+                                sourceProof
+                let withAssumptions =
+                        foldr PreparedAssume bodyProof antecedents
+                    proof =
+                        case identities of
+                            [] -> withAssumptions
+                            _ -> PreparedFix identities withAssumptions
+                pure
+                    (PreparedExactProof
+                        location
+                        (semanticName marker)
+                        targetCore
+                        proof
+                        (proofSyntaxId
+                            (encodePreparedProof proof)))
+            _ ->
+                throwProof
+                    (ExactProofUnsupportedClaim (locate block))
+
+prepareFinalPreludeFoundationClaim
+    :: CheckedFoundation
+    -> Raw.Block
+    -> Maybe Raw.Proof
+    -> Declaration.LoweringDriver
+        (Either ExactProofError PreparedFinalPreludeFoundationClaim)
+prepareFinalPreludeFoundationClaim foundation block explicitProof =
+    Except.runExceptT do
+        case (block, explicitProof) of
+            ( Raw.BlockClaim
+                    _kind location _title (Raw.Marker marker)
+                    (Raw.Claim assumptions statement)
+              , Nothing
+              ) -> do
+                envelope <-
+                    Except.lift
+                        (Exact.prepareExactClaimEnvelope
+                            assumptions
+                            statement)
+                        >>= either
+                            (Except.throwError
+                                . ExactProofElaborationFailed)
+                            pure
+                unless
+                    ( null (Exact.preparedExactClaimVariables envelope)
+                        && Exact.preparedExactClaimAntecedentCount envelope
+                            == 0
+                    )
+                    (Except.throwError
+                        (ExactProofFoundationLeafRequiresImplicitAuto
+                            location))
+                let target = Exact.preparedExactClaimTarget envelope
+                    matches =
+                        [ tag
+                        | tag <- [minBound .. maxBound]
+                        , target == foundationTarget tag
+                        ]
+                tag <- case matches of
+                    [] ->
+                        Except.throwError
+                            (ExactProofFoundationLeafTargetMismatch location)
+                    [only] ->
+                        pure only
+                    _ ->
+                        Except.throwError
+                            (ExactProofFoundationLeafTargetAmbiguous location)
+                pure
+                    (PreparedFinalPreludeFoundationClaim
+                        location
+                        (semanticName marker)
+                        target
+                        tag
+                        (implicitAutoProofSyntaxId target))
+            (Raw.BlockClaim _kind location _title _marker _claim, Just{}) ->
+                Except.throwError
+                    (ExactProofFoundationLeafRequiresImplicitAuto location)
+            _ ->
+                Except.throwError
+                    (ExactProofUnsupportedClaim (locate block))
+  where
+    foundationTarget tag =
+        embedClosedCore []
+            (mapFrozenGlobals
+                absurd
+                (foundationAxiomFrozen foundation tag))
+
+openEnvelopeVariables
+    :: ScopedCheckedCore ObjectId
+    -> [Raw.VarSymbol]
+    -> Exact.ExactBinderContext
+    -> Prepare
+        ( Exact.ExactBinderContext
+        , ScopedCheckedCore ObjectId
+        , [Exact.ExactLocalId]
+        )
+openEnvelopeVariables target variables preparedContext =
+    case NonEmpty.nonEmpty variables of
+        Nothing ->
+            pure (preparedContext, target, [])
+        Just nonempty -> do
+            (_unannotated, opened, identities) <-
+                openFixedVariables
+                Exact.emptyExactBinderContext
+                target
+                nonempty
+            let expected =
+                    reverse
+                        (fst <$> toList
+                            (Exact.exactBinderContextSupport preparedContext))
+            unless
+                (identities == expected)
+                (impossible
+                    "prepared claim annotations do not match opened binders")
+            pure (preparedContext, opened, identities)
+
+openEnvelopeAntecedents
+    :: Exact.ExactBinderContext
+    -> ScopedCheckedCore ObjectId
+    -> Natural
+    -> Prepare
+        ( [PreparedLocal]
+        , ScopedCheckedCore ObjectId
+        , [ScopedCheckedCore ObjectId]
+        )
+openEnvelopeAntecedents context initialGoal initialCount =
+    go [] [] initialGoal initialCount
+  where
+    go locals antecedents goal 0 =
+        pure (locals, goal, antecedents)
+    go locals antecedents goal remaining = do
+        (antecedent, conclusion) <-
+            maybe
+                (impossible
+                    "a prepared claim envelope has too few implications")
+                pure
+                (openScopedImplication goal)
+        local <- allocateLocal ExactAssumption context antecedent
+        go
+            (locals <> [local])
+            (antecedents <> [antecedent])
+            conclusion
+            (remaining - 1)
+
+prepareInitialSetInductionView
+    :: Raw.Stmt
+    -> Exact.ExactBinderContext
+    -> [Raw.VarSymbol]
+    -> [Exact.ExactLocalId]
+    -> [ScopedCheckedCore ObjectId]
+    -> ScopedCheckedCore ObjectId
+    -> Prepare InitialSetInductionView
+prepareInitialSetInductionView
+        statement context variables identities antecedents bodyGoal = do
+    unless (length variables == length identities)
+        (impossible
+            "opened claim binders lost their source identity association")
+    foci <- traverse checkedFocus (zip variables identities)
+    let property = foldr implyChecked bodyGoal antecedents
+        support = Exact.exactBinderContextSupport context
+    unless
+        ( scopedCoreContext property
+            == (snd <$> Vector.toList support)
+        )
+        (impossible
+            "initial set-induction property changed its checked context")
+    pure
+        (InitialSetInductionView
+            foci support property antecedents bodyGoal
+            (claimLeadingUniversalName statement))
+  where
+    checkedFocus (variable, identity) = do
+        index <-
+            maybe
+                (impossible
+                    "an opened claim binder is absent from its exact context")
+                pure
+                (Exact.exactBinderContextIndex variable context)
+        case Exact.exactBinderContextSupport context
+                Vector.!? (fromIntegral index) of
+            Just (actualIdentity, TySet)
+                | actualIdentity == identity ->
+                    pure
+                        (InitialSetInductionFocus
+                            variable identity index)
+            _ ->
+                impossible
+                    "an initial set-induction focus changed identity or type"
+
+    implyChecked antecedent conclusion =
+        fromMaybe
+            (impossible
+                "an exact claim antecedent changed context")
+            (implyScopedCore antecedent conclusion)
+
+claimLeadingUniversalName :: Raw.Stmt -> Maybe Raw.VarSymbol
+claimLeadingUniversalName = \case
+    Raw.StmtFormula
+            (Raw.FormulaQuantified _location Raw.Universally
+                (variable :| _rest) _bound _formula) ->
+        Just variable
+    Raw.SymbolicForall _location (variable :| _rest)
+            _bound _suchThat _statement ->
+        Just variable
+    Raw.StmtQuantPhrase
+            _location
+            (Raw.QuantPhrase Raw.Universally
+                (Raw.NounPhrase _left _noun variables _right _suchThat))
+            _statement ->
+        listToMaybe variables
+    Raw.StmtVerbPhrase
+            (Raw.TermQuantified Raw.Universally _location
+                (Raw.NounPhrase _left _noun variable _right _suchThat)
+                :| [])
+            _verb ->
+        variable
+    Raw.StmtNoun
+            (Raw.TermQuantified Raw.Universally _location
+                (Raw.NounPhrase _left _noun variable _right _suchThat)
+                :| [])
+            _nounPhrase ->
+        variable
+    _statement ->
+        Nothing
+
+prepareProof
+    :: Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> SetInductionBoundary
+    -> ScopedCheckedCore ObjectId
+    -> Raw.Proof
+    -> Prepare PreparedProof
+prepareProof fallback context locals inductionBoundary goal = \case
+    Raw.Omitted location ->
+        pure (PreparedOmitted location goal)
+    Raw.Qed maybeLocation justification ->
+        PreparedQed
+            <$> prepareDischarge
+                (fromMaybe fallback maybeLocation)
+                context
+                locals
+                goal
+                justification
+    Raw.FixSymbolic location variables bound continuation -> do
+        (context', goal', identities) <-
+            openFixedVariables context goal variables
+        case bound of
+            Raw.Unbounded ->
+                PreparedFix identities
+                    <$> prepareProof
+                        fallback
+                        context'
+                        locals
+                        RecursiveProofInduction
+                        goal'
+                        continuation
+            _ -> do
+                constraint <-
+                    prepareSymbolicBoundConstraints
+                        context' variables bound
+                prepareGuardedFix
+                    fallback location context' locals goal'
+                    identities constraint continuation
+    Raw.FixSuchThat location variables statement continuation -> do
+        (context', goal', identities) <-
+            openFixedVariables context goal variables
+        constraint <-
+            Exact.preparedExactPropositionCore
+                <$> prepareStatement context' statement
+        prepareGuardedFix
+            fallback location context' locals goal'
+            identities constraint continuation
+    Raw.Assume location statement continuation -> do
+        supplied <- prepareStatement context statement
+        when (isNothing (openScopedImplication goal))
+            (throwProof (ExactProofExpectedImplicationGoal location))
+        (assumption, conclusion) <-
+            maybe
+                (throwProof (ExactProofGoalStatementMismatch location))
+                pure
+                (openScopedAssumption
+                    (Exact.preparedExactPropositionCore supplied)
+                    goal)
+        local <- allocateLocal ExactAssumption context assumption
+        PreparedAssume assumption
+            <$> prepareProof
+                fallback
+                context
+                (locals <> [local])
+                RecursiveProofInduction
+                conclusion
+                continuation
+    Raw.TakeVar location variables bound statement justification continuation -> do
+        prepareSymbolicTake
+            fallback location context locals goal variables bound statement
+            justification continuation
+    Raw.TakeNoun location nounPhrase justification continuation ->
+        prepareNounTake
+            fallback location context locals goal nounPhrase
+            justification continuation
+    Raw.BySetInduction location variable continuation ->
+        prepareSetInduction
+            fallback location context locals inductionBoundary goal
+            variable continuation
+    Raw.Have location Nothing
+            (Raw.SymbolicExists _existential variables bound statement)
+            justification continuation ->
+        prepareSymbolicTake
+            fallback location context locals goal variables bound statement
+            justification continuation
+    Raw.Have location Nothing statement justification continuation -> do
+        claim <-
+            Exact.preparedExactPropositionCore
+                <$> prepareStatement context statement
+        discharge <-
+            prepareDischarge
+                location context locals claim justification
+        local <- allocateLocal ExactDerivedClaim context claim
+        PreparedHave claim discharge
+            <$> prepareProof
+                fallback
+                context
+                (locals <> [local])
+                RecursiveProofInduction
+                goal
+                continuation
+    Raw.Have location (Just sinceStatement)
+            statement justification continuation -> do
+        sinceProposition <-
+            Exact.preparedExactPropositionCore
+                <$> prepareStatement context sinceStatement
+        claim <-
+            Exact.preparedExactPropositionCore
+                <$> prepareStatement context statement
+        (evidence, sinceLocals) <-
+            case find (localMatches sinceProposition) locals of
+                Just existing ->
+                    pure (PreparedSinceExisting existing, locals)
+                Nothing -> do
+                    discharge <-
+                        prepareDischarge
+                            location
+                            context
+                            locals
+                            sinceProposition
+                            Raw.JustificationLocal
+                    local <-
+                        allocateLocal
+                            ExactDerivedClaim context sinceProposition
+                    pure
+                        ( PreparedSinceDischarged discharge local
+                        , locals <> [local]
+                        )
+        claimDischarge <-
+            prepareDischarge
+                location context sinceLocals claim justification
+        claimLocal <-
+            allocateLocal ExactDerivedClaim context claim
+        PreparedSince
+            sinceProposition evidence claim claimDischarge
+            <$> prepareProof
+                fallback
+                context
+                (sinceLocals <> [claimLocal])
+                RecursiveProofInduction
+                goal
+                continuation
+    Raw.Suffices location statement justification continuation -> do
+        reduction <-
+            Exact.preparedExactPropositionCore
+                <$> prepareStatement context statement
+        implication <-
+            maybe
+                (impossible
+                    "a checked suffices reduction changed lexical context")
+                pure
+                (implyScopedCore reduction goal)
+        discharge <-
+            prepareDischarge
+                location context locals implication justification
+        PreparedSuffices goal reduction implication discharge
+            <$> prepareProof
+                fallback
+                context
+                locals
+                (SourceStatementInduction
+                    (claimLeadingUniversalName statement))
+                reduction
+                continuation
+    Raw.Calc location quantifier calculation continuation -> do
+        prepared <-
+            prepareCalculation
+                location context locals quantifier calculation
+        local <-
+            allocateLocal
+                ExactDerivedClaim
+                context
+                (preparedCalculationResult prepared)
+        PreparedCalculate prepared
+            <$> prepareProof
+                fallback
+                context
+                (locals <> [local])
+                RecursiveProofInduction
+                goal
+                continuation
+    Raw.Subclaim location statement subproof continuation -> do
+        claim <-
+            Exact.preparedExactPropositionCore
+                <$> prepareStatement context statement
+        preparedSubproof <-
+            prepareProof
+                location
+                context
+                locals
+                (SourceStatementInduction
+                    (claimLeadingUniversalName statement))
+                claim
+                subproof
+        local <- allocateLocal ExactDerivedClaim context claim
+        PreparedSubclaim claim preparedSubproof
+            <$> prepareProof
+                fallback
+                context
+                (locals <> [local])
+                RecursiveProofInduction
+                goal
+                continuation
+    Raw.Define location variable expression continuation -> do
+        preparedBody <-
+            liftDriver
+                (Exact.prepareExactSetExpression context expression)
+                >>= either
+                    (throwProof . ExactProofElaborationFailed)
+                    pure
+        let body = Exact.preparedExactSetExpressionCore preparedBody
+        identity <- allocateLocalIdentity
+        context' <-
+            either
+                (throwProof . ExactProofElaborationFailed)
+                pure
+                (Exact.extendExactBinderContext
+                    ((identity, variable) :| [])
+                    context)
+        case Exact.preparedExactSetExpressionConstruction preparedBody of
+            Nothing -> do
+                separationCharacteristic <-
+                    liftDriver
+                        (Declaration.currentFoundationAxiomLowering
+                            SeparationCharacteristic)
+                definition <-
+                    maybe
+                        (impossible
+                            "an exact set expression did not form a local definition")
+                        pure
+                        (scopedSetDefinition separationCharacteristic body)
+                local <-
+                    allocateLocal ExactLocalDefinition context' definition
+                PreparedDefine identity body (definition :| [])
+                    <$> prepareProof
+                        fallback context' (locals <> [local])
+                        RecursiveProofInduction
+                        (weakenCheckedScopedCore TySet goal)
+                        continuation
+            Just (Exact.PreparedUnconditionalSetConstruction construction) -> do
+                characteristics <- prepareConstructionFoundation
+                (extensional, equation) <-
+                    maybe
+                        (impossible
+                            "a checked named construction has no definition views")
+                        pure
+                        (namedSetConstructionLocalViews
+                            characteristics construction)
+                extensionalLocal <-
+                    allocateLocal
+                        ExactLocalConstructionExtensional context' extensional
+                equationLocal <-
+                    allocateLocal
+                        ExactLocalConstructionEquation context' equation
+                PreparedDefine identity body (extensional :| [equation])
+                    <$> prepareProof
+                        fallback context'
+                        (locals <> [extensionalLocal, equationLocal])
+                        RecursiveProofInduction
+                        (weakenCheckedScopedCore TySet goal)
+                        continuation
+            Just (Exact.PreparedRelationalSetConstruction construction) -> do
+                characteristics <- prepareConstructionFoundation
+                let functionality =
+                        relationalSetConstructionFunctionality construction
+                discharge <-
+                    prepareDischarge
+                        location context locals functionality
+                        Raw.JustificationEmpty
+                (extensional, equation) <-
+                    maybe
+                        (impossible
+                            "a checked relational construction has no admitted definition views")
+                        pure
+                        (relationalSetConstructionLocalViews
+                            characteristics construction functionality)
+                extensionalLocal <-
+                    allocateLocal
+                        ExactLocalConstructionExtensional context' extensional
+                equationLocal <-
+                    allocateLocal
+                        ExactLocalConstructionEquation context' equation
+                PreparedDefineRelational
+                    identity body discharge (extensional :| [equation])
+                    <$> prepareProof
+                        fallback context'
+                        (locals <> [extensionalLocal, equationLocal])
+                        RecursiveProofInduction
+                        (weakenCheckedScopedCore TySet goal)
+                        continuation
+    Raw.DefineFunction
+            location function argument value bound domain continuation -> do
+        unless (argument == bound)
+            (throwProof
+                (ExactProofLocalFunctionBinderMismatch (locate bound)))
+        when (function == argument)
+            (throwProof
+                (ExactProofLocalFunctionNameConflict (locate function)))
+        argumentIdentity <- allocateLocalIdentity
+        argumentContext <-
+            either
+                (throwProof . ExactProofElaborationFailed)
+                pure
+                (Exact.extendExactBinderContext
+                    ((argumentIdentity, argument) :| [])
+                    context)
+        graph <-
+            liftDriver
+                (Exact.prepareExactLocalFunctionGraph
+                    location context argumentContext domain value)
+                >>= either
+                    (throwProof . ExactProofElaborationFailed)
+                    pure
+        functionIdentity <- allocateLocalIdentity
+        functionContext <-
+            either
+                (throwProof . ExactProofElaborationFailed)
+                pure
+                (Exact.extendExactBinderContext
+                    ((functionIdentity, function) :| [])
+                    context)
+        replacementCharacteristic <-
+            liftDriver
+                (Declaration.currentFoundationAxiomLowering
+                    ReplacementCharacteristic)
+        definition <-
+            maybe
+                (impossible
+                    "a checked replacement graph did not form a local definition")
+                pure
+                (scopedCharacteristicDefinition
+                    replacementCharacteristic
+                    (Exact.preparedExactLocalFunctionGraphCore graph)
+                    ( Exact.preparedExactLocalFunctionGraphDomain graph
+                        :| [Exact.preparedExactLocalFunctionGraphMap graph]
+                    ))
+        local <-
+            allocateLocal ExactLocalDefinition functionContext definition
+        PreparedDefineFunction
+            functionIdentity
+            (Exact.preparedExactLocalFunctionGraphCore graph)
+            definition
+            <$> prepareProof
+                fallback
+                functionContext
+                (locals <> [local])
+                RecursiveProofInduction
+                (weakenCheckedScopedCore TySet goal)
+                continuation
+    Raw.ByCase location sourceCases ->
+        prepareByCase
+            location context locals goal sourceCases
+    Raw.ByContradiction location continuation -> do
+        let falsum = falsumScopedCore (scopedCoreContext goal)
+        negation <-
+            maybe
+                (structuralFailure
+                    location
+                    "proof by contradiction requires a proposition goal")
+                pure
+                (negateScopedCore goal)
+        local <- allocateLocal ExactAssumption context negation
+        prepared <-
+            prepareProof
+                location
+                context
+                (locals <> [local])
+                RecursiveProofInduction
+                falsum
+                continuation
+        validateStructuralComposition
+            location [goal, negation, falsum]
+            (\foundation globalType ->
+                KernelProof.validateDoubleNegationComposition
+                    foundation globalType goal negation falsum)
+        pure
+            (PreparedByContradiction
+                goal negation falsum prepared)
+    Raw.Contradiction location justification -> do
+        let falsum = falsumScopedCore (scopedCoreContext goal)
+        discharge <-
+            prepareDischarge
+                location
+                context
+                locals
+                falsum
+                justification
+        validateStructuralComposition
+            location [goal, falsum]
+            (\foundation globalType ->
+                KernelProof.validateFalsumEliminationComposition
+                    foundation globalType goal falsum)
+        pure (PreparedContradiction goal falsum discharge)
+    proof ->
+        throwProof
+            (ExactProofUnsupportedStep
+                (proofLocation fallback proof))
+  where
+    localMatches proposition
+            (PreparedLocal _ordinal _origin _support local) =
+        local == proposition
+
+prepareSetInduction
+    :: Location
+    -> Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> SetInductionBoundary
+    -> ScopedCheckedCore ObjectId
+    -> Maybe Raw.Term
+    -> Raw.Proof
+    -> Prepare PreparedProof
+prepareSetInduction
+        fallback location context locals boundary goal sourceFocus
+        continuation = do
+    selected <-
+        selectSetInductionFocus
+            location context boundary goal sourceFocus
+    case selected of
+        SelectedInitialSetInduction
+                (InitialSetInductionFocus _variable identity index) -> do
+            (foci, expectedSupport, property, antecedents, childTarget) <-
+                case boundary of
+                    InitialClaimInduction
+                            (InitialSetInductionView
+                                foundFoci support foundProperty
+                                foundAntecedents foundTarget _leadingName) ->
+                        pure
+                            ( foundFoci
+                            , support
+                            , foundProperty
+                            , foundAntecedents
+                            , foundTarget
+                            )
+                    RecursiveProofInduction ->
+                        impossible
+                            "an initial induction focus escaped its claim boundary"
+                    SourceStatementInduction _leadingName ->
+                        impossible
+                            "an initial induction focus escaped its claim boundary"
+            unless
+                ( Exact.exactBinderContextSupport context == expectedSupport
+                    && goal == childTarget
+                    && any (sameInitialFocus identity index) foci
+                )
+                (throwProof
+                    (ExactProofSetInductionGoalMismatch location))
+            PreparedSetInduction
+                <$> prepareCheckedSetInduction
+                    fallback location context locals
+                    (PreparedInitialSetInductionFocus identity index)
+                    index property antecedents childTarget continuation
+        SelectedLeadingSetInduction sourceName -> do
+            (binderType, property) <-
+                maybe
+                    (throwProof
+                        (ExactProofSetInductionGoalMismatch location))
+                    pure
+                    (openScopedForall goal)
+            unless (binderType == TySet)
+                (throwProof
+                    (ExactProofSetInductionGoalMismatch location))
+            identity <- allocateLocalIdentity
+            extendedContext <-
+                either
+                    (throwProof . ExactProofElaborationFailed)
+                    pure
+                    (case sourceName of
+                        Just variable ->
+                            Exact.extendExactBinderContext
+                                ((identity, variable) :| [])
+                                context
+                        Nothing ->
+                            Exact.extendExactAnonymousBinderContext
+                                identity context)
+            let expectedResult = weakenCheckedScopedCore TySet goal
+            prepared <- prepareCheckedSetInduction
+                fallback location extendedContext locals
+                (PreparedLeadingSetInductionFocus identity)
+                0 property [] property continuation
+            unless
+                (preparedSetInductionResult prepared == expectedResult)
+                (throwProof
+                    (ExactProofSetInductionGoalMismatch location))
+            pure (PreparedSetInduction prepared)
+  where
+    sameInitialFocus expectedIdentity expectedIndex
+            (InitialSetInductionFocus _variable identity index) =
+        identity == expectedIdentity && index == expectedIndex
+
+prepareCheckedSetInduction
+    :: Location
+    -> Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> PreparedSetInductionFocus
+    -> Natural
+    -> ScopedCheckedCore ObjectId
+    -> [ScopedCheckedCore ObjectId]
+    -> ScopedCheckedCore ObjectId
+    -> Raw.Proof
+    -> Prepare PreparedSetInduction
+prepareCheckedSetInduction
+        fallback location context locals focus selected property antecedents
+        childTarget continuation = do
+    (_predicate, hypothesis, _step, result) <-
+        maybe
+            (throwProof
+                (ExactProofSetInductionGoalMismatch location))
+            pure
+            (scopedSetInductionInstance selected property)
+    validateStructuralComposition
+        location
+        (property : hypothesis : result : childTarget : antecedents)
+        (\foundation globalType ->
+            KernelProof.validateSetInductionComposition
+                foundation globalType selected property antecedents
+                childTarget hypothesis result)
+    local <- allocateLocal ExactAssumption context hypothesis
+    child <-
+        prepareProof
+            fallback
+            context
+            (locals <> [local])
+            RecursiveProofInduction
+            childTarget
+            continuation
+    pure
+        (PreparedCheckedSetInduction
+            focus property antecedents childTarget hypothesis result child)
+
+preparedSetInductionResult
+    :: PreparedSetInduction
+    -> ScopedCheckedCore ObjectId
+preparedSetInductionResult
+        (PreparedCheckedSetInduction
+            _focus _property _antecedents _target _hypothesis result _child) =
+    result
+
+selectSetInductionFocus
+    :: Location
+    -> Exact.ExactBinderContext
+    -> SetInductionBoundary
+    -> ScopedCheckedCore ObjectId
+    -> Maybe Raw.Term
+    -> Prepare SelectedSetInductionFocus
+selectSetInductionFocus location context boundary goal sourceFocus = do
+    explicit <- traverse simpleVariable sourceFocus
+    let (initialFoci, retainedLeadingName) =
+            case boundary of
+                InitialClaimInduction
+                        (InitialSetInductionView
+                            foci _support _property _antecedents _target
+                            leadingName) ->
+                    (foci, leadingName)
+                SourceStatementInduction leadingName ->
+                    ([], leadingName)
+                RecursiveProofInduction ->
+                    ([], Nothing)
+        leadingAvailable =
+            case openScopedForall goal of
+                Just (TySet, _body) -> True
+                _ -> False
+    case explicit of
+        Just variable ->
+            case find (initialNamed variable) initialFoci of
+                Just focus ->
+                    pure (SelectedInitialSetInduction focus)
+                Nothing
+                    | leadingAvailable
+                    , isJust
+                        (Exact.exactBinderContextIndex variable context) ->
+                        throwProof
+                            (ExactProofSetInductionBinderConflict
+                                location variable)
+                    | leadingAvailable ->
+                        pure
+                            (SelectedLeadingSetInduction
+                                (Just variable))
+                    | isJust
+                        (Exact.exactBinderContextIndex variable context) ->
+                        throwProof
+                            (ExactProofSetInductionActiveBinderIneligible
+                                location variable)
+                    | otherwise ->
+                        throwProof
+                            (ExactProofSetInductionVariableNotActive
+                                location variable)
+        Nothing ->
+            case
+                ( (SelectedInitialSetInduction <$> initialFoci)
+                    <> [ SelectedLeadingSetInduction retainedLeadingName
+                       | leadingAvailable
+                       ]
+                ) of
+                [only] -> pure only
+                _ ->
+                    throwProof
+                        (ExactProofSetInductionFocusAmbiguous location)
+  where
+    simpleVariable = \case
+        Raw.TermExpr (Raw.ExprVar variable) ->
+            pure variable
+        _term ->
+            throwProof
+                (ExactProofSetInductionVariableRequired location)
+
+    initialNamed variable
+            (InitialSetInductionFocus candidate _identity _index) =
+        candidate == variable
+
+prepareByCase
+    :: Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> ScopedCheckedCore ObjectId
+    -> [Raw.Case]
+    -> Prepare PreparedProof
+prepareByCase location context locals goal sourceCases = do
+    cases <-
+        maybe
+            (throwProof (ExactProofEmptyCaseSplit location))
+            (traverse prepareCase)
+            (NonEmpty.nonEmpty sourceCases)
+    exhaustive <-
+        foldM disjoin
+            (preparedCaseAssumption (NonEmpty.head cases))
+            (preparedCaseAssumption <$> NonEmpty.tail cases)
+    discharge <-
+        prepareDischarge
+            location context locals exhaustive Raw.JustificationEmpty
+    validateStructuralComposition
+        location
+        (goal : exhaustive : (preparedCaseAssumption <$> toList cases))
+        (\foundation globalType ->
+            KernelProof.validateCaseAnalysisComposition
+                foundation
+                globalType
+                goal
+                (preparedCaseAssumption <$> cases)
+                exhaustive)
+    pure
+        (PreparedByCase
+            (PreparedCaseAnalysis goal cases exhaustive discharge))
+  where
+    prepareCase (Raw.Case statement child) = do
+        assumption <-
+            Exact.preparedExactPropositionCore
+                <$> prepareStatement context statement
+        local <- allocateLocal ExactAssumption context assumption
+        prepared <-
+            prepareProof
+                (locate statement)
+                context
+                (locals <> [local])
+                RecursiveProofInduction
+                goal
+                child
+        pure (PreparedCase assumption prepared)
+
+    disjoin left right =
+        maybe
+            (structuralFailure
+                location
+                "case assumptions changed type or lexical context")
+            pure
+            (disjoinScopedCore left right)
+
+preparedCaseAssumption
+    :: PreparedCase
+    -> ScopedCheckedCore ObjectId
+preparedCaseAssumption (PreparedCase assumption _proof) =
+    assumption
+
+preparedCaseProof :: PreparedCase -> PreparedProof
+preparedCaseProof (PreparedCase _assumption proof) =
+    proof
+
+prepareGuardedFix
+    :: Location
+    -> Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> ScopedCheckedCore ObjectId
+    -> [Exact.ExactLocalId]
+    -> ScopedCheckedCore ObjectId
+    -> Raw.Proof
+    -> Prepare PreparedProof
+prepareGuardedFix
+        fallback location context locals goal identities constraint continuation = do
+    (antecedent, conclusion) <-
+        maybe
+            (throwProof (ExactProofExpectedImplicationGoal location))
+            pure
+            (openScopedImplication goal)
+    unless (constraint == antecedent)
+        (throwProof (ExactProofGoalStatementMismatch location))
+    local <- allocateLocal ExactAssumption context constraint
+    prepared <-
+        prepareProof
+            fallback
+            context
+            (locals <> [local])
+            RecursiveProofInduction
+            conclusion
+            continuation
+    pure (PreparedFix identities (PreparedAssume constraint prepared))
+
+prepareCalculation
+    :: Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> Maybe Raw.CalcQuantifier
+    -> Raw.Calc
+    -> Prepare PreparedCalculation
+prepareCalculation location context locals quantifier calculation = do
+    (identities, calculationContext, calculationGuard) <-
+        prepareCalculationScope context quantifier
+    case calculation of
+        Raw.Equation first destinations -> do
+            firstChecked <- prepareSetEndpoint calculationContext first
+            checkedDestinations <-
+                traverse
+                    (\(destination, justification) -> do
+                        checked <-
+                            prepareSetEndpoint calculationContext destination
+                        pure
+                            ( locate destination
+                            , checked
+                            , justification
+                            ))
+                    destinations
+            finishCalculation
+                location context locals TySet identities calculationGuard
+                firstChecked checkedDestinations
+        Raw.Biconditionals first destinations -> do
+            firstChecked <- preparePropositionEndpoint calculationContext first
+            checkedDestinations <-
+                traverse
+                    (\(destination, justification) -> do
+                        checked <-
+                            preparePropositionEndpoint
+                                calculationContext destination
+                        pure
+                            ( locate destination
+                            , checked
+                            , justification
+                            ))
+                    destinations
+            finishCalculation
+                location context locals TyProp identities calculationGuard
+                firstChecked checkedDestinations
+  where
+    prepareSetEndpoint endpointContext expression =
+        Exact.preparedExactSetExpressionCore
+            <$> ( liftDriver
+                    (Exact.prepareExactSetExpression
+                        endpointContext expression)
+                    >>= either
+                        (throwProof . ExactProofElaborationFailed)
+                        pure
+                )
+
+    preparePropositionEndpoint endpointContext formula =
+        Exact.preparedExactPropositionCore
+            <$> prepareStatement endpointContext (Raw.StmtFormula formula)
+
+prepareCalculationScope
+    :: Exact.ExactBinderContext
+    -> Maybe Raw.CalcQuantifier
+    -> Prepare
+        ( [Exact.ExactLocalId]
+        , Exact.ExactBinderContext
+        , Maybe (ScopedCheckedCore ObjectId)
+        )
+prepareCalculationScope context = \case
+    Nothing ->
+        pure ([], context, Nothing)
+    Just (Raw.CalcQuantifier variables bound suchThat) -> do
+        identities <- traverse (const allocateLocalIdentity) variables
+        calculationContext <-
+            either
+                (throwProof . ExactProofElaborationFailed)
+                pure
+                (Exact.extendExactBinderContext
+                    (NonEmpty.zip identities variables)
+                    context)
+        boundGuard <-
+            prepareSymbolicBoundConstraints
+                calculationContext variables bound
+        suchThatGuard <-
+            traverse
+                (fmap Exact.preparedExactPropositionCore
+                    . prepareStatement calculationContext)
+                suchThat
+        calculationGuard <-
+            normalizeCalculationGuard
+                (boundGuard : maybeToList suchThatGuard)
+        pure (toList identities, calculationContext, calculationGuard)
+
+normalizeCalculationGuard
+    :: [ScopedCheckedCore ObjectId]
+    -> Prepare (Maybe (ScopedCheckedCore ObjectId))
+normalizeCalculationGuard guards =
+    foldM add Nothing guards
+  where
+    add accumulated constraint
+        | isScopedTruth constraint = pure accumulated
+        | otherwise =
+            case accumulated of
+                Nothing -> pure (Just constraint)
+                Just previous ->
+                    Just
+                        <$> maybe
+                            (impossible
+                                "checked calculation guards changed context")
+                            pure
+                            (conjoinScopedCore previous constraint)
+
+    isScopedTruth proposition =
+        scopedCoreType proposition == TyProp
+            && scopedCoreTerm proposition == CImp CFalsum CFalsum
+
+finishCalculation
+    :: Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> CoreType
+    -> [Exact.ExactLocalId]
+    -> Maybe (ScopedCheckedCore ObjectId)
+    -> ScopedCheckedCore ObjectId
+    -> NonEmpty
+        ( Location
+        , ScopedCheckedCore ObjectId
+        , Raw.Justification
+        )
+    -> Prepare PreparedCalculation
+finishCalculation
+        fallback context locals operandType identities calculationGuard
+        first destinations = do
+    links <- prepareCalculationLinks first destinations
+    let finalEndpoint = preparedCalculationLinkDestination (NonEmpty.last links)
+    resultOpen <-
+        calculationEquality first finalEndpoint
+    result <-
+        closeCalculationProposition identities calculationGuard resultOpen
+    pure
+        (PreparedCheckedCalculation
+            operandType identities calculationGuard first links result)
+  where
+    prepareCalculationLinks previous (destination :| rest) = do
+        (next, firstLink) <- prepareCalculationLink previous destination
+        later <- prepareRemainingCalculationLinks next rest
+        pure (firstLink :| later)
+
+    prepareRemainingCalculationLinks _previous [] =
+        pure []
+    prepareRemainingCalculationLinks previous (destination : rest) = do
+        (next, link) <- prepareCalculationLink previous destination
+        (link :) <$> prepareRemainingCalculationLinks next rest
+
+    prepareCalculationLink previous
+            (destinationLocation, destination, justification) = do
+            linkOpen <- calculationEquality previous destination
+            link <- closeCalculationProposition
+                identities calculationGuard linkOpen
+            discharge <-
+                prepareDischarge
+                    (if destinationLocation == Nowhere
+                        then fallback
+                        else destinationLocation)
+                    context
+                    locals
+                    link
+                    justification
+            pure
+                ( destination
+                , PreparedCalculationLink destination discharge
+                )
+
+    calculationEquality left right =
+        maybe
+            (impossible
+                "checked calculation endpoints changed type or context")
+            pure
+            (equalScopedCore left right)
+
+closeCalculationProposition
+    :: [Exact.ExactLocalId]
+    -> Maybe (ScopedCheckedCore ObjectId)
+    -> ScopedCheckedCore ObjectId
+    -> Prepare (ScopedCheckedCore ObjectId)
+closeCalculationProposition identities calculationGuard proposition = do
+    guarded <-
+        case calculationGuard of
+            Nothing -> pure proposition
+            Just constraint ->
+                maybe
+                    (impossible
+                        "a checked calculation guard changed context")
+                    pure
+                    (implyScopedCore constraint proposition)
+    pure (closeBinders (length identities) guarded)
+  where
+    closeBinders 0 closed = closed
+    closeBinders remaining open =
+        closeBinders (remaining - 1)
+            (fromMaybe
+                (impossible
+                    "a checked calculation lost a quantified binder")
+                (closeScopedForall open))
+
+preparedCalculationResult
+    :: PreparedCalculation
+    -> ScopedCheckedCore ObjectId
+preparedCalculationResult
+        (PreparedCheckedCalculation
+            _operandType _identities _guard _first _links result) =
+    result
+
+preparedCalculationLinkDestination
+    :: PreparedCalculationLink
+    -> ScopedCheckedCore ObjectId
+preparedCalculationLinkDestination
+        (PreparedCalculationLink destination _discharge) =
+    destination
+
+preparedCalculationLinkDischarge
+    :: PreparedCalculationLink
+    -> PreparedDischarge
+preparedCalculationLinkDischarge
+        (PreparedCalculationLink _destination discharge) =
+    discharge
+
+preparedDischargeGoal
+    :: PreparedDischarge
+    -> ScopedCheckedCore ObjectId
+preparedDischargeGoal = \case
+    PreparedVampireDischarge _location _justification goal _obligation ->
+        goal
+    PreparedSetExtensionality _location goal ->
+        goal
+
+prepareSymbolicBoundConstraints
+    :: Exact.ExactBinderContext
+    -> NonEmpty Raw.VarSymbol
+    -> Raw.Bound
+    -> Prepare (ScopedCheckedCore ObjectId)
+prepareSymbolicBoundConstraints context variables bound =
+    Exact.preparedExactPropositionCore
+        <$> ( liftDriver
+                (Exact.prepareExactSymbolicBoundConstraints
+                    context variables bound)
+                >>= either
+                    (throwProof . ExactProofElaborationFailed)
+                    pure
+            )
+
+prepareSymbolicTake
+    :: Location
+    -> Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> ScopedCheckedCore ObjectId
+    -> NonEmpty Raw.VarSymbol
+    -> Raw.Bound
+    -> Raw.Stmt
+    -> Raw.Justification
+    -> Raw.Proof
+    -> Prepare PreparedProof
+prepareSymbolicTake
+        fallback location context locals goal variables bound statement
+        justification continuation = do
+    identities <- traverse (const allocateLocalIdentity) variables
+    context' <-
+        either
+            (throwProof . ExactProofElaborationFailed)
+            pure
+            (Exact.extendExactBinderContext
+                (NonEmpty.zip identities variables)
+                context)
+    witness <-
+        Exact.preparedExactPropositionCore
+            <$> ( liftDriver
+                    (Exact.prepareExactSymbolicWitnessConstraints
+                        context' variables bound statement)
+                    >>= either
+                        (throwProof . ExactProofElaborationFailed)
+                        pure
+                )
+    prepareTake
+        fallback location context locals goal context'
+        (toList identities) witness justification continuation
+
+prepareNounTake
+    :: Location
+    -> Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> ScopedCheckedCore ObjectId
+    -> Raw.NounPhrase []
+    -> Raw.Justification
+    -> Raw.Proof
+    -> Prepare PreparedProof
+prepareNounTake
+        fallback location context locals goal nounPhrase
+        justification continuation = do
+    (identities, context') <-
+        case nounPhrase of
+            Raw.NounPhrase _left _noun variables _right _suchThat ->
+                case NonEmpty.nonEmpty variables of
+                    Just binders -> do
+                        identities <-
+                            traverse (const allocateLocalIdentity) binders
+                        context' <-
+                            either
+                                (throwProof . ExactProofElaborationFailed)
+                                pure
+                                (Exact.extendExactBinderContext
+                                    (NonEmpty.zip identities binders)
+                                    context)
+                        pure (toList identities, context')
+                    Nothing -> do
+                        identity <- allocateLocalIdentity
+                        context' <-
+                            either
+                                (throwProof . ExactProofElaborationFailed)
+                                pure
+                                (Exact.extendExactAnonymousBinderContext
+                                    identity context)
+                        pure ([identity], context')
+    witness <-
+        Exact.preparedExactPropositionCore
+            <$> ( liftDriver
+                    (Exact.prepareExactNounWitnessConstraints
+                        context' nounPhrase)
+                    >>= either
+                        (throwProof . ExactProofElaborationFailed)
+                        pure
+                )
+    prepareTake
+        fallback location context locals goal context'
+        identities witness justification continuation
+
+prepareTake
+    :: Location
+    -> Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> ScopedCheckedCore ObjectId
+    -> Exact.ExactBinderContext
+    -> [Exact.ExactLocalId]
+    -> ScopedCheckedCore ObjectId
+    -> Raw.Justification
+    -> Raw.Proof
+    -> Prepare PreparedProof
+prepareTake
+        fallback location context locals goal witnessContext
+        identities witness justification continuation = do
+    let witnessCount = length identities
+        existence = closeTakenWitnesses witnessCount witness
+        goal' = weakenForTakenWitnesses witnessCount goal
+    discharge <-
+        prepareDischarge
+            location context locals existence justification
+    local <- allocateLocal ExactAssumption witnessContext witness
+    PreparedTake identities witness discharge
+        <$> prepareProof
+            fallback
+            witnessContext
+            (locals <> [local])
+            RecursiveProofInduction
+            goal'
+            continuation
+
+-- The discharged existential and the opened witness premise are the same
+-- checked proposition viewed on opposite sides of existential elimination.
+closeTakenWitnesses
+    :: Int
+    -> ScopedCheckedCore ObjectId
+    -> ScopedCheckedCore ObjectId
+closeTakenWitnesses binderCount = go binderCount
+  where
+    go 0 proposition = proposition
+    go remaining proposition =
+        go (remaining - 1)
+            (fromMaybe
+                (impossible "a taken witness has no checked binder")
+                (closeScopedExists proposition))
+
+weakenForTakenWitnesses
+    :: Int
+    -> ScopedCheckedCore ObjectId
+    -> ScopedCheckedCore ObjectId
+weakenForTakenWitnesses binderCount = go binderCount
+  where
+    go 0 proposition = proposition
+    go remaining proposition =
+        go (remaining - 1)
+            (weakenCheckedScopedCore TySet proposition)
+
+openFixedVariables
+    :: Exact.ExactBinderContext
+    -> ScopedCheckedCore ObjectId
+    -> NonEmpty Raw.VarSymbol
+    -> Prepare
+        ( Exact.ExactBinderContext
+        , ScopedCheckedCore ObjectId
+        , [Exact.ExactLocalId]
+        )
+openFixedVariables initialContext initialGoal variables =
+    foldM openOne
+        (initialContext, initialGoal, [])
+        (toList variables)
+  where
+    openOne (context, goal, identities) variable = do
+        (binderType, body) <-
+            maybe
+                (throwProof
+                    (ExactProofExpectedUniversalGoal
+                        (locate variable)))
+                pure
+                (openScopedForall goal)
+        unless (binderType == TySet)
+            (throwProof
+                (ExactProofExpectedUniversalGoal
+                    (locate variable)))
+        identity <- allocateLocalIdentity
+        context' <-
+            either
+                (throwProof . ExactProofElaborationFailed)
+                pure
+                (Exact.extendExactBinderContext
+                    ((identity, variable) :| [])
+                    context)
+        pure (context', body, identities <> [identity])
+
+allocateLocalIdentity :: Prepare Exact.ExactLocalId
+allocateLocalIdentity = do
+    state <- State.get
+    State.put
+        state
+            { prepareNextLocal = prepareNextLocal state + 1
+            }
+    pure (Exact.exactLocalId (prepareNextLocal state))
+
+allocateLocal
+    :: ExactLocalOrigin
+    -> Exact.ExactBinderContext
+    -> ScopedCheckedCore ObjectId
+    -> Prepare PreparedLocal
+allocateLocal origin context proposition = do
+    state <- State.get
+    State.put
+        state
+            { prepareNextPremise = prepareNextPremise state + 1
+            }
+    pure
+        (PreparedLocal
+            (Backend.localPremiseOrdinal
+                (prepareNextPremise state))
+            origin
+            (Exact.exactBinderContextSupport context)
+            proposition)
+
+prepareConstructionFoundation
+    :: Prepare SetConstructionFoundation
+prepareConstructionFoundation = do
+    familyUnion <- foundation FamilyUnionCharacteristic
+    separation <- foundation SeparationCharacteristic
+    replacement <- foundation ReplacementCharacteristic
+    setChoose <- foundation SetChooseWitness
+    pure
+        (setConstructionFoundation
+            familyUnion separation replacement setChoose)
+  where
+    foundation tag =
+        liftDriver
+            (Declaration.currentFoundationAxiomLowering tag)
+
+prepareDischarge
+    :: Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> ScopedCheckedCore ObjectId
+    -> Raw.Justification
+    -> Prepare PreparedDischarge
+prepareDischarge location context locals goal justification =
+    prepareDischargeWith
+        (dischargeModeFor goal)
+        [] Nothing location context locals goal justification
+
+-- A contradictory-axioms answer can establish falsum, but never an unrelated
+-- proposition directly. Derive that distinction from the checked target so
+-- every surface proof spelling reaches the same guarded request path.
+dischargeModeFor :: ScopedCheckedCore ObjectId -> DischargeMode
+dischargeModeFor goal
+    | scopedCoreType goal == TyProp
+    , scopedCoreTerm goal == CFalsum =
+        IndirectContradictionDischarge
+    | otherwise =
+        DirectDischarge
+
+data DischargeMode
+    = DirectDischarge
+    | IndirectContradictionDischarge
+
+prepareDischargeWith
+    :: DischargeMode
+    -> [FoundationAxiomTag]
+    -> Maybe Declaration.VampirePremiseSelection
+    -> Location
+    -> Exact.ExactBinderContext
+    -> [PreparedLocal]
+    -> ScopedCheckedCore ObjectId
+    -> Raw.Justification
+    -> Prepare PreparedDischarge
+prepareDischargeWith
+        dischargeMode auxiliaries selectionOverride
+        location context locals goal justification =
+    case justification of
+        Raw.JustificationSetExt -> do
+            (leftToRight, rightToLeft) <-
+                maybe
+                    (throwProof
+                        (ExactProofSetExtensionalityGoalMismatch location))
+                    pure
+                    (splitScopedSetEquality goal)
+            unless
+                ( hasDerivedLocal leftToRight
+                    && hasDerivedLocal rightToLeft
+                )
+                (throwProof
+                    (ExactProofSetExtensionalityDirectionsUnavailable
+                        location))
+            pure (PreparedSetExtensionality location goal)
+        _ -> do
+            preparedJustification <-
+                prepareJustification location justification
+            prepared <-
+                liftDriver
+                    (prepareObligation
+                        (Exact.exactBinderContextSupport context)
+                        goal
+                        (toScopedPremise <$> locals)
+                        auxiliaries
+                        (fromMaybe
+                            (vampirePremiseSelection preparedJustification)
+                            selectionOverride))
+                    >>= either
+                        (throwProof
+                            . ExactProofObligationPreparationFailed location)
+                        pure
+            pure
+                (PreparedVampireDischarge
+                    location
+                    preparedJustification
+                    goal
+                    prepared)
+  where
+    prepareObligation =
+        case dischargeMode of
+            DirectDischarge ->
+                Declaration.prepareScopedVampireObligationLowering
+            IndirectContradictionDischarge ->
+                Declaration.prepareScopedContradictionObligationLowering
+
+    hasDerivedLocal proposition =
+        any
+            (\case
+                PreparedLocal
+                        _ordinal ExactDerivedClaim _support local ->
+                    local == proposition
+                PreparedLocal{} ->
+                    False)
+            locals
+
+    toScopedPremise
+            (PreparedLocal ordinal origin support proposition) =
+        Declaration.scopedVampirePremise
+            ordinal origin support proposition
+
+prepareJustification
+    :: Location
+    -> Raw.Justification
+    -> Prepare PreparedJustification
+prepareJustification _location Raw.JustificationEmpty =
+    pure PreparedAuto
+prepareJustification location (Raw.JustificationRef markers) = do
+    resolved <- traverse (resolveReference location) (toList markers)
+    let unique = stableUnique resolved
+    case unique of
+        [] ->
+            impossible "a nonempty citation list resolved to no facts"
+        first : rest ->
+            pure (PreparedReferences (first :| rest))
+prepareJustification _location Raw.JustificationLocal =
+    pure PreparedLocalOnly
+prepareJustification location Raw.JustificationSetExt =
+    throwProof (ExactProofUnsupportedStep location)
+
+vampirePremiseSelection
+    :: PreparedJustification
+    -> Declaration.VampirePremiseSelection
+vampirePremiseSelection = \case
+    PreparedAuto ->
+        Declaration.VampireImplicitPremises
+    PreparedReferences fingerprints ->
+        Declaration.VampireExplicitPremises fingerprints
+    PreparedLocalOnly ->
+        Declaration.VampireLocalPremises
+
+resolveReference
+    :: Location
+    -> Raw.Marker
+    -> Prepare SemanticFactOccurrenceFingerprint
+resolveReference location marker@(Raw.Marker name) = do
+    resolved <-
+        liftDriver
+            (Declaration.resolveVisibleFactAliasLowering
+                (semanticName name))
+    maybe
+        (throwProof
+            (ExactProofUnknownReference location marker))
+        pure
+        resolved
+
+prepareStatement
+    :: Exact.ExactBinderContext
+    -> Raw.Stmt
+    -> Prepare Exact.PreparedExactProposition
+prepareStatement context statement =
+    liftDriver
+        (Exact.prepareExactProposition context statement)
+        >>= either
+            (throwProof . ExactProofElaborationFailed)
+            pure
+
+validateStructuralComposition
+    :: Location
+    -> [ScopedCheckedCore ObjectId]
+    -> ( CheckedFoundation
+         -> (ObjectId -> Maybe CoreType)
+         -> Either KernelProof.KernelProofBuildError ()
+       )
+    -> Prepare ()
+validateStructuralComposition location propositions validate = do
+    foundation <-
+        liftDriver Declaration.currentFoundationLowering
+    let identities =
+            Set.toAscList
+                (Set.unions
+                    ( canonicalTermGlobals . scopedCoreTerm
+                        <$> propositions
+                    ))
+    types <-
+        traverse
+            (\identity -> do
+                coreType <-
+                    liftDriver
+                        (Declaration.objectTypeLowering identity)
+                maybe
+                    (impossible
+                        "a checked structural proof lost a global object")
+                    (\availableType -> pure (identity, availableType))
+                    coreType)
+            identities
+    either
+        (throwProof
+            . ExactProofStructuralCompositionFailed location)
+        pure
+        (validate foundation
+            (\identity -> Map.lookup identity (Map.fromList types)))
+
+structuralFailure :: Location -> Text -> Prepare value
+structuralFailure location message =
+    throwProof
+        (ExactProofStructuralCompositionFailed
+            location
+            (KernelProof.ProofStructuralCompositionMismatch message))
+
+data CheckedExactProofAuthorization = CheckedExactProofAuthorization
+    !PreparedProof
+    !Bool
+
+lowerPreparedExactProof
+    :: PreparedExactProof
+    -> Declaration.LoweringDriver
+        (Either
+            Declaration.DeclarationError
+            (Declaration.CheckedDeclaration CheckedExactProofAuthorization))
+lowerPreparedExactProof
+        (PreparedExactProof _location alias target proof syntax) =
+    fmap checked
+        <$> Declaration.prepareCandidateSpecLowering
+            [] target SearchEligible [alias]
+  where
+    checked spec =
+        Declaration.checkedProofDeclaration
+            syntax [] [] [] []
+            [Declaration.checkedCandidate spec planning :| []]
+            (CheckedExactProofAuthorization
+                proof
+                (isJust (preparedProofFirstOmission proof)))
+      where
+        requests = plannedProofRequests proof
+        planning
+            | isJust (preparedProofFirstOmission proof) =
+                Declaration.checkedOmittedPlanning requests []
+            | otherwise =
+                Declaration.checkedSourceProofPlanning requests []
+
+authorizeCheckedExactProof
+    :: CheckedExactProofAuthorization
+    -> [NonEmpty Declaration.ReservedCandidate]
+    -> Declaration.Declaration ()
+authorizeCheckedExactProof
+        (CheckedExactProofAuthorization proof hasOmission) = \case
+    [candidate :| []]
+        | hasOmission ->
+            Declaration.authorizeOmittedCandidate
+                candidate
+                (executePreparedProof proof)
+        | otherwise ->
+            Declaration.authorizeVampireCandidate
+                candidate
+                (executePreparedProof proof)
+    stages ->
+        Declaration.failDeclaration
+            (Declaration.CheckedAuthorizationCandidateShapeMismatch
+                1 (length stages))
+
+data CheckedFinalPreludeFoundationAuthorization =
+    CheckedFinalPreludeFoundationAuthorization !FoundationAxiomTag
+
+lowerPreparedFinalPreludeFoundationClaim
+    :: PreparedFinalPreludeFoundationClaim
+    -> Declaration.LoweringDriver
+        (Either
+            Declaration.DeclarationError
+            (Declaration.CheckedDeclaration
+                CheckedFinalPreludeFoundationAuthorization))
+lowerPreparedFinalPreludeFoundationClaim
+        (PreparedFinalPreludeFoundationClaim
+            _location alias target tag syntax) =
+    fmap checked
+        <$> Declaration.prepareCandidateSpecLowering
+            [] target SearchEligible [alias]
+  where
+    checked spec =
+        Declaration.checkedProofDeclaration
+            syntax [] [] [] []
+            [ Declaration.checkedCandidate spec
+                (Declaration.checkedKernelPlanning
+                    (Authority.FoundationLeaf tag) [])
+                :| []
+            ]
+            (CheckedFinalPreludeFoundationAuthorization tag)
+
+authorizeCheckedFinalPreludeFoundationClaim
+    :: CheckedFinalPreludeFoundationAuthorization
+    -> [NonEmpty Declaration.ReservedCandidate]
+    -> Declaration.Declaration ()
+authorizeCheckedFinalPreludeFoundationClaim
+        (CheckedFinalPreludeFoundationAuthorization tag) = \case
+    [candidate :| []] ->
+        Declaration.authorizeKernelConstructionCandidate
+            (Authority.FoundationLeaf tag)
+            candidate
+            (pure (foundationFactDerivation tag))
+    stages ->
+        Declaration.failDeclaration
+            (Declaration.CheckedAuthorizationCandidateShapeMismatch
+                1 (length stages))
+
+preparedProofFirstOmission :: PreparedProof -> Maybe Location
+preparedProofFirstOmission = \case
+    PreparedImplicitAuto{} -> Nothing
+    PreparedQed{} -> Nothing
+    PreparedOmitted location _goal -> Just location
+    PreparedFix _identities continuation ->
+        preparedProofFirstOmission continuation
+    PreparedAssume _antecedent continuation ->
+        preparedProofFirstOmission continuation
+    PreparedTake _identities _witness _discharge continuation ->
+        preparedProofFirstOmission continuation
+    PreparedSetInduction
+            (PreparedCheckedSetInduction
+                _focus _property _antecedents _target
+                _hypothesis _result child) ->
+        preparedProofFirstOmission child
+    PreparedHave _claim _discharge continuation ->
+        preparedProofFirstOmission continuation
+    PreparedSuffices _goal _reduction _implication _discharge continuation ->
+        preparedProofFirstOmission continuation
+    PreparedCalculate _calculation continuation ->
+        preparedProofFirstOmission continuation
+    PreparedSince _since _evidence _claim _discharge continuation ->
+        preparedProofFirstOmission continuation
+    PreparedSubclaim _claim subproof continuation ->
+        preparedProofFirstOmission subproof
+            <|> preparedProofFirstOmission continuation
+    PreparedDefine _identity _body _definition continuation ->
+        preparedProofFirstOmission continuation
+    PreparedDefineRelational
+            _identity _body _functionality _definitions continuation ->
+        preparedProofFirstOmission continuation
+    PreparedDefineFunction _identity _graph _definition continuation ->
+        preparedProofFirstOmission continuation
+    PreparedByCase (PreparedCaseAnalysis _goal cases _exhaustive _discharge) ->
+        foldr
+            ((<|>) . preparedProofFirstOmission . preparedCaseProof)
+            Nothing
+            cases
+    PreparedByContradiction _goal _negation _falsum child ->
+        preparedProofFirstOmission child
+    PreparedContradiction{} -> Nothing
+
+plannedProofRequests
+    :: PreparedProof
+    -> [Declaration.CheckedPlannedVampireRequest]
+plannedProofRequests = \case
+    PreparedImplicitAuto discharge -> plannedDischargeRequests discharge
+    PreparedQed discharge -> plannedDischargeRequests discharge
+    PreparedOmitted{} -> []
+    PreparedFix _identities continuation ->
+        plannedProofRequests continuation
+    PreparedAssume _antecedent continuation ->
+        plannedProofRequests continuation
+    PreparedTake _identities _witness discharge continuation ->
+        plannedDischargeRequests discharge <> plannedProofRequests continuation
+    PreparedSetInduction
+            (PreparedCheckedSetInduction
+                _focus _property _antecedents _target
+                _hypothesis _result child) ->
+        plannedProofRequests child
+    PreparedHave _claim discharge continuation ->
+        plannedDischargeRequests discharge <> plannedProofRequests continuation
+    PreparedSuffices _goal _reduction _implication discharge continuation ->
+        plannedDischargeRequests discharge <> plannedProofRequests continuation
+    PreparedCalculate calculation continuation ->
+        plannedCalculationRequests calculation
+            <> plannedProofRequests continuation
+    PreparedSince _since evidence _claim discharge continuation ->
+        plannedSinceEvidenceRequests evidence
+            <> plannedDischargeRequests discharge
+            <> plannedProofRequests continuation
+    PreparedSubclaim _claim subproof continuation ->
+        plannedProofRequests subproof <> plannedProofRequests continuation
+    PreparedDefine _identity _body _definition continuation ->
+        plannedProofRequests continuation
+    PreparedDefineRelational
+            _identity _body functionality _definitions continuation ->
+        plannedDischargeRequests functionality
+            <> plannedProofRequests continuation
+    PreparedDefineFunction _identity _graph _definition continuation ->
+        plannedProofRequests continuation
+    PreparedByCase
+            (PreparedCaseAnalysis _goal cases _exhaustive discharge) ->
+        concatMap
+            (plannedProofRequests . preparedCaseProof)
+            (toList cases)
+            <> plannedDischargeRequests discharge
+    PreparedByContradiction _goal _negation _falsum child ->
+        plannedProofRequests child
+    PreparedContradiction _goal _falsum discharge ->
+        plannedDischargeRequests discharge
+
+plannedDischargeRequests
+    :: PreparedDischarge
+    -> [Declaration.CheckedPlannedVampireRequest]
+plannedDischargeRequests = \case
+    PreparedVampireDischarge location _justification _goal obligation ->
+        [Declaration.checkedPlannedVampireRequest location obligation]
+    PreparedSetExtensionality{} -> []
+
+plannedCalculationRequests
+    :: PreparedCalculation
+    -> [Declaration.CheckedPlannedVampireRequest]
+plannedCalculationRequests
+        (PreparedCheckedCalculation
+            _operandType _identities _guard _first links _result) =
+    concatMap
+        (plannedDischargeRequests . preparedCalculationLinkDischarge)
+        (toList links)
+
+plannedSinceEvidenceRequests
+    :: PreparedSinceEvidence
+    -> [Declaration.CheckedPlannedVampireRequest]
+plannedSinceEvidenceRequests = \case
+    PreparedSinceExisting{} -> []
+    PreparedSinceDischarged discharge _local ->
+        plannedDischargeRequests discharge
+
+executePreparedProof
+    :: PreparedProof
+    -> Declaration.CandidateProof ()
+executePreparedProof = \case
+    PreparedImplicitAuto discharge ->
+        executeDischarge discharge
+    PreparedQed discharge ->
+        executeDischarge discharge
+    PreparedOmitted _location _goal ->
+        Declaration.recordOmittedUse
+    PreparedFix _identities continuation ->
+        executePreparedProof continuation
+    PreparedAssume _antecedent continuation ->
+        executePreparedProof continuation
+    PreparedTake _identities _witness discharge continuation -> do
+        executeDischarge discharge
+        executePreparedProof continuation
+    PreparedSetInduction
+            (PreparedCheckedSetInduction
+                _focus _property _antecedents _target
+                _hypothesis _result child) ->
+        executePreparedProof child
+    PreparedHave _claim discharge continuation -> do
+        executeDischarge discharge
+        executePreparedProof continuation
+    PreparedSuffices goal reduction implication discharge continuation -> do
+        executeDischarge discharge
+        executePreparedProof continuation
+        unless
+            (implyScopedCore reduction goal == Just implication)
+            (impossible "a prepared suffices implication diverged")
+    PreparedCalculate calculation continuation -> do
+        executePreparedCalculation calculation
+        executePreparedProof continuation
+    PreparedSince sinceProposition evidence _claim discharge continuation -> do
+        executeSinceEvidence sinceProposition evidence
+        executeDischarge discharge
+        executePreparedProof continuation
+    PreparedSubclaim _claim subproof continuation -> do
+        executePreparedProof subproof
+        executePreparedProof continuation
+    PreparedDefine _identity _body _definition continuation ->
+        executePreparedProof continuation
+    PreparedDefineRelational
+            _identity _body functionality _definitions continuation -> do
+        executeDischarge functionality
+        executePreparedProof continuation
+    PreparedDefineFunction _identity _graph _definition continuation ->
+        executePreparedProof continuation
+    PreparedByCase
+            (PreparedCaseAnalysis _goal cases _exhaustive discharge) -> do
+        traverse_ (executePreparedProof . preparedCaseProof) cases
+        executeDischarge discharge
+    PreparedByContradiction _goal _negation _falsum child ->
+        executePreparedProof child
+    PreparedContradiction _goal _falsum discharge ->
+        executeDischarge discharge
+
+executeDischarge
+    :: PreparedDischarge
+    -> Declaration.CandidateProof ()
+executeDischarge
+        (PreparedVampireDischarge
+            location _justification _goal obligation) =
+    Declaration.locateProofObligation location
+        (Declaration.acceptPreparedVampireObligation obligation)
+executeDischarge PreparedSetExtensionality{} =
+    pure ()
+
+executePreparedCalculation
+    :: PreparedCalculation
+    -> Declaration.CandidateProof ()
+executePreparedCalculation
+        (PreparedCheckedCalculation
+            _operandType _identities _guard _first links _result) =
+    traverse_
+        (executeDischarge . preparedCalculationLinkDischarge)
+        links
+
+executeSinceEvidence
+    :: ScopedCheckedCore ObjectId
+    -> PreparedSinceEvidence
+    -> Declaration.CandidateProof ()
+executeSinceEvidence proposition = \case
+    PreparedSinceExisting local ->
+        unless (preparedLocalProposition local == proposition)
+            (impossible "a structural since premise diverged")
+    PreparedSinceDischarged discharge local -> do
+        executeDischarge discharge
+        unless
+            ( preparedDischargeGoal discharge == proposition
+                && preparedLocalProposition local == proposition
+            )
+            (impossible "a discharged since premise diverged")
+
+preparedLocalProposition
+    :: PreparedLocal
+    -> ScopedCheckedCore ObjectId
+preparedLocalProposition
+        (PreparedLocal _ordinal _origin _support proposition) =
+    proposition
+
+encodePreparedProof :: PreparedProof -> ByteString
+encodePreparedProof =
+    encodeCache . putPreparedProof
+
+putPreparedProof :: PreparedProof -> CachePut
+putPreparedProof = \case
+    PreparedImplicitAuto discharge -> do
+        putCacheTag 0x00
+        putPreparedDischarge discharge
+    PreparedQed discharge -> do
+        putCacheTag 0x01
+        putPreparedDischarge discharge
+    PreparedOmitted _location goal -> do
+        putCacheTag 0x06
+        putScopedProposition goal
+    PreparedFix identities continuation -> do
+        putCacheTag 0x02
+        putCacheList
+            (putCacheNatural . Exact.exactLocalIdValue)
+            identities
+        putPreparedProof continuation
+    PreparedAssume antecedent continuation -> do
+        putCacheTag 0x03
+        putScopedProposition antecedent
+        putPreparedProof continuation
+    PreparedTake identities witness discharge continuation -> do
+        putCacheTag 0x08
+        putCacheList
+            (putCacheNatural . Exact.exactLocalIdValue)
+            identities
+        putScopedProposition witness
+        putPreparedDischarge discharge
+        putPreparedProof continuation
+    PreparedSetInduction
+            (PreparedCheckedSetInduction
+                focus property antecedents target hypothesis result child) -> do
+        putCacheTag 0x07
+        putPreparedSetInductionFocus focus
+        putScopedProposition property
+        putCacheList putScopedProposition antecedents
+        putScopedProposition target
+        putScopedProposition hypothesis
+        putScopedProposition result
+        putPreparedProof child
+    PreparedHave claim discharge continuation -> do
+        putCacheTag 0x04
+        putScopedProposition claim
+        putPreparedDischarge discharge
+        putPreparedProof continuation
+    PreparedSuffices goal reduction implication discharge continuation -> do
+        putCacheTag 0x0c
+        putScopedProposition goal
+        putScopedProposition reduction
+        putScopedProposition implication
+        putPreparedDischarge discharge
+        putPreparedProof continuation
+    PreparedCalculate calculation continuation -> do
+        putCacheTag 0x0d
+        putPreparedCalculation calculation
+        putPreparedProof continuation
+    PreparedSince sinceProposition evidence claim discharge continuation -> do
+        putCacheTag 0x0e
+        putScopedProposition sinceProposition
+        putPreparedSinceEvidence evidence
+        putScopedProposition claim
+        putPreparedDischarge discharge
+        putPreparedProof continuation
+    PreparedSubclaim claim subproof continuation -> do
+        putCacheTag 0x05
+        putScopedProposition claim
+        putPreparedProof subproof
+        putPreparedProof continuation
+    PreparedDefine identity body definitions continuation -> do
+        putCacheTag 0x09
+        putCacheNatural (Exact.exactLocalIdValue identity)
+        putScopedTerm body
+        putCacheList putScopedProposition (toList definitions)
+        putPreparedProof continuation
+    PreparedDefineRelational
+            identity body functionality definitions continuation -> do
+        putCacheTag 0x11
+        putCacheNatural (Exact.exactLocalIdValue identity)
+        putScopedTerm body
+        putPreparedDischarge functionality
+        putCacheList putScopedProposition (toList definitions)
+        putPreparedProof continuation
+    PreparedByCase caseAnalysis -> do
+        putCacheTag 0x0f
+        putPreparedCaseAnalysis caseAnalysis
+    PreparedByContradiction goal negation falsum child -> do
+        putCacheTag 0x10
+        putScopedProposition goal
+        putScopedProposition negation
+        putScopedProposition falsum
+        putPreparedProof child
+    PreparedContradiction goal falsum discharge -> do
+        putCacheTag 0x0a
+        putScopedProposition goal
+        putScopedProposition falsum
+        putPreparedDischarge discharge
+    PreparedDefineFunction identity graph definition continuation -> do
+        putCacheTag 0x0b
+        putCacheNatural (Exact.exactLocalIdValue identity)
+        putScopedTerm graph
+        putScopedProposition definition
+        putPreparedProof continuation
+
+putPreparedSetInductionFocus
+    :: PreparedSetInductionFocus
+    -> CachePut
+putPreparedSetInductionFocus = \case
+    PreparedInitialSetInductionFocus identity index -> do
+        putCacheTag 0x00
+        putCacheNatural (Exact.exactLocalIdValue identity)
+        putCacheNatural index
+    PreparedLeadingSetInductionFocus identity -> do
+        putCacheTag 0x01
+        putCacheNatural (Exact.exactLocalIdValue identity)
+
+putPreparedDischarge :: PreparedDischarge -> CachePut
+putPreparedDischarge
+        (PreparedVampireDischarge
+            _location justification goal _obligation) = do
+    putPreparedDischargeSyntax justification goal
+putPreparedDischarge
+        (PreparedSetExtensionality _location goal) = do
+    putCacheTag 0x03
+    putScopedProposition goal
+
+putPreparedDischargeSyntax
+    :: PreparedJustification
+    -> ScopedCheckedCore ObjectId
+    -> CachePut
+putPreparedDischargeSyntax justification goal = do
+    putPreparedJustification justification
+    putScopedProposition goal
+
+putPreparedCalculation :: PreparedCalculation -> CachePut
+putPreparedCalculation
+        (PreparedCheckedCalculation
+            operandType identities calculationGuard first links result) = do
+    putCoreTypeCache operandType
+    putCacheList
+        (putCacheNatural . Exact.exactLocalIdValue)
+        identities
+    putCacheMaybe putScopedProposition calculationGuard
+    putCacheList putScopedTerm
+        (first : (preparedCalculationLinkDestination <$> toList links))
+    putCacheList putPreparedDischarge
+        (preparedCalculationLinkDischarge <$> toList links)
+    putScopedProposition result
+
+putPreparedSinceEvidence :: PreparedSinceEvidence -> CachePut
+putPreparedSinceEvidence = \case
+    PreparedSinceExisting local -> do
+        putCacheTag 0x00
+        putPreparedLocalEvidence local
+    PreparedSinceDischarged discharge local -> do
+        putCacheTag 0x01
+        putPreparedDischarge discharge
+        putPreparedLocalEvidence local
+
+putPreparedCaseAnalysis :: PreparedCaseAnalysis -> CachePut
+putPreparedCaseAnalysis
+        (PreparedCaseAnalysis goal cases exhaustive discharge) = do
+    putScopedProposition goal
+    putCacheList putPreparedCase (toList cases)
+    putScopedProposition exhaustive
+    putPreparedDischarge discharge
+
+putPreparedCase :: PreparedCase -> CachePut
+putPreparedCase (PreparedCase assumption proof) = do
+    putScopedProposition assumption
+    putPreparedProof proof
+
+putPreparedLocalEvidence :: PreparedLocal -> CachePut
+putPreparedLocalEvidence
+        (PreparedLocal ordinal _origin support proposition) = do
+    putCacheNatural (Backend.localPremiseOrdinalValue ordinal)
+    putCacheList
+        (\(identity, coreType) -> do
+            putCacheNatural (Exact.exactLocalIdValue identity)
+            putCoreTypeCache coreType)
+        (Vector.toList support)
+    putScopedProposition proposition
+
+implicitAutoProofSyntaxId
+    :: ScopedCheckedCore ObjectId
+    -> ProofSyntaxId
+implicitAutoProofSyntaxId goal =
+    proofSyntaxId
+        (encodeCache do
+            putCacheTag 0x00
+            putPreparedDischargeSyntax PreparedAuto goal)
+
+putPreparedJustification :: PreparedJustification -> CachePut
+putPreparedJustification = \case
+    PreparedAuto ->
+        putCacheTag 0x00
+    PreparedReferences fingerprints -> do
+        putCacheTag 0x01
+        putCacheList
+            putSemanticFactOccurrenceFingerprintCache
+            (toList fingerprints)
+    PreparedLocalOnly ->
+        putCacheTag 0x02
+
+putScopedProposition
+    :: ScopedCheckedCore ObjectId
+    -> CachePut
+putScopedProposition proposition = do
+    putCacheList putCoreTypeCache
+        (scopedCoreContext proposition)
+    putCanonicalTermCache putObjectIdCache
+        (scopedCoreTerm proposition)
+
+putScopedTerm
+    :: ScopedCheckedCore ObjectId
+    -> CachePut
+putScopedTerm term = do
+    putCacheList putCoreTypeCache
+        (scopedCoreContext term)
+    putCoreTypeCache (scopedCoreType term)
+    putCanonicalTermCache putObjectIdCache
+        (scopedCoreTerm term)
+
+proofLocation :: Location -> Raw.Proof -> Location
+proofLocation fallback = \case
+    Raw.Omitted location -> location
+    Raw.Qed maybeLocation _justification ->
+        fromMaybe fallback maybeLocation
+    Raw.Contradiction location _justification -> location
+    Raw.ByCase location _cases -> location
+    Raw.ByContradiction location _proof -> location
+    Raw.BySetInduction location _term _proof -> location
+    Raw.ByOrdInduction location _proof -> location
+    Raw.Assume location _statement _proof -> location
+    Raw.FixSymbolic location _variables _bound _proof -> location
+    Raw.FixSuchThat location _variables _statement _proof -> location
+    Raw.Calc location _quantifier _calculation _proof -> location
+    Raw.TakeVar location _variables _bound _statement _justification _proof ->
+        location
+    Raw.TakeNoun location _noun _justification _proof -> location
+    Raw.Have location _since _statement _justification _proof -> location
+    Raw.Suffices location _statement _justification _proof -> location
+    Raw.Subclaim location _statement _subproof _proof -> location
+    Raw.Define location _variable _expression _proof -> location
+    Raw.DefineFunction location _function _argument _value _bound _domain _proof ->
+        location
+    Raw.DefineFunctionLocal
+            location _function _argument _value _bound _target _rules _proof ->
+        location
+
+throwProof :: ExactProofError -> Prepare value
+throwProof =
+    State.lift . Except.throwError
+
+liftDriver
+    :: Declaration.LoweringDriver value
+    -> Prepare value
+liftDriver =
+    State.lift . Except.lift
+
+stableUnique :: Ord value => [value] -> [value]
+stableUnique =
+    reverse . snd
+        . foldl'
+            (\(seen, reversed) value ->
+                if value `Set.member` seen
+                    then (seen, reversed)
+                    else
+                        ( Set.insert value seen
+                        , value : reversed
+                        ))
+            (Set.empty, [])