[v0.4] #27 stage 5: certificates A, B, E and the audit modules as typed data, with no Lean text template in the production compiler

Child of #27; plan in this comment (its stage 2; numbered 3 here because #79 was stage 2 of the delivery, #78 stage 1). Stage 2 of the delivery, the libraries (#79, #80, #86), is merged: neither proof library is handwritten Lean any more.

Scope

The Lean the production compiler writes for each certified root is still produced from text templates in Rust. After this issue no template of Lean source remains in the production compiler: the certificates and audit modules are built as typed data and rendered to Lean by the one Lean backend (R8), like every other generated module.

Surveyed on main (39acab42):

crates/lexlean/src/production/certificate.rs (8,796 lines): certificate A and E, about 570 format! templates and 114 library lemma names (lib("…"));
production/rust_cert.rs (2,348) and rust_term.rs (375): certificate B and the Rust-term renderer;
production/preserve.rs (1,725): the staged audit module and the forbidden-token scan;
backend/lean.rs: the probe and axiom-audit module texts.

A generated certificate is large (examples/reasoning/expected/verify/preserve: certificate A of one root 143 KB, certificate B 188 KB), and states the program as a literal of the target calculus followed by instances of the library's lemmas.

Why this is not a rewrite of the strings

A kernel term has every argument explicit; the templates rely on Lean's elaborator for implicit arguments, universe levels and unification. Producing typed data therefore needs one of:

Explicit-argument forms in the library: for each lemma a certificate applies, a wrapper whose arguments are the program data (no implicit argument, no tactic), so a certificate is an application tree built from signatures the native library data already records (the registry lists every declaration and its type). The wrappers are added to the native libraries by the same one-time round trip as the migrations (regenerate Lean from the native source, state the wrapper, re-export, record the migration), so they are not handwritten Lean in the release tree.
A generic soundness theorem per certificate kind quantified over the program, with its side conditions decided by Decidable instances, so a certificate is theorem c : Sound P := soundness P (by decide) expressed as data (the GNAF certification library of §17.18 is built this way: its theorems are instantiated at each fixture).
A typed term builder with its own elaboration of implicit arguments (rejected: it re-implements the elaborator inside the trusted base).

Recommendation: 2 where a certificate kind has a decidable side condition (certificates A, E, the audit module), 1 for certificate B's per-function correspondence terms.

Work

A closed typed representation of the certificate modules (language 1.2 core-module data, lexlean/core-module/2), built by production::certificate and rendered by the Lean backend.
The library wrappers or generic theorems of 1/2 above, registered per R3.
preserve::stage and the audit read the data, not text; FORBIDDEN_TOKENS is checked on the rendered Lean as today.
Certificates A, B, E are produced for every committed root and every production corpus; leanchecker replay and the exact axiom audit unchanged.
The compiler-semantics ID, every package, golden, fixture expectation and verified record are regenerated; SPEC §22, §17.17, §31 and VERIFICATION.md follow.

DoD

No Lean source text template (a string literal that is Lean syntax) remains in production/ or backend/lean.rs; a gate (in the manner of VR-19) scans for it and is shown to fail on a planted template.
Every certified root's certificates A, B and E elaborate, replay in leanchecker, and pass the exact axiom audit; their statements (the theorem types) are byte-identical to today's, so no certificate's meaning changes.
The generated Lean is deterministic and source-mapped; two roots equal the previous output's statements.

Acceptance criteria

Planted defects each turn a named gate red: a wrong lemma application, a changed statement, a forged program literal, an added axiom, a reintroduced text template.
Languages 1.0 and 1.1 byte-identical; language 1.2 identities regenerated and recorded.
Full just vv.

Decision wanted from the maintainers

The route above (1 or 2 per certificate kind), because it fixes what the libraries must gain. I will start with certificate A and the audit module (route 2) and post the measured size of the result before certificate B.

Claiming this for implementation (Hermes agent): stage 3 of #27 — certificates A, B, E and the audit modules as typed data, no Lean text template left in the production compiler.

