Migrate to `Felix` namespaceHEADhotg

1 files changed, 1266 insertions, 0 deletions

diff --git a/source/Felix/Checking/FinalPrelude.hs b/source/Felix/Checking/FinalPrelude.hs
new file mode 100644
index 0000000..9cc43f4
--- /dev/null
+++ b/source/Felix/Checking/FinalPrelude.hs
@@ -0,0 +1,1266 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE RankNTypes #-}
+
+-- | Authority-confined construction of the inert final-prelude candidate.
+module Felix.Checking.FinalPrelude
+    ( FinalPreludeCandidate
+    , finalPreludeParsed
+    , finalPreludeSyntax
+    , finalPreludeSemantic
+    , finalPreludePrefix
+    , finalPreludeObjects
+    , PreludePublicRole(..)
+    , expectedFinalPreludePublicRoles
+    , FinalPreludeRoleTarget(..)
+    , finalPreludePublicRole
+    , FinalPreludeValidationError(..)
+    , FinalPreludeFailure(..)
+    , FinalPreludeBuildResult(..)
+    , buildFinalPreludeCandidate
+    , buildParsedFinalPreludeCandidate
+    , validateOmegaFactInventory
+    ) where
+
+import Base hiding (Empty)
+import Felix.Checking.Authority qualified as Authority
+import Felix.Checking.Core
+import Felix.Checking.Declaration qualified as Declaration
+import Felix.Checking.Exact qualified as Exact
+import Felix.Checking.Exact.Proof qualified as ExactProof
+import Felix.Checking.Foundation
+import Felix.Checking.Identity
+import Felix.Checking.SetConstruction
+import Felix.Checking.Semantic
+import Felix.Checking.Semantic qualified as Semantic
+import Felix.Module
+import Felix.Cache.Codec (CacheDigest)
+import Felix.Parse
+import Felix.Prelude qualified as Prelude
+import Felix.Source (ImportRef)
+import Felix.Report.Location
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Interface
+import Felix.Syntax.Lexicon qualified as Lexicon
+
+import Control.Monad (unless)
+import Data.Bifunctor (first)
+import Data.List qualified as List
+import Data.Map.Strict qualified as Map
+import Data.Set qualified as Set
+
+
+data FinalPreludeCandidate = FinalPreludeCandidate
+    !Prelude.ReservedParsedPrelude
+    !ModuleSyntaxInterface
+    !SemanticInterface
+    !Declaration.PendingModulePrefix
+    !CheckedObjectClosure
+    !(Map.Map PreludePublicRole FinalPreludeRoleTarget)
+
+finalPreludeParsed
+    :: FinalPreludeCandidate
+    -> Prelude.ReservedParsedPrelude
+finalPreludeParsed
+        (FinalPreludeCandidate parsed _syntax _semantic _prefix _objects
+            _roles) =
+    parsed
+
+finalPreludeSyntax
+    :: FinalPreludeCandidate
+    -> ModuleSyntaxInterface
+finalPreludeSyntax
+        (FinalPreludeCandidate _parsed syntax _semantic _prefix _objects
+            _roles) =
+    syntax
+
+finalPreludeSemantic
+    :: FinalPreludeCandidate
+    -> SemanticInterface
+finalPreludeSemantic
+        (FinalPreludeCandidate _parsed _syntax semantic _prefix _objects
+            _roles) =
+    semantic
+
+finalPreludePrefix
+    :: FinalPreludeCandidate
+    -> Declaration.PendingModulePrefix
+finalPreludePrefix
+        (FinalPreludeCandidate _parsed _syntax _semantic prefix _objects
+            _roles) =
+    prefix
+
+finalPreludeObjects
+    :: FinalPreludeCandidate
+    -> CheckedObjectClosure
+finalPreludeObjects
+        (FinalPreludeCandidate _parsed _syntax _semantic _prefix objects
+            _roles) =
+    objects
+
+data FinalPreludeRoleTarget
+    = FinalPreludeObjectRole !ObjectId
+    | FinalPreludeTheoremRole !TheoremRef
+    deriving stock (Show, Eq, Ord)
+
+-- | Stable public roles exported by the packaged final prelude.
+data PreludePublicRole
+    = PreludeInfinityTheorem
+    | PreludeOmegaObject
+    | PreludeOmegaDefiningEquation
+    | PreludeNaturalsAlias
+    | PreludeNaturalsInductiveTheorem
+    | PreludeNaturalsMinimalTheorem
+    deriving stock (Show, Eq, Ord, Enum, Bounded)
+
+expectedFinalPreludePublicRoles :: Set PreludePublicRole
+expectedFinalPreludePublicRoles =
+    Set.fromList [minBound .. maxBound]
+
+finalPreludePublicRole
+    :: FinalPreludeCandidate
+    -> PreludePublicRole
+    -> Maybe FinalPreludeRoleTarget
+finalPreludePublicRole
+        (FinalPreludeCandidate _parsed _syntax _semantic _prefix _objects
+            roles) role =
+    Map.lookup role roles
+
+data FinalPreludeValidationError
+    = FinalPreludePackagedInputMismatch
+    | FinalPreludeSemanticEnvironmentMismatch
+    | FinalPreludeDeclarationAssociationMismatch
+    | FinalPreludeUnexpectedObject !ObjectId
+    | FinalPreludeDeclarationMissing !Text
+    | FinalPreludeDeclarationDuplicate !Text
+    | FinalPreludeDeclarationShapeMismatch !Text
+    | FinalPreludeDefinitionContentMismatch !Text
+    | FinalPreludeFactContentMismatch !Text
+    | FinalPreludeValidationInventoryMismatch !DeclarationSlot
+    | FinalPreludeAuthorityMismatch !DeclarationSlot
+    | FinalPreludeBaseStructureMismatch
+    | FinalPreludePublicRoleMismatch !PreludePublicRole
+    deriving stock (Show, Eq)
+
+data FinalPreludeFailure
+    = FinalPreludeWrongOwner !ModuleName
+    | FinalPreludeHasImports ![ImportRef]
+    | FinalPreludeHasSyntaxImports ![SyntaxInterfaceId]
+    | FinalPreludeUnsupportedBlock !Location
+    | FinalPreludeUnmatchedProof !Location
+    | FinalPreludeExactDeclarationFailed !Exact.ExactCompileError
+    | FinalPreludeExactProofFailed !ExactProof.ExactProofError
+    | FinalPreludeOmittedProof !Location
+    | FinalPreludeDeclarationFailed !Declaration.DeclarationError
+    | FinalPreludeSealFailed !SemanticInterfaceError
+    | FinalPreludeValidationFailed !FinalPreludeValidationError
+    deriving stock (Show, Eq)
+
+data FinalPreludeBuildResult
+    = FinalPreludeSourceLoadFailed !Prelude.PreludeLoadError
+    | FinalPreludeSourceParseFailed !Prelude.PreludeParseError
+    | FinalPreludeBuilt !FinalPreludeCandidate
+    | FinalPreludeBuildFailed
+        !FinalPreludeFailure
+        !Declaration.PendingModulePrefix
+    | FinalPreludeBuildOpenFailed !Declaration.DriverOpenError
+
+data PlannedPreludeDeclaration
+    = PlannedPreludeBinding
+        !(Declaration.PlannedDeclaration
+            Exact.CheckedExactBindingAuthorization)
+    | PlannedPreludeFoundation
+        !(Declaration.PlannedDeclaration
+            ExactProof.CheckedFinalPreludeFoundationAuthorization)
+    | PlannedPreludeProof
+        !(Declaration.PlannedDeclaration
+            ExactProof.CheckedExactProofAuthorization)
+    | PlannedPreludeBase
+        !(Declaration.PlannedDeclaration ())
+
+data PreludePlanningFailure
+    = PreludePlanningAction !FinalPreludeFailure
+    | PreludePlanningDeclaration !Declaration.DeclarationError
+
+data PreludeModulePlan = PreludeModulePlan
+    ![PlannedPreludeDeclaration]
+    !(Maybe PreludePlanningFailure)
+
+buildFinalPreludeCandidate
+    :: CheckedFoundation
+    -> Declaration.VampireResolver
+    -> IO FinalPreludeBuildResult
+buildFinalPreludeCandidate foundation resolver =
+    Prelude.loadReservedPreludeSourceInput >>= \case
+        Left failure ->
+            pure (FinalPreludeSourceLoadFailed failure)
+        Right source ->
+            Prelude.parseReservedPreludeSource source >>= \case
+                Left failure ->
+                    pure (FinalPreludeSourceParseFailed failure)
+                Right parsed ->
+                    buildParsedFinalPreludeCandidate
+                        foundation parsed resolver
+
+-- The production acquisition path establishes packaged provenance before
+-- passing its already parsed source here.  The explicit parsed seam avoids a
+-- second load and parse on a cache miss.
+buildParsedFinalPreludeCandidate
+    :: CheckedFoundation
+    -> Prelude.ReservedParsedPrelude
+    -> Declaration.VampireResolver
+    -> IO FinalPreludeBuildResult
+buildParsedFinalPreludeCandidate foundation parsed resolver =
+    case validatePackagedPreludeInput parsed syntax of
+        Left failure -> do
+            case emptyPrefix of
+                Left prefixFailure ->
+                    pure
+                        (FinalPreludeBuildOpenFailed
+                            (Declaration.DriverInitialPrefixError
+                                prefixFailure))
+                Right prefix ->
+                    pure (FinalPreludeBuildFailed failure prefix)
+        Right () -> do
+            outcome <-
+                Declaration.runModuleDriver
+                    foundation
+                    preludeModuleName
+                    []
+                    resolver
+                    -- The confined builder never consults stored validation.
+                    Declaration.FreshValidation
+                    do
+                        PreludeModulePlan declarations terminal <-
+                            Declaration.runProspectiveLoweringDriver
+                                (planBlocks [] 0 blocks)
+                        traverse_ admitPreludeDeclaration declarations
+                        traverse_ failPreludePlanning terminal
+            pure case outcome of
+                Left failure ->
+                    FinalPreludeBuildOpenFailed failure
+                Right (Declaration.DriverFailed failure prefix) ->
+                    FinalPreludeBuildFailed
+                        (case failure of
+                            Declaration.DriverDeclarationFailed err ->
+                                FinalPreludeDeclarationFailed err
+                            Declaration.DriverActionFailed err ->
+                                err)
+                        prefix
+                Right (Declaration.DriverSealFailed failure prefix) ->
+                    FinalPreludeBuildFailed
+                        (FinalPreludeSealFailed failure)
+                        prefix
+                Right (Declaration.DriverSucceeded
+                        () semantic prefix objects) ->
+                    case validateFinalPrelude
+                            foundation parsed semantic prefix objects of
+                        Left failure ->
+                            FinalPreludeBuildFailed
+                                (FinalPreludeValidationFailed failure)
+                                prefix
+                        Right roles ->
+                            FinalPreludeBuilt
+                                (FinalPreludeCandidate
+                                    parsed syntax semantic prefix objects roles)
+  where
+    identified = Prelude.reservedParsedPreludeModule parsed
+    blocks = identifiedParsedModuleBlocks identified
+    occurrences = identifiedParsedModuleSyntaxOccurrences identified
+    syntax = identifiedParsedModuleSyntaxInterface identified
+
+    emptyPrefix =
+        Declaration.emptyPendingModulePrefix
+            <$> initialPrefixContextId
+                (theoryId foundation)
+                preludeModuleName
+                []
+
+    planBlocks completed _blockIndex [] = do
+        planBaseStructure >>= \case
+            Left failure ->
+                pure
+                    (PreludeModulePlan
+                        (reverse completed)
+                        (Just failure))
+            Right base ->
+                pure
+                    (PreludeModulePlan
+                        (reverse (base : completed))
+                        Nothing)
+    planBlocks completed blockIndex (block : remaining) =
+        case block of
+            Raw.BlockClaim{} ->
+                case remaining of
+                    Raw.BlockProof _location proof _end : rest -> do
+                        continue completed (blockIndex + 2) rest
+                            =<< planOrdinaryProof block (Just proof)
+                    _ -> do
+                        continue completed (blockIndex + 1) remaining
+                            =<< planImplicitClaim block
+            Raw.BlockProof location _proof _end ->
+                pure
+                    (PreludeModulePlan
+                        (reverse completed)
+                        (Just
+                            (PreludePlanningAction
+                                (FinalPreludeUnmatchedProof location))))
+            Raw.BlockAbbr{} -> do
+                continue completed (blockIndex + 1) remaining
+                    =<< planBinding blockIndex block
+            Raw.BlockDefn{} -> do
+                continue completed (blockIndex + 1) remaining
+                    =<< planBinding blockIndex block
+            _ ->
+                pure
+                    (PreludeModulePlan
+                        (reverse completed)
+                        (Just
+                            (PreludePlanningAction
+                                (FinalPreludeUnsupportedBlock
+                                    (locate block)))))
+      where
+        continue accumulated nextIndex rest = \case
+            Left failure ->
+                pure
+                    (PreludeModulePlan
+                        (reverse accumulated)
+                        (Just failure))
+            Right declaration ->
+                planBlocks (declaration : accumulated) nextIndex rest
+
+    planBaseStructure = do
+        slot <- Declaration.nextDeclarationSlotLowering
+        theory <- Declaration.currentTheoryLowering
+        let seed =
+                opaqueDeclarationSeed
+                    (declarationSlotModule slot)
+                    (declarationSlotOrdinal slot)
+                    StructureDeclaration
+                    (generatedObjectSlot 0)
+            coreType = TyArrow TySet TySet
+            content = OpaqueObjectContent theory seed coreType
+            identity = opaqueObjectId theory seed coreType
+            asserted = assertedObject identity content
+            structurePhrase =
+                semanticStructurePhrase Lexicon._Onesorted
+            operation =
+                semanticStructureOperation Raw.CarrierSymbol identity
+        descriptor <-
+            either
+                (pure
+                    . Left
+                    . PreludePlanningDeclaration
+                    . Declaration.DeclarationEnvironmentFailed)
+                (pure . Right)
+                (semanticStructureDescriptor
+                    structurePhrase Nothing [] [operation])
+        case descriptor of
+            Left failure -> pure (Left failure)
+            Right checkedDescriptor ->
+                planPreludeChecked PlannedPreludeBase
+                    (Declaration.checkedCompiledDeclaration
+                        (declarationSyntaxId
+                            "felix-final-prelude-base-structure-v1")
+                        [asserted] [] [] [checkedDescriptor] [] ())
+
+    planBinding blockIndex block = do
+        prepared <-
+            Exact.prepareExactDeclaration
+                block
+                [ parsedSyntaxOccurrenceEntry occurrence
+                | occurrence <- occurrences
+                , parsedSyntaxOccurrenceBlockIndex occurrence == blockIndex
+                ]
+        case prepared of
+            Left failure ->
+                pure
+                    (Left
+                        (PreludePlanningAction
+                            (FinalPreludeExactDeclarationFailed failure)))
+            Right declaration -> do
+                Exact.lowerPreparedExactBinding declaration >>= \case
+                    Left failure -> planningDeclarationFailure failure
+                    Right checked ->
+                        planPreludeChecked PlannedPreludeBinding checked
+
+    planImplicitClaim block = do
+        foundationClaim <-
+            ExactProof.prepareFinalPreludeFoundationClaim
+                foundation block Nothing
+        case foundationClaim of
+            Right claim -> do
+                ExactProof.lowerPreparedFinalPreludeFoundationClaim claim
+                    >>= \case
+                        Left failure -> planningDeclarationFailure failure
+                        Right checked ->
+                            planPreludeChecked PlannedPreludeFoundation checked
+            Left ExactProof.ExactProofFoundationLeafTargetMismatch{} ->
+                planOrdinaryProof block Nothing
+            Left ExactProof.ExactProofFoundationLeafRequiresImplicitAuto{} ->
+                planOrdinaryProof block Nothing
+            Left failure ->
+                pure
+                    (Left
+                        (PreludePlanningAction
+                            (FinalPreludeExactProofFailed failure)))
+
+    planOrdinaryProof block explicitProof = do
+        prepared <-
+            ExactProof.prepareExactProof block explicitProof
+        case prepared of
+            Left failure ->
+                pure
+                    (Left
+                        (PreludePlanningAction
+                            (FinalPreludeExactProofFailed failure)))
+            Right proof
+                | Just location <-
+                    ExactProof.preparedExactProofFirstOmission proof ->
+                    pure
+                        (Left
+                            (PreludePlanningAction
+                                (FinalPreludeOmittedProof location)))
+                | otherwise ->
+                    ExactProof.lowerPreparedExactProof proof >>= \case
+                        Left failure -> planningDeclarationFailure failure
+                        Right checked ->
+                            planPreludeChecked PlannedPreludeProof checked
+
+    planPreludeChecked
+        :: forall body.
+           (Declaration.PlannedDeclaration body
+                -> PlannedPreludeDeclaration)
+        -> Declaration.CheckedDeclaration body
+        -> Declaration.LoweringDriver
+            (Either PreludePlanningFailure PlannedPreludeDeclaration)
+    planPreludeChecked constructor checked =
+        Declaration.planCheckedDeclaration checked >>= \case
+            Left failure -> planningDeclarationFailure failure
+            Right planned -> pure (Right (constructor planned))
+
+    planningDeclarationFailure =
+        pure . Left . PreludePlanningDeclaration
+
+    admitPreludeDeclaration = \case
+        PlannedPreludeBinding planned ->
+            void
+                (Declaration.admitPlannedCheckedDeclaration
+                    planned Exact.authorizeCheckedExactBinding)
+        PlannedPreludeFoundation planned ->
+            void
+                (Declaration.admitPlannedCheckedDeclaration planned
+                    ExactProof.authorizeCheckedFinalPreludeFoundationClaim)
+        PlannedPreludeProof planned ->
+            void
+                (Declaration.admitPlannedCheckedDeclaration
+                    planned ExactProof.authorizeCheckedExactProof)
+        PlannedPreludeBase planned ->
+            void
+                (Declaration.admitPlannedCheckedDeclaration planned
+                    (\() stages ->
+                        unless
+                            (null stages)
+                            (Declaration.failDeclaration
+                                (Declaration.CheckedAuthorizationCandidateShapeMismatch
+                                    0 (length stages)))))
+
+    failPreludePlanning = \case
+        PreludePlanningAction failure ->
+            Declaration.failModuleDriver failure
+        PreludePlanningDeclaration failure ->
+            Declaration.failDeclarationDriver failure
+
+data PreludeDeclaration = PreludeDeclaration
+    !Raw.Block
+    !Declaration.CommittedDeclarationBatch
+
+data PreludeDefinitionKind
+    = PreludeDefinition
+    | PreludeAbbreviation
+
+data PreludeDefinitionView = PreludeDefinitionView
+    !ObjectId
+    !SemanticGlobalTarget
+
+validateFinalPrelude
+    :: CheckedFoundation
+    -> Prelude.ReservedParsedPrelude
+    -> SemanticInterface
+    -> Declaration.PendingModulePrefix
+    -> CheckedObjectClosure
+    -> Either
+        FinalPreludeValidationError
+        (Map.Map PreludePublicRole FinalPreludeRoleTarget)
+validateFinalPrelude foundation parsed semantic prefix objects = do
+    (declarations, baseStructure) <-
+        associatePreludeDeclarations parsed prefix
+    validateConfinedAuthority
+        foundation semantic objects declarations baseStructure
+    resolveAndValidatePublicRoles foundation objects declarations
+
+resolveAndValidatePublicRoles
+    :: CheckedFoundation
+    -> CheckedObjectClosure
+    -> [PreludeDeclaration]
+    -> Either
+        FinalPreludeValidationError
+        (Map.Map PreludePublicRole FinalPreludeRoleTarget)
+resolveAndValidatePublicRoles foundation objects declarations = do
+    successor <-
+        expectDefinition
+            foundation objects declarations
+            "prelude_successor"
+            PreludeDefinition
+            (TyArrow TySet TySet)
+            expectedSuccessorBody
+    let successorId = definitionViewObject successor
+
+    inductive <-
+        expectDefinition
+            foundation objects declarations
+            "prelude_inductive"
+            PreludeDefinition
+            (TyArrow TySet TyProp)
+            (expectedInductiveBody successorId)
+    let inductiveId = definitionViewObject inductive
+
+    u0 <-
+        expectDefinition
+            foundation objects declarations
+            "prelude_u0"
+            PreludeDefinition
+            TySet
+            (applyIntrinsic UnivOf (CIntrinsic Empty))
+    let u0Id = definitionViewObject u0
+
+    let omegaBody = expectedOmegaBody u0Id inductiveId
+    omega <-
+        expectDefinition
+            foundation objects declarations
+            "prelude_omega"
+            PreludeDefinition
+            TySet
+            omegaBody
+    let omegaId = definitionViewObject omega
+
+    omegaConstruction <-
+        expectedOmegaConstruction objects omegaBody
+    omegaDerived <-
+        maybe
+            (Left
+                (FinalPreludeFactContentMismatch
+                    "prelude_omega"))
+            Right
+            (namedSetConstructionObjectFact
+                (checkedFoundationSetConstruction foundation)
+                omegaId
+                omegaConstruction)
+
+    naturals <-
+        expectDefinition
+            foundation objects declarations
+            "prelude_naturals"
+            PreludeAbbreviation
+            TySet
+            (CGlobal omegaId)
+    case definitionViewTarget naturals of
+        TransparentExpansion{} -> pure ()
+        _ ->
+            Left
+                (FinalPreludeDefinitionContentMismatch
+                    "prelude_naturals")
+
+    (infinity, infinityTarget) <-
+        expectClaim declarations "prelude_infinity"
+    validateInfinityTarget objects inductiveId infinityTarget
+    omegaDeclaration <- findDeclaration "prelude_omega" declarations
+    omegaEquation <-
+        validateOmegaDeclaration
+            objects
+            omegaId
+            omegaBody
+            omegaDerived
+            omegaDeclaration
+    let inductiveOmega =
+            CApp (CGlobal inductiveId) (CGlobal omegaId)
+        minimalOmega = expectedMinimality inductiveId omegaId
+    naturalsInductive <-
+        fst
+            <$> expectClaimTarget
+                declarations
+                "prelude_naturals_inductive"
+                inductiveOmega
+    naturalsMinimal <-
+        fst
+            <$> expectClaimTarget
+                declarations
+                "prelude_naturals_minimal"
+                minimalOmega
+
+    let roles = Map.fromList
+            [ ( PreludeInfinityTheorem
+              , FinalPreludeTheoremRole infinity
+              )
+            , ( PreludeOmegaObject
+              , FinalPreludeObjectRole omegaId
+              )
+            , ( PreludeOmegaDefiningEquation
+              , FinalPreludeTheoremRole omegaEquation
+              )
+            , ( PreludeNaturalsAlias
+              , FinalPreludeObjectRole omegaId
+              )
+            , ( PreludeNaturalsInductiveTheorem
+              , FinalPreludeTheoremRole naturalsInductive
+              )
+            , ( PreludeNaturalsMinimalTheorem
+              , FinalPreludeTheoremRole naturalsMinimal
+              )
+            ]
+    unless
+        (Map.keysSet roles == expectedFinalPreludePublicRoles)
+        (Left
+            (FinalPreludePublicRoleMismatch
+                PreludeInfinityTheorem))
+    pure roles
+
+expectedOmegaConstruction
+    :: CheckedObjectClosure
+    -> CanonicalTerm ObjectId
+    -> Either
+        FinalPreludeValidationError
+        (NamedSetConstruction ObjectId)
+expectedOmegaConstruction objects = \case
+    CApp (CApp (CIntrinsic Sep) bound) (CLam TySet predicate) -> do
+        checkedBound <- checked [] bound
+        checkedPredicate <- checked [TySet] predicate
+        maybe
+            (Left
+                (FinalPreludeFactContentMismatch
+                    "prelude_omega"))
+            Right
+            (checkedSeparationConstruction
+                (`lookupCheckedObjectType` objects)
+                checkedBound
+                checkedPredicate)
+    _ ->
+        Left
+            (FinalPreludeFactContentMismatch
+                "prelude_omega")
+  where
+    checked context term =
+        first
+            (const
+                (FinalPreludeFactContentMismatch
+                    "prelude_omega"))
+            (checkScopedCanonicalCore
+                (`lookupCheckedObjectType` objects)
+                context
+                term)
+
+validateOmegaDeclaration
+    :: CheckedObjectClosure
+    -> ObjectId
+    -> CanonicalTerm ObjectId
+    -> NamedSetConstructionFact
+    -> PreludeDeclaration
+    -> Either FinalPreludeValidationError TheoremRef
+validateOmegaDeclaration objects omegaId omegaBody derived declaration = do
+    let batch = declarationBatch declaration
+        delta = Declaration.committedBatchDelta batch
+    omegaContent <- case lookupCheckedObjectContent omegaId objects of
+        Just content@TransparentObjectContent{} -> pure content
+        _ ->
+            Left
+                (FinalPreludeFactContentMismatch
+                    "prelude_omega")
+    unless
+        ( declarationDeltaObjects delta == [omegaId]
+          && case Declaration.committedBatchObjects batch of
+                [asserted] ->
+                    assertedObjectId asserted == omegaId
+                        && assertedObjectContent asserted == omegaContent
+                _ -> False
+          && null (Declaration.committedBatchProofValidations batch)
+        )
+        (Left
+            (FinalPreludeFactContentMismatch
+                "prelude_omega"))
+    certificates <-
+        maybe
+            (Left
+                (FinalPreludeFactContentMismatch
+                    "prelude_omega"))
+            (Right . declarationValidationRecordCertificates)
+            (Declaration.committedBatchDeclarationValidation batch)
+    validateOmegaFactInventory
+        omegaId
+        omegaBody
+        (namedSetConstructionFactProposition derived)
+        (namedSetConstructionFactDescriptor derived)
+        (declarationDeltaFacts delta)
+        (declarationDeltaAliases delta)
+        (Declaration.committedBatchPropositions batch)
+        certificates
+
+-- | Purpose-specific audit of the distinguished Omega definition.  It is
+-- deliberately not a general declaration manifest: the confined prelude has
+-- exactly one declaration whose public role requires this two-fact shape.
+-- The explicit arguments also provide a narrow pure seam for corruption
+-- regression tests.
+validateOmegaFactInventory
+    :: ObjectId
+    -> CanonicalTerm ObjectId
+    -> FrozenCheckedCore ObjectId
+    -> CacheDigest
+    -> [SemanticFactOccurrence]
+    -> [SemanticAlias]
+    -> [CheckedPropositionContent]
+    -> [Authority.ValidationCertificate]
+    -> Either FinalPreludeValidationError TheoremRef
+validateOmegaFactInventory
+        omegaId omegaBody expectedExtensional expectedDescriptor
+        facts aliases propositions certificates = do
+    (equationOccurrence, extensionalOccurrence) <-
+        case facts of
+            [equation, extensional] -> Right (equation, extensional)
+            _ -> mismatch
+    (equationCertificate, extensionalCertificate) <-
+        case certificates of
+            [equation, extensional] -> Right (equation, extensional)
+            _ -> mismatch
+    case aliases of
+        [alias]
+            | semanticAliasName alias == semanticName "prelude_omega"
+            , semanticAliasTarget alias
+                == semanticFactFingerprint equationOccurrence ->
+                    pure ()
+        _ -> mismatch
+    equation <- propositionFor equationOccurrence
+    extensional <- propositionFor extensionalOccurrence
+    unless
+        ( length propositions == 2
+          && semanticFactSearchEligibility equationOccurrence
+                == SearchIneligible
+          && frozenCoreTerm (checkedPropositionTerm equation)
+                == CEq TySet (CGlobal omegaId) omegaBody
+          && Authority.validationTarget equationCertificate
+                == semanticFactAuthority equationOccurrence
+          && Authority.validationDirectAuthorization equationCertificate
+                == Authority.CheckedKernelConstruction
+                    (Authority.CheckedDefinitionEquation omegaId)
+          && semanticFactSearchEligibility extensionalOccurrence
+                == SearchEligible
+          && checkedPropositionTerm extensional == expectedExtensional
+          && Authority.validationTarget extensionalCertificate
+                == semanticFactAuthority extensionalOccurrence
+          && Authority.validationDirectAuthorization extensionalCertificate
+                == Authority.CheckedKernelConstruction
+                    (Authority.CheckedSetConstructionExtensionality
+                        omegaId expectedDescriptor)
+        )
+        mismatch
+    pure
+        (Authority.factAuthorityTheorem
+            (semanticFactAuthority equationOccurrence))
+  where
+    mismatch =
+        Left
+            (FinalPreludeFactContentMismatch
+                "prelude_omega")
+
+    propositionFor occurrence =
+        case List.filter
+                ((== semanticFactProposition occurrence)
+                    . checkedPropositionId)
+                propositions of
+            [proposition] -> Right proposition
+            _ -> mismatch
+
+validatePackagedPreludeInput
+    :: Prelude.ReservedParsedPrelude
+    -> ModuleSyntaxInterface
+    -> Either FinalPreludeFailure ()
+validatePackagedPreludeInput parsed syntax
+    | freshModuleInputOwner input /= preludeModuleName =
+        Left (FinalPreludeWrongOwner (freshModuleInputOwner input))
+    | not (null (freshModuleInputImports input)) =
+        Left (FinalPreludeHasImports (freshModuleInputImports input))
+    | not (null (moduleSyntaxDirectInputs syntax)) =
+        Left
+            (FinalPreludeHasSyntaxImports
+                (moduleSyntaxDirectInputs syntax))
+    | otherwise = do
+        unless
+            ( freshModuleInputBinding input == FreshReservedSource
+              && freshModuleInputLocationPath input
+                    == Prelude.preludeDiagnosticLabel
+              && freshModuleInputSyntaxInterface input == syntax
+              && identifiedParsedModuleSyntaxInterface identified == syntax
+            )
+            (Left
+                (FinalPreludeValidationFailed
+                    FinalPreludePackagedInputMismatch))
+  where
+    input = Prelude.reservedParsedPreludeInput parsed
+    identified = Prelude.reservedParsedPreludeModule parsed
+
+associatePreludeDeclarations
+    :: Prelude.ReservedParsedPrelude
+    -> Declaration.PendingModulePrefix
+    -> Either
+        FinalPreludeValidationError
+        ([PreludeDeclaration], Declaration.CommittedDeclarationBatch)
+associatePreludeDeclarations parsed prefix = do
+    case List.splitAt (length sourceDeclarations) batches of
+        (sourceBatches, [baseStructure])
+            | length sourceBatches == length sourceDeclarations ->
+                pure
+                    ( zipWith PreludeDeclaration
+                        sourceDeclarations sourceBatches
+                    , baseStructure
+                    )
+        _ -> Left FinalPreludeDeclarationAssociationMismatch
+  where
+    sourceDeclarations =
+        [ block
+        | block <-
+            identifiedParsedModuleBlocks
+                (Prelude.reservedParsedPreludeModule parsed)
+        , case block of
+            Raw.BlockProof{} -> False
+            _ -> True
+        ]
+    batches = Declaration.pendingModulePrefixBatches prefix
+
+validateConfinedAuthority
+    :: CheckedFoundation
+    -> SemanticInterface
+    -> CheckedObjectClosure
+    -> [PreludeDeclaration]
+    -> Declaration.CommittedDeclarationBatch
+    -> Either FinalPreludeValidationError ()
+validateConfinedAuthority
+        foundation semantic objects declarations baseStructure = do
+    unless
+        ( semanticInterfaceOwner semantic == preludeModuleName
+          && null (semanticInterfaceDirectInputs semantic)
+        )
+        (Left FinalPreludeSemanticEnvironmentMismatch)
+    traverse_ requireTransparent
+        [ identity
+        | declaration <- declarations
+        , identity <-
+            declarationDeltaObjects
+                (Declaration.committedBatchDelta
+                    (declarationBatch declaration))
+        ]
+    traverse_ (validateDeclarationAuthority foundation objects) declarations
+    validateBaseStructure foundation objects baseStructure
+  where
+    requireTransparent identity =
+        case lookupCheckedObjectContent identity objects of
+            Just TransparentObjectContent{} -> pure ()
+            _ -> Left (FinalPreludeUnexpectedObject identity)
+
+validateBaseStructure
+    :: CheckedFoundation
+    -> CheckedObjectClosure
+    -> Declaration.CommittedDeclarationBatch
+    -> Either FinalPreludeValidationError ()
+validateBaseStructure foundation objects batch = do
+    let slot = Declaration.committedBatchSlot batch
+        delta = Declaration.committedBatchDelta batch
+        environment = declarationDeltaEnvironment delta
+        structurePhrase = semanticStructurePhrase Lexicon._Onesorted
+        expectedSeed =
+            opaqueDeclarationSeed
+                (declarationSlotModule slot)
+                (declarationSlotOrdinal slot)
+                StructureDeclaration
+                (generatedObjectSlot 0)
+        expectedType = TyArrow TySet TySet
+        expectedObject = opaqueObjectId (theoryId foundation) expectedSeed expectedType
+        expectedContent =
+            OpaqueObjectContent
+                (theoryId foundation)
+                expectedSeed
+                expectedType
+    descriptor <-
+        case semanticEnvironmentStructures environment of
+            [single] -> Right single
+            _ -> Left FinalPreludeBaseStructureMismatch
+    expectedDescriptor <-
+        first (const FinalPreludeBaseStructureMismatch)
+            (semanticStructureDescriptor
+                structurePhrase
+                Nothing
+                []
+                [semanticStructureOperation Raw.CarrierSymbol expectedObject])
+    unless
+        ( declarationSlotModule slot == preludeModuleName
+          && descriptor == expectedDescriptor
+          && null (semanticEnvironmentBindings environment)
+          && declarationDeltaObjects delta == [expectedObject]
+          && null (declarationDeltaFacts delta)
+          && null (declarationDeltaAliases delta)
+          && null (declarationDeltaPropositions delta)
+          && Declaration.committedBatchObjects batch
+                == [assertedObject expectedObject expectedContent]
+          && null (Declaration.committedBatchPropositions batch)
+          && null (Declaration.committedBatchProofValidations batch)
+          && maybe
+                False
+                (null . declarationValidationRecordCertificates)
+                (Declaration.committedBatchDeclarationValidation batch)
+          && lookupCheckedObjectContent expectedObject objects
+                == Just expectedContent
+        )
+        (Left FinalPreludeBaseStructureMismatch)
+
+validateDeclarationAuthority
+    :: CheckedFoundation
+    -> CheckedObjectClosure
+    -> PreludeDeclaration
+    -> Either FinalPreludeValidationError ()
+validateDeclarationAuthority foundation objects declaration = do
+    unless
+        (fmap Authority.validationTarget certificates
+            == fmap semanticFactAuthority facts)
+        (Left (FinalPreludeValidationInventoryMismatch slot))
+    traverse_ validateOne (zip facts certificates)
+  where
+    batch = declarationBatch declaration
+    delta = Declaration.committedBatchDelta batch
+    slot = Declaration.committedBatchSlot batch
+    facts = declarationDeltaFacts delta
+    certificates =
+        ( Semantic.proofValidationRecordCertificate
+            <$> Declaration.committedBatchProofValidations batch
+        )
+        <> maybe
+            []
+            Semantic.declarationValidationRecordCertificates
+            (Declaration.committedBatchDeclarationValidation batch)
+
+    validateOne (occurrence, certificate) = do
+        unless
+            (Authority.factAuthoritySafety
+                (semanticFactAuthority occurrence)
+                    == Authority.cleanAuthoritySafety)
+            (Left (FinalPreludeAuthorityMismatch slot))
+        proposition <-
+            maybe
+                (Left (FinalPreludeValidationInventoryMismatch slot))
+                Right
+                (List.find
+                    ((== semanticFactProposition occurrence)
+                        . checkedPropositionId)
+                    (Declaration.committedBatchPropositions batch))
+        let target = frozenCoreTerm (checkedPropositionTerm proposition)
+        case Authority.validationDirectAuthorization certificate of
+            Authority.CheckedKernelConstruction
+                    (Authority.FoundationLeaf tag) -> do
+                let expected =
+                        frozenCoreTerm
+                            (mapFrozenGlobals absurd
+                                (foundationAxiomFrozen foundation tag))
+                unless (target == expected)
+                    (Left (FinalPreludeAuthorityMismatch slot))
+            Authority.CheckedKernelConstruction
+                    (Authority.CheckedDefinitionEquation identity) ->
+                case lookupCheckedObjectContent identity objects of
+                    Just (TransparentObjectContent _theory coreType body) ->
+                        unless
+                            (target == CEq coreType (CGlobal identity) body)
+                            (Left (FinalPreludeAuthorityMismatch slot))
+                    _ ->
+                        Left (FinalPreludeAuthorityMismatch slot)
+            Authority.CheckedKernelConstruction
+                    (Authority.CheckedSetConstructionExtensionality
+                        identity _descriptor) ->
+                case lookupCheckedObjectContent identity objects of
+                    Just TransparentObjectContent{}
+                        | semanticFactSearchEligibility occurrence
+                            == SearchEligible ->
+                                pure ()
+                    _ ->
+                        Left (FinalPreludeAuthorityMismatch slot)
+            Authority.CheckedSourceProof requests ->
+                unless
+                    ( not (null requests)
+                      && case declarationBlock declaration of
+                            Raw.BlockClaim{} -> True
+                            _ -> False
+                    )
+                    (Left (FinalPreludeAuthorityMismatch slot))
+            _ ->
+                Left (FinalPreludeAuthorityMismatch slot)
+
+expectDefinition
+    :: CheckedFoundation
+    -> CheckedObjectClosure
+    -> [PreludeDeclaration]
+    -> Text
+    -> PreludeDefinitionKind
+    -> CoreType
+    -> CanonicalTerm ObjectId
+    -> Either FinalPreludeValidationError PreludeDefinitionView
+expectDefinition foundation objects declarations marker kind coreType body = do
+    declaration <- findDeclaration marker declarations
+    let delta =
+            Declaration.committedBatchDelta
+                (declarationBatch declaration)
+    unless
+        (case (kind, declarationBlock declaration) of
+            (PreludeDefinition, Raw.BlockDefn{}) -> True
+            (PreludeAbbreviation, Raw.BlockAbbr{}) -> True
+            _ -> False)
+        (Left (FinalPreludeDeclarationShapeMismatch marker))
+    binding <-
+        case semanticEnvironmentBindings
+                (declarationDeltaEnvironment delta) of
+            [single] -> Right single
+            _ -> Left (FinalPreludeDeclarationShapeMismatch marker)
+    let target = semanticGlobalBindingTarget binding
+        identity = semanticGlobalTargetObject target
+    unless
+        (case (kind, target) of
+            (PreludeDefinition, GlobalReference{}) -> True
+            (PreludeAbbreviation, TransparentExpansion{}) -> True
+            _ -> False)
+        (Left (FinalPreludeDefinitionContentMismatch marker))
+    content <-
+        maybe
+            (Left (FinalPreludeDefinitionContentMismatch marker))
+            Right
+            (lookupCheckedObjectContent identity objects)
+    let expected =
+            TransparentObjectContent
+                (theoryId foundation)
+                coreType
+                body
+    unless (content == expected)
+        (Left (FinalPreludeDefinitionContentMismatch marker))
+    pure (PreludeDefinitionView identity target)
+
+expectClaim
+    :: [PreludeDeclaration]
+    -> Text
+    -> Either
+        FinalPreludeValidationError
+        (TheoremRef, CanonicalTerm ObjectId)
+expectClaim declarations marker = do
+    declaration <- findDeclaration marker declarations
+    unless
+        (case declarationBlock declaration of
+            Raw.BlockClaim{} -> True
+            _ -> False)
+        (Left (FinalPreludeDeclarationShapeMismatch marker))
+    expectFact declarations marker
+
+expectClaimTarget
+    :: [PreludeDeclaration]
+    -> Text
+    -> CanonicalTerm ObjectId
+    -> Either
+        FinalPreludeValidationError
+        (TheoremRef, CanonicalTerm ObjectId)
+expectClaimTarget declarations marker expected = do
+    result@(_theorem, actual) <- expectClaim declarations marker
+    unless
+        (actual == expected)
+        (Left (FinalPreludeFactContentMismatch marker))
+    pure result
+
+expectFact
+    :: [PreludeDeclaration]
+    -> Text
+    -> Either
+        FinalPreludeValidationError
+        (TheoremRef, CanonicalTerm ObjectId)
+expectFact declarations marker = do
+    declaration <- findDeclaration marker declarations
+    unless
+        (length
+            (declarationDeltaFacts
+                (Declaration.committedBatchDelta
+                    (declarationBatch declaration))) == 1)
+        (Left (FinalPreludeFactContentMismatch marker))
+    expectAliasedFact declaration marker
+
+expectAliasedFact
+    :: PreludeDeclaration
+    -> Text
+    -> Either
+        FinalPreludeValidationError
+        (TheoremRef, CanonicalTerm ObjectId)
+expectAliasedFact declaration marker = do
+    let batch = declarationBatch declaration
+        delta = Declaration.committedBatchDelta batch
+        expectedAlias = semanticName marker
+    fingerprint <- case declarationDeltaAliases delta of
+        [alias]
+            | semanticAliasName alias == expectedAlias ->
+                Right (semanticAliasTarget alias)
+        _ -> Left (FinalPreludeFactContentMismatch marker)
+    occurrence <- case List.filter
+            ((== fingerprint) . semanticFactFingerprint)
+            (declarationDeltaFacts delta) of
+        [single] -> Right single
+        _ -> Left (FinalPreludeFactContentMismatch marker)
+    proposition <-
+        maybe
+            (Left (FinalPreludeFactContentMismatch marker))
+            Right
+            (List.find
+                ((== semanticFactProposition occurrence)
+                    . checkedPropositionId)
+                (Declaration.committedBatchPropositions batch))
+    pure
+        ( Authority.factAuthorityTheorem
+            (semanticFactAuthority occurrence)
+        , frozenCoreTerm (checkedPropositionTerm proposition)
+        )
+
+validateInfinityTarget
+    :: CheckedObjectClosure
+    -> ObjectId
+    -> CanonicalTerm ObjectId
+    -> Either FinalPreludeValidationError ()
+validateInfinityTarget objects inductive = \case
+    CApp (CGlobal predicate) (CGlobal witness)
+        | predicate == inductive ->
+            case lookupCheckedObjectContent witness objects of
+                Just TransparentObjectContent{} -> pure ()
+                _ ->
+                    Left
+                        (FinalPreludeFactContentMismatch
+                            "prelude_infinity")
+    _ ->
+        Left
+            (FinalPreludeFactContentMismatch
+                "prelude_infinity")
+
+findDeclaration
+    :: Text
+    -> [PreludeDeclaration]
+    -> Either FinalPreludeValidationError PreludeDeclaration
+findDeclaration marker declarations =
+    case List.filter ((== marker) . declarationMarker) declarations of
+        [] -> Left (FinalPreludeDeclarationMissing marker)
+        [single] -> Right single
+        _ -> Left (FinalPreludeDeclarationDuplicate marker)
+
+declarationBlock :: PreludeDeclaration -> Raw.Block
+declarationBlock (PreludeDeclaration block _batch) =
+    block
+
+declarationBatch
+    :: PreludeDeclaration
+    -> Declaration.CommittedDeclarationBatch
+declarationBatch (PreludeDeclaration _block batch) =
+    batch
+
+declarationMarker :: PreludeDeclaration -> Text
+declarationMarker =
+    fromMaybe "<unmarked>" . blockMarkerText . declarationBlock
+
+definitionViewObject :: PreludeDefinitionView -> ObjectId
+definitionViewObject (PreludeDefinitionView identity _target) =
+    identity
+
+definitionViewTarget
+    :: PreludeDefinitionView
+    -> SemanticGlobalTarget
+definitionViewTarget (PreludeDefinitionView _identity target) =
+    target
+
+blockMarkerText :: Raw.Block -> Maybe Text
+blockMarkerText = fmap (\(Raw.Marker marker) -> marker) . \case
+    Raw.BlockAxiom _location _title marker _axiom -> Just marker
+    Raw.BlockClaim _kind _location _title marker _claim -> Just marker
+    Raw.BlockDefn _location _title marker _definition -> Just marker
+    Raw.BlockAbbr _location _title marker _abbreviation -> Just marker
+    Raw.BlockData _location _title marker _datatype -> Just marker
+    Raw.BlockInductive _location _title marker _inductive -> Just marker
+    Raw.BlockSig _location _title marker _assumptions _signature -> Just marker
+    Raw.BlockStruct _location _title marker _structure -> Just marker
+    Raw.BlockProof{} -> Nothing
+
+expectedSuccessorBody :: CanonicalTerm ObjectId
+expectedSuccessorBody =
+    CLam TySet
+        (canonicalSetInsert (CBound 0) (CBound 0))
+
+expectedInductiveBody :: ObjectId -> CanonicalTerm ObjectId
+expectedInductiveBody successor =
+    CLam TySet
+        (logicalAnd
+            (memberTerm (CIntrinsic Empty) (CBound 0))
+            (CForall TySet
+                (CImp
+                    (memberTerm (CBound 0) (CBound 1))
+                    (memberTerm
+                        (CApp (CGlobal successor) (CBound 0))
+                        (CBound 1)))))
+
+expectedOmegaBody
+    :: ObjectId
+    -> ObjectId
+    -> CanonicalTerm ObjectId
+expectedOmegaBody u0 inductive =
+    CApp
+        (CApp (CIntrinsic Sep) (CGlobal u0))
+        (CLam TySet
+            (CForall TySet
+                (CImp
+                    (CApp (CGlobal inductive) (CBound 0))
+                    (memberTerm (CBound 1) (CBound 0)))))
+
+expectedMinimality
+    :: ObjectId
+    -> ObjectId
+    -> CanonicalTerm ObjectId
+expectedMinimality inductive omega =
+    CForall TySet
+        (CImp
+            (CApp (CGlobal inductive) (CBound 0))
+            (CForall TySet
+                (CImp
+                    (memberTerm (CBound 0) (CGlobal omega))
+                    (memberTerm (CBound 0) (CBound 1)))))
+
+applyIntrinsic
+    :: CoreIntrinsicTag
+    -> CanonicalTerm global
+    -> CanonicalTerm global
+applyIntrinsic intrinsic argument =
+    CApp (CIntrinsic intrinsic) argument
+
+applyIntrinsic2
+    :: CoreIntrinsicTag
+    -> CanonicalTerm global
+    -> CanonicalTerm global
+    -> CanonicalTerm global
+applyIntrinsic2 intrinsic firstArgument secondArgument =
+    CApp
+        (CApp (CIntrinsic intrinsic) firstArgument)
+        secondArgument
+
+memberTerm
+    :: CanonicalTerm global
+    -> CanonicalTerm global
+    -> CanonicalTerm global
+memberTerm =
+    applyIntrinsic2 Member
+
+logicalAnd
+    :: CanonicalTerm global
+    -> CanonicalTerm global
+    -> CanonicalTerm global
+logicalAnd left right =
+    CImp
+        (CImp left (CImp right CFalsum))
+        CFalsum