Classify complete typed prover problems

3 files changed, 1346 insertions, 8 deletions

diff --git a/source/Checking/Backend/Problem.hs b/source/Checking/Backend/Problem.hs
new file mode 100644
index 0000000..01ca0bf
--- /dev/null
+++ b/source/Checking/Backend/Problem.hs
@@ -0,0 +1,1295 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Pure selection and complete-problem FOF/TH0 classification.
+module Checking.Backend.Problem
+    ( SupportedProposition
+    , supportedProposition
+    , supportedPropositionSupport
+    , supportedPropositionTerm
+    , weakenClosedSupportedProposition
+    , SupportedPropositionError(..)
+    , CheckedFofProjection
+    , checkedFofProjectionProposition
+    , FofCapability(..)
+    , BackendFofExclusion(..)
+    , BackendClassificationError(..)
+    , classifySupportedProposition
+    , TypedBackendFactInput
+    , typedBackendFactInput
+    , TypedBackendFact
+    , typedBackendFactReference
+    , typedBackendFactAliases
+    , typedBackendFactOrigin
+    , typedBackendFactProposition
+    , typedBackendFactCapability
+    , TypedFactInventory
+    , prepareTypedFactInventory
+    , typedFactInventoryOrder
+    , typedFactInventoryFofOrder
+    , TypedFactInventoryError(..)
+    , LocalPremiseOrdinal
+    , localPremiseOrdinal
+    , localPremiseOrdinalValue
+    , TypedLocalPremise
+    , typedLocalPremise
+    , typedLocalPremiseOrdinal
+    , typedLocalPremiseOrigin
+    , typedLocalPremiseProposition
+    , typedLocalPremiseCapability
+    , GlobalPremisePolicy(..)
+    , LocalPremisePolicy(..)
+    , TypedProblemRoute(..)
+    , TypedProblem
+    , planTypedProblem
+    , typedProblemRoute
+    , typedProblemClaim
+    , typedProblemGlobalPremises
+    , typedProblemLocalPremises
+    , typedProblemAuxiliaries
+    , typedProblemGlobalTypes
+    , typedProblemLocalTypes
+    , TypedProblemError(..)
+    ) where
+
+import Base
+import Checking.Core
+import Checking.Foundation
+import Syntax.Internal (Marker)
+
+import Control.Monad (foldM, unless, when)
+import Data.Bifunctor (first)
+import Data.List qualified as List
+import Data.Map.Strict qualified as Map
+import Data.Set qualified as Set
+import Data.Vector (Vector)
+import Data.Vector qualified as Vector
+import Numeric.Natural (Natural)
+
+
+-- | A proposition under its exact nearest-first ambient-local support.
+data SupportedProposition local global =
+    SupportedProposition
+        !(Vector (local, CoreType))
+        !(ScopedCheckedCore global)
+    deriving stock (Eq)
+
+data SupportedPropositionError local
+    = SupportedPropositionIsNotProposition !CoreType
+    | SupportedPropositionContextMismatch
+        ![CoreType]
+        ![CoreType]
+    | DuplicateSupportedLocal !local
+    | UnusedSupportedLocal !local
+    deriving stock (Show, Eq)
+
+supportedProposition
+    :: Ord local
+    => Vector (local, CoreType)
+    -> ScopedCheckedCore global
+    -> Either
+        (SupportedPropositionError local)
+        (SupportedProposition local global)
+supportedProposition support statement = do
+    unless
+        (scopedCoreType statement == TyProp)
+        (Left
+            (SupportedPropositionIsNotProposition
+                (scopedCoreType statement)))
+    let expectedContext =
+            snd <$> Vector.toList support
+        actualContext =
+            scopedCoreContext statement
+    unless
+        (actualContext == expectedContext)
+        (Left
+            (SupportedPropositionContextMismatch
+                expectedContext
+                actualContext))
+    void
+        (foldM
+            (\seen (local, _coreType) ->
+                if local `Set.member` seen
+                    then
+                        Left
+                            (DuplicateSupportedLocal local)
+                    else
+                        Right (Set.insert local seen))
+            Set.empty
+            support)
+    case
+        List.find
+            (\(ordinal, _entry) ->
+                fromIntegral ordinal
+                    `Set.notMember`
+                        ambientIndices
+                            (scopedCoreTerm statement))
+            (Vector.toList
+                (Vector.indexed support)) of
+        Just (_ordinal, (local, _coreType)) ->
+            Left (UnusedSupportedLocal local)
+        Nothing ->
+            pure ()
+    pure
+        (SupportedProposition
+            support
+            statement)
+
+ambientIndices
+    :: CanonicalTerm global
+    -> Set Natural
+ambientIndices =
+    go 0
+  where
+    go depth = \case
+        CBound index
+            | index < depth ->
+                mempty
+            | otherwise ->
+                Set.singleton (index - depth)
+        CGlobal{} ->
+            mempty
+        CIntrinsic{} ->
+            mempty
+        COpaqueInteger{} ->
+            mempty
+        CApp function argument ->
+            go depth function <> go depth argument
+        CLam _binderType body ->
+            go (depth + 1) body
+        CFalsum ->
+            mempty
+        CImp premise conclusion ->
+            go depth premise <> go depth conclusion
+        CEq _operandType left right ->
+            go depth left <> go depth right
+        CForall _binderType body ->
+            go (depth + 1) body
+
+supportedPropositionSupport
+    :: SupportedProposition local global
+    -> Vector (local, CoreType)
+supportedPropositionSupport
+        (SupportedProposition support _statement) =
+    support
+
+supportedPropositionTerm
+    :: SupportedProposition local global
+    -> CanonicalTerm global
+supportedPropositionTerm
+        (SupportedProposition _support statement) =
+    scopedCoreTerm statement
+
+weakenClosedSupportedProposition
+    :: SupportedProposition Void global
+    -> SupportedProposition local global
+weakenClosedSupportedProposition
+        (SupportedProposition support statement) =
+    SupportedProposition
+        (fmap
+            (\(local, coreType) ->
+                (absurd local, coreType))
+            support)
+        statement
+
+
+newtype CheckedFofProjection local global =
+    CheckedFofProjection
+        (SupportedProposition local global)
+    deriving stock (Eq)
+
+checkedFofProjectionProposition
+    :: CheckedFofProjection local global
+    -> SupportedProposition local global
+checkedFofProjectionProposition
+        (CheckedFofProjection proposition) =
+    proposition
+
+data FofCapability projection
+    = FofProjectable !projection
+    | RequiresTh0 !(NonEmpty BackendFofExclusion)
+    deriving stock (Eq)
+
+data BackendFofExclusion
+    = StructuralFofExclusion !FofExclusion
+    | HigherOrderGlobalType !CoreType
+    | HigherOrderAmbientLocal !CoreType
+    deriving stock (Show, Eq, Ord)
+
+data BackendClassificationError global
+    = UnknownBackendGlobal !global
+    | BackendFofProjectionInvariantFailed
+    deriving stock (Show, Eq)
+
+classifySupportedProposition
+    :: Ord global
+    => (global -> Maybe CoreType)
+    -> SupportedProposition local global
+    -> Either
+        (BackendClassificationError global)
+        (FofCapability
+            (CheckedFofProjection local global))
+classifySupportedProposition globalType proposition = do
+    globalExclusions <-
+        foldM
+            collectGlobal
+            Set.empty
+            (Set.toAscList
+                (canonicalGlobals
+                    (supportedPropositionTerm proposition)))
+    let structuralExclusions =
+            case classifyScopedStructure proposition of
+                FoundationFofProjectable ->
+                    Set.empty
+                FoundationRequiresTh0 structural ->
+                    Set.fromList
+                        (StructuralFofExclusion
+                            <$> toList structural)
+        localExclusions =
+            Set.fromList
+                [ HigherOrderAmbientLocal coreType
+                | (_local, coreType) <-
+                    Vector.toList
+                        (supportedPropositionSupport
+                            proposition)
+                , coreType /= TySet
+                ]
+        exclusions =
+            structuralExclusions
+                <> globalExclusions
+                <> localExclusions
+    case Set.toAscList exclusions of
+        [] ->
+            if isFirstOrderProposition
+                    globalType
+                    proposition
+                then
+                    Right
+                        (FofProjectable
+                            (CheckedFofProjection
+                                proposition))
+                else
+                    Left BackendFofProjectionInvariantFailed
+        firstExclusion : remainingExclusions ->
+            Right
+                (RequiresTh0
+                    (firstExclusion
+                        :| remainingExclusions))
+  where
+    collectGlobal exclusions global =
+        case globalType global of
+            Nothing ->
+                Left (UnknownBackendGlobal global)
+            Just coreType ->
+                Right
+                    (if isFirstOrderGlobalType coreType
+                        then exclusions
+                        else
+                            Set.insert
+                                (HigherOrderGlobalType
+                                    coreType)
+                                exclusions)
+
+classifyScopedStructure
+    :: SupportedProposition local global
+    -> FoundationBackendClass
+classifyScopedStructure =
+    classifyCanonicalFofStructure
+        . supportedPropositionTerm
+
+isFirstOrderGlobalType :: CoreType -> Bool
+isFirstOrderGlobalType =
+    go
+  where
+    go = \case
+        TySet ->
+            True
+        TyProp ->
+            True
+        TyArrow TySet result ->
+            go result
+        TyArrow _argument _result ->
+            False
+
+-- The structural and type exclusions make this projection total. This final
+-- walk catches an accidentally unsaturated first-order head.
+isFirstOrderProposition
+    :: (global -> Maybe CoreType)
+    -> SupportedProposition local global
+    -> Bool
+isFirstOrderProposition globalType proposition =
+    isFormula initialContext
+        (supportedPropositionTerm proposition)
+  where
+    initialContext =
+        snd
+            <$> Vector.toList
+                (supportedPropositionSupport
+                    proposition)
+
+    isFormula context = \case
+        CFalsum ->
+            True
+        CImp premise conclusion ->
+            isFormula context premise
+                && isFormula context conclusion
+        CEq TySet left right ->
+            isTerm context left
+                && isTerm context right
+        CEq TyProp left right ->
+            isFormula context left
+                && isFormula context right
+        CForall TySet body ->
+            isFormula (TySet : context) body
+        application ->
+            case applicationHead application of
+                (CGlobal global, arguments) ->
+                    maybe
+                        False
+                        (\coreType ->
+                            applicationResult
+                                coreType
+                                arguments
+                                == Just TyProp
+                                && all
+                                    (isTerm context)
+                                    arguments)
+                        (globalType global)
+                (CIntrinsic intrinsic, arguments) ->
+                    applicationResult
+                        (coreIntrinsicType intrinsic)
+                        arguments
+                        == Just TyProp
+                        && all
+                            (isTerm context)
+                            arguments
+                _ ->
+                    False
+
+    isTerm context = \case
+        CBound index ->
+            contextAt index context
+                == Just TySet
+        CGlobal global ->
+            globalType global == Just TySet
+        CIntrinsic intrinsic ->
+            coreIntrinsicType intrinsic == TySet
+        COpaqueInteger{} ->
+            True
+        application ->
+            case applicationHead application of
+                (CGlobal global, arguments) ->
+                    maybe
+                        False
+                        (\coreType ->
+                            applicationResult
+                                coreType
+                                arguments
+                                == Just TySet
+                                && all
+                                    (isTerm context)
+                                    arguments)
+                        (globalType global)
+                (CIntrinsic intrinsic, arguments) ->
+                    applicationResult
+                        (coreIntrinsicType intrinsic)
+                        arguments
+                        == Just TySet
+                        && all
+                            (isTerm context)
+                            arguments
+                _ ->
+                    False
+
+applicationHead
+    :: CanonicalTerm global
+    -> (CanonicalTerm global, [CanonicalTerm global])
+applicationHead =
+    go []
+  where
+    go arguments = \case
+        CApp function argument ->
+            go (argument : arguments) function
+        headTerm ->
+            (headTerm, arguments)
+
+applicationResult
+    :: CoreType
+    -> [CanonicalTerm global]
+    -> Maybe CoreType
+applicationResult =
+    foldM
+        (\coreType _argument ->
+            case coreType of
+                TyArrow TySet result ->
+                    Just result
+                _ ->
+                    Nothing)
+
+contextAt :: Natural -> [value] -> Maybe value
+contextAt _index [] =
+    Nothing
+contextAt 0 (value : _remaining) =
+    Just value
+contextAt index (_value : remaining) =
+    contextAt (index - 1) remaining
+
+canonicalGlobals
+    :: Ord global
+    => CanonicalTerm global
+    -> Set global
+canonicalGlobals = \case
+    CBound{} ->
+        mempty
+    CGlobal global ->
+        Set.singleton global
+    CIntrinsic{} ->
+        mempty
+    COpaqueInteger{} ->
+        mempty
+    CApp function argument ->
+        canonicalGlobals function
+            <> canonicalGlobals argument
+    CLam _binderType body ->
+        canonicalGlobals body
+    CFalsum ->
+        mempty
+    CImp premise conclusion ->
+        canonicalGlobals premise
+            <> canonicalGlobals conclusion
+    CEq _operandType left right ->
+        canonicalGlobals left
+            <> canonicalGlobals right
+    CForall _binderType body ->
+        canonicalGlobals body
+
+
+data TypedBackendFactInput ref origin global =
+    TypedBackendFactInput
+        !ref
+        !(NonEmpty Marker)
+        !origin
+        !(FrozenCheckedCore global)
+
+typedBackendFactInput
+    :: ref
+    -> NonEmpty Marker
+    -> origin
+    -> FrozenCheckedCore global
+    -> TypedBackendFactInput ref origin global
+typedBackendFactInput =
+    TypedBackendFactInput
+
+data TypedBackendFact ref origin global =
+    TypedBackendFact
+        !ref
+        !(NonEmpty Marker)
+        !origin
+        !(SupportedProposition Void global)
+        !(FofCapability
+            (CheckedFofProjection Void global))
+    deriving stock (Eq)
+
+typedBackendFactReference
+    :: TypedBackendFact ref origin global
+    -> ref
+typedBackendFactReference
+        (TypedBackendFact
+            reference
+            _aliases
+            _origin
+            _proposition
+            _capability) =
+    reference
+
+typedBackendFactAliases
+    :: TypedBackendFact ref origin global
+    -> NonEmpty Marker
+typedBackendFactAliases
+        (TypedBackendFact
+            _reference
+            aliases
+            _origin
+            _proposition
+            _capability) =
+    aliases
+
+typedBackendFactOrigin
+    :: TypedBackendFact ref origin global
+    -> origin
+typedBackendFactOrigin
+        (TypedBackendFact
+            _reference
+            _aliases
+            factOrigin
+            _proposition
+            _capability) =
+    factOrigin
+
+typedBackendFactProposition
+    :: TypedBackendFact ref origin global
+    -> SupportedProposition Void global
+typedBackendFactProposition
+        (TypedBackendFact
+            _reference
+            _aliases
+            _origin
+            proposition
+            _capability) =
+    proposition
+
+typedBackendFactCapability
+    :: TypedBackendFact ref origin global
+    -> FofCapability
+        (CheckedFofProjection Void global)
+typedBackendFactCapability
+        (TypedBackendFact
+            _reference
+            _aliases
+            _origin
+            _proposition
+            capability) =
+    capability
+
+data TypedFactInventory ref origin global =
+    TypedFactInventory
+        !(Map ref (TypedBackendFact ref origin global))
+        !(Map Marker ref)
+        !(Vector ref)
+        !(Vector ref)
+
+data TypedFactInventoryError ref origin global
+    = TypedFactStatementIsNotProposition !ref !CoreType
+    | TypedFactClassificationFailed
+        !ref
+        !(BackendClassificationError global)
+    | DuplicateTypedFactReference !ref
+    | TypedFactAliasConflict
+        !Marker
+        !ref
+        !origin
+        !ref
+        !origin
+    deriving stock (Show, Eq)
+
+prepareTypedFactInventory
+    :: (Ord ref, Ord global)
+    => (global -> Maybe CoreType)
+    -> [TypedBackendFactInput ref origin global]
+    -> Either
+        (TypedFactInventoryError ref origin global)
+        (TypedFactInventory ref origin global)
+prepareTypedFactInventory globalType inputs = do
+    (byReference, byAlias, reversedOrder, reversedFofOrder) <-
+        foldM
+            insertInput
+            (Map.empty, Map.empty, [], [])
+            inputs
+    pure
+        (TypedFactInventory
+            byReference
+            byAlias
+            (Vector.fromList
+                (reverse reversedOrder))
+            (Vector.fromList
+                (reverse reversedFofOrder)))
+  where
+    insertInput
+            (byReference, byAlias, reversedOrder, reversedFofOrder)
+            (TypedBackendFactInput
+                reference
+                aliases
+                factOrigin
+                statement) = do
+        when
+            (Map.member reference byReference)
+            (Left
+                (DuplicateTypedFactReference
+                    reference))
+        unless
+            (frozenCoreType statement == TyProp)
+            (Left
+                (TypedFactStatementIsNotProposition
+                    reference
+                    (frozenCoreType statement)))
+        scoped <-
+            pure (embedClosedCore [] statement)
+        proposition <-
+            first
+                (const
+                    (TypedFactStatementIsNotProposition
+                        reference
+                        (frozenCoreType statement)))
+                (supportedProposition
+                    Vector.empty
+                    scoped)
+        capability <-
+            first
+                (TypedFactClassificationFailed
+                    reference)
+                (classifySupportedProposition
+                    globalType
+                    proposition)
+        byAlias' <-
+            foldM
+                (insertAlias
+                    reference
+                    factOrigin
+                    byReference)
+                byAlias
+                aliases
+        let fact =
+                TypedBackendFact
+                    reference
+                    aliases
+                    factOrigin
+                    proposition
+                    capability
+            reversedFofOrder' =
+                case capability of
+                    FofProjectable{} ->
+                        reference : reversedFofOrder
+                    RequiresTh0{} ->
+                        reversedFofOrder
+        pure
+            ( Map.insert reference fact byReference
+            , byAlias'
+            , reference : reversedOrder
+            , reversedFofOrder'
+            )
+
+    insertAlias
+            reference
+            factOrigin
+            byReference
+            byAlias
+            alias =
+        case Map.lookup alias byAlias of
+            Nothing ->
+                Right
+                    (Map.insert
+                        alias
+                        reference
+                        byAlias)
+            Just previousReference ->
+                if previousReference == reference
+                    then
+                        Right byAlias
+                    else
+                        case Map.lookup previousReference byReference of
+                            Nothing ->
+                                Left
+                                    (DuplicateTypedFactReference
+                                        previousReference)
+                            Just previous ->
+                                Left
+                                    (TypedFactAliasConflict
+                                        alias
+                                        previousReference
+                                        (typedBackendFactOrigin
+                                            previous)
+                                        reference
+                                        factOrigin)
+
+typedFactInventoryOrder
+    :: TypedFactInventory ref origin global
+    -> Vector ref
+typedFactInventoryOrder
+        (TypedFactInventory
+            _byReference
+            _byAlias
+            order
+            _fofOrder) =
+    order
+
+typedFactInventoryFofOrder
+    :: TypedFactInventory ref origin global
+    -> Vector ref
+typedFactInventoryFofOrder
+        (TypedFactInventory
+            _byReference
+            _byAlias
+            _order
+            fofOrder) =
+    fofOrder
+
+
+newtype LocalPremiseOrdinal =
+    LocalPremiseOrdinal Natural
+    deriving stock (Show, Eq, Ord)
+
+localPremiseOrdinal :: Natural -> LocalPremiseOrdinal
+localPremiseOrdinal =
+    LocalPremiseOrdinal
+
+localPremiseOrdinalValue
+    :: LocalPremiseOrdinal
+    -> Natural
+localPremiseOrdinalValue
+        (LocalPremiseOrdinal ordinal) =
+    ordinal
+
+data TypedLocalPremise local origin global =
+    TypedLocalPremise
+        !LocalPremiseOrdinal
+        !origin
+        !(SupportedProposition local global)
+        !(FofCapability
+            (CheckedFofProjection local global))
+    deriving stock (Eq)
+
+typedLocalPremise
+    :: Ord global
+    => (global -> Maybe CoreType)
+    -> LocalPremiseOrdinal
+    -> origin
+    -> SupportedProposition local global
+    -> Either
+        (BackendClassificationError global)
+        (TypedLocalPremise local origin global)
+typedLocalPremise globalType ordinal premiseOrigin proposition =
+    TypedLocalPremise
+        ordinal
+        premiseOrigin
+        proposition
+        <$> classifySupportedProposition
+            globalType
+            proposition
+
+typedLocalPremiseOrdinal
+    :: TypedLocalPremise local origin global
+    -> LocalPremiseOrdinal
+typedLocalPremiseOrdinal
+        (TypedLocalPremise
+            ordinal
+            _origin
+            _proposition
+            _capability) =
+    ordinal
+
+typedLocalPremiseOrigin
+    :: TypedLocalPremise local origin global
+    -> origin
+typedLocalPremiseOrigin
+        (TypedLocalPremise
+            _ordinal
+            premiseOrigin
+            _proposition
+            _capability) =
+    premiseOrigin
+
+typedLocalPremiseProposition
+    :: TypedLocalPremise local origin global
+    -> SupportedProposition local global
+typedLocalPremiseProposition
+        (TypedLocalPremise
+            _ordinal
+            _origin
+            proposition
+            _capability) =
+    proposition
+
+typedLocalPremiseCapability
+    :: TypedLocalPremise local origin global
+    -> FofCapability
+        (CheckedFofProjection local global)
+typedLocalPremiseCapability
+        (TypedLocalPremise
+            _ordinal
+            _origin
+            _proposition
+            capability) =
+    capability
+
+
+data GlobalPremisePolicy
+    = ImplicitFofFacts
+    | ExplicitFacts !(NonEmpty Marker)
+    | NoGlobalFacts
+    deriving stock (Show, Eq)
+
+data LocalPremisePolicy
+    = FirstOrderLocals
+    | AllLocals
+    deriving stock (Show, Eq)
+
+data TypedProblemRoute
+    = RouteFof
+    | RouteTh0
+    deriving stock (Show, Eq)
+
+data TypedProblem ref local origin global =
+    TypedProblem
+        !TypedProblemRoute
+        !(SupportedProposition local global)
+        !(Vector (TypedBackendFact ref origin global))
+        !(Vector (TypedLocalPremise local origin global))
+        !(Vector (FrozenCheckedCore global))
+        !(Map global CoreType)
+        !(Map local CoreType)
+
+data TypedProblemError ref local origin global
+    = TypedProblemClaimClassificationFailed
+        !(BackendClassificationError global)
+    | TypedProblemAuxiliaryClassificationFailed
+        !Natural
+        !(BackendClassificationError global)
+    | TypedProblemAuxiliaryIsNotProposition
+        !Natural
+        !CoreType
+    | TypedProblemUnknownFactAlias !Marker
+    | TypedProblemFactReferenceMissing !ref
+    | TypedProblemExplicitHigherOrderJustificationRequired
+        !(NonEmpty BackendFofExclusion)
+    | TypedProblemInvalidPolicyCombination
+        !GlobalPremisePolicy
+        !LocalPremisePolicy
+    | TypedProblemDuplicateLocalPremiseOrdinal
+        !LocalPremiseOrdinal
+    | TypedProblemLocalTypeMismatch
+        !local
+        !CoreType
+        !CoreType
+    deriving stock (Show, Eq)
+
+planTypedProblem
+    :: (Ord ref, Ord local, Ord global)
+    => (global -> Maybe CoreType)
+    -> TypedFactInventory ref origin global
+    -> SupportedProposition local global
+    -> [TypedLocalPremise local origin global]
+    -> [FrozenCheckedCore global]
+    -> GlobalPremisePolicy
+    -> LocalPremisePolicy
+    -> Either
+        (TypedProblemError ref local origin global)
+        (TypedProblem ref local origin global)
+planTypedProblem
+        globalType
+        inventory
+        claim
+        availableLocals
+        auxiliaries
+        globalPolicy
+        localPolicy = do
+    validatePolicyCombination
+        globalPolicy
+        localPolicy
+    validateLocalPremiseOrdinals
+        availableLocals
+    claimCapability <-
+        first
+            TypedProblemClaimClassificationFailed
+            (classifySupportedProposition
+                globalType
+                claim)
+    selectedFacts <-
+        selectFacts
+            inventory
+            globalPolicy
+    let selectedLocals =
+            Vector.fromList
+                (List.sortOn
+                    typedLocalPremiseOrdinal
+                    (case localPolicy of
+                        FirstOrderLocals ->
+                            List.filter
+                                (isFofCapability
+                                    . typedLocalPremiseCapability)
+                                availableLocals
+                        AllLocals ->
+                            availableLocals))
+    auxiliaryCapabilities <-
+        traverse
+            classifyAuxiliary
+            (zip [0..] auxiliaries)
+    case globalPolicy of
+        ImplicitFofFacts ->
+            case implicitTh0Requirement
+                    claimCapability
+                    auxiliaryCapabilities of
+                Nothing ->
+                    pure ()
+                Just exclusions ->
+                    Left
+                        (TypedProblemExplicitHigherOrderJustificationRequired
+                            exclusions)
+        _ ->
+            pure ()
+    let selectedFofCapabilities =
+            isFofCapability claimCapability
+                : (isFofCapability
+                    . typedBackendFactCapability
+                    <$> Vector.toList selectedFacts)
+                <> (isFofCapability
+                    . typedLocalPremiseCapability
+                    <$> Vector.toList selectedLocals)
+                <> (isFofCapability
+                    <$> auxiliaryCapabilities)
+        route =
+            if and selectedFofCapabilities
+                then RouteFof
+                else RouteTh0
+    globalTypes <-
+        collectProblemGlobals
+            globalType
+            claim
+            selectedFacts
+            selectedLocals
+            auxiliaries
+    localTypes <-
+        collectProblemLocals
+            claim
+            selectedLocals
+    pure
+        (TypedProblem
+            route
+            claim
+            selectedFacts
+            selectedLocals
+            (Vector.fromList auxiliaries)
+            globalTypes
+            localTypes)
+  where
+    implicitTh0Requirement claimCapability
+            auxiliaryCapabilities =
+        case claimCapability of
+            RequiresTh0 exclusions ->
+                Just exclusions
+            FofProjectable{} ->
+                firstAuxiliaryRequirement
+                    auxiliaryCapabilities
+
+    firstAuxiliaryRequirement = \case
+        [] ->
+            Nothing
+        FofProjectable{} : remaining ->
+            firstAuxiliaryRequirement remaining
+        RequiresTh0 exclusions : _remaining ->
+            Just exclusions
+
+    classifyAuxiliary (ordinal, auxiliary) = do
+        unless
+            (frozenCoreType auxiliary == TyProp)
+            (Left
+                (TypedProblemAuxiliaryIsNotProposition
+                    ordinal
+                    (frozenCoreType auxiliary)))
+        proposition <-
+            first
+                (const
+                    (TypedProblemAuxiliaryClassificationFailed
+                        ordinal
+                        BackendFofProjectionInvariantFailed))
+                (supportedProposition
+                    (Vector.empty
+                        :: Vector
+                            (Void, CoreType))
+                    (embedClosedCore [] auxiliary))
+        first
+            (TypedProblemAuxiliaryClassificationFailed
+                ordinal)
+            (classifySupportedProposition
+                globalType
+                proposition)
+
+validatePolicyCombination
+    :: GlobalPremisePolicy
+    -> LocalPremisePolicy
+    -> Either
+        (TypedProblemError ref local origin global)
+        ()
+validatePolicyCombination globalPolicy localPolicy =
+    case (globalPolicy, localPolicy) of
+        (ImplicitFofFacts, FirstOrderLocals) ->
+            Right ()
+        (ExplicitFacts{}, FirstOrderLocals) ->
+            Right ()
+        (NoGlobalFacts, AllLocals) ->
+            Right ()
+        _ ->
+            Left
+                (TypedProblemInvalidPolicyCombination
+                    globalPolicy
+                    localPolicy)
+
+validateLocalPremiseOrdinals
+    :: [TypedLocalPremise local origin global]
+    -> Either
+        (TypedProblemError ref local origin global)
+        ()
+validateLocalPremiseOrdinals =
+    void
+        . foldM
+            (\seen premise ->
+                let ordinal =
+                        typedLocalPremiseOrdinal premise
+                in
+                    if ordinal `Set.member` seen
+                        then
+                            Left
+                                (TypedProblemDuplicateLocalPremiseOrdinal
+                                    ordinal)
+                        else
+                            Right
+                                (Set.insert
+                                    ordinal
+                                    seen))
+            Set.empty
+
+selectFacts
+    :: Ord ref
+    => TypedFactInventory ref origin global
+    -> GlobalPremisePolicy
+    -> Either
+        (TypedProblemError ref local origin global)
+        (Vector (TypedBackendFact ref origin global))
+selectFacts
+        inventory@(TypedFactInventory
+            _byReference
+            byAlias
+            _order
+            fofOrder)
+        policy = do
+    references <-
+        case policy of
+            ImplicitFofFacts ->
+                Right (Vector.toList fofOrder)
+            ExplicitFacts aliases ->
+                stableUnique
+                    <$> traverse
+                        (\alias ->
+                            maybe
+                                (Left
+                                    (TypedProblemUnknownFactAlias
+                                        alias))
+                                Right
+                                (Map.lookup alias byAlias))
+                        (toList aliases)
+            NoGlobalFacts ->
+                Right []
+    Vector.fromList
+        <$> traverse
+            (\reference ->
+                maybe
+                    (Left
+                        (TypedProblemFactReferenceMissing
+                            reference))
+                    Right
+                    (lookupTypedFact reference inventory))
+            references
+  where
+    stableUnique =
+        reverse . snd
+            . foldl'
+                (\(seen, reversed) reference ->
+                    if reference `Set.member` seen
+                        then (seen, reversed)
+                        else
+                            ( Set.insert reference seen
+                            , reference : reversed
+                            ))
+                (Set.empty, [])
+
+lookupTypedFact
+    :: Ord ref
+    => ref
+    -> TypedFactInventory ref origin global
+    -> Maybe (TypedBackendFact ref origin global)
+lookupTypedFact reference
+        (TypedFactInventory
+            byReference
+            _byAlias
+            _order
+            _fofOrder) =
+    Map.lookup reference byReference
+
+isFofCapability :: FofCapability projection -> Bool
+isFofCapability = \case
+    FofProjectable{} ->
+        True
+    RequiresTh0{} ->
+        False
+
+collectProblemGlobals
+    :: Ord global
+    => (global -> Maybe CoreType)
+    -> SupportedProposition local global
+    -> Vector (TypedBackendFact ref origin global)
+    -> Vector (TypedLocalPremise local origin global)
+    -> [FrozenCheckedCore global]
+    -> Either
+        (TypedProblemError ref local origin global)
+        (Map global CoreType)
+collectProblemGlobals
+        globalType
+        claim
+        facts
+        locals
+        auxiliaries =
+    Map.fromAscList
+        <$> traverse
+            resolveGlobal
+            (Set.toAscList globals)
+  where
+    globals =
+        canonicalGlobals
+            (supportedPropositionTerm claim)
+            <> foldMap
+                (canonicalGlobals
+                    . supportedPropositionTerm
+                    . typedBackendFactProposition)
+                facts
+            <> foldMap
+                (canonicalGlobals
+                    . supportedPropositionTerm
+                    . typedLocalPremiseProposition)
+                locals
+            <> foldMap frozenCoreGlobals auxiliaries
+
+    resolveGlobal global =
+        case globalType global of
+            Nothing ->
+                Left
+                    (TypedProblemClaimClassificationFailed
+                        (UnknownBackendGlobal global))
+            Just coreType ->
+                Right (global, coreType)
+
+collectProblemLocals
+    :: Ord local
+    => SupportedProposition local global
+    -> Vector (TypedLocalPremise local origin global)
+    -> Either
+        (TypedProblemError ref local origin global)
+        (Map local CoreType)
+collectProblemLocals claim locals =
+    foldM
+        insertSupport
+        Map.empty
+        supports
+  where
+    supports =
+        Vector.toList
+            (supportedPropositionSupport claim)
+            <> concatMap
+                (Vector.toList
+                    . supportedPropositionSupport
+                    . typedLocalPremiseProposition)
+                (Vector.toList locals)
+
+    insertSupport current (local, coreType) =
+        case Map.lookup local current of
+            Nothing ->
+                Right
+                    (Map.insert
+                        local
+                        coreType
+                        current)
+            Just previousType
+                | previousType == coreType ->
+                    Right current
+                | otherwise ->
+                    Left
+                        (TypedProblemLocalTypeMismatch
+                            local
+                            previousType
+                            coreType)
+
+typedProblemRoute
+    :: TypedProblem ref local origin global
+    -> TypedProblemRoute
+typedProblemRoute
+        (TypedProblem
+            route
+            _claim
+            _facts
+            _locals
+            _auxiliaries
+            _globals
+            _localTypes) =
+    route
+
+typedProblemClaim
+    :: TypedProblem ref local origin global
+    -> SupportedProposition local global
+typedProblemClaim
+        (TypedProblem
+            _route
+            claim
+            _facts
+            _locals
+            _auxiliaries
+            _globals
+            _localTypes) =
+    claim
+
+typedProblemGlobalPremises
+    :: TypedProblem ref local origin global
+    -> Vector (TypedBackendFact ref origin global)
+typedProblemGlobalPremises
+        (TypedProblem
+            _route
+            _claim
+            facts
+            _locals
+            _auxiliaries
+            _globals
+            _localTypes) =
+    facts
+
+typedProblemLocalPremises
+    :: TypedProblem ref local origin global
+    -> Vector (TypedLocalPremise local origin global)
+typedProblemLocalPremises
+        (TypedProblem
+            _route
+            _claim
+            _facts
+            locals
+            _auxiliaries
+            _globals
+            _localTypes) =
+    locals
+
+typedProblemAuxiliaries
+    :: TypedProblem ref local origin global
+    -> Vector (FrozenCheckedCore global)
+typedProblemAuxiliaries
+        (TypedProblem
+            _route
+            _claim
+            _facts
+            _locals
+            auxiliaries
+            _globals
+            _localTypes) =
+    auxiliaries
+
+typedProblemGlobalTypes
+    :: TypedProblem ref local origin global
+    -> Map global CoreType
+typedProblemGlobalTypes
+        (TypedProblem
+            _route
+            _claim
+            _facts
+            _locals
+            _auxiliaries
+            globals
+            _localTypes) =
+    globals
+
+typedProblemLocalTypes
+    :: TypedProblem ref local origin global
+    -> Map local CoreType
+typedProblemLocalTypes
+        (TypedProblem
+            _route
+            _claim
+            _facts
+            _locals
+            _auxiliaries
+            _globals
+            localTypes) =
+    localTypes
diff --git a/source/Checking/Foundation.hs b/source/Checking/Foundation.hs
index 0364171..83fea67 100644
--- a/source/Checking/Foundation.hs
+++ b/source/Checking/Foundation.hs
@@ -26,6 +26,7 @@ module Checking.Foundation
     , foundationAxiomFrozen
     , foundationAxiomBackendClass
     , foundationRuleSignature
