[v0.4] Author the production compiler itself in LexLean and verify the generated Lean implementation

Scope

Replace the normative production compiler implementation with LexLean-authored source.

Work

Express the production IR, lowering, certification, optimization, Rust AST, rendering, and diagnostics using language 1.2 constructs.
Generate the compiler's Lean implementation exclusively through LexLean.
Verify the generated compiler with the same Lean elaboration, leanchecker replay, exact axiom audit, source maps, coverage, and deterministic identity machinery used for other LexLean programs.
Keep bootstrap/oracle tooling outside the normative semantic source.

DoD

No handwritten Lean or handwritten Rust contains normative compiler semantics.
Compiler source is ordinary closed .lex.tex/semantic-module content and can be snapshotted like any other project.
Compiler build is reproducible and content-addressed.
Any host/runtime adapter is minimal, typed, and explicitly outside semantic logic.

Acceptance criteria

A clean checkout builds and verifies the compiler from LexLean source.
The resulting compiler successfully compiles a nontrivial corpus of other LexLean programs.
Editing generated Lean/Rust cannot become authoritative; regeneration restores canonical artifacts.
A planted compiler-source vs generated-artifact drift is caught by gates.
Full just vv passes.

Depends on #17-#25.

PrismPM adoption review of c21dd7e09afe6c4253af3cf56d8c67bc99b3f771 identifies a concrete issue27 dependency. The full upstream VV/package qualification does not discharge it.

The normal package includes language/lcnf-1.2/extract.lean; production/lcnf.rs embeds this handwritten metaprogram verbatim. PrismPM's complete source audit refuses handwritten Lean in the admitted dependency. Main 0e7e84f8bcbb83d7e9534d42b6a1b08339975a99 retains the same adapter. Removing it from the archive, exempting its path or accepting an opaque Lean-text escape hatch would not correct this boundary.

Required correction:

Register generic, closed compiler-tooling semantics for typed authority calls, meta/environment execution, entrypoint registration and the complete recursive traversal. Add the required scenario and real fail-first conformance before implementation; preserve R1–R10.
Define the adapter through LexLean's semantic model and generate its temporary Lean with the normal compiler. No handwritten Lean/template or authority-name allowlist may bypass semantic typing, source mapping or closure.
Preserve all NE01–NE06 obligations: exact named roots, complete code/kernel/erased-proof dependency closure, exact signatures/constructors/constants, Lean identity, base-phase translation with no subsequent LCNF pass, drift refusal and actual process evidence. Update §22.10, compiler-semantics identity and package/generated records together.
Preserve every existing extraction/VV/package owner and negative. Include forged signature/constructor/constant drift, malformed output, missing dependencies, wrong authority identity and handwritten/opaque adapter refusal. Require two-root/source-mapped generated-adapter equivalence against the pinned real Lean authority, complete original VV/package and independent review.
PrismPM adopts the complete normal package only after its unchanged source audit, generated applications, real Hologram owner, native lanes, immutable SDK and downstream criteria pass. No exception, subset archive or partial-gate result is acceptance.

The pinned lean4-prod extractor is not a drop-in replacement: its d.simp {} step and output/closure semantics differ from LexLean §22.10. This is an implementation dependency, not permission to defer PrismPM's native execution or model/compiler work.

Stage 1 design for the "Required correction" above (proposal; work proceeds unless objected to)

Per the maintainers' decision, #27 is delivered in staged PRs and stays open until its whole definition of done holds. Stage 1 is the correction in the comment above: the extraction adapter is LexLean-authored and generated by the normal compiler.

What the survey found

language/lcnf-1.2/extract.lean is 368 lines of real metaprogramming (JSON emitters, mutual traversals of Expr/Code/FunDecl/Alt, NameSet closures, a command elaborator, a worklist in CoreM, environment queries), pinned by authority.toml (61 calls with exact signatures, 75 types with complete constructor lists, a plumbing list). production/lcnf.rs embeds it verbatim.
The current semantic IR cannot express it: no foreign types or calls, no effects, no partial or termination-free mutual recursion, flat patterns only, no Char/string append, a hard-coded module header, and the generated-Lean token audit forbids IO, #eval and character literals. Extending the ordinary semantic modules would mean threading each new variant through about 27 exhaustive matches (term) or about 42 arms (declaration), including the three audited production files that this tooling will never reach.

Proposal

