{-# 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 "" . 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