Define semantic interface identities

5 files changed, 1475 insertions, 0 deletions

diff --git a/source/Checking/Semantic.hs b/source/Checking/Semantic.hs
new file mode 100644
index 0000000..0c9eb4d
--- /dev/null
+++ b/source/Checking/Semantic.hs
@@ -0,0 +1,1093 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Canonical semantic declaration, prefix, interface, and validation keys.
+module Checking.Semantic
+    ( DeclarationSlot
+    , declarationSlot
+    , declarationSlotModule
+    , declarationSlotOrdinal
+    , FactSlot
+    , factSlot
+    , factSlotModule
+    , factSlotOrdinal
+    , SemanticName
+    , semanticName
+    , semanticNameText
+    , FactSearchEligibility(..)
+    , SemanticFactOccurrence
+    , semanticFactOccurrence
+    , semanticFactSlot
+    , semanticFactProposition
+    , semanticFactAuthority
+    , semanticFactSearchEligibility
+    , SemanticFactOccurrenceFingerprint
+    , semanticFactOccurrenceFingerprint
+    , semanticFactFingerprintDigest
+    , SemanticAlias
+    , semanticAlias
+    , semanticAliasName
+    , semanticAliasTarget
+    , SemanticEnvironmentMutation(..)
+    , SemanticEnvironmentDelta
+    , semanticEnvironmentDelta
+    , semanticEnvironmentMutations
+    , SemanticEnvironmentError(..)
+    , DeclarationInterfaceDelta
+    , declarationInterfaceDelta
+    , declarationDeltaSlot
+    , declarationDeltaFacts
+    , declarationDeltaAliases
+    , declarationDeltaObjects
+    , declarationDeltaPropositions
+    , declarationDeltaEnvironment
+    , DeclarationInterfaceError(..)
+    , SemanticInterfaceId
+    , semanticInterfaceIdDigest
+    , SemanticInterface
+    , semanticInterface
+    , semanticInterfaceOwner
+    , semanticInterfaceDirectInputs
+    , semanticInterfaceDeclarations
+    , semanticInterfaceAssertedId
+    , SemanticInterfaceError(..)
+    , PrefixContextId
+    , initialPrefixContextId
+    , nextPrefixContextId
+    , prefixContextIdDigest
+    , ProofSyntaxId
+    , proofSyntaxId
+    , DeclarationSyntaxId
+    , declarationSyntaxId
+    , ProofValidationKey
+    , proofValidationKey
+    , proofValidationKeyDigest
+    , DeclarationValidationKey
+    , declarationValidationKey
+    , declarationValidationKeyDigest
+    , ModuleArtifactKey
+    , moduleArtifactKey
+    , ModuleArtifactId
+    , moduleArtifactId
+    , moduleArtifactIdDigest
+    , SealedModuleResult
+    , sealedModuleResult
+    , sealedModuleSyntax
+    , sealedModuleSemantic
+    , ModuleArtifactResult
+    , moduleArtifactResult
+    , moduleArtifactResultId
+    , moduleArtifactResultSyntax
+    , moduleArtifactResultSemantic
+    , putSemanticFactOccurrenceFingerprintCache
+    , getSemanticFactOccurrenceFingerprintCache
+    , putSemanticFactOccurrenceCache
+    , getSemanticFactOccurrenceCache
+    , putSemanticEnvironmentDeltaCache
+    , getSemanticEnvironmentDeltaCache
+    , putDeclarationInterfaceDeltaCache
+    , getDeclarationInterfaceDeltaCache
+    , putSemanticInterfaceCache
+    , getSemanticInterfaceCache
+    , putSemanticInterfaceIdCache
+    , getSemanticInterfaceIdCache
+    , putPrefixContextIdCache
+    , getPrefixContextIdCache
+    ) where
+
+import Base
+import Checking.Authority
+import Checking.Core
+import Checking.Identity
+import Felix.Cache.Codec
+import Felix.Math.Codec
+import Felix.Module
+import Felix.Parsed.Identity
+import Felix.Source
+import Syntax.Interface
+
+import Control.DeepSeq (NFData)
+import Control.Monad (unless)
+import Data.ByteString (ByteString)
+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
+    !PropositionId
+    !FactAuthority
+    !FactSearchEligibility
+    !SemanticFactOccurrenceFingerprint
+    deriving stock (Show, Eq, Ord, Generic)
+
+semanticFactOccurrence
+    :: FactSlot
+    -> PropositionId
+    -> FactAuthority
+    -> FactSearchEligibility
+    -> SemanticFactOccurrence
+semanticFactOccurrence slot proposition authority eligibility =
+    SemanticFactOccurrence
+        slot
+        proposition
+        authority
+        eligibility
+        (semanticFactOccurrenceFingerprint slot authority)
+
+semanticFactSlot :: SemanticFactOccurrence -> FactSlot
+semanticFactSlot
+        (SemanticFactOccurrence slot _ _ _ _) =
+    slot
+
+semanticFactProposition
+    :: SemanticFactOccurrence
+    -> PropositionId
+semanticFactProposition
+        (SemanticFactOccurrence _ proposition _ _ _) =
+    proposition
+
+semanticFactAuthority
+    :: SemanticFactOccurrence
+    -> FactAuthority
+semanticFactAuthority
+        (SemanticFactOccurrence _ _ authority _ _) =
+    authority
+
+semanticFactSearchEligibility
+    :: SemanticFactOccurrence
+    -> FactSearchEligibility
+semanticFactSearchEligibility
+        (SemanticFactOccurrence _ _ _ eligibility _) =
+    eligibility
+
+semanticFactFingerprint
+    :: SemanticFactOccurrence
+    -> SemanticFactOccurrenceFingerprint
+semanticFactFingerprint
+        (SemanticFactOccurrence _ _ _ _ fingerprint) =
+    fingerprint
+
+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
+
+
+-- | The closed Phase 1 mutation inventory. Content payload rows remain
+-- separate; these cases record only later-visible environment changes.
+data SemanticEnvironmentMutation
+    = AddAbbreviation
+        !SemanticName
+        !CoreType
+        !(CanonicalTerm ObjectId)
+    | AddPredicateDefinition
+        !SemanticName
+        !(CanonicalTerm ObjectId)
+    | AddSymbolDependency
+        !ObjectId
+        !ObjectId
+    | ClaimSymbolOwnership
+        !SemanticName
+        !ObjectId
+    | FreezeSymbol
+        !ObjectId
+    | AddStructureEdge
+        !ObjectId
+        !ObjectId
+    | ReserveDeclarationName
+        !SemanticName
+    | BindGlobalObject
+        !SemanticName
+        !ObjectId
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+newtype SemanticEnvironmentDelta =
+    SemanticEnvironmentDelta [SemanticEnvironmentMutation]
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+data SemanticEnvironmentError
+    = DuplicateSemanticEnvironmentMutation
+        !SemanticEnvironmentMutation
+    deriving stock (Show, Eq)
+
+semanticEnvironmentDelta
+    :: [SemanticEnvironmentMutation]
+    -> Either SemanticEnvironmentError SemanticEnvironmentDelta
+semanticEnvironmentDelta mutations =
+    case firstDuplicate mutations of
+        Nothing ->
+            Right (SemanticEnvironmentDelta mutations)
+        Just duplicate ->
+            Left
+                (DuplicateSemanticEnvironmentMutation duplicate)
+
+semanticEnvironmentMutations
+    :: SemanticEnvironmentDelta
+    -> [SemanticEnvironmentMutation]
+semanticEnvironmentMutations
+        (SemanticEnvironmentDelta mutations) =
+    mutations
+
+
+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
+    | DeclarationFactTheoremMismatch
+        !PropositionId
+        !TheoremRef
+    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
+            reference =
+                factAuthorityTheorem
+                    (semanticFactAuthority occurrence)
+        unless
+            (proposition `Set.member` propositionSet)
+            (Left (DeclarationFactPropositionMissing proposition))
+        unless
+            (theoremRefProposition reference == proposition)
+            (Left
+                (DeclarationFactTheoremMismatch
+                    proposition reference))
+
+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
+    | SemanticInterfaceIdMismatch
+        !SemanticInterfaceId
+        !SemanticInterfaceId
+    deriving stock (Show, Eq)
+
+semanticInterface
+    :: ModuleName
+    -> [SemanticInterfaceId]
+    -> [DeclarationInterfaceDelta]
+    -> Either SemanticInterfaceError SemanticInterface
+semanticInterface owner direct declarations =
+    validateSemanticInterface
+        owner
+        direct
+        declarations
+        (computeSemanticInterfaceId
+            owner direct declarations)
+
+validateSemanticInterface
+    :: ModuleName
+    -> [SemanticInterfaceId]
+    -> [DeclarationInterfaceDelta]
+    -> SemanticInterfaceId
+    -> Either SemanticInterfaceError SemanticInterface
+validateSemanticInterface owner direct declarations asserted = do
+    rejectDuplicate
+        DuplicateDirectSemanticInterface
+        direct
+    traverse_
+        (\delta ->
+            unless
+                (declarationSlotModule
+                    (declarationDeltaSlot delta)
+                    == owner)
+                (Left
+                    (SemanticDeclarationOwnerMismatch
+                        (declarationDeltaSlot delta))))
+        declarations
+    unless
+        (strictlyIncreasing
+            ( localDeclarationOrdinalValue
+                . declarationSlotOrdinal
+                . declarationDeltaSlot
+                <$> declarations))
+        (Left NonIncreasingDeclarationSlots)
+    let computed =
+            computeSemanticInterfaceId
+                owner direct declarations
+    unless
+        (asserted == computed)
+        (Left
+            (SemanticInterfaceIdMismatch asserted computed))
+    pure
+        (SemanticInterface
+            owner direct declarations asserted)
+
+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)
+
+initialPrefixContextId
+    :: TheoryId
+    -> ModuleName
+    -> [SemanticInterfaceId]
+    -> PrefixContextId
+initialPrefixContextId theory owner direct =
+    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
+
+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 ModuleArtifactKey = ModuleArtifactKey
+    !ModuleName
+    !ParsedModuleId
+    ![SemanticInterfaceId]
+    !TheoryId
+    deriving stock (Show, Eq, Ord)
+
+moduleArtifactKey
+    :: ModuleName
+    -> ParsedModuleId
+    -> [SemanticInterfaceId]
+    -> TheoryId
+    -> ModuleArtifactKey
+moduleArtifactKey =
+    ModuleArtifactKey
+
+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 SealedModuleResult = SealedModuleResult
+    !SyntaxInterfaceId
+    !SemanticInterfaceId
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+sealedModuleResult
+    :: SyntaxInterfaceId
+    -> SemanticInterfaceId
+    -> SealedModuleResult
+sealedModuleResult =
+    SealedModuleResult
+
+sealedModuleSyntax
+    :: SealedModuleResult
+    -> SyntaxInterfaceId
+sealedModuleSyntax (SealedModuleResult syntax _) =
+    syntax
+
+sealedModuleSemantic
+    :: SealedModuleResult
+    -> SemanticInterfaceId
+sealedModuleSemantic (SealedModuleResult _ semantic) =
+    semantic
+
+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 proposition authority eligibility fingerprint) = do
+    putFactSlotCache slot
+    putPropositionIdCache proposition
+    putFactAuthorityCache authority
+    putEligibility eligibility
+    putSemanticFactOccurrenceFingerprintCache fingerprint
+
+getSemanticFactOccurrenceCache
+    :: CacheGet SemanticFactOccurrence
+getSemanticFactOccurrenceCache = do
+    slot <- getFactSlotCache
+    proposition <- getPropositionIdCache
+    authority <- getFactAuthorityCache
+    eligibility <- getEligibility
+    asserted <- getSemanticFactOccurrenceFingerprintCache
+    let occurrence =
+            semanticFactOccurrence
+                slot proposition authority eligibility
+    unless
+        (semanticFactFingerprint occurrence == asserted)
+        (fail "cache semantic fact fingerprint mismatch")
+    pure occurrence
+
+putSemanticEnvironmentDeltaCache
+    :: SemanticEnvironmentDelta
+    -> CachePut
+putSemanticEnvironmentDeltaCache
+        (SemanticEnvironmentDelta mutations) =
+    putCacheList putEnvironmentMutation mutations
+
+getSemanticEnvironmentDeltaCache
+    :: CacheGet SemanticEnvironmentDelta
+getSemanticEnvironmentDeltaCache = do
+    mutations <- getCacheList getEnvironmentMutation
+    either
+        (fail . ("invalid semantic environment delta: " <>) . show)
+        pure
+        (semanticEnvironmentDelta mutations)
+
+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
+
+
+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)
+
+putEnvironmentMutation
+    :: SemanticEnvironmentMutation
+    -> CachePut
+putEnvironmentMutation = \case
+    AddAbbreviation name coreType body -> do
+        putCacheTag 0x00
+        putSemanticNameCache name
+        putCoreTypeCache coreType
+        putCanonicalTermCache putObjectIdCache body
+    AddPredicateDefinition name body -> do
+        putCacheTag 0x01
+        putSemanticNameCache name
+        putCanonicalTermCache putObjectIdCache body
+    AddSymbolDependency dependent dependency -> do
+        putCacheTag 0x02
+        putObjectIdCache dependent
+        putObjectIdCache dependency
+    ClaimSymbolOwnership name identity -> do
+        putCacheTag 0x03
+        putSemanticNameCache name
+        putObjectIdCache identity
+    FreezeSymbol identity -> do
+        putCacheTag 0x04
+        putObjectIdCache identity
+    AddStructureEdge child parent -> do
+        putCacheTag 0x05
+        putObjectIdCache child
+        putObjectIdCache parent
+    ReserveDeclarationName name -> do
+        putCacheTag 0x06
+        putSemanticNameCache name
+    BindGlobalObject name identity -> do
+        putCacheTag 0x07
+        putSemanticNameCache name
+        putObjectIdCache identity
+
+getEnvironmentMutation :: CacheGet SemanticEnvironmentMutation
+getEnvironmentMutation =
+    getCacheTag >>= \case
+        0x00 ->
+            AddAbbreviation
+                <$> getSemanticNameCache
+                <*> getCoreTypeCache
+                <*> getCanonicalTermCache getObjectIdCache
+        0x01 ->
+            AddPredicateDefinition
+                <$> getSemanticNameCache
+                <*> getCanonicalTermCache getObjectIdCache
+        0x02 ->
+            AddSymbolDependency
+                <$> getObjectIdCache
+                <*> getObjectIdCache
+        0x03 ->
+            ClaimSymbolOwnership
+                <$> getSemanticNameCache
+                <*> getObjectIdCache
+        0x04 ->
+            FreezeSymbol <$> getObjectIdCache
+        0x05 ->
+            AddStructureEdge
+                <$> getObjectIdCache
+                <*> getObjectIdCache
+        0x06 ->
+            ReserveDeclarationName <$> getSemanticNameCache
+        0x07 ->
+            BindGlobalObject
+                <$> getSemanticNameCache
+                <*> getObjectIdCache
+        tag ->
+            fail ("unknown semantic environment mutation tag " <> show tag)
+
+putModuleArtifactKeyCache :: ModuleArtifactKey -> CachePut
+putModuleArtifactKeyCache
+        (ModuleArtifactKey owner parsed direct theory) = do
+    putModuleNameCache owner
+    putParsedModuleIdCache parsed
+    putCacheList putSemanticInterfaceIdCache direct
+    putTheoryIdCache theory
+
+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))
diff --git a/source/Felix/Parsed/Identity.hs b/source/Felix/Parsed/Identity.hs
new file mode 100644
index 0000000..0a73e5a
--- /dev/null
+++ b/source/Felix/Parsed/Identity.hs
@@ -0,0 +1,89 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Owner-independent parsed artifact identities.
+module Felix.Parsed.Identity
+    ( ParsedModuleKey
+    , parsedModuleKey
+    , parsedModuleKeyDigest
+    , ParsedModuleId
+    , parsedModuleId
+    , parsedModuleIdDigest
+    , putParsedModuleKeyCache
+    , getParsedModuleKeyCache
+    , putParsedModuleIdCache
+    , getParsedModuleIdCache
+    ) where
+
+import Base
+import Felix.Cache.Codec
+import Felix.Source.Content
+import Syntax.Interface
+
+import Control.DeepSeq (NFData)
+import Data.ByteString (ByteString)
+
+
+newtype ParsedModuleKey =
+    ParsedModuleKey CacheDigest
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+parsedModuleKey
+    :: SourceContentId
+    -> BaseSyntaxInterfaceId
+    -> [SyntaxInterfaceId]
+    -> ParsedModuleKey
+parsedModuleKey sourceContent base direct =
+    ParsedModuleKey
+        (hashCacheFields
+            "felix-parsed-module-key-v1"
+            [ encodeCache
+                (putSourceContentIdCache sourceContent)
+            , encodeCache
+                (putBaseSyntaxInterfaceIdCache base)
+            , encodeCache
+                (putCacheList
+                    putSyntaxInterfaceIdCache
+                    direct)
+            ])
+
+parsedModuleKeyDigest :: ParsedModuleKey -> CacheDigest
+parsedModuleKeyDigest (ParsedModuleKey digest) =
+    digest
+
+newtype ParsedModuleId =
+    ParsedModuleId CacheDigest
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+-- | The payload is the complete canonical owner-independent parsed value.
+parsedModuleId :: ParsedModuleKey -> ByteString -> ParsedModuleId
+parsedModuleId key payload =
+    ParsedModuleId
+        (hashCacheFields
+            "felix-parsed-module-v1"
+            [ encodeCache (putParsedModuleKeyCache key)
+            , payload
+            ])
+
+parsedModuleIdDigest :: ParsedModuleId -> CacheDigest
+parsedModuleIdDigest (ParsedModuleId digest) =
+    digest
+
+putParsedModuleKeyCache :: ParsedModuleKey -> CachePut
+putParsedModuleKeyCache (ParsedModuleKey digest) =
+    putCacheDigest digest
+
+getParsedModuleKeyCache :: CacheGet ParsedModuleKey
+getParsedModuleKeyCache =
+    ParsedModuleKey <$> getCacheDigest
+
+putParsedModuleIdCache :: ParsedModuleId -> CachePut
+putParsedModuleIdCache (ParsedModuleId digest) =
+    putCacheDigest digest
+
+getParsedModuleIdCache :: CacheGet ParsedModuleId
+getParsedModuleIdCache =
+    ParsedModuleId <$> getCacheDigest
diff --git a/source/Syntax/Interface.hs b/source/Syntax/Interface.hs
index c66cc7d..bb2c4f3 100644
--- a/source/Syntax/Interface.hs
+++ b/source/Syntax/Interface.hs
@@ -42,6 +42,10 @@ module Syntax.Interface
     , getCanonicalSyntaxDeltaCache
     , putModuleSyntaxInterfaceCache
     , getModuleSyntaxInterfaceCache
