[afflom]

Stacked on #243 (claude/issue-91-stage4-runtime-core at f04907d); draft. No register row of its own: RB-16 and SP-22 cover every function the module defines.

What

The 92 functions of the eight widths are source, written out one per function and width (no ItemDef family): fixed_<w>::checked_add, checked_sub, checked_mul, checked_quot, bit_and, bit_or, bit_xor, bit_not, shift_left, shift_right, convert (88) and checked_neg_<w> for the four signed widths (4), each a call of a machine primitive, with a refines_<path with _> theorem each. The runtime module is then 110 functions and 110 theorems.

• Modules by path. An exported name that is a path (fixed_u8::checked_add) prints inside pub mod fixed_u8 { … } under its last segment, the consecutive functions of a module in one block. The path is the runtime item's path; RustSyntax gains no construct for it. The fixed! macro, the macro rows and the method rows nothing uses are gone from the base text and the library table, which lists the path forms the generated text uses.
• convert and RustType.i128. convert(a: i128) takes the node RustType.i128 (the AST, the decoder, the Lean constructor appended after overflow, the certificate B encoder, the leaf LkI128 of RustValidate, one more hand-built crate: BS-05 counts 443/195/306/82, 749 in all); its body is the machine primitive tryFrom, so no new machine constructor.
• RB-16. rb_16 compiles the handwritten oracle and the generated runtime together and runs all 110 functions on 9 boundary values of the width (pairs, six shift amounts, nine conversion inputs) and 200 seeded calls each: 27 s; three width plants (checked_add of u8 for checked_sub, shift_left of i32 for shift_right, bit_xor of u16 for bit_or) fail at their function.
• SP-22. The 110 theorems verify in 8 min 1 s (13 min 51 s of CPU), about 4 s a theorem, on this host; sp_22 is 566 s with rb_16 and rb_09, its plant runs on one theorem, and its project allows an hour. SP-22 is the one case of a new bdd part, preservation-runtime (.github/bdd-parts.json, a row in .github/vv-rows.json). The proofs need allWidth and hasWidth among their definitions; a head without them did not terminate.
• Reader stack, measured. The runtime module reads to 1.14 MB of data nested 119 levels (a list of n elements nests n levels), and the reader recurses once per level in frames of about 17 KB in a debug build. Run on threads of 2 to 64 MiB, the read overflows at 2 MiB, which is what a default or test thread has, and succeeds at 4 MiB. So sp_22 (before it had a thread of its own), rp_10 (which recomputes the compiler-semantics ID through identity_bytes) and the decoder in runtime::core each spawn a thread of lexlean::READER_STACK. You wrote 256 MiB; I set 64 MiB, sixteen times the measured need, because it is virtual memory touched only as deep as the recursion goes. The measurement, the three places and the reason are in VERIFICATION.md's SP-22 section.

Results

Pass: rb_01 … rb_06 rb_08 rb_09 rb_15 rb_16 tc_07 sp_12 sp_13 sp_18 sp_21 sp_22 sp_23 sm_35 sm_36 rp_* but rp_10, fmt, clippy -D warnings, validate-model, validate-spec-links. conformance_bs_05 passes every leg through the certified export (1,959 s, with bootstrap/lexlean.lock relocked locally, not committed) and fails only at the comparison with the committed packages.

Fail only on records bound to the compiler-semantics ID, which the regeneration at the end of the stack rewrites once: rb_07, rp_10 (the example lock's 1.0 ID), the lexlean digest unit tests, bs_05's last leg. This PR moves the compiler-semantics ID again on top of #243's move (RustSyntax gains RustType.i128) and leaves every such record as it found it. Not run: just vv, other hosts, repro, honesty, the production export.

Next

equal/compare (traits, PR for the item kinds), then the heap items and the memory model.

---

Generated by Claude Code

[afflom]

Maintainer: 526caf7 is the right fix for the examples failure. The sweep had verified std-models and std-reasoning on the new identity, but my copy-back carried only compiler, stdlib, bootstrap and the examples, so the committed records were release/v0.4's; the audit prefixes in 526caf7 (Ae8004bb2…, Aead6f803…) are what the binary of this tree computes for the two packages, and the commit touches nothing else. The copy list in the landing scripts is corrected for the next landings.

Plan from here, so pushes do not cancel each other's gate: the full gate on 526caf7 runs now (run 39657091738). When it is green bar the Atlas, I join the Atlas records from its thirteen shard artifacts and push that join together with one more harness change (every conformance case runs on the compiler's reader stack, the general form of 497bb77, validated locally on the verification part), then the final gate and the merge by merge commit. Please hold further pushes to this branch until that final gate is up.

