path: root/source/Checking/FinalPrelude.hs

{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE RankNTypes #-}

-- | Authority-confined construction of the inert final-prelude candidate.
module Checking.FinalPrelude
    ( FinalPreludeCandidate
    , finalPreludeParsed
    , finalPreludeSyntax
    , finalPreludeSemantic
    , finalPreludePrefix
    , finalPreludeObjects
    , PreludePublicRole(..)
    , expectedFinalPreludePublicRoles
    , FinalPreludeRoleTarget(..)
    , finalPreludePublicRole
    , FinalPreludeValidationError(..)
    , FinalPreludeFailure(..)
    , FinalPreludeBuildResult(..)
    , buildFinalPreludeCandidate
    , buildParsedFinalPreludeCandidate
    ) where

import Base hiding (Empty)
import Checking.Authority qualified as Authority
import Checking.Core
import Checking.Declaration qualified as Declaration
import Checking.Exact qualified as Exact
import Checking.Exact.Proof qualified as ExactProof
import Checking.Foundation
import Checking.Identity
import Checking.Semantic
import Checking.Semantic qualified as Semantic
import Felix.Module
import Felix.Parse
import Felix.Prelude qualified as Prelude
import Felix.Source (ImportRef)
import Report.Location
import Syntax.Abstract qualified as Raw
import Syntax.Interface
import 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 (Maybe ObjectId))
    | 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

    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
    omegaEquation <-
        fst
            <$> expectFactTarget
                declarations
                "prelude_omega"
                (CEq TySet (CGlobal omegaId) omegaBody)
    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

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.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
    let batch = declarationBatch declaration
        delta = Declaration.committedBatchDelta batch
        expectedAlias = semanticName marker
    occurrence <- case declarationDeltaFacts delta of
        [single] -> Right single
        _ -> Left (FinalPreludeFactContentMismatch marker)
    unless
        (declarationDeltaAliases delta
            == [semanticAlias expectedAlias
                    (semanticFactFingerprint occurrence)])
        (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)
        )

expectFactTarget
    :: [PreludeDeclaration]
    -> Text
    -> CanonicalTerm ObjectId
    -> Either
        FinalPreludeValidationError
        (TheoremRef, CanonicalTerm ObjectId)
expectFactTarget declarations marker expected = do
    result@(_theorem, actual) <- expectFact declarations marker
    unless
        (actual == expected)
        (Left (FinalPreludeFactContentMismatch marker))
    pure result

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