+    , putBaseSyntaxInterfaceIdCache
+    , getBaseSyntaxInterfaceIdCache
+    , putSyntaxInterfaceIdCache
+    , getSyntaxInterfaceIdCache
     ) where
 
 import Base
diff --git a/source/Test/Unit.hs b/source/Test/Unit.hs
index d21cde1..2e73f79 100644
--- a/source/Test/Unit.hs
+++ b/source/Test/Unit.hs
@@ -20,6 +20,7 @@ import Test.Unit.Lexicon qualified as Lexicon
 import Test.Unit.Meaning qualified as Meaning
 import Test.Unit.Migration qualified as Migration
 import Test.Unit.Provers qualified as Provers
+import Test.Unit.Semantic qualified as Semantic
 import Test.Unit.Source qualified as Source
 import Test.Unit.Symdiff qualified as Symdiff
 import Test.Unit.Token qualified as Token
@@ -44,6 +45,7 @@ unitTests = testGroup "unit tests"
     , Meaning.unitTests
     , Migration.unitTests
     , Provers.unitTests
+    , Semantic.unitTests
     , Source.unitTests
     , Token.unitTests
     ]
diff --git a/source/Test/Unit/Semantic.hs b/source/Test/Unit/Semantic.hs
new file mode 100644
index 0000000..2ab59e3
--- /dev/null
+++ b/source/Test/Unit/Semantic.hs
@@ -0,0 +1,287 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module Test.Unit.Semantic (unitTests) where
+
+import Base
+import Checking.Authority qualified as Authority
+import Checking.Core qualified as Core
+import Checking.Foundation qualified as Foundation
+import Checking.Identity qualified as Identity
+import Checking.Semantic qualified as Semantic
+import Felix.Cache.Codec
+import Felix.Math.Codec
+import Felix.Module
+import Felix.Parsed.Identity
+import Felix.Source
+import Felix.Source.Content
+import Syntax.Interface qualified as Syntax
+
+import Data.ByteString (ByteString)
+import Test.Tasty
+import Test.Tasty.HUnit
+
+
+unitTests :: TestTree
+unitTests =
+    testGroup "Semantic interfaces"
+        [ testCase "separates syntax and semantic Merkle identities"
+            separatesSyntaxAndSemantics
+        , testCase "round-trips closed semantic declaration state"
+            roundTripsSemanticState
+        , testCase "keys exact proof and module inputs"
+            keysExactInputs
+        ]
+
+separatesSyntaxAndSemantics :: Assertion
+separatesSyntaxAndSemantics = do
+    fixture <- makeFixture
+    firstSyntax <- makeSyntax "first"
+    secondSyntax <- makeSyntax "second"
+    assertBool
+        "notation changes syntax identity"
+        ( Syntax.moduleSyntaxAssertedId firstSyntax
+            /= Syntax.moduleSyntaxAssertedId secondSyntax
+        )
+    let semantic = fixtureInterface fixture
+        firstSealed =
+            Semantic.sealedModuleResult
+                (Syntax.moduleSyntaxAssertedId firstSyntax)
+                (Semantic.semanticInterfaceAssertedId semantic)
+        secondSealed =
+            Semantic.sealedModuleResult
+                (Syntax.moduleSyntaxAssertedId secondSyntax)
+                (Semantic.semanticInterfaceAssertedId semantic)
+    assertEqual
+        "notation does not enter semantic interface identity"
+        (Semantic.sealedModuleSemantic firstSealed)
+        (Semantic.sealedModuleSemantic secondSealed)
+    assertEqual
+        "notation does not enter semantic prefix identity"
+        (fixtureNextPrefix fixture)
+        (Semantic.nextPrefixContextId
+            (fixtureInitialPrefix fixture)
+            (fixtureDelta fixture))
+
+roundTripsSemanticState :: Assertion
+roundTripsSemanticState = do
+    fixture <- makeFixture
+    assertEqual
+        "semantic interface cache round trip"
+        (Right (fixtureInterface fixture))
+        (decodeCache
+            Semantic.getSemanticInterfaceCache
+            (encodeCache
+                (Semantic.putSemanticInterfaceCache
+                    (fixtureInterface fixture))))
+    assertEqual
+        "duplicate explicit environment mutation"
+        (Left
+            (Semantic.DuplicateSemanticEnvironmentMutation
+                (Semantic.ReserveDeclarationName
+                    (Semantic.semanticName "theorem"))))
+        (Semantic.semanticEnvironmentDelta
+            [ Semantic.ReserveDeclarationName
+                (Semantic.semanticName "theorem")
+            , Semantic.ReserveDeclarationName
+                (Semantic.semanticName "theorem")
+            ])
+    let object = fixtureObject fixture
+        name = Semantic.semanticName "entry"
+        mutations =
+            [ Semantic.AddAbbreviation
+                name Core.TyProp Core.CFalsum
+            , Semantic.AddPredicateDefinition
+                name Core.CFalsum
+            , Semantic.AddSymbolDependency object object
+            , Semantic.ClaimSymbolOwnership name object
+            , Semantic.FreezeSymbol object
+            , Semantic.AddStructureEdge object object
+            , Semantic.ReserveDeclarationName name
+            , Semantic.BindGlobalObject name object
+            ]
+    completeEnvironment <- expectRight
+        (Semantic.semanticEnvironmentDelta mutations)
+    assertEqual
+        "every closed environment mutation round trips"
+        (Right completeEnvironment)
+        (decodeCache
+            Semantic.getSemanticEnvironmentDeltaCache
+            (encodeCache
+                (Semantic.putSemanticEnvironmentDeltaCache
+                    completeEnvironment)))
+
+keysExactInputs :: Assertion
+keysExactInputs = do
+    fixture <- makeFixture
+    let theorem =
+            Identity.theoremId
+                (fixtureTheorem fixture)
+        firstProof =
+            Semantic.proofValidationKey
+                theorem
+                (Semantic.proofSyntaxId "proof-a")
+                (fixtureInitialPrefix fixture)
+        secondProof =
+            Semantic.proofValidationKey
+                theorem
+                (Semantic.proofSyntaxId "proof-b")
+                (fixtureInitialPrefix fixture)
+        laterContext =
+            Semantic.proofValidationKey
+                theorem
+                (Semantic.proofSyntaxId "proof-a")
+                (fixtureNextPrefix fixture)
+    assertBool
+        "proof syntax is an exact validation input"
+        (firstProof /= secondProof)
+    assertBool
+        "semantic predecessor is an exact validation input"
+        (firstProof /= laterContext)
+    let firstParsedKey =
+            parsedModuleKey
+                (fixtureSourceContentId "source-a")
+                Syntax.baseSyntaxInterfaceId
+                []
+        secondParsedKey =
+            parsedModuleKey
+                (fixtureSourceContentId "source-b")
+                Syntax.baseSyntaxInterfaceId
+                []
+        firstParsed =
+            parsedModuleId firstParsedKey "parsed"
+        secondParsed =
+            parsedModuleId secondParsedKey "parsed"
+        firstArtifact =
+            Semantic.moduleArtifactId
+                (Semantic.moduleArtifactKey
+                    (fixtureOwner fixture)
+                    firstParsed
+                    []
+                    (fixtureTheory fixture))
+        secondArtifact =
+            Semantic.moduleArtifactId
+                (Semantic.moduleArtifactKey
+                    (fixtureOwner fixture)
+                    secondParsed
+                    []
+                    (fixtureTheory fixture))
+    assertBool
+        "module artifact binds parsed source identity"
+        (firstArtifact /= secondArtifact)
+
+
+data Fixture = Fixture
+    { fixtureTheory :: !Identity.TheoryId
+    , fixtureOwner :: !ModuleName
+    , fixtureObject :: !Identity.ObjectId
+    , fixtureTheorem :: !Identity.TheoremRef
+    , fixtureDelta :: !Semantic.DeclarationInterfaceDelta
+    , fixtureInterface :: !Semantic.SemanticInterface
+    , fixtureInitialPrefix :: !Semantic.PrefixContextId
+    , fixtureNextPrefix :: !Semantic.PrefixContextId
+    }
+
+makeFixture :: IO Fixture
+makeFixture = do
+    foundation <- expectRight Foundation.checkedFoundation
+    namespaceDigest <- expectRight
+        (hashCanonicalFields
+            "semantic-test-namespace"
+            ["root"])
+    relative <- expectRight (safeRelativePath "module.tex")
+    closure <- expectRight
+        (Identity.validateObjectClosure
+            (Identity.theoryId foundation)
+            [])
+    proposition <- expectRight
+        (Identity.validatePropositionContent
+            closure
+            Core.CFalsum)
+    environment <- expectRight
+        (Semantic.semanticEnvironmentDelta
+            [ Semantic.ReserveDeclarationName
+                (Semantic.semanticName "theorem")
+            ])
+    let theory =
+            Identity.theoryId foundation
+        object =
+            Identity.intrinsicObjectId
+                theory Core.Empty Core.TySet
+        owner =
+            moduleNameFromParts
+                (sourceNamespaceIdFromDigest namespaceDigest)
+                relative
+        reference =
+            Identity.theoremRef
+                theory
+                (Identity.checkedPropositionId proposition)
+        authority =
+            Authority.factAuthority
+                reference
+                Authority.cleanAuthoritySafety
+        occurrence =
+            Semantic.semanticFactOccurrence
+                (Semantic.factSlot owner (localFactOrdinal 0))
+                (Identity.checkedPropositionId proposition)
+                authority
+                Semantic.SearchEligible
+        slot =
+            Semantic.declarationSlot
+                owner
+                (localDeclarationOrdinal 0)
+    delta <- expectRight
+        (Semantic.declarationInterfaceDelta
+            slot
+            [occurrence]
+            [ Semantic.semanticAlias
+                (Semantic.semanticName "theorem")
+                (Semantic.semanticFactOccurrenceFingerprint
+                    (Semantic.factSlot owner (localFactOrdinal 0))
+                    authority)
+            ]
+            []
+            [Identity.checkedPropositionId proposition]
+            environment)
+    interface <- expectRight
+        (Semantic.semanticInterface owner [] [delta])
+    let initial =
+            Semantic.initialPrefixContextId theory owner []
+    pure
+        Fixture
+            { fixtureTheory = theory
+            , fixtureOwner = owner
+            , fixtureObject = object
+            , fixtureTheorem = reference
+            , fixtureDelta = delta
+            , fixtureInterface = interface
+            , fixtureInitialPrefix = initial
+            , fixtureNextPrefix =
+                Semantic.nextPrefixContextId initial delta
+            }
+
+makeSyntax :: Text -> IO Syntax.ModuleSyntaxInterface
+makeSyntax command = do
+    delta <- expectRight
+        (Syntax.canonicalSyntaxDelta
+            [Syntax.CanonicalStructureOperation command])
+    expectRight (Syntax.moduleSyntaxInterface [] delta)
+
+fixtureSourceContentId :: ByteString -> SourceContentId
+fixtureSourceContentId bytes =
+    either
+        (impossible . show)
+        id
+        (decodeCache
+            getSourceContentIdCache
+            (encodeCache
+                (putCacheDigest
+                    (hashCacheFields
+                        "semantic-test-source"
+                        [bytes]))))
+
+expectRight :: Show error => Either error value -> IO value
+expectRight = \case
+    Left err ->
+        assertFailure (show err) >> fail "unreachable"
+    Right value ->
+        pure value