{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE NoImplicitPrelude #-} -- | The one compiled monomorphic HOL/HOTG foundation. -- -- Constructing 'CheckedFoundation' requires exact manifest coverage, closed -- well-typed schemas, and structural backend classification. This gate -- certifies manifest conformance only; it is not a consistency proof. module Felix.Checking.Foundation ( FoundationAxiomTag(..) , KernelRuleTag(..) , KernelRuleSignature(..) , FoundationRuleInput(..) , FoundationBackendClass(..) , FofExclusion(..) , FoundationAxiomInput(..) , FoundationManifestError(..) , FoundationManifestAudit , auditFoundationManifest , compiledFoundationIntrinsicRows , compiledFoundationRuleRows , compiledFoundationAxiomRows , CheckedFoundation , checkedFoundation , foundationAxiomProposition , foundationAxiomFrozen , foundationAxiomBackendClass , foundationRuleSignature , foundationAxiomDependencies , classifyCanonicalFofStructure , classifyFrozenCore ) where import Base hiding (Empty) import Felix.Checking.Core import Control.Monad (unless) import Data.List qualified as List import Data.Map.Strict qualified as Map import Data.Set qualified as Set import Numeric.Natural (Natural) -- | The complete axiom inventory. Ordinary implication, quantifier, equality, -- and falsum rules are dedicated kernel operations rather than manifest rows. data FoundationAxiomTag = EmptyCharacteristic | PairSetCharacteristic | FamilyUnionCharacteristic | PowerSetCharacteristic | SeparationCharacteristic | ReplacementCharacteristic | SetChooseWitness | SetExtensionality | SetInduction | PropositionalExtensionality | DoubleNegationElim | UnivOfContains | UnivOfTransitive | UnivOfFamilyUnionClosed | UnivOfPowerSetClosed | UnivOfReplacementClosed | UnivOfMinimal deriving stock (Show, Eq, Ord, Enum, Bounded) -- | The complete guarded-rule inventory. data KernelRuleTag = SetLfpBound | SetLfpLeast | SetLfpFixed | SetLfpInduct deriving stock (Show, Eq, Ord, Enum, Bounded) data KernelRuleSignature = KernelRuleSignature ![CoreType] !Natural deriving stock (Show, Eq) data FoundationRuleInput = FoundationRuleInput !KernelRuleTag !KernelRuleSignature deriving stock (Show, Eq) data FofExclusion = HigherOrderBinder !CoreType | HigherOrderEquality !CoreType | HigherOrderLambda | HigherOrderIntrinsic !CoreIntrinsicTag deriving stock (Show, Eq, Ord) data FoundationBackendClass = FoundationFofProjectable | FoundationRequiresTh0 !(NonEmpty FofExclusion) deriving stock (Show, Eq) -- | One proposed manifest row. This is deliberately not an authority-bearing -- fact; only the fixed compiled rows can produce 'CheckedFoundation'. data FoundationAxiomInput = FoundationAxiomInput !FoundationAxiomTag !(CoreSyntax Void Natural) !FoundationBackendClass data FoundationManifestError = MissingFoundationIntrinsic !CoreIntrinsicTag | DuplicateFoundationIntrinsic !CoreIntrinsicTag | FoundationIntrinsicTypeMismatch !CoreIntrinsicTag !CoreType !CoreType | MissingFoundationRule !KernelRuleTag | DuplicateFoundationRule !KernelRuleTag | FoundationRuleSignatureMismatch !KernelRuleTag !KernelRuleSignature !KernelRuleSignature | MissingFoundationAxiom !FoundationAxiomTag | DuplicateFoundationAxiom !FoundationAxiomTag | FoundationAxiomIllTyped !FoundationAxiomTag !CoreCheckError | FoundationAxiomFreezeFailed !FoundationAxiomTag !FreezeError | FoundationAxiomStatementMismatch !FoundationAxiomTag | FoundationAxiomBackendClassMismatch !FoundationAxiomTag !FoundationBackendClass !FoundationBackendClass deriving stock (Show, Eq) data CheckedFoundationAxiom = CheckedFoundationAxiom !(ClosedCheckedProposition Void) !(FrozenCheckedCore Void) !FoundationBackendClass newtype FoundationManifestAudit = FoundationManifestAudit ( Map FoundationAxiomTag CheckedFoundationAxiom , Map KernelRuleTag KernelRuleSignature ) data CheckedFoundation = CheckedFoundation !(Map FoundationAxiomTag CheckedFoundationAxiom) !(Map KernelRuleTag KernelRuleSignature) compiledFoundationIntrinsicRows :: [(CoreIntrinsicTag, CoreType)] compiledFoundationIntrinsicRows = [ (Member, TySet `TyArrow` (TySet `TyArrow` TyProp)) , (Empty, TySet) , (PairSet, TySet `TyArrow` (TySet `TyArrow` TySet)) , (FamilyUnion, TySet `TyArrow` TySet) , (PowerSet, TySet `TyArrow` TySet) , ( Sep , TySet `TyArrow` ((TySet `TyArrow` TyProp) `TyArrow` TySet) ) , ( Repl , TySet `TyArrow` ((TySet `TyArrow` TySet) `TyArrow` TySet) ) , (SetChoose, (TySet `TyArrow` TyProp) `TyArrow` TySet) , (UnivOf, TySet `TyArrow` TySet) , ( ISetLfp , TySet `TyArrow` ((TySet `TyArrow` TySet) `TyArrow` TySet) ) ] compiledFoundationRuleRows :: [FoundationRuleInput] compiledFoundationRuleRows = [ FoundationRuleInput tag (expectedKernelRuleSignature tag) | tag <- allKernelRuleTags ] compiledFoundationAxiomRows :: [FoundationAxiomInput] compiledFoundationAxiomRows = [ FoundationAxiomInput tag (foundationAxiomSyntax tag) (expectedFoundationBackendClass tag) | tag <- allFoundationAxiomTags ] checkedFoundation :: Either (NonEmpty FoundationManifestError) CheckedFoundation checkedFoundation = do FoundationManifestAudit (axioms, rules) <- auditFoundationManifest compiledFoundationIntrinsicRows compiledFoundationRuleRows compiledFoundationAxiomRows pure (CheckedFoundation axioms rules) -- | Audit arbitrary proposed rows without granting foundation authority. -- This is also the pure mutation boundary used by conformance tests. auditFoundationManifest :: [(CoreIntrinsicTag, CoreType)] -> [FoundationRuleInput] -> [FoundationAxiomInput] -> Either (NonEmpty FoundationManifestError) FoundationManifestAudit auditFoundationManifest intrinsicRows ruleRows axiomRows = case intrinsicErrors <> ruleErrors <> axiomCoverageErrors <> axiomErrors of [] -> case checkedRows of Left errors -> Left errors Right rows -> Right (FoundationManifestAudit ( Map.fromList rows , Map.fromList [ (tag, signature) | FoundationRuleInput tag signature <- ruleRows ] )) firstError : remainingErrors -> Left (firstError :| remainingErrors) where intrinsicErrors = coverageErrors MissingFoundationIntrinsic DuplicateFoundationIntrinsic allCoreIntrinsicTags (fst <$> intrinsicRows) <> [ FoundationIntrinsicTypeMismatch tag (coreIntrinsicType tag) actual | (tag, actual) <- intrinsicRows , actual /= coreIntrinsicType tag ] axiomCoverageErrors = coverageErrors MissingFoundationAxiom DuplicateFoundationAxiom allFoundationAxiomTags [ tag | FoundationAxiomInput tag _syntax _backendClass <- axiomRows ] ruleErrors = coverageErrors MissingFoundationRule DuplicateFoundationRule allKernelRuleTags [ tag | FoundationRuleInput tag _signature <- ruleRows ] <> [ FoundationRuleSignatureMismatch tag (expectedKernelRuleSignature tag) actual | FoundationRuleInput tag actual <- ruleRows , actual /= expectedKernelRuleSignature tag ] checkedRows = traverse checkAxiomRow axiomRows axiomErrors = case checkedRows of Left errors -> toList errors Right _rows -> [] checkAxiomRow :: FoundationAxiomInput -> Either (NonEmpty FoundationManifestError) (FoundationAxiomTag, CheckedFoundationAxiom) checkAxiomRow (FoundationAxiomInput tag syntax declaredBackendClass) = do proposition <- firstOne (FoundationAxiomIllTyped tag) (checkClosedProposition absurd syntax) frozen <- firstOne (FoundationAxiomFreezeFailed tag) (freezeClosed (checkedPropositionCore proposition)) expectedFrozen <- expectedFoundationAxiom tag unless (frozen == expectedFrozen) (Left (FoundationAxiomStatementMismatch tag :| [])) let actualBackendClass = classifyFrozenCore frozen unless (declaredBackendClass == actualBackendClass) (Left (FoundationAxiomBackendClassMismatch tag declaredBackendClass actualBackendClass :| [])) pure ( tag , CheckedFoundationAxiom proposition frozen actualBackendClass ) expectedFoundationAxiom :: FoundationAxiomTag -> Either (NonEmpty FoundationManifestError) (FrozenCheckedCore Void) expectedFoundationAxiom tag = do proposition <- firstOne (FoundationAxiomIllTyped tag) (checkClosedProposition absurd (foundationAxiomSyntax tag)) firstOne (FoundationAxiomFreezeFailed tag) (freezeClosed (checkedPropositionCore proposition)) foundationAxiomProposition :: CheckedFoundation -> FoundationAxiomTag -> ClosedCheckedProposition Void foundationAxiomProposition foundation tag = case lookupFoundationAxiom foundation tag of CheckedFoundationAxiom proposition _frozen _backendClass -> proposition foundationAxiomFrozen :: CheckedFoundation -> FoundationAxiomTag -> FrozenCheckedCore Void foundationAxiomFrozen foundation tag = case lookupFoundationAxiom foundation tag of CheckedFoundationAxiom _proposition frozen _backendClass -> frozen foundationAxiomBackendClass :: CheckedFoundation -> FoundationAxiomTag -> FoundationBackendClass foundationAxiomBackendClass foundation tag = case lookupFoundationAxiom foundation tag of CheckedFoundationAxiom _proposition _frozen backendClass -> backendClass lookupFoundationAxiom :: CheckedFoundation -> FoundationAxiomTag -> CheckedFoundationAxiom lookupFoundationAxiom (CheckedFoundation axioms _rules) tag = case Map.lookup tag axioms of Just axiom -> axiom Nothing -> impossible "checked foundation omitted a validated axiom tag" foundationRuleSignature :: CheckedFoundation -> KernelRuleTag -> KernelRuleSignature foundationRuleSignature (CheckedFoundation _axioms rules) tag = case Map.lookup tag rules of Just signature -> signature Nothing -> impossible "checked foundation omitted a validated kernel rule" classifyFrozenCore :: FrozenCheckedCore global -> FoundationBackendClass classifyFrozenCore = classifyCanonicalFofStructure . frozenCoreTerm classifyCanonicalFofStructure :: CanonicalTerm global -> FoundationBackendClass classifyCanonicalFofStructure term = case Set.toAscList (termFofExclusions term) of [] -> FoundationFofProjectable firstExclusion : remainingExclusions -> FoundationRequiresTh0 (firstExclusion :| remainingExclusions) foundationAxiomDependencies :: CanonicalTerm global -> Set FoundationAxiomTag foundationAxiomDependencies = \case CBound{} -> mempty CGlobal{} -> mempty CIntrinsic intrinsic -> intrinsicFoundationAxioms intrinsic COpaqueInteger{} -> mempty CApp function argument -> foundationAxiomDependencies function <> foundationAxiomDependencies argument CLam _binderType body -> foundationAxiomDependencies body CFalsum -> mempty CImp premise conclusion -> foundationAxiomDependencies premise <> foundationAxiomDependencies conclusion CEq _operandType left right -> foundationAxiomDependencies left <> foundationAxiomDependencies right CForall _binderType body -> foundationAxiomDependencies body intrinsicFoundationAxioms :: CoreIntrinsicTag -> Set FoundationAxiomTag intrinsicFoundationAxioms = Set.fromList . \case Member -> [] Empty -> [EmptyCharacteristic] PairSet -> [PairSetCharacteristic] FamilyUnion -> [FamilyUnionCharacteristic] PowerSet -> [PowerSetCharacteristic] Sep -> [SeparationCharacteristic] Repl -> [ReplacementCharacteristic] SetChoose -> [SetChooseWitness] UnivOf -> [] ISetLfp -> [] termFofExclusions :: CanonicalTerm global -> Set FofExclusion termFofExclusions = \case CBound{} -> mempty CGlobal{} -> mempty CIntrinsic intrinsic | intrinsic `elem` [Sep, Repl, SetChoose, ISetLfp] -> Set.singleton (HigherOrderIntrinsic intrinsic) | otherwise -> mempty COpaqueInteger{} -> mempty CApp function argument -> termFofExclusions function <> termFofExclusions argument CLam _binderType body -> Set.insert HigherOrderLambda (termFofExclusions body) CFalsum -> mempty CImp premise conclusion -> termFofExclusions premise <> termFofExclusions conclusion CEq operandType left right -> (case operandType of TyArrow{} -> Set.singleton (HigherOrderEquality operandType) _ -> mempty) <> termFofExclusions left <> termFofExclusions right CForall binderType body -> (case binderType of TySet -> mempty _ -> Set.singleton (HigherOrderBinder binderType)) <> termFofExclusions body allCoreIntrinsicTags :: [CoreIntrinsicTag] allCoreIntrinsicTags = [minBound .. maxBound] allFoundationAxiomTags :: [FoundationAxiomTag] allFoundationAxiomTags = [minBound .. maxBound] allKernelRuleTags :: [KernelRuleTag] allKernelRuleTags = [minBound .. maxBound] expectedKernelRuleSignature :: KernelRuleTag -> KernelRuleSignature expectedKernelRuleSignature = \case SetLfpBound -> KernelRuleSignature [TySet, TySet `TyArrow` TySet] 0 SetLfpLeast -> KernelRuleSignature [TySet, TySet `TyArrow` TySet, TySet] 2 SetLfpFixed -> KernelRuleSignature [TySet, TySet `TyArrow` TySet] 1 SetLfpInduct -> KernelRuleSignature [ TySet , TySet `TyArrow` TySet , TySet `TyArrow` TyProp , TySet ] 3 coverageErrors :: Ord tag => (tag -> error) -> (tag -> error) -> [tag] -> [tag] -> [error] coverageErrors missing duplicate expected actual = [ missing tag | tag <- expected , occurrenceCount tag == 0 ] <> [ duplicate tag | tag <- expected , occurrenceCount tag > 1 ] where occurrenceCount tag = length (List.filter (== tag) actual) firstOne :: (error -> FoundationManifestError) -> Either error value -> Either (NonEmpty FoundationManifestError) value firstOne wrap = either (Left . (:| []) . wrap) Right type FoundationSyntax = CoreSyntax Void Natural foundationAxiomSyntax :: FoundationAxiomTag -> FoundationSyntax foundationAxiomSyntax = \case EmptyCharacteristic -> foralls [(x, TySet)] (iff (member (var x) emptySet) coreFalsum) PairSetCharacteristic -> foralls [(a, TySet), (b, TySet), (x, TySet)] (iff (member (var x) (pairSet (var a) (var b))) (orP (eqSet (var x) (var a)) (eqSet (var x) (var b)))) FamilyUnionCharacteristic -> foralls [(a, TySet), (x, TySet)] (iff (member (var x) (familyUnion (var a))) (exists b TySet (andP (member (var b) (var a)) (member (var x) (var b))))) PowerSetCharacteristic -> foralls [(a, TySet), (b, TySet)] (iff (member (var b) (powerSet (var a))) (subset (var b) (var a))) SeparationCharacteristic -> foralls [ (a, TySet) , (p, TySet `TyArrow` TyProp) , (x, TySet) ] (iff (member (var x) (separation (var a) (var p))) (andP (member (var x) (var a)) (apply (var p) (var x)))) ReplacementCharacteristic -> foralls [ (a, TySet) , (f, TySet `TyArrow` TySet) , (y, TySet) ] (iff (member (var y) (replacement (var a) (var f))) (exists x TySet (andP (member (var x) (var a)) (eqSet (var y) (apply (var f) (var x)))))) SetChooseWitness -> foralls [ (p, TySet `TyArrow` TyProp) , (x, TySet) ] (implies (apply (var p) (var x)) (apply (var p) (setChoose (var p)))) SetExtensionality -> foralls [(a, TySet), (b, TySet)] (implies (subset (var a) (var b)) (implies (subset (var b) (var a)) (eqSet (var a) (var b)))) SetInduction -> forallOne p (TySet `TyArrow` TyProp) (implies (forallOne a TySet (implies (forallOne x TySet (implies (member (var x) (var a)) (apply (var p) (var x)))) (apply (var p) (var a)))) (forallOne a TySet (apply (var p) (var a)))) PropositionalExtensionality -> foralls [(p, TyProp), (q, TyProp)] (implies (implies (var p) (var q)) (implies (implies (var q) (var p)) (coreEquality TyProp (var p) (var q)))) DoubleNegationElim -> forallOne p TyProp (implies (notP (notP (var p))) (var p)) UnivOfContains -> forallOne n TySet (member (var n) (univOf (var n))) UnivOfTransitive -> forallOne n TySet (transitive (univOf (var n))) UnivOfFamilyUnionClosed -> forallOne n TySet (familyUnionClosed (univOf (var n))) UnivOfPowerSetClosed -> forallOne n TySet (powerSetClosed (univOf (var n))) UnivOfReplacementClosed -> forallOne n TySet (replacementClosed (univOf (var n))) UnivOfMinimal -> foralls [(n, TySet), (u, TySet)] (implies (member (var n) (var u)) (implies (transitive (var u)) (implies (familyUnionClosed (var u)) (implies (powerSetClosed (var u)) (implies (replacementClosed (var u)) (subset (univOf (var n)) (var u))))))) expectedFoundationBackendClass :: FoundationAxiomTag -> FoundationBackendClass expectedFoundationBackendClass = \case EmptyCharacteristic -> FoundationFofProjectable PairSetCharacteristic -> FoundationFofProjectable FamilyUnionCharacteristic -> FoundationFofProjectable PowerSetCharacteristic -> FoundationFofProjectable SeparationCharacteristic -> requiresTh0 (HigherOrderBinder (TySet `TyArrow` TyProp)) [HigherOrderIntrinsic Sep] ReplacementCharacteristic -> requiresTh0 (HigherOrderBinder (TySet `TyArrow` TySet)) [HigherOrderIntrinsic Repl] SetChooseWitness -> requiresTh0 (HigherOrderBinder (TySet `TyArrow` TyProp)) [HigherOrderIntrinsic SetChoose] SetExtensionality -> FoundationFofProjectable SetInduction -> requiresTh0 (HigherOrderBinder (TySet `TyArrow` TyProp)) [] PropositionalExtensionality -> requiresTh0 (HigherOrderBinder TyProp) [] DoubleNegationElim -> requiresTh0 (HigherOrderBinder TyProp) [] UnivOfContains -> FoundationFofProjectable UnivOfTransitive -> FoundationFofProjectable UnivOfFamilyUnionClosed -> FoundationFofProjectable UnivOfPowerSetClosed -> FoundationFofProjectable UnivOfReplacementClosed -> requiresTh0 (HigherOrderBinder (TySet `TyArrow` TySet)) [HigherOrderIntrinsic Repl] UnivOfMinimal -> requiresTh0 (HigherOrderBinder (TySet `TyArrow` TySet)) [HigherOrderIntrinsic Repl] where requiresTh0 firstExclusion remainingExclusions = FoundationRequiresTh0 (firstExclusion :| remainingExclusions) x, y, a, b, p, q, f, n, u :: Natural x = 0 y = 1 a = 2 b = 3 p = 4 q = 5 f = 6 n = 7 u = 8 var :: Natural -> FoundationSyntax var = coreLocal apply :: FoundationSyntax -> FoundationSyntax -> FoundationSyntax apply = coreApply apply2 :: FoundationSyntax -> FoundationSyntax -> FoundationSyntax -> FoundationSyntax apply2 function firstArgument secondArgument = apply (apply function firstArgument) secondArgument member :: FoundationSyntax -> FoundationSyntax -> FoundationSyntax member = apply2 (coreIntrinsic Member) emptySet :: FoundationSyntax emptySet = coreIntrinsic Empty pairSet :: FoundationSyntax -> FoundationSyntax -> FoundationSyntax pairSet = apply2 (coreIntrinsic PairSet) familyUnion :: FoundationSyntax -> FoundationSyntax familyUnion = apply (coreIntrinsic FamilyUnion) powerSet :: FoundationSyntax -> FoundationSyntax powerSet = apply (coreIntrinsic PowerSet) separation :: FoundationSyntax -> FoundationSyntax -> FoundationSyntax separation = apply2 (coreIntrinsic Sep) replacement :: FoundationSyntax -> FoundationSyntax -> FoundationSyntax replacement = apply2 (coreIntrinsic Repl) setChoose :: FoundationSyntax -> FoundationSyntax setChoose = apply (coreIntrinsic SetChoose) univOf :: FoundationSyntax -> FoundationSyntax univOf = apply (coreIntrinsic UnivOf) implies :: FoundationSyntax -> FoundationSyntax -> FoundationSyntax implies = coreImplication notP :: FoundationSyntax -> FoundationSyntax notP proposition = implies proposition coreFalsum andP :: FoundationSyntax -> FoundationSyntax -> FoundationSyntax andP left right = notP (implies left (notP right)) orP :: FoundationSyntax -> FoundationSyntax -> FoundationSyntax orP left right = implies (notP left) right iff :: FoundationSyntax -> FoundationSyntax -> FoundationSyntax iff = coreEquality TyProp eqSet :: FoundationSyntax -> FoundationSyntax -> FoundationSyntax eqSet = coreEquality TySet forallOne :: Natural -> CoreType -> FoundationSyntax -> FoundationSyntax forallOne local binderType = coreForall binderType local foralls :: [(Natural, CoreType)] -> FoundationSyntax -> FoundationSyntax foralls binders body = foldr (uncurry forallOne) body binders exists :: Natural -> CoreType -> FoundationSyntax -> FoundationSyntax exists local binderType body = notP (forallOne local binderType (notP body)) subset :: FoundationSyntax -> FoundationSyntax -> FoundationSyntax subset left right = forallOne x TySet (implies (member (var x) left) (member (var x) right)) transitive :: FoundationSyntax -> FoundationSyntax transitive universe = forallOne a TySet (implies (member (var a) universe) (subset (var a) universe)) familyUnionClosed :: FoundationSyntax -> FoundationSyntax familyUnionClosed universe = forallOne a TySet (implies (member (var a) universe) (member (familyUnion (var a)) universe)) powerSetClosed :: FoundationSyntax -> FoundationSyntax powerSetClosed universe = forallOne a TySet (implies (member (var a) universe) (member (powerSet (var a)) universe)) replacementClosed :: FoundationSyntax -> FoundationSyntax replacementClosed universe = foralls [ (a, TySet) , (f, TySet `TyArrow` TySet) ] (implies (member (var a) universe) (implies (forallOne x TySet (implies (member (var x) (var a)) (member (apply (var f) (var x)) universe))) (member (replacement (var a) (var f)) universe)))