Migrate to `Felix` namespaceHEADhotg

1 files changed, 1023 insertions, 0 deletions

diff --git a/source/Felix/Checking/Identity.hs b/source/Felix/Checking/Identity.hs
new file mode 100644
index 0000000..67347a3
--- /dev/null
+++ b/source/Felix/Checking/Identity.hs
@@ -0,0 +1,1023 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Content-addressed identities for checked mathematical content.
+module Felix.Checking.Identity
+    ( TheoryId
+    , theoryId
+    , theoryIdDigest
+    , encodeFoundationManifest
+    , foundationManifestTags
+    , encodeKernelRuleTag
+    , ObjectFamily(..)
+    , ObjectId
+    , objectId
+    , objectIdFamily
+    , objectIdDigest
+    , encodeObjectId
+    , OpaqueDeclarationSeed
+    , opaqueDeclarationSeed
+    , opaqueDeclarationSeedDigest
+    , ObjectContent(..)
+    , objectContentTheory
+    , objectContentType
+    , intrinsicObjectId
+    , transparentObjectId
+    , opaqueObjectId
+    , AssertedObject
+    , assertedObject
+    , assertedObjectId
+    , assertedObjectContent
+    , CheckedObjectClosure
+    , checkedObjectClosureTheory
+    , checkedObjectIds
+    , lookupCheckedObjectType
+    , lookupCheckedObjectContent
+    , validateObjectClosure
+    , extendObjectClosure
+    , ObjectValidationError(..)
+    , PropositionId
+    , propositionIdDigest
+    , CheckedPropositionContent
+    , checkedPropositionId
+    , checkedPropositionTerm
+    , validatePropositionContent
+    , validateAssertedPropositionContent
+    , propositionIdOf
+    , PropositionValidationError(..)
+    , TheoremRef
+    , theoremRef
+    , theoremRefTheory
+    , theoremRefProposition
+    , encodeTheoremRef
+    , TheoremId
+    , theoremId
+    , theoremIdDigest
+    , putTheoryIdCache
+    , getTheoryIdCache
+    , putObjectIdCache
+    , getObjectIdCache
+    , putObjectContentCache
+    , getObjectContentCache
+    , putPropositionIdCache
+    , getPropositionIdCache
+    , putTheoremRefCache
+    , getTheoremRefCache
+    ) where
+
+import Base
+import Felix.Checking.Core
+import Felix.Checking.Foundation
+import Felix.Cache.Codec
+import Felix.Math.Codec
+import Felix.Module
+
+import Control.DeepSeq (NFData)
+import Control.Monad.State.Strict
+import Data.Bifunctor (first)
+import Data.ByteString (ByteString)
+import Data.ByteString qualified as ByteString
+import Data.List qualified as List
+import Data.Map.Strict qualified as Map
+import Data.Set qualified as Set
+import Data.Word (Word8)
+
+
+newtype TheoryId =
+    TheoryId MathematicalDigest
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+theoryId :: CheckedFoundation -> TheoryId
+theoryId foundation =
+    TheoryId
+        (codecInvariant
+            (hashCanonicalFields
+                "felix-theory"
+                [encodeFoundationManifest foundation]))
+
+theoryIdDigest :: TheoryId -> MathematicalDigest
+theoryIdDigest (TheoryId digest) =
+    digest
+
+-- | Canonical ordered intrinsic/rule/axiom manifest. Backend classification is
+-- intentionally absent.
+encodeFoundationManifest :: CheckedFoundation -> ByteString
+encodeFoundationManifest foundation =
+    codecInvariant
+        (encodeSequence
+            [ codecInvariant (encodeSequence intrinsicRows)
+            , codecInvariant (encodeSequence ruleRows)
+            , codecInvariant (encodeSequence axiomRows)
+            ])
+  where
+    (intrinsicTags, ruleTags, axiomTags) =
+        foundationManifestTags
+
+    intrinsicRows =
+        [ encodeCoreIntrinsicTag tag
+            <> encodeFrame (encodeCoreType (coreIntrinsicType tag))
+        | tag <- intrinsicTags
+        ]
+
+    ruleRows =
+        [ encodeKernelRuleTag tag
+            <> encodeFrame
+                (codecInvariant
+                    (encodeSequence
+                        (encodeCoreType <$> inputTypes)))
+            <> encodeFrame (encodeNatural binderCount)
+        | tag <- ruleTags
+        , let KernelRuleSignature inputTypes binderCount =
+                foundationRuleSignature foundation tag
+        ]
+
+    axiomRows =
+        [ encodeFoundationAxiomTag tag
+            <> encodeFrame
+                (encodeCanonicalTerm
+                    absurd
+                    (frozenCoreTerm
+                        (foundationAxiomFrozen foundation tag)))
+        | tag <- axiomTags
+        ]
+
+-- | Exhaustive foundation inventories in their stable encoded-tag order.
+foundationManifestTags
+    :: ( [CoreIntrinsicTag]
+       , [KernelRuleTag]
+       , [FoundationAxiomTag]
+       )
+foundationManifestTags =
+    ( stableTagOrder
+        "core intrinsic"
+        encodeCoreIntrinsicTag
+        allCoreIntrinsicTags
+    , stableTagOrder
+        "kernel rule"
+        encodeKernelRuleTag
+        allKernelRuleTags
+    , stableTagOrder
+        "foundation axiom"
+        encodeFoundationAxiomTag
+        allFoundationAxiomTags
+    )
+
+
+data ObjectFamily
+    = IntrinsicObject
+    | TransparentObject
+    | OpaqueObject
+    deriving stock (Show, Eq, Ord, Enum, Bounded, Generic)
+    deriving anyclass (NFData)
+
+data ObjectId = ObjectId
+    !ObjectFamily
+    !MathematicalDigest
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+objectId
+    :: ObjectFamily
+    -> MathematicalDigest
+    -> ObjectId
+objectId =
+    ObjectId
+
+objectIdFamily :: ObjectId -> ObjectFamily
+objectIdFamily (ObjectId family _digest) =
+    family
+
+objectIdDigest :: ObjectId -> MathematicalDigest
+objectIdDigest (ObjectId _family digest) =
+    digest
+
+encodeObjectId :: ObjectId -> ByteString
+encodeObjectId (ObjectId family digest) =
+    ByteString.singleton (objectFamilyTag family)
+        <> mathematicalDigestBytes digest
+
+
+newtype OpaqueDeclarationSeed =
+    OpaqueDeclarationSeed MathematicalDigest
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+opaqueDeclarationSeed
+    :: ModuleName
+    -> LocalDeclarationOrdinal
+    -> DeclarationFamilyTag
+    -> GeneratedObjectSlot
+    -> OpaqueDeclarationSeed
+opaqueDeclarationSeed
+        owner
+        declarationOrdinal
+        family
+        generatedSlot =
+    OpaqueDeclarationSeed
+        (codecInvariant
+            (hashCanonicalFields
+                "felix-opaque-declaration-v1"
+                [ encodeModuleName owner
+                , encodeNatural
+                    (localDeclarationOrdinalValue
+                        declarationOrdinal)
+                , encodeDeclarationFamilyTag family
+                , encodeNatural
+                    (generatedObjectSlotValue
+                        generatedSlot)
+                ]))
+
+opaqueDeclarationSeedDigest
+    :: OpaqueDeclarationSeed
+    -> MathematicalDigest
+opaqueDeclarationSeedDigest
+        (OpaqueDeclarationSeed digest) =
+    digest
+
+
+data ObjectContent
+    = IntrinsicObjectContent
+        !TheoryId
+        !CoreIntrinsicTag
+        !CoreType
+    | TransparentObjectContent
+        !TheoryId
+        !CoreType
+        !(CanonicalTerm ObjectId)
+    | OpaqueObjectContent
+        !TheoryId
+        !OpaqueDeclarationSeed
+        !CoreType
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+objectContentTheory :: ObjectContent -> TheoryId
+objectContentTheory = \case
+    IntrinsicObjectContent identity _tag _coreType ->
+        identity
+    TransparentObjectContent identity _coreType _body ->
+        identity
+    OpaqueObjectContent identity _seed _coreType ->
+        identity
+
+objectContentType :: ObjectContent -> CoreType
+objectContentType = \case
+    IntrinsicObjectContent _identity _tag coreType ->
+        coreType
+    TransparentObjectContent _identity coreType _body ->
+        coreType
+    OpaqueObjectContent _identity _seed coreType ->
+        coreType
+
+intrinsicObjectId
+    :: TheoryId
+    -> CoreIntrinsicTag
+    -> CoreType
+    -> ObjectId
+intrinsicObjectId identity tag coreType =
+    ObjectId
+        IntrinsicObject
+        (codecInvariant
+            (hashCanonicalFields
+                "felix-intrinsic-object-v1"
+                [ mathematicalDigestBytes
+                    (theoryIdDigest identity)
+                , encodeCoreIntrinsicTag tag
+                , encodeCoreType coreType
+                ]))
+
+transparentObjectId
+    :: TheoryId
+    -> CoreType
+    -> CanonicalTerm ObjectId
+    -> ObjectId
+transparentObjectId identity coreType body =
+    ObjectId
+        TransparentObject
+        (codecInvariant
+            (hashCanonicalFields
+                "felix-transparent-object-v1"
+                [ mathematicalDigestBytes
+                    (theoryIdDigest identity)
+                , encodeCoreType coreType
+                , encodeCanonicalTerm encodeObjectId body
+                ]))
+
+opaqueObjectId
+    :: TheoryId
+    -> OpaqueDeclarationSeed
+    -> CoreType
+    -> ObjectId
+opaqueObjectId identity seed coreType =
+    ObjectId
+        OpaqueObject
+        (codecInvariant
+            (hashCanonicalFields
+                "felix-opaque-object-v1"
+                [ mathematicalDigestBytes
+                    (theoryIdDigest identity)
+                , mathematicalDigestBytes
+                    (opaqueDeclarationSeedDigest seed)
+                , encodeCoreType coreType
+                ]))
+
+
+data AssertedObject = AssertedObject
+    !ObjectId
+    !ObjectContent
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+assertedObject :: ObjectId -> ObjectContent -> AssertedObject
+assertedObject =
+    AssertedObject
+
+assertedObjectId :: AssertedObject -> ObjectId
+assertedObjectId (AssertedObject identity _content) =
+    identity
+
+assertedObjectContent :: AssertedObject -> ObjectContent
+assertedObjectContent (AssertedObject _identity content) =
+    content
+
+data CheckedObject = CheckedObject
+    !ObjectContent
+    !CoreType
+
+data CheckedObjectClosure = CheckedObjectClosure
+    !TheoryId
+    !(Map ObjectId CheckedObject)
+
+checkedObjectClosureTheory :: CheckedObjectClosure -> TheoryId
+checkedObjectClosureTheory (CheckedObjectClosure identity _objects) =
+    identity
+
+checkedObjectIds :: CheckedObjectClosure -> Set ObjectId
+checkedObjectIds (CheckedObjectClosure _identity objects) =
+    Map.keysSet objects
+
+lookupCheckedObjectType
+    :: ObjectId
+    -> CheckedObjectClosure
+    -> Maybe CoreType
+lookupCheckedObjectType identity
+        (CheckedObjectClosure _theory objects) =
+    checkedObjectType
+        <$> Map.lookup identity objects
+
+lookupCheckedObjectContent
+    :: ObjectId
+    -> CheckedObjectClosure
+    -> Maybe ObjectContent
+lookupCheckedObjectContent identity
+        (CheckedObjectClosure _theory objects) =
+    checkedObjectContent
+        <$> Map.lookup identity objects
+
+checkedObjectType :: CheckedObject -> CoreType
+checkedObjectType (CheckedObject _content coreType) =
+    coreType
+
+checkedObjectContent :: CheckedObject -> ObjectContent
+checkedObjectContent (CheckedObject content _coreType) =
+    content
+
+
+data ObjectValidationError
+    = DuplicateAssertedObjectId !ObjectId
+    | ObjectContentTheoryMismatch
+        !ObjectId
+        !TheoryId
+        !TheoryId
+    | ObjectContentFamilyMismatch
+        !ObjectId
+        !ObjectFamily
+        !ObjectFamily
+    | IntrinsicObjectTypeMismatch
+        !ObjectId
+        !CoreIntrinsicTag
+        !CoreType
+        !CoreType
+    | TransparentObjectReferenceMissing
+        !ObjectId
+        !ObjectId
+    | TransparentObjectCycle !(NonEmpty ObjectId)
+    | TransparentObjectCoreCheckError
+        !ObjectId
+        !CoreCheckError
+    | TransparentObjectTypeMismatch
+        !ObjectId
+        !CoreType
+        !CoreType
+    | ObjectIdPayloadMismatch
+        !ObjectId
+        !ObjectId
+    deriving stock (Show, Eq)
+
+data ObjectValidationState = ObjectValidationState
+    { validationStack :: ![ObjectId]
+    , validatedObjects :: !(Map ObjectId CheckedObject)
+    }
+
+validateObjectClosure
+    :: TheoryId
+    -> [AssertedObject]
+    -> Either ObjectValidationError CheckedObjectClosure
+validateObjectClosure expectedTheory asserted = do
+    inventory <- buildObjectInventory asserted
+    finalState <-
+        execStateT
+            (traverse_ (validateOneObject expectedTheory inventory)
+                (Map.keys inventory))
+            (ObjectValidationState [] Map.empty)
+    pure
+        (CheckedObjectClosure
+            expectedTheory
+            (validatedObjects finalState))
+
+-- | Validate one declaration's new objects against an already checked
+-- closure. The existing closure is returned unchanged for an empty batch.
+extendObjectClosure
+    :: CheckedObjectClosure
+    -> [AssertedObject]
+    -> Either ObjectValidationError CheckedObjectClosure
+extendObjectClosure closure [] =
+    Right closure
+extendObjectClosure
+        (CheckedObjectClosure expectedTheory existing)
+        asserted = do
+    additions <- buildObjectInventory asserted
+    traverse_
+        (\identity ->
+            when
+                (Map.member identity existing)
+                (Left (DuplicateAssertedObjectId identity)))
+        (Map.keys additions)
+    let existingInventory =
+            checkedObjectContent <$> existing
+        inventory =
+            Map.union additions existingInventory
+    finalState <-
+        execStateT
+            (traverse_
+                (validateOneObject expectedTheory inventory)
+                (Map.keys additions))
+            (ObjectValidationState [] existing)
+    pure
+        (CheckedObjectClosure
+            expectedTheory
+            (validatedObjects finalState))
+
+buildObjectInventory
+    :: [AssertedObject]
+    -> Either ObjectValidationError (Map ObjectId ObjectContent)
+buildObjectInventory =
+    foldM insertOne Map.empty
+  where
+    insertOne inventory (AssertedObject identity content)
+        | Map.member identity inventory =
+            Left (DuplicateAssertedObjectId identity)
+        | otherwise =
+            Right (Map.insert identity content inventory)
+
+validateOneObject
+    :: TheoryId
+    -> Map ObjectId ObjectContent
+    -> ObjectId
+    -> StateT
+        ObjectValidationState
+        (Either ObjectValidationError)
+        ()
+validateOneObject expectedTheory inventory identity = do
+    alreadyValidated <-
+        gets (Map.member identity . validatedObjects)
+    unless alreadyValidated do
+        stack <- gets validationStack
+        when (identity `elem` stack) do
+            lift
+                (Left
+                    (TransparentObjectCycle
+                        (cyclePath identity stack)))
+        content <-
+            case Map.lookup identity inventory of
+                Nothing ->
+                    impossible
+                        "object validation root is absent from its inventory"
+                Just found ->
+                    pure found
+        unless
+            (objectContentTheory content == expectedTheory)
+            (lift
+                (Left
+                    (ObjectContentTheoryMismatch
+                        identity
+                        expectedTheory
+                        (objectContentTheory content))))
+        let expectedFamily =
+                objectContentFamily content
+            suppliedFamily =
+                objectIdFamily identity
+        unless
+            (suppliedFamily == expectedFamily)
+            (lift
+                (Left
+                    (ObjectContentFamilyMismatch
+                        identity
+                        expectedFamily
+                        suppliedFamily)))
+        modify'
+            (\validationState ->
+                validationState
+                    { validationStack =
+                        identity
+                            : validationStack validationState
+                    })
+        checked <- case content of
+            IntrinsicObjectContent
+                    theory
+                    tag
+                    suppliedType -> do
+                let expectedType =
+                        coreIntrinsicType tag
+                unless
+                    (suppliedType == expectedType)
+                    (lift
+                        (Left
+                            (IntrinsicObjectTypeMismatch
+                                identity
+                                tag
+                                expectedType
+                                suppliedType)))
+                verifyObjectId
+                    identity
+                    (intrinsicObjectId
+                        theory
+                        tag
+                        suppliedType)
+                pure
+                    (CheckedObject content suppliedType)
+            TransparentObjectContent
+                    theory
+                    suppliedType
+                    body -> do
+                traverse_
+                    (validateDependency expectedTheory inventory identity)
+                    (Set.toAscList (canonicalTermGlobals body))
+                resolvedObjects <-
+                    gets validatedObjects
+                checkedBody <-
+                    lift
+                        (first
+                            (TransparentObjectCoreCheckError
+                                identity)
+                            (checkCanonicalCore
+                                (\reference ->
+                                    checkedObjectType
+                                        <$> Map.lookup
+                                            reference
+                                            resolvedObjects)
+                                body))
+                let inferredType =
+                        frozenCoreType checkedBody
+                unless
+                    (inferredType == suppliedType)
+                    (lift
+                        (Left
+                            (TransparentObjectTypeMismatch
+                                identity
+                                suppliedType
+                                inferredType)))
+                verifyObjectId
+                    identity
+                    (transparentObjectId
+                        theory
+                        suppliedType
+                        body)
+                pure
+                    (CheckedObject content suppliedType)
+            OpaqueObjectContent
+                    theory
+                    seed
+                    suppliedType -> do
+                verifyObjectId
+                    identity
+                    (opaqueObjectId
+                        theory
+                        seed
+                        suppliedType)
+                pure
+                    (CheckedObject content suppliedType)
+        modify'
+            (\validationState ->
+                validationState
+                    { validationStack =
+                        dropCurrent
+                            identity
+                            (validationStack validationState)
+                    , validatedObjects =
+                        Map.insert
+                            identity
+                            checked
+                            (validatedObjects validationState)
+                    })
+  where
+    verifyObjectId supplied computed =
+        unless
+            (supplied == computed)
+            (lift
+                (Left
+                    (ObjectIdPayloadMismatch
+                        supplied
+                        computed)))
+
+validateDependency
+    :: TheoryId
+    -> Map ObjectId ObjectContent
+    -> ObjectId
+    -> ObjectId
+    -> StateT
+        ObjectValidationState
+        (Either ObjectValidationError)
+        ()
+validateDependency expectedTheory inventory parent dependency =
+    case Map.lookup dependency inventory of
+        Nothing ->
+            lift
+                (Left
+                    (TransparentObjectReferenceMissing
+                        parent
+                        dependency))
+        Just _ ->
+            validateOneObject
+                expectedTheory
+                inventory
+                dependency
+
+cyclePath :: ObjectId -> [ObjectId] -> NonEmpty ObjectId
+cyclePath repeated stack =
+    case break (== repeated) stack of
+        (between, _repeated : _outer) ->
+            repeated :| (reverse between <> [repeated])
+        _ ->
+            impossible "repeated object is absent from validation stack"
+
+dropCurrent :: ObjectId -> [ObjectId] -> [ObjectId]
+dropCurrent expected = \case
+    current : rest
+        | current == expected ->
+            rest
+    _ ->
+        impossible "object validation stack is inconsistent"
+
+objectContentFamily :: ObjectContent -> ObjectFamily
+objectContentFamily = \case
+    IntrinsicObjectContent{} ->
+        IntrinsicObject
+    TransparentObjectContent{} ->
+        TransparentObject
+    OpaqueObjectContent{} ->
+        OpaqueObject
+
+newtype PropositionId =
+    PropositionId MathematicalDigest
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+propositionIdDigest :: PropositionId -> MathematicalDigest
+propositionIdDigest (PropositionId digest) =
+    digest
+
+data CheckedPropositionContent = CheckedPropositionContent
+    !PropositionId
+    !(FrozenCheckedCore ObjectId)
+    deriving stock (Generic)
+    deriving anyclass (NFData)
+
+checkedPropositionId
+    :: CheckedPropositionContent
+    -> PropositionId
+checkedPropositionId
+        (CheckedPropositionContent identity _term) =
+    identity
+
+checkedPropositionTerm
+    :: CheckedPropositionContent
+    -> FrozenCheckedCore ObjectId
+checkedPropositionTerm
+        (CheckedPropositionContent _identity term) =
+    term
+
+data PropositionValidationError
+    = PropositionObjectMissing !ObjectId
+    | PropositionCoreCheckError !CoreCheckError
+    | PropositionIsNotProp !CoreType
+    | PropositionIdPayloadMismatch
+        !PropositionId
+        !PropositionId
+    deriving stock (Show, Eq)
+
+validatePropositionContent
+    :: CheckedObjectClosure
+    -> CanonicalTerm ObjectId
+    -> Either
+        PropositionValidationError
+        CheckedPropositionContent
+validatePropositionContent closure term = do
+    traverse_
+        (\identity ->
+            unless
+                (isJust
+                    (lookupCheckedObjectType identity closure))
+                (Left (PropositionObjectMissing identity)))
+        (Set.toAscList (canonicalTermGlobals term))
+    checked <-
+        first PropositionCoreCheckError
+            (checkCanonicalCore
+                (\identity ->
+                    lookupCheckedObjectType identity closure)
+                term)
+    unless
+        (frozenCoreType checked == TyProp)
+        (Left
+            (PropositionIsNotProp
+                (frozenCoreType checked)))
+    let identity =
+            propositionIdOf term
+    pure
+        (CheckedPropositionContent
+            identity
+            checked)
+
+validateAssertedPropositionContent
+    :: CheckedObjectClosure
+    -> PropositionId
+    -> CanonicalTerm ObjectId
+    -> Either
+        PropositionValidationError
+        CheckedPropositionContent
+validateAssertedPropositionContent closure supplied term = do
+    checked <-
+        validatePropositionContent closure term
+    let computed =
+            checkedPropositionId checked
+    unless
+        (supplied == computed)
+        (Left
+            (PropositionIdPayloadMismatch
+                supplied
+                computed))
+    pure checked
+
+propositionIdOf
+    :: CanonicalTerm ObjectId
+    -> PropositionId
+propositionIdOf term =
+    PropositionId
+        (codecInvariant
+            (hashCanonicalFields
+                "felix-proposition-v1"
+                [encodeCanonicalTerm encodeObjectId term]))
+
+
+data TheoremRef = TheoremRef
+    !TheoryId
+    !PropositionId
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+theoremRef :: TheoryId -> PropositionId -> TheoremRef
+theoremRef =
+    TheoremRef
+
+theoremRefTheory :: TheoremRef -> TheoryId
+theoremRefTheory (TheoremRef identity _proposition) =
+    identity
+
+theoremRefProposition :: TheoremRef -> PropositionId
+theoremRefProposition (TheoremRef _identity proposition) =
+    proposition
+
+encodeTheoremRef :: TheoremRef -> ByteString
+encodeTheoremRef (TheoremRef identity proposition) =
+    encodeFrame
+        (mathematicalDigestBytes
+            (theoryIdDigest identity))
+        <> encodeFrame
+            (mathematicalDigestBytes
+                (propositionIdDigest proposition))
+
+newtype TheoremId =
+    TheoremId MathematicalDigest
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+theoremId :: TheoremRef -> TheoremId
+theoremId reference =
+    TheoremId
+        (codecInvariant
+            (hashCanonicalFields
+                "felix-theorem"
+                [encodeTheoremRef reference]))
+
+theoremIdDigest :: TheoremId -> MathematicalDigest
+theoremIdDigest (TheoremId digest) =
+    digest
+
+
+putTheoryIdCache :: TheoryId -> CachePut
+putTheoryIdCache =
+    putMathematicalDigestCache . theoryIdDigest
+
+getTheoryIdCache :: CacheGet TheoryId
+getTheoryIdCache =
+    TheoryId <$> getMathematicalDigestCache
+
+putObjectIdCache :: ObjectId -> CachePut
+putObjectIdCache (ObjectId family digest) = do
+    putCacheTag (objectFamilyTag family)
+    putMathematicalDigestCache digest
+
+getObjectIdCache :: CacheGet ObjectId
+getObjectIdCache = do
+    family <- getCacheTag >>= \case
+        0x00 ->
+            pure IntrinsicObject
+        0x01 ->
+            pure TransparentObject
+        0x02 ->
+            pure OpaqueObject
+        tag ->
+            fail ("unknown cache object-family tag " <> show tag)
+    ObjectId family <$> getMathematicalDigestCache
+
+putOpaqueDeclarationSeedCache
+    :: OpaqueDeclarationSeed
+    -> CachePut
+putOpaqueDeclarationSeedCache =
+    putMathematicalDigestCache
+        . opaqueDeclarationSeedDigest
+
+getOpaqueDeclarationSeedCache
+    :: CacheGet OpaqueDeclarationSeed
+getOpaqueDeclarationSeedCache =
+    OpaqueDeclarationSeed
+        <$> getMathematicalDigestCache
+
+putObjectContentCache :: ObjectContent -> CachePut
+putObjectContentCache = \case
+    IntrinsicObjectContent identity tag coreType -> do
+        putCacheTag 0x00
+        putTheoryIdCache identity
+        putCoreIntrinsicTagCache tag
+        putCoreTypeCache coreType
+    TransparentObjectContent identity coreType body -> do
+        putCacheTag 0x01
+        putTheoryIdCache identity
+        putCoreTypeCache coreType
+        putCanonicalTermCache putObjectIdCache body
+    OpaqueObjectContent identity seed coreType -> do
+        putCacheTag 0x02
+        putTheoryIdCache identity
+        putOpaqueDeclarationSeedCache seed
+        putCoreTypeCache coreType
+
+getObjectContentCache :: CacheGet ObjectContent
+getObjectContentCache =
+    getCacheTag >>= \case
+        0x00 ->
+            IntrinsicObjectContent
+                <$> getTheoryIdCache
+                <*> getCoreIntrinsicTagCache
+                <*> getCoreTypeCache
+        0x01 ->
+            TransparentObjectContent
+                <$> getTheoryIdCache
+                <*> getCoreTypeCache
+                <*> getCanonicalTermCache getObjectIdCache
+        0x02 ->
+            OpaqueObjectContent
+                <$> getTheoryIdCache
+                <*> getOpaqueDeclarationSeedCache
+                <*> getCoreTypeCache
+        tag ->
+            fail ("unknown cache object-content tag " <> show tag)
+
+putPropositionIdCache :: PropositionId -> CachePut
+putPropositionIdCache =
+    putMathematicalDigestCache . propositionIdDigest
+
+getPropositionIdCache :: CacheGet PropositionId
+getPropositionIdCache =
+    PropositionId <$> getMathematicalDigestCache
+
+putTheoremRefCache :: TheoremRef -> CachePut
+putTheoremRefCache (TheoremRef identity proposition) = do
+    putTheoryIdCache identity
+    putPropositionIdCache proposition
+
+getTheoremRefCache :: CacheGet TheoremRef
+getTheoremRefCache =
+    TheoremRef
+        <$> getTheoryIdCache
+        <*> getPropositionIdCache
+
+
+objectFamilyTag :: ObjectFamily -> Word8
+objectFamilyTag = \case
+    IntrinsicObject ->
+        0x00
+    TransparentObject ->
+        0x01
+    OpaqueObject ->
+        0x02
+
+encodeKernelRuleTag :: KernelRuleTag -> ByteString
+encodeKernelRuleTag =
+    ByteString.singleton . \case
+        SetLfpBound ->
+            0x00
+        SetLfpLeast ->
+            0x01
+        SetLfpFixed ->
+            0x02
+        SetLfpInduct ->
+            0x03
+
+encodeFoundationAxiomTag :: FoundationAxiomTag -> ByteString
+encodeFoundationAxiomTag =
+    ByteString.singleton . \case
+        EmptyCharacteristic ->
+            0x00
+        PairSetCharacteristic ->
+            0x01
+        FamilyUnionCharacteristic ->
+            0x02
+        PowerSetCharacteristic ->
+            0x03
+        SeparationCharacteristic ->
+            0x04
+        ReplacementCharacteristic ->
+            0x05
+        SetChooseWitness ->
+            0x06
+        SetExtensionality ->
+            0x07
+        SetInduction ->
+            0x08
+        PropositionalExtensionality ->
+            0x09
+        DoubleNegationElim ->
+            0x0a
+        UnivOfContains ->
+            0x0b
+        UnivOfTransitive ->
+            0x0c
+        UnivOfFamilyUnionClosed ->
+            0x0d
+        UnivOfPowerSetClosed ->
+            0x0e
+        UnivOfReplacementClosed ->
+            0x0f
+        UnivOfMinimal ->
+            0x10
+
+allCoreIntrinsicTags :: [CoreIntrinsicTag]
+allCoreIntrinsicTags =
+    [minBound .. maxBound]
+
+allKernelRuleTags :: [KernelRuleTag]
+allKernelRuleTags =
+    [minBound .. maxBound]
+
+allFoundationAxiomTags :: [FoundationAxiomTag]
+allFoundationAxiomTags =
+    [minBound .. maxBound]
+
+stableTagOrder
+    :: Show tag
+    => String
+    -> (tag -> ByteString)
+    -> [tag]
+    -> [tag]
+stableTagOrder description encodeTag tags
+    | Set.size encodedTags == length tags =
+        List.sortOn encodeTag tags
+    | otherwise =
+        impossible
+            ("duplicate stable "
+                <> description
+                <> " tag in "
+                <> show tags)
+  where
+    encodedTags =
+        Set.fromList (encodeTag <$> tags)
+
+codecInvariant
+    :: Either MathematicalCodecError value
+    -> value
+codecInvariant =
+    either
+        (impossible . ("canonical codec invariant: " <>) . show)
+        id