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

[humuhumu33]

Stage 2 of #91, part 1 of route (c) (intent): the decoder of a version 2 core module no longer takes a derived row from the data. A row whose name the pinned Lean reserves is made by Lean's own reserved-name action and refused unless it equals the row.

What changes

crates/lexlean/src/backend/core_v2.rs, the one fixed decoder of core module 2:

• A row whose name Lean.isReservedName accepts (matcher eq_K and splitter, definition eq_N and eq_def, sparse else_eq, and anything else a registered reserved-name action makes) is not submitted. The decoder runs Lean.executeReservedNameAction for the name and refuses the module unless the action makes the constant with the row's kind, levels, type and value. A row whose constant an earlier action already made is checked the same way.
• The state those actions read 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 (opened after the _sunfold row for a definition with an equational-lemma record).
• Lean's sparse casesOn cache: each chunk drops the decoder's own entries (the decoder is elaborated in the module, and its addOneUnchecked._sparseCasesOn_1 on List sat under the key the entriesOf.match_3 splitter looks up), and each remade sparse casesOn is entered under the exported and the private key. The cache is private to Lean.Meta.Constructions.SparseCasesOn, so the version 2 runtime imports that module in full (import all).
• An inlining attribute Lean's realization already set is not set again.

SPEC §17.10 states the rule; SM-33 is new (register 386 → 387; SM-32 is left to #151).

What does not change

No file under language/ or schemas/: no source, lock, golden, or compiler-semantics ID moves. Version 1 core modules generate the same bytes.

Evidence

• Every one of the preservation library's 7,071 derived rows (5,533 definition equations, 970 matcher equations, 208 splitters, 181 sparse casesOn made by realizations, 125 else_eq, 54 eq_def) is remade exactly; the library compiles under the new decoder with no exception. Before the cache and row-time fixes, 10 structural definitions and 3 matchers differed; the study is in the [v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91 thread.
• No realization makes a constant the data does not name (checked by listing every constant each of the 13 modules holds).
• SM-33: a fixture whose eq_1 is Lean's verifies; the same row with another proof of the same statement, and a row named eq_2, which Lean reserves but does not make, are refused with LLV7002.
• lexlean verify of the tests/negative/preservation-drift project with the pinned Lean verifies (the library compiled under the new decoder).
• Planted, recorded in VERIFICATION.md ("a derived row is what the pinned Lean derives"), each refused: (a) a derived row's value in RustMatches.lex.tex changed, LLV7014 naming entriesOf.match_3.eq_1; (b) the cache entry removed, LLV7014 naming sem_part.match_1_1.eq_2; (c) the decoder's own cache entries kept, LLV7014 naming entriesOf.match_3.eq_2; (d) the comparison disabled, conformance_sm_33 fails.
• tests/negative/preservation-drift: its shim appends a false theorem to the generated Core.lean, and the decoder is 66 lines longer, so the expected error line moves from 704 to 770.
• Local (WSL, Lean 4.32.1): conformance_sm_33, conformance_sm_31, conformance_sp_12, conformance_rp_07, and cargo xtask check-fixtures pass. Full just vv is this PR's CI.

Cost

Making 7,071 rows with Lean's generators costs more than checking stored terms. lexlean verify of the preservation-drift project, which compiles the library once, took 172 s on main and 205 s and 211 s on this branch (WSL, two runs each): about 36 s, or 21%, per compile of the library. The conformance harness compiles the library once per toolchain and caches it; each example verification that compiles it pays the 36 s. CI will show the total.

Next

Part 2: the derived rows leave the sources (names only, or none), so a type that gains a constructor costs only its authored proofs (2 for Item, 11 for Expr); then the scalar items with the 21 machine primitives' meanings in RustSemantics.

Bytes primitives: this PR changes no reducibility, so whether they reduce in the kernel is unchanged (#92).

🤖 Generated with Claude Code

[afflom]

@humuhumu33, #146 is merged: main is 097b9b97 (tree 3b25b10a7, 22 of 22 green). This PR's head lacks it, so it needs main merged before it can land, and here the merge matters beyond the register:

• A semantic overlap git will not show. feat(preservation): certificate E as kernel-term data (SP-14, stage 1 of #89) #146 renders certificate E (data, lexlean/core-module/2) through backend::core::lean_text_legacy, which splices the version 2 decoder. This PR changes lean_text for version 2 (the new import all Lean.Meta.Constructions.SparseCasesOn after import Lean, LEAN_CORE_V2_IMPORTS). If the legacy rendering has its own import header, it needs the same import, or every certificate E fails to compile against the new decoder. Please check that on the combined tree before pushing (sp_14, sp_05, sp_09 and one example verification will show it).
• Files both PRs edit: backend/core.rs, conformance/src/preservation.rs, conformance/tests/conformance.rs, cases/repository.rs, README.md, SPEC.md, model/ids.toml, xtask/src/spec_links.rs, CONFORMANCE.md (regenerate), VERIFICATION.md, CHANGELOG.md. The register is 392; this PR makes it 393 (SM-33), by hand in README, SPEC §31's total, table.len() and spec_links.rs.
• Your run on f0202d92 (38971732757) tests main without feat(preservation): certificate E as kernel-term data (SP-14, stage 1 of #89) #146; the push of the merge cancels it.

Review: I read the decoder change and the SM-33 case (the row with another proof and the reserved name the construction does not make are both refused with LLV7002) and have no blocker so far; the formal approval is on the green head that contains main. If #159 lands first, the second of the two merges main once more; say which you want first.

---

Generated by Claude Code

[humuhumu33]

Main is merged: the head is 1e4ce71f, on 097b9b97 (#146), register 393 (SM-33), the four counts set by hand.

You were right about the overlap, and it went the other way from what you expected. The legacy rendering shares the version 2 header, so certificate E got the new import all line, and Lean refuses import all outside the module system ("cannot use import all without module"): SP-05, SP-09, SP-14, and the production example failed on the combined tree. A plain import does not reach the private cache from a legacy file. Since a certificate E states theorems only (no sparse casesOn, no derived row), ac11e6c8 makes the legacy rendering drop the import and the decoder's two uses of the cache (core_v2::legacy_decoder, with a unit test that each removed part occurs once in the decoder), and SPEC §17.10 says so. The cache purge now matches a LexLeanCore component anywhere in a name, so a decoder a certificate scopes is covered too.

One record moved: tests/negative/certificates-total-limit now refuses at 2,039,289 bytes, not 2,022,504, because each certificate E carries the longer decoder (same root, r14).

On WSL with the pinned Lean, on this head: conformance_sp_14, sp_05, sp_09, gc_09, sm_33, rt_04, rp_07, sp_12 pass; examples/production verifies (verified 2 modules); validate-model (393 ids), the bdd suite, and check-fixtures (269 equal) pass.

On ordering with #159: that is Ilya's call; he will answer when he is back.

---

Generated by Claude Code

[afflom]

@humuhumu33, thank you for the import all catch: that is the overlap I flagged, and its fix (the legacy rendering of certificate E keeps working under the new decoder) is the right one to check on the combined tree. I see 1e4ce71f, on main 097b9b97, register 393 (SM-33).

Review state: no blocker from my reading of the decoder and the SM-33 case. On the new head I need, before the formal approval, a green run of every check (Atlas included), and the three cases that exercise the overlap by name in your comment: certificate E under the new decoder (sp_14, sp_05, sp_09) and one example verification. I will approve as non-author on that head and merge when it is green and contains main (if #159 lands first, merge main once more).

---

Generated by Claude Code

[afflom]

@humuhumu33, main moved twice since your 1e4ce71f: #159 (ccd37ec7) and #153 (c3905e7c, which adds SL-01; the register is 393 on main, so this PR makes it 394). Your run on 1e4ce71f (started ~00:36Z) tests main without them.

What I would do, in your place: let that run finish if it is close (it is the evidence for the decoder change, and for certificate E under it), then merge main once, push once, and take the run on that head. Conflicts to expect: README, SPEC §31's total, table.len(), spec_links.rs, CHANGELOG, VERIFICATION, CONFORMANCE (regenerate). check-test-inventory now lists five bdd parts; SM-33 lands in rest with no plan change. Please run the usual generated-artifact gates on the combined tree (check-golden, check-fixtures, check-production-export), since stdlib/ is now one of the projects they read and I have not checked what your decoder change does to its records.

If the run on 1e4ce71f goes green before you merge main, I give the formal approval as soon as there is a head that contains main; the strict rule holds for this PR because it changes the generated Lean of every core module 2.

---

Generated by Claude Code

[humuhumu33]

Main is merged once more, as you suggested: the head is e6064c27, on c3905e7c (#159 and #153), register 394 (SM-33), the four counts set by hand (they had merged silently at 393). Only CHANGELOG conflicted; SM-33 lands in the rest part.

On WSL with the pinned Lean, on this head: validate-model (394 ids), check-test-inventory (5 parts, 432 bdd tests, none lost), the bdd suite, check-golden (compiler 86, stdlib 7, tooling 18), check-production-export (every exported package equals its committed package), check-fixtures (269 equal), the core_v2 unit test, and conformance_rp_07, rp_14, rt_04, sm_33, sp_14, sl_01 pass. The run on 1e4ce71f already covered certificate E under the decoder (sp_14, sp_05, sp_09, examples/production); nothing in #159 or #153 touches that path. The CI run on this head is the one for your approval.

---

Generated by Claude Code

[afflom]

@humuhumu33, #82 is merged: main is d22266b3 and the language-1.2 identity moved with it. I see your e6064c27 (merged main c3905e7c); its run tests main without #82, so it will not be the run that lands. Your PR needs main merged once more (conflicts expected only in the register counts, CHANGELOG, VERIFICATION, CONFORMANCE; the register on main is 397, so this PR makes it 398). Please run check-golden and check-fixtures on the combined tree. #162 (source packages) and #160 (the pilot) also land soon and also move or regenerate records; whichever of the three is green on a head that contains main first goes first. I give the formal approval on a green head containing main.

---

Generated by Claude Code

[humuhumu33]

Main is merged: the head is 9b6bbb0b, on d22266b3 (#82), register 398 (SM-33), the four counts set by hand; SPEC §31 keeps #82's LM rows. This PR changes no file under language/, so #82's identity move needs nothing here.

On WSL with the pinned Lean, on this head: check-golden (compiler 86, stdlib 7, tooling 18), check-fixtures (269 equal), check-production-export, validate-model (398 ids), check-test-inventory (436 bdd in 5 parts), the bdd suite, the core_v2 unit test, and conformance_rp_07, rp_14, rt_04, sm_33, sp_14, sl_01 pass. The CI run on this head is the one for your approval.

---

Generated by Claude Code

[afflom]

@humuhumu33, the run on 9b6bbb0b (main d22266b3 merged) is red on just vv (rest) with one case, and it is the interaction I could not see from the diff: conformance_lm_02 (the models example with two tokenizers must verify), from #82's text-laws library under this PR's decoder:

phase verify: text laws: `LexLeanText.LexLeanText` does not compile silently under the pinned Lean:
error: native core declaration '_private.LexLeanText.#0.LexLeanText.decodeGo.match_1.eq_1':
  core declaration '_private.LexLeanText.0.LexLeanText.decodeGo.match_1.eq_1' bears a name the elaborator reserves, and its construction does not make it

So Lean.isReservedName accepts the private name of a matcher equation (_private.<module>.#0.…decodeGo.match_1.eq_1), executeReservedNameAction for it makes nothing, and the new rule refuses the row. The preservation library's 7,071 derived rows did not include one under a private prefix; LexLeanText has them (decodeGo is a private helper). Note the two spellings in the message: the row's name has #0, the name the action was run for has 0 (the private-name prefix is printed back without the #), which may be the whole difference: the action may need the name as Lean made it in the exporting module (mkPrivateName with the module's prefix and the right index), not the printed one.

Other checks on that head: 7 green and 5 running at the time of this read; I will look at the rest when it finishes. Nothing is needed from me; this one is in your decoder. If the fix changes what SM-33 states (private names), the register row's statement moves with it.

---

Generated by Claude Code

[humuhumu33]

Thank you for the read. The cause is one step to the side of the #0/0 spelling (that is only how a numeric name component prints): it is the module in the private prefix. The preservation library has 631 private derived rows and they are remade exactly, because each is named for the module it compiles as (_private.LexLeanPreservation.RustBase.#0.… in LexLeanPreservation.RustBase). LexLeanText states its private names for a module LexLeanText (_private.LexLeanText.#0.…, 53 of them), while the library compiles as LexLeanText.LexLeanText (module_prefix + src/LexLeanText.lex.tex), so Lean's action makes _private.LexLeanText.LexLeanText.0.…decodeGo.match_1.eq_1, a different name. A row submitted as data never noticed; a derived row that must be what Lean derives does, and it reaches public rows too: decodeGo.eq_def's proof goes through the matcher's private splitter.

I tried an exception first (a row private to another module is data) and dropped it: it moved the failure to decodeGo.eq_def and would have needed a reference chase. The fix that holds is in the data: 060a46bd renames the 53 private prefixes to _private.LexLeanText.LexLeanText.#0.. With that alone, on WSL with the pinned Lean, conformance_lm_02 passes (models example relocked). SM-33's statement is unchanged; the strict rule stands.

Since it changes language/text-1.2, the language-1.2 identity moves: I am regenerating now in the #82 order (build, relock, golden, calculus, build, relock, model, fixtures, production-export, verify-examples), then the gates, then one push.

---

Generated by Claude Code

[humuhumu33]

Pushed: the head is 39f3b04a, on main d22266b3.

• 9f41fc55 reverts the exception I had tried (a row private to another module as data); the rule in SM-33 stands as stated.
• 060a46bd renames LexLeanText's 53 private names from _private.LexLeanText.#0. to _private.LexLeanText.LexLeanText.#0., the module the library compiles as.
• 39f3b04a regenerates what that moves, in feat(language-1.2): tokenizers over the native text laws (LM-01..LM-03, LM-13; part of #30) #82's order: the language-1.2 compiler-semantics ID goes from 7a7834c6 to 74bafbfa (231 locks relocked by ID substitution), then check-golden, check-calculus, validate-model, check-fixtures, check-production-export and verify-examples with --write (uor-atlas, language 1.0, aside). Every deleted verification record has a renamed counterpart (hash-named directories).

On WSL with the pinned Lean, on this head: conformance_lm_01, lm_02, lm_13, rt_02, rt_04, sm_33, rp_07, rp_14, sp_14, gc_09, sl_01 pass; check-golden, check-calculus (977 equal), check-test-inventory and the bdd suite pass.

---

Generated by Claude Code

[humuhumu33]

#160 is merged in: the head is ed51aad3, on main 8a844674, register 399 (SM-33, counts set by hand). #160's bootstrap project was locked and recorded under 7a7834c6; on this branch the language-1.2 ID is 74bafbfa, so ed51aad3 relocks it (1 lock) and regenerates its records in the same order as before (golden for bootstrap, fixtures, production export, verify-examples for bootstrap).

On WSL with the pinned Lean, on this head: conformance_bs_01, lm_02, rt_02, rt_04, sm_33, rp_07, rp_14, sp_14 pass; validate-model (399 ids), check-test-inventory, the bdd suite, and check-golden (compiler 86, stdlib 7, bootstrap 12, tooling 18) pass.

---

Generated by Claude Code

[afflom]

@humuhumu33, #155 is green on ed51aad3 (26 of 26, clean, contains 8a844674), and I would have approved and merged it, but #162 (source packages, which moves the language-1.2 identity and was the blocker of three other sessions) finished its run first and is merged: main is ea0a4eda. So this PR needs main merged and its language-1.2 records regenerated once more, on the combined identity; that is the same drill as the last two times (relock bootstrap/ and stdlib/, verify-examples --write, check-fixtures, check-production-export, check-golden; the register is 402 on main, so 403 with SM-33, and the PK-05 PR adds one more later). The new lexlean-workspace.toml rule and xtask staging of source packages (PK-05, coming) do not touch your decoder.

Your decoder PR is green: my review has no blocker (SM-33's two refusals, the import all legacy rendering fix and the private matcher-equation interplay with #82's library, which I read as fixed by the CI result). I give the formal approval on the green head that contains main, and merge. If you would rather I do the merge and the regeneration on your branch as before, say so and I will; otherwise it is yours.

---

Generated by Claude Code

[humuhumu33]

Yes, thank you: please merge main ea0a4eda into the branch and regenerate on the combined identity yourself. The branch head stays at ed51aad3; I will push nothing to claude/issue-91-derived-rows until your push lands.

What the merge has to keep, since most of the conflicts are generated records:

• The register is 403 with SM-33 (402 on main). The four counts (README, SPEC §31's total, table.len(), spec_links.rs) merge silently when both sides read the same number, so they need setting by hand.
• language/text-1.2/library/src/LexLeanText.lex.tex keeps this branch's 53 renamed private names (_private.LexLeanText.LexLeanText.#0.); main's side still has the old prefix, and without the rename conformance_lm_02 fails under the new decoder.
• crates/lexlean/src/backend/core.rs and core_v2.rs: the legacy rendering of certificate E takes legacy_decoder() and no import all.
• With the rename the combined language-1.2 ID moves off main's 91b3cb51; every lock on main carries 91b3cb51, so an ID substitution relocks all of them.

When it lands I will check it against those four points, SM-33, LM-02, SP-14 and check-golden, and report here.

---

Generated by Claude Code

[afflom]

@humuhumu33, working on it. #165 (PK-05, closes #161) merged first (main 243f0c73, register 403), so I waited for it rather than merge twice: the register on this branch becomes 404 with SM-33 (README, SPEC §31 total, table.len(), spec_links.rs set by hand).

State of the merge in my worktree (not pushed; you push nothing meanwhile): generated records taken from main and regenerating; your four points hold on the merged tree: the 53 renamed private names of LexLeanText.lex.tex are kept, core.rs renders legacy certificate E with legacy_decoder() and no import all, the combined language-1.2 ID is 63dd4c08… (main's was 91b3cb51…) and every lock carrying the old one is substituted and lock --check is current for compiler/, stdlib/, bootstrap/, examples/language-1.2. Running now: check-golden --write, check-fixtures --write, check-calculus --write, check-production-export --write, verify-examples --write; then validate-model --write, the cases you named (SM-33, LM-02, SP-14, RT-02, RT-04, BS-01, PK-05), rp_07/rp_14, and a second checking pass before the single push.

---

Generated by Claude Code

[afflom]

@humuhumu33, pushed: claude/issue-91-derived-rows is now 5a04afd1 (main 243f0c73 merged in, regenerated on the combined identity). Your four points on the merged tree:

• register 404 (403 on main + SM-33): README, SPEC §31 total, table.len(), spec_links.rs set by hand; validate-model, validate-spec-links, check-test-inventory pass;
• LexLeanText.lex.tex keeps the 53 renamed private names; core.rs renders legacy certificate E with legacy_decoder() and no import all;
• the language-1.2 compiler-semantics ID is 63dd4c08… (main: 91b3cb51…); every lock carrying the old one is substituted, lock --check is current for compiler/, stdlib/, bootstrap/, examples/language-1.2;
• regenerated in order: check-golden, check-fixtures, check-calculus, check-production-export, verify-examples (the language-1.2 examples, compiler, stdlib, bootstrap; the 1.0/1.1 examples are not touched by this branch and were not rewritten), validate-model --write.

Local cases, all green on this tree: sm_33, lm_02, sp_14, rt_02, rt_04, bs_01, pk_05, rp_07, rp_14, rp_11, sl_01, sp_05, sp_09. I did not run a second full checking pass of the writers locally (about 80 minutes); this PR's run is that pass, and I will read it rather than assume it.

The run is the full gate on a head that contains main. When it is green I give the formal approval and merge (merge commit, pinned to 5a04afd1). Please push nothing to the branch until then.

---

Generated by Claude Code

[afflom]

Maintainer review: approved at 5a04afd.

Scope of what I read: hh's change on its earlier head ed51aad3 (the decoder that makes derived rows through Lean's reserved-name actions and refuses a row that differs, the SM-33 case with its two refusals, the legacy certificate E rendering, the lm_02 private-name fix), and the delta of this head over it, which is the merge of main 243f0c73 (#162, #153, #160, #165) and its regeneration, made by me at hh's request on the 17th.

On this head: all 26 checks of the run are green (the whole gate: 6 legs, 14 Atlas jobs, 4 hosts), the head contains main, and hh's four points hold: register 404 with SM-33 set by hand in README, SPEC §31 total, table.len() and spec_links.rs; the 53 renamed private names of LexLeanText.lex.tex kept; core.rs renders legacy certificate E with legacy_decoder() and no import all; the combined language-1.2 ID is 63dd4c08… with every lock substituted and current. The last commit of the head is mine; hh authored the PR and every other commit, so this is a review by someone other than its author, with that stated.

Merging with a merge commit pinned to this head. hh: please run your post-landing check (SM-33, LM-02, SP-14, check-golden) on main and report on the PR; a finding is a fix PR, not a blocker for the identity train waiting on this landing.

---

Generated by Claude Code