Skip to content

Accepting wildcards cut 1: name the verdict classifier and the two route gates - #13382

Closed
gunbai-bot[bot] wants to merge 4 commits into
mainfrom
accepting-wildcards-1
Closed

gunbai-bot[bot] wants to merge 4 commits into
mainfrom
accepting-wildcards-1

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Oct 5, 2026

Copy link
Copy Markdown
Contributor

Accepting wildcards, cut 1: the verdict classifier and the two route gates

Three closed-coproduct matches whose wildcard arm returned the ACCEPTING answer, so an unhandled or future constructor silently inherited acceptance. Each is repaired by naming every arm; no fallback is swapped for another. Three non_fold_residue rows deleted by hand with this receipt.

1. dag/gunbc/fleet/fleet_revision_acceptance.dag::merge_group_run_carries_verdict

  • Bad state: match c { Cancelled => false, Skipped => false, _ => true } over WorkflowRunConclusion (8 constructors) — every conclusion the arm did not name was treated as carrying a verdict.
  • Path that permitted it: a floor run concluded Neutral (the workflow did not apply to the revision) was counted as a verdict, landed in others, and (a) refused an all-neutral floor as RequiredCiMergeGroupRunsNotSuccess — "the floor ran and did not succeed", a different refusal demanding a different operator action — or (b) blocked admission of a floor where another run succeeded, reading not applicable as contradicting verdict.
  • Owning invariant: a run carries a verdict exactly when GitHub states a terminal outcome for it (Success, Failure, TimedOut, ActionRequired, StartupFailure); Neutral, Cancelled and Skipped report that no verdict was rendered (DESIGN 5: the failure arm must refuse, never widen).
  • Repair at the owner: the classifier names all eight conclusions; the admission flow consumes it unchanged. A conclusion added to WorkflowRunConclusion later cannot inherit verdict-carrying — the match refuses to compile without an arm (NonExhaustiveMatch).
  • Executed discriminator (red before, green after), both run on the remote runner (BuildBuddy, cold build, gunbc run --claim-run, cgroup-bound 24 GiB):
    • a_floor_of_neutral_runs_refuses_as_unconcluded_not_not_success: FAIL before (refused ...NotSuccess), PASS after (refuses RequiredCiMergeGroupRunUnconcluded, run_ids == [11]).
    • a_neutral_run_beside_a_success_admits: FAIL before (neutral beside a success blocked the entry), PASS after.
    • Every other claim in fleet_desired_merge_queue_admission_witness_test.dag (26) and fleet_revision_acceptance_witness_test.dag (9) PASSES before and after; merge_group_runs_with_no_verdict_refuse_as_unconcluded is unaffected.
  • Census row deleted: dag/gunbc/fleet/fleet_revision_acceptance.dag::merge_group_run_carries_verdict.

merge_group_run_succeeded (_ => false) is left as is: a narrow "is exactly Success, else false" accessor whose false is right for every other constructor — out of scope per the brief, its census row stays.

