feat(core): derived rows are made by Lean's reserved-name actions and checked (SM-33, stage 2 of #91, part 1)

CHANGELOG.md

@@ -15,6 +15,13 @@ 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.
 - 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

CONFORMANCE.md

@@ -536,6 +536,7 @@ the error registry does not sanction (R5, `ERRORS.md`).
 | `SM-29` | `build` | Reordered equivalent map, set, and graph literals link to byte-identical semantic data and generated Lean, LaTeX, and lexicon-closure artifacts, while duplicate keys, non-literal literal keys, and key types without a canonical order are rejected. |
 | `SM-30` | `build` | Language 1.2 graph literals reference only declared nodes, a graph's nodes are its keys and every successor, and successor, reachability, and topological-order queries are deterministic, bounded by the node count, and report a cycle as none. |
 | `SM-31` | `build` | Language 1.2 accepts a second native core-module schema, and only language 1.2 does, whose annotation nodes, extended names, definition safety and groups, compiled and reducibility state, and matcher, projection, no-confusion, simplification, equation-record, inlining, sparse-casesOn, and grind extension state are closed data that the linker validates against the kind of the declaration carrying it and bounds in depth by max_scope_depth, and that both backends render, and that the Lean backend's one fixed decoder submits through Lean's checked declaration API, so that the generated module elaborates under the pinned Lean with exactly its pinned axioms. |
+| `SM-33` | `build` | A version 2 core-module row whose name the pinned Lean reserves is not submitted as data: the decoder runs the pinned Lean's own action for the name and refuses the module when the action does not make the name or makes a constant whose kind, levels, type, or value differ from the row's. |
 
 ## stdlib
 

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 403 registered conformance IDs are implemented and pass; `just vv` runs clean from a checkout with the pinned toolchain installed.
+All 404 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.
 
@@ -159,7 +159,7 @@ Every row is validated by `just vv`; the IDs link the claim to its register row,
 | Total lexical closure: every accepted atom is covered by exactly one declared origin | `LX-01`..`LX-14` | `build` |
 | Versioned lexicon packages with closed schemas, denotations, and renderer tokens | `GL-01`..`GL-18` | `build` |
 | Fixed structural, mathematical, and proposition grammar with closed ambiguity handling | `GR-01`..`GR-16` | `build` |
-| Typed closed IR with canonical serialization, native core modules (and the second schema of them that lossless migration of the proof library needs), portable language-1.1 application data and operations, versioned language-1.2 semantic modules, products, and first-class functions, ordered collections and graphs, semantic snapshots, alpha identities, recursion evidence, and content identities | `SM-01`..`SM-31` | `build` |
+| Typed closed IR with canonical serialization, native core modules (and the second schema of them that lossless migration of the proof library needs), portable language-1.1 application data and operations, versioned language-1.2 semantic modules, products, and first-class functions, ordered collections and graphs, semantic snapshots, alpha identities, recursion evidence, and content identities | `SM-01`..`SM-33` | `build` |
 | Document and generic semantic declarations with exact self-application, type checking, structural recursion, recursive and mutual language-1.2 data, generic and executable higher-order definitions, mutual and well-founded recursion with semantic evidence, explicit state threading, and acyclicity rules | `DF-01`..`DF-18` | `build` |
 | The structured proof language with pinned Lean lowerings, including closed linear arithmetic, integer order, and the fold laws | `PF-01`..`PF-23` | `build` |
 | Prose-free deterministic generated Lean with complete token traceability | `LN-01`..`LN-12` | `build` |

SPEC.md

@@ -2378,7 +2378,9 @@ axiom audit. Any other generated row without a native owner is rejected. This
 classification is generic and structural: it is not selected by an Atlas
 name, module, or feature. Generated Lean may import only the foundational
 modules listed in the core data and other modules in the generated graph. The
-generic environment-reconstruction runtime may privately import `Lean`; no
+generic environment-reconstruction runtime may privately import `Lean`, and
+the runtime of a version 2 module also `Lean.Meta.Constructions.SparseCasesOn`
+in full (below); no
 generated module may import an independently authored implementation of the
 declarations being generated.
 
