Skip to content

WIP: Jcb/formalization2 #4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
johnchandlerburnham wants to merge 21 commits into
base: dev
Choose a base branch
from
Open

WIP: Jcb/formalization2 #4

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
c0b04d7
verify: drop spurious noncomputable markers on singleton replay rows
johnchandlerburnham Aug 8, 2026
48b9980
inductive: compute of_run by replaying the transparent decomposition
johnchandlerburnham Aug 8, 2026
731d0f9
verify: compute staged ofRun packagers by replaying their builders
johnchandlerburnham Aug 8, 2026
ff5ffc7
verify: drop noncomputable markers freed by computable staged owners
johnchandlerburnham Aug 8, 2026
ffe2cd4
verify: add trExprS?, the deterministic shadow of strict translation
johnchandlerburnham Aug 8, 2026
ea73301
verify: compute the generation packages through the deterministic tra…
johnchandlerburnham Aug 8, 2026
e0ee54e
verify: decide the nested inductive representation
johnchandlerburnham Aug 10, 2026
b8899c7
theory: flatten nested inductives against target metadata
johnchandlerburnham Aug 10, 2026
4b3d449
theory+verify: restore nested generation artifacts and align the tran…
johnchandlerburnham Aug 10, 2026
3475370
verify: round-trip real nested addInductive output through the artifacts
johnchandlerburnham Aug 10, 2026
b71ab5c
theory: prove typed transport along constant interpretations
johnchandlerburnham Aug 10, 2026
a77e358
verify: replay the rose nested declaration through TrEnv'.inductNested
johnchandlerburnham Aug 10, 2026
e297560
verify: replay the nested-indexed fixture and close nested generation
johnchandlerburnham Aug 10, 2026
3689b11
theory: prove the generated iota pattern core for certified blocks
johnchandlerburnham Aug 10, 2026
bc51f98
theory: prove pattern soundness and add the block-local assembler
johnchandlerburnham Aug 10, 2026
0587b91
theory+verify: close L4L-11 replay and certificate API
johnchandlerburnham Aug 10, 2026
958d03b
theory+verify: close L4L-12A API extraction
johnchandlerburnham Aug 10, 2026
a6ea75f
theory+verify: close L4L-12B literal readiness
johnchandlerburnham Aug 10, 2026
de7eef7
theory+verify: close L4L-13A/B projection semantics
johnchandlerburnham Aug 10, 2026
c62085d
theory+verify: close L4L-14 projection structural laws
johnchandlerburnham Aug 10, 2026
b2bf43e
docs: refresh formalization roadmap for L4L-14
johnchandlerburnham Aug 11, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 8 additions & 11 deletions Lean4Lean/Audit/SorryFrontier.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,15 +2,19 @@ import Lean4Lean.Theory
import Lean4Lean.Theory.ConstructorValidityFixtures
import Lean4Lean.Theory.Inductive
import Lean4Lean.Theory.InductiveFixtures
import Lean4Lean.Theory.Literals
import Lean4Lean.Theory.LocalContext
import Lean4Lean.Theory.Meta
import Lean4Lean.Theory.MutualInductiveFixtures
import Lean4Lean.Theory.Projection
import Lean4Lean.Theory.Quot
import Lean4Lean.Theory.SingletonParity
import Lean4Lean.Theory.Typing.Basic
import Lean4Lean.Theory.Typing.ChurchRosser
import Lean4Lean.Theory.Typing.Env
import Lean4Lean.Theory.Typing.EnvLemmas
import Lean4Lean.Theory.Typing.HeadReduction
import Lean4Lean.Theory.Typing.InductiveCertificate
import Lean4Lean.Theory.Typing.InductiveLemmas
import Lean4Lean.Theory.Typing.Injectivity
import Lean4Lean.Theory.Typing.Lemmas
Expand All @@ -31,6 +35,7 @@ import Lean4Lean.Verify.Environment.CandidateIdentityReplay
import Lean4Lean.Verify.Environment.ConstructorValidation
import Lean4Lean.Verify.Environment.ConstructorValidityMatrix
import Lean4Lean.Verify.Environment.ConstructorValidityReplay
import Lean4Lean.Verify.Environment.DeepNestedReplay
import Lean4Lean.Verify.Environment.Elimination
import Lean4Lean.Verify.Environment.EliminationFixtures
import Lean4Lean.Verify.Environment.EliminationFixturesCommon
Expand All @@ -46,6 +51,7 @@ import Lean4Lean.Verify.Environment.IndexedVecConstructors
import Lean4Lean.Verify.Environment.IndexedVecOuterReplay
import Lean4Lean.Verify.Environment.IndexedVecSemanticReplay
import Lean4Lean.Verify.Environment.InductiveFixtures
import Lean4Lean.Verify.Environment.InductiveReplayMatrix
import Lean4Lean.Verify.Environment.Lemmas
import Lean4Lean.Verify.Environment.MutualInductiveFixtures
import Lean4Lean.Verify.Environment.Normalization
Expand Down Expand Up @@ -126,17 +132,7 @@ private def surfacePrefixes : Array Lean.Name := #[`Lean4Lean.Theory, `Lean4Lean
S (missing specification), P (stated but sorried, blocked on S), V (checker
verification, blocked on S/P), R (research-grade metatheory, upstream-driven). -/
private def allowlist : Array Lean.Name := #[
-- Tier S — missing specification
`Lean4Lean.TrProj,
-- Tier P — blocked only on Tier S
`Lean4Lean.TrProj.weak',
`Lean4Lean.TrProj.weak'_inv,
`Lean4Lean.TrProj.defeqDFC,
`Lean4Lean.TrProj.wf,
`Lean4Lean.TrProj.uniq,
`Lean4Lean.TrProj.instN,
`Lean4Lean.TrProj.instL,
-- Tier V — checker verification, blocked on Tiers S/P
-- Tier V — checker verification, blocked on Tier P
-- (NormLevel.subsumption_eval and Level.isEquiv_wf were proved on the
-- formalization line, 2026-08-05/07, and left the frontier.)
`Lean4Lean.addDecl.WF,
Expand All @@ -150,6 +146,7 @@ private def allowlist : Array Lean.Name := #[
`Lean4Lean.VEnv.IsDefEqU.forallE_inv_stratified,
`Lean4Lean.VEnv.IsDefEqU.sort_forallE_inv,
`Lean4Lean.VEnv.IsDefEqU.weakN_iff,
`Lean4Lean.VEnv.WF.registeredStructureHeadInversion,
`Lean4Lean.VEnv.NormalEq.parRed,
-- Tier F — deliberately kernel-rejected inductive fixtures. Elaborator error
-- recovery admits the invalid `inductive` with `sorryAx`, so the constant
Expand Down
Loading