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

.github/bdd-parts.json

@@ -2,6 +2,8 @@
   "remainder": "rest",
   "parts": {
     "compiler": [
+      "BS-01",
+      "BS-02",
       "GC-02",
       "GN-02",
       "GN-03",

CHANGELOG.md

@@ -25,6 +25,18 @@ versions, and the entries below say what each tag does and does not claim.
   the gate are the rows of `.github/vv-rows.json`, the matrix the plan hands
   to `vv`. `release.yml` still runs `just vv` whole and reads no earlier run.
   The register is unchanged: the statement of `RP-14` is extended.
+- The second component of the compiler's own pipeline as language-1.2 source:
+  the preservation lexer and token audit (SPEC.md §17.23, §17.17, `BS-02`, #92;
+  no new diagnostic code, no change to the language-1.2 identity).
+  `bootstrap/src/TokenAudit.lex.tex` imports `LexLeanStd.Text` via source
+  package and declares `lex` and `auditTokens` as production roots for
+  `rust-std`. `BS-02` runs 1,731 deterministic Lean 4 source vectors and 300
+  seeded combinations per root against the stage-0 Rust oracle
+  `production::preserve::{lex, audit_tokens}` under the calculus evaluator and
+  5,731 inputs per root under the pinned `rustc`, detects seven planted defects,
+  and, under the pinned Lean, compares the certified `audit_tokens` and `lex`
+  packages with the committed ones under `tests/production-export/bootstrap/`.
+  `BS-02` brings the register to 414 IDs.
 - Explicit shared byte literals (#68, `SM-19`, `MD-02`; languages 1.1 and 1.2):
   a modeled byte literal is lowered as `_root_.ByteArray.mk #[…]` with every
   octet written `_root_.UInt8.ofNat (nat_lit n)`, an octet occurring four or
@@ -280,19 +292,23 @@ versions, and the entries below say what each tag does and does not claim.
   golden, fixture expectation, calculus package, production export, and
   verified record is regenerated. The register holds 391 IDs.
 
-- The runtime gates read what they claimed to (#154, follow-up to #144; no new
-  diagnostic code, no new ID). `RT-04` finds a Lean runtime text in any string
-  literal of the compiler's source outside unit-test items, in production code
-  after a test module, with or without a `namespace` line (a declaration
+- The runtime gates read what they claimed to (#154, #169, follow-ups to #144;
+  no new diagnostic code, no new ID). `RT-04` finds a Lean runtime text in any
+  string literal of the compiler's source outside unit-test items, in
+  production code after a test module or after a `#[cfg(test)]` that is not on
+  an item (or an inline `#![cfg(test)]`), with or without a `namespace` line (a
+  declaration
   under a runtime name is one), written whole or in literals joined by
   `concat!`, an array, `+` or `format!`; its statement now also asserts
   what it said of generated modules: every committed language-1.2 module
   imports the runtime modules whose constants it names and declares nothing
   under a runtime namespace. `RT-02` recomputes the compiler-semantics IDs
   with each frozen file changed (1.0 and 1.1 unchanged, 1.2 changed). `RT-03`
   plants the second direction of the axiom check. Every directory that holds a
-  `CACHEDIR.TAG` is skipped by the repository walkers, so a build directory
-  beside the sources no longer reads as source. No compiled behavior changes.
+  `CACHEDIR.TAG` is skipped by every repository walker, so a build directory
+  beside the sources no longer reads as source, and `RP-03` (#170) asserts that
+  the tracked tree (`git ls-files`) holds no `CACHEDIR.TAG` and no walker-skipped
+  path component outside the sanctioned `expected/` oracle directories. No compiled behavior changes.
 - UOR Atlas is verified in CI as the parts of one run (SPEC.md §9.4, §22.11,
   `RP-14`, `VR-23`, #131; no new diagnostic code). The examples leg, 178
   minutes on `main` at 514e95ad (CI run 38716449420), was 156 minutes of

CONFORMANCE.md

@@ -60,6 +60,7 @@ the error registry does not sanction (R5, `ERRORS.md`).
 | ID | Level | Statement |
 | --- | --- | --- |
 | `BS-01` | `build` | The axiom-output parser of SPEC.md §22.5 is language-1.2 source in the `bootstrap/` project: `parseAuditOutput` and the closed Lean-name check `isClosedLeanName` are production roots eligible for `rust-std` with exactly their declared effects; the parser's lowered program under the calculus evaluator agrees with the Rust parser `verify::axiom` on the result, the rejection message, and the attributed declaration for every committed golden vector (accepted, accepted-wrapped, and rejected); both roots' rendered `rust-std` packages under the pinned rustc agree with the Rust oracle on a large seeded corpus of generated, wrapped, and mutated audit outputs with no disagreement; a planted defect in the source is detected; and the certified packages the production export publishes for the project are the committed ones. |
+| `BS-02` | `build` | The preservation lexer and token audit of SPEC.md §17.17 are language-1.2 source in the `bootstrap/` project: `lex` and `auditTokens` of `TokenAudit` are production roots eligible for `rust-std` with exactly their declared effects; both roots' lowered programs under the calculus evaluator agree with the Rust oracle `production::preserve::{lex, audit_tokens}` on every lexeme, position, and rejection message for the first 1,500 characters of every module of the shipped preservation library and calculus modules, the number-lexing corpus, and every token-audit unit vector; both roots' rendered `rust-std` packages under the pinned rustc agree with the Rust oracle on a large seeded corpus of generated and mutated Lean texts with no disagreement; a planted defect in the source is detected; and the certified packages the production export publishes for the project are the committed ones. |
 
 ## calculus
 
@@ -452,7 +453,7 @@ the error registry does not sanction (R5, `ERRORS.md`).
 | --- | --- | --- |
 | `RP-01` | `build` | The repository, crate, executable, metadata, and licenses have the exact LexLean identity specified. |
 | `RP-02` | `build` | The repository is derived from the pinned UOR template commit and contains no inherited domain-specific claim logic. |
-| `RP-03` | `build` | The completed repository has the required file and crate layout. |
+| `RP-03` | `build` | The completed repository has the required file and crate layout, and the tracked tree holds no CACHEDIR.TAG or path component the repository walkers skip outside sanctioned expected/ oracle directories. |
 | `RP-04` | `build` | Only the lexlean crate is shipped and no shipped crate depends on repository-only tooling. |
 | `RP-05` | `build` | The just vv recipe runs every normative acceptance gate in the specified order. |
 | `RP-06` | `build` | CONFORMANCE.md and ERRORS.md are exact generated views of model files. |

README.md

@@ -142,7 +142,7 @@ just vv        # the complete normative acceptance gate (SPEC.md §9.2)
 just release   # vv, then the §30 release criterion; refused until 1.0.0
 ```
 
-All 413 registered conformance IDs are implemented and pass; `just vv` runs clean from a checkout with the pinned toolchain installed.
+All 414 registered conformance IDs are implemented and pass; `just vv` runs clean from a checkout with the pinned toolchain installed.
 
 The differential against the independent generator `lean4-prod` (SPEC.md §17.19, `OR-01`..`OR-08`) acquires it at its pinned commit: from the checkout `LEXLEAN_ORACLE_DIR` names, or by fetching the commit with `git` into the Cargo target directory (`LEXLEAN_ORACLE_CACHE` overrides), and builds it with the pinned Lean and Rust toolchains. It is validation evidence only and no input to any identity. An oracle that cannot be acquired, is not the pinned files, or fails is unavailable: that fails the gate on Linux x86-64 and is printed as `NOT VALIDATED` elsewhere, and is never reported as agreement.
 
@@ -183,7 +183,7 @@ Every row is validated by `just vv`; the IDs link the claim to its register row,
 | The language-1.2 authoring notation: a readable `.lex.tex` text for a semantic module, in bijection with its canonical JSON, whose every position and variant is read from the schema, with readable forms for types and terms and a generic form for every other value, formatted canonically by `fmt` (which also writes a module out of its data form), linking to exactly the module its data form links to, failing closed, the only form in which a language-1.2 source of the product is written, the same for the compiler-tooling modules in the generic notation, with no compiler-semantics ID that depends on which form an embedded module is written in, with no product source owned by a generator but five named records, read and written by programs only through the authoring API (`lexlean::sdk`), and, for a native core module, a readable program over the shared table of kernel terms whose numbering is the order of its text | `AU-01`..`AU-12` | `build` |
 | The runtime of generated Lean as native modules: the portable, collection, model, and reasoning runtimes of language 1.2 are LexLean source that every generated module imports, migrated losslessly and audited against their exact axioms, the released runtime text of languages 1.0 and 1.1 is frozen data equal to their released output, and no other Lean runtime text remains in the compiler but the decoder of core module 2 | `RT-01`..`RT-04` | `build` |
 | The standard library: language-1.2 source beside the compiler whose members are certified production roots, each validated against Rust's standard library by a seeded differential of its evaluator and rustc realizations; bytes and text over `Bytes` | `SL-01` | `build` |
-| The bootstrap project: the compiler's own components as language-1.2 source compiled by LexLean's production pipeline to certified Rust packages, the first being the exact axiom-output parser and its closed Lean-name check, each held to the Rust it replaces (the stage-0 oracle) by the committed golden vectors and a seeded differential of its evaluator and rustc realizations, with planted defects detected and the production export committed | `BS-01` | `build` |
+| The bootstrap project: the compiler's own components as language-1.2 source compiled by LexLean's production pipeline to certified Rust packages, the exact axiom-output parser and its closed Lean-name check and the preservation lexer and token audit, each held to the Rust it replaces (the stage-0 oracle) by the committed vectors and a seeded differential of its evaluator and rustc realizations, with planted defects detected and the production export committed | `BS-01`..`BS-02` | `build` |
 | Source packages: a language-1.2 project imports the modules of a locked, content-addressed package of its workspace: `[[source_package]]` and `lexlean-workspace.toml`, the pins in `lexlean.lock` recomputed by every command, imports closed at link, no re-export of a package's production roots, and the package's modules replayed by the importer's `verify` with their origin in the records | `PK-01`..`PK-05` | `build` |
 | The literal `nat-add-zero` example, the Lean-verified feature examples, and the complete negative fixture suite | `EX-01`..`EX-08` | `build` |
 | Language-1.2 text components, first slice: tokenizers and their round-trip laws, with the laws carried as one native core module the generated modules import rather than authored Lean text (context windows, text generators, text classifiers, adapters, and composition follow in their own slices and add their rows then) | `LM-01`, `LM-02`, `LM-03`, `LM-13` | `build` |