[v0.4] #27 stage 8: the production compiler authored in .lex.tex and compiled by LexLean to production software

Child of #27; plan in this comment, re-scoped by the maintainers' decision of 2026-10-14 (#27 comment). Delivery stage 8, the last.

Decisions (made by the maintainers)

The concern is LexLean → production software. Lean 4 verifies LexLean and has nothing to do with the production environment. The earlier recommendation on this issue (the compiler's execution engine is generated Lean driven by a typed host adapter) is withdrawn: the compiler is a LexLean program compiled by LexLean's own production pipeline to production Rust, and that Rust is the compiler that runs.
.lex.tex is the only authorized authoring surface of LexLean. The compiler's logic is committed as .lex.tex; Rust builders, Rust modules and JSON generated by tools are not sources.
"Production IR" is the semantic IR (the maintainers did not object to the recommendation, and it is what the pipeline consumes today); to be confirmed in the first sub-stage.

Scope

The production pipeline is Rust: production/ (23,522 lines: certificate.rs 8,796, lower.rs 3,682, eligibility.rs 3,350, rust_cert.rs 2,348, preserve.rs 1,725, lcnf.rs 1,727, source.rs 893, mod.rs 626, rust_term.rs 375) and the target calculus calculus/ (about 11k lines with calculus/rust/): eligibility, lowering, certificate generation, the Rust AST, lowering, validation, printing, packaging, and the compiler's own front end. After this issue that logic is authored in language 1.2 .lex.tex, certified as a production root, and rendered to a Rust package by the compiler it implements.

Self-hosting acceptance (the bootstrap)

Stage 0: today's Rust compiler (the oracle, kept under tests/ until the fixed point).
Stage 1: stage 0 compiles the .lex.tex compiler to a certified Rust package; its provenance binds the source, certificates A, B, E and the runtime.
Stage 2: stage 1 compiles the same .lex.tex compiler.
Fixed point: stage 2's package is byte-identical to stage 1's, and stage 1 equals stage 0 on every committed project, corpus, fixture and golden (differential, byte for byte), and on the Atlas verification records. Only then are the Rust modules removed.

What it needs (inventory, to be refined in the first sub-stage)

A way to write the compiler: the authoring surface (stage 3 of [v0.4] Author the production compiler itself in LexLean and verify the generated Lean implementation #27), with module structure, strings, bytes, maps and sets, sorting, canonical JSON, SHA-256, and diagnostics expressed as production-eligible LexLean (stdlib members, certified, not host calls where avoidable).
Effects at the boundary: reading files, writing files, running Lean for verification, process exit. These need a defined, minimal, typed entry for a production root (arguments, a file system capability, a child process capability), itself part of the language rather than a handwritten shim; the first sub-stage fixes its design.
Stages 4 to 6 ([v0.4] #27 stage 4: the backend's fixed Lean runtimes generated through native modules #90, [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, [v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91) first: the runtimes, certificates and the Rust runtime are generated, so the compiler's output contains no handwritten code.

Proposed order inside this stage

Boundary and effects design (a short design issue, then implementation); the capability set.
Library needs as stdlib members: strings, bytes, maps, sorting, JSON, SHA-256.
Pilot: the preservation lexer and token audit (preserve.rs), and the axiom-audit parser: small, closed, with a differential against the oracle.
calculus::check and rust::{lower, validate, print, package}.
The production registry, eligibility, source and lowering stages.
Certificates (after [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).
Front end (lexicon, grammar, linking), then the fixed point and removal of the Rust modules.

DoD (whole stage)

The production compiler's logic exists only as .lex.tex; the Rust of those modules is absent from the release tree.
The fixed point above holds on the normative host, and the compiler that ran just vv is the one LexLean built.
The differential against stage 0 is byte-identical on every committed root and corpus before removal.
Lean verifies the compiler's certificates; no Lean text is produced by or consulted at compile time of production output.

Acceptance criteria

Per sub-stage: equivalence evidence, planted defects turn named gates red, languages 1.0/1.1 byte-identical, 1.2 identities regenerated, full just vv.

#92 spike: what a compiler component needs today, and the boundary/effects design

Measured on main at 2fd1c1e9 (after #103), with the release binary, in a scratch project (not committed). The question the spike answers: can a pure piece of this compiler be authored in .lex.tex, verified by Lean, compiled by LexLean's own production pipeline to Rust, and agree with the Rust it replaces? The answer is yes for byte-level algorithms today. The rest is the list of what is missing, with an owner for each item.

1. The pilot

Three production roots in one language-1.2 module, authored in the readable notation (no JSON, no Rust):

root	replaces	shape
`isClosedLeanName(raw : Bytes) : Bool`	`ir::core::validate_name` (ASCII Lean-name grammar; used by the axiom-output parser, §22.5)	a 3-state byte machine, `iterate_until` over `raw`
`splitOnByte(subject : Bytes, delimiter : UInt8) : List Bytes`	`str::split` / the line splitter	`iterate` with `(position, start, pieces)` state, `list_fold` to reverse
`startsWith(subject, prefix : Bytes) : Bool`	`starts_with` / `strip_prefix`	`iterate` over the prefix

Results, all with the pinned Lean 4.32.1:

lexlean check: eligible for rust-std with effects: [allocation, overflow]. rust-core is refused with LLT4005 ("type.bytes requires heap allocation"), so a compiler is a rust-std program.
lexlean verify: 16 theorems by reflexivity{} (accepts/rejects of names, splits, prefixes) pass the kernel; the axiom audit is exact per declaration (Quot.sound, propext for the UInt8 range checks and what depends on them, none for the rest).
lexlean production build: 3 certified Rust packages (certificates A, B, E accepted). Wall clock 3m25s for one root and 4m30s for three, almost all Lean.
Differential against plain Rust, on the generated crates: 1,000,000 random names against a hand-written validate_name (alphabet biased to the grammar's boundaries, plus every byte in first and later position), 1,000,000 splits against slice::split, 1,000,000 prefix tests against starts_with: no disagreement. This is the shape of evidence [v0.4] #27 stage 8: the production compiler authored in .lex.tex and compiled by LexLean to production software #92's stage 0 oracle gives.

2. What is missing, by owner

A. A defect found, filed as #105 (part of the path, needs to land before #92 stage 3). iterate, iterate_until and list_fold (and the other 17 library templates) are realized as self-recursive Rust functions, yet the registry rows say recursion = false. A root that scans a 80,000-byte name aborts with a stack overflow on an 8 MiB stack while declaring no recursion effect. A compiler whose loops are all folds over 48 MB modules cannot run until the templates are loops, or the effect is honest and the host provides the stack. #105 has the repro, and the fix in two steps (true now; cheap later with a loop construct, which is #91 stage 3).

B. Primitive semantics the pilot had to work around (stdlib stage, with #90/#91's calculus work; no hurry, none blocks a pilot):

No widening conversion. checked_convert must target a fixed width, so a UInt8 cannot become a Nat. Character classes were written as checked_subtract byte low / checked_subtract high byte both some, which works and is how the stdlib must say it until there is a to_nat.
No Ordering literal or match. compare_bytes a b can only be compared with another compare_bytes (compare_bytes 0x 0x as "equal").
Strings are opaque. No scalar iteration, only utf8_encode/utf8_decode/split_exact/join. Components should work on Bytes; the stdlib's text functions (startsWith, endsWith, trim, lines, splitOn, joinWith, find) are then ordinary members over bytes.
Bytes and text primitives are not kernel-reducible. rfl fails on equal of Bytes, compare_bytes, utf8_encode, split_exact, join, format_decimal, parse_decimal (it succeeds on length, index, slice, append, the fixed-width operations, Nat, String equality). Cause: LexLeanRuntime.compareBytes is compare left.toList right.toList, and ByteArray.toList, ByteArray.instBEq and String.toUTF8 are core definitions that the module system does not expose to a downstream module; the runtime's own definitions are @[expose] but bottom out in them. So a theorem about text processing stated as an equation cannot be discharged by evaluation. Remedy: define those operations in the runtime over exposed structural definitions (fuel-indexed over data[i]?, as LexLeanCollections does for its key order), which is a runtime-content change (identity regenerates) that must agree with the calculus' compare. Until then the compiler's text logic is validated by differential against stage 0, not by in-language theorems.
Authoring friction worth fixing in the surface, not the language: Nat subtraction only as prim subtract, + needs parentheses, lambda captures are explicit and must be sorted, and an exact axiom policy reports one violation per verify, so aligning N declarations costs N runs (a mode that lists every mismatch would be one run).

C. Not expressible at all, by design: effects. Everything above is a function from data to data. The compiler also reads and writes files, lists directories, reads a few environment variables, runs lean/lake/leanchecker under a time and output limit, and exits with a code. #92 asks for "a defined, minimal, typed entry".

3. Proposal: the effects boundary (for the maintainers' decision)

The program is a pure state machine; a generated driver performs the requests. No effect enters the calculus.

Request  := ReadFile path | WriteFile path bytes | ListDir path | Stat path | MakeDir path
          | Rename from to | Remove path | Environment name
          | Run argv env limits       -- limits = the config's child_timeout_ms, max_child_output_bytes
          | Emit stream bytes         -- stdout / stderr
Response := Contents bytes | Listing (List entry) | Info stat | Done | Missing | Denied reason
          | Exited code stdout stderr | Value (Option bytes) | Failed reason
Step S   := Finished code | Ask Request S
root start  : Arguments -> Step S                         -- S is first-order data
root resume : S -> Response -> Step S

A root takes and returns first-order data (§17.13 rule 1), so the continuation is data: a defunctionalized state, which is how the compiler already organizes its phases (a record of what is done and what is next).
The driver (perform : Request -> Response in a loop) is the only code that touches the host. It is part of the Rust machine: a runtime profile item in RustSyntax, authored in .lex.tex as [v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91 stage 4 makes the runtime source, with the Rust standard-library calls it uses on the closed list of machine primitives [v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91 stage 1 fixes (file read/write, std::process::Command with a timeout, env::var). This is not a new trust category: it is the same kind of item as tick.
Semantics. TargetSemantics and the preservation certificates cover the pure functions start and resume, for every response sequence (the compiler is correct against any host behaviour, including Denied and Failed). The claim that the driver performs the request is a table of machine primitives with stated meanings and a differential, at level build, never some-true: honest in the same way the work counter is.
Determinism (R10). No clock, no randomness, no ambient state: the environment is read only through Environment name for a closed list of names. Output order is the order of requests. The existing deterministic-artifacts gates therefore apply unchanged.
Effect registry. allocation, overflow and recursion stay what they are (resource failures of the pure function). I/O is not a fourth effect; it is the Ask data a root returns. A host profile is a new registry entry beside rust-core/rust-std (call it rust-host: rust-std plus the driver), so a root that does not use the entry stays a library and the driver exists only where a program asks for it.
Parallelism is not semantics. Today's compiler uses all cores in places (reading the identity of language 1.2: 0.8 s on four cores). The first realization is sequential; a map over independent items that the driver may evaluate in parallel is a later, separate addition with its own determinism statement. [v0.4] #27 stage 8: the production compiler authored in .lex.tex and compiled by LexLean to production software #92's performance gate should be a measurement (a regression bound on just vv), not a promise.

Alternatives considered: (a) an effect monad inside the calculus (rejected: it puts state and failure into TargetSemantics and re-proves every certificate); (b) a typed host-function table callable from any closure member (rejected: it makes purity a convention, and the eligibility analysis could not tell a pure member from an effectful one); (c) world-passing (World -> (a, World)): equivalent to the state machine but needs a nominal World and linearity, which the calculus does not have.

4. Stdlib and order

The stdlib is source (.lex.tex, language 1.2, certified), a package of modules the compiler project imports: bytes and text over Bytes (item B3), sorting and Map/Set-based dedup (the collections exist; they are templates, so #105 first), canonical JSON, decimal and hex, SHA-256 (expressible today over UInt32 bit operations and iterate; to be measured, because the digest is on the hot path of every build), a diagnostic record and the closed error model's constructors.

Proposed order, replacing my earlier list:

Land production: the collection and iteration primitives are realized by self-recursive functions but registered recursion = false; a root overflows the stack at about 40k iterations #105 (honest effects; loops after [v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91 stage 3) and [v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91 stage 1 (feat(rust): close the runtime's library boundary (RB-09, stage 1 of #91) #102).
Boundary design agreement on this comment; then one PR: SPEC §17.x for the host profile, register rows, the Request/Response/Step types as a language-1.2 stdlib module, a gate that no handwritten driver text exists.
Stdlib members in the order the pilot needs them: bytes and text, sorting, JSON, hex/decimal, SHA-256 (each with a differential against its Rust counterpart on a seeded corpus).
First real pilot: the axiom-output parser (verify/axiom.rs, 210 lines, §22.5): closed, pure, one Result of data, with committed golden vectors (tests/golden/axiom-parser/: accepted, wrapped, rejected) as the oracle and LLV7004 as its only error. Then the preservation lexer/token audit.
calculus::check, rust::{lower, validate, print, package}, the production stages, certificates, front end (as the issue says), each under the differential and, at the end, the fixed point.

Questions

Is the state-machine boundary (§3) the direction? If yes I draft its SPEC section and register rows as the first PR of this issue once production: the collection and iteration primitives are realized by self-recursive functions but registered recursion = false; a root overflows the stack at about 40k iterations #105 and feat(rust): close the runtime's library boundary (RB-09, stage 1 of #91) #102 are in.
rust-host as a third target profile, or the driver as a feature of rust-std? I recommend a profile: eligibility then states, per root, whether it may ask.
Item B4 (making the bytes and text primitives kernel-reducible) is a runtime change that regenerates the language-1.2 identity. It can ride with [v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91 stage 2 (which changes the runtime's content address anyway) or stand alone; I recommend riding with it.

Generated by Claude Code

Note: SHA-256, the last stdlib member in the spike comment (§4, step 3), is being delivered under #126 (claim posted there; stage 1 = module + differential against sha2 + production-build measurement, stage 2 = switching every identity).

Claiming the stdlib lane of this issue (step 3 of the order above): the members, in the order the pilot needs them, starting with bytes and text. Not the effects boundary (§3), which stays with afflom.

Member 1: bytes and text over Bytes. A language-1.2 project stdlib/ beside compiler/ (module prefix LexLeanStd; the examples leg verifies it as it does compiler/), first module Text, seven production roots for rust-std, written in the notation:

root	oracle (Rust std)
`startsWith (subject prefix : Bytes) : Bool`	`<[u8]>::starts_with`
`endsWith (subject suffix : Bytes) : Bool`	`<[u8]>::ends_with`
`trim (subject : Bytes) : Bytes`	`<[u8]>::trim_ascii`
`lines (subject : Bytes) : List Bytes`	`str::lines` on UTF-8 input (`\n` and `\r\n` end a line, the last line needs no ending)
`splitOn (subject : Bytes) (delimiter : UInt8) : List Bytes`	`<[u8]>::split`
`joinWith (pieces : List Bytes) (separator : Bytes) : Bytes`	`<[Vec<u8>]>::join`
`find (subject needle : Bytes) : Option Nat`	`str::find` on UTF-8 input

Written as the spike did (B1–B3): components over Bytes, character classes by equal on UInt8, no String scalar iteration; iterate, iterate_until and list_fold carry recursion (#129).

Evidence (R3): one register row, SL-01 in a new suite stdlib, scenario and failing test first. The test (a) checks and builds the project and reads the seven roots' eligibility, (b) runs each root's lowered program through the calculus interpreter and its rust-std rendering through the pinned rustc on a seeded corpus against the oracle above, zero disagreements, (c) detects a planted defect in a member, and (d) under the pinned Lean, exports the certified packages (certificates A, B, E) through lexlean::api::production, committed under tests/production-export/stdlib/ and compared by check-production-export. Theorems that need Bytes equality by evaluation wait for B4 (#91 stage 2); until then the module's text logic is validated by the differential only, as §2.B4 says.

Branch claude/issue-92-stdlib-bytes-text; draft PR to follow. Sorting, JSON and hex/decimal come after, one PR each, unless the layout is objected to (SHA-256 is claimed under #126 and stays out of this lane).

Member 1 (bytes and text over Bytes) is up as draft PR #153: stdlib/ beside compiler/, seven rust-std roots in LexLeanStd.Text, SL-01 (suite stdlib, SPEC §17.22, register 382) green locally in 156 s including the Lean-backed export; fast vv legs green, the long legs run in its CI. Sorting is next, in its own PR, unless the layout draws an objection there.

chore(stdlib): regenerate the lock, records, and packages on the merg…

Maintainer decisions on the three questions of the spike comment, so that the effects boundary has an answer and the stdlib lane (#153, #126) is not waiting on one. Each follows from what the issue already requires; none needs more information.

The state-machine boundary of §3 is the direction. The program is a pure start/resume pair over first-order data and a generated driver performs the requests. The alternatives fail the issue's own text: an effect monad puts state and failure into TargetSemantics and re-proves every certificate; a host-function table makes purity a convention, so eligibility could not tell a pure member from an effectful one; world-passing needs a nominal World and linearity the calculus lacks. The one thing this fixes for the stdlib: no member may call a host function, and effects are the Ask data a root returns.
rust-host is a third target profile, rust-std plus the driver. Eligibility then states per root whether it may ask, which a feature of rust-std would hide.
B4 rides with [v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91 stage 2, which changes the runtime's content address anyway: one regeneration of the language-1.2 identity instead of two. Until it lands, theorems that need Bytes equality by evaluation wait, and the stdlib's text logic is validated by its differential, as the spike says.

What this leaves in order: the boundary's SPEC section, register rows, the Request/Response/Step module and the gate come after #91 stage 4, because the driver is a runtime profile item that is authored in .lex.tex and rendered by the Rust backend, and it cannot exist as handwritten Rust (this issue's DoD and #91's). I will not land a boundary text with no driver behind it: that would be a register row claiming what nothing implements. The stdlib members (#153 and the ones after it) do not wait for it: they are pure.

Generated by Claude Code

@humuhumu33

Claiming step 4 of the order above, the first real pilot: the exact axiom-output parser (verify/axiom.rs, §22.5), authored as .lex.tex production roots, certified (A, B, E) and compared with the Rust it replaces. A contributor session has it, stacked on #153's Text members (branch claude/issue-92-pilot-axiom-parser, from claude/issue-92-stdlib-bytes-text; nothing is pushed to #153's branch). It will post its project layout here before building, and open a draft PR (Refs #92) with one register row (BS-01), the golden vectors of tests/golden/axiom-parser/ and a seeded differential as the evidence. The Rust parser stays as the stage-0 oracle until the fixed point.

@humuhumu33: this is the user of #153's startsWith, trim, lines, splitOn, find. If the pilot finds a member missing or wrong, it will say so on #153, not patch your lane. It does not move the language-1.2 identity; if it needs to, it stops and reports here first.

The boundary (SPEC section, register rows, the Request/Response/Step module and its gate) is still after #91 stage 4, as decided above.

Generated by Claude Code

Pilot layout (step 4, axiom-output parser). Proceeding unless the maintainer objects here.

Cross-project imports are impossible today. A project reads only its own source_roots; config::is_project_relative rejects .., and symlinks are refused (project.rs). So bootstrap/ cannot \importmodule LexLeanStd.Text.

Least-bad layout:

New project bootstrap/ beside compiler/ and stdlib/, module prefix LexLeanBoot, module AxiomOutput holding the production roots of the parser.
bootstrap/src/Text.lex.tex is a vendored copy of feat(stdlib): the first member, bytes and text over Bytes (#92) #153's stdlib/src/Text.lex.tex, identical except that the production: clauses are removed (so the copy is a library and does not republish seven duplicate certified packages). The BS-01 case asserts that equivalence on every run (the copy equals stdlib/src/Text.lex.tex with the production: clauses stripped), so the copy cannot drift from feat(stdlib): the first member, bytes and text over Bytes (#92) #153. It is deleted once projects can depend on projects.
Rejected alternative: adding the module to stdlib/. It would change stdlib/expected/ and tests/production-export/stdlib/, which feat(stdlib): the first member, bytes and text over Bytes (#92) #153 and the later stdlib members compare byte for byte, and it would put a bootstrap component into the library lane.

One member does not fit: Text.trim is trim_ascii, by design. The Rust parser uses str::trim and char::is_whitespace (Unicode White_Space: VT, U+0085, U+00A0, U+2000-200A, ...), so the pilot defines the Unicode variants locally and the differential includes those characters. I will say so on #153 rather than change it there.

No runtime or calculus change is planned; the language-1.2 identity is not touched. Branch claude/issue-92-pilot-axiom-parser.

Generated by Claude Code

wip(bootstrap): axiom policies aligned; decimal formatting under inve…

Maintainer: the pilot layout above is accepted; proceed.

The vendored Text.lex.tex is acceptable because the case asserts on every run that it equals #153's file with the production: clauses stripped, so it can only be a copy, not a fork. It is temporary and has to say so in its header and in the SPEC paragraph.

The finding behind it is bigger than the pilot, and it is on this issue's path: a project cannot import another project's modules (source_roots stay inside the project, .. and symlinks are refused). Step 2 of the order here ("a package of modules the compiler project imports") has no mechanism today, and the lexicon_source kinds (builtin, path, git) are for glossaries, not source modules. Before the compiler's own modules (steps 5 to 7) import the stdlib at scale there must be one. Options, for whoever takes it (I will write the design comment when #153 and #146 have landed, so it can rest on the stdlib as it is then): (a) one project holds both, the stdlib being modules of the compiler project and stdlib/ its published slice; (b) a source_package kind of lexicon_source that pins another project's modules by tree hash, read into the importing project's graph and identity; (c) a project-level [[dependency]] with the same pinning. (b) and (c) change the identity and the lock format, so they belong with #91 stage 2's regeneration, not before.

Not in the pilot's scope; no change to its plan.

Generated by Claude Code

Pilot status (step 4): draft PR #160 (Refs #92), stacked on #153.

Certificate generator findings (found while getting parseAuditOutput through lexlean verify; no change made, the source avoids each). Certificate A is rejected with LLV7013 (Application type mismatch, generated __rel_N) for programs that elaborate, check, lower, and run correctly:

A user-defined call that is the entire then/else of an if, or the right operand of &&/|| (for example (if c then (axiomList name list) else ...), ((mode =? 1) && (isLater byte)), ((Text::endsWith p a) || (Text::endsWith p b))). Binding the call with let before the if, or making it the scrutinee of an inner if, verifies.
iterate_until whose initial state contains a parameter, (prim iterate_until step fuel (number, 0x)); a literal initial state, (0, 0x), verifies. Reproduced in a one-definition project with and without quotient/remainder, and with a helper definition or (number + 0) for the state.

If these are generator gaps they live in preserve.rs/certificate.rs and would move the language-1.2 identity, so I have not touched them. Happy to attach the scratch repros if wanted.

Smaller language gaps hit (all worked around in source): no Nat to fixed-width conversion (checked_convert needs a fixed-width or Int input), so a Nat is formatted to decimal by place values; binder names record, axiom, first, second are reserved; \importmodule precedes \title; a top-level match on the recursive argument cannot refer to that argument in its branches.

Generated by Claude Code

chore(stdlib): regenerate the lock, records, and packages on the merg…

docs(bootstrap): say why the vendored Text module is temporary

Merge pull request #153 from UOR-Foundation/claude/issue-92-stdlib-by…

fix(bootstrap): regenerate bootstrap/ after #82; give rustc a 64 MiB …

Merge pull request #160 from UOR-Foundation/claude/issue-92-pilot-axi…

Pilot summary (#160, merged), for the next component:

Certificate A is the sharp edge. A user call that is the whole then/else of an if (or the right operand of &&/||), and an iterate_until whose initial state holds a parameter, are rejected by lexlean verify (LLV7013) though they check, lower, and run correctly; check/build do not see it, and each verify costs about 3 minutes, so author with let-bound calls and literal initial states, and expect the axiom policy to be aligned declaration by declaration (one violation per run; a loop script did it in ~35 runs). The nested-expression/rustc-stack output finding is production: a generated rust-std package can need more rustc stack than a default Windows thread gives (found by #160) #164.
Missing primitives and surface limits that cost the most: no Nat to fixed-width conversion (so decimal formatting of a Nat is 20 unrolled place values, with a 10^20 domain), no rfind/parse usize/Unicode trim in Text (the pilot defines splitLast, isWord, trimmed), no &&/|| that certifies with call operands, no comment form for provenance notes, binder names like record/axiom/first/second reserved, a recursive match cannot name its recursive argument in a branch, and a project cannot import another's modules (hence the temporary vendored Text).
What worked: the differential is the right instrument for text code (the Rust oracle plus a corpus of boundaries, wrapping, and mutations found no disagreement in the final program; the seven planted defects were each caught), and a pure first-order Result of data (an association list and a Rejection structure) crosses the root boundary cleanly, so the preservation lexer/token audit can follow the same shape.

Generated by Claude Code

@afflom

Next compiler component, proposed (nothing built yet): the preservation lexer and token audit. The other half of step 3 in the order above; #160 was the axiom half.

What. production::preserve::lex and audit_tokens (§17.17, about 380 lines of Rust) as a new module LexLeanBoot.PreserveLex in bootstrap/, with two rust-std roots: lexLean (text : Bytes) : Result (List Lexeme) Bytes and auditTokens (text : Bytes) (imports : List Bytes) : Option Bytes. The Rust stays as the stage-0 oracle.

Why this one. It is on the trust path (every certificate and library module goes through it), it has the pilot's shape (a pure, first-order result over bytes), and it fits the closed 1.2 primitives with no Unicode tables: is_control is Cc, and the letter-like and subscript classes are explicit ranges. It needs no new stdlib member. UTF-8 decoding, one hex byte and list membership are local helpers, to be lifted into the stdlib if a second component needs them. Keeping it out of stdlib/ also avoids a clash while #126 regenerates that directory.

Evidence. One row, BS-02, with the scenario and failing test first. The lowered program under the evaluator and the rendered package under the pinned rustc must match the Rust on the lexeme list, the verdict and the message, for:

every committed generated Lean text (495 files, the largest 625 KB);
a seeded corpus covering every lexer edge.

Planted defects must be caught, and the certified packages are exported. PK-05's "the roots are exactly these two" assertion grows to four. No identity moves. Only bootstrap/ records change, regenerated once after #167 and #126 land.

One design point. iterate is still self-recursive Rust (#105), so a per-scalar scan of a 625 KB certificate nests 625k calls. The harness's 1 GiB thread hides this; an 8 MiB main thread would not. I plan a two-level scan: chunks of the text, then the scalars within a chunk, so the depth is about √n. I will measure it first and drop it if the rendering turns out not to need it. The source follows your pilot notes: let-bound calls and literal iterate_until states.

@afflom, two questions:

Your v0.4 plan puts more stdlib members first. Should this start now, alongside them (it needs none), or after the next members (sorting, JSON, hex/decimal)?
Two-level scan now, or wait for loops ([v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91 stage 3)?

The other candidates, ranked: the canonical-JSON byte-form check (ir::core::CanonicalSyntax), the §12.2 primitive scanner, content-identity framing (after #126), and the reserved-token check (lean_tokens).

Author bootstrap preservation lexer and token audit (BS-02, #92)

Status update on the preservation lexer and token audit (BS-02):

Draft PR #171 (issue-92-source-audit, head 90d7992de) is implemented, verified, and green on the draft CI leg (ci/just vv (rest), honesty, reproducibility):

bootstrap/src/TokenAudit.lex.tex (LexLeanBoot.TokenAudit) imports LexLeanStd.Text via source package and declares lex and auditTokens as rust-std production roots.
BS-02 verifies differential agreement with production::preserve::{lex, audit_tokens} across 1,731 deterministic Lean 4 source vectors, 300 seeded runs per root under the calculus evaluator, 5,731 inputs per root under the pinned rustc, all 7 TOKEN_PLANTS, and full Lean kernel certification + production export under tests/production-export/bootstrap/packages/rust-std/{audit_tokens,lex}/.
Kept as draft until v0.4 train: byte literals (#68), widening (#151), dyadic floats (#150), certificates A and B as data, package scaffolding, regenerated once #167 (v0.4-train) lands on main so its bootstrap/expected/verify/ records and register count can be rebased once onto post-v0.4 train: byte literals (#68), widening (#151), dyadic floats (#150), certificates A and B as data, package scaffolding, regenerated once #167 main.

@afflom

Thanks. #171 covers the lexer and token audit, so I withdraw that proposal.

Next component, proposed (nothing built): the §12.2 primitive scanner, source::scan::{scan, reject_forbidden_atoms} (about 360 lines), as LexLeanBoot.PrimitiveScan in bootstrap/, row BS-03. Nothing on this issue or in the open PRs claims it. The Rust stays as the stage-0 oracle.

Why this one. Every source of every build goes through it. It is the front end's first layer, the one piece of step 7 that ports without the rest of the front end. SPEC already says it has no dependency on host Unicode character classes, so it fits the 1.2 primitives as written: ASCII byte classes, scalar widths from the lead byte, columns counted in scalars. It needs no new stdlib member. The one Nat it formats (the max_primitive_atoms message) reuses #160's decimal. No identity moves.

Roots: scanSource (path text : Bytes) (maxAtoms : Nat) : Result (List Atom) Rejection and rejectAtoms (path : Bytes) (atoms : List Atom) (forbidden : List Bytes) : Option Rejection. Rejection carries the code, message, span and help the Rust sets. The SemanticDataContext rules are transcribed one to one.

Evidence: the scenario and failing test come first. The evaluator and the rendered package under the pinned rustc must match the Rust on atoms, spans and rejections for:

every committed .lex.tex, 581 files, normalized as link.rs does (the two preservation-library sources of 9 and 24 MB run under rustc only);
a seeded corpus of edges: controls, multibyte columns, the atom limit at N and N+1, leading-zero adjacency, payload strings and notation bodies.

Planted defects must be caught, and the packages are exported. Depth follows #171's precedent: no chunking, stated in the PR, left to #105's loops.

Timing: I would branch from main after #167, and regenerate bootstrap/ once #171 and #172 are in, so the root lists of PK-05 and bootstrap.rs merge once.

@afflom: may I take it? The order question from my last comment still stands: if you want the next stdlib members (sorting, JSON, hex/decimal) first, I will start with those and leave this for after. A small follow-up I could take as well: backend::lean_tokens::is_reserved.

Generated by Claude Code

Author bootstrap preservation lexer and token audit (BS-02, #92)

Wave 2: bootstrap preservation lexer and token audit (BS-02, #92), with

Taking BS-03 (the §12.2 primitive scanner, LexLeanBoot.PrimitiveScan) as proposed above; branch claude/issue-92-primitive-scan, draft PR to follow.

Generated by Claude Code

BS-04 design: `LexLeanBoot.CalculusCheck` (`lexlean::calculus::check`)

Proposal before building (#27 stage 8, step 4, first component). Branch will be claude/issue-92-calculus-check; BS-03 untouched.

Roots (rust-std, no capabilities)

Root	Oracle
`checkProgram (program : Program) : Result Unit Bytes`	`calculus::check::check` (`Err(reason)` ↔ `Result.error` of the reason's UTF-8 bytes)
`checkArguments (program : Program) (entry : Nat) (arguments : List Value) : Result Unit Bytes`	`calculus::check::check_arguments`

primitive_type is an internal definition, exercised through both roots and by direct vectors on checkProgram (every Prim at every operand-type shape).

Input encoding — the lowered representation, not JSON bytes

Program, Adt, Function, Ty, Value, Shape, Prim, Expr, Arm are 1.2 inductives mirroring calculus/mod.rs one to one (mutual group for the Ty/Value nest and the Expr/Arm nest; nested occurrences only under List, Option, Box-free direct fields). Recursion over them uses mutual definition groups (the Recur.lex.tex pattern, DF-16), so no new stdlib member and no new primitive is needed. Chosen over "canonical JSON read as Bytes" because a JSON reader is a different component (Program::parse, serde deny_unknown_fields, canonical re-encoding, calculus::load) and belongs to its own row; the checker's input is first-order data (§17.13 rule 1) and that is the data. The harness builds the argument Value tree from the Rust Program.
Consequence stated up front (R2): BS-04 does not cover Program::parse/canonical/load; parse-level rejections (unknown kinds, unknown fields, duplicate keys) are out of its scope and not claimed.

Oracle mapping and exact messages

Result is Result.ok () / Result.error message, the oracle's String to the byte. The oracle formats {:?} of Ty, Shape, Prim, Value, so the module reproduces #[derive(Debug)] output (struct-variant spelling, Box transparency, Vec as [a, b], u64 in base ten). One part I do not think 1.2 can reproduce exactly: Rust's Debug for a str (a Value::String inside a "literal … does not have type …" message) escapes by char::is_printable/Grapheme_Extend tables. The module will escape \" \\ \n \r \t \0, ASCII controls and U+007F exactly as Rust does and copy every other scalar literally; strings with non-ASCII non-printable or grapheme-extending scalars are therefore excluded from the corpora and from the claim, and the register statement will say so. If you would rather have a Unicode-table stdlib member for this, that is a separate proposal; I will not approximate silently.

Vectors

Evaluator (normative host): every committed program accepted by the oracle: the program of every compiler/rust/{rust-std,rust-core}/*/package.json and every tests/production-export/*/packages/*/*/package.json (239 + 73 files, deduplicated by canonical bytes) and every compiler/fixtures/*.json program (122) with its entry arguments through checkArguments; plus the refused programs among them (compiler/rust/negative, reasoning rejections) with the oracle's exact rejection; plus a seeded mutation corpus (~600 mutants of the committed programs: retyped operand, dropped/duplicated/unreachable arm, wrong binder count, shadowed/unbound local, out-of-range literal, non-canonical decimal, bad byte hex, undeclared ADT/function/constructor, over-capturing closure, every Prim at wrong operand types, field on a multi-constructor ADT). Counts finalised after measuring the evaluator cost (BS-02's differential runs on every host of the matrix and costs the gate about 140 runner-minutes #190).
rustc (every host, Split BS-01 and BS-02 differential between host matrix and normative host (#190) #192 split): the rendered rust-std packages of both roots under the pinned rustc on a larger seeded corpus (~20,000 programs/mutants), outcome = Ok/message.
Register statement will state the split: evaluator + seeded corpora + plants on the normative host, rustc vector differential on every host.

Planted defects (each must be detected)

(1) exhaustiveness check dropped, (2) duplicate arm accepted, (3) closure capturing all parameters accepted, (4) nat bound off by one (2^64), (5) -0/leading-zero decimal accepted, (6) shadowed binder not rejected within an arm, (7) field on a multi-constructor ADT accepted, (8) shift_left second operand type widened to the first operand's, (9) odd-length byte hex accepted, (10) Cons binder type wrong (tail typed as element).

Gates

BS-04 in the compiler part; register row + §31 row + features + conformance_bs_04; roots added to tests/production-export/bootstrap/roots.json; regenerated records via the writers only. Count moves by one (BS-03 adds another; maintainer reconciles at integration).

I will start building one hour after this comment unless told otherwise. Any objection to the encoding choice (data, not JSON bytes) or to the Debug-string exclusion is the thing to say now.

Generated by Claude Code

Navigation Menu

Repository navigation

[v0.4] #27 stage 8: the production compiler authored in .lex.tex and compiled by LexLean to production software #92

Decisions (made by the maintainers)

Scope

Self-hosting acceptance (the bootstrap)

What it needs (inventory, to be refined in the first sub-stage)

Proposed order inside this stage

DoD (whole stage)

Acceptance criteria

#92 spike: what a compiler component needs today, and the boundary/effects design

1. The pilot

2. What is missing, by owner

3. Proposal: the effects boundary (for the maintainers' decision)

4. Stdlib and order

Questions

6 remaining items

BS-04 design: `LexLeanBoot.CalculusCheck` (`lexlean::calculus::check`)

Roots (rust-std, no capabilities)

Input encoding — the lowered representation, not JSON bytes

Oracle mapping and exact messages

Vectors

Planted defects (each must be detected)

Gates

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

[v0.4] #27 stage 8: the production compiler authored in .lex.tex and compiled by LexLean to production software #92

Description

Decisions (made by the maintainers)

Scope

Self-hosting acceptance (the bootstrap)

What it needs (inventory, to be refined in the first sub-stage)

Proposed order inside this stage

DoD (whole stage)

Acceptance criteria

Activity

afflom commented on Oct 15, 2026

#92 spike: what a compiler component needs today, and the boundary/effects design

1. The pilot

2. What is missing, by owner

3. Proposal: the effects boundary (for the maintainers' decision)

4. Stdlib and order

Questions

humuhumu33 commented on Oct 15, 2026

humuhumu33 commented on Oct 15, 2026

humuhumu33 commented on Oct 16, 2026

afflom commented on Oct 16, 2026

afflom commented on Oct 16, 2026

afflom commented on Oct 16, 2026

afflom commented on Oct 16, 2026

6 remaining items

afflom commented on Oct 16, 2026

afflom commented on Oct 17, 2026

humuhumu33 commented on Oct 17, 2026

afflom commented on Oct 18, 2026

humuhumu33 commented on Oct 18, 2026

afflom commented on Oct 18, 2026

afflom commented on Oct 18, 2026

BS-04 design: LexLeanBoot.CalculusCheck (lexlean::calculus::check)

Roots (rust-std, no capabilities)

Input encoding — the lowered representation, not JSON bytes

Oracle mapping and exact messages

Vectors

Planted defects (each must be detected)

Gates

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

BS-04 design: `LexLeanBoot.CalculusCheck` (`lexlean::calculus::check`)