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

.gitignore

@@ -27,3 +27,4 @@ compiler/.lexlean/
 # Claude Code worktrees and session state (never part of the release set).
 .claude/
 stdlib/.lexlean/
+bootstrap/.lexlean/

CHANGELOG.md

@@ -15,6 +15,23 @@ versions, and the entries below say what each tag does and does not claim.
 
 ## Unreleased
 
+- The first component of the compiler's own pipeline as language-1.2 source:
+  the exact axiom-output parser (SPEC.md §17.23, §22.5, `BS-01`, #92 step 4;
+  no new diagnostic code, no change to the language-1.2 identity).
+  `bootstrap/` is a language-1.2 project beside `compiler/` and `stdlib/`
+  under the module prefix `LexLeanBoot`; its `AxiomOutput` module declares
+  `parseAuditOutput` and `isClosedLeanName` as production roots for
+  `rust-std`. A project cannot import another's modules, so `Text` is a copy
+  of the standard library's without its `production` declarations, compared
+  with `stdlib/src/Text.lex.tex` on every run. `BS-01` runs the committed
+  golden vectors of `tests/golden/axiom-parser/` and a seeded corpus of
+  generated, wrapped, and mutated audit outputs against the Rust parser
+  `verify::axiom` (the stage-0 oracle, unchanged) under the calculus
+  evaluator and under the pinned rustc, detects seven planted defects, and,
+  under the pinned Lean, compares the certified packages the production
+  export publishes with the committed ones under
+  `tests/production-export/bootstrap/`. `bootstrap/expected/` holds the
+  example-gate records. `BS-01` brings the register to 398 IDs.
 - A language-1.2 `tokenizer` elaborates, in linking, to ordinary definitions
   over the embedded text-laws library and to generated theorems the library
   proves (SPEC.md §17.12, `LM-01`..`LM-03`, `LM-13`, #30). The library is

CONFORMANCE.md

@@ -55,6 +55,12 @@ the error registry does not sanction (R5, `ERRORS.md`).
 | `AU-11` | `build` | Malformed core notation fails closed and never panics: an unclosed delimiter, a keyword used as a name, a label that is not the number of its node, a reference to a node not yet written, a numeral with a redundant leading zero, a statement that defines no node, a nesting beyond the bound, and every single-token deletion and duplication of a committed module fail with a registered code at a position in the notation or link to a module that decodes. |
 | `AU-12` | `build` | A core module written with names for its statements and its variables reads to exactly the module its canonical notation reads to, and the canonical notation keeps the names of the binders and writes the numbers of the statements: a variable is written by the name of its binder exactly when no nearer binder has the name, a constant a binder in scope is named like is written as a string, a theorem added to the certification library by name reads to the committed module and is written as the committed bytes, and an unknown or repeated statement name and a variable given universe levels are refused with a position. |
 
+## bootstrap
+
+| 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. |
+
 ## calculus
 
 | ID | Level | Statement |

README.md

@@ -138,7 +138,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 397 registered conformance IDs are implemented and pass; `just vv` runs clean from a checkout with the pinned toolchain installed.
+All 398 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.
 
@@ -179,6 +179,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 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` |
 

SPEC.md

@@ -6627,6 +6627,77 @@ realizes a library template, and no member recurses itself. Theorems over the
 members wait for equality of `Bytes` by evaluation; until then the module's
 behavior is held by the differential (`SL-01`).
 
+### 17.23 The bootstrap project
+
+The bootstrap project, `bootstrap/` beside `compiler/` and `stdlib/`, holds the
+components of LexLean's own pipeline that are authored as language-1.2 source
+and compiled by LexLean's production pipeline to certified Rust packages, so
+that the compiler's logic is eventually only `.lex.tex` (the self-hosting plan
+of issue 92). It is written in the authoring notation (§17.21) under the
+module prefix `LexLeanBoot`, and passes the gates of §28.6 as the standard
+library does. The Rust it replaces stays in the tree as the *stage-0 oracle*
+until the fixed point of that plan; a component is added only with a
+differential against that Rust, and is never a source of the Rust.
+
+A project reads only its own source roots (§10.1: a source root is a
+project-relative path that names no parent directory, and a symbolic link is
+refused), so a project cannot import another's modules. The module `Text` of
+the standard library (§17.22) is therefore present in `bootstrap/src/` as a
+copy of `stdlib/src/Text.lex.tex` in which the `production` declarations are
+removed, so that the copy is a library of the project and republishes none of
+the standard library's packages. `BS-01` compares the copy with the standard
+library's module on every run, and it is removed when a project can depend on
+another.
+
+The first component is the axiom-output parser (§22.5), the module
+`AxiomOutput`, with two production roots for `rust-std`:
+
+| Root | Oracle |
+| --- | --- |
+| `parseAuditOutput (stdout : Bytes) (expected : List Bytes) : Result (List (Bytes * List Bytes)) Rejection` | `verify::axiom::parse_audit_output` |
+| `isClosedLeanName (raw : Bytes) : Bool` | `ir::core::is_closed_lean_name` |
+
+The parser is the function of §22.5 on the bytes of valid UTF-8 text: the
+lines of `stdout` (`str::lines`), white space as Unicode `White_Space`
+(`str::trim`, `char::is_whitespace`) and not the ASCII white space of
+`Text.trim`, the optional information envelope, the reassembly of a record
+wrapped at the format width, the payload grammar with a duplicate-free axiom
+list sorted bytewise, and the rejection of a missing, duplicate, extra,
+reordered, or malformed record. The result is first-order data (§17.13 rule 1):
+`Result.ok` of the observed axioms per declaration, as an association list
+ascending by the declaration's bytes (the order of a `BTreeMap`), or
+`Result.error` of a `Rejection`, a structure of the diagnostic's `message` and
+the `declaration` it is about when the parser attributes it to exactly one
+expected declaration, as the oracle's `AuditFailure` does. The one diagnostic
+of the parser is `LLV7004`, the code of every `Rejection`; it is registered
+in the oracle and not carried in the data, so a host raises it from the
+rejection. The root takes no capability: it is the pure function whose host
+entry is the boundary of issue 92, and its input is the audit output the
+driver has read.
+
+A message is the oracle's message to the byte; a count in a message is written
+in base ten by the module, which has no formatting of a `Nat`. The
+association list is in the order of the sorted declaration names, so that a
+duplicated expected name is the rejection `duplicate record for` as it is for
+the oracle's map.
+
+`BS-01` holds both roots to the oracle. The lowered program of
+`parseAuditOutput` is run under the calculus evaluator (§17.14) on every
+committed golden vector of `tests/golden/axiom-parser/` (each line of
+`accepted.txt` and `rejected.txt`, each blank-line separated record of
+`accepted-wrapped.txt`, and each file whole against its declarations), and the
+rendered `rust-std` packages of both roots (§17.16), compiled by the pinned
+rustc, are run on a seeded corpus: records built from the payload grammar and
+its boundaries (names at the edges of the closed grammar, axiom lists of every
+length, every envelope shape and every malformed one, every Unicode white
+space), wrapped at every width, and mutated (a record dropped, duplicated,
+reordered, added, truncated, oversized, or given a stray byte). The outcome
+of a run is the result, the rejection's message, and its declaration, and one
+difference fails the case. Planted defects in the source are each detected by
+the same differential. Under the pinned Lean, the production export (§24.7)
+certifies both roots, and its packages are the committed ones under
+`tests/production-export/bootstrap/`.
+
 ## 18. Lean backend
 
 ### 18.1 Output contract
@@ -9424,14 +9495,15 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte
 | `RT-03` | `runtime` | A verification compiles every runtime module that a project's generated modules, or the calculus modules its certificates are checked against, import before the project's modules, replays it with `leanchecker`, and audits each of its declarations against the axioms its row pins; the committed verification of a project that uses the collections prints them, the runtime's own project verifies under the pinned Lean, and a row that pins another axiom set than its declaration observes fails with LLV7005. | §17.12, §22.3, §22.5, §22.6 |
 | `RT-04` | `runtime` | No Lean runtime text remains in the language-1.2 compiler: a generated language-1.2 module imports the runtime modules whose constants it names and declares nothing under a runtime namespace, and the only Lean runtime text in the compiler's source outside unit-test items, in one string literal or in several written together, is the decoder of core module 2, which loads native modules and so cannot be one; a runtime text planted in any of its shapes, raw or escaped, with or without a namespace line, split across literals, or after a test module, is found. | §17.12, §18.1 |
 | `SL-01` | `stdlib` | The standard library's `Text` module is language-1.2 source whose seven members over `Bytes` (`startsWith`, `endsWith`, `trim`, `lines`, `splitOn`, `joinWith`, `find`) are production roots eligible for `rust-std` with exactly their declared effects; each member's lowered program under the calculus evaluator and its rendered `rust-std` package under the pinned rustc agree with Rust's `starts_with`, `ends_with`, `trim_ascii`, `lines`, `split`, `join`, and `find` on a seeded corpus; a planted defect in a member is detected; and the certified packages the production export publishes for it are the committed ones. | §17.22 |
+| `BS-01` | `bootstrap` | 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. | §17.23, §22.5 |
 
 
 | `LM-01` | `language-models` | A `tokenizer` is a closed language-1.2 declaration whose scheme is `byte_level` or `longest_match` and whose vocabulary is a #29 artifact with role `vocabulary` and schema `utf8_lines`; tokens are `uint32`, the single bytes are the ids 0..255 present always as the byte fallback, the vocabulary pieces take the ids from 256 in artifact order, and the declaration elaborates to `encode` and `decode` over `bytes` together with `encodeText` and `decodeText` over `string` through `utf8_encode` and `utf8_decode`, so a scheme outside the closed enumeration, a vocabulary whose role or schema is not the one stated, or a token outside `uint32` is refused as a schema violation (`LLT4001`) or by the artifact rules (`LLR3007`). | §17.12 |
 | `LM-02` | `language-models` | A tokenizer's laws are generated and kernel-checked: `roundtrip` states that for every byte string `b`, `decode (encode b)` is `some b`; `text_roundtrip` states the same over `string`; and `in_range` states that every token a decode produces indexes the vocabulary, so the round trip also fixes the token boundaries, and a tokenizer whose elaboration does not close these laws fails verification. | §17.12 |
 | `LM-03` | `language-models` | Text that is not valid UTF-8 is refused and never tokenized: an artifact whose bytes do not decode under the `utf8_lines` schema — invalid UTF-8, a CR, or a missing final LF — fails by its artifact rules before any byte is decoded, and a text offered to `encodeText` that is not valid UTF-8 is refused rather than transcoded. | §17.12 |
 | `LM-13` | `language-models` | The text laws a tokenizer elaborates through are LexLean source and not authored text: the module that states them is one language-1.2 native core module of the embedded `language/text-1.2` project, the project holds no file of Lean source, no independently authored Lean file anywhere in the release tree declares the `LexLeanText` namespace or lies under its module root, and the one-time migration input is absent; the registry lists only that module, the declarations and their exact axiom policies are read from its native data, which the compiler embeds and hashes into the language-1.2 semantics, and a module that declares a text component imports the generated module rather than splicing any Lean text. | §17.10, §17.12 |
 
-**Total required capability IDs:** 397.
+**Total required capability IDs:** 398.
 
 No row may be downgraded to `some-true` or `open`. Upstream Lean facts are ledger/authority rows, not substitutions for these build behaviors.