Migrate to `Felix` namespaceHEADhotg

1 files changed, 1264 insertions, 0 deletions

diff --git a/source/Felix/Checking/Kernel/Derivation.hs b/source/Felix/Checking/Kernel/Derivation.hs
new file mode 100644
index 0000000..e83b376
--- /dev/null
+++ b/source/Felix/Checking/Kernel/Derivation.hs
@@ -0,0 +1,1264 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Private in-memory proof trees and independent kernel replay.
+module Felix.Checking.Kernel.Derivation
+    ( ImportIx
+    , importIx
+    , importIxValue
+    , HypothesisIx
+    , hypothesisIx
+    , DerivationImportJudgment
+    , derivationImportJudgment
+    , derivationImportStatement
+    , KernelDerivation
+    , mapKernelDerivationGlobals
+    , importedFactDerivation
+    , localHypothesisDerivation
+    , foundationFactDerivation
+    , implicationEliminationDerivation
+    , forallEliminationDerivation
+    , falsumEliminationDerivation
+    , implicationIntroductionDerivation
+    , forallIntroductionDerivation
+    , ConversionPlan
+    , conversionPlan
+    , conversionPlanBudget
+    , ConversionPlanError(..)
+    , convertJudgmentDerivation
+    , equalityReflexivityDerivation
+    , scopedEqualityReflexivityDerivation
+    , equalityCongruenceApplicationDerivation
+    , equalityCongruenceLambdaDerivation
+    , equalityModusPonensDerivation
+    , setLfpBoundDerivation
+    , setLfpLeastDerivation
+    , setLfpFixedDerivation
+    , setLfpInductDerivation
+    , weakenDerivationHypotheses
+    , KernelReplayLimits
+    , kernelReplayLimits
+    , defaultKernelReplayLimits
+    , KernelReplayLimitError(..)
+    , ReplayedKernelDerivation
+    , replayKernelDerivation
+    , replayedKernelTarget
+    , replayedKernelImportUses
+    , replayedKernelFoundationUses
+    , replayedKernelRuleUses
+    , replayedKernelNodeCount
+    , replayedKernelMaximumDepth
+    , DerivationImportError(..)
+    , KernelReplayError(..)
+    ) where
+
+import Base
+import Felix.Checking.Core
+import Felix.Checking.Foundation
+import Felix.Checking.Kernel.Semantics qualified as Semantics
+import Felix.Checking.Kernel.SetLfp qualified as SetLfp
+
+import Control.Monad (unless)
+import Data.Bifunctor (first)
+import Data.Set qualified as Set
+import Data.Vector (Vector)
+import Data.Vector qualified as Vector
+import Numeric.Natural (Natural)
+
+
+newtype ImportIx = ImportIx Natural
+    deriving stock (Show, Eq, Ord)
+
+importIx :: Natural -> ImportIx
+importIx = ImportIx
+
+importIxValue :: ImportIx -> Natural
+importIxValue (ImportIx index) =
+    index
+
+newtype HypothesisIx = HypothesisIx Natural
+    deriving stock (Show, Eq, Ord)
+
+hypothesisIx :: Natural -> HypothesisIx
+hypothesisIx = HypothesisIx
+
+newtype DerivationImportJudgment global =
+    DerivationImportJudgment
+        (FrozenCheckedCore global)
+    deriving stock (Eq)
+
+data DerivationImportError =
+    DerivationImportIsNotProposition !CoreType
+    deriving stock (Show, Eq)
+
+derivationImportJudgment
+    :: FrozenCheckedCore global
+    -> Either
+        DerivationImportError
+        (DerivationImportJudgment global)
+derivationImportJudgment statement
+    | frozenCoreType statement == TyProp =
+        Right (DerivationImportJudgment statement)
+    | otherwise =
+        Left
+            (DerivationImportIsNotProposition
+                (frozenCoreType statement))
+
+derivationImportStatement
+    :: DerivationImportJudgment global
+    -> FrozenCheckedCore global
+derivationImportStatement
+        (DerivationImportJudgment statement) =
+    statement
+
+data KernelDerivation global
+    = UseImportedFact !ImportIx
+    | UseLocalHypothesis !HypothesisIx
+    | UseFoundationFact !FoundationAxiomTag
+    | ImplicationElimination
+        !(KernelDerivation global)
+        !(KernelDerivation global)
+    | ForallElimination
+        !(KernelDerivation global)
+        !(ScopedCheckedCore global)
+    | FalsumElimination
+        !(KernelDerivation global)
+        !(ScopedCheckedCore global)
+    | ImplicationIntroduction
+        !(ScopedCheckedCore global)
+        !(KernelDerivation global)
+    | ForallIntroduction
+        !CoreType
+        !(KernelDerivation global)
+    | ConvertJudgment
+        !(KernelDerivation global)
+        !(ScopedCheckedCore global)
+        !ConversionPlan
+    | EqualityReflexivity
+        !(ScopedCheckedCore global)
+    | EqualityCongruenceApplication
+        !(KernelDerivation global)
+        !(KernelDerivation global)
+    | EqualityCongruenceLambda
+        !CoreType
+        !(KernelDerivation global)
+    | EqualityModusPonens
+        !(KernelDerivation global)
+        !(KernelDerivation global)
+    | ApplySetLfpBound
+        !(ScopedCheckedCore global)
+        !(ScopedCheckedCore global)
+    | ApplySetLfpLeast
+        !(ScopedCheckedCore global)
+        !(ScopedCheckedCore global)
+        !(ScopedCheckedCore global)
+        !(KernelDerivation global)
+        !(KernelDerivation global)
+    | ApplySetLfpFixed
+        !(ScopedCheckedCore global)
+        !(ScopedCheckedCore global)
+        !(KernelDerivation global)
+    | ApplySetLfpInduct
+        !(ScopedCheckedCore global)
+        !(ScopedCheckedCore global)
+        !(ScopedCheckedCore global)
+        !(ScopedCheckedCore global)
+        !(KernelDerivation global)
+        !(KernelDerivation global)
+        !(KernelDerivation global)
+    deriving stock (Eq)
+
+mapKernelDerivationGlobals
+    :: (left -> right)
+    -> KernelDerivation left
+    -> KernelDerivation right
+mapKernelDerivationGlobals transform = go
+  where
+    scoped = mapScopedGlobals transform
+    go = \case
+        UseImportedFact index ->
+            UseImportedFact index
+        UseLocalHypothesis index ->
+            UseLocalHypothesis index
+        UseFoundationFact tag ->
+            UseFoundationFact tag
+        ImplicationElimination premise implication ->
+            ImplicationElimination (go premise) (go implication)
+        ForallElimination proof argument ->
+            ForallElimination (go proof) (scoped argument)
+        FalsumElimination proof target ->
+            FalsumElimination (go proof) (scoped target)
+        ImplicationIntroduction premise proof ->
+            ImplicationIntroduction (scoped premise) (go proof)
+        ForallIntroduction binderType proof ->
+            ForallIntroduction binderType (go proof)
+        ConvertJudgment proof target plan ->
+            ConvertJudgment (go proof) (scoped target) plan
+        EqualityReflexivity term ->
+            EqualityReflexivity (scoped term)
+        EqualityCongruenceApplication function argument ->
+            EqualityCongruenceApplication (go function) (go argument)
+        EqualityCongruenceLambda binderType proof ->
+            EqualityCongruenceLambda binderType (go proof)
+        EqualityModusPonens equality proof ->
+            EqualityModusPonens (go equality) (go proof)
+        ApplySetLfpBound domain operator ->
+            ApplySetLfpBound (scoped domain) (scoped operator)
+        ApplySetLfpLeast domain operator candidate bounded closed ->
+            ApplySetLfpLeast
+                (scoped domain)
+                (scoped operator)
+                (scoped candidate)
+                (go bounded)
+                (go closed)
+        ApplySetLfpFixed domain operator monotone ->
+            ApplySetLfpFixed
+                (scoped domain)
+                (scoped operator)
+                (go monotone)
+        ApplySetLfpInduct domain operator predicate element
+                monotone member closed ->
+            ApplySetLfpInduct
+                (scoped domain)
+                (scoped operator)
+                (scoped predicate)
+                (scoped element)
+                (go monotone)
+                (go member)
+                (go closed)
+
+importedFactDerivation
+    :: ImportIx
+    -> KernelDerivation global
+importedFactDerivation =
+    UseImportedFact
+
+localHypothesisDerivation
+    :: HypothesisIx
+    -> KernelDerivation global
+localHypothesisDerivation =
+    UseLocalHypothesis
+
+foundationFactDerivation
+    :: FoundationAxiomTag
+    -> KernelDerivation global
+foundationFactDerivation =
+    UseFoundationFact
+
+implicationEliminationDerivation
+    :: KernelDerivation global
+    -> KernelDerivation global
+    -> KernelDerivation global
+implicationEliminationDerivation =
+    ImplicationElimination
+
+forallEliminationDerivation
+    :: KernelDerivation global
+    -> ScopedCheckedCore global
+    -> KernelDerivation global
+forallEliminationDerivation =
+    ForallElimination
+
+falsumEliminationDerivation
+    :: KernelDerivation global
+    -> ScopedCheckedCore global
+    -> KernelDerivation global
+falsumEliminationDerivation =
+    FalsumElimination
+
+implicationIntroductionDerivation
+    :: ScopedCheckedCore global
+    -> KernelDerivation global
+    -> KernelDerivation global
+implicationIntroductionDerivation =
+    ImplicationIntroduction
+
+forallIntroductionDerivation
+    :: CoreType
+    -> KernelDerivation global
+    -> KernelDerivation global
+forallIntroductionDerivation =
+    ForallIntroduction
+
+newtype ConversionPlan = ConversionPlan Natural
+    deriving stock (Show, Eq, Ord)
+
+data ConversionPlanError =
+    ConversionPlanExceedsLimit !Natural
+    deriving stock (Show, Eq)
+
+conversionPlanLimit :: Natural
+conversionPlanLimit =
+    100000
+
+conversionPlan
+    :: Natural
+    -> Either ConversionPlanError ConversionPlan
+conversionPlan budget
+    | budget <= conversionPlanLimit =
+        Right (ConversionPlan budget)
+    | otherwise =
+        Left (ConversionPlanExceedsLimit budget)
+
+conversionPlanBudget :: ConversionPlan -> Natural
+conversionPlanBudget (ConversionPlan budget) =
+    budget
+
+convertJudgmentDerivation
+    :: KernelDerivation global
+    -> ScopedCheckedCore global
+    -> ConversionPlan
+    -> KernelDerivation global
+convertJudgmentDerivation =
+    ConvertJudgment
+
+equalityReflexivityDerivation
+    :: FrozenCheckedCore global
+    -> KernelDerivation global
+equalityReflexivityDerivation =
+    EqualityReflexivity . embedClosedCore []
+
+scopedEqualityReflexivityDerivation
+    :: ScopedCheckedCore global
+    -> KernelDerivation global
+scopedEqualityReflexivityDerivation =
+    EqualityReflexivity
+
+equalityCongruenceApplicationDerivation
+    :: KernelDerivation global
+    -> KernelDerivation global
+    -> KernelDerivation global
+equalityCongruenceApplicationDerivation =
+    EqualityCongruenceApplication
+
+equalityCongruenceLambdaDerivation
+    :: CoreType
+    -> KernelDerivation global
+    -> KernelDerivation global
+equalityCongruenceLambdaDerivation =
+    EqualityCongruenceLambda
+
+equalityModusPonensDerivation
+    :: KernelDerivation global
+    -> KernelDerivation global
+    -> KernelDerivation global
+equalityModusPonensDerivation =
+    EqualityModusPonens
+
+setLfpBoundDerivation
+    :: ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> KernelDerivation global
+setLfpBoundDerivation =
+    ApplySetLfpBound
+
+setLfpLeastDerivation
+    :: ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> KernelDerivation global
+    -> KernelDerivation global
+    -> KernelDerivation global
+setLfpLeastDerivation =
+    ApplySetLfpLeast
+
+setLfpFixedDerivation
+    :: ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> KernelDerivation global
+    -> KernelDerivation global
+setLfpFixedDerivation =
+    ApplySetLfpFixed
+
+setLfpInductDerivation
+    :: ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> KernelDerivation global
+    -> KernelDerivation global
+    -> KernelDerivation global
+    -> KernelDerivation global
+setLfpInductDerivation =
+    ApplySetLfpInduct
+
+-- | Add hypotheses outside a derivation while preserving hypotheses introduced
+-- by implication nodes inside it.
+weakenDerivationHypotheses
+    :: Natural
+    -> KernelDerivation global
+    -> KernelDerivation global
+weakenDerivationHypotheses amount =
+    shift 0
+  where
+    shift cutoff = \case
+        UseImportedFact index ->
+            UseImportedFact index
+        UseLocalHypothesis (HypothesisIx index) ->
+            UseLocalHypothesis
+                (HypothesisIx
+                    (if index >= cutoff
+                        then index + amount
+                        else index))
+        UseFoundationFact tag ->
+            UseFoundationFact tag
+        ImplicationElimination implication premise ->
+            ImplicationElimination
+                (shift cutoff implication)
+                (shift cutoff premise)
+        ForallElimination quantified argument ->
+            ForallElimination
+                (shift cutoff quantified)
+                argument
+        FalsumElimination falsum target ->
+            FalsumElimination
+                (shift cutoff falsum)
+                target
+        ImplicationIntroduction premise body ->
+            ImplicationIntroduction
+                premise
+                (shift (cutoff + 1) body)
+        ForallIntroduction binderType body ->
+            ForallIntroduction
+                binderType
+                (shift cutoff body)
+        ConvertJudgment source target plan ->
+            ConvertJudgment
+                (shift cutoff source)
+                target
+                plan
+        EqualityReflexivity operand ->
+            EqualityReflexivity operand
+        EqualityCongruenceApplication function argument ->
+            EqualityCongruenceApplication
+                (shift cutoff function)
+                (shift cutoff argument)
+        EqualityCongruenceLambda binderType body ->
+            EqualityCongruenceLambda
+                binderType
+                (shift cutoff body)
+        EqualityModusPonens equality premise ->
+            EqualityModusPonens
+                (shift cutoff equality)
+                (shift cutoff premise)
+        ApplySetLfpBound domain operator ->
+            ApplySetLfpBound domain operator
+        ApplySetLfpLeast
+                domain operator candidate
+                closed bounded ->
+            ApplySetLfpLeast
+                domain
+                operator
+                candidate
+                (shift cutoff closed)
+                (shift cutoff bounded)
+        ApplySetLfpFixed domain operator monotone ->
+            ApplySetLfpFixed
+                domain
+                operator
+                (shift cutoff monotone)
+        ApplySetLfpInduct
+                domain operator predicate element
+                monotone member closure ->
+            ApplySetLfpInduct
+                domain
+                operator
+                predicate
+                element
+                (shift cutoff monotone)
+                (shift cutoff member)
+                (shift cutoff closure)
+
+data KernelReplayLimits = KernelReplayLimits
+    !Natural
+    !Natural
+    deriving stock (Show, Eq)
+
+data KernelReplayLimitError
+    = KernelReplayNodeLimitIsZero
+    | KernelReplayNodeLimitTooLarge !Natural
+    | KernelReplayDepthLimitTooLarge !Natural
+    deriving stock (Show, Eq)
+
+maximumKernelReplayNodes :: Natural
+maximumKernelReplayNodes =
+    1000000
+
+maximumKernelReplayDepth :: Natural
+maximumKernelReplayDepth =
+    4096
+
+kernelReplayLimits
+    :: Natural
+    -> Natural
+    -> Either KernelReplayLimitError KernelReplayLimits
+kernelReplayLimits nodeLimit depthLimit
+    | nodeLimit == 0 =
+        Left KernelReplayNodeLimitIsZero
+    | nodeLimit > maximumKernelReplayNodes =
+        Left (KernelReplayNodeLimitTooLarge nodeLimit)
+    | depthLimit > maximumKernelReplayDepth =
+        Left (KernelReplayDepthLimitTooLarge depthLimit)
+    | otherwise =
+        Right
+            (KernelReplayLimits
+                nodeLimit
+                depthLimit)
+
+defaultKernelReplayLimits :: KernelReplayLimits
+defaultKernelReplayLimits =
+    KernelReplayLimits
+        200000
+        2048
+
+data ReplayedKernelDerivation global =
+    ReplayedKernelDerivation
+        !(FrozenCheckedCore global)
+        !(Set ImportIx)
+        !(Set FoundationAxiomTag)
+        !(Set KernelRuleTag)
+        !Natural
+        !Natural
+    deriving stock (Eq)
+
+replayedKernelTarget
+    :: ReplayedKernelDerivation global
+    -> FrozenCheckedCore global
+replayedKernelTarget
+        (ReplayedKernelDerivation
+            target
+            _importUses
+            _foundationUses
+            _ruleUses
+            _nodeCount
+            _maximumDepth) =
+    target
+
+replayedKernelImportUses
+    :: ReplayedKernelDerivation global
+    -> Set ImportIx
+replayedKernelImportUses
+        (ReplayedKernelDerivation
+            _target
+            importUses
+            _foundationUses
+            _ruleUses
+            _nodeCount
+            _maximumDepth) =
+    importUses
+
+replayedKernelFoundationUses
+    :: ReplayedKernelDerivation global
+    -> Set FoundationAxiomTag
+replayedKernelFoundationUses
+        (ReplayedKernelDerivation
+            _target
+            _importUses
+            foundationUses
+            _ruleUses
+            _nodeCount
+            _maximumDepth) =
+    foundationUses
+
+replayedKernelRuleUses
+    :: ReplayedKernelDerivation global
+    -> Set KernelRuleTag
+replayedKernelRuleUses
+        (ReplayedKernelDerivation
+            _target
+            _importUses
+            _foundationUses
+            ruleUses
+            _nodeCount
+            _maximumDepth) =
+    ruleUses
+
+replayedKernelNodeCount
+    :: ReplayedKernelDerivation global
+    -> Natural
+replayedKernelNodeCount
+        (ReplayedKernelDerivation
+            _target
+            _importUses
+            _foundationUses
+            _ruleUses
+            nodeCount
+            _maximumDepth) =
+    nodeCount
+
+replayedKernelMaximumDepth
+    :: ReplayedKernelDerivation global
+    -> Natural
+replayedKernelMaximumDepth
+        (ReplayedKernelDerivation
+            _target
+            _importUses
+            _foundationUses
+            _ruleUses
+            _nodeCount
+            maximumDepth) =
+    maximumDepth
+
+data ReplayStep global = ReplayStep
+    !(ScopedCheckedCore global)
+    !(Set ImportIx)
+    !(Set FoundationAxiomTag)
+    !(Set KernelRuleTag)
+    !Natural
+    !Natural
+
+data KernelReplayError
+    = KernelReplaySemanticsError
+        !Semantics.KernelSemanticsError
+    | KernelReplaySetLfpRuleError
+        !SetLfp.SetLfpRuleError
+    | KernelReplayImportOutOfBounds !ImportIx
+    | KernelReplayHypothesisOutOfBounds !HypothesisIx
+    | KernelReplayStoredContextMismatch
+        ![CoreType]
+        ![CoreType]
+    | KernelReplayStoredTermIllTyped !CoreCheckError
+    | KernelReplayStoredTypeMismatch
+        !CoreType
+        !CoreType
+    | KernelReplayWeakeningError !CoreCheckError
+    | KernelReplayNodeLimitExceeded !Natural
+    | KernelReplayDepthLimitExceeded !Natural
+    | KernelReplayRootRemainedOpen
+    | KernelReplayTargetMismatch
+    deriving stock (Show, Eq)
+
+replayKernelDerivation
+    :: Eq global
+    => CheckedFoundation
+    -> KernelReplayLimits
+    -> (global -> Maybe CoreType)
+    -> Vector (DerivationImportJudgment global)
+    -> FrozenCheckedCore global
+    -> KernelDerivation global
+    -> Either
+        KernelReplayError
+        (ReplayedKernelDerivation global)
+replayKernelDerivation
+        checkedFoundationValue
+        limits
+        globalType
+        imports
+        expectedTarget
+        derivation =
+    checkedFoundationValue `seq` do
+        expectedTarget' <-
+            recheckClosed expectedTarget
+        ReplayStep
+            synthesized
+            importUses
+            foundationUses
+            ruleUses
+            nodeCount
+            maximumDepth <-
+                replay [] [] 0 derivation
+        closed <-
+            maybe
+                (Left KernelReplayRootRemainedOpen)
+                Right
+                (closeScopedCore synthesized)
+        unless
+            (closed == expectedTarget')
+            (Left KernelReplayTargetMismatch)
+        pure
+            (ReplayedKernelDerivation
+                closed
+                importUses
+                foundationUses
+                ruleUses
+                nodeCount
+                maximumDepth)
+  where
+    replay context hypotheses depth derivationNode
+        | depth > replayDepthLimit =
+            Left
+                (KernelReplayDepthLimitExceeded
+                    replayDepthLimit)
+        | otherwise = do
+            step <-
+                replayWithin
+                    context
+                    hypotheses
+                    depth
+                    derivationNode
+            if stepNodeCount step > replayNodeLimit
+                then
+                    Left
+                        (KernelReplayNodeLimitExceeded
+                            replayNodeLimit)
+                else
+                    Right step
+
+    replayWithin context hypotheses depth = \case
+        UseImportedFact index -> do
+            judgment <-
+                lookupImport index
+            statement <-
+                recheckStored
+                    context
+                    (embedClosedCore context
+                        (derivationImportStatement
+                            judgment))
+            pure
+                (leaf
+                    depth
+                    statement
+                    (Set.singleton index)
+                    mempty)
+        UseLocalHypothesis index -> do
+            hypothesis <-
+                lookupHypothesis index hypotheses
+            checkedHypothesis <-
+                recheckStored context hypothesis
+            pure
+                (leaf
+                    depth
+                    checkedHypothesis
+                    mempty
+                    mempty)
+        UseFoundationFact tag -> do
+            statement <-
+                recheckStored
+                    context
+                    (embedClosedCore context
+                        (mapFrozenGlobals
+                            absurd
+                            (foundationAxiomFrozen
+                                checkedFoundationValue
+                                tag)))
+            pure
+                (leaf
+                    depth
+                    statement
+                    mempty
+                    (Set.singleton tag))
+        ImplicationElimination implication premise -> do
+            implicationStep <-
+                replay context hypotheses (depth + 1) implication
+            premiseStep <-
+                replay context hypotheses (depth + 1) premise
+            combine2 depth
+                (Semantics.implicationElimination
+                    globalType
+                    (stepValue implicationStep)
+                    (stepValue premiseStep))
+                implicationStep
+                premiseStep
+        ForallElimination quantified argument -> do
+            argument' <-
+                recheckStored context argument
+            quantifiedStep <-
+                replay context hypotheses (depth + 1) quantified
+            combine1 depth
+                (Semantics.forallElimination
+                    globalType
+                    (stepValue quantifiedStep)
+                    argument')
+                quantifiedStep
+        FalsumElimination falsum target -> do
+            target' <-
+                recheckStored context target
+            falsumStep <-
+                replay context hypotheses (depth + 1) falsum
+            combine1 depth
+                (Semantics.falsumElimination
+                    globalType
+                    (stepValue falsumStep)
+                    target')
+                falsumStep
+        ImplicationIntroduction premise body -> do
+            premise' <-
+                recheckStored context premise
+            bodyStep <-
+                replay
+                    context
+                    (premise' : hypotheses)
+                    (depth + 1)
+                    body
+            combine1 depth
+                (Semantics.implicationIntroduction
+                    globalType
+                    premise'
+                    (stepValue bodyStep))
+                bodyStep
+        ForallIntroduction binderType body -> do
+            weakenedHypotheses <-
+                traverse
+                    (first KernelReplayWeakeningError
+                        . weakenScopedCore
+                            globalType
+                            binderType)
+                    hypotheses
+            bodyStep <-
+                replay
+                    (binderType : context)
+                    weakenedHypotheses
+                    (depth + 1)
+                    body
+            combine1 depth
+                (Semantics.forallIntroduction
+                    globalType
+                    binderType
+                    (stepValue bodyStep))
+                bodyStep
+        ConvertJudgment source target plan -> do
+            target' <-
+                recheckStored context target
+            sourceStep <-
+                replay
+                    context
+                    hypotheses
+                    (depth + 1)
+                    source
+            combine1 depth
+                (Semantics.convertJudgment
+                    globalType
+                    (conversionPlanBudget plan)
+                    (stepValue sourceStep)
+                    target')
+                sourceStep
+        EqualityReflexivity operand -> do
+            operand' <-
+                recheckStored context operand
+            value <-
+                first KernelReplaySemanticsError
+                    (Semantics.equalityReflexivity
+                        globalType
+                        operand')
+            pure (leaf depth value mempty mempty)
+        EqualityCongruenceApplication
+                functionEquality
+                argumentEquality -> do
+            functionStep <-
+                replay
+                    context
+                    hypotheses
+                    (depth + 1)
+                    functionEquality
+            argumentStep <-
+                replay
+                    context
+                    hypotheses
+                    (depth + 1)
+                    argumentEquality
+            combine2 depth
+                (Semantics.equalityCongruenceApplication
+                    globalType
+                    (stepValue functionStep)
+                    (stepValue argumentStep))
+                functionStep
+                argumentStep
+        EqualityCongruenceLambda binderType bodyEquality -> do
+            weakenedHypotheses <-
+                traverse
+                    (first KernelReplayWeakeningError
+                        . weakenScopedCore
+                            globalType
+                            binderType)
+                    hypotheses
+            bodyStep <-
+                replay
+                    (binderType : context)
+                    weakenedHypotheses
+                    (depth + 1)
+                    bodyEquality
+            combine1 depth
+                (Semantics.equalityCongruenceLambda
+                    globalType
+                    binderType
+                    (stepValue bodyStep))
+                bodyStep
+        EqualityModusPonens equality premise -> do
+            equalityStep <-
+                replay context hypotheses (depth + 1) equality
+            premiseStep <-
+                replay context hypotheses (depth + 1) premise
+            combine2 depth
+                (Semantics.equalityModusPonens
+                    globalType
+                    (stepValue equalityStep)
+                    (stepValue premiseStep))
+                equalityStep
+                premiseStep
+        ApplySetLfpBound domain operator -> do
+            domain' <-
+                recheckStored context domain
+            operator' <-
+                recheckStored context operator
+            value <-
+                first KernelReplaySetLfpRuleError
+                    (SetLfp.setLfpBound
+                        checkedFoundationValue
+                        globalType
+                        domain'
+                        operator')
+            pure
+                (ruleLeaf
+                    depth
+                    SetLfpBound
+                    value)
+        ApplySetLfpLeast
+                domain
+                operator
+                candidate
+                closedPremise
+                boundedPremise -> do
+            domain' <-
+                recheckStored context domain
+            operator' <-
+                recheckStored context operator
+            candidate' <-
+                recheckStored context candidate
+            closedStep <-
+                replay
+                    context
+                    hypotheses
+                    (depth + 1)
+                    closedPremise
+            boundedStep <-
+                replay
+                    context
+                    hypotheses
+                    (depth + 1)
+                    boundedPremise
+            combineRule depth SetLfpLeast
+                (SetLfp.setLfpLeast
+                    checkedFoundationValue
+                    globalType
+                    domain'
+                    operator'
+                    candidate'
+                    (stepValue closedStep)
+                    (stepValue boundedStep))
+                [closedStep, boundedStep]
+        ApplySetLfpFixed domain operator monotonePremise -> do
+            domain' <-
+                recheckStored context domain
+            operator' <-
+                recheckStored context operator
+            monotoneStep <-
+                replay
+                    context
+                    hypotheses
+                    (depth + 1)
+                    monotonePremise
+            combineRule depth SetLfpFixed
+                (SetLfp.setLfpFixed
+                    checkedFoundationValue
+                    globalType
+                    domain'
+                    operator'
+                    (stepValue monotoneStep))
+                [monotoneStep]
+        ApplySetLfpInduct
+                domain
+                operator
+                predicate
+                element
+                monotonePremise
+                memberPremise
+                closurePremise -> do
+            domain' <-
+                recheckStored context domain
+            operator' <-
+                recheckStored context operator
+            predicate' <-
+                recheckStored context predicate
+            element' <-
+                recheckStored context element
+            monotoneStep <-
+                replay
+                    context
+                    hypotheses
+                    (depth + 1)
+                    monotonePremise
+            memberStep <-
+                replay
+                    context
+                    hypotheses
+                    (depth + 1)
+                    memberPremise
+            closureStep <-
+                replay
+                    context
+                    hypotheses
+                    (depth + 1)
+                    closurePremise
+            combineRule depth SetLfpInduct
+                (SetLfp.setLfpInduct
+                    checkedFoundationValue
+                    globalType
+                    domain'
+                    operator'
+                    predicate'
+                    element'
+                    (stepValue monotoneStep)
+                    (stepValue memberStep)
+                    (stepValue closureStep))
+                [ monotoneStep
+                , memberStep
+                , closureStep
+                ]
+
+    lookupImport index@(ImportIx naturalIndex)
+        | naturalIndex
+            > fromIntegral (maxBound :: Int) =
+                Left
+                    (KernelReplayImportOutOfBounds
+                        index)
+        | otherwise =
+            maybe
+                (Left
+                    (KernelReplayImportOutOfBounds
+                        index))
+                Right
+                (imports
+                    Vector.!?
+                        (fromIntegral naturalIndex))
+
+    lookupHypothesis
+            index@(HypothesisIx naturalIndex)
+            hypotheses =
+        maybe
+            (Left
+                (KernelReplayHypothesisOutOfBounds
+                    index))
+            Right
+            (atNatural naturalIndex hypotheses)
+
+    requireContext expected value
+        | scopedCoreContext value == expected =
+            Right ()
+        | otherwise =
+            Left
+                (KernelReplayStoredContextMismatch
+                    expected
+                    (scopedCoreContext value))
+
+    recheckStored expectedContext stored = do
+        requireContext expectedContext stored
+        checked <-
+            first KernelReplayStoredTermIllTyped
+                (checkScopedCanonicalCore
+                    globalType
+                    expectedContext
+                    (scopedCoreTerm stored))
+        unless
+            (scopedCoreType checked
+                == scopedCoreType stored)
+            (Left
+                (KernelReplayStoredTypeMismatch
+                    (scopedCoreType stored)
+                    (scopedCoreType checked)))
+        pure checked
+
+    recheckClosed stored = do
+        checked <-
+            first KernelReplayStoredTermIllTyped
+                (checkCanonicalCore
+                    globalType
+                    (frozenCoreTerm stored))
+        unless
+            (frozenCoreType checked
+                == frozenCoreType stored)
+            (Left
+                (KernelReplayStoredTypeMismatch
+                    (frozenCoreType stored)
+                    (frozenCoreType checked)))
+        pure checked
+
+    replayNodeLimit =
+        case limits of
+            KernelReplayLimits nodeLimit _depthLimit ->
+                nodeLimit
+
+    replayDepthLimit =
+        case limits of
+            KernelReplayLimits _nodeLimit depthLimit ->
+                depthLimit
+
+leaf
+    :: Natural
+    -> ScopedCheckedCore global
+    -> Set ImportIx
+    -> Set FoundationAxiomTag
+    -> ReplayStep global
+leaf depth value importUses foundationUses =
+    ReplayStep
+        value
+        importUses
+        foundationUses
+        mempty
+        1
+        depth
+
+ruleLeaf
+    :: Natural
+    -> KernelRuleTag
+    -> ScopedCheckedCore global
+    -> ReplayStep global
+ruleLeaf depth tag value =
+    ReplayStep
+        value
+        mempty
+        mempty
+        (Set.singleton tag)
+        1
+        depth
+
+stepValue :: ReplayStep global -> ScopedCheckedCore global
+stepValue
+        (ReplayStep
+            value
+            _importUses
+            _foundationUses
+            _ruleUses
+            _nodeCount
+            _maximumDepth) =
+    value
+
+combine1
+    :: Natural
+    -> Either
+        Semantics.KernelSemanticsError
+        (ScopedCheckedCore global)
+    -> ReplayStep global
+    -> Either KernelReplayError (ReplayStep global)
+combine1 depth synthesized child = do
+    value <-
+        first KernelReplaySemanticsError synthesized
+    pure
+        (ReplayStep
+            value
+            (stepImportUses child)
+            (stepFoundationUses child)
+            (stepRuleUses child)
+            (1 + stepNodeCount child)
+            (max depth
+                (stepMaximumDepth child)))
+
+combine2
+    :: Natural
+    -> Either
+        Semantics.KernelSemanticsError
+        (ScopedCheckedCore global)
+    -> ReplayStep global
+    -> ReplayStep global
+    -> Either KernelReplayError (ReplayStep global)
+combine2 depth synthesized left right = do
+    value <-
+        first KernelReplaySemanticsError synthesized
+    pure
+        (ReplayStep
+            value
+            (stepImportUses left
+                <> stepImportUses right)
+            (stepFoundationUses left
+                <> stepFoundationUses right)
+            (stepRuleUses left
+                <> stepRuleUses right)
+            (1
+                + stepNodeCount left
+                + stepNodeCount right)
+            (maximum
+                [ depth
+                , stepMaximumDepth left
+                , stepMaximumDepth right
+                ]))
+
+combineRule
+    :: Natural
+    -> KernelRuleTag
+    -> Either
+        SetLfp.SetLfpRuleError
+        (ScopedCheckedCore global)
+    -> [ReplayStep global]
+    -> Either KernelReplayError (ReplayStep global)
+combineRule depth tag synthesized children = do
+    value <-
+        first KernelReplaySetLfpRuleError synthesized
+    pure
+        (ReplayStep
+            value
+            (foldMap stepImportUses children)
+            (foldMap stepFoundationUses children)
+            (Set.insert tag
+                (foldMap stepRuleUses children))
+            (1 + sum (stepNodeCount <$> children))
+            (maximum
+                (depth
+                    : (stepMaximumDepth <$> children))))
+
+stepImportUses
+    :: ReplayStep global
+    -> Set ImportIx
+stepImportUses
+        (ReplayStep
+            _value
+            importUses
+            _foundationUses
+            _ruleUses
+            _nodeCount
+            _maximumDepth) =
+    importUses
+
+stepFoundationUses
+    :: ReplayStep global
+    -> Set FoundationAxiomTag
+stepFoundationUses
+        (ReplayStep
+            _value
+            _importUses
+            foundationUses
+            _ruleUses
+            _nodeCount
+            _maximumDepth) =
+    foundationUses
+
+stepRuleUses
+    :: ReplayStep global
+    -> Set KernelRuleTag
+stepRuleUses
+        (ReplayStep
+            _value
+            _importUses
+            _foundationUses
+            ruleUses
+            _nodeCount
+            _maximumDepth) =
+    ruleUses
+
+stepNodeCount :: ReplayStep global -> Natural
+stepNodeCount
+        (ReplayStep
+            _value
+            _importUses
+            _foundationUses
+            _ruleUses
+            nodeCount
+            _maximumDepth) =
+    nodeCount
+
+stepMaximumDepth :: ReplayStep global -> Natural
+stepMaximumDepth
+        (ReplayStep
+            _value
+            _importUses
+            _foundationUses
+            _ruleUses
+            _nodeCount
+            maximumDepth) =
+    maximumDepth
+
+atNatural :: Natural -> [a] -> Maybe a
+atNatural _index [] =
+    Nothing
+atNatural 0 (value : _rest) =
+    Just value
+atNatural index (_value : rest) =
+    atNatural (index - 1) rest