Migrate to `Felix` namespaceHEADhotg

1 files changed, 1759 insertions, 0 deletions

diff --git a/source/Felix/Checking/Semantic.hs b/source/Felix/Checking/Semantic.hs
new file mode 100644
index 0000000..c9442f3
--- /dev/null
+++ b/source/Felix/Checking/Semantic.hs
@@ -0,0 +1,1759 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Canonical semantic declaration, prefix, interface, and validation keys.
+module Felix.Checking.Semantic
+    ( DeclarationSlot
+    , declarationSlot
+    , declarationSlotModule
+    , declarationSlotOrdinal
+    , FactSlot
+    , factSlot
+    , factSlotModule
+    , factSlotOrdinal
+    , SemanticName
+    , semanticName
+    , semanticNameText
+    , FactSearchEligibility(..)
+    , SemanticFactOccurrence
+    , semanticFactOccurrence
+    , semanticFactSlot
+    , semanticFactProposition
+    , semanticFactAuthority
+    , semanticFactSearchEligibility
+    , semanticFactFingerprint
+    , SemanticFactOccurrenceFingerprint
+    , semanticFactOccurrenceFingerprint
+    , semanticFactFingerprintDigest
+    , SemanticAlias
+    , semanticAlias
+    , semanticAliasName
+    , semanticAliasTarget
+    , SemanticGlobalKey(..)
+    , semanticGlobalKeyFromLexicalEntry
+    , semanticGlobalKeyType
+    , SemanticGlobalTarget(..)
+    , semanticGlobalTargetObject
+    , semanticGlobalTargetRequirements
+    , SemanticGlobalBinding
+    , semanticGlobalBinding
+    , semanticGlobalBindingKey
+    , semanticGlobalBindingTarget
+    , SemanticGlobalTargetError(..)
+    , validateSemanticGlobalBindingTarget
+    , SemanticEnvironmentDelta
+    , emptySemanticEnvironmentDelta
+    , semanticEnvironmentDelta
+    , semanticEnvironmentWithStructures
+    , semanticEnvironmentBindings
+    , semanticEnvironmentStructures
+    , SemanticStructurePhrase
+    , semanticStructurePhrase
+    , semanticStructurePhraseSingular
+    , semanticStructurePhrasePlural
+    , semanticStructurePhraseMarker
+    , SemanticStructureOperation
+    , semanticStructureOperation
+    , semanticStructureOperationSymbol
+    , semanticStructureOperationObject
+    , SemanticStructureDescriptor
+    , semanticStructureDescriptor
+    , semanticStructureDescriptorPhrase
+    , semanticStructureDescriptorPredicate
+    , semanticStructureDescriptorParents
+    , semanticStructureDescriptorOperations
+    , SemanticEnvironmentError(..)
+    , DeclarationInterfaceDelta
+    , declarationInterfaceDelta
+    , declarationDeltaSlot
+    , declarationDeltaFacts
+    , declarationDeltaAliases
+    , declarationDeltaObjects
+    , declarationDeltaPropositions
+    , declarationDeltaEnvironment
+    , DeclarationInterfaceError(..)
+    , SemanticInterfaceId
+    , semanticInterfaceIdDigest
+    , SemanticInterface
+    , semanticInterface
+    , semanticInterfaceOwner
+    , semanticInterfaceDirectInputs
+    , semanticInterfaceDeclarations
+    , semanticInterfaceAssertedId
+    , SemanticInterfaceError(..)
+    , validateSemanticInterface
+    , renderSemanticInterfaceError
+    , PrefixContextId
+    , initialPrefixContextId
+    , PrefixContextError(..)
+    , nextPrefixContextId
+    , prefixContextIdDigest
+    , ProofSyntaxId
+    , proofSyntaxId
+    , DeclarationSyntaxId
+    , declarationSyntaxId
+    , ProofValidationKey
+    , proofValidationKey
+    , proofValidationKeyDigest
+    , ProofValidationRecord
+    , proofValidationRecord
+    , proofValidationRecordKey
+    , proofValidationRecordCertificate
+    , DeclarationValidationKey
+    , declarationValidationKey
+    , declarationValidationKeyDigest
+    , DeclarationValidationRecord
+    , declarationValidationRecord
+    , declarationValidationRecordKey
+    , declarationValidationRecordCertificates
+    , ModuleArtifactKey
+    , moduleArtifactKey
+    , moduleArtifactKeyOwner
+    , moduleArtifactKeyDirectSemanticInputs
+    , moduleArtifactKeyTheory
+    , ModuleArtifactKeyError(..)
+    , ModuleArtifactId
+    , moduleArtifactId
+    , moduleArtifactIdDigest
+    , ModuleArtifactResult
+    , moduleArtifactResult
+    , moduleArtifactResultId
+    , moduleArtifactResultSyntax
+    , moduleArtifactResultSemantic
+    , putModuleArtifactKeyCache
+    , getModuleArtifactKeyCache
+    , putModuleArtifactIdCache
+    , getModuleArtifactIdCache
+    , putModuleArtifactResultCache
+    , getModuleArtifactResultCache
+    , putSemanticFactOccurrenceFingerprintCache
+    , getSemanticFactOccurrenceFingerprintCache
+    , putSemanticFactOccurrenceCache
+    , getSemanticFactOccurrenceCache
+    , putSemanticEnvironmentDeltaCache
+    , getSemanticEnvironmentDeltaCache
+    , putSemanticGlobalKeyCache
+    , getSemanticGlobalKeyCache
+    , putDeclarationInterfaceDeltaCache
+    , getDeclarationInterfaceDeltaCache
+    , putSemanticInterfaceCache
+    , getSemanticInterfaceCache
+    , putSemanticInterfaceIdCache
+    , getSemanticInterfaceIdCache
+    , putPrefixContextIdCache
+    , getPrefixContextIdCache
+    , putProofValidationRecordCache
+    , getProofValidationRecordCache
+    , putDeclarationValidationRecordCache
+    , getDeclarationValidationRecordCache
+    ) where
+
+import Base
+import Felix.Checking.Authority
+import Felix.Checking.Core
+import Felix.Checking.Identity
+import Felix.Cache.Codec
+import Felix.Math.Codec
+import Felix.Module
+import Felix.Parsed.Identity
+import Felix.Source
+import Felix.Syntax.Interface
+import Felix.Syntax.Abstract
+
+import Control.DeepSeq (NFData)
+import Control.Monad (unless, when)
+import Data.ByteString (ByteString)
+import Data.List qualified as List
+import Data.Map.Strict qualified as Map
+import Numeric.Natural (Natural)
+import Data.Set qualified as Set
+import Data.Text qualified as Text
+
+
+data DeclarationSlot = DeclarationSlot
+    !ModuleName
+    !LocalDeclarationOrdinal
+    deriving stock (Show, Eq, Ord)
+
+declarationSlot
+    :: ModuleName
+    -> LocalDeclarationOrdinal
+    -> DeclarationSlot
+declarationSlot =
+    DeclarationSlot
+
+declarationSlotModule :: DeclarationSlot -> ModuleName
+declarationSlotModule (DeclarationSlot owner _) =
+    owner
+
+declarationSlotOrdinal
+    :: DeclarationSlot
+    -> LocalDeclarationOrdinal
+declarationSlotOrdinal (DeclarationSlot _ ordinal) =
+    ordinal
+
+data FactSlot = FactSlot
+    !ModuleName
+    !LocalFactOrdinal
+    deriving stock (Show, Eq, Ord)
+
+factSlot :: ModuleName -> LocalFactOrdinal -> FactSlot
+factSlot =
+    FactSlot
+
+factSlotModule :: FactSlot -> ModuleName
+factSlotModule (FactSlot owner _) =
+    owner
+
+factSlotOrdinal :: FactSlot -> LocalFactOrdinal
+factSlotOrdinal (FactSlot _ ordinal) =
+    ordinal
+
+newtype SemanticName =
+    SemanticName Text
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+semanticName :: Text -> SemanticName
+semanticName =
+    SemanticName
+
+semanticNameText :: SemanticName -> Text
+semanticNameText (SemanticName name) =
+    name
+
+data FactSearchEligibility
+    = SearchEligible
+    | SearchIneligible
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+newtype SemanticFactOccurrenceFingerprint =
+    SemanticFactOccurrenceFingerprint CacheDigest
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+semanticFactOccurrenceFingerprint
+    :: FactSlot
+    -> FactAuthority
+    -> SemanticFactOccurrenceFingerprint
+semanticFactOccurrenceFingerprint slot authority =
+    SemanticFactOccurrenceFingerprint
+        (hashCacheFields
+            "felix-semantic-fact-occurrence-v1"
+            [ encodeCache (putFactSlotCache slot)
+            , encodeCache (putFactAuthorityCache authority)
+            ])
+
+semanticFactFingerprintDigest
+    :: SemanticFactOccurrenceFingerprint
+    -> CacheDigest
+semanticFactFingerprintDigest
+        (SemanticFactOccurrenceFingerprint digest) =
+    digest
+
+data SemanticFactOccurrence = SemanticFactOccurrence
+    !FactSlot
+    !FactAuthority
+    !FactSearchEligibility
+    deriving stock (Show, Eq, Ord, Generic)
+
+semanticFactOccurrence
+    :: FactSlot
+    -> FactAuthority
+    -> FactSearchEligibility
+    -> SemanticFactOccurrence
+semanticFactOccurrence =
+    SemanticFactOccurrence
+
+semanticFactSlot :: SemanticFactOccurrence -> FactSlot
+semanticFactSlot
+        (SemanticFactOccurrence slot _ _) =
+    slot
+
+semanticFactProposition
+    :: SemanticFactOccurrence
+    -> PropositionId
+semanticFactProposition
+        (SemanticFactOccurrence _ authority _) =
+    theoremRefProposition
+        (factAuthorityTheorem authority)
+
+semanticFactAuthority
+    :: SemanticFactOccurrence
+    -> FactAuthority
+semanticFactAuthority
+        (SemanticFactOccurrence _ authority _) =
+    authority
+
+semanticFactSearchEligibility
+    :: SemanticFactOccurrence
+    -> FactSearchEligibility
+semanticFactSearchEligibility
+        (SemanticFactOccurrence _ _ eligibility) =
+    eligibility
+
+semanticFactFingerprint
+    :: SemanticFactOccurrence
+    -> SemanticFactOccurrenceFingerprint
+semanticFactFingerprint
+        (SemanticFactOccurrence slot authority _) =
+    semanticFactOccurrenceFingerprint slot authority
+
+data SemanticAlias = SemanticAlias
+    !SemanticName
+    !SemanticFactOccurrenceFingerprint
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+semanticAlias
+    :: SemanticName
+    -> SemanticFactOccurrenceFingerprint
+    -> SemanticAlias
+semanticAlias =
+    SemanticAlias
+
+semanticAliasName :: SemanticAlias -> SemanticName
+semanticAliasName (SemanticAlias name _) =
+    name
+
+semanticAliasTarget
+    :: SemanticAlias
+    -> SemanticFactOccurrenceFingerprint
+semanticAliasTarget (SemanticAlias _ target) =
+    target
+
+
+-- | Exact source-level name used to resolve a declared monomorphic object.
+-- Presentation markers and expression fixity are deliberately absent.
+data SemanticGlobalKey
+    = SemanticLeftAdjective !Pattern
+    | SemanticRightAdjective !Pattern
+    | SemanticFunctionPhrase !Pattern !Pattern
+    | SemanticNoun !Pattern !Pattern
+    | SemanticVerb !Pattern !Pattern
+    | SemanticRelation !Token !ParameterArity
+    | SemanticExpressionFunction !Pattern
+    | SemanticPrefixPredicate !Text !Natural
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+semanticGlobalKeyType :: SemanticGlobalKey -> Maybe CoreType
+semanticGlobalKeyType = \case
+    SemanticLeftAdjective pat ->
+        Just (setArguments (1 + patternArity pat) TyProp)
+    SemanticRightAdjective pat ->
+        Just (setArguments (1 + patternArity pat) TyProp)
+    SemanticFunctionPhrase singular plural
+        | patternArity singular == patternArity plural ->
+            Just (setArguments (patternArity singular) TySet)
+        | otherwise -> Nothing
+    SemanticNoun singular plural
+        | patternArity singular == patternArity plural ->
+            Just (setArguments (1 + patternArity singular) TyProp)
+        | otherwise -> Nothing
+    SemanticVerb singular plural
+        | patternArity singular == patternArity plural ->
+            Just (setArguments (1 + patternArity singular) TyProp)
+        | otherwise -> Nothing
+    SemanticRelation _token arity ->
+        Just
+            (setArguments
+                (2 + parameterArityValue arity)
+                TyProp)
+    SemanticExpressionFunction pat ->
+        Just (setArguments (patternArity pat) TySet)
+    SemanticPrefixPredicate _command arity ->
+        Just (setArguments arity TyProp)
+  where
+    patternArity :: Pattern -> Natural
+    patternArity = \case
+        End -> 0
+        HoleCons rest -> 1 + patternArity rest
+        TokenCons _token rest -> patternArity rest
+
+    setArguments :: Natural -> CoreType -> CoreType
+    setArguments argumentCount result =
+        foldr
+            (const (TyArrow TySet))
+            result
+            [1 .. argumentCount]
+
+semanticGlobalKeyFromLexicalEntry
+    :: CanonicalLexicalEntry
+    -> Maybe SemanticGlobalKey
+semanticGlobalKeyFromLexicalEntry = \case
+    CanonicalLeftAdjective pat _marker ->
+        Just (SemanticLeftAdjective pat)
+    CanonicalRightAdjective pat _marker ->
+        Just (SemanticRightAdjective pat)
+    CanonicalFunctionPhrase singular plural _marker ->
+        Just (SemanticFunctionPhrase singular plural)
+    CanonicalNoun singular plural _marker ->
+        Just (SemanticNoun singular plural)
+    CanonicalVerb singular plural _marker ->
+        Just (SemanticVerb singular plural)
+    CanonicalRelation token arity _marker ->
+        Just (SemanticRelation token arity)
+    CanonicalExpressionFunction pat _marker _fixity ->
+        Just (SemanticExpressionFunction pat)
+    CanonicalPrefixPredicate command arity _marker ->
+        Just (SemanticPrefixPredicate command arity)
+    CanonicalStructureNoun{} ->
+        Nothing
+    CanonicalStructureOperation{} ->
+        Nothing
+
+data SemanticGlobalTarget
+    = GlobalReference !ObjectId
+    | TransparentExpansion !ObjectId
+    | ContextualTransparentExpansion
+        !ObjectId
+        !(Map.Map StructSymbol ObjectId)
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+semanticGlobalTargetObject :: SemanticGlobalTarget -> ObjectId
+semanticGlobalTargetObject = \case
+    GlobalReference identity -> identity
+    TransparentExpansion identity -> identity
+    ContextualTransparentExpansion identity _requirements -> identity
+
+semanticGlobalTargetRequirements
+    :: SemanticGlobalTarget
+    -> Map.Map StructSymbol ObjectId
+semanticGlobalTargetRequirements = \case
+    GlobalReference{} -> Map.empty
+    TransparentExpansion{} -> Map.empty
+    ContextualTransparentExpansion _identity requirements -> requirements
+
+data SemanticGlobalBinding = SemanticGlobalBinding
+    !SemanticGlobalKey
+    !SemanticGlobalTarget
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+semanticGlobalBinding
+    :: SemanticGlobalKey
+    -> SemanticGlobalTarget
+    -> SemanticGlobalBinding
+semanticGlobalBinding =
+    SemanticGlobalBinding
+
+semanticGlobalBindingKey
+    :: SemanticGlobalBinding
+    -> SemanticGlobalKey
+semanticGlobalBindingKey (SemanticGlobalBinding key _target) =
+    key
+
+semanticGlobalBindingTarget
+    :: SemanticGlobalBinding
+    -> SemanticGlobalTarget
+semanticGlobalBindingTarget (SemanticGlobalBinding _key target) =
+    target
+
+data SemanticGlobalTargetError
+    = SemanticGlobalKeyHasInconsistentArity !SemanticGlobalKey
+    | SemanticGlobalTargetMissing !ObjectId
+    | SemanticGlobalTargetIsIntrinsic !ObjectId
+    | SemanticGlobalTargetTypeMismatch !ObjectId !CoreType !CoreType
+    | SemanticGlobalExpansionNotTransparent !ObjectId
+    | SemanticGlobalContextualRequirementsEmpty !ObjectId
+    | SemanticGlobalContextualRequirementMissing !StructSymbol !ObjectId
+    | SemanticGlobalContextualRequirementIsIntrinsic !StructSymbol !ObjectId
+    | SemanticGlobalContextualRequirementTypeMismatch
+        !StructSymbol !ObjectId !CoreType !CoreType
+    | SemanticGlobalContextualRequirementNotProvided
+        !StructSymbol !ObjectId
+    | SemanticGlobalContextualRequirementNotReferenced !StructSymbol !ObjectId
+    deriving stock (Show, Eq)
+
+validateSemanticGlobalBindingTarget
+    :: Set.Set (StructSymbol, ObjectId)
+    -> CheckedObjectClosure
+    -> SemanticGlobalBinding
+    -> Either SemanticGlobalTargetError ()
+validateSemanticGlobalBindingTarget operationBindings closure binding = do
+    expected <-
+        maybe
+            (Left (SemanticGlobalKeyHasInconsistentArity key))
+            Right
+            (semanticGlobalKeyType key)
+    content <-
+        maybe
+            (Left (SemanticGlobalTargetMissing identity))
+            Right
+            (lookupCheckedObjectContent identity closure)
+    when
+        (objectIdFamily identity == IntrinsicObject)
+        (Left (SemanticGlobalTargetIsIntrinsic identity))
+    let targetExpected =
+            case target of
+                ContextualTransparentExpansion{} ->
+                    TyArrow TySet expected
+                _ -> expected
+        actual = objectContentType content
+    unless
+        (actual == targetExpected)
+        (Left
+            (SemanticGlobalTargetTypeMismatch
+                identity targetExpected actual))
+    case target of
+        GlobalReference{} -> pure ()
+        TransparentExpansion{} ->
+            validateTransparent content
+        ContextualTransparentExpansion _ requirements -> do
+            validateTransparent content
+            when
+                (Map.null requirements)
+                (Left (SemanticGlobalContextualRequirementsEmpty identity))
+            traverse_ (validateRequirement content) (Map.toAscList requirements)
+  where
+    key = semanticGlobalBindingKey binding
+    target = semanticGlobalBindingTarget binding
+    identity = semanticGlobalTargetObject target
+
+    validateTransparent = \case
+        TransparentObjectContent{} -> pure ()
+        _ -> Left (SemanticGlobalExpansionNotTransparent identity)
+
+    validateRequirement content (symbol, object) = do
+        operationContent <-
+            maybe
+                (Left
+                    (SemanticGlobalContextualRequirementMissing
+                        symbol object))
+                Right
+                (lookupCheckedObjectContent object closure)
+        when
+            (objectIdFamily object == IntrinsicObject)
+            (Left
+                (SemanticGlobalContextualRequirementIsIntrinsic
+                    symbol object))
+        let expectedOperation = TyArrow TySet TySet
+            actualOperation = objectContentType operationContent
+        unless
+            (actualOperation == expectedOperation)
+            (Left
+                (SemanticGlobalContextualRequirementTypeMismatch
+                    symbol object expectedOperation actualOperation))
+        unless
+            ((symbol, object) `Set.member` operationBindings)
+            (Left
+                (SemanticGlobalContextualRequirementNotProvided
+                    symbol object))
+        case content of
+            TransparentObjectContent _theory _coreType body ->
+                unless
+                    (object `Set.member` canonicalTermGlobals body)
+                    (Left
+                        (SemanticGlobalContextualRequirementNotReferenced
+                            symbol object))
+            _ -> impossible "a contextual expansion was not transparent"
+
+data SemanticEnvironmentDelta
+    = EmptySemanticEnvironmentDelta
+    | SemanticGlobalBindings ![SemanticGlobalBinding]
+    | SemanticGlobalBindingsAndStructures
+        ![SemanticGlobalBinding]
+        ![SemanticStructureDescriptor]
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+data SemanticStructurePhrase = SemanticStructurePhrase
+    !Pattern
+    !Pattern
+    !Marker
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+semanticStructurePhrase :: LexicalItemSgPl -> SemanticStructurePhrase
+semanticStructurePhrase (LexicalItemSgPl forms marker) =
+    SemanticStructurePhrase (sg forms) (pl forms) marker
+
+semanticStructurePhraseSingular :: SemanticStructurePhrase -> Pattern
+semanticStructurePhraseSingular (SemanticStructurePhrase singular _ _) =
+    singular
+
+semanticStructurePhrasePlural :: SemanticStructurePhrase -> Pattern
+semanticStructurePhrasePlural (SemanticStructurePhrase _ plural _) =
+    plural
+
+semanticStructurePhraseMarker :: SemanticStructurePhrase -> Marker
+semanticStructurePhraseMarker (SemanticStructurePhrase _ _ marker) =
+    marker
+
+data SemanticStructureOperation = SemanticStructureOperation
+    !StructSymbol
+    !ObjectId
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+semanticStructureOperation
+    :: StructSymbol
+    -> ObjectId
+    -> SemanticStructureOperation
+semanticStructureOperation =
+    SemanticStructureOperation
+
+semanticStructureOperationSymbol
+    :: SemanticStructureOperation
+    -> StructSymbol
+semanticStructureOperationSymbol (SemanticStructureOperation symbol _) =
+    symbol
+
+semanticStructureOperationObject
+    :: SemanticStructureOperation
+    -> ObjectId
+semanticStructureOperationObject (SemanticStructureOperation _ object) =
+    object
+
+data SemanticStructureDescriptor = SemanticStructureDescriptor
+    !SemanticStructurePhrase
+    !(Maybe ObjectId)
+    ![SemanticStructurePhrase]
+    ![SemanticStructureOperation]
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+semanticStructureDescriptor
+    :: SemanticStructurePhrase
+    -> Maybe ObjectId
+    -> [SemanticStructurePhrase]
+    -> [SemanticStructureOperation]
+    -> Either SemanticEnvironmentError SemanticStructureDescriptor
+semanticStructureDescriptor structurePhrase predicate parents operations = do
+    case firstDuplicate parents of
+        Just duplicate ->
+            Left (DuplicateSemanticStructureParent duplicate)
+        Nothing -> pure ()
+    when
+        (structurePhrase `elem` parents)
+        (Left (SelfSemanticStructureParent structurePhrase))
+    case firstDuplicate (semanticStructureOperationSymbol <$> operations) of
+        Just duplicate ->
+            Left (DuplicateSemanticStructureOperation duplicate)
+        Nothing -> pure ()
+    pure
+        (SemanticStructureDescriptor
+            structurePhrase predicate parents operations)
+
+semanticStructureDescriptorPhrase
+    :: SemanticStructureDescriptor
+    -> SemanticStructurePhrase
+semanticStructureDescriptorPhrase
+        (SemanticStructureDescriptor structurePhrase _ _ _) =
+    structurePhrase
+
+semanticStructureDescriptorPredicate
+    :: SemanticStructureDescriptor
+    -> Maybe ObjectId
+semanticStructureDescriptorPredicate
+        (SemanticStructureDescriptor _ predicate _ _) =
+    predicate
+
+semanticStructureDescriptorParents
+    :: SemanticStructureDescriptor
+    -> [SemanticStructurePhrase]
+semanticStructureDescriptorParents
+        (SemanticStructureDescriptor _ _ parents _) =
+    parents
+
+semanticStructureDescriptorOperations
+    :: SemanticStructureDescriptor
+    -> [SemanticStructureOperation]
+semanticStructureDescriptorOperations
+        (SemanticStructureDescriptor _ _ _ operations) =
+    operations
+
+data SemanticEnvironmentError
+    = DuplicateSemanticGlobalKey !SemanticGlobalKey
+    | NonCanonicalSemanticGlobalBindingOrder
+    | DuplicateSemanticStructure !SemanticStructurePhrase
+    | NonCanonicalSemanticStructureOrder
+    | DuplicateSemanticStructureParent !SemanticStructurePhrase
+    | SelfSemanticStructureParent !SemanticStructurePhrase
+    | DuplicateSemanticStructureOperation !StructSymbol
+    deriving stock (Show, Eq)
+
+emptySemanticEnvironmentDelta :: SemanticEnvironmentDelta
+emptySemanticEnvironmentDelta =
+    EmptySemanticEnvironmentDelta
+
+semanticEnvironmentDelta
+    :: [SemanticGlobalBinding]
+    -> Either SemanticEnvironmentError SemanticEnvironmentDelta
+semanticEnvironmentDelta bindings =
+    semanticEnvironmentWithStructures bindings []
+
+semanticEnvironmentWithStructures
+    :: [SemanticGlobalBinding]
+    -> [SemanticStructureDescriptor]
+    -> Either SemanticEnvironmentError SemanticEnvironmentDelta
+semanticEnvironmentWithStructures [] [] =
+    Right EmptySemanticEnvironmentDelta
+semanticEnvironmentWithStructures bindings structures = do
+    case firstDuplicate (semanticGlobalBindingKey <$> bindings) of
+        Just duplicate ->
+            Left (DuplicateSemanticGlobalKey duplicate)
+        Nothing ->
+            pure ()
+    unless
+        (bindings == List.sortOn semanticGlobalBindingKey bindings)
+        (Left NonCanonicalSemanticGlobalBindingOrder)
+    case firstDuplicate (semanticStructureDescriptorPhrase <$> structures) of
+        Just duplicate ->
+            Left (DuplicateSemanticStructure duplicate)
+        Nothing -> pure ()
+    unless
+        ( structures
+            == List.sortOn semanticStructureDescriptorPhrase structures
+        )
+        (Left NonCanonicalSemanticStructureOrder)
+    pure
+        (case structures of
+            [] -> SemanticGlobalBindings bindings
+            _ -> SemanticGlobalBindingsAndStructures bindings structures)
+
+semanticEnvironmentBindings
+    :: SemanticEnvironmentDelta
+    -> [SemanticGlobalBinding]
+semanticEnvironmentBindings = \case
+    EmptySemanticEnvironmentDelta -> []
+    SemanticGlobalBindings bindings -> bindings
+    SemanticGlobalBindingsAndStructures bindings _ -> bindings
+
+semanticEnvironmentStructures
+    :: SemanticEnvironmentDelta
+    -> [SemanticStructureDescriptor]
+semanticEnvironmentStructures = \case
+    EmptySemanticEnvironmentDelta -> []
+    SemanticGlobalBindings{} -> []
+    SemanticGlobalBindingsAndStructures _ structures -> structures
+
+
+data DeclarationInterfaceDelta = DeclarationInterfaceDelta
+    !DeclarationSlot
+    ![SemanticFactOccurrence]
+    ![SemanticAlias]
+    ![ObjectId]
+    ![PropositionId]
+    !SemanticEnvironmentDelta
+    deriving stock (Show, Eq, Ord, Generic)
+
+data DeclarationInterfaceError
+    = DeclarationFactOwnerMismatch !FactSlot
+    | DuplicateDeclarationFactSlot !FactSlot
+    | DuplicateDeclarationFactFingerprint
+        !SemanticFactOccurrenceFingerprint
+    | DuplicateDeclarationAlias !SemanticName
+    | DuplicateDeclarationObject !ObjectId
+    | DuplicateDeclarationProposition !PropositionId
+    | DeclarationFactPropositionMissing !PropositionId
+    deriving stock (Show, Eq)
+
+declarationInterfaceDelta
+    :: DeclarationSlot
+    -> [SemanticFactOccurrence]
+    -> [SemanticAlias]
+    -> [ObjectId]
+    -> [PropositionId]
+    -> SemanticEnvironmentDelta
+    -> Either DeclarationInterfaceError DeclarationInterfaceDelta
+declarationInterfaceDelta
+        slot facts aliases objects propositions environment = do
+    traverse_ validateFact facts
+    rejectDuplicate
+        DuplicateDeclarationFactSlot
+        (semanticFactSlot <$> facts)
+    rejectDuplicate
+        DuplicateDeclarationFactFingerprint
+        (semanticFactFingerprint <$> facts)
+    rejectDuplicate
+        DuplicateDeclarationAlias
+        (semanticAliasName <$> aliases)
+    rejectDuplicate DuplicateDeclarationObject objects
+    rejectDuplicate DuplicateDeclarationProposition propositions
+    pure
+        (DeclarationInterfaceDelta
+            slot facts aliases objects propositions environment)
+  where
+    owner = declarationSlotModule slot
+    propositionSet = Set.fromList propositions
+
+    validateFact occurrence = do
+        unless
+            (factSlotModule (semanticFactSlot occurrence) == owner)
+            (Left
+                (DeclarationFactOwnerMismatch
+                    (semanticFactSlot occurrence)))
+        let proposition =
+                semanticFactProposition occurrence
+        unless
+            (proposition `Set.member` propositionSet)
+            (Left (DeclarationFactPropositionMissing proposition))
+
+declarationDeltaSlot
+    :: DeclarationInterfaceDelta
+    -> DeclarationSlot
+declarationDeltaSlot
+        (DeclarationInterfaceDelta slot _ _ _ _ _) =
+    slot
+
+declarationDeltaFacts
+    :: DeclarationInterfaceDelta
+    -> [SemanticFactOccurrence]
+declarationDeltaFacts
+        (DeclarationInterfaceDelta _ facts _ _ _ _) =
+    facts
+
+declarationDeltaAliases
+    :: DeclarationInterfaceDelta
+    -> [SemanticAlias]
+declarationDeltaAliases
+        (DeclarationInterfaceDelta _ _ aliases _ _ _) =
+    aliases
+
+declarationDeltaObjects
+    :: DeclarationInterfaceDelta
+    -> [ObjectId]
+declarationDeltaObjects
+        (DeclarationInterfaceDelta _ _ _ objects _ _) =
+    objects
+
+declarationDeltaPropositions
+    :: DeclarationInterfaceDelta
+    -> [PropositionId]
+declarationDeltaPropositions
+        (DeclarationInterfaceDelta _ _ _ _ propositions _) =
+    propositions
+
+declarationDeltaEnvironment
+    :: DeclarationInterfaceDelta
+    -> SemanticEnvironmentDelta
+declarationDeltaEnvironment
+        (DeclarationInterfaceDelta _ _ _ _ _ environment) =
+    environment
+
+
+newtype SemanticInterfaceId =
+    SemanticInterfaceId CacheDigest
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+semanticInterfaceIdDigest
+    :: SemanticInterfaceId
+    -> CacheDigest
+semanticInterfaceIdDigest (SemanticInterfaceId digest) =
+    digest
+
+data SemanticInterface = SemanticInterface
+    !ModuleName
+    ![SemanticInterfaceId]
+    ![DeclarationInterfaceDelta]
+    !SemanticInterfaceId
+    deriving stock (Show, Eq, Ord)
+
+data SemanticInterfaceError
+    = DuplicateDirectSemanticInterface !SemanticInterfaceId
+    | SemanticDeclarationOwnerMismatch !DeclarationSlot
+    | NonIncreasingDeclarationSlots
+    | NonIncreasingFactSlots
+    | SemanticInterfaceIdMismatch
+        !SemanticInterfaceId
+        !SemanticInterfaceId
+    deriving stock (Show, Eq)
+
+renderSemanticInterfaceError :: SemanticInterfaceError -> Text
+renderSemanticInterfaceError = \case
+    DuplicateDirectSemanticInterface interface ->
+        "direct semantic interface occurs more than once: "
+            <> Text.pack (show interface)
+    SemanticDeclarationOwnerMismatch slot ->
+        "declaration belongs to a different module: "
+            <> Text.pack (show slot)
+    NonIncreasingDeclarationSlots ->
+        "declaration slots are not in increasing order"
+    NonIncreasingFactSlots ->
+        "fact slots are not in increasing order"
+    SemanticInterfaceIdMismatch expected actual ->
+        "semantic interface identity mismatch: expected "
+            <> Text.pack (show expected)
+            <> ", found " <> Text.pack (show actual)
+
+semanticInterface
+    :: ModuleName
+    -> [SemanticInterfaceId]
+    -> [DeclarationInterfaceDelta]
+    -> Either SemanticInterfaceError SemanticInterface
+semanticInterface owner direct declarations = do
+    validateSemanticInterfaceStructure owner direct declarations
+    let identity =
+            computeSemanticInterfaceId owner direct declarations
+    pure (SemanticInterface owner direct declarations identity)
+
+validateSemanticInterface
+    :: ModuleName
+    -> [SemanticInterfaceId]
+    -> [DeclarationInterfaceDelta]
+    -> SemanticInterfaceId
+    -> Either SemanticInterfaceError SemanticInterface
+validateSemanticInterface owner direct declarations asserted = do
+    validateSemanticInterfaceStructure owner direct declarations
+    let computed =
+            computeSemanticInterfaceId
+                owner direct declarations
+    unless
+        (asserted == computed)
+        (Left
+            (SemanticInterfaceIdMismatch asserted computed))
+    pure
+        (SemanticInterface
+            owner direct declarations asserted)
+
+validateSemanticInterfaceStructure
+    :: ModuleName
+    -> [SemanticInterfaceId]
+    -> [DeclarationInterfaceDelta]
+    -> Either SemanticInterfaceError ()
+validateSemanticInterfaceStructure owner direct declarations = do
+    rejectDuplicate
+        DuplicateDirectSemanticInterface
+        direct
+    traverse_
+        (\delta ->
+            unless
+                (declarationSlotModule
+                    (declarationDeltaSlot delta)
+                    == owner)
+                (Left
+                    (SemanticDeclarationOwnerMismatch
+                        (declarationDeltaSlot delta))))
+        declarations
+    unless
+        (strictlyIncreasing
+            ( localDeclarationOrdinalValue
+                . declarationSlotOrdinal
+                . declarationDeltaSlot
+                <$> declarations))
+        (Left NonIncreasingDeclarationSlots)
+    unless
+        (strictlyIncreasing
+            ( localFactOrdinalValue
+                . factSlotOrdinal
+                . semanticFactSlot
+                <$> concatMap
+                    declarationDeltaFacts
+                    declarations))
+        (Left NonIncreasingFactSlots)
+
+semanticInterfaceOwner :: SemanticInterface -> ModuleName
+semanticInterfaceOwner
+        (SemanticInterface owner _ _ _) =
+    owner
+
+semanticInterfaceDirectInputs
+    :: SemanticInterface
+    -> [SemanticInterfaceId]
+semanticInterfaceDirectInputs
+        (SemanticInterface _ direct _ _) =
+    direct
+
+semanticInterfaceDeclarations
+    :: SemanticInterface
+    -> [DeclarationInterfaceDelta]
+semanticInterfaceDeclarations
+        (SemanticInterface _ _ declarations _) =
+    declarations
+
+semanticInterfaceAssertedId
+    :: SemanticInterface
+    -> SemanticInterfaceId
+semanticInterfaceAssertedId
+        (SemanticInterface _ _ _ asserted) =
+    asserted
+
+computeSemanticInterfaceId
+    :: ModuleName
+    -> [SemanticInterfaceId]
+    -> [DeclarationInterfaceDelta]
+    -> SemanticInterfaceId
+computeSemanticInterfaceId owner direct declarations =
+    SemanticInterfaceId
+        (hashCacheFields
+            "felix-semantic-interface-v1"
+            [ encodeCache (putModuleNameCache owner)
+            , encodeCache
+                (putCacheList
+                    putSemanticInterfaceIdCache
+                    direct)
+            , encodeCache
+                (putCacheList
+                    putDeclarationInterfaceDeltaCache
+                    declarations)
+            ])
+
+
+newtype PrefixContextId =
+    PrefixContextId CacheDigest
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+data PrefixContextError
+    = DuplicateInitialPrefixSemanticInput !SemanticInterfaceId
+    deriving stock (Show, Eq)
+
+initialPrefixContextId
+    :: TheoryId
+    -> ModuleName
+    -> [SemanticInterfaceId]
+    -> Either PrefixContextError PrefixContextId
+initialPrefixContextId theory owner direct = do
+    rejectDuplicate
+        DuplicateInitialPrefixSemanticInput
+        direct
+    pure
+        (PrefixContextId
+            (hashCacheFields
+                "felix-prefix-initial-v1"
+                [ encodeCache (putTheoryIdCache theory)
+                , encodeCache (putModuleNameCache owner)
+                , encodeCache
+                    (putCacheList
+                        putSemanticInterfaceIdCache
+                        direct)
+                ]))
+
+nextPrefixContextId
+    :: PrefixContextId
+    -> DeclarationInterfaceDelta
+    -> PrefixContextId
+nextPrefixContextId previous delta =
+    PrefixContextId
+        (hashCacheFields
+            "felix-prefix-step-v1"
+            [ encodeCache (putPrefixContextIdCache previous)
+            , encodeCache
+                (putDeclarationInterfaceDeltaCache delta)
+            ])
+
+prefixContextIdDigest :: PrefixContextId -> CacheDigest
+prefixContextIdDigest (PrefixContextId digest) =
+    digest
+
+
+newtype ProofSyntaxId =
+    ProofSyntaxId CacheDigest
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+proofSyntaxId :: ByteString -> ProofSyntaxId
+proofSyntaxId bytes =
+    ProofSyntaxId
+        (hashCacheFields "felix-proof-syntax-v1" [bytes])
+
+newtype DeclarationSyntaxId =
+    DeclarationSyntaxId CacheDigest
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+declarationSyntaxId :: ByteString -> DeclarationSyntaxId
+declarationSyntaxId bytes =
+    DeclarationSyntaxId
+        (hashCacheFields "felix-declaration-syntax-v1" [bytes])
+
+newtype ProofValidationKey =
+    ProofValidationKey CacheDigest
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+proofValidationKey
+    :: TheoremId
+    -> ProofSyntaxId
+    -> PrefixContextId
+    -> ProofValidationKey
+proofValidationKey theorem (ProofSyntaxId syntax) prefix =
+    ProofValidationKey
+        (hashCacheFields
+            "felix-proof-validation"
+            [ mathematicalDigestBytes
+                (theoremIdDigest theorem)
+            , cacheDigestBytes syntax
+            , encodeCache (putPrefixContextIdCache prefix)
+            ])
+
+proofValidationKeyDigest
+    :: ProofValidationKey
+    -> CacheDigest
+proofValidationKeyDigest (ProofValidationKey digest) =
+    digest
+
+data ProofValidationRecord = ProofValidationRecord
+    !ProofValidationKey
+    !ValidationCertificate
+    deriving stock (Show, Eq, Ord, Generic)
+
+proofValidationRecord
+    :: ProofValidationKey
+    -> ValidationCertificate
+    -> ProofValidationRecord
+proofValidationRecord =
+    ProofValidationRecord
+
+proofValidationRecordKey
+    :: ProofValidationRecord
+    -> ProofValidationKey
+proofValidationRecordKey
+        (ProofValidationRecord key _) =
+    key
+
+proofValidationRecordCertificate
+    :: ProofValidationRecord
+    -> ValidationCertificate
+proofValidationRecordCertificate
+        (ProofValidationRecord _ certificate) =
+    certificate
+
+newtype DeclarationValidationKey =
+    DeclarationValidationKey CacheDigest
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+declarationValidationKey
+    :: DeclarationSyntaxId
+    -> PrefixContextId
+    -> [ObjectId]
+    -> [TheoremId]
+    -> DeclarationValidationKey
+declarationValidationKey
+        (DeclarationSyntaxId syntax)
+        prefix objects theorems =
+    DeclarationValidationKey
+        (hashCacheFields
+            "felix-declaration-validation"
+            [ cacheDigestBytes syntax
+            , encodeCache (putPrefixContextIdCache prefix)
+            , encodeCache (putCacheList putObjectIdCache objects)
+            , encodeCache
+                (putCacheList
+                    (putMathematicalDigestCache . theoremIdDigest)
+                    theorems)
+            ])
+
+declarationValidationKeyDigest
+    :: DeclarationValidationKey
+    -> CacheDigest
+declarationValidationKeyDigest
+        (DeclarationValidationKey digest) =
+    digest
+
+data DeclarationValidationRecord = DeclarationValidationRecord
+    !DeclarationValidationKey
+    ![ValidationCertificate]
+    deriving stock (Show, Eq, Ord, Generic)
+
+declarationValidationRecord
+    :: DeclarationValidationKey
+    -> [ValidationCertificate]
+    -> DeclarationValidationRecord
+declarationValidationRecord =
+    DeclarationValidationRecord
+
+declarationValidationRecordKey
+    :: DeclarationValidationRecord
+    -> DeclarationValidationKey
+declarationValidationRecordKey
+        (DeclarationValidationRecord key _) =
+    key
+
+declarationValidationRecordCertificates
+    :: DeclarationValidationRecord
+    -> [ValidationCertificate]
+declarationValidationRecordCertificates
+        (DeclarationValidationRecord _ certificates) =
+    certificates
+
+
+data ModuleArtifactKey = ModuleArtifactKey
+    !ModuleName
+    !ParsedModuleId
+    ![SemanticInterfaceId]
+    !TheoryId
+    deriving stock (Show, Eq, Ord)
+
+data ModuleArtifactKeyError
+    = DuplicateModuleArtifactSemanticInput
+        !SemanticInterfaceId
+    deriving stock (Show, Eq)
+
+moduleArtifactKey
+    :: ModuleName
+    -> ParsedModuleId
+    -> [SemanticInterfaceId]
+    -> TheoryId
+    -> Either ModuleArtifactKeyError ModuleArtifactKey
+moduleArtifactKey owner parsed direct theory = do
+    rejectDuplicate
+        DuplicateModuleArtifactSemanticInput
+        direct
+    pure (ModuleArtifactKey owner parsed direct theory)
+
+moduleArtifactKeyOwner :: ModuleArtifactKey -> ModuleName
+moduleArtifactKeyOwner (ModuleArtifactKey owner _parsed _direct _theory) =
+    owner
+
+moduleArtifactKeyDirectSemanticInputs
+    :: ModuleArtifactKey
+    -> [SemanticInterfaceId]
+moduleArtifactKeyDirectSemanticInputs
+        (ModuleArtifactKey _owner _parsed direct _theory) =
+    direct
+
+moduleArtifactKeyTheory :: ModuleArtifactKey -> TheoryId
+moduleArtifactKeyTheory
+        (ModuleArtifactKey _owner _parsed _direct theory) =
+    theory
+
+newtype ModuleArtifactId =
+    ModuleArtifactId CacheDigest
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+moduleArtifactId :: ModuleArtifactKey -> ModuleArtifactId
+moduleArtifactId key =
+    ModuleArtifactId
+        (hashCacheFields
+            "felix-module-artifact-v1"
+            [encodeCache (putModuleArtifactKeyCache key)])
+
+moduleArtifactIdDigest :: ModuleArtifactId -> CacheDigest
+moduleArtifactIdDigest (ModuleArtifactId digest) =
+    digest
+
+data ModuleArtifactResult = ModuleArtifactResult
+    !ModuleArtifactId
+    !SyntaxInterfaceId
+    !SemanticInterfaceId
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+moduleArtifactResult
+    :: ModuleArtifactKey
+    -> SyntaxInterfaceId
+    -> SemanticInterfaceId
+    -> ModuleArtifactResult
+moduleArtifactResult key =
+    ModuleArtifactResult (moduleArtifactId key)
+
+moduleArtifactResultId
+    :: ModuleArtifactResult
+    -> ModuleArtifactId
+moduleArtifactResultId
+        (ModuleArtifactResult identity _ _) =
+    identity
+
+moduleArtifactResultSyntax
+    :: ModuleArtifactResult
+    -> SyntaxInterfaceId
+moduleArtifactResultSyntax
+        (ModuleArtifactResult _ syntax _) =
+    syntax
+
+moduleArtifactResultSemantic
+    :: ModuleArtifactResult
+    -> SemanticInterfaceId
+moduleArtifactResultSemantic
+        (ModuleArtifactResult _ _ semantic) =
+    semantic
+
+
+putSemanticFactOccurrenceFingerprintCache
+    :: SemanticFactOccurrenceFingerprint
+    -> CachePut
+putSemanticFactOccurrenceFingerprintCache
+        (SemanticFactOccurrenceFingerprint digest) =
+    putCacheDigest digest
+
+getSemanticFactOccurrenceFingerprintCache
+    :: CacheGet SemanticFactOccurrenceFingerprint
+getSemanticFactOccurrenceFingerprintCache =
+    SemanticFactOccurrenceFingerprint <$> getCacheDigest
+
+putSemanticFactOccurrenceCache
+    :: SemanticFactOccurrence
+    -> CachePut
+putSemanticFactOccurrenceCache
+        (SemanticFactOccurrence slot authority eligibility) = do
+    putFactSlotCache slot
+    putFactAuthorityCache authority
+    putEligibility eligibility
+
+getSemanticFactOccurrenceCache
+    :: CacheGet SemanticFactOccurrence
+getSemanticFactOccurrenceCache =
+    semanticFactOccurrence
+        <$> getFactSlotCache
+        <*> getFactAuthorityCache
+        <*> getEligibility
+
+putSemanticEnvironmentDeltaCache
+    :: SemanticEnvironmentDelta
+    -> CachePut
+putSemanticEnvironmentDeltaCache EmptySemanticEnvironmentDelta =
+    putCacheTag 0x00
+putSemanticEnvironmentDeltaCache (SemanticGlobalBindings bindings) = do
+    putCacheTag 0x01
+    putCacheList putSemanticGlobalBindingCache bindings
+putSemanticEnvironmentDeltaCache
+        (SemanticGlobalBindingsAndStructures bindings structures) = do
+    putCacheTag 0x02
+    putCacheList putSemanticGlobalBindingCache bindings
+    putCacheList putSemanticStructureDescriptorCache structures
+
+getSemanticEnvironmentDeltaCache
+    :: CacheGet SemanticEnvironmentDelta
+getSemanticEnvironmentDeltaCache =
+    getCacheTag >>= \case
+        0x00 ->
+            pure EmptySemanticEnvironmentDelta
+        0x01 -> do
+            bindings <- getCacheList getSemanticGlobalBindingCache
+            either
+                (fail . ("invalid semantic environment delta: " <>) . show)
+                pure
+                (semanticEnvironmentDelta bindings)
+        0x02 -> do
+            bindings <- getCacheList getSemanticGlobalBindingCache
+            structures <- getCacheList getSemanticStructureDescriptorCache
+            either
+                (fail . ("invalid semantic environment delta: " <>) . show)
+                pure
+                (semanticEnvironmentWithStructures bindings structures)
+        tag ->
+            fail
+                ("unknown semantic environment delta tag "
+                    <> show tag)
+
+putSemanticGlobalKeyCache :: SemanticGlobalKey -> CachePut
+putSemanticGlobalKeyCache = \case
+    SemanticLeftAdjective pat -> do
+        putCacheTag 0x00
+        putPatternCache pat
+    SemanticRightAdjective pat -> do
+        putCacheTag 0x01
+        putPatternCache pat
+    SemanticFunctionPhrase singular plural -> do
+        putCacheTag 0x02
+        putPatternCache singular
+        putPatternCache plural
+    SemanticNoun singular plural -> do
+        putCacheTag 0x03
+        putPatternCache singular
+        putPatternCache plural
+    SemanticVerb singular plural -> do
+        putCacheTag 0x04
+        putPatternCache singular
+        putPatternCache plural
+    SemanticRelation token arity -> do
+        putCacheTag 0x05
+        putTokenCache token
+        putCacheNatural (parameterArityValue arity)
+    SemanticExpressionFunction pat -> do
+        putCacheTag 0x06
+        putPatternCache pat
+    SemanticPrefixPredicate command arity -> do
+        putCacheTag 0x07
+        putCacheText command
+        putCacheNatural arity
+
+getSemanticGlobalKeyCache :: CacheGet SemanticGlobalKey
+getSemanticGlobalKeyCache =
+    getCacheTag >>= \case
+        0x00 -> SemanticLeftAdjective <$> getPatternCache
+        0x01 -> SemanticRightAdjective <$> getPatternCache
+        0x02 ->
+            SemanticFunctionPhrase
+                <$> getPatternCache
+                <*> getPatternCache
+        0x03 ->
+            SemanticNoun
+                <$> getPatternCache
+                <*> getPatternCache
+        0x04 ->
+            SemanticVerb
+                <$> getPatternCache
+                <*> getPatternCache
+        0x05 ->
+            SemanticRelation
+                <$> getTokenCache
+                <*> (ParameterArity <$> getCacheNatural)
+        0x06 -> SemanticExpressionFunction <$> getPatternCache
+        0x07 ->
+            SemanticPrefixPredicate
+                <$> getCacheText
+                <*> getCacheNatural
+        tag ->
+            fail ("unknown semantic global key tag " <> show tag)
+
+putSemanticGlobalBindingCache :: SemanticGlobalBinding -> CachePut
+putSemanticGlobalBindingCache (SemanticGlobalBinding key target) = do
+    putSemanticGlobalKeyCache key
+    case target of
+        GlobalReference identity -> do
+            putCacheTag 0x00
+            putObjectIdCache identity
+        TransparentExpansion identity -> do
+            putCacheTag 0x01
+            putObjectIdCache identity
+        ContextualTransparentExpansion identity requirements -> do
+            putCacheTag 0x02
+            putObjectIdCache identity
+            putCanonicalCacheMap
+                (\(StructSymbol symbol) -> putCacheText symbol)
+                putObjectIdCache
+                requirements
+
+getSemanticGlobalBindingCache :: CacheGet SemanticGlobalBinding
+getSemanticGlobalBindingCache =
+    SemanticGlobalBinding
+        <$> getSemanticGlobalKeyCache
+        <*> (getCacheTag >>= \case
+                0x00 -> GlobalReference <$> getObjectIdCache
+                0x01 -> TransparentExpansion <$> getObjectIdCache
+                0x02 ->
+                    ContextualTransparentExpansion
+                        <$> getObjectIdCache
+                        <*> getCanonicalCacheMap
+                            (StructSymbol <$> getCacheText)
+                            getObjectIdCache
+                tag ->
+                    fail
+                        ("unknown semantic global target tag "
+                            <> show tag))
+
+putSemanticStructureDescriptorCache
+    :: SemanticStructureDescriptor
+    -> CachePut
+putSemanticStructureDescriptorCache
+        (SemanticStructureDescriptor structurePhrase predicate parents operations) = do
+    putSemanticStructurePhraseCache structurePhrase
+    putCacheMaybe putObjectIdCache predicate
+    putCacheList putSemanticStructurePhraseCache parents
+    putCacheList putSemanticStructureOperationCache operations
+
+getSemanticStructureDescriptorCache
+    :: CacheGet SemanticStructureDescriptor
+getSemanticStructureDescriptorCache = do
+    structurePhrase <- getSemanticStructurePhraseCache
+    predicate <- getCacheMaybe getObjectIdCache
+    parents <- getCacheList getSemanticStructurePhraseCache
+    operations <- getCacheList getSemanticStructureOperationCache
+    either
+        (fail . ("invalid semantic structure descriptor: " <>) . show)
+        pure
+        (semanticStructureDescriptor structurePhrase predicate parents operations)
+
+putSemanticStructurePhraseCache
+    :: SemanticStructurePhrase
+    -> CachePut
+putSemanticStructurePhraseCache
+        (SemanticStructurePhrase singular plural (Marker marker)) = do
+    putPatternCache singular
+    putPatternCache plural
+    putCacheText marker
+
+getSemanticStructurePhraseCache
+    :: CacheGet SemanticStructurePhrase
+getSemanticStructurePhraseCache =
+    SemanticStructurePhrase
+        <$> getPatternCache
+        <*> getPatternCache
+        <*> (Marker <$> getCacheText)
+
+putSemanticStructureOperationCache
+    :: SemanticStructureOperation
+    -> CachePut
+putSemanticStructureOperationCache
+        (SemanticStructureOperation (StructSymbol symbol) object) = do
+    putCacheText symbol
+    putObjectIdCache object
+
+getSemanticStructureOperationCache
+    :: CacheGet SemanticStructureOperation
+getSemanticStructureOperationCache =
+    SemanticStructureOperation
+        <$> (StructSymbol <$> getCacheText)
+        <*> getObjectIdCache
+
+putDeclarationInterfaceDeltaCache
+    :: DeclarationInterfaceDelta
+    -> CachePut
+putDeclarationInterfaceDeltaCache
+        (DeclarationInterfaceDelta
+            slot facts aliases objects propositions environment) = do
+    putDeclarationSlotCache slot
+    putCacheList putSemanticFactOccurrenceCache facts
+    putCacheList putSemanticAliasCache aliases
+    putCacheList putObjectIdCache objects
+    putCacheList putPropositionIdCache propositions
+    putSemanticEnvironmentDeltaCache environment
+
+getDeclarationInterfaceDeltaCache
+    :: CacheGet DeclarationInterfaceDelta
+getDeclarationInterfaceDeltaCache = do
+    slot <- getDeclarationSlotCache
+    facts <- getCacheList getSemanticFactOccurrenceCache
+    aliases <- getCacheList getSemanticAliasCache
+    objects <- getCacheList getObjectIdCache
+    propositions <- getCacheList getPropositionIdCache
+    environment <- getSemanticEnvironmentDeltaCache
+    either
+        (fail . ("invalid declaration interface delta: " <>) . show)
+        pure
+        (declarationInterfaceDelta
+            slot facts aliases objects propositions environment)
+
+putSemanticInterfaceCache :: SemanticInterface -> CachePut
+putSemanticInterfaceCache
+        (SemanticInterface owner direct declarations asserted) = do
+    putModuleNameCache owner
+    putCacheList putSemanticInterfaceIdCache direct
+    putCacheList putDeclarationInterfaceDeltaCache declarations
+    putSemanticInterfaceIdCache asserted
+
+getSemanticInterfaceCache :: CacheGet SemanticInterface
+getSemanticInterfaceCache = do
+    owner <- getModuleNameCache
+    direct <- getCacheList getSemanticInterfaceIdCache
+    declarations <- getCacheList getDeclarationInterfaceDeltaCache
+    asserted <- getSemanticInterfaceIdCache
+    either
+        (fail . ("invalid semantic interface: " <>) . show)
+        pure
+        (validateSemanticInterface
+            owner direct declarations asserted)
+
+putSemanticInterfaceIdCache :: SemanticInterfaceId -> CachePut
+putSemanticInterfaceIdCache (SemanticInterfaceId digest) =
+    putCacheDigest digest
+
+getSemanticInterfaceIdCache :: CacheGet SemanticInterfaceId
+getSemanticInterfaceIdCache =
+    SemanticInterfaceId <$> getCacheDigest
+
+putPrefixContextIdCache :: PrefixContextId -> CachePut
+putPrefixContextIdCache (PrefixContextId digest) =
+    putCacheDigest digest
+
+getPrefixContextIdCache :: CacheGet PrefixContextId
+getPrefixContextIdCache =
+    PrefixContextId <$> getCacheDigest
+
+putModuleArtifactKeyCache :: ModuleArtifactKey -> CachePut
+putModuleArtifactKeyCache =
+    putModuleArtifactKeyFields
+
+getModuleArtifactKeyCache :: CacheGet ModuleArtifactKey
+getModuleArtifactKeyCache = do
+    owner <- getModuleNameCache
+    parsed <- getParsedModuleIdCache
+    direct <- getCacheList getSemanticInterfaceIdCache
+    theory <- getTheoryIdCache
+    either
+        (fail . ("invalid module artifact key: " <>) . show)
+        pure
+        (moduleArtifactKey owner parsed direct theory)
+
+putModuleArtifactIdCache :: ModuleArtifactId -> CachePut
+putModuleArtifactIdCache (ModuleArtifactId digest) =
+    putCacheDigest digest
+
+getModuleArtifactIdCache :: CacheGet ModuleArtifactId
+getModuleArtifactIdCache =
+    ModuleArtifactId <$> getCacheDigest
+
+putModuleArtifactResultCache
+    :: ModuleArtifactResult
+    -> CachePut
+putModuleArtifactResultCache
+        (ModuleArtifactResult identity syntax semantic) = do
+    putModuleArtifactIdCache identity
+    putSyntaxInterfaceIdCache syntax
+    putSemanticInterfaceIdCache semantic
+
+getModuleArtifactResultCache
+    :: ModuleArtifactId
+    -> CacheGet ModuleArtifactResult
+getModuleArtifactResultCache expected = do
+    asserted <- getModuleArtifactIdCache
+    unless
+        (asserted == expected)
+        (fail "module artifact result ID mismatch")
+    ModuleArtifactResult asserted
+        <$> getSyntaxInterfaceIdCache
+        <*> getSemanticInterfaceIdCache
+
+putProofValidationRecordCache
+    :: ProofValidationRecord
+    -> CachePut
+putProofValidationRecordCache
+        (ProofValidationRecord key certificate) = do
+    putProofValidationKeyCache key
+    putValidationCertificateCache certificate
+
+getProofValidationRecordCache
+    :: CacheGet ProofValidationRecord
+getProofValidationRecordCache =
+    ProofValidationRecord
+        <$> getProofValidationKeyCache
+        <*> getValidationCertificateCache
+
+putDeclarationValidationRecordCache
+    :: DeclarationValidationRecord
+    -> CachePut
+putDeclarationValidationRecordCache
+        (DeclarationValidationRecord key certificates) = do
+    putDeclarationValidationKeyCache key
+    putCacheList putValidationCertificateCache certificates
+
+getDeclarationValidationRecordCache
+    :: CacheGet DeclarationValidationRecord
+getDeclarationValidationRecordCache =
+    DeclarationValidationRecord
+        <$> getDeclarationValidationKeyCache
+        <*> getCacheList getValidationCertificateCache
+
+
+putDeclarationSlotCache :: DeclarationSlot -> CachePut
+putDeclarationSlotCache (DeclarationSlot owner ordinal) = do
+    putModuleNameCache owner
+    putCacheNatural (localDeclarationOrdinalValue ordinal)
+
+getDeclarationSlotCache :: CacheGet DeclarationSlot
+getDeclarationSlotCache =
+    DeclarationSlot
+        <$> getModuleNameCache
+        <*> (localDeclarationOrdinal <$> getCacheNatural)
+
+putFactSlotCache :: FactSlot -> CachePut
+putFactSlotCache (FactSlot owner ordinal) = do
+    putModuleNameCache owner
+    putCacheNatural (localFactOrdinalValue ordinal)
+
+getFactSlotCache :: CacheGet FactSlot
+getFactSlotCache =
+    FactSlot
+        <$> getModuleNameCache
+        <*> (localFactOrdinal <$> getCacheNatural)
+
+putModuleNameCache :: ModuleName -> CachePut
+putModuleNameCache owner = do
+    putMathematicalDigestCache
+        (sourceNamespaceDigest
+            (moduleNameNamespace owner))
+    putCacheText
+        (Text.pack
+            (safeRelativePathFilePath
+                (moduleNameRelativePath owner)))
+
+getModuleNameCache :: CacheGet ModuleName
+getModuleNameCache = do
+    namespace <-
+        sourceNamespaceIdFromDigest
+            <$> getMathematicalDigestCache
+    rawPath <- Text.unpack <$> getCacheText
+    relative <-
+        either
+            (fail . ("invalid cache module path: " <>) . show)
+            pure
+            (safeRelativePath rawPath)
+    pure (moduleNameFromParts namespace relative)
+
+putSemanticAliasCache :: SemanticAlias -> CachePut
+putSemanticAliasCache (SemanticAlias name target) = do
+    putSemanticNameCache name
+    putSemanticFactOccurrenceFingerprintCache target
+
+getSemanticAliasCache :: CacheGet SemanticAlias
+getSemanticAliasCache =
+    SemanticAlias
+        <$> getSemanticNameCache
+        <*> getSemanticFactOccurrenceFingerprintCache
+
+putSemanticNameCache :: SemanticName -> CachePut
+putSemanticNameCache (SemanticName name) =
+    putCacheText name
+
+getSemanticNameCache :: CacheGet SemanticName
+getSemanticNameCache =
+    SemanticName <$> getCacheText
+
+putEligibility :: FactSearchEligibility -> CachePut
+putEligibility = \case
+    SearchEligible -> putCacheTag 0x00
+    SearchIneligible -> putCacheTag 0x01
+
+getEligibility :: CacheGet FactSearchEligibility
+getEligibility =
+    getCacheTag >>= \case
+        0x00 -> pure SearchEligible
+        0x01 -> pure SearchIneligible
+        tag ->
+            fail ("unknown fact-search eligibility tag " <> show tag)
+
+putModuleArtifactKeyFields :: ModuleArtifactKey -> CachePut
+putModuleArtifactKeyFields
+        (ModuleArtifactKey owner parsed direct theory) = do
+    putModuleNameCache owner
+    putParsedModuleIdCache parsed
+    putCacheList putSemanticInterfaceIdCache direct
+    putTheoryIdCache theory
+
+putProofValidationKeyCache :: ProofValidationKey -> CachePut
+putProofValidationKeyCache (ProofValidationKey digest) =
+    putCacheDigest digest
+
+getProofValidationKeyCache :: CacheGet ProofValidationKey
+getProofValidationKeyCache =
+    ProofValidationKey <$> getCacheDigest
+
+putDeclarationValidationKeyCache
+    :: DeclarationValidationKey
+    -> CachePut
+putDeclarationValidationKeyCache
+        (DeclarationValidationKey digest) =
+    putCacheDigest digest
+
+getDeclarationValidationKeyCache
+    :: CacheGet DeclarationValidationKey
+getDeclarationValidationKeyCache =
+    DeclarationValidationKey <$> getCacheDigest
+
+firstDuplicate :: Ord value => [value] -> Maybe value
+firstDuplicate =
+    go Set.empty
+  where
+    go _ [] =
+        Nothing
+    go seen (value : rest)
+        | value `Set.member` seen =
+            Just value
+        | otherwise =
+            go (Set.insert value seen) rest
+
+rejectDuplicate
+    :: Ord value
+    => (value -> error)
+    -> [value]
+    -> Either error ()
+rejectDuplicate makeError values =
+    maybe
+        (Right ())
+        (Left . makeError)
+        (firstDuplicate values)
+
+strictlyIncreasing :: Ord value => [value] -> Bool
+strictlyIncreasing values =
+    and
+        (zipWith (<) values (drop 1 values))