@@ -2437,7 +2439,31 @@ are data of the module, not conventions of a backend.
   (two constants of one module may be the same construction, which a shared
   cache would otherwise return once), numbered and visible as the row's name
   shows, and refuses the module unless the constant, its name, and its record
-  are those the row states.
+  are those the row states. It then enters the constant in the elaborator's
+  cache of sparse `casesOn`, under the exported and the private key unless
+  the key is taken, so that a later construction that needs the same one
+  finds it, as it did when the elaborator made the module; each chunk first
+  drops from the cache the runtime's own constants, which are not the
+  module's. The cache is private to its Lean module, which the runtime
+  therefore imports in full. A certificate rendered outside the module
+  system (§17.17) cannot import a module in full; it states theorems only,
+  no sparse `casesOn` and no derived row, and its runtime leaves the cache
+  alone.
+- A row whose name the pinned Lean reserves (`Lean.isReservedName`: the
+  equations and splitter of a matcher, the equations and unfolding theorem
+  of a definition, the `else_eq` of a sparse `casesOn`, and the other names
+  a registered reserved-name action makes) is not submitted: the decoder runs
+  the action the pinned Lean registers for the name and refuses the module
+  unless the action makes the constant and the constant has the row's kind,
+  levels, type, and value. A row whose constant an earlier action of the
+  module already made is checked the same way. So that each action makes what
+  the elaborator made, the state it reads is installed as each row is added,
+  not after the module: the `recursive` tag, the transparency, the matcher
+  record, the equational-lemma record, and the row's realization context,
+  which for a definition with an equational-lemma record is opened once its
+  smart-unfolding row (`_sunfold`) is in. A derived row is therefore what the
+  pinned Lean derives from the module, checked against the data rather than
+  taken from it.
 
 A version 2 row that states a field of another kind of declaration is
 rejected; the group of a definition names only declarations of the module; an
@@ -9260,6 +9286,7 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte
 | `SM-29` | `semantic-ir` | Reordered equivalent map, set, and graph literals link to byte-identical semantic data and generated Lean, LaTeX, and lexicon-closure artifacts, while duplicate keys, non-literal literal keys, and key types without a canonical order are rejected. | §17.12, §21 |
 | `SM-30` | `semantic-ir` | Language 1.2 graph literals reference only declared nodes, a graph's nodes are its keys and every successor, and successor, reachability, and topological-order queries are deterministic, bounded by the node count, and report a cycle as none. | §17.12 |
 | `SM-31` | `semantic-ir` | Language 1.2 accepts a second native core-module schema, and only language 1.2 does, whose annotation nodes, extended names, definition safety and groups, compiled and reducibility state, and matcher, projection, no-confusion, simplification, equation-record, inlining, sparse-casesOn, and grind extension state are closed data that the linker validates against the kind of the declaration carrying it and bounds in depth by max_scope_depth, and that both backends render, and that the Lean backend's one fixed decoder submits through Lean's checked declaration API, so that the generated module elaborates under the pinned Lean with exactly its pinned axioms. | §17.10 |
+| `SM-33` | `semantic-ir` | A version 2 core-module row whose name the pinned Lean reserves is not submitted as data: the decoder runs the pinned Lean's own action for the name and refuses the module when the action does not make the name or makes a constant whose kind, levels, type, or value differ from the row's. | §17.10 |
 | `DF-01` | `declarations` | A valid type-definition sentence emits one nonrecursive sort-valued Lean def linked to its document entry. | §15.7, §18.6 |
 | `DF-02` | `declarations` | A valid term-definition sentence emits one nonrecursive explicitly typed Lean def. | §15.7, §18.6 |
 | `DF-03` | `declarations` | A valid predicate-definition sentence emits one nonrecursive Prop-valued Lean def. | §15.7, §18.6 |