+    , classifyCanonicalFofStructure
     , classifyFrozenCore
     ) where
 
@@ -395,10 +396,17 @@ foundationRuleSignature
 classifyFrozenCore
     :: FrozenCheckedCore global
     -> FoundationBackendClass
-classifyFrozenCore frozen =
+classifyFrozenCore =
+    classifyCanonicalFofStructure
+        . frozenCoreTerm
+
+classifyCanonicalFofStructure
+    :: CanonicalTerm global
+    -> FoundationBackendClass
+classifyCanonicalFofStructure term =
     case Set.toAscList
             (termFofExclusions
-                (frozenCoreTerm frozen)) of
+                term) of
         [] ->
             FoundationFofProjectable
         firstExclusion : remainingExclusions ->
diff --git a/source/Checking/Transition.hs b/source/Checking/Transition.hs
index 8802f90..ae4ea6c 100644
--- a/source/Checking/Transition.hs
+++ b/source/Checking/Transition.hs
@@ -30,6 +30,7 @@ module Checking.Transition
     , TypedSemanticFact
     , prepareTypedSemanticFact
     , typedSemanticStatement
+    , typedSemanticFofCapability
     , TypedDirectAxiomManifestEntry
     , typedDirectAssumptionFact
     , typedDirectAssumptionKind
