Define semantic interface identities

1 files changed, 1093 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))