feat(preservation): certificate B as kernel-term data (SP-16)

.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,91 @@ versions, and the entries below say what each tag does and does not claim.
 
 ## Unreleased
 
+- The decoder of a version 2 core module no longer takes a derived row from
+  the data (`SM-33`, SPEC.md §17.10, part 1 of #91 stage 2): a row whose name
+  the pinned Lean reserves (matcher equations and splitters, definition
+  equations and unfolding theorems, sparse `else_eq`) is made by Lean's own
+  reserved-name action and refused unless it equals the row. Every one of the
+  preservation library's 7,071 derived rows is remade exactly; no source,
+  lock, or compiler-semantics ID changes.
+- IEEE-754 bit patterns as exact dyadic rationals (#118, SPEC.md §17.12 rule
+  15, `MD-13`, language 1.2 only; the register is 404 rows). `Models.Recognizer`
+  decodes `binary32` and `binary64` bit patterns (and their little-endian
+  `Bytes` forms) to `(sign, mantissa, exponent)` over `nat` and `int`,
+  rejecting out-of-width patterns and the non-finite biased exponents, and
+  derives `round(a * b / c * 2^32)` scale ratios (ties to even) by exact
+  integer division; 43 theorems (39 in `Models.Recognizer`, 4 in `Models.Main`) are closed by `decide`. The change is to the
+  `models` example and the register only: no compiler source moves.
+
+- Widening conversions (#114, SPEC.md §17.12 *Widening conversions*, `SM-32`,
+  language 1.2 only). The total primitives `to_int` (any fixed-width integer to
+  `Int`) and `to_nat` (any unsigned fixed-width integer to `Nat`) elaborate in
+  linking to a single-evaluation `let` over bit tests (`bit_and`, `equal`) and a
+  balanced exact sum, so a production root decodes a byte string to integers
+  with no decimal text in its lowered program. Under language 1.0 and 1.1 they
+  are rejected with `LLT4001` and those identities are unchanged. Certificates read
+  elaborated declarations, so the certificate data needs no `to_int`/`to_nat`
+  rule. The register is 404 rows with `SM-32`; the language-1.2
+  compiler-semantics, semantic-IR (`12` to `13`), source, semantic, and build
+  IDs move, and the oracle tables are at versions 4 (`known-differences`) and 4
+  (`known-non-overlap`).
+- The Rust package scaffolding is data (#91 slice 1, SPEC.md §17.16, `RB-10`..`RB-13`, language 1.2).
+  The Cargo manifest's edition, publication, rustc and Clippy lint gates, and the ten allowed
+  lints, each now with its Clippy group, are the declarations of one semantic module,
+  `language/package-1.2/RustPackage.lex.tex`, which the compiler embeds, hashes into the
+  language-1.2 compiler-semantics ID, and reads by decoding its semantic data (it is not
+  evaluated and not spliced). `package::ALLOWED_LINTS` and the manifest template are gone; the
+  crate attributes are derived, `#![no_std]` from `allocation = false` on the target row of
+  `language/production-1.2.toml` and `#![forbid(lint)]` from each gate at `forbid`. No allowed
+  lint is in Clippy's `correctness` group, which the reader refuses and the module states as a
+  theorem; the SPEC §17.16 table equals the module's rows. `lexlean/rust-provenance/1` and the
+  package manifest `lexlean/rust-package/1` gain `effects` (#105 step 3b): the effects of the
+  realization on its profile, which production takes from the root's eligibility and the
+  renderer checks against what the package shows of itself; the `recursion` effect of
+  `language/production-1.2.toml` now says that exhausting the stack aborts the process.
+  Rendered `Cargo.toml` and `src/lib.rs` are byte-identical to the previous renderer's. The
+  language-1.2 compiler-semantics ID moves once; languages 1.0 and 1.1 are unchanged. The
+  register gains `RB-10`..`RB-13`.
+- Source packages (#161, SPEC.md §10.5, `PK-01`..`PK-04`, language 1.2 only).
+  A project declares `[[source_package]]` tables (`package`, `version`, `kind`
+  `path`, `path`), each naming a member project of the workspace an optional
+  `lexlean-workspace.toml` at the repository root lists, and imports its
+  modules by their own Lean names (`\importmodule{LexLeanStd.Text}`). The lock
+  gains `[[source_package]]` rows (tree digest over the package's manifest and
+  source files, manifest digest, version, prefix, its own packages) that every
+  command recomputes; a changed byte or version is `LLC0105` naming both
+  digests, a pin for an undeclared package `LLC0106`, a module prefix claimed
+  twice `LLC0107`, a project or path outside the workspace rule `LLC0108`
+  (a symlink or an escaping path is `LLS8001`), and an import of a package the
+  scope does not declare `LLR3009`. A package definition is an ordinary
+  definition of the importing project: its own `production:` roots are not
+  roots of the importer and nothing is re-exported. `verify` replays the
+  package modules under the package's prefix, with the package as their
+  `origin` in the build manifest, the snapshot, and the attestation; `fmt`
+  never writes a package file. The schema change moves the language-1.2
+  compiler-semantics ID once; languages 1.0 and 1.1, and a language-1.2 project
+  without source packages, keep their bytes apart from that identity. The
+  register gains `PK-01`..`PK-05` (403 rows with `SL-01`, `BS-01`, and `LM-01`..`LM-03`, `LM-13`); `PK-05`: the `bootstrap/`
+  pilot imports `stdlib/` through a source package, its vendored copy of `Text`
+  and the equivalence assertion of `BS-01` are deleted, the repository gains a
+  root `lexlean-workspace.toml`, and `xtask` stages a project with its packages.
+- 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
@@ -74,6 +159,45 @@ versions, and the entries below say what each tag does and does not claim.
   `leanchecker`; a mismatch is `LLI9001`, naming the record and both digests.
   Every CI job installs the same pinned toolchain, so this held by practice
   and is now checked.
+- No Lean source text template remains in the production compiler (SPEC.md §17.17, `SP-17`; stage 4 of #89): the staged audit module is an auxiliary module of typed commands, the calculus-to-Lean-text builders that certificate B's old path left (`render_ty`, `render_value`, `render_program`, `lean_type_text`, `lean_list`, `budget_options`) are deleted or moved to the conformance crate, and a lexer-level scan of `production/` and the auxiliary part of `backend/lean.rs` is shown to fail on a planted template (register 413).
+- Certificate B as kernel-term data (SPEC.md §17.17, `SP-16`; stage 2 of #89).
+  The per-function correspondence of every production root is no longer written
+  as Lean text by `production/rust_cert.rs` and `production/rust_term.rs`: the
+  compiler builds it as a native core module of schema `lexlean/core-module/2`
+  (`production/certificate/data_b`) on the vehicle of certificates E and A. The
+  program and the crate are kernel terms (the crate constructor for constructor
+  as the text printed it), each of the 49 rules of `Corr` is applied with every
+  argument written (the judgment the aligner derives, and the values it holds),
+  `FunOK` is written out as its witnesses and the derivation, and `crate_ok` is
+  a case analysis on the function index in place of a tactic block. The library
+  did not grow: no explicit-argument form was needed, so the language-1.2
+  identity does not move for this stage. The verify record holds the module in
+  the authoring notation (`R<i>/RustStd.lex.tex` in place of `.lean`), which
+  reads back to the data byte for byte, and `preservation.json` and the
+  production export bind those bytes. The statements of the 76 certificates B
+  of the four corpora are those the text stated, up to the kernel's
+  definitional equality (`tests/preservation-certificates/B-STATEMENTS.md`).
+  The aligner moved to `production/certificate/data_b/align.rs`, the Rust-term
+  renderer is gone, and the Rust machine's conformance harness evaluates the
+  crates by the same kernel terms. No diagnostic code is new; the register
+  gains `SP-16` (394 rows).
+- Certificate A as kernel-term data (SPEC.md §17.17, `SP-15`; stage 3 of #89).
+  The preservation certificate of every production root is no longer written as
+  Lean text by `production/certificate.rs`: the compiler builds it as a native
+  core module of schema `lexlean/core-module/2` on the vehicle of
+  certificate E (`production/kernel.rs`), the program literal, encoders, width
+  predicates, relation theorems, validators, and entry as rows, each lemma
+  applied with every argument written, structural and well-founded recursion as
+  recursor and `WellFounded.fix` terms with the source's own decrease theorems,
+  and the collection templates' clause proofs as kernel terms in place of
+  tactics. The verify record holds the module in the authoring notation
+  (`R<i>.lex.tex` in place of `R<i>.lean`), which reads back to the data byte
+  for byte, and `preservation.json` binds those bytes. The statements of the 57
+  certificates A of the four corpora are those the text stated, up to the
+  kernel's definitional equality
+  (`tests/preservation-certificates/A-STATEMENTS.md`). Roughly 5 000 lines of the
+  text generator are gone from `production/certificate.rs`. Certificate B is
+  still Lean text. No diagnostic code is new; the register gains `SP-15` (403 rows).
 - Certificate E as kernel-term data (SPEC.md §17.17, `SP-14`; stage 1 of #89,
   stage 5 of #27). The composition certificate of every production root is no
   longer written as Lean text by `production/certificate.rs`: the compiler
@@ -88,9 +212,9 @@ versions, and the entries below say what each tag does and does not claim.
   policies, forbidden constants) and the audit module prints and checks the
   axioms of every one of its rows. The statements of the 76 certificates E of
   the four corpora are those the text stated, kernel term for kernel term
-  (`tests/preservation-certificates/E-STATEMENTS.md`). Certificates A and B are
-  still Lean text, so the data certificate is rendered outside the module
-  system until they follow. Languages 1.0 and 1.1 have no certificates and are
+  (`tests/preservation-certificates/E-STATEMENTS.md`). Certificate B (and, until
+  stage 3 of #89, certificate A) is still Lean text, so the data certificate is
+  rendered outside the module system until they follow. Languages 1.0 and 1.1 have no certificates and are
   untouched. No diagnostic code is new; the register gains `SP-14` (383 rows with `SP-13`, `RB-09`, and `PX-13`).
 - Program equalities over all inputs (#117, SPEC.md §17.12, `PF-20`..`PF-23`,
   no new diagnostic code). Language 1.2 orders `Int` and every fixed-width