fix(#154): the runtime gates read what they claim to

[afflom]

Closes #154.

Follow-up to #144 (closes #90), which merged before its review. Each item of #154 and where it is met:

#154	Change	Evidence
1, 2	RT-04 reads every literal outside unit-test items: an item under #[cfg(test)] is blanked and the production code after it is read, a declaration under a runtime name is runtime text with or without a namespace line, and literals written together (concat!, an array, +, format!) are read joined with and without a line break.	The case plants ten shapes in memory and asserts each is found; four are also planted on the committed tree and recorded in VERIFICATION.md with the output that names them (verify/mod.rs:2731 after HEAVY_FRACTION, semantic.rs:2965/2966). A fixture inside a test item is not found.
3	RT-03 plants the other direction of the axiom check; the changed-declaration plant is run and recorded.	LLV7005 … observed [propext]. A type-correct body change passes RT-01..RT-04 and is caught by the identity pins (LLC0102, the audit prefix of the committed record); recorded as such, with no runtime-specific oracle claimed.
4	The statement is made true of its case: rt_04 also asserts that every committed language-1.2 generated module imports the runtime modules whose constants it names and declares nothing under a runtime namespace, and refuses a module that drops its imports or splices a declaration.	Register, SPEC §31, scenario and CONFORMANCE.md carry the new statement (RP-07 bijective, 387 IDs).
5	RT-02 recomputes the three compiler-semantics IDs from disk with each frozen file changed: 1.0 and 1.1 unchanged, 1.2 changed. RP-10's recomputation is shared in support.	conformance_rt_02, conformance_rp_10.
6	Every repository walker skips a directory that holds a CACHEDIR.TAG.	RT-01 and SP-12 pass with a Cargo target directory named target-check in the checkout.
7	The blank line before the #145 section of VERIFICATION.md.

What RT-04 cannot see is written in VERIFICATION.md: a text built at run time from parts declared apart. The output-side half of the statement is what bounds it.

No new register row and no new diagnostic code; no compiled behavior changes, so no identity, golden, fixture or record moves.

Local verification

cargo fmt --check, cargo clippy --workspace --all-targets --all-features -D warnings, cargo xtask validate-model, validate-spec-links, and conformance_rt_01..rt_04, rp_07, rp_10, rp_11, rp_14, vr_23, the au_* cases, vr_19, sp_12, ar_06 pass on the tree merged with main 2a3c6f7d (#152).

🤖 Generated with Claude Code

https://claude.ai/code/session_013QppGKetUURseXowZun9KY

---

Generated by Claude Code

[afflom]

A process note, @humuhumu33. We now treat main as protected as #154 describes: a pull request merges only when every check of the current head is green, the head contains main, and an approving review from someone other than its author is on that head. This PR (the author's own account, with all 22 checks green) merged just before the rule, so it has no such review. Could you review it after the fact? Anything you find becomes a follow-up issue; nothing here needs reverting that I know of. From here on a pull request of this account (mine and the contributor sessions') waits for your approval, and one of yours waits for mine.

---

Generated by Claude Code

[humuhumu33]

After-the-fact review of #156 (head 3e87c24, merged as 80331cb), as asked on 2026-10-16. Verdict: sound with follow-ups. Every #154 item is met for the shapes it names, all 22 checks were green, nothing is hidden on the current tree, and nothing needs reverting. Four findings; three need follow-up issues, drafted below for you to file or edit.

How I checked: I compiled the head's RT-04 scanner (crates/conformance/src/cases/runtime.rs:384-752) standalone and planted 19 shapes after the real backend/semantic.rs, the case's own method. The base finds nothing and a plain runtime const is found once.

1. (follow-up, soon) RT-04 blanks production code after a #[cfg(test)] that is not on an item, and blanks the whole file for #![cfg(test)] written anywhere. runtime.rs:594-597 blanks the file if the text contains #![cfg(test)]. runtime.rs:598-636 ends the item at the first ; or { at nesting 0 and does not stop at a } that closes the enclosing scope. Found 0 times: a runtime const after a struct with a #[cfg(test)] field; the same after an enum with a #[cfg(test)] variant; the text in a function whose parameter is #[cfg(test)] (the body is blanked); the text in a match arm after a #[cfg(test)] arm (blanked to end of file); any file holding mod probe { #![cfg(test)] }. Today every #[cfg(test)] in crates/lexlean/src is on a mod, so nothing is hidden, but a cfg'd field is ordinary Rust. Draft A.

2. (follow-up) A committed CACHEDIR.TAG takes its directory out of every walker that gained the skip, and nothing checks that none is tracked. support.rs:33-35 checks only that a file of that name exists. The skip feeds RT-01 and RT-04 (runtime.rs:47), the no-handwritten-Lean helper (support.rs:60), VR-19 (verification.rs:1242), the authoring gates (authoring.rs:71,616,720,1110,1163; authoring_core.rs:54), repository.rs:459 and oracle.rs:186,446. .gitignore does not ignore the file, so one ordinary line in a diff, say beside a hand-written UorAtlas*.lean, hides it from VR-19. This is not a new class: a committed .lexlean directory outside examples/, tests/ or compiler/, or a force-added target/, did the same before. One gate on the tracked tree closes both. Also, "every repository walker" is not literal: xtask/src/audit.rs:10, lib.rs:197 and cases/oracle.rs:2403 still skip by name. They walk named subtrees, so [v0.4] Follow-up to the early merge of #144: RT-04 gate holes, plants #90 asked for, a statement that its test does not check, a docs join #154 item 6 is still met. Draft B.

3. (follow-up, low) Shapes RT-04 still misses that its statement covers ("in several written together", "in any of its shapes"). Found 0 times: concat! with a comment of more than 64 bytes, or a // comment holding a ;, between two halves (runtime.rs:744 measures the gap in source, which includes comments); def _root_.LexLeanRuntime.x; def «LexLeanRuntime».x; /-- doc -/ public def LexLeanRuntime.x on one line; set_option … in def LexLeanRuntime.x (runtime.rs:644-708); and cr#"…"# inside a test module, which desyncs the scan because opens_raw (runtime.rs:405-412) does not know the c prefix. The + join is found, but no plant covers it, though CHANGELOG and the PR body claim it. VERIFICATION.md:7845 records the panic at runtime.rs:765; on the head that assertion is at line 814, and the three runs are condensed into one block. Draft C.

4. (no new issue) The namespace list RT-01 and RT-04 share (runtime.rs:27-32) is a hand list. feat(proofs): program equalities over all inputs: integer order, linear_arithmetic over the runtime, fold laws, and the law form (PF-20..PF-23, #117) #158 merged right after this PR and added LexLeanRuntime.Laws, which declares under LexLeanLaws, so on main 8765fee both gates miss LexLeanLaws text without a namespace line, and RT-01 misses namespace LexLeanLaws in a .lean file. 89b7bcf on v0.4 train: byte literals (#68), widening (#151), dyadic floats (#150), certificates A and B as data, package scaffolding, regenerated once #167 fixes it and asserts the list equals the shipped runtime's namespaces. Keep it on the train, or land it alone if the train is far off.

--- Draft A ---
Title: [v0.4] RT-04: blank only test items, never the code after a cfg(test) that is not on an item (follow-up to #156)

Body:
Follow-up to #156 (review comment of ). without_test_items (crates/conformance/src/cases/runtime.rs:582-636) assumes every #[cfg(test)] is on an item. It ends the item at the first ; or { at nesting 0 after the attribute, and does not stop at a } that closes the enclosing scope. It also blanks the whole file when #![cfg(test)] appears anywhere. A runtime text after a struct with a #[cfg(test)] field, after an enum with a #[cfg(test)] variant, inside a function with a #[cfg(test)] parameter, in a match arm after a #[cfg(test)] arm, or anywhere in a file holding mod m { #![cfg(test)] }, passes conformance_rt_04. Nothing is hidden on main today: every #[cfg(test)] in crates/lexlean/src is on a mod.

Definition of done:

• A #[cfg(test)] blanks only when, after further outer attributes and a visibility, it is followed by an item keyword (mod, fn, use, impl, const, static, struct, enum, type, trait, macro_rules!). Otherwise nothing is blanked, and the code is read.
• The scan for an item's end stops at a } or , at nesting 0 that closes the enclosing scope.
• #![cfg(test)] blanks a file only as one of its leading inner attributes, before any item.
• rt_04 plants each shape in memory (field, variant, parameter, match arm, inline mod with #![cfg(test)]), each followed by a runtime text, and asserts each is found once.
• One shape is planted on the committed tree and recorded in VERIFICATION.md with its output.
• The base tree still reports only backend/core_v2.rs. No new row, no new diagnostic code, just vv green.

--- Draft B ---
Title: [v0.4] The tracked tree holds nothing the repository walkers skip (CACHEDIR.TAG, target, .lexlean, .lake) (follow-up to #156)

Body:
Follow-up to #156. support::holds_cache_tag (crates/conformance/src/support.rs:33-35) skips any directory holding a file named CACHEDIR.TAG. The name-based skips (target, .git, .lexlean, .lake, expected) skip by directory name. Both serve build output beside the sources, but a committed CACHEDIR.TAG, a committed .lexlean directory outside examples/, tests/ and compiler/ (not ignored there), or a force-added target/ takes a directory out of RT-01, RT-04's generated-module check, VR-19, assert_library_has_no_handwritten_lean, the authoring gates and the oracle tree digest. Nothing checks the tracked tree for that. No such path is tracked today.

Definition of done:

• A conformance case, or an extension of an existing RP row with its statement amended, reads the tracked tree (git ls-files, or the release manifest's file list) and fails when any tracked path is named CACHEDIR.TAG, or has a component the walkers skip by name, outside the paths that are legitimately committed under such names (list them, for example expected/ oracles).
• Planted defects recorded in VERIFICATION.md: a tracked examples//CACHEDIR.TAG, and a tracked .lexlean directory outside the ignored roots, each failing the case.
• The CHANGELOG line "every repository walker" is corrected, or the remaining name-only walkers (xtask/src/audit.rs:10, crates/conformance/src/lib.rs:197, cases/oracle.rs:2403) gain the same skip.
• R3 row if a new capability is claimed, just vv green, no weaker gate.

--- Draft C ---
Title: [v0.4] RT-04: read or name the remaining split and Lean-spelling shapes (follow-up to #156)

Body:
Follow-up to #156. The RT-04 statement says a runtime text "in several [literals] written together" and "in any of its shapes" is found. Found 0 times on the merged scanner:
(1) concat!("public def LexLean", <a comment over 64 bytes, or a // comment holding ;> "Runtime.x : Nat := 0"). runtime.rs:744 measures the gap between literals in source, comments included.
(2) def root.LexLeanRuntime.x and def «LexLeanRuntime».x.
(3) a doc comment or set_option … in before the keyword on the same line (declaration(), runtime.rs:644-682).
(4) cr#"…"# (opens_raw, runtime.rs:405-412, does not know the c prefix): inside a test module it desyncs the scan and blanks the production code after the module.
The + join is claimed in CHANGELOG and #156 but has no plant. VERIFICATION.md:7845 records the panic at runtime.rs:765 while the assertion is at runtime.rs:814 on the merged head.

Definition of done:

• The gap between literals is measured in code with comments blanked (scan().code), so comments neither break nor make a run.
• A declared name is compared after stripping root. and « ».
• declaration() skips a leading doc comment and set_option … in.
• opens_raw accepts the c prefix.
• Each shape, and a + join, is planted in rt_04 and asserted found. Any shape left unread is named in VERIFICATION.md beside "a text built at run time from parts declared apart".
• The recorded panic location matches the head that produced it.
• No new row, just vv green.

This is a COMMENT on a merged PR. The formal approval rule (afflom, 2026-10-16) applies from the next PR on; no approval is due here.