[afflom]

Stacked on #248 (claude/issue-91-stage4-widths-2 at ea10267, merged in); draft.

What

The last handwritten text of the core runtime, CORE_BASE, is source.

• RuntimeSyntax (compiler/src/RuntimeSyntax.lex.tex): a second closed module beside RustSyntax, not a widening of it. Items: use, unit struct with derives, alias with parameters, static, trait of signatures, impl (trait or inherent) with bounded generics, generic function. Types, expressions and patterns are listed in SPEC §17.16. A name outside the crate is one entry of a closed table (Result, AtomicU64, AtomicU64::new, fetch_add, load, cmp).
• RuntimeSupport (compiler/src/RuntimeSupport.lex.tex, shipped byte for byte at language/rust-runtime-1.2/): supportCrate, 32 items — the uses, Overflow, R<T>, WORK, tick, work, the traits Same/Key with their impls (the scalar macro is nine written-out impls), equal, compare.
• Rust side: rust::rt (AST + printer), rt_decode (shares the source reader via with_reader), rt_validate (24 named rules, each planted; the case reads the rule names from the validator's source and requires the planted set to equal it). runtime::core() prints the support where CORE_BASE stood; CORE_BASE is gone.
• RuntimeSemantics (compiler/src/RuntimeSemantics.lex.tex): the declared meaning of a RuntimeSyntax crate over the calculus values; a method is found among the impls by the receiver's shape. No change to RustSyntax or RustSemantics.
• The #91 stage 4, PR 4: the width families of the core runtime as source (RB-16, SP-22) #248 review fixes (identity_bytes no longer panics, theorems() decodes once, the refines_<path> clause in SPEC, SP-22's wording and measured memory) and the CHANGELOG entry for the whole stage-4 stack are in this PR, as the maintainer decided.

Rows

• RB-17 (build): shipped copy = compiler module; decode/validate/print; differential against the handwritten core runtime (equal, compare, tick, work; scalars, orderings, pairs, and 500 seeded rounds of nested keys of depth two and three, 1,000 depth-three comparisons deciding 491 less, 26 equal, 483 greater); planted modules refused by rule name. Command and host: cargo test -p repo-conformance --test conformance -- conformance_rb_17, 4-core 15 GB Linux x86-64 container, rustc 1.97.1: 9.6 s.
• SP-25 (build; was SP-24 until renumbered, [0.5.0] Content-addressed artifacts as compile-time constants of production roots #115 owns SP-24 on v0.5): 143 equation theorems that rtRun 24 supportCrate "equal"|"compare" args = fromPrimitive (primitive equal|compare args) for the values the calculus types as the arguments of equal (bool, nat, the eight widths, ordering) and of compare (bool, nat, int, the eight widths, and pairs of two of those); the theorem set is computed from the predicate by the case, not read from the module. 16 modules (RuntimeSupport + 11 RuntimeKeys<scalar>, split because 100 theorems in one module were OOM-killed at >13 GB). Command and host: cargo test -p repo-conformance --test conformance -- conformance_sp_25, same host, pinned Lean 4.32.1: 1,440 s on the head 59b93d3cc (24 min wall, 39 min user CPU, 16 min system CPU), peak lean 5.90 GB; the same case took 815 s on a quieter tree before the merge (VERIFICATION.md has all three figures and the spread). lexlean verify of the 16 modules alone: 12 min 28 s; each key module 127–140 s, 5.8–5.9 GB.
• SP-22 now asserts that every authored item is in one of two sets: refined functions (each names a runtime item and has its theorem) and support items of the closed kinds, where tick/work are held by the counted-work gate and equal/compare by SP-25. A new bdd part preservation-support holds SP-25.

What is not proved (stated in the row)

The calculus admits pairs of pairs for compare (calculus/check.rs, orderable). SP-25's theorems stop at a pair of two scalars: each pair level spends rtRun fuel, so the induction needs fuel arithmetic under a symbolic depth that the closed proof language lacks. For nested keys the evidence is RB-17's differential (validation, never a proof). Proof-language step filed for v0.5: #249. There is no Lean twin of the runtime validator yet; SPEC §17.16 states it as the condition of the heap half's second step (H2), and until then the evidence for the closed set is the Rust rule set and its plants.

i128

RustType.i128 (the node of convert's parameter) is accepted by the validator and printed, and is runtime-only: no lowering emits it, and correspond refuses type:i128 in a lowered crate as a construct with no target-semantics correspondence. RB-17 plants it (a crate with an i128 parameter is refused; a row added to the table fails the case).

Identity

RuntimeSyntax/RuntimeSupport/RuntimeSemantics are not imported by Main; the embedded tree gains language/rust-runtime-1.2/RuntimeSupport.lex.tex and the printed core runtime text changes (rust_runtime_core), so the compiler-semantics ID and the runtime digests move; records, locks and goldens bound to it are left to the regeneration. The Runtime modules are in the canonical form of the merged compiler (lexlean fmt); RustRuntime.lex.tex and bootstrap/src/RustValidate.lex.tex are not canonical either and are #248's landing commit's.

Gates (this head, 085564b2b)

validate-model/validate-spec-links 445, fmt, clippy -D warnings, rb_06 rb_09 rb_16 rb_17 rp_* (but rp_10, identity-bound) pass; sp_22 (913 s) and sp_25 pass on the merged tree. Plants and measurements: VERIFICATION.md (RB-17, SP-25).

---

🤖 Generated with Claude Code

https://claude.ai/code/session_018vK7Tm6xHF5etAwKM6r9HG

[afflom]

Maintainer review of 59b93d3cc against the #91 rulings. Scope is right (no RustSyntax/RustSemantics change; the trait/impl fragment, equal/compare over the value predicate, RB-17, SP-25), R3 order holds (first commit d4bf49620 carries rows, scenarios and the failing cases; statements equal the register after trim), the SP-25 theorems quantify over values against TargetSemantics::primitive, the measured numbers are measured. One round, one push:

1. Nine of the 24 validator rules have no plant: call-arity, duplicate-name, function-receiver, impl-extra, match-arms, method-arity, self-type, trait-method, use-path (rt_validate.rs names 24; crates/conformance/src/cases/rust_support.rs:145-250 plants 15, profile-root twice). The ruling was one plant per rule; as it stands any of the nine checks can be deleted and conformance_rb_17 passes. Plant each, list all 24 in the RB-17 record, and add trait-method to SPEC §17.16's rule list (it names 23).
2. SPEC.md ~5839 asserts RuntimeValidate, a bootstrap root beside BS-05, which does not exist on this head. That is a placeholder component in normative text (R4). Word it as the condition the twin discharges in H2 ("until RuntimeValidate lands, the validator's evidence is the Rust rule set and its plants"), or move the sentence to H2's PR.
3. i128 refusal is claimed, not tested: correspond refuses type:i128 only by its absence from CORRESPONDENCE (validate.rs:1222-1238), and no case lowers a crate with Type::I128. Add the plant (a row added to the table must fail a test).
4. Records: VERIFICATION's SP-25 says 815 s, the PR body says 1,442 s on the merged tree; put the measured figure of the head in both, with the "Command and host:" line SP-22's records carry, naming conformance_rb_17 and conformance_sp_25 and the host for the RB-17 figures.
5. SPEC §17.16 ~5842 "for each scalar of the core profile's predicate (bool and every width)" omits the natural and the integer that the register, the case and the 143 theorems include.
6. Anti-vacuity nit in rust_support.rs:105-108: the nested tally check matches " 0," and " 0]", so a zero in the first slot passes; check the first slot too.

Decisions on the two questions the review raised: the #248 review fixes folded into 7dd89f625 (identity_bytes thread fallback, decode-once in rust_refinement.rs, the SP-22 wording) stay in this PR; #248's landing commit is artifacts only and this PR lands directly after it. The CHANGELOG entry for the whole stage-4 stack (RB-15, RB-16, RB-17, SP-21 to SP-23, SP-25, SM-35, SM-36, the runtime as source) goes in this PR too, under Unreleased. Commit titles starting "WIP:" stay; no history rewrite.

---

Generated by Claude Code

[afflom]

Round at 085564b2b verified by reading: all 24 rules planted with the planted set asserted equal to the names parsed from rt_validate.rs (not vacuous: an empty or superset plant list fails the length check), each of the nine new AST plants traced to its check; the twin stated as H2's condition; the i128 plant reaches correspond's type:i128 row and a row added to the table fails it; records and body agree on the measured figures with command and host lines; the predicate prose lists bool, nat, int, every width, Ordering and pairs; the nested tally is checked slot by slot; the CHANGELOG entry names the nine rows. One nit for the landing commit, not a round: VERIFICATION attributes the 5.90 GB peak to the earlier run while the body attaches it to the 1,440 s run.

Accepted. Lands directly after #248 with its own regeneration (the runtime digests and the compiler-semantics identity move with RuntimeSupport.lex.tex).

---

Generated by Claude Code

[afflom]

Maintainer: merged release/v0.4 (9796067, with #248) into this branch at 6cb71ba, resolving README's three table rows to the merged wording with SP-01..SP-25. The landing regeneration runs now on this head (rebuild, relock fixed point, ID substitution, production export, fixtures, model-write, the identity cases, then the verify sweep and records). Please hold pushes to this branch until the final gate is up; the next push here is mine, with the regenerated artifacts.

---

Generated by Claude Code

[afflom]

Maintainer: the landing regeneration is pushed (7fdec04 and 0f372c7) and the PR is ready; the full gate is running on 0f372c7. The records rust_renderer, rust_runtime_core and rust_runtime_std in language/semantics-1.2.toml are set to the digests the record tests compute (the body left them to the regeneration; each one moves the compiler-semantics ID, so they were set before the final fixed point), the ID is 30c5829b…, every project but the Atlas is verified under it, and rb_07, bs_05, rb_16 and rb_17 pass on the committed tree. The Atlas records are joined from the gate's shard artifacts next, then the final gate and the merge. No pushes to this branch, please, until it is merged.

---

Generated by Claude Code

[humuhumu33]

A second read of the hand-written part at 16ee56c90 (compiler/src/Runtime*.lex.tex, rust::rt, rt_decode, rt_validate, the RB-17/SP-25/SP-22 cases, SPEC and VERIFICATION). It is not a request for changes: nothing here blocks landing, and I've pushed nothing. These are offered as follow-ups after the merge, to open as issues if you agree.

What checked out:

• All 143 SP-25 statements: their parameter types and constructors match their names, and each runs supportCrate at fuel 24.
• The hand-listed predicate matches Prim::Equal and orderable in the calculus checker today (check.rs:470, :539).
• Pair keys reach less, equal and greater at both levels.
• Each of the 24 plants reaches its own rule rather than an earlier one, and the planted-set check cannot pass vacuously.

Follow-ups

1. Strings bypass the closed set.

   • rt_validate.rs:108 skips Item::UnitStruct, so derive names are never checked.
   • :69 checks only the first segment of a use path, and path() (:536-551) only the head.
   • Reader::string (source.rs:205) applies no identifier rule, and rt.rs:274-282 prints derives and paths verbatim.

   So a derive string of Debug)] pub struct X; pub fn f() { unsafe { … } } #[derive(Clone validates and prints. The differential stays green because nothing calls f. The only backstop is RB-17's substring check for alloc, std:: and macro_rules (rust_support.rs:83-88). This contradicts rt.rs:7-8 ("an item outside the set cannot be written, decoded, or printed") and §17.16's "refused by name". Suggested fix: one identifier rule applied to every string the printer emits as a name, with a plant.

2. Plants are per rule name, not per check. Each of these checks lacks a plant of its own:

   • the impl-complete "states twice" branch (rt_validate.rs:329-334);
   • the trait-method arity check (:508-516): the units.cmp() plant is refused earlier, by the table check at :444;
   • the function-receiver check (:276-282), which appears unreachable.

   Either of the first two can be deleted and RB-17 stays green. That falsifies VERIFICATION's "none can be deleted without the case failing".

3. SP-22's coverage check sees only free functions. held (rust_refinement.rs:87, :110) inspects Support::Fn items only. The validator accepts an inherent impl with pub methods, and no visibility rule covers them (rt_validate.rs:152-156). So the SPEC's "refuses an authored item in neither" does not hold for impl or trait methods. Generated code cannot call them, so the impact is low.

4. SP-25's guard is fixed to today's checker. The predicate is hand-listed (runtime_semantics.rs:33-44) rather than derived from orderable/prim_type, so if the checker gains a type, SP-25 stays green. complete (:132-145) matches theorems by name and substring, without checking the argument types or that the crate is supportCrate.

Minor

• The work counter never wraps in the test: the tick amounts in rust_support.rs:43 sum below 2^64, both sides use a wrapping fetch_add, and RuntimeSemantics leaves tick/work stuck. A wrap would under-report work silently.
• rt.rs:183-188 prints method calls, fields, borrows and == without parentheses. For example, Equals(Equals(..)) prints a == b == c. The shipped crate uses none of these shapes.