A third module kind, the tooling module, modelled on coremodule: \begin{toolingmodule}\toolingdata{…}\end{toolingmodule}, canonical JSON lexlean/tooling-module/1, language 1.2 only, never production-eligible, refused in user projects and accepted only for compiler-embedded tooling projects. Both backends derive from the one linked value (R8).

Typed authority calls. authority, type (parameters, exact constructor list with typed fields, per-constructor index constraint for families such as LetValue .pure), call (structured exact signature: binder kinds, defaults, universes; pinned source file and SHA-256) and plumbing are declarations. They replace authority.toml as the single source; the lexlean_signature probes and the both-directions registry check are generated from them.
Meta/environment execution. function declarations (meta phase, optional partial, mutual groups) over a closed, explicitly typed term language: literals, let, lambda/apply, flat exhaustive match over authority constructors (index-aware), if, constructor application, field projection, and calls with explicit type arguments. Monadic sequencing is only typed authority calls (Bind.bind, Pure.pure, …). There is no raw Lean text and no do text.
Entrypoint registration. command declarations generate syntax plus @[command_elab] from structured grammar atoms; invoke and evaluate declarations, which the host builds as semantic data, replace the driver's text template.
Complete recursive traversal. A function group may be declared a traversal of an authority type; linking then requires every type of its closed field-type closure to be matched exhaustively and every constructor of it handled, so a traversal cannot silently skip a constructor. A registry change that adds one is a link error, not a silent omission.

Evidence and obligations kept

NE-01..06 and every existing extraction, VV and package owner and negative are kept and retargeted (the NE-04 drift plants mutate the generated adapter instead of the handwritten one); forged signature, constructor and constant drift, malformed output, missing dependencies, wrong authority identity and a handwritten or opaque adapter are refused.
The previous handwritten adapter moves out of the packaged tree into a test oracle. The generated adapter must equal it byte for byte on the real corpus for two roots, with source-mapped generated Lean, before it replaces it. §22.10, the compiler-semantics ID and the package and generated records are updated together.
New capability IDs follow R3 (register row, SPEC §31 row, one scenario, one failing named test, then the implementation) with planted-defect records in VERIFICATION.md.

Delivery

Two PRs, because each changes the 1.2 compiler-semantics ID and so regenerates every lock and golden: 1a the tooling-module language (IR, checker, both backends, linking, conformance IDs, fixtures verified by real Lean), 1b the adapter, driver, retargeted NE owners and the removal of the handwritten Lean from the package. The remaining stages (production IR, lowering, certification and rendering in LexLean) stay under this issue.

Decision wanted from the maintainers, not blocking 1a: language/preservation-1.2/library/ holds 13 handwritten .lean files (about 526 KB; SPEC §17.17 declares them handwritten by design) and the same "no handwritten Lean in the admitted dependency" audit would flag them. Is it in scope for #27's definition of done, or is it a separate, declared exception?

Generated by Claude Code

feat(tooling): closed compiler-tooling modules and the extraction ada…

Reopened. Merging #78 closed this issue automatically: the PR description said it does not close #27, but GitHub's closing-keyword parser ignores the negation. #78 is stage 1 only (the tooling-module language and the extraction adapter written in it), and this issue's definition of done is not met.

Per the maintainers' answer on the open question, handwritten Lean is out of scope as normative content, so language/preservation-1.2/library/ (13 handwritten .lean files) is part of this issue's definition of done: it has to be generated from LexLean, not carried as authored Lean. I will post the survey and the staged plan for that next, before any implementation.

Generated by Claude Code

Plan for the rest of #27 after stage 1 (#78), and what starts now

Per the maintainers' answer, handwritten Lean is out of normative content, so the preservation library (13 files, 934 registered declarations) and compiler/proofs/LexLeanCertification (13 files, 107) are in this issue's definition of done. Each stage below gets its own child issue with its own DoD and acceptance criteria, and its PR is merged only when its checks pass and that child's criteria are verified.

What is handwritten and normative today (survey of `main` at `ba52c601`)

