Support proof-local function graphsHEADhotg

10 files changed, 701 insertions, 70 deletions

diff --git a/source/Checking/Core.hs b/source/Checking/Core.hs
index 6e8d175..4b7478f 100644
--- a/source/Checking/Core.hs
+++ b/source/Checking/Core.hs
@@ -49,6 +49,8 @@ module Checking.Core
     , weakenCheckedScopedCore
     , weakenScopedCore
     , scopedSetDefinition
+    , scopedCharacteristicDefinition
+    , scopedReplacementGraph
     , implyScopedCore
     , splitScopedSetEquality
     , scopedSetInductionHypothesis
@@ -697,53 +699,194 @@ weakenScopedCore globalType binderType scoped =
         (shiftCanonical 1 0
             (scopedCoreTerm scoped))
 
--- | Introduce a fresh set-valued local definition.  Separation uses the
--- checked characteristic rule so its local premise remains first-order.
+-- | Introduce a fresh set-valued local definition. Separation specializes
+-- the checked foundation characteristic so its local premise remains
+-- first-order.
 scopedSetDefinition
-    :: ScopedCheckedCore global
+    :: Eq global
+    => FrozenCheckedCore Void
+    -> ScopedCheckedCore global
     -> Maybe (ScopedCheckedCore global)
 scopedSetDefinition
-        (ScopedCheckedCore context TySet expression) =
-    Just
-        (ScopedCheckedCore
-            (TySet : context)
-            TyProp
-            (case expression of
-                CApp
-                        (CApp (CIntrinsic Sep) bound)
-                        (CLam TySet predicate) ->
-                    separationCharacteristic bound predicate
-                _ ->
-                    CEq
+        characteristic
+        expression@(ScopedCheckedCore context TySet term) =
+    case term of
+        CApp
+                (CApp (CIntrinsic Sep) bound)
+                predicate@(CLam TySet _body) ->
+            scopedCharacteristicDefinition
+                characteristic
+                expression
+                ( ScopedCheckedCore context TySet bound
+                    :| [ ScopedCheckedCore
+                            context
+                            (TySet `TyArrow` TyProp)
+                            predicate
+                       ]
+                )
+        _ ->
+            Just
+                (ScopedCheckedCore
+                    (TySet : context)
+                    TyProp
+                    (CEq
                         TySet
                         (CBound 0)
-                        (shiftCanonical 1 0 expression)))
-  where
-    separationCharacteristic bound predicate =
-        CForall
-            TySet
-            (CEq
-                TyProp
-                (member (CBound 0) (CBound 1))
-                (andP
-                    (member
-                        (CBound 0)
-                        (shiftCanonical 2 0 bound))
-                    (shiftCanonical 1 1 predicate)))
+                        (shiftCanonical 1 0 term)))
+scopedSetDefinition _characteristic _expression =
+    Nothing
 
-    member element set =
-        CApp
-            (CApp (CIntrinsic Member) element)
-            set
+-- | Specialize a checked characteristic and abstract its set-valued target
+-- into one fresh nearest binder. Checked substitution and beta reduction
+-- preserve the foundation row's proposition type.
+scopedCharacteristicDefinition
+    :: Eq global
+    => FrozenCheckedCore Void
+    -> ScopedCheckedCore global
+    -> NonEmpty (ScopedCheckedCore global)
+    -> Maybe (ScopedCheckedCore global)
+scopedCharacteristicDefinition
+        (FrozenCheckedCore TyProp frozen)
+        (ScopedCheckedCore context TySet target)
+        arguments
+    | all ((== context) . scopedCoreContext) arguments = do
+        specialized <-
+            specialize
+                (mapCanonicalGlobals absurd frozen)
+                (toList arguments)
+        let normalized = betaNormalizeCanonical specialized
+            (found, abstracted) = abstractTarget 0 normalized
+        guard found
+        pure
+            (ScopedCheckedCore
+                (TySet : context)
+                TyProp
+                abstracted)
+  where
+    specialize term [] =
+        Just term
+    specialize (CForall binderType body)
+            (ScopedCheckedCore _ argumentType argument : rest)
+        | binderType == argumentType =
+            specialize
+                (instantiateCanonical argument body)
+                rest
+    specialize _term _arguments =
+        Nothing
 
