diff options
Diffstat (limited to 'source/Felix/Checking/FinalPrelude.hs')
| -rw-r--r-- | source/Felix/Checking/FinalPrelude.hs | 1266 |
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 |