feat(bootstrap): the axiom-output parser as language-1.2 source (BS-01)

[afflom]

Refs #92

Step 4 of the order in #92, the first real pilot: the exact axiom-output parser (verify/axiom.rs, SPEC §22.5) authored as .lex.tex production roots, certified (A, B, E) and held to the Rust it replaces. The Rust stays in the tree, unchanged, as the stage-0 oracle.

Stacked on #153 (base is its branch; nothing is pushed to it), so the diff is the pilot only. Retarget to main once #153 merges.

What is here

• bootstrap/ project (module prefix LexLeanBoot), module AxiomOutput: roots parseAuditOutput and isClosedLeanName, both rust-std, effects allocation, overflow, recursion.
• bootstrap/src/Text.lex.tex is a vendored copy of feat(stdlib): the first member, bytes and text over Bytes (#92) #153's Text without its production: clauses (a project cannot import another's modules; layout posted on [v0.4] #27 stage 8: the production compiler authored in .lex.tex and compiled by LexLean to production software #92). The case asserts the equivalence on every run.
• BS-01 (suite bootstrap, SPEC §17.23, register 393), scenario, conformance_bs_01, tests/production-export/bootstrap/, bootstrap/expected/, VERIFICATION and CHANGELOG entries.
• No runtime or calculus change. Merged main once; main moved the language-1.2 identity, so only bootstrap/ was regenerated (stdlib/ stays feat(stdlib): the first member, bytes and text over Bytes (#92) #153's to regenerate).

Findings reported on #92: the preservation generator rejects (certificate A, LLV7013) a user call that is the whole branch of an if or the right operand of &&/||, and an iterate_until whose initial state holds a parameter; the source avoids them.

Evidence follows in a comment once the post-merge run is green.

---

Generated by Claude Code

[afflom]

Evidence for BS-01, measured locally on the head after merging main (the language-1.2 identity moved with main; only bootstrap/ was regenerated).

Passed

• conformance_bs_01: ok in 419 s, with the production export under the pinned Lean 4.32.1 (certificates A, B, E accepted for both roots; the exported packages are byte-identical to tests/production-export/bootstrap/ and realize the lowered programs the differential ran).
• Eligibility: isClosedLeanName and parseAuditOutput are eligible for rust-std, declared effects [allocation, overflow, recursion] = realized effects.
• Committed vectors under the calculus evaluator: 28 runs (13 accepted, 15 rejected: each line of accepted.txt/rejected.txt, each wrapped record, each file whole) agree with verify::axiom on result, rejection message, and attributed declaration.
• Evaluator corpus: 400 audit outputs, 2,000 names, no disagreement.
• rustc (pinned) on the rendered rust-std packages: 12,000 audit outputs and 40,000 names, no disagreement (corpus: grammar boundaries, every envelope shape and malformed envelope, usize edges, every Unicode white space and look-alikes, wrapping at widths 1 to 10,000, dropped/duplicated/extra/reordered/truncated/oversized records, expected-list mutations).
• cargo fmt --check, cargo clippy --workspace --all-targets --all-features -- -D warnings, validate-model (393 ids), validate-spec-links, check-test-inventory, bootstrap fmt --check and lock --check.

Planted (each on a copy of the source, every run) and caught, outputs in VERIFICATION.md:
continuation loses its space (run 48), U+0085 not white space (run 34), usize bound off by one (run 150), axioms ordered descending (run 1), rejected line loses its declaration (run 11), digit-first name segment ("9"), duplicate-record check dropped (run 76).

Not run locally (CI's): the full just vv; check-golden and check-production-export for the other projects (I regenerated only bootstrap/). stdlib/'s lock and expected records predate main's identity change and are #153's to regenerate; this PR does not touch them.

Honesty: build level, a differential and certificates, not a proof of equivalence. Domain: valid UTF-8 input. A Nat count in a message is formatted for values below 10^20.

Staying draft until the base (#153) merges and CI is green on a head that contains main; I will not merge.

---

Generated by Claude Code

[afflom]

Ready for review. Head merges main (c3905e7, with #153 and #159), retargeted to main; register 394; bootstrap lock current (this merge did not move the identity, so nothing was regenerated). One push for this batch.

Local, on this head: conformance_bs_01 ok in 563 s (production export under the pinned Lean included); fmt --check, clippy -D warnings, validate-model, validate-spec-links, check-test-inventory (5 bdd parts, BS-01 in rest) clean.

Differential corpus: 28 committed vectors (13 accepted, 15 rejected) under the evaluator; 400 generated audit outputs and 2,000 names under the evaluator; 12,000 generated audit outputs and 40,000 names under the pinned rustc. Zero disagreements on result, message, and attributed declaration.

Planted defects (each made on a copy of the source by the case on every run), the red line of each:

the continuation joins without the space the unwrapped form has: run 48 on "'A.b' depends on axioms: [propext,\n  'C.d' does not depend on any axioms" ["A.b"]: the program gives error {"`A.b' depends on axioms: [propext,'C.d` is not a Lean name", some "A.b"}, the oracle error {"`A.b' depends on axioms: [propext, 'C.d` is not a Lean name", some "A.b"}
the next-line control (U+0085) is not white space: run 34 on "\u{85}'A.b' does not depend on any axioms\u{a0}\n" ["A.b"]: the program gives error {"unrecognized audit line: \u{85}'A.b' does not depend on any axioms", some "A.b"}, the oracle ok [("A.b", [])]
a location number may be one past the largest `usize`: run 150 on "A.lean:18446744073709551616:0: info: 'A.b' does not depend on any axioms" ["A.b"]: the program gives ok [("A.b", [])], the oracle error {"unrecognized audit line: A.lean:18446744073709551616:0: info: 'A.b' does not depend on any axioms", some "A.b"}
the axioms are ordered descending: run 1 on "'Demo.M.uses_choice' depends on axioms: [Classical.choice, propext, Quot.sound]" ["Demo.M.uses_choice"]: the program gives ok [("Demo.M.uses_choice", ["propext", "Quot.sound", "Classical.choice"])], the oracle ok [("Demo.M.uses_choice", ["Classical.choice", "Quot.sound", "propext"])]
a rejected line is not attributed to the declaration expected there: run 11 on "\"Demo.M.wrongquote\" does not depend on any axioms" ["Demo.M.unknown"]: the program gives error {"unrecognized audit line: \"Demo.M.wrongquote\" does not depend on any axioms", none}, the oracle error {"unrecognized audit line: \"Demo.M.wrongquote\" does not depend on any axioms", some "Demo.M.unknown"}
a name segment may begin with a digit: run 16 on "9": the program gives true, the oracle false
the duplicate record check is dropped: run 76 on "'A.b' does not depend on any axioms\n'A.b' does not depend on any axioms\n" ["A.b", "A.b"]: the program gives ok [("A.b", [])], the oracle error {"duplicate record for `A.b`", some "A.b"}

Vendored Text: the equivalence assertion (copy = stdlib/src/Text.lex.tex minus its production: clauses) is in BS-01. The "temporary, and why" note is bootstrap/README.md, because the notation has no comment form and the case compares the copy byte for byte.

If #155 or #82 move the identity before this lands, I regenerate bootstrap/ once more. Marking ready now.

---

Generated by Claude Code

[afflom]

One batch, one push, answering the two red checks of 60ed15b. Head merges main d22266b (#82; register 398 by hand in README, SPEC §31 total, cases/repository.rs, xtask/src/spec_links.rs).

1. just vv (examples): missing expected/verify/preserve/.../Compose/RustStd.lex.tex. Certificate E's notation record had never been committed for bootstrap/. After the merge the identity moved (the lock was stale), so I relocked and regenerated only bootstrap/ (verify-examples --write, check-golden --write, check-production-export --write, restricted to the one project by a local filter that is not in the diff). The Compose/RustStd.lex.tex records (R0, R1) are now committed.

2. Windows conformance_bs_01: rustc overflowed its stack in optimize module run_boot_*. Reproduced on Linux with RUST_MIN_STACK on the cargo children:

• 256 KiB: rustc dies (SIGSEGV) even on its target probe, which is not informative.
• 1 MiB: rustc is killed by SIGSEGV compiling both generated package libs, boot_is_closed_lean_name_std and boot_parse_audit_output_std (not only the harness).
• the default (2 MiB, Linux): passes.
  So the generated libs need more rustc stack than a 1 MiB thread gives, and the Windows threads are smaller than Linux's. The fix is in the harness: rust_build::cargo_in now sets RUST_MIN_STACK=64 MiB for cargo's children on every host, so the evidence is the same everywhere. This also applies to the cases that share cargo_in (SL-01 re-run below). I did not isolate which construct nests deepest in the emitted Rust (candidates: the 20-term append chain of decimal, the nested conditionals of whiteLength); if you want that cut down in the source rather than by stack, say so and I will bisect it, but I have not changed the program for it and BS-01 is not narrowed.

Ran locally on this head: conformance_bs_01 ok (433 s, export under the pinned Lean included); conformance_sl_01 ok (242 s); cargo xtask check-golden (all projects, bootstrap: 12 artifacts equal their oracles); check-calculus; validate-model (398 ids); check-test-inventory; cargo fmt --check; cargo clippy --workspace --all-targets --all-features -- -D warnings. check-fixtures was not run (nothing it covers changed).

Ready for review. If #162 lands first I will regenerate bootstrap/ once more; tell me when it does.

---

Generated by Claude Code

[afflom]

Maintainer review: approved at d0605814.

CI. All 26 checks green on this head (host legs including Windows, examples, rest with BS-01, the 14 Atlas jobs and atlas (join), repro, honesty). The head contains main d22266b3 (#82), still main's tip. The two red checks of 60ed15bd are fixed as the contributor described: the missing Compose/RustStd.lex.tex records of bootstrap/, and the Windows rustc stack overflow (the harness's cargo children get RUST_MIN_STACK of 64 MiB on every host; the output-side question is #164).

Against the brief (#92, step 4).

• R3, in the history. The first commit registers BS-01, its scenario, SPEC §17.23 and the failing case; the implementation follows.
• The parser is LexLean. bootstrap/src/AxiomOutput.lex.tex (636 lines of notation, no Rust, no Lean text) implements isClosedLeanName and parseAuditOutput: reassembly of wrapped records, the payload grammar, duplicate/missing/extra rejection, attribution to the expected declaration, and the closed Lean-name check; both are eligible for rust-std with declared effects equal to realized effects, and certified (A, B, E).
• Equal to the Rust it replaces, by evidence of the build level. 28 committed vectors (13 accepted, 15 rejected) under the evaluator; 400 generated audit outputs and 2,000 names under the evaluator; 12,000 audit outputs and 40,000 names under the pinned rustc; zero disagreements on result, message and attributed declaration. Seven planted defects (continuation without the space, U+0085 treated as white space, a location number past usize, descending axioms, wrong attribution, a digit-leading segment, the duplicate check dropped) are made by the case on a copy on every run, each with its red line in the PR. verify::axiom stays in the tree as the stage-0 oracle.
• The vendored Text.lex.tex. BS-01 asserts on every run that it equals stdlib/src/Text.lex.tex minus its production: clauses, so it cannot drift; it is temporary until source packages ([v0.4] Source packages: a project imports the modules of a locked, content-addressed package (needed by #92's stdlib and #32) #161) let a project import another, and PK-05 deletes it. The sentence that says so in SPEC §17.23 and bootstrap/README.md is one local commit the session holds and will push with its next change; I accepted that rather than restart a green run.
• Identity. No compiler-semantics ID move of its own; bootstrap/'s records were regenerated on the combined tree.

Merging with a merge commit pinned to this head. The session of #161 can now take PK-05's input as landed on main.

---

Generated by Claude Code