---

Generated by Claude Code

[afflom]

Maintainer: the rest part of run 39657091738 is red on two cases, both fallout of my regeneration, and I have the fixes in hand; please leave them to me so the pushes do not collide again.

• conformance_rb_16: the shipped copy language/rust-runtime-1.2/RustRuntime.lex.tex was left in its pre-canonical form when the compiler project was canonicalized in the landing (a0e9447), so it no longer equals compiler/src/RustRuntime.lex.tex byte for byte. Fix: the canonical text at the shipped path. The compiler-semantics ID does not move, because a notation module contributes its data form to the identity (identity_bytes); confirmed on the rebuilt binary: the compiler project's lock is current and its semantic ID is unchanged.
• conformance_rb_06: the plant site pub fn nat_sub(a: u64, b: u64) -> u64 { a.saturating_sub(b) } is now printed from the runtime module as pub fn nat_sub(p0: u64, p1: u64) -> u64 { u64::saturating_sub(p0, p1) } over three lines. Fix: the plant and its wrapping replacement spelled in the printed form.

Both cases, the identity unit tests and clippy are running locally now. The push comes with the Atlas join once the five shards of this run have uploaded their parts (the shards do not depend on rest), then the final gate.

---

Generated by Claude Code

[afflom]

Maintainer: pushed 20efca5 on top of 9666ee5. The two fixes in 9666ee5 are the same text I had validated locally (conformance_rb_06 and conformance_rb_16 pass, the identity unit tests pass, clippy clean), with one difference: rustfmt wraps the let from = "…" line, so 9666ee5 fails cargo fmt --all -- --check, which is the first recipe of every just vv job. 20efca5 is that wrap, and it carries the harness change announced earlier (every conformance case runs on the compiler's reader stack, crates/conformance/src/cases/mod.rs; the verification part passed on it locally, 91 cases).

This run is the one whose Atlas shards I join; the join is the next push, then the final gate. Nothing else is outstanding on this branch, so no further push is needed from anyone until then.

---

Generated by Claude Code

[afflom]

Maintainer: bdd-production of run 39663718224 is red on conformance_md_02 and the cause is my harness commit 463a625, not the tree. MD-02 re-runs itself in a process whose address space ulimit -v bounds at 1 GiB, where the wide artifact must be refused before decoding; the 64 MB stack of the per-case thread is reserved in that space and leaves it no headroom (memory allocation of 5 bytes failed). The part was green on 526caf7 without that commit.

Fix: a revert of 463a625 (the AU-* cases keep their own reader-stack thread from 497bb77, which is all the overflow needed). I am holding the revert locally and will push it together with the Atlas join once this run's shards have uploaded their parts, so that one push starts the final gate. Please hold pushes to this branch.

---

Generated by Claude Code

[afflom]

Maintainer: pushed 677e88d, the final candidate. It carries the revert of my harness commit (MD-02's two reds) and the Atlas verification records joined locally from the thirteen shard artifacts of run 39663718224 (347 records, verified-digest ad57cd76…, audit prefix A9e69b244…, the one the gate's join asked for). On run 39663718224 every other job was green: rest with the two case fixes, examples with the package records, every bdd part, all thirteen Atlas shards. The gate on 677e88d is run 39679288933; on green I merge by merge commit, close the contained issues, and tell the sessions.

---

Generated by Claude Code