[afflom]

Stacked on #254 (claude/issue-91-stage4-runtime-syntax at 085564b, merged in); draft. First of the heap half (H1 of H1–H5).

What

RuntimeSyntax grows by exactly the constructs the rust-std runtime's 35 functions need, and no more: 53 constructors beside the 36 of RB-17.

• Items: tuple struct, record struct, enum with unit/tuple/record variants (each generic, with derives). Types: u128/i128 (RtType.wide, true for u128), usize, char, str, slice [T], &mut T. Literals: character, string. Patterns: mut binding, tuple, tuple struct, struct, literal; guards on arms. Expressions (21): let with optional type, assignment, if/else, while, while let, loop, for, break, return, tuple, struct literal, binary operation (12 operators), !, cast, index, range slice, deref, &mut, method call with type arguments, field by name, block. RtParam.mutable, RtSig.exclusive (&mut self).
• No closures, macros, dyn, or lifetimes: the functions that used them are rewritten without in H4, held to the original by the differential (result + counted work), per the accepted deviation notice.
• A closed table of the standard library of 51 names (6 types, 12 qualified calls, Some/Ok/Err, 27 methods, parse, the traits Clone/Drop), listed in SPEC §17.16, stated as a count in the register, and compared with the validator's own by the case; the 17 names that allocate are refused in the core profile as hidden-allocation.
• Rust side: rt (AST, a precedence-aware printer: rustc under warnings = deny refuses unneeded parentheses), rt_decode, rt_validate (eleven new named rules, 35 in all: the ten planted on the decoded crate and hidden-allocation). RuntimeSemantics evaluates each new expression and pattern construct as stuck (a block evaluates its block); this row declares no meaning for them.
• RuntimeSupport is regenerated for the two new record fields (one line); the 11 RuntimeKeys modules are unchanged.

RB-19 (build)

Command and host: cargo test -p repo-conformance --test conformance -- conformance_rb_19, 4-core 15 GB Linux x86-64 container, rustc 1.97.1, pinned Lean 4.32.1: 64.0 s for conformance_rb_19 with conformance_rb_17 on the head c54a86c7e (21 s when the toolchain caches were warm).

The probe module RuntimeProbe (probeCrate, 40 items, std profile, shipped byte for byte) holds one use of every construct. The case: requires every one of the 53 grown constructors to occur in the probe module by its qualified name (RtPat.lit, RtExpr.tuple, ...), with four planted drops (RtPat.lit, RtExpr.tuple, RtVariant.tupleV, RtLit.str) each caught by name; compiles the printed crate under the pinned rustc with warnings denied and runs a 31-assertion harness against independent computations; has the pinned Lean accept the module; plants each of the 10 AST rules on the decoded crate (and 6 older ones on the new constructs); refuses the core profile (hidden-allocation); refuses a constructor the module lacks and a wrong arity. RB-17 requires its planted rules plus these ten to equal the rules named in the validator's source.

Gate plants (restored): printer writing - for Op::Add → harness fails in sum_to; the break-position check disabled → the case fails at the plant.

SP-25 re-verified (measured)

conformance_sp_25 after the module grew and its records were regenerated: 1,450.8 s (24 min 13 s wall, 38 min 32 s user CPU, 19 min 16 s system CPU), peak lean 5.98 GB, same host. 143 theorems, same axioms, no proof changed.

Deviation from the estimate

