[afflom]

Stacked on claude/issue-91-stage4-heap-syntax at 021879e (#255); draft; to be retargeted to release/v0.4 after #255 merges. It answers the read of 021879e on #255 (its six items) as the maintainer scoped it (comment 6354499859).

Identity-neutral. Only rt_validate.rs, rt.rs and rt_decode.rs (a cargo fmt of one pre-existing line) change in crates/lexlean; none is in RENDERER_FILES, so no record and no ID moves. Nothing under language/, no renderer file, no lock, golden or record.

What

1. One rule family for names and derives (items 1, 2; #91 stage 4, PR 5: the core runtime's support items as source — RuntimeSyntax, RuntimeSupport, RuntimeSemantics (RB-17, SP-25) #254's finding 1). Every string the printer writes as a name must be an identifier that is not a keyword (identifier; Self and self are keywords for names and are accepted only as a path head), and a derive must come from a closed table of five (derive: Clone, Copy, Debug, Eq, PartialEq). Sites: item names (unit/tuple/record struct, enum, alias, static, trait, function), generics (tuple struct, record struct, enum, alias parameter, function), record field names, variant names and record variant field names, trait-method names, parameter names, use segments and aliases, pattern bindings (bind and mut), the field of fieldNamed, struct-pattern field names, and path segments after a struct head, an integer head, an enum variant, and an imported head.
2. RtLit.char is one scalar value (item 3), in an expression and in a pattern (char-literal).
3. The three loud cases (item 4).
   • a struct literal outside parentheses in the head of an if/while/while let/for/match is refused (struct-head; the check mirrors the printer's parenthesisation, so a struct literal the printer would parenthesise is accepted);
   • a left operand of < that ends in a cast, at any depth (x + y as u8 < z), is printed with that operand in parentheses (rt.rs), so the printer stays a function of the module;
   • a generic parameter in a let type, a cast, or a type argument is refused (type-scope): the printer writes those types without the generics in scope, and the runtime has no such use.
4. A plant per site (item 5), not per rule name: variant declared twice; record struct of unequal names and types; struct literal of a path that is no record; tuple variant matched with the wrong number of patterns; struct pattern of unequal names and patterns; and the five sites of hidden-allocation (heap type, String, call, method, method with type arguments) in the core profile.
5. SPEC §17.16 (item 6): the sentence says what RuntimeSemantics does: the expression constructs the module grew by are stuck (except a block and a string literal), and of the pattern constructs a mutable binding binds as a binding does while the tuple, tuple-struct, struct and literal patterns are stuck. The rule list is 40 (sixteen join the 24 of RB-17).

R3 and rows

No new register row (RB-19's row and its plants are the home). The first commit (bd6c992) is the case with its plants. Against the validator at 021879e it is red on the 31 plants of the five new rules (identifier, derive, char-literal, struct-head, type-scope; first as the rule char-literal has no plant, then a unit struct name: ()), on the comparison plant (the printer without the parenthesis), and on RB-17's bijection between the validator's rules and the planted ones; it is not red on the item-5 site plants, which were already green before. The second commit (e06cae1) is the implementation and the text; the third (eaa9dd1) is the review's three nits (Self among the keywords, a no-op retain and a mut gone). RULES of RB-19 grows from 10 to 15 (char-literal, derive, identifier, struct-head, type-scope).

Plants

• ~60 sites planted on the decoded crate, each asserting the rule and the site named in the message (list in VERIFICATION.md).
• The printer's parenthesis is planted by compiling the printed less(x, y, z) = x + y as u8 < z and then the same text without the parenthesis, which rustc refuses with generic arguments.
• Seven sites were disabled alone in the validator (cast-type scope, field-access name, pattern-field names, enum derives, match head, character-literal length, tuple-variant arity); each failed conformance_rb_19; a control edit that changes nothing left it green.

Gates run

cargo fmt --check, cargo clippy --workspace --all-targets -- -D warnings, validate-model and validate-spec-links (446), check-test-inventory, conformance_rb_15 rb_16 rb_17 rb_19 (the last two in 10 s after the build), lexlean --lib: 208 pass; the two record tests (rust_renderer, rust_runtime_core) fail as they do at 021879e. just vv was not run in full (no pinned-toolchain full run on this host and disk); the parts above are the ones the change can reach.

🤖 Generated with Claude Code

https://claude.ai/code/session_018vK7Tm6xHF5etAwKM6r9HG

[afflom]

Maintainer review of e06cae1ca (read from the diff, nothing built): accepted, three nits to ride one small push.

• (a) Self is the one strict keyword missing from KEYWORDS (rt_validate.rs:154), so struct Self; or let Self = .. passes the validator and fails rustc loudly. Add it; segments already special-cases it for paths.
• (b) sites.retain(|_| true); at rust_heap_syntax.rs:1138 is a no-op that only justifies let mut sites; drop both.
• (c) The first commit's message says the case is "red: the validator does not yet refuse them"; that is true of the 31 new-rule plants, the comparison plant and RB-17's rule-count bijection (35 vs 40), not of the item-5 site plants, which were already green on the old validator. Wording only; say so in the PR body.

What checked out: every string rt.rs prints from the module is identifier-checked (once/idents/sig/binds/path/FieldNamed/struct-pattern fields), a closed-table member (derives, METHODS, WRAPPERS, CALLS), or resolved against an identifier-checked declaration (Type::Named, Expr::Call, Expr::Method, impl trait, bounds, struct-literal fields, Expr::Var); ident is ASCII [A-Za-z_][A-Za-z0-9_]* against a 51-entry keyword list, no r#, no non-ASCII. literal() refuses any char but one scalar in expressions and patterns; the printer's {:?} escapes both literals. struct_exposed mirrors the printer's thresholds and head() is applied at If/While/WhileLet/For/Match; binary_left_parenthesized with ends_in_cast parenthesises at any depth; unscoped refuses Type::Param in let/cast/type-argument types while signatures keep it. 46 site plants each assert rule and site; VERIFICATION records seven single-site disablings and a no-op control; 40 rule names equal the §17.16 list and RB-17's bijection; RULES 15. The §17.16 pattern sentence matches RuntimeSemantics.lex.tex:387-394. Identity-neutral: only rt_validate.rs, rt.rs, rt_decode.rs, none in RENDERER_FILES. R4 and R5 clean; the first commit compiles against the old validator.

Landing: after #255 merges I retarget this PR to release/v0.4; it needs no regeneration and goes in before #259.

---

Generated by Claude Code

[afflom]

Maintainer: eaa9dd185 verified (Self in KEYWORDS, 52; the no-op and the let mut gone; the body's red-first wording corrected). #294 is accepted at this head and lands right after #255, retargeted to release/v0.4.

---

Generated by Claude Code