-    andP left right =
-        notP (CImp left (notP right))
+    abstractTarget depth term
+        | term == shiftCanonical depth 0 target =
+            (True, CBound (fromIntegral depth))
+        | otherwise =
+            case term of
+                CBound index
+                    | index < fromIntegral depth ->
+                        (False, CBound index)
+                    | otherwise ->
+                        (False, CBound (index + 1))
+                CGlobal global ->
+                    (False, CGlobal global)
+                CIntrinsic intrinsic ->
+                    (False, CIntrinsic intrinsic)
+                COpaqueInteger integer ->
+                    (False, COpaqueInteger integer)
+                CApp function argument ->
+                    combine CApp
+                        (abstractTarget depth function)
+                        (abstractTarget depth argument)
+                CLam binderType body ->
+                    let (found, abstracted) =
+                            abstractTarget (depth + 1) body
+                    in (found, CLam binderType abstracted)
+                CFalsum ->
+                    (False, CFalsum)
+                CImp premise conclusion ->
+                    combine CImp
+                        (abstractTarget depth premise)
+                        (abstractTarget depth conclusion)
+                CEq operandType left right ->
+                    combine (CEq operandType)
+                        (abstractTarget depth left)
+                        (abstractTarget depth right)
+                CForall binderType body ->
+                    let (found, abstracted) =
+                            abstractTarget (depth + 1) body
+                    in (found, CForall binderType abstracted)
+
+    combine constructor (leftFound, left) (rightFound, right) =
+        (leftFound || rightFound, constructor left right)
+scopedCharacteristicDefinition _characteristic _target _arguments =
+    Nothing
 
-    notP proposition =
-        CImp proposition CFalsum
-scopedSetDefinition _expression =
+-- | Build the replacement graph of one checked set-valued local function.
+-- The ordered-pair constructor is an ordinary checked source object.
+scopedReplacementGraph
+    :: ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> Maybe
+        ( ScopedCheckedCore global
+        , ScopedCheckedCore global
+        , ScopedCheckedCore global
+        )
+scopedReplacementGraph
+        (ScopedCheckedCore context pairType pair)
+        domain@(ScopedCheckedCore domainContext TySet domainTerm)
+        (ScopedCheckedCore valueContext TySet value)
+    | pairType == TySet `TyArrow` (TySet `TyArrow` TySet)
+    , domainContext == context
+    , valueContext == TySet : context =
+        let pairValue =
+                CApp
+                    (CApp
+                        (shiftCanonical 1 0 pair)
+                        (CBound 0))
+                    value
+            function = CLam TySet pairValue
+            graph =
+                CApp
+                    (CApp (CIntrinsic Repl) domainTerm)
+                    function
+        in Just
+            ( ScopedCheckedCore context TySet graph
+            , domain
+            , ScopedCheckedCore
+                context
+                (TySet `TyArrow` TySet)
+                function
+            )
+scopedReplacementGraph _pair _domain _value =
     Nothing
 
+betaNormalizeCanonical
+    :: CanonicalTerm global
+    -> CanonicalTerm global
+betaNormalizeCanonical = \case
+    CApp function argument ->
+        case betaNormalizeCanonical function of
+            CLam _binderType body ->
+                betaNormalizeCanonical
+                    (instantiateCanonical
+                        (betaNormalizeCanonical argument)
+                        body)
+            normalizedFunction ->
+                CApp
+                    normalizedFunction
+                    (betaNormalizeCanonical argument)
+    CLam binderType body ->
+        CLam binderType (betaNormalizeCanonical body)
+    CImp premise conclusion ->
+        CImp
+            (betaNormalizeCanonical premise)
+            (betaNormalizeCanonical conclusion)
+    CEq operandType left right ->
+        CEq operandType
+            (betaNormalizeCanonical left)
+            (betaNormalizeCanonical right)
+    CForall binderType body ->
+        CForall binderType (betaNormalizeCanonical body)
+    term -> term
+
 -- | Combine two checked propositions under the same lexical context.
 implyScopedCore
     :: ScopedCheckedCore global
diff --git a/source/Checking/Declaration.hs b/source/Checking/Declaration.hs
index 53e3e02..800a100 100644
--- a/source/Checking/Declaration.hs
+++ b/source/Checking/Declaration.hs
@@ -17,6 +17,7 @@ module Checking.Declaration
     , importSealedModuleDriver
     , nextDeclarationSlotDriver
     , currentTheoryDriver
+    , currentFoundationAxiomDriver
     , resolveVisibleFactAliasDriver
     , resolveVisibleFactTargetsDriver
     , resolveVisibleGlobalDriver
@@ -848,6 +849,17 @@ currentTheoryDriver =
             (\(DriverState _resolver builder _prefix _validation) ->
                 logicalBuilderTheory builder))
 
