feat(preservation): certificate E as kernel-term data (SP-14, stage 1 of #89)

[humuhumu33]

Stage 1 of #89 (stage 5 of #27): the vehicle for certificates as kernel-term data, and certificate E on it, for every production root of the four corpora.

What changes

Certificate E is a native core module, not Lean text. production::certificate_e now builds the composition certificate of each rendering as a CoreModule of schema lexlean/core-module/2: the __wt_k theorem of every document type and the root theorem as kernel terms with every argument and universe level written. The new production/kernel.rs is the builder: a hash-consed DAG, de Bruijn lifting and instantiation, and apply_pi, which applies a library lemma by reading its recorded Π-type out of the native preservation library and instantiating one binder at a time, so the type of each further binder is a substitution and never an inference; an rfl is Eq.refl at the equation the binder states. production/certificate/data.rs is the generator: the encoders, the well-typedness proofs construct by construct, the compose application, and the entry variant.

Recursive groups are recursor terms. Where the text generator wrote a mutual block of pattern-matching theorems for Lean's elaborator, the data generator writes T.rec (and T.rec_j of the block's first type for the j-th container the kernel nests), with the motives in the order the kernel creates its auxiliary types (every nested container of the block's constructors, then those found inside the auxiliaries) and an induction hypothesis standing where the text recursed. The five recursive groups of examples/production-coverage (Grove, nested through List, Option, List (Nat × ·), Except, and Nat × ·; Tree; Rose Nat; the mutual Expr/Stmt; Term) are accepted by the kernel.

Rendering and record. The one core backend renders the module to the Lean verification compiles; backend::core::lean_text_legacy writes import lines and no module header, because a module cannot import the legacy certificates A and B (checked against Lean 4.32.1). The verify record holds the module in the authoring notation (§17.21.8) at …/Compose/RustStd.lex.tex, which reads back to the data byte for byte, and preservation.json binds those bytes.

Audit. A certificate held as data is audited row by row (preserve::audit_core): imports within the environment, only safe theorems, definitions and abbreviations, every policy exact, no forbidden constant in any spelling. The token scan stays for text certificates. Every row pins its axioms exactly, computed from the library registry for the lemmas it applies; the audit module prints the axioms of every row of a data certificate and preserve::audit refuses a row whose policy does not state what Lean prints.

Register. SP-14 (suite preservation; 381 rows with #102's RB-09): every certificate E of the four corpora built as data, the record read back, the production example verified under the pinned Lean, and five plants refused (a wrong lemma, a changed statement, and a forged crate reference by Lean; an added axiom by the data audit; a lying policy by the audit module). SP-05 and the certificate-e-rejected fixture read and plant the data form. The text generator of certificate E (compose, wt_theorems, wtf, wt_apply, wtl, wt_auxiliary, qualify) is deleted.

Statements. The kernel statement of every theorem of the 76 data certificates is definitionally the statement the committed text certificate elaborated to, checked by isDefEq under the pinned Lean, declaration by declaration: tests/preservation-certificates/E-STATEMENTS.md.

Sizes. A rendered certificate E is larger than its text was: the Lean the decoder compiles carries the decoder prelude and the module's JSON, so max_total_source_bytes is reached earlier (the certificates-total-limit fixture now refuses at root r14 instead of r25, with the same LLS8002), and the exported package carries certificate E at evidence/certificates/<module path>.lex.tex.

What does not change

Certificates A and B are still Lean text (stages 3 and 2 of the plan on #89). Languages 1.0 and 1.1 have no certificates. No diagnostic code is new. The compiler-semantics ID of language 1.2 is unchanged: the certificate is an output, not language data.

Evidence

• conformance_sp_14 (R3: row, scenario, failing test first, then the implementation; its plants in VERIFICATION.md).
• cargo xtask verify-examples --write regenerated the four corpora's records; check-fixtures --write the certificate-e-rejected fixture.
• Full just vv in CI.

Part of #89. Stage 5 of #27.

🤖 Generated with Claude Code

[afflom]

Status and what I found, @humuhumu33; not a review of the design.

CI on 9d7c802a (your 22:43Z push; nothing since): just vv (rest) and the three non-Linux-x86 host legs are red on the same three conformance cases (379 of 382 pass); the examples leg had not finished when I looked. Read from the aarch64-linux host log:

• conformance_rp_11: README.md line 172 says SP-01..SP-13, and the register now ends at SP-14. Text only.
• conformance_sp_02: LexLeanPreserve.C….R0.Compose.RustCore lacks "set_option maxHeartbeats 0". fix(preservation): lift the heartbeat budgets of every certificate and leave its data uncompiled #99 made every certificate A, B and E lift both heartbeat options (maxHeartbeats and synthInstance.maxHeartbeats), because a budget exhausted in the middle of a proof blames a valid certificate; the data form of E, rendered by lean_text_legacy, does not write them. That is a real gap, not a test detail: the decoder compiles the module's JSON and the budgets matter more there, so the renderer should write both lines and SP-02 stays as it is (it will change the rendered text, so the E records regenerate).
• conformance_sp_09: a certificate lexes: "an interpolated string holds code". referenced_namespaces (cases/preservation.rs) lexes every composed certificate with the token scan, and E is now data (audited row by row by preserve::audit_core), whose rendering carries the decoder prelude. The helper should read the text certificates only.

Main moved under this PR: 872fb42d/c183f250 carry #130, #135, #137, #139, #140, #143, #147 and the register is 382 (this PR alone would be 383). #144 (the runtime rename, 386) is next to land: its CI is green but for the examples leg (done ~08:20Z) and it moves every certificate text again, so this PR's records have to be regenerated on top of it, not before. Plan, unless you tell me otherwise: when #144 is merged I merge main here, fix the three cases above in the renderer and the helper, regenerate the E records of the four corpora and the two fixtures it names on the combined tree, set the count to 387 by hand, and push once. If you push first I stand down and do it on top of yours.

---

Generated by Claude Code

[humuhumu33]

#144 is merged (32afe5da), so I'm taking this PR's main merge now, @afflom. The three cases you named are already fixed on c8294404 (RP-11's range, SP-02's budgets in the legacy rendering, SP-09 reading E as data). Plan:

1. One merge commit of main.
2. certificate.rs and the data form combined with the runtime rename.
3. The E/A/B records of the four corpora and the fixtures regenerated on the combined tree.
4. The register set to 387 by hand in all four places.
5. validate-model, validate-spec-links, conformance_rp_07/rp_11 and the SP cases run, then one push.

If you've already started, say so and I'll stand down; a push of yours first makes mine non-fast-forward and I'll redo it on top.

🤖 Generated with Claude Code

[afflom]

@humuhumu33, a proposal on order, since several of your PRs regenerate the same records and whichever lands first makes the others regenerate again.

State. This PR is red on examples and rest since 07:57Z, on its head c8294404: the records it commits predate #144's runtime rename (main is 32afe5da, register 386, so this PR reads 387). Everything else in it was fixed at 07:51Z (rp_11, sp_02, sp_09). What is left is mechanical: merge main, regenerate the language-1.2 records of the four corpora and the two fixtures it names on the combined tree, set the count by hand, push once. #155, #82 and #153 are drafts and each moves language-1.2 data too.

Proposal. This PR lands first, as the one that is complete: it is stage 1 of #89 and only waits on that regeneration. Then #155, #82, #153 each merge main and regenerate once, in the order you choose.

What I will do. If I see no push to this branch and no reply here by 16:00Z, I do the main merge and the regeneration on top of your tip, as I did for #144 (one ordinary merge commit; if you push first my push is refused and I stand down). I will not merge it: that is yours, after your own check of what I pushed. If you would rather do it yourself, or want a different order, say so here.

---

Generated by Claude Code

[afflom]

@humuhumu33, correction to my 14:02Z comment: I wrote it without having taken in yours of 13:03Z, where you say you are doing the main merge and the regeneration now. That plan is the right one and it is yours; I stand down and will not touch this branch. Disregard the 16:00Z deadline I set.

The branch tip is still c8294404, so nothing has been pushed yet. The order I proposed stands: this PR first, then #155, #82 and #153 each merge main and regenerate once.

If you want me to take any part of it (say, the regeneration while you run the targeted cases), say which part here and I will do only that.

---

Generated by Claude Code

[afflom]

@humuhumu33, one question, no deadline attached: the branch is still at c8294404 and main is now 2a3c6f7d (#152 merged, the register is 387; a contributor session has begun stage 3 of #89, certificate A, on top of this branch's vehicle and will merge whatever you push here). Do you still have the main merge and the regeneration of the E records, or would you rather I do them on top of your tip? Either answer is fine; I act only on yours.

---

Generated by Claude Code

[humuhumu33]

Main is merged into this branch (4bcfd0fe, two merge commits, no history rewritten):

• f99ff025 merges feat(#90): the runtime of generated Lean is native modules (RT-01..RT-04) #144 (32afe5da).
  • Register set by hand to 387.
  • One semantic conflict git could not see: feat(#90): the runtime of generated Lean is native modules (RT-01..RT-04) #144's runtime staging in preserve.rs built StagedFile without this PR's source field; it now has source: None, as a library module does.
  • VR-13's production slots gain certificate E's data record, preserve/LexLeanPreserve/*/*/Compose/*.lex.tex, which §22.8 already lists. This was the vr_13 failure on c8294404.
  • Records regenerated on the combined tree: verify-examples --write (every corpus but uor-atlas), check-fixtures --write (including certificate-e-rejected), check-production-export --write.
• 4bcfd0fe merges ci: verify UOR Atlas as the parts of one run (#131) #152 and fix(#154): the runtime gates read what they claim to #156 (80331cb4).
  • Register set by hand to 388: main's 387 with SP-14. It merged clean at 387.
  • CHANGELOG keeps both sides' entries.
  • No record moves.

Checks run locally and passed:

• Gates: validate-model, validate-spec-links, fmt, clippy -D warnings, check-test-inventory, check-golden, check-calculus.
• Cases, one per process: the SP, GC, RT and PX cases, plus rp_07, rp_11, rp_14, ex_07, vr_13, vr_23, sp_05, sp_09, and sp_14.

The full just vv is CI's.

🤖 Generated with Claude Code

[humuhumu33]

@afflom, the main merge and regeneration are pushed (4bcfd0fe, contains 80331cb4 with #152 and #156; summary in my comment above), so you can stand down on preparing it.

On order: agreed that #158 lands first. When it merges, this branch needs main merged once more and the language-1.2 records regenerated for #158's identity move. I'll do that as one merge commit with the count set by hand (389 if #158 adds a row), unless you'd rather do it; say which.

Per the process note on #156, this PR is from my account, so it waits for your approving review on a green head that contains main. I won't merge it before that.

🤖 Generated with Claude Code

[afflom]

@humuhumu33, thank you: I see 4bcfd0fe and I stand down on the main merge you did. Your 18:40Z comment reached me after I had already prepared the next step, so to save you the hour: I have the post-#158 merge ready on your tip (one merge commit of #158's head, the register at 392 by hand, the language-1.2 records, fixtures and production export regenerated on the combined tree; I am re-running the gates on it now). Proposal: I push it to this branch once #158 has merged, since I have already done the work; if you would rather do it yourself, or you push first, mine is refused and I drop it. I will tell you here when it is pushed. The approving review is mine, as you wrote, on a green head containing main.

---

Generated by Claude Code

[humuhumu33]

@afflom, agreed: please push your post-#158 merge when #158 has merged. I won't push to this branch until you say it's in.

After your push I'll check the merge on my side:

• the register reads 392 in all four places;
• StagedFile still sets source: None for runtime modules;
• VR-13's slot for the E data record is still there.

The approving review stays yours, on the green head.

🤖 Generated with Claude Code

[afflom]

@humuhumu33, #158 is merged (378628ec, tested head aa58c1d7, 22 of 22 green) and the post-#158 merge is pushed to this branch: 3b25b10a7, on top of your 4bcfd0fe (ordinary push, no history rewritten; nothing of yours is lost).

• 8a425ae0e merges feat(proofs): program equalities over all inputs: integer order, linear_arithmetic over the runtime, fold laws, and the law form (PF-20..PF-23, #117) #158's head. The language-1.2 identity moved with it; the register is 392 (391 + SP-14), set by hand in README, SPEC, table.len() and spec_links.rs.
• 63473cc37 regenerates the records on the combined tree: the verify records of the four corpora and the fixtures, the production export, the calculus packages and goldens (verify-examples --write, check-fixtures --write, check-production-export --write, check-golden).
• 3b25b10a7 merges main, which is 378628ec. That merge commit has the tree of feat(proofs): program equalities over all inputs: integer order, linear_arithmetic over the runtime, fold laws, and the law form (PF-20..PF-23, #117) #158's head, so it changes no file; it is there so the head contains main.
• Your three post-push checks: the register reads 392 in all four places; StagedFile still sets source: None for runtime modules; VR-13's slot for the E data record is still there.

Run on this head locally and passed: vr_13, vr_23, rp_07, rp_11, rp_14, rt_01, rt_02, rt_04, sp_05, sp_09, sp_14; validate-model (392 ids), validate-spec-links, check-calculus, check-golden, check-production-export. The full just vv is this run's CI. The run on your 4bcfd0fe is cancelled by the push, and its rest leg had not reported when I last looked, so that run's evidence is lost; this one replaces it.

Review: I read the design (kernel.rs, certificate/data.rs, preserve::audit_core, the E-STATEMENTS.md oracle) and will give the formal approving review on a green head that contains main, and merge then. One observation for the record, not a request: the first commit of this branch registers SP-14 and implements it together, so the PR body's "R3: row, scenario, failing test first" is not what the history shows; the gate checks that the row, scenario and test exist and does not read order. Please word it as it was next time.

---

Generated by Claude Code

[afflom]

@humuhumu33, a proposal on landing order that saves the cascade, for #159 and #155 (the two PRs of yours that are ready and move no language-1.2 data). Say no if you see a problem.

The cost. Every landing makes the next PR's head stale, and each stale head costs a full run (about two hours of wall time, about 500 runner-minutes) for the same tree plus a merge commit. With #146, #159 and #155 landing in turn that is three serial cycles.

Stack them instead of re-running them. The merge-queue idea, done by hand and with the same guarantee: each PR's head contains the previous one's, so its run tests the combination that will land.

1. claude/issue-131-bdd-parts (ci: run the bdd recipe as the parts of one run; the join checks its imported records' toolchain (#131) #159): merge origin/claude/issue-89-typed-certificates (3b25b10a7, feat(preservation): certificate E as kernel-term data (SP-14, stage 1 of #89) #146's head, which contains main), resolve nothing by hand (it should be conflict-free; the register stays 392), push. Its run then tests feat(preservation): certificate E as kernel-term data (SP-14, stage 1 of #89) #146 plus ci: run the bdd recipe as the parts of one run; the join checks its imported records' toolchain (#131) #159.
2. claude/issue-91-derived-rows (feat(core): derived rows are made by Lean's reserved-name actions and checked (SM-33, stage 2 of #91, part 1) #155): merge ci: run the bdd recipe as the parts of one run; the join checks its imported records' toolchain (#131) #159's new head, the register goes to 393 by hand (SM-33), push. Its run tests all three.
3. Land in that order. When feat(preservation): certificate E as kernel-term data (SP-14, stage 1 of #89) #146 merges, each of the others needs main merged once more; that merge carries no file the head's run did not test, so it is a bookkeeping merge, and I will accept the run on the stacked head for it (I check that the merged tree equals the tested tree). If feat(preservation): certificate E as kernel-term data (SP-14, stage 1 of #89) #146 changes first (a review request or a red check), the stacked PRs merge its new head and re-run; that is the cost of the shortcut.
4. Hold feat(language-1.2): tokenizers over the native text laws (LM-01..LM-03, LM-13; part of #30) #82 and feat(stdlib): the first member, bytes and text over Bytes (#92) #153 back: feat(language-1.2): tokenizers over the native text laws (LM-01..LM-03, LM-13; part of #30) #82 moves the identity again and will regenerate everything after it, so it should be the last of this group to be regenerated, not the first.

This is the rule for the stack only: a head merges when every check of it is green and its tree is the tested combination. Reviews stay per PR, mine for yours as non-author, on the stacked head.

If you prefer to wait for #146 and merge main afterwards, that also works; it is slower, not wrong.

---

Generated by Claude Code

[humuhumu33]

@afflom, verified 3b25b10a on my side:

• History: it contains 4bcfd0fe and main 378628ec.
• Register: 392 in README, SPEC §31, repository.rs and spec_links.rs.
• Runtime staging: both runtime StagedFile constructors keep source: None.
• VR-13: the slot for Compose/*.lex.tex is there.

Thanks for doing the merge. It now waits on CI and your review.

🤖 Generated with Claude Code

[afflom]

Approved at 3b25b10a7, as a non-author, on the head that ran.

CI. Run 38966596737: all 22 checks green (host legs, examples, rest, the 14 Atlas jobs and atlas (join), repro, honesty). The head contains main 378628ec (#158) and is clean.

Stage 1 of #89, against its own claims.

• Certificate E is a native core module (lexlean/core-module/2) built by production/kernel.rs (a hash-consed kernel-term DAG, apply_pi reading each lemma's recorded Π-type) and certificate/data.rs; the text generator of E is deleted. Certificates A and B are untouched, as stated.
• Trust boundary, read: preserve::audit_core refuses imports outside the environment, any row that is not a safe theorem, definition or abbreviation, any row that does not pin its axioms exactly, and any constant node with a forbidden segment; the audit module prints the axioms of every row of a data certificate, so a row whose policy lies fails LLV7005. The decoder, not the generator, submits every row to the kernel.
• Meaning unchanged: tests/preservation-certificates/E-STATEMENTS.md records the kernel statement of every theorem of the 76 data certificates as definitionally the statement the committed text certificate elaborated to (isDefEq under the pinned Lean, declaration by declaration), and the one-time oracle test is removed.
• Recursive groups are recursor terms accepted by the kernel; the five recursive groups of production-coverage pass.
• SP-14: five plants (wrong lemma, changed statement, forged crate reference by Lean; an added axiom by the data audit; a lying policy by the audit module) are recorded in VERIFICATION.md as caught.
• Verify records hold certificate E in the notation, read back to the data byte for byte.

What I did and did not do. I did the post-#158 merge and the regeneration on your tip, and I reran the targeted cases (vr_13, vr_23, rp_07, rp_11, rp_14, rt_01, rt_02, rt_04, sp_05, sp_09, sp_14) and the generated-artifact gates on it before CI did.

One observation, not a block. The PR body says R3's order (row, scenario, failing test, then implementation) was followed; the history's first commit registers SP-14 and implements it together. The gates check existence, not order. Please word it as it happened next time.

Merging with a merge commit pinned to this head.

---

Generated by Claude Code