path: root/source/Felix/Checking/Identity.hs

{-# 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