+currentFoundationAxiomDriver
+    :: FoundationAxiomTag
+    -> ModuleDriver failure (FrozenCheckedCore Void)
+currentFoundationAxiomDriver tag =
+    ModuleDriver
+        (State.gets
+            (\(DriverState _resolver builder _prefix _validation) ->
+                foundationAxiomFrozen
+                    (logicalBuilderFoundation builder)
+                    tag))
+
 resolveVisibleFactAliasDriver
     :: SemanticName
     -> ModuleDriver failure
diff --git a/source/Checking/Exact.hs b/source/Checking/Exact.hs
index 6bb8bd6..d2f4418 100644
--- a/source/Checking/Exact.hs
+++ b/source/Checking/Exact.hs
@@ -17,6 +17,11 @@ module Checking.Exact
     , PreparedExactSetExpression
     , preparedExactSetExpressionCore
     , prepareExactSetExpression
+    , PreparedExactLocalFunctionGraph
+    , preparedExactLocalFunctionGraphCore
+    , preparedExactLocalFunctionGraphDomain
+    , preparedExactLocalFunctionGraphMap
+    , prepareExactLocalFunctionGraph
     , PreparedExactClaimEnvelope
     , preparedExactClaimTarget
     , preparedExactClaimVariables
@@ -151,6 +156,35 @@ preparedExactSetExpressionCore
 preparedExactSetExpressionCore (PreparedExactSetExpression expression) =
     expression
 
+-- | A checked replacement graph and the two checked arguments used to
+-- specialize its foundation characteristic. This is transient proof
+-- preparation data, not a declaration or durable object.
+data PreparedExactLocalFunctionGraph = PreparedExactLocalFunctionGraph
+    !(ScopedCheckedCore ObjectId)
+    !(ScopedCheckedCore ObjectId)
+    !(ScopedCheckedCore ObjectId)
+
+preparedExactLocalFunctionGraphCore
+    :: PreparedExactLocalFunctionGraph
+    -> ScopedCheckedCore ObjectId
+preparedExactLocalFunctionGraphCore
+        (PreparedExactLocalFunctionGraph graph _domain _function) =
+    graph
+
+preparedExactLocalFunctionGraphDomain
+    :: PreparedExactLocalFunctionGraph
+    -> ScopedCheckedCore ObjectId
+preparedExactLocalFunctionGraphDomain
+        (PreparedExactLocalFunctionGraph _graph domain _function) =
+    domain
+
+preparedExactLocalFunctionGraphMap
+    :: PreparedExactLocalFunctionGraph
+    -> ScopedCheckedCore ObjectId
+preparedExactLocalFunctionGraphMap
+        (PreparedExactLocalFunctionGraph _graph _domain function) =
+    function
+
 -- | One authoritative closed proposition prepared from a top-level claim
 -- header and conclusion. The remaining fields are transient opening data for
 -- the proof compiler.
@@ -434,6 +468,64 @@ prepareExactSetExpression context expression =
                     (scopedCoreType checked)))
         pure (PreparedExactSetExpression checked)
 
+prepareExactLocalFunctionGraph
+    :: Location
+    -> ExactBinderContext
+    -> ExactBinderContext
+    -> Raw.Expr
+    -> Raw.Expr
+    -> Declaration.ModuleDriver failure
+        (Either ExactCompileError PreparedExactLocalFunctionGraph)
+prepareExactLocalFunctionGraph
+        location context argumentContext domainExpression valueExpression =
+    Except.runExceptT do
+        domain <-
+            preparedExactSetExpressionCore
+                <$> ( Except.lift
+                        (prepareExactSetExpression context domainExpression)
+                        >>= Except.liftEither
+                    )
+        value <-
+            preparedExactSetExpressionCore
+                <$> ( Except.lift
+                        (prepareExactSetExpression
+                            argumentContext valueExpression)
+                        >>= Except.liftEither
+                    )
+        pair <- prepareOrderedPair
+        case scopedReplacementGraph pair domain value of
+            Just (graph, checkedDomain, function) ->
+                pure
+                    (PreparedExactLocalFunctionGraph
+                        graph checkedDomain function)
+            Nothing ->
+                impossible
+                    "checked local-function components did not form a replacement graph"
+  where
+    prepareOrderedPair = do
+        let initialElaboration =
+                ElaborationState
+                    (binderIndices context)
+                    mempty
+            key =
+                SemanticExpressionFunction
+                    (Raw.mixfixPattern Raw.PairSymbol)
+            expected = TySet `TyArrow` (TySet `TyArrow` TySet)
+        ((term, actual), finalElaboration) <-
+            State.runStateT
+                (applyResolvedTyped location key [])
+                initialElaboration
+        unless (actual == expected)
+            (Except.throwError
+                (ExactObjectTypeMismatch location expected actual))
+        either
+            (Except.throwError . ExactCoreCheckFailed location)
+            pure
+            (checkScopedCanonicalCore
+                (`Map.lookup` elaborationGlobals finalElaboration)
+                (binderTypes context)
+                term)
+
 prepareExactClaimEnvelope
     :: [Raw.Asm]
     -> Raw.Stmt