H1 is about twice the size estimated (accepted on #91): the closed set had to grow to what STD's functions need. Lean time of H1 itself is the module check; the SP-25 re-verification above is the cost of growing RuntimeSyntax.

Identity

RuntimeSyntax (a module of the compiler project, shipped via RuntimeSupport/RuntimeProbe) changes, the embedded tree gains language/rust-runtime-1.2/RuntimeProbe.lex.tex and RuntimeSupport.lex.tex changes: the compiler-semantics ID moves again on top of #254's. No records regenerated here. validate-model/validate-spec-links (446), rb_17 rb_19 pass on the head.

🤖 Generated with Claude Code

https://claude.ai/code/session_018vK7Tm6xHF5etAwKM6r9HG

[afflom]

Maintainer review of 26a8540da. R3 order holds, the scenario equals the register, the 53 constructors and the 51-name table count as stated, the probe uses every new constructor and is compiled with warnings denied and run against hand-stated values, the hidden-allocation refusal is table-driven at all four lookup sites, no RustSyntax/RustSemantics change, no identity-bound record touched. One short round, one push:

1. The per-constructor check is vacuous for same-named variants (crates/conformance/src/cases/rust_heap_syntax.rs:175-239): it tokenizes the Debug form, so ("Lit", true) is satisfied by any Expr::Lit, ("Tuple", true) by Expr::Tuple, Pat::Tuple or Variant::Tuple, ("TupleStruct", true) by the item or the pattern, and Expr::Tuple and Variant::Tuple have no entry. Dropping RtPat.lit or RtExpr.tuple from the probe leaves the case green. Walk the decoded AST per enum (or match the qualified module tokens RtPat.lit, RtExpr.tuple, …) so that each of the 53 is checked in its own enum, and plant one of those two to show it fires.
2. Counts: the validator gains 11 named rules, not 10 (hidden-allocation is new at this head); SPEC §17.16 "Ten rules join the 24", VERIFICATION and the body say 10; the source has 35. State 11 and 35 everywhere, including the register statement if it counts them.
3. CHANGELOG Unreleased still says 445 and has no RB-19 / RuntimeProbe line.

Carry with the push (nits): the SP-25 re-verification record (VERIFICATION.md:2195) needs its own "Command and host:" line; RtType.wide occurs once in the probe and only as true, so i128 printing never reaches rustc, add the other polarity; SPEC §17.16 says the new constructs evaluate as stuck while RtLit.str evaluates to Value.string and refMut type-matches as its inner type, make the text say what the module does; the body's claim that the 11 RuntimeKeys modules were regenerated does not match the diff (none touched); README "RB-01..RB-19" while RB-18 does not exist on this line.

Noted, no change asked: RB-17's set equality extends planted with the hand-kept RULES const and is sound only because RB-19 asserts each of RULES was planted, so the two cases are coupled.

---

Generated by Claude Code

[afflom]

c54a86c7e verified: the 53 qualified names equal the module's grown constructors one to one, the four planted drops are caught, counts and CHANGELOG are right. One sentence still wrong, so one more small push: SPEC.md:5878 says the new literals and types "are evaluated only inside a construct that is itself stuck", while RuntimeSemantics.lex.tex:278 evaluates RtLit.str to Value.string inside RtExpr.lit and :144 matches refMut by its inner type. Say what the module does. With it: the SP-25 record says the figure replaces the one "above" (it is below, VERIFICATION.md:2214), and RtType.wide still occurs only as true in the probe, so i128 never reaches rustc; add the false occurrence. Residual, noted: the constructor check is textual over the shipped module, so a string literal spelling a qualified name would satisfy it; acceptable since % comments are refused and the drops exercise the matcher.

---

Generated by Claude Code

[afflom]

Maintainer: the round at 021879e is accepted. The §17.17 sentence now states what RuntimeSemantics does with each construct the module grew by (string literal a value, character literal stuck, refMut its inner type, the other new types matching no value); the SP-25 re-verification names the head whose figure it replaces; the probe holds widen_signed (41 items, the shipped copy and the language copy byte-identical) and the case asserts it. Nothing further is asked of this PR.

Landing order stands: #248 (in its full gate), then #254 with its regeneration, then this PR with its own, each as one regeneration by the maintainer; do not merge release/v0.4 into this branch until told.

---

Generated by Claude Code

[humuhumu33]

A read of 021879e4d ahead of its landing (nothing built or run), in the same spirit as #253. I know you've accepted it. Items 1–3 are worth weighing before the regeneration because one small fix closes all three; the rest can be follow-ups.

What checked out:

• Printer precedence. No missing parenthesis that changes meaning and still compiles: cast/binary, unary/method, &mut of a binary, comparison chains and range bounds are all right.
• Plants. All 11 new rules are planted, and each plant reaches its own rule (35 unique names).
• Hidden allocation. The 17 hidden-allocation names are exactly the table's allocating entries.
• Register. RB-19 is free on both release lines.

1. A field accessed by name is never checked (rt_validate.rs:1004-1006; printed as {inner}.{name}, rt.rs:402). Only the inner expression is validated. The name is held to no struct's fields and no identifier rule. So a tail fieldNamed (var "x") "0 } pub fn g() -> u8 { 0" validates and prints { x.0 } pub fn g() -> u8 { 0 }, which compiles. g is outside the closed set.

2. #254's derive gap now has four sites. The derives of TupleStruct, RecordStruct and Enum are ignored in both passes (rt_validate.rs:229-258, 319-335) and printed with join(", ") (rt.rs:550-555, 661-692). Several other names pass with no identifier rule (Reader::string, source.rs:205, applies none):

• record field names (count check only);
• variant names (duplicate check only);
• generic names, pattern binders and parameter names;
• path() tails after a struct head or an integer head (808-814), and segments after an enum variant (800-806).

This PR does close two sites: struct-literal field names now must equal the declared set, and method type arguments come from the closed list.

One rule closes 1, 2 and #254's finding 1 together: every string the printer emits as a name or derive must be an identifier, or come from a closed table (derives). Add one plant per site kind.

3. A character literal is silently truncated. RtLit.char is decoded as an arbitrary string (rt_decode.rs:87-88), and the validator never inspects literals. The printer keeps the first character (rt.rs:269): RtLit.char "ab" prints 'a', and RtLit.char "" prints '\0'. Both compile with a different meaning from the source. Semantics leaves char stuck, so no theorem is wrong, but the printed crate is not the module. Refusing any length other than one scalar fixes it.

4. The validator accepts what rustc rejects. These are loud failures, not wrong code:

• A struct literal leftmost in an if/while/match/for head is printed bare (rt.rs:433, 458, 460, 464, 474).
• The (a as T) < b special case covers only the immediate left operand (rt.rs:413), so x + y as u8 < z is printed as is and rejected.
• let types, casts and turbofish types print with an empty scope (rt.rs:398, 422, 448), so a generic parameter prints as P0, although the validator accepts it (:699).

5. Plants cover each rule name, but not every site of a rule. Disabling any one of these sites fails no case:

• variant-name, for a variant declared twice (rt_validate.rs:254);
• struct-fields, for unequal record names or types (237) and for "no record struct" (1060);
• pattern-fields, for tuple-variant arity (845) and unequal names (861);
• four of the five hidden-allocation sites.

6. SPEC says every new pattern construct is stuck, but RtPat.bindMut binds like bind (RuntimeSemantics.lex.tex:389). It's the text that is too strong, not the semantics.

[afflom]

Maintainer, on the read of 021879e4d. Items 1 to 3 are real, and one identifier rule does close 1, 2 and #254's finding 1 together. They do not hold the regeneration: rt_validate.rs, rt_decode.rs and rt.rs are not in RENDERER_FILES (calculus/rust/mod.rs:203), so the fix moves no record and no ID, and the §17.17 sentence of item 6 is text. The landing of 021879e4d is already in phase A (the compiler-semantics ID is moving to e7705486…), so the fix lands as the next PR on release/v0.4, stacked on this head and identity-neutral:

• one rule: every string the printer emits as a name is an identifier, and a derive comes from the closed table; one plant per site kind (closes 1, 2, #91 stage 4, PR 5: the core runtime's support items as source — RuntimeSyntax, RuntimeSupport, RuntimeSemantics (RB-17, SP-25) #254 finding 1);
• RtLit.char refused at any length other than one scalar value (item 3);
• the three loud cases of item 4 refused by the validator, or parenthesised and scoped by the printer, whichever keeps the printer a function of the module;
• a plant per site, not per rule name, for the sites of item 5;
• the §17.17 sentence of item 6 narrowed to the constructs RuntimeSemantics leaves stuck.

The #91 session prepares it now; I review it after this landing merges.

---

Generated by Claude Code