Plan of record, following the route in the issue: start with certificate A and the audit module under route 2 (a generic soundness theorem per certificate kind, side conditions decided by Decidable), post the measured size of the result, then certificate B under route 1 (explicit-argument library forms). Register per R3: the VR-19-style template scan (row, §31, scenario, failing test, implementation), then the typed representation, then regeneration of every language-1.2 identity, package, golden, fixture expectation and verified record.

Branch: claude/issue-89-certificates-as-typed-data off main. I will post the measured size of certificate A before starting certificate B, as the issue asks.

Stage 3 reconnaissance, measured on main d284b1652 (branch claude/issue-89-certificates-as-typed-data).

Route I am taking, as the issue proposes: route 2 (a generic soundness theorem per certificate kind, side conditions by Decidable) for certificate A, certificate E and the audit module; route 1 (explicit-argument library forms) for certificate B's per-function correspondence terms. Route 2's ingredients are already in the migrated library — per-construct soundness theorems LexLeanPreservation.Rust.{armPat,build,const,foldB,foldN,foldStep}_sound and Decidable instances such as instDecidableEqIntKind_lexLeanPreservation. Whether a single program-quantified soundness theorem already exists is the first thing the first slice settles (RustSound holds only 29 declarations, so it is readable in full).

Measured:


`crates/lexlean/src/production/`	23,522 lines (`certificate.rs` 8,796)
`format!` sites under `production/`	897 — the issue's "about 570" has grown
distinct `lib("…")` lemma names	114 (`FunRel`, `ListEnc`, `LookOps`, `Obs`, `OptEnc`, `Rel`, …)
certificate modules, one root set (`examples/reasoning/expected/verify/preserve/`)	`R2/RustStd.lean` 283,057 B · `R3/RustStd.lean` 229,776 B · `R5/RustCore.lean` 175,647 B · `R7.lean` 60,880 B · `Compose/*` 5–8 KB · `audit.txt` 735,864 B
the library	13 core modules `language/preservation-1.2/library/src/.lex.tex`, schema `lexlean/core-module/2`, 9,247 declarations*, 52.9 MB of source
the round trip	`tests/preservation-library/oracle/export.lean` + script under pinned Lean 4.32.1; record `tests/preservation-library/MIGRATION.md` (the library was 13 handwritten Lean files, 525,026 bytes, at `ba52c601`)

The gate: VR-19 is not a template scan — it states that the native Atlas source graph is self-contained (suite verification, case crates/conformance/src/cases/verification.rs:1139). So "a gate in the manner of VR-19" means a new sibling row in suite verification, registered per R3 with its own scenario and conformance_<id>, whose plant is a Lean-syntax string literal left in production/ or backend/lean.rs.

First slice, in order: (1) settle the program-quantified soundness question by reading RustSound and one committed certificate; (2) register the template-scan gate per R3 and make it fail on a planted template; (3) certificate A as typed data, constructed as a core module and rendered by the one Lean backend, with its emitted statements byte-identical; (4) the audit module on the same representation; (5) regenerate the 1.2 identities, packages, goldens and records, with languages 1.0/1.1 byte-identical; then post the measured size of the result before starting certificate B.

Route 2 validated — with one measured caveat (read out of the native library on main d284b1652).

1. The program-quantified soundness theorem exists. RustSound holds 29 declarations in full — sound, simulate, funSem_of, fl_of, fnFallible.eq_1, isTemp.eq_*, plainItem.eq_*, item_ne, kind_ne, and the private match helpers. LexLeanPreservation.Rust.sound is a theorem of exact policy (axioms Classical.choice, Quot.sound, propext) with the Π-spine

(p : LexLeanTarget.TargetSyntax.Program)   [implicit]   -- the program
(c : LexLeanPreservation.Rust.RCrate)      [implicit]   -- the crate
(A : LexLeanPreservation.Rust.Flags)       [implicit]   -- flags
(hcrate : CrateOK c)                       [instance]   -- the side condition
(n : Nat) (Γ : Rust.Ctx) (fl : Bool) (j : Rust.Jd) (a : …)  -- the judgement
→ …

simulate and funSem_of have the same shape (their types are 12,140 and 563 bytes of kernel data). So the certificate side already has one theorem quantified over the program, which is what route 2 needs.