diff --git a/source/Checking/Exact/Proof.hs b/source/Checking/Exact/Proof.hs
index b66ebfe..5a7958e 100644
--- a/source/Checking/Exact/Proof.hs
+++ b/source/Checking/Exact/Proof.hs
@@ -63,6 +63,8 @@ data ExactProofError
     | ExactProofExpectedImplicationGoal !Location
     | ExactProofGoalStatementMismatch !Location
     | ExactProofContradictionGoalMismatch !Location
+    | ExactProofLocalFunctionBinderMismatch !Location
+    | ExactProofLocalFunctionNameConflict !Location
     | ExactProofUnknownReference !Location !Raw.Marker
     | ExactProofElaborationFailed !Exact.ExactCompileError
     | ExactProofObligationPreparationFailed
@@ -91,6 +93,8 @@ exactProofErrorLocation = \case
     ExactProofExpectedImplicationGoal location -> location
     ExactProofGoalStatementMismatch location -> location
     ExactProofContradictionGoalMismatch location -> location
+    ExactProofLocalFunctionBinderMismatch location -> location
+    ExactProofLocalFunctionNameConflict location -> location
     ExactProofUnknownReference location _marker -> location
     ExactProofElaborationFailed failure ->
         Exact.exactCompileErrorLocation failure
@@ -131,6 +135,10 @@ renderExactProofError = \case
         at location <> "the proof step does not match the current goal"
     ExactProofContradictionGoalMismatch location ->
         at location <> "contradiction requires falsum as the current goal"
+    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 ->
@@ -210,6 +218,11 @@ data PreparedProof
         !(ScopedCheckedCore ObjectId)
         !(ScopedCheckedCore ObjectId)
         !PreparedProof
+    | PreparedDefineFunction
+        !Exact.ExactLocalId
+        !(ScopedCheckedCore ObjectId)
+        !(ScopedCheckedCore ObjectId)
+        !PreparedProof
     | PreparedContradiction !PreparedDischarge
 
 data PreparedExactProof = PreparedExactProof
@@ -639,12 +652,16 @@ prepareProof fallback context locals inductionAntecedents goal = \case
                 (Exact.extendExactBinderContext
                     ((identity, variable) :| [])
                     context)
+        separationCharacteristic <-
+            liftDriver
+                (Declaration.currentFoundationAxiomDriver
+                    SeparationCharacteristic)
         definition <-
             maybe
                 (impossible
                     "an exact set expression did not form a local definition")
                 pure
-                (scopedSetDefinition body)
+                (scopedSetDefinition separationCharacteristic body)
         local <-
             allocateLocal ExactLocalDefinition context' definition
         PreparedDefine identity body definition