2. dag/gunbc/runner/runner_throughput_qualification_route.dag::route_bmc_writes_are_gated

  • Bad state: the gate audit matched StageEffect with BmcWrite { .. } => <gate check>, _ => true — any effect that is not exactly BmcWrite trivially complied.
  • Path that permitted it: a write-shaped effect added to StageEffect later (the coproduct is the audit's own vocabulary: BmcWrite, GitHubControlPlaneWrite, ObservationOnly) would have inherited "not a BMC write" and skipped the approval-gate audit by declaration identity — the route qualified without anyone deciding what the new effect means for the gate.
  • Owning invariant: EVERY BMC WRITE IS UNDER THE APPROVAL GATE, by declaration identity; the audit is the owner of that reading, and stage_is_effectful/stage_egress already spell all three effects by name.
  • Repair at the owner: ObservationOnly => true and GitHubControlPlaneWrite { authority: _ } => true are named — both true today, but now true by arm, not by fallback; a fresh effect demands an arm at this gate.
  • Executed discriminator: behavior is unchanged for every existing constructor (the 29-claim runner witness file PASSES identically before and after). Totality executed by removing the ObservationOnly arm: the module load refuses with the compiler's non-exhaustiveness diagnostic naming this match — the same refusal a fresh constructor produces (output in the run log; the diagnostic is CompilerDiagnostic::NonExhaustiveMatch, rendered "(non-exhaustive)").
  • Census row deleted: dag/gunbc/runner/runner_throughput_qualification_route.dag::route_bmc_writes_are_gated.

3. dag/gunbc/runner/runner_throughput_qualification_route.dag::route_dispatch_selector_names_the_attempt

  • Bad state: DispatchFloorToSlot { .. } => <selector check>, _ => true over QualificationStage (5 constructors).
  • Path that permitted it: a stage constructor added later inherited the vacuous "names the attempt" pass without the route deciding whether a dispatch-shaped stage must name the attempt.
  • Owning invariant: the selector-names-the-attempt requirement is a property of dispatch stages; the other four stage kinds say so explicitly rather than by default (the house rule of dag/gunbc/product/compute_board/composition.dag: _ on a closed coproduct means a variant added later contributes silently).
  • Repair at the owner: all four non-dispatch stages named => true.
  • Executed discriminator: 29-claim runner witness file PASSES identically before and after; totality executed by removing the CollectInstruments arm — the load refuses non-exhaustive, naming this match.
  • Census row deleted: dag/gunbc/runner/runner_throughput_qualification_route.dag::route_dispatch_selector_names_the_attempt.

Census

Three rows deleted from dag/gunbc/non_fold_residue.dag by hand (the detector's doctrine: never auto-delete; greening a site deletes its row with the receipt on the PR). Roster goes 907 → 904. The remaining rows are the wider roster — out of scope for this cut.

Benign wildcards passed over (one line each)

  • cohort_observation.dag::instants_comparable — "is exactly Incomparable, else comparable": the true answer is right for every other constructor of the closed comparison result; not a policy site.
  • emit_copy_qualification_transport.dag filter, mtcollins1_boot_run.dag::observer_ok (Optional Present/none), bmc_model.dag::bmc_sol_drop_fired (is-exactly shape) — instruments/measurement or is-exactly accessors, not policy/decision sites.

Brian Searls added 3 commits October 5, 2026 10:13
…ute gates

Three closed-coproduct matches whose wildcard arm returned the ACCEPTING
answer, so an unhandled or future constructor silently inherited
acceptance. Each now names every arm; no fallback was swapped for
another. Three non_fold_residue rows deleted by hand with the receipt.

- merge_group_run_carries_verdict: _ => true over WorkflowRunConclusion
  counted a Neutral conclusion (no verdict rendered) as a competing
  verdict: an all-neutral floor refused as NotSuccess instead of
  Unconcluded, and a neutral run beside a success blocked the entry as
  contradictory. All eight conclusions are named; two witnesses pin the
  no-verdict arm (red before, green after).
- route_bmc_writes_are_gated: _ => true let a write-shaped StageEffect
  added later skip the approval-gate audit. ObservationOnly and
  GitHubControlPlaneWrite are named true-by-arm.
- route_dispatch_selector_names_the_attempt: _ => true over
  QualificationStage inherited the vacuous pass for stages added later.
  The four non-dispatch stages are named.

Fresh-constructor acceptance test: each match now refuses to compile
without an arm (NonExhaustiveMatch naming the site, executed on the
runner by removing one arm per site).
The floor's parse refuses '//' inside a declaration body (DESIGN 4c:
only leading blocks at module-item grain); move the verdict-classifier
and dispatch-gate rationale above their declarations.
The row I deleted asserted the fn's wildcard residue; the fn still
carried one (_ => false over WorkflowRunStatus), so the floor's
diff verdict read unrostered=1. Name Queued, InProgress, Waiting,
Requested and Pending => false -- a run that has not completed has
rendered nothing yet -- so the fn carries no wildcard at all and the
deletion is earned.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Approved at 5d25b04.

The verdict repair is semantically discriminating, not only exhaustive: all eight WorkflowRunConclusion arms and all six WorkflowRunStatus arms are named. Neutral no longer enters the verdict population, so an all-neutral floor reaches RequiredCiMergeGroupRunUnconcluded and a neutral run cannot contradict an independently successful run; Failure, TimedOut, ActionRequired and StartupFailure remain verdict-bearing non-successes. The two new controls exercise both changed downstream outcomes.

The route edits preserve current behavior while closing the accepting fallback: StageEffect is covered 3/3 and QualificationStage 5/5, with every constructor named exactly once and no invented fields. A future constructor now requires an explicit policy decision instead of inheriting true.

The non_fold_residue delta is exact: the only three deleted rows are the three totalled sites; merge_group_run_succeeded and the other benign/is-exactly wildcards remain rostered or untouched as described. The PR changes only the two production modules, the two semantic witnesses, and the three-row roster deletion. All four exact-head jobs are green and GitHub reports the PR mergeable. No blockers.

@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Oct 5, 2026
@gunbai-bot
gunbai-bot Bot removed this pull request from the merge queue due to a manual request Oct 6, 2026
Main independently landed the same totality repair in
merge_group_run_carries_verdict/merge_group_run_succeeded. Resolution keeps this
branch's named arms (a superset of main's naming) and main's roster wholesale:
the only semantic delta is Neutral => false, this PR's deliberate, witnessed
behavior change (floor-of-neutral refuses as Unconcluded; neutral beside a
success admits). Main's roster already drops the three frontier rows this PR
dissolves, so the merged roster is main's verbatim.
@gunbai-bot

gunbai-bot Bot commented Oct 8, 2026

Copy link
Copy Markdown
Contributor Author

The red floor at 93dfc07 isn't from this diff. It's the runner pool's missing browser-toolchain premise (RunnerBrowserToolchainReadyForJobUser): all four floor runners tested (srv1-03, srv1-08, srv3-03, srv4-09) refuse the browser/spark wet claims this PR's changed-witness closure selects, with WetTerminalHostPremiseUnmet, and origin/main reproduces the same refusals in a full floor run. No content change can fix it; it needs a host action on the floor runners. The PR stays approved and unqueued until that lands. — sent from lively-ram-153

@gunbai-bot

gunbai-bot Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor Author

Closed without folding in the v1 closeout bankruptcy (#13641). Accepting-wildcards cut 1 is blocked only on the retiring floor's browser-toolchain premise; the surviving native job doesn't require it. Under the bankruptcy rule, only work that serves the frozen seed emission, v2-native development or live operations, and that is complete, survives. The branch is kept for archaeology; no follow-up obligation is created. — sent from neat-wolf-604

@gunbai-bot gunbai-bot Bot closed this Oct 9, 2026
gunbai-bot Bot pushed a commit that referenced this pull request Oct 10, 2026
…3383, #1 (#13694)

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: gunbc-ci-auto-heal <searlsbrian@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant