[v0.4] #27 stage 4: the backend's fixed Lean runtimes generated through native modules

Child of #27; plan in this comment (its stage 3). Delivery order: stage 1 #78, stage 2 #79 (merged), stage 3 #89, this is stage 4.

Scope

The Lean backend splices fixed runtime text into every generated module of a language-1.1 or 1.2 project: backend/semantic.rs (3,708 lines; the collections, models and reasoning runtimes at lines 1340–1806 and the portable primitives), backend/core.rs (1,752; the core-module decoder) and backend/lean.rs (2,600). That text is handwritten Lean carried as Rust string constants, normative for what every generated module means.

The constraint that shapes it

Languages 1.0 and 1.1 are public: their generated output must stay byte-identical (RP-10, #79's DoD). The runtime text a 1.1 module splices cannot be regenerated from an exported kernel environment byte for byte: an export prints canonical terms, not the handwritten layout. So the two languages need different treatment, and the treatment is the decision this issue needs.

Proposal (for the maintainers to confirm or change)

Language 1.2: the runtimes become native core modules of a compiler-embedded project, as the proof libraries did ([v0.4] #27 stage 2: preservation and certification proof libraries as native core modules #79): a one-time lossless export of the elaborated environment, committed as .lex.tex, with the exporter and the equivalence record outside the release tree; generated 1.2 modules import the generated runtime module instead of splicing text, and the language-1.2 compiler-semantics ID records its content address. This changes the generated Lean of every 1.2 project (declared in the issue, regenerated by writers).
Languages 1.0 and 1.1: their frozen text is a compatibility fixture of those language versions, not part of language 1.2's compiler. It stays as committed bytes under a named, audited location (a language/ data file the 1.0/1.1 backends read) with a permanent test that it equals the bytes of the released 1.1 output, and the permanent no-handwritten-Lean gate (VR-19, SP-12, GC-11) is extended to say that this one declared exception holds only released bytes of frozen versions.
Alternative if the maintainers want no exception: declare 1.1 closed to new projects and generate its runtime text from native modules whose rendering is made to reproduce the frozen bytes (a rendering mode, not an export); this is larger and I do not recommend it.

Work

Export, equivalence (declaration by declaration, types, values, reducibility, attributes), migration record under tests/, as for [v0.4] #27 stage 2: preservation and certification proof libraries as native core modules #79.
Embedded runtime project; 1.2 backend imports it; both backends and the portable-primitive restatements re-pointed.
The probe and audit module texts of backend/lean.rs as typed data (shares the representation of [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).
RP-10 for 1.0/1.1; 1.2 identities regenerated.
Per R3: register rows, scenarios, named tests, VERIFICATION.md plants.

DoD

No handwritten Lean runtime remains in the 1.2 compiler: a gate fails on a planted runtime text constant.
The frozen 1.0/1.1 bytes are the only declared exception and are tested against the released output.
Every registered runtime declaration with its exact axioms unchanged; generated 1.2 modules import only Init and the generated graph.
Elaboration, leanchecker replay and exact axiom audit pass for every example and corpus on the new runtime.

Acceptance criteria

Equivalence evidence recorded; planted defects (a changed runtime declaration, an added axiom, a stale generated runtime, a handwritten runtime text reintroduced) each turn a named gate red.
Languages 1.0 and 1.1 byte-identical; full just vv.

Decision wanted

How 1.0/1.1 are to be treated (a declared frozen-bytes exception, or closing the versions).

Maintainer decision recorded: accepted as proposed. Language 1.2 gets the fixed runtimes as native core modules (a one-time lossless export, the route of #79, with the exporter outside the release tree and a migration record); languages 1.0 and 1.1 keep their frozen released bytes as the one declared exception, held as data and tested against the released output, with the permanent no-handwritten-Lean gates stating exactly that exception.

Ordering: this is a one-time export of existing text, not new authored content, so it does not wait for the authoring surface and can run in parallel with it (delivery stage 4). Once the surface exists, the exported modules are printed into it, so the runtimes become editable source rather than opaque kernel data.

Generated by Claude Code

Claiming this (Hermes agent): stage 4 of #27 — the backend fixed Lean runtimes through native modules — per the maintainer decision recorded here on 2026-10-14.

Plan of record, as decided: language 1.2 gets the runtimes as native core modules of a compiler-embedded project through a one-time lossless export (the #79 route, exporter and equivalence record outside the release tree), and generated 1.2 modules import the generated runtime module instead of splicing text; languages 1.0 and 1.1 keep their frozen released bytes as the single declared, audited exception, with a permanent test that those bytes equal the released 1.1 output, and the no-handwritten-Lean gate (VR-19, SP-12, GC-11) extended to name that exception.

Register per R3 (row, SPEC §31, scenario, failing conformance_<id>, implementation, VERIFICATION.md plants): a gate that fails on a planted runtime text constant, the frozen-bytes test, and the per-declaration equivalence record under tests/. Branch claude/issue-90-native-runtimes off main. I am taking this stage while the authoring surface is in flight because it does not depend on #93.

Reconnaissance and plan for stage 4, measured on main d284b1652 (branch claude/issue-90-native-runtimes).

Proposal, in the manner of the stage 1 design: work proceeds unless objected to. Three corrections to this issue's own survey first, because they change the plan:

backend/lean.rs carries no runtime text constant. Its probe and audit module texts are built procedurally (backend/lean.rs:2447 probe, :2531 audit modules), so the "2,600 lines" in the scope above is not runtime text: it contributes 0 bytes to this stage's export.
The 1.2 core decoder was not listed. It is LEAN_CORE_DECODER_V2 in crates/lexlean/src/backend/core_v2.rs:34, 27,636 bytes, schema lexlean/core-module/2 — 1.2-only, and it must move with the other 1.2 runtimes.
The [v0.4] #27 stage 2: preservation and certification proof libraries as native core modules #79 oracle is not in the tree. tests/preservation-library/oracle/ existed only at checkpoint d54dbf8551190e4ae77fbf69267fd4328e19db3f and was removed by the commit that follows it; the record that survives is tests/preservation-library/MIGRATION.md. The exporter for this stage has to be recovered from that checkpoint (or re-authored), which is the single largest unknown below.

Measured runtime text (6 literals, 79,457 bytes):

file	constant	bytes	language
`backend/semantic.rs:1340`	`COLLECTIONS_RUNTIME`	8,016	1.2 only
`backend/semantic.rs:1492`	`MODELS_RUNTIME`	5,101	1.2 only
`backend/semantic.rs:1570`	`REASONING_RUNTIME`	12,532	1.2 only
`backend/semantic.rs:2045`	`portable_runtime`	13,339	1.0/1.1 frozen
`backend/core.rs:785`	`LEAN_CORE_DECODER`	12,833	1.0/1.1 frozen (`core-module/1`)
`backend/core_v2.rs:34`	`LEAN_CORE_DECODER_V2`	27,636	1.2 only

portable_runtime_1_2 (13,491 B) is a derived rendering of portable_runtime, spliced for semantic-module/1 only — language 1.0 has no semantic module (semantic_module_spec("1.0") = None). The splice sites are backend/semantic.rs:2429-2433 (portable) and :2436-2452 (collections/models/reasoning).

The full plan — the #79 procedure, the embedded-project layout, the nine call sites to re-point, the RP-10/VR-19/SP-12/GC-11 details, the ordered steps and the plants — follows.

Issue #90 — export-and-repoint plan: the backend's fixed Lean runtimes through native modules

Reconnaissance on ~/lexlean-81, branch claude/issue-90-native-runtimes (HEAD d284b1652245b83ba0818fe9b266a76c25606aff, = base main). No repository edits, no git state changes. Every number below is measured; anything I could not confirm is marked UNVERIFIED.

Maintainer decision (issue #90, comment 2026-10-14T13:12:31Z, IC_kwDOT5tTcs8AAAABb7YgiA), accepted as proposed; plan comment on #27 (2026-10-14, IC_kwDOT5tTcs8AAAABb7YgiA sibling, stage 4). Not re-litigated here:

1.2: fixed runtimes become native core modules of a compiler-embedded project via a one-time lossless export (the [v0.4] #27 stage 2: preservation and certification proof libraries as native core modules #79 route, exporter and equivalence record outside the release tree); generated 1.2 modules import the generated runtime module instead of splicing text; the 1.2 compiler-semantics ID records its content address.
1.0/1.1: frozen runtime text stays as committed bytes in a named, audited language/ data file the 1.0/1.1 backends read, with a permanent test that it equals the released 1.1 output; the permanent no-handwritten-Lean gates VR-19, SP-12, GC-11 are extended to name that single declared exception.

Corrections to the brief (verified)

backend/lean.rs carries no raw-string runtime text. grep -c 'r#"' backend/lean.rs = 0; grep -E 'const |static ' finds none. It is the printer (2,600 lines) plus the procedurally built probe/audit module texts. So the brief's "backend/lean.rs (2,600)" as a runtime-text carrier is wrong: that file contributes 0 runtime-text bytes.
A fourth runtime-text file exists that the brief omits: backend/core_v2.rs (LEAN_CORE_DECODER_V2, 27,636 bytes) — the language-1.2 core-module decoder. backend/core.rs's LEAN_CORE_DECODER (12,833 bytes) is the 1.0/1.1 decoder (core-module/1).
The [v0.4] #27 stage 2: preservation and certification proof libraries as native core modules #79 oracle is not in the tree. tests/preservation-library/oracle/ existed only at checkpoint commit d54dbf8551190e4ae77fbf69267fd4328e19db3f (chore(#79): migration oracle checkpoint … (final)) and was removed by the commit that follows. It is recoverable with git ls-tree/git show at that commit; the committed record is tests/preservation-library/MIGRATION.md. The 8 oracle files: README.md (1,640 B), build.sh (928), canon.py (4,869), compare.py (4,933), equivalence.sh (1,904), export.lean (18,945), flags.lean (2,626), probe.lean (2,421).
RP-10 does not pin the runtime text. RP-10 (crates/conformance/src/cases/repository.rs:530) recomputes the compiler-semantics ID = tree_digest over files under language/, schemas/, tests/golden/axiom-parser, tests/golden/canonical-json. Rust source is not in that tree (lib.rs:135-185 lists only language/… and schemas/…). So a changed Rust runtime constant does not move any of the three IDs. Byte-identity of generated 1.0/1.1 output is pinned by the committed goldens (examples/*/expected/build/modules/…, checked by just golden → cargo xtask check-golden), not by RP-10. See §5.
1.0 has no semantic module. ir/semantic.rs:2219-2225 — semantic_module_spec("1.0") = None, ("1.1") = Some("lexlean/semantic-module/1"), ("1.2") = Some("lexlean/semantic-module/2"). So the frozen portable_runtime() text is spliced only for semantic-module/1 (1.1); 1.0 splices it nowhere. core-module/1 serves 1.0 and 1.1 (ir/core.rs:747-755); core-module/2 is 1.2-only.

1. The runtime text, measured

Command (script measure.py): walks each backend file, extracts every Rust raw-string literal r#…"…"# / r##…"##, and reports the enclosing const/static/fn name, source line and UTF-8 byte length.

### semantic.rs total_lines= 3709
  COLLECTIONS_RUNTIME          line= 1340 bytes=8016
  MODELS_RUNTIME               line= 1492 bytes=5101
  REASONING_RUNTIME            line= 1570 bytes=12532
  emit_declarations_for        line= 2046 bytes=13339   <- portable_runtime()
  render_latex                 line= 3602 bytes=91      <- test string
  ... (test strings)
### core.rs total_lines= 1753
  LEAN_CORE_DECODER            line=  785 bytes=12833
### core_v2.rs total_lines= 539
  LEAN_CORE_DECODER_V2         line=   34 bytes=27636
### lean.rs total_lines= 2601
### tooling.rs total_lines= 755
### latex.rs total_lines= 2670
### mod.rs total_lines= 224

portable_runtime() (the const-less fn at semantic.rs:2045, literal opens at 2046) is the frozen 1.1 text. portable_runtime_1_2() (semantic.rs:2027) is derived from it, not a separate literal: it maps each line, prefixing @[expose, noinline] to lines starting @[noinline] public def and @[expose] to lines starting public def . Measured with size12.py (replays the exact transformation):

frozen portable_runtime bytes: 13339 lines: 283
exposed portable_runtime_1_2 bytes: 13491
lines with @[noinline] public def: 14  bare public def: 4   (delta = 9*18 = 162)

Inventory and classification

constant	file:line	bytes	spliced for	class
`COLLECTIONS_RUNTIME`	`semantic.rs:1340`	8,016	`semantic-module/2` only, when `uses_collections` or `reasoning`	1.2-only
`MODELS_RUNTIME`	`semantic.rs:1492`	5,101	`semantic-module/2` only, when a model declaration is present	1.2-only
`REASONING_RUNTIME`	`semantic.rs:1570`	12,532	`semantic-module/2` only, when a reasoning declaration is present	1.2-only
`portable_runtime()`	`semantic.rs:2045` (lit. 2046)	13,339	`semantic-module/1` (1.1)	1.0/1.1 frozen (source of the 1.2 variant)
`portable_runtime_1_2()`	`semantic.rs:2027`	13,491 (derived)	`semantic-module/2` (1.2)	1.2-only (derived, not literal)
`LEAN_CORE_DECODER`	`core.rs:785`	12,833	`core-module/1` (1.0 and 1.1)	1.0/1.1 frozen
`LEAN_CORE_DECODER_V2`	`core_v2.rs:34`	27,636	`core-module/2` (1.2)	1.2-only

Per-file totals of runtime text constants: semantic.rs — 4 constants, 38,988 B (plus the derived 1.2 variant, 13,491 B); core.rs — 1 constant, 12,833 B; core_v2.rs — 1 constant, 27,636 B; lean.rs — 0 B.
Total across the three files named in the brief (semantic.rs + core.rs + lean.rs): 5 literals, 51,821 B. Including core_v2.rs: 6 literals, 79,457 B.
COLLECTIONS_RUNTIME/MODELS_RUNTIME/REASONING_RUNTIME are 1.2-only because their triggers exist only in 1.2: uses_collections tests SemanticPrimitive::language_1_2 (semantic.rs:1307-1329), and models/reasoning constructs call require_language_1_2 (ir/semantic/model.rs:5327, ir/semantic/reasoning.rs:6127).

Splice sites (quoted)

All in crates/lexlean/src/backend/semantic.rs::render_lean (fn at 2360), body starts at 2404 let mut text = String::from("module\npublic import Init\n");:

    if runtime {
        if module.spec == "lexlean/semantic-module/2" {
            text.push_str(portable_runtime_1_2());
        } else {
            text.push_str(portable_runtime());
        }
    }
    if reasoning
        || uses_collections(
            &serde_json::to_value((&lowered, module.elaboration.all_checks()))
                .expect("elaborated declarations serialize"),
        )
    {
        text.push_str(COLLECTIONS_RUNTIME);
    }
    if module
        .declarations
        .iter()
        .any(|declaration| crate::ir::semantic::model::declaration_construct(declaration).is_some())
    {
        text.push_str(MODELS_RUNTIME);
    }
    if reasoning {
        text.push_str(REASONING_RUNTIME);
    }

(semantic.rs:2427-2452.) runtime is set at semantic.rs:2414 (let runtime = elaborated.contains("\"kind\":\"primitive\"") || reasoning;).

Core decoder splice, crates/lexlean/src/backend/core.rs::lean_text (1376):

    text.push_str(if core.version() == 2 {
        crate::backend::core_v2::LEAN_CORE_DECODER_V2
    } else {
        LEAN_CORE_DECODER
    });

(core.rs:1384-1388.)

2. The #79 route, exactly

Recover the oracle (read-only): git show d54dbf8551190e4ae77fbf69267fd4328e19db3f:tests/preservation-library/oracle/<file>.

Inputs (oracle/README.md): the Lean sources of commit ba52c601 — language/preservation-1.2/library/LexLeanPreservation/*.lean and language/preservation-1.2/modules/LexLeanTarget/*.lean; pinned Lean 4.32.1; Python 3.

Procedure

build.sh — for each of LexLeanTarget.{TargetSyntax,TargetSemantics,RustSyntax,RustSemantics} then the 13 LexLeanPreservation.* modules, in dependency order: lean -R src -o out/<M>.olean src/<M>.lean, logging rc= and seconds= per module to out/summary.txt. Per-module cumulative timing lived only in that scratch file (total wall time UNVERIFIED; [v0.4] Author the production compiler itself in LexLean and verify the generated Lean implementation #27's plan comment measures the whole library "compiles in about 2 minutes", 8,916 environment declarations, ~334k unique kernel expression nodes, "the size class of the Atlas migration (24 MB)").
flags.lean — run in a scratch dir with LEAN_PATH=out; reads from the environment the two facts the exporter cannot: which constants the code generator compiled (compiled.txt) and which casesOn constants are sparse (sparse.json).
export.lean — run with LEAN_PATH=out, EXPORT_DIR=<dir>; imports all 13 modules, open Lean Meta. For every declaration each module owns, it writes a child-before-parent DAG of kernel terms via node/push (a memoised ExprStructEq → Nat table; node kinds b,s,c,a,l,p,e,n,t,d,j for bvar/sort/const/app/lam/forallE/letE/nat-lit/string-lit/mdata/proj), plus: universe parameters, type, value, reducibility hints and transparency, the structure/class/instance/projection registrations, simp-set and no-confusion records, matcher and equation-lemma data, reducibility tags, compiler-inlining attributes, sparse casesOn records, grind registrations, and the exact axioms #print axioms reports (via Lean.collectAxioms, i.e. the data stored in each .olean, not a derived set — the first exporter derived them and was wrong for 51 rows).
canon.py <dir> (with EXPORT=<export dir>, FLAGS=<flags dir>) — writes the data as canonical JSON of lexlean/core-module/2 and wraps each module as a .lex.tex source; the output is exactly what language/preservation-1.2/library/src/ holds (13 files).
equivalence.sh <generated> <work> — takes the Lean the compiler generated from the committed native modules (lexlean build of the library project, modules/), compiles it with the pinned Lean, re-exports with the same flags.lean + export.lean, converts with the same canon.py, and requires the result to equal step 4 byte for byte. It also runs probe.lean over both environments and diffs the two outputs.
compare.py — the declaration-by-declaration comparator.

Equivalence record (tests/preservation-library/MIGRATION.md, committed). Declaration by declaration, everything the row carries is compared as trees of kernel terms (nodes are renumbered by meeting order, so rows compare by the terms they root): kind, universe parameters, type, value, reducibility hints and transparency, tags, structure, class, instance, projection, matcher, no-confusion, simplification, equation-record, inlining, sparse-casesOn, grind state, compiled flags, and exact axioms. Result: 9,247 declarations in the same order in the same 13 modules; 8,934 rows equal in every byte of their terms; 313 rows — exactly the sparse casesOn constants — equal up to bound-variable names (the elaborator's fresh hygienic names, invisible to any kernel judgment); the one other difference is the private Lean import the runtime adds (allowed by SPEC §17.10). The attribute probe output is equal. The exporter's output over the original environment is itself reproduced byte-for-byte by the final exporter. Registry: library.toml no longer lists declarations; the 934 hand-registered at ba52c601 are all among the 7,740 plain-identifier names printed by the audit, same module and exact axioms (SHA-256 of the sorted name/module/axioms list b8744d3dd836ee35f12dd2a14b2409c4d097b87fc4cef39efb229c5fbb96afcf).

Sizes (measured, du -sb on this checkout):

53023143  language/preservation-1.2/library/src     (13 .lex.tex, 51 MB)
  472145  language/preservation-1.2/modules         (LexLeanTarget)

Original hand-written Lean: 13 files, 525,026 bytes, Git tree 50f70bb5ffed11244522abd197d4608d27386302. Per-module DAG/source-byte table is in MIGRATION.md (total 9,247 decls / 1,096,101 nodes).

The Atlas (1.0) precedent (examples/uor-atlas/MIGRATION.md): the oracle closed at commit f972285f…; the exhaustive conformance_vr_19 comparison passed in 1,019.88 seconds; 5,577 source declaration records (5,519 native env declarations + 58 private source-compiler records kept as hashed provenance); examples/uor-atlas/src = 24,796,287 B. After equivalence the exporter was removed and VR-19 enforces the permanent condition.

What differs for a runtime rather than a proof library. A proof library is one self-contained import-closed project with a module registry and an entrypoint set; the runtimes are not one project:

They are split across three files (semantic.rs, core.rs, core_v2.rs) and four independent namespaces (LexLeanRuntime, LexLeanCollections, LexLeanModels, LexLeanReasoning), plus the LexLeanCore.Runtime decoder, which is a program (JSON decoder + Lean.addDecl submission), not merely declarations — it cannot be represented as pure core-module data at all (a decoder that concatenates and submits Lean declarations is compiler behaviour). This is the same wall the [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 recon hit: 3266656cd recon(#89 vehicle): certificate text is not core-module data.
Splicing is conditional (if runtime, if uses_collections, if model…, if reasoning), so a runtime project has no single "one module per generated module" shape; it must be a small set of always-imported modules with the conditional economy expressed as ordinary imports.
The 1.1 variant is lossy relative to 1.2: 1.2 needs every definition @[expose]d (a definition's body is invisible across the module system otherwise — semantic.rs:2021-2026), so the exported 1.2 runtime is not byte-equal to the frozen 1.1 text; the frozen text is a deliberately un-exposed rendering. The exporter must reproduce the exposed form, and a separate compatibility fixture must hold the un-exposed bytes.
The decoder text is generated Lean that the generated-Lean audit refuses for comments/char-literals/§18.2 words (see core_v2.rs:9-13), so the exported runtime's rendering must clear the same audit.

3. The embedded project

language/preservation-1.2/library/ is compiled into the binary, not read as a path at runtime. The mechanism:

crates/lexlean/build.rs (SPEC §12.3, §21.2) walks SEMANTIC_DIRS = [("language","language"),("schemas","schemas"),("tests/golden/axiom-parser",…),("tests/golden/canonical-json",…)], bytewise-sorts, and writes OUT_DIR/embedded.rs as
```
pub static FILES: &[(&str, &[u8])] = &[ ("<repo-relative path>", include_bytes!("<abs path>")), … ];
```
(build.rs:25-33, :48-63). A missing normative directory is a build failure.

crates/lexlean/src/production/preserve.rs:150-157 reads it:

fn embedded_text(path: &str) -> Result<&'static str, Diagnostic> {
    crate::embedded::FILES.iter()
        .find(|(candidate, _)| *candidate == path)
        .and_then(|(_, bytes)| std::str::from_utf8(bytes).ok())
        .ok_or_else(|| internal(format!("embedded `{path}` is missing")))
}

Paths and the registry (preserve.rs:28-41):
```
pub const LIBRARY_PATH: &str = "language/preservation-1.2/library.toml";
pub const LIBRARY_SPEC: &str = "lexlean/preservation-library/2";
pub const LIBRARY_DIR:  &str = "language/preservation-1.2/library";
pub const LIBRARY_PREFIX: &str = "LexLeanPreservation";
pub const MODULES_DIR:  &str = "language/preservation-1.2/modules";
```
native_source_path(module) = "{LIBRARY_DIR}/src/{rel}.lex.tex" (preserve.rs:283-289); module_path(module) = "{module with '.'→'/'}.lean" (preserve.rs:162-165). library() (:393) reads LIBRARY_PATH through embedded_text, and build_native (:295-…) parses each module with CoreModule::from_source(&source, "1.2") and checks each import is Init, a TARGET_MODULES calculus module, or an earlier library module.
The project itself (language/preservation-1.2/library/lexlean.toml): spec = "lexlean/project/1", name = "preservation-library", language = "1.2", module_prefix = "LexLeanPreservation", source_roots = ["src"], entrypoints = ["src/Compose.lex.tex", "src/Fixed.lex.tex"], lean_workspace = ".", lean_toolchain = "leanprover/lean4:v4.32.1", a glossary source glossary/preservation.titles, and [limits] … child_timeout_ms = 10800000. The 13 sources are library/src/*.lex.tex (schema lexlean/core-module/2); library.toml lists only modules.
It is also read from disk in tests/conformance at the repo root: support.rs:373 (repo_root().join(LIBRARY_DIR)), cases/preservation.rs:1551, and the shipped calculus modules via MODULES_DIR (calculus.rs:3684-3689).
Because language/preservation-1.2/ is inside the RP-10 tree, it is hashed into the language-1.2 compiler-semantics ID: lib.rs:175 || path.starts_with("language/preservation-1.2/").

By analogy the runtime's project should be a new embedded 1.2 project, e.g. language/runtime-1.2/library/ (mirroring the preservation layout — lexlean.toml with language="1.2", a module_prefix such as LexLeanRuntimeGraph, src/*.lex.tex core-module/2 sources, a glossary/*.titles), plus a registry (language/runtime-1.2/runtime.toml with modules = […], spec, toolchain) and consts RUNTIME_REGISTRY, RUNTIME_DIR, RUNTIME_PREFIX alongside LIBRARY_* in preserve.rs (or a sibling module). It enters the RP-10 tree via build.rs automatically (it is under language/), and lib.rs::is_v1_2_file must gain path.starts_with("language/runtime-1.2/") so the frozen 1.0/1.1 IDs are untouched.

4. The re-point

Where a generated 1.2 module gets the runtime text today: crates/lexlean/src/backend/semantic.rs::render_lean at 2429-2433 — if module.spec == "lexlean/semantic-module/2" { text.push_str(portable_runtime_1_2()); }. (The 1.1 branch pushes portable_runtime(); the 1.0 path never reaches this function.)

What replaces it for 1.2: a public import of the generated runtime module. The import list is built by crates/lexlean/src/backend/lean.rs::module_imports (2031-2044):

pub fn module_imports(document, closure, module_prefix) -> Vec<String> {
    let mut imports: BTreeSet<String> = BTreeSet::new();
    for external in document_externals(document, closure).values() {
        imports.insert(external.lean_module.clone());
    }
    for import in &document.imports {
        imports.insert(format!("{module_prefix}.{import}"));
    }
    imports.into_iter().collect()
}

and consumed by the ordinary-module printer render_module (lean.rs:2083-2140) at 2111 inside the sink.kw("public")/import loop, which already emits, per the comment there, every import as public import. The semantic path (cg. lean.rs:2094) builds its own header: semantic.rs:2404 String::from("module\npublic import Init\n") then a loop over document.imports (2406-2412).

Call sites / functions that must change

backend/semantic.rs:2429-2433 — drop the portable_runtime_1_2() splice for semantic-module/2 and instead prepend the runtime module to the module's imports; the runtime must appear in document.imports (or be added by render_lean) so it lands in the public import loop.
backend/semantic.rs:2427 — the portable_runtime() branch stays (1.1) but reads its bytes from the new frozen-bytes data file (§5), not the literal.
backend/semantic.rs:2436-2452 — COLLECTIONS_RUNTIME/MODELS_RUNTIME/REASONING_RUNTIME splices become runtime-module imports for 1.2 (they are the 1.2-only texts).
backend/lean.rs:2031-2044 (module_imports) and :2091-2097 (render_module dispatch) — the runtime module must join Init + the generated graph in every 1.2 module's public import set; the missing public import Init in the semantic path is generated at semantic.rs:2404.
backend/semantic.rs:2404-2412 — the header text ("module\npublic import Init\n" + document.imports) must admit the generated runtime module.
verify/mod.rs:948-989 — all_names (module-name-conflict rejection) and the externals closure must include the runtime project's modules, and probe_module/audit_modules must see them.
config.rs:275-290 SHIPPED_ROOTS — add the runtime project's module root(s) (the same way LexLeanCollections/LexLeanRuntime/… are already listed).
lib.rs:135-185 is_v1_2_file — add the runtime project path prefix; production/preserve.rs:28-41 — add the runtime registry/dir consts.
backend/core.rs:1384-1388 — unchanged for LEAN_CORE_DECODER (1.0/1.1 frozen) but the 1.2 decoder (core_v2.rs) is a program and stays a text constant unless routed through [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's typed-data representation.

The three probe/audit module texts. In backend/lean.rs there are exactly two text-building auxiliary-module functions: probe_module (lean.rs:2447, String::from("module\n") at 2484) and audit_modules (lean.rs:2531, format!("module\nimport {generated_module}\n") at 2543). I could not find a third in lean.rs; the only other probe text in the backend is the test-only LexLeanTokenProbe builder at backend/lean_tokens.rs:393-400 (String::from("namespace LexLeanTokenProbe\n") … end LexLeanTokenProbe\n), which is not a shipped generated module. The brief's "three probe/audit module texts in backend/lean.rs" is UNVERIFIED — the verified statement is: two (probe, audit) in lean.rs, one test-only in lean_tokens.rs. None of the three is inherently 1.2-only — verify/mod.rs generates the probe and audit for every language's verification. What is 1.2-only is the typed-data representation: only a semantic-module/2/core-module/2 project can carry the probe/audit as native data (the #89 recon 3266656cd shows the semantic-module vehicle rejects certificate text at linking). So the #89 coupling affects the probe/audit texts only when compiling language 1.2; for 1.0/1.1 they remain Rust text, like the frozen runtimes.

5. 1.0/1.1 byte-identity

Where RP-10 is implemented: crates/conformance/src/cases/repository.rs:530-660, case id "RP-10" (registered as RP-10 … §21.2). It:

reads every file under language, schemas, tests/golden/axiom-parser, tests/golden/canonical-json from disk, sorts by bytewise path, computes lexlean::artifact::content_id::tree_digest, and asserts it equals lexlean::compiler_semantics_id_for(lexlean::LATEST_LANGUAGE_VERSION) (repository.rs:565, message "RP-10: the embedded semantics ID differs from the disk recomputation");
parses SPEC §21.2's two exclusion lists ("files introduced solely for 1.2" / "solely for 1.1") and recomputes the 1.1 id (exclude 1.2-only) and 1.0 id (exclude both), asserting each (repository.rs:633-638, "RP-10: the 1.1 ID" / "RP-10: the 1.0 ID");
asserts each listed path exists in the embedded tree, and that examples/nat-add-zero/lexlean.lock (1.0) and examples/semantic-1.1/lexlean.lock (1.1) carry the recomputed ids.

What it compares: three SHA-256 tree digests of the embedded normative files, against compiler_semantics_id_for(language) (lexlean/src/lib.rs:191). It does not read Rust source and does not compare generated Lean. So it is the identity pin for the language data, and it holds the 1.0/1.1 IDs stable by construction (lib.rs:135-160 is_v1_1_file names only language/core-1.1/…, language/std/*-1.1/, language/bootstrap-1.1.toml, language/semantics-1.1.toml, schemas/semantic-module.schema.json, schemas/semantic-snapshot.schema.json). Generated-output byte-identity is pinned separately by the committed goldens (just golden → cargo xtask check-golden; Justfile:71-90) and check-reproducibility (Justfile:78). The 1.1 golden carrying the frozen runtime is examples/semantic-1.1/expected/build/modules/SemanticFixture/Portable.lean and …/KernelReductionDefinitions.lean (both open namespace LexLeanRuntime); the 1.0 goldens (examples/nat-add-zero, peano-arithmetic, list-induction, propositional-logic, uor-atlas) carry no runtime namespace (measured: only 2 golden files under 1.1 and 27 under 1.2 contain namespace LexLeanRuntime).

Where the frozen-bytes data file and its test would live. Put the frozen bytes at a named language/ data file — e.g. language/runtime-1.0-1.1/portable.lex.lean + language/runtime-1.0-1.1/core-decoder.lex.lean (or a single language/frozen-runtime-1.1/<name>.txt) — read by the 1.0/1.1 backends via embedded_text (the build.rs walker embeds any file under language/). The permanent test that it "equals the released 1.1 output" belongs next to the existing frozen-runtime unit tests in backend/semantic.rs (language_1_2_runtime_exposes_every_definition_and_keeps_1_1_frozen, semantic.rs:3647-3688, and imported_list_construction_remains_kernel_reducible, :3682) or as a conformance case: load the data file, and assert it equals the namespace LexLeanRuntime … block of the committed golden examples/semantic-1.1/expected/build/modules/SemanticFixture/Portable.lean (and the core decoder against whatever golden carries LexLeanCore.Runtime). Because the data file would live under language/, adding it changes the RP-10 tree for all three languages unless it is excluded for 1.0/1.1 in SPEC §21.2 — a decision to record: either the file is 1.2-partitioned (language/…-1.2/…) so 1.0/1.1 IDs are untouched, or §21.2's exclusion lists are extended to exclude it from the 1.0/1.1 digests. This is the one place the plan risks moving a frozen 1.0/1.1 ID.

Gate wordings to extend (row + case). The current rows name the libraries, not the runtimes; the exception ("released bytes of frozen versions, the only declared exception") must be added to each. Sites:

gate	SPEC.md row	CONFORMANCE.md row	case (suite)	implementation
`VR-19`	`SPEC.md:8573`	`CONFORMANCE.md:519`	`crates/conformance/src/cases/verification.rs:1139` (`verification`)	inline block, 1139-…
`SP-12`	`SPEC.md:8678`	`CONFORMANCE.md:322`	`crates/conformance/src/cases/preservation.rs:1537` (`preservation`)	inline block, 1537-…
`GC-11`	`SPEC.md:8666`	`CONFORMANCE.md:178`	`crates/conformance/src/cases/certification.rs:205` → `fn gc_11()` at `:2633` (`certification`)	`support::assert_library_has_no_handwritten_lean(prefix, oracle)` (`support.rs:37-68`)

VR-19's row currently reads "…every generated Atlas module publicly depends only on Init and the generated graph, its only backend-support import is Lean, and no independently authored Atlas implementation exists." Extending it to the runtime: every generated 1.2 module publicly depends only on Init, the generated runtime graph, and its own generated graph. assert_library_has_no_handwritten_lean is the shared "no Lean file declares the namespace / lies under the module root" scanner; the extension idiom is to keep that scan but add a narrowly-scoped stated exception for the two frozen data files (they are language/ data objects, not .lean under a module root, so the existing scan would not even flag them — the wording must say so explicitly).

6. The plan

Ordered steps. "Regenerations" means running the write recipes (just golden-write, cargo xtask verify-examples --write, just calculus-write) — the task forbids me from running them now; the implementing PR runs them.

Freeze the 1.0/1.1 bytes first. Extract the exact bytes of portable_runtime() and LEAN_CORE_DECODER into language/runtime-1.0-1.1/<name> data files; change the 1.0/1.1 backends to read them via embedded_text; add the permanent "equals the released 1.1 output" test against the committed 1.1 goldens. Decide the RP-10 partition question (exclude from 1.0/1.1 digests, or place under a 1.2 path). Register the new capability row.
Export the 1.2 runtimes. Stand up a one-time oracle (outside the release tree, as tests/runtime-library/oracle/, deleted by the following commit): build.sh compiling a small Lean project stating the three 1.2 runtimes (portable_runtime_1_2, collections, models, reasoning) as one import-closed project; export.lean (reuse [v0.4] #27 stage 2: preservation and certification proof libraries as native core modules #79's, adapting libMods); flags.lean; canon.py. Commit the resulting .lex.tex under language/runtime-1.2/library/src/ plus runtime.toml.
Equivalence. equivalence.sh on the compiler-generated Lean of the runtime project; require declaration-by-declaration equality (types, values, reducibility, attributes, sparse-casesOn, grind, compiled flags, exact axioms) and byte-equal attribute-probe output. Record it in tests/runtime-library/MIGRATION.md. Confirm the exported projection is @[expose]-decorated so cross-module reduction works (§17.12).
Re-point the 1.2 semantic backend (the §4 call sites): generated 1.2 modules public import the runtime module and drop the four splices. The 1.1 branch keeps reading the frozen data file; there is no 1.0 splice.
Regenerations. The 1.2 compiler-semantics ID changes → regenerate every 1.2 lock, golden, fixture expectation, and expected/verify record (just golden-write, cargo xtask verify-examples --write). The 1.0/1.1 goldens and locks must not change — diff them explicitly.
R3 registrations. For each new condition: a row in SPEC §31 (SPEC.md:8363 "Complete conformance-ID registry"), the matching CONFORMANCE.md row, one scenario, one failing named test conformance_<id>, the implementation, and a VERIFICATION.md plant. Which rows/suite: a runtime-library condition in the preservation suite (sibling of SP-12) for "the runtime project is native core modules, no handwritten Lean, registry lists modules only", and the frozen-bytes condition in the repository suite next to RP-10; the exported-runtime equivalence is recorded under tests/ (a tests/runtime-library/MIGRATION.md), and VR-19/SP-12/GC-11 are edited in place (wording extended) rather than duplicated.
Gates to keep green. just vv = fmt-check model spec-links lint test features bdd inventory examples golden repro deny (Justfile:7). Specifics: RP-10 (three IDs), SP-12, GC-11, VR-19, the new runtime row, cargo xtask check-golden, cargo xtask check-reproducibility, cargo xtask verify-examples, and cargo xtask check-calculus (not --write).
Plants (VERIFICATION.md) — each must turn a named gate red: (a) a changed runtime declaration in language/runtime-1.2/library/src/… → equivalence/conformance_<runtime-id> red; (b) an added axiom to a runtime row → the exact-axiom audit red; (c) a stale generated runtime (commit the sources, revert the generated Lean) → the "generated Lean is byte-for-byte what a verification stages" check red (the idiom of SP-12/GC-11); (d) a handwritten runtime text reintroduced (put back portable_runtime_1_2/COLLECTIONS_RUNTIME into semantic.rs) → the new no-handwritten-Lean runtime gate red; (e) mutate the frozen-bytes file → the "equals the released 1.1 output" test red.

Riskiest step: step 2–3, the lossless export of the 1.2 runtime environment and its declaration-by-declaration equivalence — because the runtime is not one import-closed library (three files, four namespaces, a conditional splice economy, a program-shaped decoder in core_v2.rs, and the exposed/un-exposed rendering difference), and because #79 already burned 51 wrong rows on the first pass deriving attributes/axioms instead of reading them. How to falsify: re-run equivalence.sh — export the original environment and the regenerated one with the same export.lean/flags.lean/canon.py, and require byte-equality of the converted output and equal attribute-probe output; any row that differs must be shown to be a bound-variable-name or private-import difference only. If the decoder (LEAN_CORE_DECODER_V2) proves not representable as core-module data, that is a genuine scope finding (the #89 wall) and must be surfaced, not papered over.

UNVERIFIED list

The brief's "three probe/audit module texts in backend/lean.rs" — verified only two there (probe_module:2447, audit_modules:2531); a third probe text is the test-only lean_tokens.rs:393.
Exact wall-clock/runtime cost of the preservation oracle and of a runtime export (only [v0.4] Author the production compiler itself in LexLean and verify the generated Lean implementation #27's "~2 min" for the library; Atlas conformance_vr_19 = 1,019.88 s; per-module seconds lived in an uncommitted out/summary.txt).
Whether COLLECTIONS_RUNTIME/MODELS_RUNTIME/REASONING_RUNTIME ever reach a non-1.2 module (reasoned from language_1_2 construct gates, not exercised).
Which language/ path partition keeps the frozen data out of the 1.0/1.1 RP-10 digests — a design decision, not yet made.

Two findings from starting the implementation (branch claude/issue-90-native-runtimes), both of which refine the plan above.

1. Every runtime text is a namespace-scoped fragment, not a module. Measured from the literals:

constant	opens with	bytes	consumed at
`COLLECTIONS_RUNTIME` (`backend/semantic.rs:1340`)	`namespace LexLeanCollections`	7,812	`semantic.rs:2441`
`MODELS_RUNTIME` (`:1492`)	`namespace LexLeanModels`	4,886	`:2448`
`REASONING_RUNTIME` (`:1570`)	`namespace LexLeanReasoning`	12,293	`:2451`
`portable_runtime()` — a function, not a constant	`namespace LexLeanCore.Runtime`-style body	13,339	`:2432` (1.1 frozen), `:2430` (`portable_runtime_1_2`, derived)
`LEAN_CORE_DECODER_V2` (`backend/core_v2.rs:34`)	`namespace LexLeanCore.Runtime`	1,286 literal (the rest is assembled)	core-module/2 decoding

Each is text.push_str(...) inside the module the backend is already writing, so they share the generated module's imports and options. Consequence for this stage: before the language-1.2 backend can import the runtime instead of splicing it, each fragment has to become a proper module — module + public import + the same namespace content under a stable module name. The generated 1.2 text changes shape (already declared in this issue's proposal), while every name a generated module uses (LexLeanCollections.Key, LexLeanReasoning.Star, …) still resolves, so what a module means does not change. That is also the thing the equivalence check has to pin.

2. The #79 exporter is recovered and its procedure is reproducible, so the export is not blocked on re-authoring anything. From checkpoint d54dbf8551190e4ae77fbf69267fd4328e19db3f (tests/preservation-library/oracle/, removed by the commit that follows it; 9 files, ~37 KB):

build.sh — compile the calculus modules and the library modules into out/ (lean -R src -o out/<M>.olean), pinned Lean 4.32.1, a per-module log and a summary.txt.
flags.lean — run with LEAN_PATH=out in a scratch directory; writes sparse.json and compiled.txt (the constants the code generator compiled, and the sparse casesOn records).
export.lean — run with LEAN_PATH=out and EXPORT_DIR=<dir>; one JSON per module, each declaration with its kernel data, extension state, and the axioms #print axioms reports.
canon.py <dir> with EXPORT=/FLAGS= — the canonical lexlean/core-module/2 sources, which is what language/preservation-1.2/library/src/ holds.
equivalence.sh <generated> <work> — compile the Lean the compiler generates from those sources, export it again with the same programs, convert with the same script, and require byte-equality; probe.lean additionally compares the attribute state of every constant read by the pinned Lean's own queries from both environments.

So the stage's first implementation step is an extractor: take each runtime fragment out of its Rust literal, wrap it as a module, and drive steps 1-4 over it. Nothing about this stage is blocked; it is a matter of the export, the re-point and the regeneration.

One runtime cannot be a native module of itself: the core-module 2 decoder. A decision is wanted before this issue can close as written.

LEAN_CORE_DECODER_V2 (backend/core_v2.rs:34, 27,636 bytes) is how a native core module reaches Lean at all. core::lean_text writes the module header, splices the decoder, and then one run_cmd … LexLeanCore.Runtime.decodeAndAdd #[…] (…) per chunk of JSON (core.rs:1376-1397). If the decoder were exported as a native core module like the others, the Lean of that module would need the decoder spliced into it to load. The circle is closed only by printing the decoder's kernel terms back to Lean declarations: the lossless kernel-term printer of #93 stage 3c. For this module it would also have to print matcher registrations, the partial groups and the code the generator compiled, because the decoder runs at elaboration time.

What this PR will do, per the decision above:

Four runtimes become native modules. The language-1.2 runtimes portable_runtime_1_2, COLLECTIONS_RUNTIME, MODELS_RUNTIME and REASONING_RUNTIME become native lexlean/core-module/2 modules of an embedded project under language/runtime-1.2/. They are made by the one-time lossless export of [v0.4] #27 stage 2: preservation and certification proof libraries as native core modules #79, with the exporter outside the release tree and a migration record under tests/. Generated 1.2 modules public import them instead of splicing the text.
The frozen bytes move to data. portable_runtime() and LEAN_CORE_DECODER (core-module 1) become committed bytes that the 1.0/1.1 backends read. A permanent test checks them against the released 1.1 output, and VR-19, SP-12 and GC-11 name that exception.
The probe and audit texts become typed data. The probe and audit modules of backend/lean.rs become typed data rendered by the backend.
A gate fails on a planted runtime text constant.

Proposal for the decoder: it stays as the one bootstrap text of language 1.2, named by that gate as the loader of native data. That makes two declared exceptions in all: the frozen 1.0/1.1 bytes and this loader. It is printed from a native module once #93's stage 3c printer exists, tracked as a follow-up issue.

Question: do you accept the decoder as a declared bootstrap exception, so this PR closes #90 and a follow-up carries the decoder? Or should #90 stay open until 3c, with this PR as part of it? Work proceeds on the first reading unless you object; the PR says "Part of #90" until you answer.

A second consequence of "import instead of splice": the native proof libraries name the per-module runtime copies.

Today each generated 1.2 module splices the runtime inside its own namespace (semantic.rs:2425-2452), so every module that uses it has a private copy: LexLeanTarget.TargetSemantics.LexLeanRuntime.index, LexLeanTarget.RustSemantics.LexLeanRuntime.…, and so on. Once the runtime is one imported module, those constants become LexLeanRuntime.…, LexLeanCollections.…. The native libraries are kernel data, and they name the old constants. Measured on main d284b165 (constant nodes in *.lex.tex, excluding expected/):

copy referenced	node references
`LexLeanTarget.TargetSemantics.LexLeanRuntime.*`	226
`LexLeanTarget.TargetSemantics.LexLeanCollections.*`	31
`LexLeanTarget.RustSemantics.LexLeanRuntime.*`	22
`LexLeanTarget.Certification.LexLeanRuntime.*`	15
`LexLeanTarget.Gnaf.LexLeanRuntime.*`	4

The references are in 12 modules of language/preservation-1.2/library/src and 11 of compiler/proofs/src (the certification library). Certificate A also writes one by name (production/certificate.rs:3723, {SEMANTICS}.LexLeanRuntime.append).

Plan for it, unless you object: a renaming of those constants to the shared runtime's names, carried out as data and proved the way #79 proved the migration. I rewrite the constant names and merge the nodes that become equal. Then I compile the generated Lean of both libraries against the regenerated calculus modules, so the kernel re-checks every proof. Then I re-export that environment with the #79 exporter and require it to equal the rewritten data byte for byte. The record goes in tests/runtime-library/MIGRATION.md, beside the export of the runtimes. The copies are identical definitions, so identifying them preserves every typing judgement; the kernel replay confirms that rather than taking it on trust. No library statement changes except for the names of the runtime constants it mentions.

If you would rather keep a per-module copy for the calculus modules, say so: that would leave a runtime text in the 1.2 compiler, against this issue's DoD.

@humuhumu33

Heads-up for @humuhumu33 (and for #84 / #89, which touch the same files): PR #103 (stacked on #96/#98, part of #93) makes the calculus and the Rust machine sources.

crates/conformance/src/{calculus_source,rust_source,gnaf_model,certification_model}.rs are deleted. examples/…/compiler/{TargetSyntax,TargetSemantics,RustSyntax,RustSemantics,Gnaf,Certification}.lex.tex are now edited as .lex.tex (authoring notation) like any other source; cargo xtask check-calculus no longer rewrites them (it still regenerates the five fixture/oracle records AU-07 names).
Conformance helpers that built modules (lx.rs, tl.rs) now delegate to lexlean::sdk (SPEC §24.8), the public authoring API; there is no second authoring path.
A branch that adds to those builders will conflict at the deletion — carry the change into the committed .lex.tex instead. Identities do not change (§21.2: notation is not part of any ID), so no re-verification is triggered.

If your branch for this issue edits one of those builders, tell me and I will do the port.

Generated by Claude Code

Thanks. This branch does not edit calculus_source, rust_source, gnaf_model, certification_model, lx.rs or tl.rs, and no committed .lex.tex of the compiler project. What it changes in that area is generated output: the calculus modules now public import the runtime modules instead of splicing a copy, so the shipped language/preservation-1.2/modules/ and the regenerated records move. I'll rebase after #103 and regenerate, and no port is needed.

The decoder of core module 2 is the loader's seed; #144 closes this issue on that basis.

The open question was whether LEAN_CORE_DECODER_V2 may stay the one Lean text of the language-1.2 compiler. #144 keeps it, declared and gated, for these reasons:

A loader cannot load itself. The decoder is what turns native core-module data into Lean declarations. A native module of the decoder would need the decoder spliced into its own Lean to load.
feat(#93): core modules in the authoring notation, with names (AU-09..AU-12); the language-1.2 libraries are written in it #104 does not change that. Stage 3c's printer prints kernel terms into the core notation, not into Lean. Printing the decoder back as elaboratable Lean would be a large new path: matchers, compiled code, and every auxiliary declaration would have to elaborate to the same kernel terms.
It is not in the trusted base. Every declaration the decoder submits goes through addDecl, so Lean's kernel checks it. A defect in the decoder can fail a build; it cannot admit a statement.
It is bounded. RT-04 holds the decoder to be the only string literal of the compiler that holds Lean declarations under a namespace, and finds a planted second runtime text, raw or escaped.
It is not a runtime of generated programs. That is what this issue removes. The portable, collection, model, and reasoning runtimes are now native modules that generated modules import (feat(#90): the runtime of generated Lean is native modules (RT-01..RT-04) #144).

If you would rather track the decoder separately, say so in review and I'll switch #144 back to "Part of #90".

chore(#90): regenerate the models and reasoning records and the certi…

Merge pull request #144 from UOR-Foundation/claude/issue-90-native-ru…

#90 closed by #144 (merged 08:01Z, merge commit 32afe5da), verified against its DoD. CI of the merged head 6a448857 (main c183f250 merged into the PR; counts 386; the models, reasoning and certificate-resource-exhausted records regenerated on the combined tree): just vv rest and examples, all four host legs, repro and honesty green.

DoD / acceptance line	Where it is met
No handwritten Lean runtime remains in the 1.2 compiler; a gate fails on a planted runtime text constant	`RT-01` (the runtime is four native core modules, no per-module copy, only released 1.0/1.1 output declares a runtime namespace), `RT-04` (no Lean runtime text in the compiler but the core-module-2 decoder; a planted constant, raw or escaped, is found)
The frozen 1.0/1.1 bytes are the declared exception and are tested against the released output	`RT-02`: `language/runtime-1.2/frozen/*` equal the released output byte for byte, and a one-byte change is caught; 1.0 and 1.1 are byte-identical
Every registered runtime declaration with its exact axioms; generated 1.2 modules import only `Init` and the generated graph	`RT-01` (every row pins exact axioms), `RT-03` (verification audits the runtime; a wrongly pinned axiom is `LLV7005`)
Elaboration, `leanchecker` replay and exact axiom audit pass for every example and corpus on the new runtime	the `examples` leg and `bdd`, every 1.2 record regenerated over the renamed libraries
Equivalence evidence; planted defects turn named gates red	`tests/runtime-library/MIGRATION.md` (371 declarations: 368 byte-exact, 3 sparse `casesOn` rows equal up to binder names), five plants in `VERIFICATION.md`

One thing the DoD did not say, now settled: the DoD names the frozen bytes as "the only declared exception". There are two: the core-module-2 decoder (LEAN_CORE_DECODER_V2) is Lean text too. It is the loader of native modules, so by construction it cannot be one of them (a loader cannot load itself); it is not a runtime of any generated program, every declaration it submits is checked by Lean's kernel (a defect in it can fail a build, never admit a statement), and RT-04 bounds it to exactly that one text. The seed is the second declared exception, and #144's description records the argument.

The decision wanted in the issue (how 1.0/1.1 are treated) was settled as proposed: a declared frozen-bytes exception, not closing the versions.

Generated by Claude Code

Correction to my DoD comment above. It mapped every line of the definition of done and acceptance to a gate and called them met. The post-merge review of #144 (#154) found that three lines are only partly met:

"a gate fails on a planted runtime text constant": RT-04 fails on a literal that holds a namespace line and a declaration; a runtime definition without a namespace line, or one placed after a file's first #[cfg(test)] (for example verify/mod.rs lines 2700 to 2783), is not seen. Both reproduced.
Acceptance, "planted defects (a changed runtime declaration, an added axiom, a stale generated runtime, a handwritten runtime text reintroduced) each turn a named gate red": a changed declaration that still type-checks and the reverse-axiom case have no recorded plant.
"imports only Init and the generated graph" holds for the runtime project (RT-01) and is exercised for generated modules by other cases, but RT-04's statement says it and its case does not check it.

The merged behavior itself is sound (main's push CI for 32afe5da is green); the gaps are in the gates' strength. They are tracked in #154, and #90 stays closed with that issue as its follow-up.

Generated by Claude Code

Navigation Menu

Repository navigation

[v0.4] #27 stage 4: the backend's fixed Lean runtimes generated through native modules #90

Scope

The constraint that shapes it

Proposal (for the maintainers to confirm or change)

Work

DoD

Acceptance criteria

Decision wanted

Issue #90 — export-and-repoint plan: the backend's fixed Lean runtimes through native modules

Corrections to the brief (verified)

1. The runtime text, measured

Inventory and classification

Splice sites (quoted)

2. The #79 route, exactly

3. The embedded project

4. The re-point

5. 1.0/1.1 byte-identity

6. The plan

UNVERIFIED list

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

[v0.4] #27 stage 4: the backend's fixed Lean runtimes generated through native modules #90

Description

Scope

The constraint that shapes it

Proposal (for the maintainers to confirm or change)

Work

DoD

Acceptance criteria

Decision wanted

Activity

afflom commented on Oct 14, 2026

humuhumu33 commented on Oct 14, 2026

humuhumu33 commented on Oct 14, 2026

Issue #90 — export-and-repoint plan: the backend's fixed Lean runtimes through native modules

Corrections to the brief (verified)

1. The runtime text, measured

Inventory and classification

Splice sites (quoted)

2. The #79 route, exactly

3. The embedded project

4. The re-point

5. 1.0/1.1 byte-identity

6. The plan

UNVERIFIED list

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 15, 2026

humuhumu33 commented on Oct 15, 2026

afflom commented on Oct 16, 2026

afflom commented on Oct 16, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions