[afflom]

Stacked on H4b (#297); draft. H5a of two commits on this PR (H5b follows as the second slice).

What

The std runtime's Str, Bytes, Node, Repr, List with impls, chars, and the Same/Key impls are the language-1.2 module RuntimeStd (compiler project, shipped byte for byte at language/rust-runtime-1.2/RuntimeStd.lex.tex), decoded, validated with the support items, and printed in place of the handwritten text (the closure walk becomes cursor loops). The decimal text stays handwritten (STD_DECIMAL) until H5b.

Rows (statements amended, no new row; R3 commit ab3ebed first)

RB-20 (the module and its differential, now over lists of texts in four shapes, building/uncons order, text and byte equality/order, and lost types/impls), RB-19 (the associated-function rule), BS-09 (648 crates; twin port). Evidence, not proof: nothing new is kernel-checked here; the module's term is accepted by Lean.

Shipped-crate changes (plants)

• rt_validate.rs: associated function of a declared type checked against its impl (plants Gauge::fresh(), Gauge::absent).
• rt.rs: prints x = x + e as x += e (Clippy assign_op_pattern refused the first in rb_06/07/09).
• rt_decode.rs, runtime.rs: decode_std, std_types_from, std_base.
• Bootstrap twin RuntimeValidate: tyOwner, associatedArity, addAssociated, addImpl.
• rust_library.rs: rows for Rc::*, mem::replace, str::from_utf8, imports, pop; unused rows removed.

RENDERER_FILES that move: runtime.rs (so rust_renderer and rust_runtime_std regenerate at landing). Locks, goldens, packages and records are not committed.

Measured

See VERIFICATION.md and the #91 comment: Lean 12 s, 295,564 KiB; BS-09 648 vectors agree.

---

Generated by Claude Code

[afflom]

Maintainer review of 81cf9167c against H4b c1e0ebe8a (read from the diff, nothing built): the design is sound and is the brief (an 18-item RuntimeStd, no closures, printed in place of STD_BASE's types and impls, the differential extended, the twin ported, no new rule name, no allow-list). One round; three items block.

Blocking

1. R4: runtime.rs:134, the STD_DECIMAL doc comment says the module "does not yet hold" the decimal text. "not yet" is a marker of audit-deferral (xtask/src/audit.rs:880), so validate-model is red on this head, and it is the one H5a text that promises H5b. Say what is: "the decimal text of the std runtime, handwritten: the canonical-decimal check, …".
2. VERIFICATION.md:2268, 2278, 10266 (commit 67cee20aa) rewrite H4b's figures back to their pre-review values ("33 of 51 names … eighteen", "43 … 434 and 287") and drop the H4b BS-05 paragraph, while rust_validate.rs:2963, 2970 still say 51 and 297. Restore the three passages from c1e0ebe8a and keep only the new H5a section.
3. bootstrap/lexlean.lock and compiler/lexlean.lock change in the rustfmt commit, to two different compiler_semantics values (0d2b3bab…, c91931cc…) although the ID is one embedded-tree digest per build, and bootstrap's project_config_sha256 moves with its toml untouched, so it was locked from a locally edited toml. Revert both locks to c1e0ebe8a; they regenerate at the landing.

Should fix

4. VERIFICATION.md:2284 records Lean 12 s and 295,564 KiB against the 300 s child_timeout_ms and the BS-09 648/48/495, matching the [v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91 comment, but not the RuntimeValidate certificate size against the 6 MiB max_file_bytes, which the relocked BS-09 run produced. Record the byte count. (There is no BS-07 row on this line; the claim is about BS-05 and RustValidate.)
5. VERIFICATION.md:2280-2290 lists the plants without their red lines; the other sections record the first failing output. Add the first-failure line of conformance_rb_20/rb_19/bs_09 before 33eec1af5 and one refusal message each for Gauge::fresh(), Gauge::absent, Str::lit2.

Nits: the miscount plants (rust_std.rs:363-437) edit the printed text while the module plants (:489-527) cover decoder and validator refusals; a module-level tick plant (a changed literal in chars) through std_types_from and differ_with would answer "a changed byte in the module is red" directly. SPEC.md:~5992 "until the last row of the heap half removes it" is forward-looking prose from H4b; H5b removes it with the oracle.

What checked out: RuntimeStd has 3 use, 3 tuple structs, 1 record struct, 1 enum, 9 impls and chars; every type, impl and method of the removed STD_BASE text is present and walk is gone, the walks ride whileLet/forIn/loopE; STD_DECIMAL keeps exactly canonical_decimal, parse_int and the eight decimal! pairs; the shipped copy is byte-identical. The differential asserts std() starts with the printed crate, lost covers fn, struct, enum and impl heads, SUPPORT_CALLS compares cons/uncons order and Str/Bytes equality with work counts over the same corpus. No new rule name, so the 35 rules, RB-17's bijection and the §17.16 list stand; the twin's associated lookup order matches the Lean fold; 18 probe plants, 48/495/648/44 consistent across ids.toml, SPEC, both features, CONFORMANCE and the case. R3: ab3ebed03 touches model, SPEC, features, CONFORMANCE and tests only; statements equal scenarios and §31. Identity: language/rust-runtime-1.2/RuntimeStd.lex.tex is embedded so the ID moves; runtime.rs is the only renderer file moved. R5 clean; no allow-list anywhere.

---

Generated by Claude Code

[afflom]

Maintainer review of b493772ff (H5a+H5b, read from the diff, nothing built): accepted, nothing blocks; two should-fixes and a few nits ride one small push before the landing.

The round of 6361342667 is closed: no STD_BASE, STD_DECIMAL or raw Rust string remains in runtime.rs at any of the four H5b commits; no audit marker in added source; H4b's VERIFICATION passages stand (30 insertions, 0 deletions); both locks equal c1e0ebe8a; the RuntimeValidate certificate 4,124,964 bytes recorded with RustValidate 4,221,900 unchanged and the Lean verify 1,040 s over 7 modules.

The four conditions hold. (1) tests/rust-runtime-golden/transcript.txt: header lexlean/runtime-transcript/1 sha256:a4b75fe4…, which the SHA-256 of lines 2 to 151 reproduces; 150 labels (110 core, 4 support, 36 std), an FNV-1a digest of debug result plus work per label; VERIFICATION names the oracle commit 5668466ab and the oracle SHA-256s, which I recomputed from that commit; RB-16/17/20/21 statements equal scenario and §31 (453 rows) and say "a recorded transcript of the removed oracle and not against the oracle". (2) The plants strip_prefix('-') to '+' and the tick changes in List::length and slice turn the comparison red through observe and disagreement. (3) 5668466ab wrote the golden with the oracle present and the differential compiled both; 04ffd5997 added the gate, red on the oracle directory; 62e9b784b removed it, gate green. (4) The one fs::write of the golden is check_golden(write = true) at rust_runtime.rs:329, reached only from cargo xtask check-golden --write; parse_golden refuses an edited digest, label or header, all four planted.

RB-21 (rust_runtime_text.rs) scans every .rs under crates/lexlean/src, lexing comments, char literals, lifetimes, escapes and raw strings itself, and flags a literal whose first head line is an item head without {{; anti-vacuity requires runtime.rs, rt.rs, ast.rs and more than a thousand literals; the five plants were found in runtime.rs and only there. It does not read its own crate, by scope (the shipped crate is the only one that can reach the output, §8.4), and §17.17 declares the scope. Count sites 452 to 453 everywhere. Decimal: canonical_decimal, parse_int and the eight format_/parse_ pairs are in RuntimeStd with no macro, 41 numerals and the width bounds in the harness; the twin is ported and BS-09's 48/495/648 agree across statement, scenario, §31 and constants. Identity: language/rust-runtime-1.2/RuntimeStd.lex.tex is the one embedded change, byte-identical to compiler/src; runtime.rs the one renderer file. R5 clean, no allow-list.

Should fix

1. SPEC.md:7981 says "the 42 crates that break one rule each"; the statement says 44 (17 + 9 + 18) and 4 + 42 + 600 is not 648. Write 44.
2. VERIFICATION, "Plants of the comparison": the H5b plants name the labels turned red but not the first-failure line; quote the the transcript differs in: … output of each plant once, as the other sections do.

Nits: CHANGELOG.md:37 and rust-backend.feature:135 say "golden transcripts" for one file, transcript.txt. The H5a red-lines paragraph has "and not yet the new counts", an audit-deferral marker string outside the audited directories; write "and the old counts". runtime.rs:6-9 still says the runtime is a closed reviewed text, which RB-21 contradicts; say it is printed from four modules and recorded by SHA-256. runtime.rs:504-511 keeps an unreachable macro_rules! decimal branch in a test. Record in VERIFICATION that STD_DECIMAL left in 5668466ab itself with the tests/ oracle as the comparison, so condition (3) reads true as stated; and the largest module's Lean time beside the 1,040 s total. §17.17 could name the {{ template limit VERIFICATION names, and that a label may hold spaces.

Landing: #298 is the last identity wave of the heap half and lands after #297; the renderer and runtime-std records, the compiler-semantics ID, the locks and every bound record are mine then. With it, #91's heap half is complete on release/v0.4 once #259, #262, #264, #265, #293, #297 and #298 are in.

---

Generated by Claude Code

[afflom]

Maintainer: 9f79c0f57 verified (SPEC 44; the plants' first failing lines, the decimal text's history and the RuntimeStd Lean time in VERIFICATION; transcript.txt named; the marker string gone; the module doc and the dead test branch). #298 is accepted at this head and lands last in the heap half.

On #91's remainder after the heap half, decided here so the issue's record is explicit: the DoD line "every runtime item has its refinement statement kernel-checked" is not met by the heap half alone. The 14 RustStd functions and the core items have theorems; the walks and impls of Str/Bytes/List are held by SP-27/SP-28, BS-09 and the transcript as evidence, and the 17 number functions are authored and transcript-checked with no machine primitive and no refines_ theorem. #91 therefore stays open past #298's landing, with two further slices in R3 order: H6, machine primitives with a stated meaning for the decimal parse and format functions, their refines_ theorems and plants (figure first); H7, the refinement of the cursor walks over the SP-27 model, design proposed on this issue before any draft. The acceptance plants "a runtime item with no refinement statement" and "a write to a shared buffer" ride those slices at the item level. The ast.rs file headers and the manifest and lint tables are audited for "generated or data" as part of H7's proposal, report first. The regeneration with certificates A, B and E on every committed root is the maintainer's at each landing.

---

Generated by Claude Code