[humuhumu33]

Stacked on H5 (#298, claude/issue-91-stage4-heap-h5 at 45f2f07ef); draft. Contributor session continuing afflom's H6 WIP (befb1a0ee, fc276d224, merge 1e32dc3c8) with new commits on the same branch; nothing of his is rewritten. It extends SP-29 and RB-20 of #293/#297/#298 to the number functions and adds SP-30, so it merges only after #298 and retargets to release/v0.4 with it. No release/v0.4 merge in this branch.

What

• The eighteen number functions as source with kernel-checked refinement. RustStd (shipped byte for byte at language/rust-runtime-1.2/RustStd.lex.tex) defines parse_int, format_int, and the format_/parse_ function of each of the eight widths. Each is one machine call: Machine.formatDecimal w (family 40), parseDecimal w (41), parseDecimalInt (42, optional; parse_int turns None into Err(Overflow)), and formatDecimalInt (43). RustSemantics gives each an existing calculus primitive as its meaning: Prim.formatDecimal, and Prim.parseDecimal at the fixed type or at Ty.int. Each has its refines_<function> theorem (runExport 12 stdCrate "<function>" args = runItem std Item.<item> args, by term_cases, axioms [Classical.choice, Quot.sound, propext]). All 32 theorems of the module share one definitions list of 63 of the 73 names, pruned as H4b did.
• format_int. Item::FormatInt (the decimal text of an integer) had no function and no statement: the generated code called format_i64, and refines_format_i64 is over Value.i64, which machineAccepts does not let a Value.int through. format_int(a: Int) -> Str is one call of formatDecimalInt, printed Str::format_i64(a); Item::FormatInt is called as format_int. The golden transcript has no format_int label. HELD_AS holds its digest to the recorded format_i64 digest on the same values, so transcript.txt is unchanged.
• SP-30 (new, register 454): every runtime item has its refinement statement. cases/rust_items.rs reads the 144 items of runtime::Item::all() and the statements of the refines_ theorems of RustRuntime and RustStd. It requires exactly one statement per item, at its profile, on the function Item::path gives it; equal and compare are held by SP-25. This is the item-level acceptance plant "a runtime item with no refinement statement" of [v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91.
• Already done by #91 stage 4, H5a: the types, impls, and helpers of the std runtime as source (RB-20, RB-19, BS-09) #298 (H5b), so not here. The planted-constant gate (RB-21) and the removal of STD_BASE and the oracles, whose results are the transcript digests.

Rows

R3 commits first: 113070614 (SP-30: the row, its scenario, §31, CONFORMANCE, the case; red: every runtime item is held: "`formatInt` is a runtime item with no refinement statement"), accde1454 (SP-29 and RB-20 statements name format_int and formatDecimalInt), and 0f38e4ae5 (the laws and the harness, red until a9415a7db). SP-29 and RB-20 are amended. The SPEC, CONFORMANCE and feature copies of RB-20 now equal ids.toml byte for byte; the WIP had amended only ids.toml.

Shipped-crate changes (each with its plant)

Change	Plant
ast.rs: Machine::FormatDecimalInt (family 43, arity 1, printed Str::format_i64(a)), next to the WIP's FormatDecimal, ParseDecimal, ParseDecimalInt	SP-23 takes 44 constructors; RB-15; SP-29 (a machine call of another primitive)
runtime.rs: Item::FormatInt is called as format_int; the unit test looks a free function up at the start of a line (it took the method Str::parse_int for parse_int)	SP-30 (the item called as format_i64 is refused)
data_b/syntax.rs: formatDecimalInt	BS-05

RENDERER_FILES that move: ast.rs, runtime.rs. The bootstrap twin of RustValidate learns family 43 and the item row format_int.

Measured (SP-22 protocol, posted on #91 before this draft)

• lexlean verify of the scratch project, two runs on a shared host: 33 s and 61 s, peak 706 to 719 MB with #91 stage 4, H5a: the types, impls, and helpers of the std runtime as source (RB-20, RB-19, BS-09) #298's modules; 30 s and 70 s, 703 to 745 MB with the arms; 91 s and 91 s, 1,631 to 1,649 MB with RustStd's 32 theorems pruned (unpruned 2,160 to 2,199 MB).
• conformance_sp_29 258.5 s, peak lean 1,399,332 KiB. conformance_rb_20 96.9 s. conformance_sp_23 227 s. rb_15, rb_19, rb_21 and sp_30 pass.
• Not run locally: conformance_bs_05 (it exceeds the 4.5 GB lanes here) and the bootstrap verify that sizes RustValidate's certificate against max_file_bytes (6,291,456). Both are left to CI on this draft. The BS-05 counts are raised by one per family: 55, 464/213, 327/100, 438/301.

Found on #298's head

conformance_rb_20 fails on 45f2f07ef. The plant "an index that finds the next position" overflows at the harness index u64::MAX and panics without naming index_list. b736ca1dd writes i.wrapping_add(1), after which the plant is the transcript differs in: index_list.

What fails here until the regeneration

The locks (compiler, bootstrap; LLC0102), the records rust_renderer, rust_runtime_core and rust_runtime_std and the compiler-semantics ID (the_compiler_semantics_records_the_runtime, conformance_rb_07, rp_10), the generated packages and the production export (every package that formats an integer now calls format_int), BS-05's committed-export assertion, and the goldens bound to the ID. transcript.txt does not change. Locks, goldens, packages and records are not committed.

---

🤖 Generated with Claude Code

[afflom]

Maintainer review of H6 at 5c6c99012 on 45f2f07ef (the clean h5 merge 624d1f712 changes nothing of it): accepted, one fix before the landing.

Checked and found as stated: the R3 order (113070614 row, scenario byte-equal to the register at every site, conformance_sp_30 red with "formatInt is a runtime item with no refinement statement" until a9415a7db; the case unchanged from the R3 commit to the head); SP-30 reads the 144 items of Item::all() and the refines_ statements of both RustRuntime (110) and RustStd (32), one per item at its profile on Item::path, equal/compare held to the equal_*/compare_* theorems, and its five plants are real code paths (the format_i64 plant goes through the path closure and exercises the same statement.function != called branch, which is acceptable); the four machine constructors map to Prim.formatDecimal and Prim.parseDecimal at the fixed type or Ty.int, identical to itemPrimitive, no new meaning, machineAccepts lets Value.string and Value.int through only where machineWidth is none, 42 alone optional; format_int as Item::FormatInt's function, the twin's item row moved, the four committed generated packages that still call format_i64( left to my regeneration as the body says; HELD_AS is sound (same values [i64::MIN, -1, 0, i64::MAX], same seen! form, the digest covers value and work bytes and not the label, both functions one Str::format_i64(a) call) and transcript.txt is untouched; the rb_20 plant fix is the one line and the old i + 1 panics in the debug-built harness at u64::MAX; the register is 454 by +1 at every count site, SP-01..SP-30, §17.17 at families 26 to 43; no deferral, no new public failure path, no unwrap in shipped code; the 29 files are all named by the body; the 32 theorems share one 63-name list, axioms [Classical.choice, Quot.sound, propext], and the shipped copies are the same blobs as the compiler sources.

The fix. The BS-05 statement (model/ids.toml, features/suites/bootstrap.feature, SPEC §31, CONFORMANCE through validate-model --write) still quotes the H3 figures: 37 machine crates, 446 validateCrate runs (195 refusals), 309 correspondCrate runs (82 refusals). The constants at this head are 55 / 464 (213) / 327 (100), and were already 51 / 460 (209) / 323 (96) at #298. Set the statement to the head's figures in #304 (R1: the register is the source and the figures are part of the statement); I set the intermediate figures at each landing of #265, #293, #297 and #298 with my BS-05/BS-06 recounts, as I did for #259. No other change.

Order: #262 is in its sweep; #264, #265, #293, #297, #298 follow; #304 lands after #298 and retargets to release/v0.4 with my regeneration (the format_i64( to format_int( rewrite of the generated packages included).

---

Generated by Claude Code

[afflom]

Defect and fix on this head, one commit (65d4e1616, on 624d1f712):

• bootstrap/src/RustValidate.lex.tex machineName (line 2239) and machineArity (line 2247) each end their body with one ) too many, so the module did not parse (LLP2001 at 2239:1970, the parenthesis count). Two characters removed; lexlean check of bootstrap/ reports 7 modules clean and lexlean fmt --check of bootstrap/ (6 modules) and compiler/ (17 modules) is canonical, both on a scratch relock of the committed projects (the committed locks are the landing's to regenerate).
• The BS-05 statement carried the H3 figures; it now states the head's: 55 hand-built machine crates (MACHINE_CRATES), 464 validateCrate runs of which 213 refusals, 327 correspondCrate runs of which 100 refusals (the evaluator's 438 and 301 are in the case's constants, not in the statement). Edited in model/ids.toml, features/suites/bootstrap.feature, SPEC §31, and CONFORMANCE.md via the model write; validate-model is clean (454 ids).

Not run here: conformance_bs_05/conformance_bs_09 (the bootstrap verification, about 17 minutes of Lean plus the stale committed locks); they are for the landing.

---

Generated by Claude Code

[humuhumu33]

Thanks for 65d4e1616: the extra ) in machineName/machineArity was mine (my edit script closed the new branch twice), and the BS-05 statement figures are the head's now.

One commit on top, 609968ed3: rustfmt only. CI's just vv (rest) failed at fmt-check on 5c6c99012, because the format_int plant block in cases/rust_std.rs and one block in cases/rust_items.rs were not in rustfmt layout. On the new head it is past fmt-check. repro fails on examples/collections: LLC0102 (lexlean.lock is stale), which belongs to the regeneration.

conformance_bs_05 and conformance_bs_09 were not run here. As you said, they are for the landing.

---

🤖 Generated with Claude Code