Native route admits on main: own the three unowned fatal causes; record the class

[gunbai-bot]

Work item adhoc-93d78779-4bb: why //gunbc/instruments:v2-native-frontier refuses its own admission on main.

Diagnosis

The refusals in the brief do not reproduce on main. positive_population_empty, required_native_pass_regressed and both unobserved controls were measured at eb5987e and cfc470c.

Main 1457bd8, measured with claim_executor --v2-native-route on BuildBuddy using the #12550 recipe:

• The smoke member v2.test.native_lane_smoke native_route_positive_population_smoke passes.
• The live pair in v2.native_lane_fixture.control is observed.
• The admission refuses on two clauses only: unattributed_exclusions_present and unattributed_file_refusals_present.

The earliest unjustified boundary is the ownership table v2.workflow.compile_door_cause_ownership known_frontier_causes. Three fatal reasons have producers but have never had a FatalGrain row:

cause	producer	on main
body_lowering_reason_unsupported_form	#12245, #12315 (body lowering's catch-all)	56 member rows (Context), 72 file refusals
body_lowering_reason_function_value_body_unread	#12210	41 file refusals
infer_match_shape_invalid	v2.compiler.04_infer infer_match_bool_arm_row (older; newly reached)	13 member rows (Prepare)

• Why nothing caught it: the producer and its ownership row are joined only by gunbc.witness_v2_native_route native_route_exclusions_all_classified and native_route_file_refusals_attributed. Only the native route runs that join, and the native route is off the merge path (gunbc.rung_drop v2_native_route_off_the_merge_path). So each of those PRs landed without the row it owed.
• A hypothesis this falsified (recorded so nobody re-chases it): I first predicted that the caret refusal from MQ-1 PR-1: a caret symbol in value position refuses at the caret instead of lowering to its ^ token #12392, which refuses v2.std.logic at context, was cascading through imports and emptying the positive population. The parent of MQ-1 PR-1: a caret symbol in value position refuses at the caret instead of lowering to its ^ token #12392 (19f039b) disproved it: there the smoke member reached eval and refused with eval_rejected_invalid_node. That was a separate eval defect, and it is fixed on main. The caret refusals remain real frontier debt; they are owned, and MQ-1 PR-2: a caret symbol lowers to a symbol literal (retire PR-1's refusal) #12420 retires them.
• gunbc.rung_drop native_lane_live_pair_expected_red: already retired (gunbc#12009). The pair is observed on main, and LivePairRequired is the correct standing, so no change is needed.

What this admission stands on: n = 1

• The admitted positive population is exactly 1 NativeTestPassed, the smoke member v2.test.native_lane_smoke native_route_positive_population_smoke, whose body is true. The other 4,694 members are typed exclusions: refused at Context, Prepare or Eval.
• native_route_admission sets no floor beyond non-empty. It has two positive-side clauses:
  • native_route_positive_population_present checks census.agreement_pass > 0;
  • native_route_required_passes_hold requires every identity in native_route_required_pass_identities to pass. That roster holds one identity, the same smoke member.
• Together with the live false/true pair, this proves the verdict path is live and discriminating. It says nothing about how much real test coverage the native route carries.
• Follow-up, deliberately not done here: a floor over the positive population at identity grain. That means enrolling real passing identities in the required-pass roster as they turn native, not a count literal (DESIGN §5). The required lane's first green frontier run, the trigger for v2_native_route_off_the_merge_path, will stand on n = 1 until that exists.

Change

• Three FatalGrain CauseOwnership rows, each with a lane and a flip trigger that names the capability. unsupported_form is a catch-all reason, so its trigger is that each producing site gets a reason naming its shape. A zero count alone is not the trigger.
• RFM gunbc.recurring_failure_mode.refusal_producer_lands_without_its_ownership_row:
  • invalid state, harm, distinguishing facts;
  • rung: mitigated;
  • ceiling: structurally guaranteed;
  • trigger, naming the capability: the admission executes on the landing path, or a merge-path claim joins every fatal reason a stage can emit to a FatalGrain row.

Evidence (same recipe, pinned pushed shas, build and run in one dispatch, 24 GiB cgroup bound after the build)

sha	admission	rc
1457bd8 (base)	refused: unattributed_exclusions_present, unattributed_file_refusals_present	1
8b2d2ac (head)	admitted — universe=4695 population=4695 file_refusals=969, 1704 s, peak RSS 10.3 GB; the emitted binary printed the [native-frontier-roster] proposal	0

• Per-cause aggregates of driver-rows.jsonl are identical on base and head: 1 NativeTestPassed, and the same refused counts per (stage, cause). The change moves attribution only; the population is unchanged.
• The discriminating red is the base run and the positive control is the head run, on the real route.
• I did not add a claim of the form "these three causes are owned". It would re-read the same table it sits beside, so it would be green by construction (DESIGN §4b). The wall that actually discriminates is the admission clause, and it is the trigger in the RFM.
• MQ-1 PR-2: a caret symbol lowers to a symbol literal (retire PR-1's refusal) #12420's head (4475ef4) showed the same two refusals, so this change is independent of it.
• Not verified here: whether //gunbc/instruments:v2-native-frontier itself now answers FrontierUnminted rather than NOT A MEASUREMENT. The roster is unminted by design (gunbc.native_frontier_debt), and minting belongs to the required lane.

🤖 Generated with Claude Code