@@ -655,6 +672,65 @@ prepareProof fallback context locals inductionAntecedents goal = \case
                 Nothing
                 (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.currentFoundationAxiomDriver
+                    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])
+                Nothing
+                (weakenCheckedScopedCore TySet goal)
+                continuation
     Raw.Contradiction location justification -> do
         unless
             ( scopedCoreType goal == TyProp
@@ -978,6 +1054,8 @@ preparedProofFirstOmission = \case
             <|> preparedProofFirstOmission continuation
     PreparedDefine _identity _body _definition continuation ->
         preparedProofFirstOmission continuation
+    PreparedDefineFunction _identity _graph _definition continuation ->
+        preparedProofFirstOmission continuation
     PreparedContradiction{} -> Nothing
 
 executePreparedProof
@@ -1007,6 +1085,8 @@ executePreparedProof = \case
         executePreparedProof continuation
     PreparedDefine _identity _body _definition continuation ->
         executePreparedProof continuation
+    PreparedDefineFunction _identity _graph _definition continuation ->
+        executePreparedProof continuation
     PreparedContradiction discharge ->
         executeDischarge discharge
 
@@ -1077,6 +1157,12 @@ putPreparedProof = \case
     PreparedContradiction discharge -> do
         putCacheTag 0x0a
         putPreparedDischarge discharge
+    PreparedDefineFunction identity graph definition continuation -> do
+        putCacheTag 0x0b
+        putCacheNatural (Exact.exactLocalIdValue identity)
+        putScopedTerm graph
+        putScopedProposition definition
+        putPreparedProof continuation
 
 putPreparedDischarge :: PreparedDischarge -> CachePut
 putPreparedDischarge
diff --git a/source/Felix/Cache/Codec.hs b/source/Felix/Cache/Codec.hs
index 0bfa975..e1fb35d 100644
--- a/source/Felix/Cache/Codec.hs
+++ b/source/Felix/Cache/Codec.hs
@@ -75,7 +75,7 @@ newtype CacheEpoch = CacheEpoch Word32
 
 currentCacheEpoch :: CacheEpoch
 currentCacheEpoch =
-    CacheEpoch 19
+    CacheEpoch 20
 
 cacheEpochValue :: CacheEpoch -> Word32
 cacheEpochValue (CacheEpoch value) =
diff --git a/source/Felix/Migration.hs b/source/Felix/Migration.hs
index 0fcb05d..741eb2f 100644
--- a/source/Felix/Migration.hs
+++ b/source/Felix/Migration.hs
@@ -200,6 +200,8 @@ typedMigrationModules =
         , migrationProjectModule "test/phase5/exact-proofs.tex"
         , migrationProjectModule "test/phase5/exact-local-definition.tex"
         , migrationProjectModule "test/phase5/exact-local-definition-failure.tex"
+        , migrationProjectModule "test/phase5/exact-local-function.tex"
+        , migrationProjectModule "test/phase5/exact-local-function-failure.tex"
         , migrationProjectModule "test/phase5/exact-contradiction.tex"
         , migrationProjectModule "test/phase5/exact-contradiction-goal.tex"
         , migrationProjectModule "test/phase5/exact-relation-expression.tex"
diff --git a/source/Test/Unit/Core.hs b/source/Test/Unit/Core.hs
index fd817c6..e1ba10d 100644
--- a/source/Test/Unit/Core.hs
+++ b/source/Test/Unit/Core.hs
@@ -15,16 +15,20 @@ import Test.Tasty.HUnit hiding (assert)
 import Test.Tasty.Hedgehog (testPropertyNamed)
 
 
-data TestGlobal = TestGlobal
+data TestGlobal
+    = TestGlobal
+    | TestPairGlobal
     deriving (Show, Eq, Ord)
 
 instance NFData TestGlobal where
-    rnf TestGlobal =
+    rnf _global =
         ()
 
 testGlobalType :: TestGlobal -> Maybe CoreType
 testGlobalType TestGlobal =
     Just TySet
+testGlobalType TestPairGlobal =
+    Just (TySet `TyArrow` (TySet `TyArrow` TySet))
 
 unitTests :: TestTree
 unitTests =
@@ -51,6 +55,9 @@ unitTests =
             "specializes the checked separation characteristic"
             specializesCheckedSeparationCharacteristic
         , testCase
+            "specializes the checked replacement characteristic"
+            specializesCheckedReplacementCharacteristic
+        , testCase
             "thaws checked closed terms without changing them"
             thawsCheckedClosedTerms
         , testPropertyNamed
@@ -325,7 +332,11 @@ specializesCheckedSeparationCharacteristic = do
         maybe
             (assertFailure "separation did not form a set definition")
             pure
-            (scopedSetDefinition body)
+            (scopedSetDefinition
+                (Foundation.foundationAxiomFrozen
+                    foundation
+                    Foundation.SeparationCharacteristic)
+                body)
     let generated =
             instantiateCanonical
                 separation
@@ -343,36 +354,90 @@ specializesCheckedSeparationCharacteristic = do
         "local characteristic is the checked rule specialization"
         expected
         generated
+
+specializesCheckedReplacementCharacteristic :: Assertion
+specializesCheckedReplacementCharacteristic = do
+    foundation <-
+        either
+            (assertFailure . show)
+            pure
+            Foundation.checkedFoundation
+    pair <- checked [] (CGlobal TestPairGlobal)
+    domain <- checked [] (CIntrinsic Empty)
+    value <- checked [TySet] (CBound 0)
+    (graph, checkedDomain, function) <-
+        maybe
+            (assertFailure "checked values did not form a replacement graph")
+            pure
+            (scopedReplacementGraph pair domain value)
+    definition <-
+        maybe
+            (assertFailure "replacement graph did not form a definition")
+            pure
+            (scopedCharacteristicDefinition
+                (Foundation.foundationAxiomFrozen
+                    foundation
+                    Foundation.ReplacementCharacteristic)
+                graph
+                (checkedDomain :| [function]))
+    let generated =
+            instantiateCanonical
+                (scopedCoreTerm graph)
+                (scopedCoreTerm definition)
+        expected =
+            betaNormalize
+                (specializeForall (scopedCoreTerm function)
+                (specializeForall (scopedCoreTerm checkedDomain)
+                    (mapCanonicalGlobals absurd
+                        (frozenCoreTerm
+                            (Foundation.foundationAxiomFrozen
+                                foundation
+                                Foundation.ReplacementCharacteristic)))))
+    assertEqual
+        "local graph characteristic is the checked rule specialization"
+        expected
+        generated
   where
-    specializeForall argument = \case
-        CForall _binderType body ->
-            instantiateCanonical argument body
-        _ ->
-            error "the checked separation characteristic lost a binder"
+    checked context term =
+        either
+            (assertFailure . show)
+            pure
+            (checkScopedCanonicalCore testGlobalType context term)
+
+specializeForall
+    :: CanonicalTerm global
+    -> CanonicalTerm global
+    -> CanonicalTerm global
+specializeForall argument = \case
+    CForall _binderType body ->
+        instantiateCanonical argument body
+    _ ->
+        error "the checked characteristic lost a binder"
 
-    betaNormalize = \case
-        CApp function argument ->
-            case betaNormalize function of
-                CLam _binderType body ->
-                    betaNormalize
-                        (instantiateCanonical
-                            (betaNormalize argument)
-                            body)
-                normalizedFunction ->
-                    CApp normalizedFunction (betaNormalize argument)
-        CLam binderType body ->
-            CLam binderType (betaNormalize body)
-        CImp premise conclusion ->
-            CImp
-                (betaNormalize premise)
-                (betaNormalize conclusion)
-        CEq operandType left right ->
-            CEq operandType
-                (betaNormalize left)
-                (betaNormalize right)
-        CForall binderType body ->
-            CForall binderType (betaNormalize body)
-        term -> term
+betaNormalize :: CanonicalTerm global -> CanonicalTerm global
+betaNormalize = \case
+    CApp function argument ->
+        case betaNormalize function of
+            CLam _binderType body ->
+                betaNormalize
+                    (instantiateCanonical
+                        (betaNormalize argument)
+                        body)
+            normalizedFunction ->
+                CApp normalizedFunction (betaNormalize argument)
+    CLam binderType body ->
+        CLam binderType (betaNormalize body)
+    CImp premise conclusion ->
+        CImp
+            (betaNormalize premise)
+            (betaNormalize conclusion)
+    CEq operandType left right ->
+        CEq operandType
+            (betaNormalize left)
+            (betaNormalize right)
+    CForall binderType body ->
+        CForall binderType (betaNormalize body)
+    term -> term
 
 thawsCheckedClosedTerms :: Assertion
 thawsCheckedClosedTerms = do
diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index 1cf62e5..296d7c2 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -98,6 +98,8 @@ unitTests =
             compilesExactOrdinaryProofs
         , testCase "compiles and reuses proof-local set definitions"
             compilesAndReusesProofLocalSetDefinitions
+        , testCase "compiles and reuses proof-local function graphs"
+            compilesAndReusesProofLocalFunctionGraphs
         , testCase "confines terminal exact contradiction"
             confinesTerminalExactContradiction
         , testCase "compiles exact separation comprehensions"
@@ -2307,6 +2309,209 @@ compilesAndReusesProofLocalSetDefinitions =
             (Core.CImp left (Core.CImp right Core.CFalsum))
             Core.CFalsum
 
+compilesAndReusesProofLocalFunctionGraphs :: Assertion
+compilesAndReusesProofLocalFunctionGraphs =
+    Temp.withSystemTempDirectory "felix-exact-local-function" \root -> do
+        let relative = "test/phase5/exact-local-function.tex"
+            failedRelative =
+                "test/phase5/exact-local-function-failure.tex"
+            executable = root Posix.</> "vampire"
+            storePath = root Posix.</> "store.sqlite"
+        writeAcceptedFixtureVampire executable
+        foundation <- expectRight Foundation.checkedFoundation
+        bootstrap <-
+            expectRight
+                =<< Module.buildBootstrapPreludeFixture
+                    foundation unusedResolver
+        mounts <- exactFixtureMounts =<< getCurrentDirectory
+        workspace <- parseExactWorkspace bootstrap mounts relative
+        observations <- newIORef []
+        let resolver = Declaration.vampireResolver \prepared -> do
+                let problem =
+                        Provers.preparedTypedProverLogicalProblem prepared
+                    premises =
+                        [ ( Backend.typedProblemRoute problem
+                          , fmap snd
+                                (Vector.toList
+                                    (Backend.supportedPropositionSupport
+                                        proposition))
+                          , Backend.supportedPropositionTerm proposition
+                          )
+                        | premise <-
+                            Vector.toList
+                                (Backend.typedProblemLocalPremises problem)
+                        , let proposition =
+                                Backend.typedLocalPremiseProposition premise
+                        ]
+                modifyIORef' observations (<> premises)
+                runNoLoggingT
+                    (Provers.runPreparedTypedProver
+                        (Provers.vampire
+                            executable
+                            Provers.defaultTimeLimit
+                            Provers.defaultMemoryLimit)
+                        prepared)
+        freshModules <-
+            compileParsedWorkspaceWithValidation
+                foundation bootstrap resolver
+                Declaration.FreshValidation workspace
+        allObserved <- readIORef observations
+        let observed =
+                [ (route, proposition)
+                | (route, support, proposition) <- allObserved
+                , support == [Core.TySet, Core.TySet]
+                , isJust (localFunctionPair proposition)
+                ]
+        assertBool
+            ("the local graph characteristic reaches a discharge: "
+                <> show allObserved)
+            (not (null observed))
+        for_ observed \(route, proposition) -> do
+            assertEqual "local function characteristic stays on FOF"
+                Backend.RouteFof route
+            assertExactLocalFunctionCharacteristic proposition
+        freshRoot <- sole "fresh local-function root"
+            (take 1 (reverse freshModules))
+        rootBatch <- sole "local function publishes only its theorem"
+            (drop 1
+                (Declaration.pendingModulePrefixBatches
+                    (Module.sealedTypedModulePrefix freshRoot)))
+        assertEqual "local function publishes no object"
+            [] (Declaration.committedBatchObjects rootBatch)
+        assertEqual "local function publishes only its theorem"
+            1
+            (length
+                (Declaration.committedBatchPropositions rootBatch))
+        assertEqual "local function publishes no semantic binding"
+            []
+            (Semantic.semanticEnvironmentBindings
+                (Semantic.declarationDeltaEnvironment
+                    (Declaration.committedBatchDelta rootBatch)))
+        rootFact <- sole "local-function theorem"
+            (Semantic.declarationDeltaFacts
+                (Declaration.committedBatchDelta rootBatch))
+        assertEqual "local-function theorem remains clean"
+            Authority.cleanAuthoritySafety
+            (Authority.factAuthoritySafety
+                (Semantic.semanticFactAuthority rootFact))
+
+        bracket
+            (snd <$> (Store.openStore storePath
+                (Identity.theoryId foundation) >>= expectRight))
+            Store.closeStore
+            \store -> do
+                traverse_
+                    (expectRightIO
+                        . Store.writePendingModulePrefix store
+                        . Module.sealedTypedModulePrefix)
+                    freshModules
+                let validation =
+                        Declaration.WarmValidation
+                            (Declaration.validationLookup
+                                (expectRightIO
+                                    . Store.loadProofValidation store)
+                                (expectRightIO
+                                    . Store.loadDeclarationValidation store))
+                warmRuns <- newIORef (0 :: Int)
+                warmModules <-
+                    compileParsedWorkspaceWithValidation
+                        foundation bootstrap
+                        (countingAcceptedResolver executable warmRuns)
+                        validation workspace
+                assertEqual "warm local-function graph skips Vampire"
+                    0 =<< readIORef warmRuns
+                warmRoot <- sole "warm local-function root"
+                    (take 1 (reverse warmModules))
+                assertEqual "warm local-function semantic interface"
+                    (Module.sealedTypedModuleSemantic freshRoot)
+                    (Module.sealedTypedModuleSemantic warmRoot)
+                assertEqual "warm local-function prefix"
+                    (Declaration.pendingModulePrefixCurrent
+                        (Module.sealedTypedModulePrefix freshRoot))
+                    (Declaration.pendingModulePrefixCurrent
+                        (Module.sealedTypedModulePrefix warmRoot))
+
+        failedWorkspace <-
+            parseExactWorkspace bootstrap mounts failedRelative
+        failedInput <- expectRight
+            (Module.typedModuleInput
+                foundation
+                (Module.bootstrapPreludeReadiness bootstrap)
+                unusedResolver
+                Declaration.FreshValidation
+                (Parse.parsedWorkspaceRootModule failedWorkspace)
+                [])
+        Module.runTypedModule failedInput >>= \case
+            Module.TypedModuleFailed
+                    (Module.TypedActionFailed
+                        (Module.TypedExactProofFailed
+                            (ExactProof.ExactProofElaborationFailed
+                                (Exact.ExactFreeVariable location
+                                    (Raw.NamedVar "f")))))
+                    prefix -> do
+                assertEqual "self-reference rejection line"
+                    6 (locLine location)
+                assertBool "failed local function publishes no theorem"
+                    (null
+                        (Declaration.pendingModulePrefixBatches prefix))
+            Module.TypedModuleSucceeded{} ->
+                assertFailure "self-referential local function was accepted"
+            Module.TypedModuleOpenFailed failure ->
+                assertFailure
+                    ("local-function failure fixture did not open: "
+                        <> show failure)
+            Module.TypedModuleFailed failure _prefix ->
+                assertFailure
+                    ("unexpected local-function failure: "
+                        <> show failure)
+  where
+    assertExactLocalFunctionCharacteristic proposition = do
+        pair <-
+            maybe
+                (assertFailure "local function characteristic has wrong shape")
+                pure
+                (localFunctionPair proposition)
+        assertEqual "local function uses the exact replacement characteristic"
+            (expectedLocalFunctionCharacteristic pair)
+            proposition
+
+    localFunctionPair proposition =
+        case Set.toList (Core.canonicalTermGlobals proposition) of
+            [pair]
+                | proposition == expectedLocalFunctionCharacteristic pair ->
+                    Just pair
+            _ ->
+                Nothing
+
+    expectedLocalFunctionCharacteristic pair =
+        Core.CForall Core.TySet
+            (Core.CEq Core.TyProp
+                (member (Core.CBound 0) (Core.CBound 1))
+                (existsP
+                    (andP
+                        (member (Core.CBound 0) (Core.CBound 3))
+                        (Core.CEq Core.TySet
+                            (Core.CBound 1)
+                            (Core.CApp
+                                (Core.CApp
+                                    (Core.CGlobal pair)
+                                    (Core.CBound 0))
+                                (Core.CBound 0))))))
+
+    member element set =
+        Core.CApp
+            (Core.CApp (Core.CIntrinsic Core.Member) element)
+            set
+
+    andP left right =
+        notP (Core.CImp left (notP right))
+
+    existsP proposition =
+        notP (Core.CForall Core.TySet (notP proposition))
+
+    notP proposition =
+        Core.CImp proposition Core.CFalsum
+
 confinesTerminalExactContradiction :: Assertion
 confinesTerminalExactContradiction =
     Temp.withSystemTempDirectory "felix-exact-contradiction" \directory -> do
diff --git a/test/phase5/exact-local-function-failure.tex b/test/phase5/exact-local-function-failure.tex
new file mode 100644
index 0000000..f1afc9b
--- /dev/null
+++ b/test/phase5/exact-local-function-failure.tex
@@ -0,0 +1,8 @@
+\begin{proposition}\label{phase5_local_function_failure}
+    For all $A$ we have $A = A$.
+\end{proposition}
+\begin{proof}
+    Fix $A$.
+    Let $f(x) = f$ for $x\in A$.
+    Follows by assumption.
+\end{proof}
diff --git a/test/phase5/exact-local-function.tex b/test/phase5/exact-local-function.tex
new file mode 100644
index 0000000..03e6ce4
--- /dev/null
+++ b/test/phase5/exact-local-function.tex
@@ -0,0 +1,18 @@
+\begin{signature}\label{phase5_local_pair}
+    $(x,y)$ is a set.
+\end{signature}
+
+\begin{proposition}\label{phase5_local_function}
+    For all $A$ we have $A = A$.
+\end{proposition}
+\begin{proof}
+    Fix $A$.
+    Let $f(x) = x$ for $x\in A$.
+    Show for all $y$ we have if $y\in A$, then $(y,y)\in f$.
+    \begin{subproof}
+        Fix $y$.
+        Assume $y\in A$.
+        Follows by assumption.
+    \end{subproof}
+    Follows by assumption.
+\end{proof}