@@ -9554,7 +9581,7 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte
 | `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:** 403.
+**Total required capability IDs:** 404.
 
 No row may be downgraded to `some-true` or `open`. Upstream Lean facts are ledger/authority rows, not substitutions for these build behaviors.
 

VERIFICATION.md

@@ -1254,6 +1254,62 @@ What was not run on the development host: the verification of
 its records do not depend on this change and CI reverifies them) and
 `conformance_vr_19`. The CI legs run both.
 
+### a derived row is what the pinned Lean derives
+
+A version 2 row whose name the pinned Lean reserves is made by Lean's own
+reserved-name action and refused unless it equals the row (`SM-33`, §17.10,
+#91). Run with the pinned Lean 4.32.1 on WSL, on `main` `c183f250` with the
+change. The plants that change the library or the decoder were run with
+`lexlean lock && lexlean verify` in a copy of the project of
+`tests/negative/preservation-drift`, the compiler rebuilt for each, and the
+file restored with `git checkout`. Unplanted, the same command verifies
+(`verified 2 modules`): all 7,071 derived rows of the library are remade
+exactly.
+
+Planted (a): the value of the derived row
+`entriesOf.match_3.eq_1` in `src/RustMatches.lex.tex` replaced by its own
+type node (`@234896` to `@234887`). Expected: the theorem Lean's matcher
+equations make differs from the row, and the module is refused.
+
+```text
+error[LLV7014]: preservation environment: `LexLeanPreservation.RustMatches` does not compile silently under the pinned Lean: error: native core declaration '_private.LexLeanPreservation.RustMatches.#0.LexLeanPreservation.Rust.entriesOf.match_3.eq_1':
+  core declaration '_private.LexLeanPreservation.RustMatches.0.LexLeanPreservation.Rust.entriesOf.match_3.eq_1' is not what the elaborator's construction makes
+```
+
+Planted (b): a remade sparse `casesOn` no longer entered in Lean's sparse
+`casesOn` cache (`crates/lexlean/src/backend/core_v2.rs`, the loop over the
+two keys made empty). Expected: the splitter proof of a matcher finds no
+cached constant under the private key, makes its own, and differs from the
+row.
+
+```text
+error[LLV7014]: preservation environment: `LexLeanPreservation.RustLemmas` does not compile silently under the pinned Lean: error: native core declaration '_private.LexLeanPreservation.RustLemmas.#0.LexLeanPreservation.Rust.sem_part.match_1_1.eq_2':
+  core declaration '_private.LexLeanPreservation.RustLemmas.0.LexLeanPreservation.Rust.sem_part.match_1_1.eq_2' is not what the elaborator's construction makes
+```
+
+Planted (c): the decoder's own constants kept in the cache (the filter at the
+start of `decodeAndAdd` removed). Expected: the splitter of
+`entriesOf.match_3` takes the decoder's `addOneUnchecked._sparseCasesOn_1`,
+cached under the same key, instead of the module's constant.
+
+```text
+error[LLV7014]: preservation environment: `LexLeanPreservation.RustMatches` does not compile silently under the pinned Lean: error: native core declaration '_private.LexLeanPreservation.RustMatches.#0.LexLeanPreservation.Rust.entriesOf.match_3.eq_2':
+  core declaration '_private.LexLeanPreservation.RustMatches.0.LexLeanPreservation.Rust.entriesOf.match_3.eq_2' is not what the elaborator's construction makes
+```
+
+Planted (d): the comparison in `sameAsRow` disabled (its condition prefixed
+with `true ||`). Command: `cargo test -p repo-conformance --test conformance
+-- conformance_sm_33`. Expected: the fixture whose `eq_1` has another proof of
+the same statement is no longer refused.
+
+```text
+thread 'conformance_sm_33' panicked at crates/conformance/src/support.rs:641:14:
+verify fails
+test result: FAILED. 0 passed; 1 failed; 0 ignored; 0 measured; 386 filtered out
+```
+
+Removed: every plant was reverted; `conformance_sm_33`, `conformance_sm_31`,
+`conformance_sp_12`, and `conformance_rp_07` pass, and `cargo xtask check-fixtures` holds 269 fixtures equal (on `main` `32afe5da`).
 ### the fold laws can fail
 
 Integer order, `linear_arithmetic` over the runtime, the fold laws, and the