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

[afflom]

Closes #169
Closes #170
Refs #92

Wave 2 after the v0.4 train (#167): the second bootstrap component, BS-02, on the merged identity, carrying the two small hygiene PRs that were ready at the same time so that the gate runs once for the three.

Members

Member	What it is	On this PR
BS-02 (#92 step 3, this branch's own commits e347382c7, 9e2de819f)	the preservation lexer and token audit of SPEC.md §17.17 as language-1.2 source, bootstrap/src/TokenAudit.lex.tex, with lex and auditTokens as rust-std production roots held to the Rust oracle production::preserve::{lex, audit_tokens}	register 414
#173 (#169)	RT-04's source scanner blanks only test items	head 1cc1ab1cc merged; closes #169; #173 to be closed by hand with a pointer
#174 (#170)	the tracked tree holds nothing the repository walkers skip	head 77553dbf3 merged; closes #170; #174 to be closed by hand with a pointer

What BS-02 establishes

• Both roots are eligible for rust-std with exactly their declared effects (none), read from the eligibility report the build writes.
• Under the calculus evaluator, the lowered programs agree with the oracle on every lexeme, position, and rejection message for 1,731 deterministic vectors (the token-audit unit vectors, every prefix of SP-09's number-lexing corpus, and the first 1,500 characters of every module of the shipped preservation library and calculus modules) and 300 seeded texts per root.
• Under the pinned rustc, the rendered packages agree with the oracle on those vectors plus 4,000 seeded texts per root (5,731 runs each).
• Seven planted defects in TokenAudit.lex.tex (nested-comment depth, uppercase hex digits, interpolated strings, C1 controls, quoted forbidden attribute, qualified forbidden constant, unlisted import) are each detected by the differential.
• Under Lean, the production export's certified lex and audit_tokens packages are byte-identical to the committed ones under tests/production-export/bootstrap/ and realize the lowered program the differential ran.

Changed at integration, by hand (maintainer, on top of 9e2de819f)

• The register statement, scenario, §31 row and §17.23 prose of BS-02 say that the evaluator reads the first 1,500 characters of each library and calculus module; the gate always did (the evaluator interprets the lowered program, and the prefix keeps its time bounded), and the statement claimed the whole modules. R2: the statement says what runs. CONFORMANCE.md regenerated.
• .github/bdd-parts.json: BS-01 and BS-02 run in the compiler bdd part. Both build the bootstrap project once per test process (§9.4: cases sharing a fixture are named by one part), and BS-02 takes about 45 minutes on the normative host; in the remainder it would have made the rest leg every draft push runs (24 min on the train's run) about three times as long. compiler is the shortest leg (15 min). check-test-inventory (RP-13) passes: compiler 23, rest 292.

Records

e347382c7 is the author's rebase onto main (193cd2148, register 414) with the records regenerated there. The maintainer regenerated them independently on the same identity (records reset to main's, then lexlean lock, check-golden --write, check-production-export --write, verify-examples --write with compiler, stdlib and one example as controls, all byte-identical to their committed records): the result is byte-identical to 9e2de819f, so no regeneration commit is on this PR.

Checked locally on the tree of this head

cargo fmt --check, clippy -D warnings, validate-model, validate-spec-links (414 rows), check-test-inventory, check-golden, check-production-export; conformance_bs_02 (Lean-backed, 2,687 s), conformance_rt_* (4), conformance_rp_* (14), the xtask unit tests. The whole gate runs in CI on this head.

How this merges

The head contains main (193cd2148). It is ready for review; the merge is a merge commit pinned to the final head, and the push run on main runs nothing when this PR's run passed every job (#166). It needs an approval from someone other than its authors.

🤖 Generated with Claude Code

https://claude.ai/code/session_013QppGKetUURseXowZun9KY

[afflom]

@afflom @humuhumu33 Status update for #171 (BS-02, #92 preservation lexer and token audit):

• Rebased onto main (8765feea3) at 90d7992de; draft CI (ci/just vv (rest), honesty, reproducibility) is green.
• Kept as draft while 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, which moves certificates A and B to kernel-term data and updates the register count) finishes its full gate run and merges to main, so bootstrap/expected/verify/ and the 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 before marking ready.

[afflom]

Rebased onto main (193cd2148, register 414), regenerated bootstrap/expected/{build,verify} and tests/production-export/bootstrap/packages under the data-certificate and package-scaffolding schemas from #167, verified cargo xtask validate, check-test-inventory, conformance_rp_01..14, conformance_pk_05, conformance_vr_13, and conformance_bs_02 locally, and marked ready for the full gate at e347382c7. cc @afflom @humuhumu33

[afflom]

Maintainer: I am taking this branch from 9e2de819f to land it as the second wave after the train. Please hold further pushes to issue-92-source-audit; anything else goes in a comment here and I carry it.

Independently regenerated here on the merged identity (lock, check-golden --write, check-production-export --write, verify-examples --write with compiler, stdlib and one example as controls), the records are byte-identical to the ones on 9e2de819f, your Audit.json fix included. conformance_bs_02 passes here (Lean-backed, 2,687 s). On top of 9e2de819f I add: (1) the BS-02 statement, scenario, §31 row and §17.23 prose say that the evaluator reads the first 1,500 characters of each library and calculus module, which is what the gate does; (2) BS-01/BS-02 move to the compiler bdd part so the rest leg every draft push runs does not grow by 45 minutes; (3) #173 and #174, both reviewed and green locally, merged in so the gate runs once for the three. Title and body follow.

---

Generated by Claude Code

[afflom]

The whole gate is green on 1df1b9f7f: run 39125361480, 25 of 25 jobs (27 check runs) success; mergeable; the head contains main (193cd2148).

Measured against the train's run (730 runner-minutes, 102 min wall): 872 runner-minutes, 158 min wall. bdd-compiler 15 → 30 min (BS-01/BS-02 moved there, as intended), bdd-production 27 → 43 (the export certifies two more roots), and every host of the matrix grew because cargo test --workspace runs BS-02's evaluator-and-rustc differential on each (Windows 69 → 105, Intel mac 100 → 140, arm mac 78 → 87, arm Linux 58 → 66). That is the case's cost, not a fault; filed separately with a proposal so the gate does not keep it.

@humuhumu33 this needs an approval from someone other than its authors; the three hand changes on top of 9e2de819f are listed in the description (statement, bdd part, the two merged PRs).

---

Generated by Claude Code

[afflom]

Maintainer review at 1df1b9f7f: merged on the owner's rule — the gate is green on the head and the linked issues' DoD is met — without waiting for a second reviewer.

Checked against #92 step 3 (the pilot's second component): TokenAudit.lex.tex is the only authoring surface; both roots are rust-std-eligible with no effects; the evaluator and rustc differentials against production::preserve::{lex, audit_tokens} agree on 1,731 vectors plus the seeded corpora; seven planted defects are each caught; the exported certified packages are byte-identical to the committed ones (Lean-backed, passed here and in CI). #169 and #170 are met by the merged heads of #173 and #174 (RT-04 scanner, RP-03 walker assertion), whose cases pass. hh's reading of the three hand changes is still welcome after the fact; anything found goes in a follow-up.

---

Generated by Claude Code