@@ -82,6 +83,7 @@ module Checking.Transition
     ) where
 
 import Base
+import Checking.Backend.Problem qualified as Backend
 import Checking.Core
 import Checking.Facts qualified as Facts
 import Checking.Foundation
@@ -238,27 +240,55 @@ transitionTypedFactReference = \case
     TransitionTypedFactRef reference ->
         Just reference
 
-newtype TypedSemanticFact = TypedSemanticFact
-    (FrozenCheckedCore CheckedGlobalRef)
+data TypedSemanticFact = TypedSemanticFact
+    !(FrozenCheckedCore CheckedGlobalRef)
+    !(Backend.FofCapability
+        (Backend.CheckedFofProjection
+            Void
+            CheckedGlobalRef))
     deriving stock (Eq)
 
 prepareTypedSemanticFact
     :: FrozenCheckedCore CheckedGlobalRef
     -> Either TransitionModuleError TypedSemanticFact
 prepareTypedSemanticFact statement
-    | frozenCoreType statement == TyProp =
-        Right (TypedSemanticFact statement)
-    | otherwise =
+    | frozenCoreType statement /= TyProp =
         Left
             (TransitionTypedFactIsNotProposition
                 (frozenCoreType statement))
+    | otherwise = do
+        proposition <-
+            first TransitionTypedFactSupportError
+                (Backend.supportedProposition
+                    Vector.empty
+                    (embedClosedCore [] statement))
+        capability <-
+            first TransitionTypedFactClassificationError
+                (Backend.classifySupportedProposition
+                    (Just . checkedGlobalType)
+                    proposition)
+        Right
+            (TypedSemanticFact
+                statement
+                capability)
 
 typedSemanticStatement
     :: TypedSemanticFact
     -> FrozenCheckedCore CheckedGlobalRef
-typedSemanticStatement (TypedSemanticFact statement) =
+typedSemanticStatement
+        (TypedSemanticFact statement _capability) =
     statement
 
+typedSemanticFofCapability
+    :: TypedSemanticFact
+    -> Backend.FofCapability
+        (Backend.CheckedFofProjection
+            Void
+            CheckedGlobalRef)
+typedSemanticFofCapability
+        (TypedSemanticFact _statement capability) =
+    capability
+
 data TypedDirectAxiomManifestEntry =
     TypedDirectAxiomManifestEntry
         !FactRef
@@ -1583,6 +1613,11 @@ data TransitionModuleError
         !(Set CheckedGlobalRef)
     | TransitionTypedFactIsNotProposition
         !CoreType
+    | TransitionTypedFactSupportError
+        !(Backend.SupportedPropositionError Void)
+    | TransitionTypedFactClassificationError
+        !(Backend.BackendClassificationError
+            CheckedGlobalRef)
     | TransitionKernelTargetMismatch
     | TransitionKernelReplayError
         !KernelReplayError