One witness per subject where a conjunction over five was the corpus's most expensive row

[gunbai-bot]

One witness per subject, where a conjunction over five was the most expensive row in the corpus

root4_measure_missing_generics_witness_holds conjoined five sub-witnesses, four of which each run a full compile_dag_rust_emit_check — a separate emit compile per snippet. So it cost roughly five times a one-snippet witness by construction. This splits it into five witnesses, one per subject.

The cost, from the floor's own instrument

The required floor emits one [over-cost] <identity> wall_ms= cpu_ms= line_ms= outcome= line per row over the 1552ms disclosure line. This row's cpu_ms across five consecutive main runs:

run	cpu_ms	vs 1552ms line	vs 5000ms fail-stop
c5d52fe67	3322	2.1×	under
83d7f5b5d	3901	2.5×	under
9b4a3d2be	3998	2.6×	under
045ab6278	4252	2.7×	under
2a2804f4d	5623	3.6×	over — failed the required run

Roster stable at planned=11095–11096 across all five, so the row was present in every run and nothing was missing from the denominator.

The median is the finding, not the excursion. Every one of the five is 2.1×–3.6× the disclosure line — the row was over the line in its best run. This is not a well-behaved witness that got unlucky against a tight threshold; it is an expensive row whose ordinary variance reaches the fail-stop. The gate had been reporting this debt all along.

That distinction decided the remedy. The alternative on the table was to reconsider whether completed_over_cost_requirement should block — which would have meant reversing the recorded operator ruling of 2026-08-19, to accommodate a row that should not be near the limit in the first place. Ruled against: fix the row, leave the 5000ms limit and the ruling untouched. Nothing about the gate changes here.

The split is strictly stronger than the conjunction it replaces

a && b && c && d && e reports one verdict for five subjects. When it goes red, nothing says which subject regressed, and the four that held are indistinguishable from the one that did not. Five witnesses name the failing subject in the failure itself.

Nothing is asserted less. The same five predicates run over the same five fixtures with the same required and excluded spellings. No assertion was trimmed to fit a budget — a witness made cheap by asserting less is the failure this work exists to avoid, and if the cost had turned out to be intrinsic to what the row asserts the right move would have been to stop and say so rather than shave it.

The w_ names are unchanged, so the RED-control prose in the module note — which names w_zero_param_alias_use_site_stays_bare and w_unrelated_zero_param_leaf_unchanged as its controls — still names its subjects correctly. No prose rots.

Safety of the rename

Grepped before splitting: root4_measure_missing_generics_witness_holds appears in no roster, quarantine list, or route-gap ledger — the only references anywhere are the module's own declaration and a file-path mention in docs/plans/nat-grounding-unification-design.md. Renaming a witness that is enrolled reds the gating rosters; this one is not.

Execution

All five executed standalone and returned true.

Local wall times are not quoted as floor costs and are not evidence of the improvement: a standalone gunbc run is dominated by corpus startup and runs with the memo disabled, which is 2–3× off the floor's per-claim cost. What the local runs establish is that the five witnesses are green when standalone. The cost claim rests entirely on the [over-cost] readings above, which come from the required runs themselves.

What this does not claim

This does not make the row's total work smaller — five witnesses still run four emit compiles between them. What it does is stop any single claim from carrying five subjects' cost into one 5000ms budget, and make a red name its subject. Whether the four compile-based subjects can share a resolution is a separate question I have not investigated.

Precedent: #9269, the same shape and the same argument on split_dispositions_fabricate_no_loop (four subjects, cpu 4058 in the same failing run — second on the over-cost list behind this one).

— sent from cool-hawk-324

---

This is a specific repair, not a precedent for splitting on shape

A census of all 150 rows on the required floor's [over-cost] list was run after this PR was opened, and it refutes the generalization that motivated looking for a second one:

• 128 of the 150 assert exactly one subject. The two rows split (this one and its sibling) are ranks 1 and 2 by cost; the multi-subject pattern does not survive rank 3.
• The corpus-wide median gap (multi 3372ms vs single 2198ms) is module-confounded. 15 of the 22 multi-subject rows live in test.claim.live_deploy.emit; within that module, single-subject median is 3358ms against multi-subject 3375ms — identical. Cost tracks module, not shape.
• The sharper hypothesis — that the driver is multiple compile subjects — fails in the opposite direction: rows reaching a compile/emit check median 1890ms against 2540ms for rows that don't.
• Corpus-wide the shape is common and cheap: 3,700 of 12,635 test fn declarations are multi-subject (29.3%), 411 with six or more subjects, and almost all of them have always been under the disclosure line.

What survives is this row on its own facts: it carried several independent subjects into one 5000ms budget, it was at or over the fail-stop, and a red named no subject. That is sufficient here and generalizes to nothing. Nothing further was split, and on the evidence there is no reason to split anything on this shape.

The better-supported lead the census produced is per-family fixture cost — live_deploy.emit is 14% of the over-cost list on its own, at a cost independent of what any individual row asserts. That is logged, not started.

— sent from cool-hawk-324