[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

Follow-up to #144 (closes #90), merged as 32afe5da before its review was done. Reviewed after the merge; nothing below breaks the merged behavior, but four gates and a docs join are weaker than #90's definition of done and its acceptance criteria say.

What happened

• just vv (examples) of the head 6a448857 finished at 08:01:27Z; the PR was merged at 08:01:59Z, 32 s later, by its author, before any maintainer review of the two commits the afflom session had pushed to the branch at ~05:00Z (ab4e9eba, main merged into it with one code conflict, certificate.rs; and 6a448857, the regenerated models/reasoning records, certificate-resource-exhausted fixture and counts). No repository rule stopped it.
• Outcome on main: the push runs for 32afe5da are green (ci 38870996321, reproducibility, honesty), and all eight checks of the PR head were green.

What the review checked, and found sound

The #90 DoD against RT-01..RT-04; the verifier's runtime staging (compile, leanchecker replay, per-declaration axiom comparison in both directions, LLV7005); backend/runtime.rs (imports closed over Init and earlier runtime modules, exact pins, no duplicate row); the equation-lemma rule in preserve.rs (a duplicate is accepted only when both rows are the same declaration up to binder names); packaging (build.rs embeds all of language/, is_v1_2_file puts language/runtime-1.2/ in the 1.2 partition only); the language-1.2 ID in the locks (a4111005…) against the docs; check-calculus, check-golden, check-production-export, validate-model, validate-spec-links, workspace Clippy and the lexlean unit tests on the merged tree. Not done: a line-by-line read of the ~2,400 regenerated records (the gates compare them), and of the oracle table changes beyond their counts.

Remaining issues (each reproduced on 32afe5da; planted files restored)

1. RT-04 cannot see production code after a file's first #[cfg(test)]. The case cuts each source at the first \n#[cfg(test)]. In crates/lexlean/src/verify/mod.rs the first test module ends at line 2694 and lean_error, HEAVY_FRACTION and resource_death (lines 2700 to 2783) are production code after it. A runtime text constant planted after HEAVY_FRACTION passes conformance_rt_04.
2. RT-04 only fires on a literal that holds a namespace line and a declaration. public def LexLeanRuntime.listFold … := … with no namespace line, planted as a string constant in backend/semantic.rs, passes. A text split over literals, concat! or format! is equally unseen. [v0.4] #27 stage 4: the backend's fixed Lean runtimes generated through native modules #90's DoD: "a gate fails on a planted runtime text constant".
3. The acceptance plants of [v0.4] #27 stage 4: the backend's fixed Lean runtimes generated through native modules #90 are not all recorded. It names a changed runtime declaration, an added axiom, a stale generated runtime and a reintroduced text. VERIFICATION.md records five: reintroduced text, frozen byte changed, a generated copy committed beside its source, a per-module runtime name put back, and a row pinning an axiom its declaration does not use. Missing: a runtime declaration whose body changes and still type-checks (no record of which gate fires), and the other direction of the axiom check (a declaration that uses an axiom its row does not pin; the code compares the sets both ways, the plant exercises one).
4. RT-04's register statement claims what its case does not check. "A generated language-1.2 module imports the runtime modules it uses and splices none" is not asserted by rt_04, which reads compiler source only. The import side is exercised elsewhere (semantic_ir.rs, configuration_lock.rs) and the no-splice side by RT-01's namespace scan; the statement should be true of its own case.
5. RT-02 checks "excluded from the language-1.0 and 1.1 identities" by grepping SPEC.md for `language/runtime-1.2/`. The exclusion is real (lib.rs, is_v1_2_file), but the case does not recompute an ID with a frozen byte changed.
6. A local-environment trap in RT-01 and SP-12: their walkers skip only directories named target, .git, .lexlean. A build directory with another name inside the checkout (I used target-check) holds the shipped-preservation build (…/lexlean-preserve-shipped/…) and both cases fail on its Lean files. Cargo marks its target directories with CACHEDIR.TAG; skipping any directory that holds one removes the dependence on the name.
7. A docs join of mine: after resolving the VERIFICATION.md conflict in ab4e9eba by keeping both sides, ## The planted verification of the compiler project (Issue #145) follows the runtime section's last line with no blank line (around line 7705).

Definition of done

• 1 and 2: RT-04 finds a runtime text in any literal outside the decoder and unit-test items, in production code after test modules, whether or not it carries a namespace line, split or not; plants of each shape in VERIFICATION.md, each failing the case.
• 3: the changed-declaration and the reverse-axiom plants run, recorded with the gate that fires (or a new gate if none does).
• 4: rt_04 asserts the statement, or the statement is cut to what rt_04 asserts.
• 5: a test recomputes the 1.0 and 1.1 compiler-semantics IDs with each frozen file changed and finds them unchanged, and the 1.2 ID changed.
• 6: the walkers skip directories that hold CACHEDIR.TAG.
• 7: the blank line.
• A register row where a new capability is claimed (R3), just vv green, and no weaker gate.

Process (for the maintainers)

A merge by the PR's author seconds after the last check, over commits the author had not read, is the failure. Protecting main with the required checks (just vv rest and examples, the four host legs, repro, honesty) and one approving review other than the author's would have held this PR until its review. That is a repository setting, not code.