2. Its side condition is not decidable today. LexLeanPreservation.Rust.CrateOK is a definition (kind: definition, fun p => …, transparency semireducible, axioms Quot.sound, propext), defined in RustCorr, and no declaration in the library mentions it besides itself. The library's only Decidable instance is instDecidableEqIntKind_lexLeanPreservation. So route 2 for certificate A needs a decision procedure for CrateOK (and whatever its body requires) added to the native library by the one-time round trip — an addition to the library, not just a re-rendering of the certificate. That addition is the measured cost the route decision hinges on, and I will post its size before certificate B, as the issue asks.

3. What a committed certificate actually holds (examples/reasoning/expected/verify/preserve/…/R2/RustStd.lean, 283,057 B):

import LexLeanPreservation.RustSound
namespace LexLeanPreserve.C21e79bf….R2.RustStd
def program : TargetSyntax.Program := { adts := [{ constructors := [[.nat, .nat, .nat …
def krate   : RustSyntax.Crate := …
def flags   : Flags := [(([(.adt 2)], (.option (.adt 2))), true)]
theorem fun0 : FunOK program krate flags 0 := …
theorem fun1 : FunOK program krate flags 1 := …      (one per function)

It cites Rust.sound zero times — the soundness application is not in the certificate module; the certificate states the program, the crate, the flags and a FunOK obligation per function, plus a CrateOK assembly. So certificate A's statements are already data-shaped; what the 897 template sites actually produce is the proof bodies. Route 1/2 must reproduce those as kernel terms (every implicit argument explicit) while the statements stay byte-identical — which is what makes "no certificate's meaning changes" the acceptance test rather than a slogan.

Correction to my reconnaissance above, and the vehicle finding.

Correction — I mislabelled the artifacts. examples/reasoning/expected/verify/preserve/LexLeanPreserve/C21e79bf….R2/RustStd.lean is certificate B (module_for(a, "rust-std")), not certificate A. Certificate A of that root is the sibling R2.lean (189,200 bytes), which opens with twelve import LexLeanPreservation.* lines and def __prog : _root_.LexLeanTarget.TargetSyntax.Program :=. The def program / def krate / def flags definitions I described belong to certificate B and are emitted by production/rust_cert.rs::certificate_b (lines 2263-2267), using certificate::render_program and rust_term::crate_term. The measurements (sizes, 897 format! sites, 114 lib("…") names, the Rust.sound Π-spine, CrateOK being a definition with no Decidable instance) stand.

The vehicle, checked by execution:

A certificate module is not core-module data. The one constructor, CoreModule::parse / from_source (crates/lexlean/src/ir/core.rs:689,699), accepts exactly one \coredata{…} payload — what a native .lex.tex exporter writes. Fed certificate text it refuses: from_source(certificate) -> a native core source holds exactly one core payload.
backend/core.rs::lean_text renders a core module as module / public import … / namespace LexLeanCore.Runtime + a JSON decoder + encoded chunks — a different species of file from a certificate module.
The semantic/document backend renders the same typed value in a different textual form: compiler/expected/build/modules/LexLeanTarget/TargetFixtures.lean:439 is dense, fully-qualified and ascriptive, where the certificate writes a compact multi-line { adts := […], functions := […] } with opened short names. So neither existing backend reproduces the certificate's current text.
The typed builders that do exist: crates/conformance/src/lx.rs (module_tex :318, with inductive/structure/definition/theorem/mutual :265-299, emitting lexlean/semantic-module/2), the typed calculus term builder crates/lexlean/src/calculus/term.rs (program :320), and the render dispatcher backend/lean.rs::render_module :2083.

What this means for the route. The certificate's program/krate/flags values are already typed (calculus::Program, calculus::rust::ast::Crate); what is text is their rendering, the proof bodies, and the module layout. So the work is the library + representation change the issue names — route 1's explicit-argument wrappers and/or route 2's generic theorem with decidable side conditions, plus a typed representation of the certificate module itself — not a mechanical replacement of format! in production/certificate.rs.

One clarification of the DoD I will hold to as stated: it requires each certificate's statements (the theorem types) to be byte-identical to today's, with the files themselves regenerated — not whole-file byte-identity. That is what makes a typed path viable while the renderer's form changes.

Evidence is executable: a unit test was added at crates/lexlean/src/backend/core.rs asserting the certificate text is rejected as a core source and printing the head of lean_text(RustSound); it passes (cargo test -p lexlean --lib certificate_text_is_not_core_module_data).

Maintainer decision recorded: the route proposed above is accepted. Certificates A and E and the audit module use a generic soundness theorem per certificate kind, with its side conditions decided by Decidable instances; certificate B uses explicit-argument forms of the library lemmas.

Ordering change (see the #27 comment of 2026-10-14): the new theorems and wrappers this needs are new LexLean content in the proof library, and the maintainers want the repository to own its authoring surface for that. So this issue now depends on the authoring surface (the new stage 3 of #27) and starts after it; the library growth is authored in .lex.tex through it, not by a one-time Lean round trip. Delivery stage is now 5.

Generated by Claude Code

Vehicle verdict: the existing typed representation cannot state a certificate — with two independent reasons, both executed.

The experiment is committed as a test (312 lines, crates/lexlean/tests/typed_certificate_vehicle.rs, two tests, both passing). It states certificate B's two declarations in lexlean/semantic-module/2 — a definition of type TargetSyntax.Program and a theorem whose statement applies FunOK — decodes them, renders them with backend::semantic::render_lean, and compares against the committed certificate.

1. The typed module is rejected at linking.

code: LLT4001
reason: forward or unavailable module reference `TargetSyntax`

A certificate names TargetSyntax.Program, FunOK, CrateOK — constants no \useglossary package declares (the certificate relies on import LexLeanPreservation.RustSound plus open LexLeanTarget LexLeanPreservation.Rust). The semantic-module IR has no way to reference an external constant, so a certificate cannot be stated in it at all, before any question of rendering.

2. Even rendered, the statements are not byte-identical. The backend emits

@[expose] public def program : LexLeanTarget.TargetSyntax.Program :=
  ({ adts := ([] : List (LexLeanTarget.TargetSyntax.Adt)) } : LexLeanTarget.TargetSyntax.Program)

public theorem fun0 : FunOK (program) (krate) (flags) (0) := by
  rfl

where the certificate writes

def program : TargetSyntax.Program :=
theorem fun0 : FunOK program krate flags 0 :=

Structural differences, not cosmetics: an attribute and a visibility modifier the certificate does not have (@[expose] public vs bare def); a module-qualified name (LexLeanTarget.TargetSyntax.Program, or a leading-dot .TargetSyntax.Program with an empty prefix) where the certificate relies on open; every application argument parenthesised and ascribed (FunOK (program) (krate) (flags) (0)) where the certificate writes the bare form; a proof rendered as a tactic script (:= by rfl) where the certificate carries a proof term; and a prefixed import (public import LexLeanTarget.LexLeanPreservation.RustSound vs import LexLeanPreservation.RustSound).

What this means for the route, and the decision I need.

If "each certificate's statements are byte-identical to today's" means the text today, then a certificate needs its own typed representation and its own rendering mode: the semantic-module vehicle cannot produce this form, and re-pointing the certificate at it would change every statement in every certificate.
If it means the same statement up to elaboration, the linking refusal still has to be solved — the representation must gain external-constant references — before the question of rendering even arises.

Either way, this issue is not a replacement of format! inside production/certificate.rs: it is (a) a representation for certificate modules that can name the library, and (b) the library additions of route 1/2 (including a Decidable for CrateOK, which the earlier comment showed is missing). Which of the two readings you intend decides how much of (a) has to exist, and I would rather ask than guess: is the requirement on the emitted text, or on the statement up to elaboration?

Parking this work, per the ordering recorded on #27 (2026-10-14): #89 now depends on the authoring surface (#93) and starts after it, and the library additions are authored in .lex.tex through that surface rather than by a one-time Lean round trip. The reconnaissance and the vehicle verdict above stand as input for that stage — in particular that a certificate cannot be stated in the existing semantic-module representation (linking refuses the library references) and that the backend renders neither the certificate's bare def form nor its proof terms. Branch claude/issue-89-certificates-as-typed-data is kept as an archive (with the executable vehicle test); I am not proposing it for merge, and I will not implement against the superseded route.

Resuming #89 now that #93 is verified (its DoD comment of 2026-10-15). Plan of record, measured on main at c257a657, and what starts today.

What the certificates are, on `main`

kind	modules committed	what the module holds	Lean text written by
A (`R<i>.lean`)	57	`__prog` literal, encoders `__enc_k`, width predicates `__fits_k`, one `theorem __rel_k : FunRel __prog k […] (Rel …)` per closure member with a proof term built from 114 library lemmas, then `root` and `denote`	`production/certificate.rs`, 568 `format!` sites
B (`R<i>/Rust*.lean`)	76	`program`, `krate`, `flags` literals; `theorem fun<n> : FunOK …` from a typed derivation tree of 20 rules; `theorem crate_ok : CrateOK … := by intro …; match …` (the one tactic proof)	`rust_cert.rs` 41, `rust_term.rs` 71
E (`R<i>/Compose/Rust*.lean`)	76	`theorem __wt_k : ∀ v, WT program krate flags (enc v) (.adt k)` per encoded type, `theorem root : ∃ ro, RealizesFn … ∧ RCI …` by `Rust.compose`; 8 lemma names in all	`certificate.rs` (`compose`, from line 7733)
audit module	1 per project	`import …`, `#print axioms …` per library declaration and certificate root, the vocabulary `#check`s	`preserve.rs::audit_text`

(The 897 format! sites of my earlier count include diagnostics and the lowering; the Lean text ones are the 680 above.) The 76 is 7 + 6 + 36 + 27 roots over examples/{production,production-coverage,models,reasoning} with their targets; lexlean verify writes them into expected/verify/preserve/ and preservation.json.

The representation

A certificate becomes a native core module (lexlean/core-module/2, SPEC §17.10, §17.21.8): kernel terms as a shared DAG with every argument and universe level explicit, built by production::certificate as a CoreModule value, rendered to Lean by the one core backend (backend::core::lean_text, the same decoder the libraries use), and written into the verify records in the authoring notation (sdk::to_notation), so a committed certificate is .lex.tex a person can read, not Lean. The same species as the libraries, which is what #79 made them; the _root_.-qualification pass (from_the_root), the qualify pass of E and the FORBIDDEN_TOKENS scan have nothing to scan in kernel data (the schema has no axiom kind, and every row carries the exact{axioms} policy the decoder enforces), so the scan stays on the rendered Lean and the policy row is the guard, as for the libraries.

This answers the two vehicle findings of 2026-10-14: a core module names any constant of its imports (Reasoning.Clinic.feverish, LexLeanPreservation.Rust.compose), so linking does not refuse it (the semantic-module IR cannot name them, and is not the vehicle); and no rendering form has to be imitated.

The two routes, as accepted, and what each actually costs here

A kernel term has every implicit argument written. The generator can write them when the argument is determined by the lemma's recorded Π-type (language/preservation-1.2/library, every declaration's type is kernel data) and the arguments it already has: that is substitution into a Π-type, not elaboration. Where the elaborator today unifies (an rfl, a _), the explicit term is Eq.refl at the type read off the instantiated signature. Where an implicit is not determined by the explicit arguments and the expected type, the lemma gets an explicit-argument form in the library (route 1), authored in the notation through #93's surface in language/preservation-1.2/library/src/*.lex.tex and kernel-checked with the library (as LexLeanCertification.authored_eq_symm was in #104). Route 2 (a generic theorem with a Decidable side condition) is for the one tactic proof, crate_ok: a library theorem crateOK_of_funs : (∀ i, FunOK p k A i) → CrateOK p k A or a Decidable (CrateOK p k A) instance, whichever is smaller when measured. I will post the count of lemmas that need a route-1 form before the stage that uses them, since that count is the library growth the maintainers asked to see.

The statement clause of the DoD, as I will hold it

"Statements byte-identical to today's" cannot mean the module text: a core module renders as a decoder and data, and §17.17 states the certificate as a Lean statement, not a text. I hold it as: the type of every theorem of the typed certificate, after the decoder installs it, is the kernel term the current text elaborates to, declaration by declaration, for every committed root (57 A, 76 B, 76 E). Evidence: an oracle under tests/ (outside the release tree, as tests/preservation-library/oracle/ is) elaborates the current certificates and compares. If the maintainers meant the text, say so here and I stop before stage 1.

Stages, smallest first, each a PR green on full `just vv`, each registered per R3 before its implementation

stage	what	library growth	plants
1 (starting now)	the vehicle: a kernel-term builder in `production/` (nodes, constants with levels, binders, literals, instantiation of a recorded Π-type), `Certificate` carrying a `CoreModule`, `preserve::stage` rendering through the core backend, the record in notation; certificate E on it (76 modules, 8 lemmas: `compose`, `rel_ne_stuck`, `wt_adt`, `wtl_cons`/`wtl_nil`, the `wt_*` encoders, `RealizesFn`, `RCI`); the statement oracle	none expected; measured	a wrong lemma application, a changed statement, a forged program literal, an added axiom
2	certificate B: the 20 derivation rules as explicit applications, `program`/`krate`/`flags` as kernel literals, `crate_ok` by route 2	the route-1 forms the 20 rules need, plus `crate_ok`'s theorem	the same four, on B
3	certificate A: the 114 lemma applications of the 568 sites, encoders and `fits` as kernel definitions, `denote`	the route-1 forms A needs (measured in stage 1's builder before starting)	the same four, on A
4	the audit module as typed commands on #90's `AuxiliaryModule` (the probe and axiom-audit texts of `backend/lean.rs` are already typed on that branch, so this issue leaves `backend/lean.rs` to #90 and takes `preserve.rs::audit_text` after #90 lands); the gate: a `verification`-suite row that no Lean-syntax string literal remains in `production/`, failing on a planted template; SPEC §17.17/§22 wording, §31, CHANGELOG, VERIFICATION, the regenerated language-1.2 identities and records	none	the reintroduced template

Languages 1.0 and 1.1 have no certificates, so their bytes do not move. Stage 1's branch is claude/issue-89-typed-certificates off c257a657; the archived claude/issue-89-certificates-as-typed-data stays as it is.

Stage 1 is up as #146: the vehicle, and certificate E on it, for all 76 certificates E of the four corpora. Measured on the branch at its head, Lean 4.32.1, Linux x86-64.

What the stage delivers


representation	certificate E is a native core module (`lexlean/core-module/2`), built by `production/certificate/data.rs` over a kernel-term builder (`production/kernel.rs`: a hash-consed DAG, lifting and instantiation, `apply_pi`, which applies a library lemma by instantiating its recorded Π-type one binder at a time; an `rfl` is `Eq.refl` at the stated equation)
recursive groups	`T.rec` and `T.rec_j` terms, the motives in the order the kernel nests the containers (the block's constructors first, then what the auxiliaries nest), an induction hypothesis where the text recursed; the five groups of `production-coverage` (`Grove`, nested through `List`, `Option`, `List (Nat × ·)`, `Except`, `Nat × ·`; `Tree`; `Rose Nat`; the mutual `Expr`/`Stmt`; `Term`) pass the kernel
rendering	the one core backend; `lean_text_legacy` writes `import` lines, no `module` header, and the decoder under the module's own namespace, because a `module` cannot import the legacy A and B texts (Lean refuses: `cannot import non-module … from module`) and two legacy-rendered core modules imported together would declare the decoder twice (found by the audit module)
record	the authoring notation, `…/Compose/RustStd.lex.tex`, 1,424,062 bytes for the 76 (18.7 KB each on average), reading back to the data byte for byte; `preservation.json` binds those bytes
audit	row by row (`audit_core`): imports within the environment, only safe theorems/definitions/abbreviations, every policy exact, no forbidden constant in any spelling; every row pins its axioms from the library registry (for example `__wt_k` rows pin `[propext]`, `root` the three), and the audit module prints and checks every row
statements	131 theorem rows of the 76 certificates: each definitionally the statement the committed text elaborated to (`isDefEq`), `tests/preservation-certificates/E-STATEMENTS.md`
register	`SP-14`, with five plants refused: a wrong lemma, a changed statement, a forged crate reference (by the kernel), an added axiom (by the data audit, before Lean), 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 E (`compose`, `wt_theorems`, `wtf`, `wt_apply`, `wtl`, `wt_auxiliary`, `qualify`, 472 lines) is deleted
verification	`lexlean verify` of the four corpora end to end (A and B as text, E as data), every example's records regenerated, `check-fixtures` 269 equal, `check-golden`, `check-calculus`, `check-production-export` green; full `just vv` in the PR's CI

What the measurement says for stages 2 and 3

Route 1 (explicit-argument forms) was not needed for E. Every implicit of the 8 lemmas E applies is determined by arguments the generator holds (the program, crate and flags constants; element types and encoders; field values and types), so the library grew by zero declarations for this stage. The question for B and A is the same per lemma: the 20 derivation rules of B and the 114 lemma names of A will be classified the same way before each stage starts, and only the ones whose implicits the arguments do not determine get a library form.
Two things Lean had been doing for the text that the data must do itself: the recursor of a nested inductive (now written), and the module system's privacy of the decoder (now scoped). Stage 2 inherits both solutions.
Cost: a rendered data certificate is larger than its text (the decoder prelude and the JSON), so max_total_source_bytes is reached earlier (certificates-total-limit now refuses at r14 instead of r25, same LLS8002); the elaboration time of the four corpora did not move noticeably (production 3m47s wall for its whole verify).
The DoD clause on statements is held as "the kernel statement up to elaboration", checked by the oracle above and recorded; if the maintainers meant the text, the record shows exactly what differs (the form of the proof terms and of the module, nothing in a statement).

Next: stage 2, certificate B (rust_cert.rs: program, krate, flags as kernel literals, the 20 rules as explicit applications, crate_ok by a library theorem or a Decidable instance, measured first), on the same vehicle.

#89 stage 2: per-phase timing of a rule application (to be removed)

#89 stage 2: node-walk counter (to be removed)

#89 stage 2: the kernel builder opens a lemma once (checkpoint)

#89 stage 2: scaling lens at 400 arms (checkpoint)

#89 stage 2: build/render timing (checkpoint)

#89 stage 2: the kernel builder remembers the loose-variable bound of…

#89 stage 2: scaling lens (checkpoint)

#89 stage 2: the placeholder-free shortcut belongs to resolve, not to…

#89 stage 2: remove the timing lenses

#89 stage 2: the crates the Rust machine evaluates are computable def…

#89 stage 2: keep the machine module on failure (to be removed)

#89 stage 2: remove the machine-module diagnostic

feat(preservation): no Lean source text template remains in the produ…

train: regenerate every record the combined tree moves

train: no ignored test remains; SM-32 precedes SM-33; one README row …

Navigation Menu

Repository navigation

[v0.4] #27 stage 5: certificates A, B, E and the audit modules as typed data, with no Lean text template in the production compiler #89

Scope

Why this is not a rewrite of the strings

Work

DoD

Acceptance criteria

Decision wanted from the maintainers

What the certificates are, on `main`

The representation

The two routes, as accepted, and what each actually costs here

The statement clause of the DoD, as I will hold it

Stages, smallest first, each a PR green on full `just vv`, each registered per R3 before its implementation

What the stage delivers

What the measurement says for stages 2 and 3

49 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

[v0.4] #27 stage 5: certificates A, B, E and the audit modules as typed data, with no Lean text template in the production compiler #89

Description

Scope

Why this is not a rewrite of the strings

Work

DoD

Acceptance criteria

Decision wanted from the maintainers

Activity

humuhumu33 commented on Oct 14, 2026

humuhumu33 commented on Oct 14, 2026

humuhumu33 commented on Oct 14, 2026

humuhumu33 commented on Oct 14, 2026

afflom commented on Oct 14, 2026

humuhumu33 commented on Oct 14, 2026

humuhumu33 commented on Oct 14, 2026

humuhumu33 commented on Oct 15, 2026

What the certificates are, on main

The representation

The two routes, as accepted, and what each actually costs here

The statement clause of the DoD, as I will hold it

Stages, smallest first, each a PR green on full just vv, each registered per R3 before its implementation

humuhumu33 commented on Oct 15, 2026

What the stage delivers

What the measurement says for stages 2 and 3

49 remaining items

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

What the certificates are, on `main`

Stages, smallest first, each a PR green on full `just vv`, each registered per R3 before its implementation