Lean: the two libraries above; Lean text templates in Rust for certificates A, B, E and the audit modules (production/certificate.rs ~570 format!, rust_cert.rs, rust_term.rs, preserve.rs); the fixed Lean runtimes the backend splices into generated modules (backend/semantic.rs, ~700 lines, and core.rs, lean.rs).
Rust: the production pipeline (production/*.rs, ~23k lines) and the target calculus (calculus/**, ~11k lines), whose models in compiler/ are already LexLean but whose lowering, rendering and certificate generation are not; the ~255-line Rust runtime text.

The route for the libraries already exists

SPEC §17.10 and examples/uor-atlas/MIGRATION.md record how an elaborated Lean library becomes LexLean source: a one-time lossless export into native core-module/1 data, committed as .lex.tex, with both backends generating from it and the exporter absent from the release tree. I measured the preservation library under the pinned Lean: it compiles in about 2 minutes and has 8,916 environment declarations and about 334k unique kernel expression nodes, the size class of the Atlas migration (24 MB), not beyond it. So I will use that route and not re-author ~800 theorems in a proof language that cannot state the evaluator.

Stages

Libraries as native core modules (starting now). Equivalence evidence: re-exporting the regenerated environment equals the original export, declaration by declaration; certificates A/B/E and the registered axioms are unchanged; the SPEC's quoted statement vocabulary and the correspondence audit are re-pointed at the generated artifacts; a permanent gate extends VR-19's "no independently authored Lean" condition to the 1.2 libraries.
Certificates A, B, E and audit modules built as typed core-module data, so no Lean text template remains in the production compiler.
Backend fixed runtimes generated through native modules (this touches generated Lean of 1.1/1.2 projects, so I will state the compatibility treatment in that child issue first).
Rust runtime and package text generated, or declared as the minimal typed adapter.
Production compiler logic (eligibility, lowering, certification, Rust AST and rendering) authored in language 1.2, with the Rust modules kept only as oracles under tests/ until byte-identity gates pass, then removed.

Decisions needed before stage 5 (not blocking stages 1–4)

Execution engine. I recommend the generated Lean built by the pinned toolchain and driven by a typed host adapter (bytes in, bytes out).
"Production IR." The Rust pipeline today consumes the semantic IR, not compiler-input/2 (only verify publishes it, and nothing consumes it); SPEC §22.10 speaks of LCNF. I recommend the semantic IR.
Authoring surface. The calculus is already authored as Rust builders that render committed .lex.tex and are checked by check-calculus. I read the DoD as satisfied when the committed .lex.tex is the normative source and the generator is bootstrap tooling outside it; please say if you read it differently.

Generated by Claude Code

fix(production-export): regenerate the committed packages for main's …

feat(api): production export contract and stable compiler API (#28) (#76

Merge pull request #80 from UOR-Foundation/claude/trusting-ramanujan-…

Status after stage 2 (#79: PRs #80 and #86, both merged; neither proof library is handwritten Lean any more), and the remaining stages as child issues:

delivery stage	issue	decision wanted before it starts
1 tooling modules and the extraction adapter	#78, merged	none
2 proof libraries as native core modules	#79, closed	none
3 certificates A, B, E and the audit modules as typed data	#89	the route (explicit-argument library forms, or generic soundness theorems with decided side conditions, per certificate kind)
4 the backend's fixed Lean runtimes through native modules	#90	how languages 1.0 and 1.1, whose output must stay byte-identical, are treated (a declared frozen-bytes exception, or closing them to new projects)
5 the Rust runtime and package text	#91	whether a declared, typed, bidirectionally gated runtime adapter satisfies "no handwritten implementation" for the trusted Rust runtime
6 the production compiler's logic in language 1.2	#92	the three decisions of the plan (engine, "production IR", authoring surface)

#89 can start without an answer (its first step, certificate A and the audit module, is the same under either route); the others wait for the decision in their last section. Stage 3 changes every language-1.2 identity, so it follows #88 (the rust-std ownership and list rendering, #81), which is in CI.

One consequence of stage 2 for #84: the RustSyntax/RustSemantics edits #84 describes now meet a preservation library that is native kernel-term data, so a change to the machine has to be re-proved in that library; I have put the question on #84.

Generated by Claude Code

Maintainer decisions on the open questions (2026-10-14), and the plan they imply

Recorded from the maintainers' answers, so that they are durable:

LexLean has to include its own authoring surface. The sources of the compiler, the libraries and the models are authored today as Rust builders in crates/conformance that render \semanticdata{…JSON…}; the repository does not contain a way to write them. Part of [v0.4] Author the production compiler itself in LexLean and verify the generated Lean implementation #27 therefore includes a LexLean SDK/API (or equivalent), so the repository owns its authoring surface. .lex.tex is the only authorized authoring surface: nothing else is normative, and no other tool's output is a source.
[v0.4] #27 stage 5: certificates A, B, E and the audit modules as typed data, with no Lean text template in the production compiler #89 (certificates A, B, E as typed data): the recommended route is accepted (generic soundness theorems with decided side conditions for certificates A, E and the audit module; explicit-argument forms for certificate B).
[v0.4] #27 stage 4: the backend's fixed Lean runtimes generated through native modules #90 (backend fixed Lean runtimes): accepted. Language 1.2 gets native modules; languages 1.0 and 1.1 keep their frozen released bytes as a declared exception, tested against the released output.
[v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91 (Rust runtime): the closed AST is to be completed so that the runtime is generated from the calculus. There is the LexLean way and all others, and the LexLean way is chosen: no declared trusted adapter.
[v0.4] #27 stage 8: the production compiler authored in .lex.tex and compiled by LexLean to production software #92 (production compiler): production concerns are LexLean → production software. Lean 4 verifies LexLean and has nothing to do with the production environment, so the execution engine is not generated Lean; the compiler is a LexLean program compiled by LexLean's own production pipeline. .lex.tex is the only authoring surface.
[v0.4] perf(backend): borrowed projections, fold as a runtime item, and list views as borrows in the rust-std machine (follow-up to #81) #84 is ordered after the authoring surface and is not started before it.
The maintainers' standing permission covers managing branches, issues and PRs as needed.

Revised delivery order

stage	issue	what	depends on
1	#78, merged	tooling modules and the extraction adapter
2	#79, closed	proof libraries as native core modules
3	new (below)	the authoring surface and SDK: human-writable `.lex.tex` for semantic, core and tooling modules, a public API, round trip with the canonical data, every committed source migrated
4	#90	backend fixed Lean runtimes as native modules (1.2)	can start in parallel with 3 (a one-time export, as #79)
5	#89	certificates A, B, E as typed data	3 (new library theorems are authored in the surface)
6	#91	the closed Rust AST completed; the runtime generated from the calculus	3 (it changes the machine and its proofs)
7	#84	borrowed projections, fold as a runtime item, region rule	3, 6
8	#92	the production compiler authored in `.lex.tex` and compiled to production Rust	3, 4, 5, 6

The authoring surface is the critical path, and it is next. I will post its design as an issue before implementing, in the manner of the stage 1 design, and start with the part every later stage needs (the semantic-module surface with a lossless round trip).

Generated by Claude Code

feat(surface): the language-1.2 authoring notation for semantic modul…

Merge pull request #94: the language-1.2 authoring notation for seman…

Recorded as item L2.1 of the completion plan #106. Two plan items depend on it: L1.3 (#111, the specification and register as LexLean source) needs #93, and L4.7 (#125, the compiler carrying its own optimality certificate) needs the compiler as a production root. L5.1 (#126, SHA-256 in LexLean) is part of this issue's rule that no handwritten code carries normative semantics.

Generated by Claude Code

Navigation Menu

Repository navigation

[v0.4] Author the production compiler itself in LexLean and verify the generated Lean implementation #27

Scope

Work

DoD

Acceptance criteria

Stage 1 design for the "Required correction" above (proposal; work proceeds unless objected to)

What the survey found

Proposal

Evidence and obligations kept

Delivery

Plan for the rest of #27 after stage 1 (#78), and what starts now

What is handwritten and normative today (survey of `main` at `ba52c601`)

The route for the libraries already exists

Stages

Decisions needed before stage 5 (not blocking stages 1–4)

Maintainer decisions on the open questions (2026-10-14), and the plan they imply

Revised delivery order

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

[v0.4] Author the production compiler itself in LexLean and verify the generated Lean implementation #27

Description

Scope

Work

DoD

Acceptance criteria

Activity

afflom commented on Oct 6, 2026

afflom commented on Oct 12, 2026

Stage 1 design for the "Required correction" above (proposal; work proceeds unless objected to)

What the survey found

Proposal

Evidence and obligations kept

Delivery

afflom commented on Oct 13, 2026

afflom commented on Oct 13, 2026

Plan for the rest of #27 after stage 1 (#78), and what starts now

What is handwritten and normative today (survey of main at ba52c601)

The route for the libraries already exists

Stages

Decisions needed before stage 5 (not blocking stages 1–4)

afflom commented on Oct 14, 2026

afflom commented on Oct 14, 2026

Maintainer decisions on the open questions (2026-10-14), and the plan they imply

Revised delivery order

afflom commented on Oct 15, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

What is handwritten and normative today (survey of `main` at `ba52c601`)