WIP: New Ix.Kernel in Lean with certification of consistency based on Con-Leche - #638
Open
johnchandlerburnham wants to merge 3 commits into
Open
johnchandlerburnham wants to merge 3 commits into
johnchandlerburnham wants to merge 3 commits into
Conversation
… audits Port the address-native set model (58 modules) from the jcb/ix-kernel-consistency branch at ad60e5f6 into Ix.Kernel.Model with only the namespace rename and a provenance header per file. Split Ix.Address into the pure key (Ix.Address.Core), the host module, and Ix.Address.Pure over the Blake3 package's pure implementation (pin bumped to 18b4b1c8). Add the K0 kernel scaffold: Env, Config/Error/Decl, a declining checkDecls, and the public theorems check_has_model, checkDecls_has_model, and no_proof_of_False with their statements frozen. Add the audits (exact axiom sets, import allowlist, runtime closure, negative controls), the provenance manifest and checker, the IxKernel Lake target, the check-kernel gate, and the ported Models/SetTheory package (not yet built here). lake run check-kernel passes.
…cks, structures, literals, quotients, and the standard axioms, with the Lean-core closure, the standalone kernel package, and letE Kernel package and closure: - IxKernel/ Lake package over the shared Ix/ sources, depending on nothing; Models/SetTheory depends on it alone. - Import trim: Lean.Level and Batteries are gone; the closure of Ix.Kernel is Init plus the kernel and Ix.Address.Core. - letE in VExpr/AExpr with substitution semantics, TypingClaim.letE, ConversionClaim.zeta, and cases through the model. K1: - Ix.Kernel.Level, Claims, Infer (proof-carrying step/whnf/inferA/isDefEqCore/isDefEq), Annotate (unverified regime pass validated by inferA; fuel and ill-typedness reported separately). - Env: Model carries Environment.WF; StepClaim. Check: checkDeclC installs single safe definitions, theorems, and opaques with the model extension; check/checkDecls erase the proof component. - Consistency: the three public theorems re-proved over the real fold; statements unchanged. K2, ordinary inductives: - Ported the old branch ordinary route (Ix.Kernel.Certified.Ordinary, Certified.Telescope, Inductive.Levels): no input store, the recursor at member 1 of the family block (Ixon muts layout), inference in place of witness validation. - Read.lean: unverified shape reader; a block is accepted only when it equals the block generated from its shape. - Inductive/Ordinary.lean: installation with the model extension and the list/overlay environment bridge. - Iota in whnf through published rule equations with typed endpoints (ConstantFact.typed) and arities (ConstantFact.recursor); constructor parameters and indices are converted against the recursor. - K-like reduction: a recursor with a single field-free rule reduces on a non-constructor major by synthesizing the constructor from its parameters; the major converts to it by proof irrelevance. K2, structures: - Ported the structure route (Ix.Kernel.Certified.Structure, Certified.Signature): projection facts, eta and iota equations on the family entry with a ConstantFact.structure carrying the arities; rules typed in the published environment. - Kernel: projection typing through the projection facts, projection iota and structure eta through the equations with rule endpoints typed by inference; proof irrelevance factored out. - Structure/Read.lean: description reader with inferred field sorts; Inductive/Structure.lean: installation with the model extension. K2, Nat: - Literals name their family on raw and annotated syntax (natLit r n); no pin in Config or Env. - Ported the Natural route (Ix.Kernel.Certified.Natural): the exact zero/successor block gets the natural fact, whose meaning gains the successor function membership (NaturalMeaning.succApp) needed for well-denoted literal unfolding; Inductive/Natural.lean installs it. - Kernel: literal typing at the family, one-step literal unfolding against constructors in conversion and for recursor iota majors. K2, quotients: - Model: ConstantFact.quotient/quotientLift with meanings pinning the former, constructor, and lift values (Model/QuotientValues.lean); Basis/Interface and Basis/Equality ported model-only (the Eq shape and its checked-block link split into Basis/EqualityChecked) so the kernel core can read the equality interface. - Ported Certified/Quotient Syntax and Reading with one reading per pinned value; Quotient/Install.lean installs the former, constructor, lift, eliminator, and Quot.sound one entry at a time, each from its exact generated declaration. - No computation rule is published: liftRule_claim derives the lift's rule from the published facts and the admitted Eq interface, indRule_claim holds outright; the kernel's quotIota reduces through them with endpoints typed by inference (reduceByRule). K2, standard axioms: - Ported Basis/Iff, Basis/Nonempty, and Certified/Standard Realization; Standard/Checked adapted to a reference and a Spec with checkSort; Standard/Install.lean installs propext and Classical.choice with the point and a choice function as values. - Check: axiom arms admit propext over Eq and Iff and Classical.choice over Nonempty (family at member 0, constructor 0, recursor at member 1), and Quot.sound; other axioms decline. Fixtures: definitions; False, True, And, Or, Nat, List, Eq with a hand-encoded Nat block equal to the generated one, Nat.rec arithmetic under Eq.refl, and K-like reduction; Prod, And, a dependent subtype, and a proposition with a data field, with projection typing, projection iota, structure eta, and rejections; literals at Nat, 3 = succ 2, add 2 2 = 4 through literal majors, and rejections; the five quotient primitives with Quot.lift f h (Quot.mk a) = f a by Eq.refl and rejections; propext and Classical.choice over their interfaces, each used, and rejections. Audits: runtime closure 757 compiled functions, 14 inherited externs, 1 inherited unsafe (Array.ugetBorrowed via List.zipIdx); statements and axioms unchanged. Provenance: 97 ported, 24 authored modules, source hashes verified. lake run check-kernel --with-model passes.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
description tbd