Preserve superseded witness workflow verdicts

.github/workflows/witnesses.yml

@@ -119,7 +119,7 @@ jobs:
     runs-on: [self-hosted, linux, arm64]
     needs: [build, floor]
     timeout-minutes: 5
-    if: always()
+    if: always() && needs.build.result != 'cancelled' && needs.floor.result != 'cancelled'
     steps:
       - name: Both required lanes must have succeeded
         run: |

dag/gunbc/required_lanes_gate.dag

@@ -66,8 +66,9 @@ fn required_lanes_echo(words: List<Node>) -> Node {
   bash_build_command_with_words(words: words)
 }
 
-// The receipt line, printed on every run: it is what preserves the cancelled-versus-failed
-// distinction that the job's own conclusion loses under `always()`.
+// The receipt line, printed on every non-cancelled run: it locates which live required lane
+// failed or skipped. Workflow-level cancellation is preserved before this script by the
+// aggregate job condition and never collapsed into a lane failure here.
 fn required_lanes_receipt_stmt(build_var: String, floor_var: String) -> Node {
   required_lanes_echo(
     words: [

dag/gunbc/witness_floor_workflow.dag

@@ -1045,65 +1045,66 @@ fn build_lane_job() -> Job {
 // precondition paragraph records, and the reason a bare `needs.*.result` comparison would not
 // have worked here either).
 //
-// IT IS `always()` AND NOT `!cancelled()`, WHICH IS THE ONE PLACE IN THIS FILE THAT DEPARTS
-// FROM THE HOUSE GUARD -- stated explicitly, because a reader who knows the convention will
-// otherwise correct it back and reopen the hole. Every other guard here is about whether a STEP
-// should run inside a job that is already running, and there `!cancelled()` is right: a
-// cancelled run should stop. This condition decides something else -- whether the REQUIRED
-// CONTEXT EXISTS AT ALL -- and under `!cancelled()` a cancelled run leaves the aggregator
-// skipped, so the context is reported as skipped rather than as a verdict.
-//
-// That is the same question one layer out, and it is a question about GITHUB rather than about
-// this repository: does a skipped or cancelled required check block a merge? NOBODY HERE HAS
-// EXECUTED THAT, and the right response is not to go and measure it -- it is to make the
-// outcome not depend on it. Under `always()` the job runs unconditionally, always reads both
-// results, and always reports success or failure ON ITS OWN TERMS, so SKIPPED disappears from
-// the required context entirely. That is construction over validation (§5): the ambiguous state
-// becomes unrepresentable rather than tested, and a third-party behaviour becomes a property of
-// our own file.
-//
-// WHAT IT COSTS, named rather than glossed: a lawfully superseded run now reports this context
-// RED instead of cancelled, because a cancelled lane is not `success`. Measured on run
-// 32883390033, where a fleet event ended both lanes and this job duly published `failure`.
-//
-// THE STRONGEST ARGUMENT AGAINST THIS CHOICE IS RECORDED HERE RATHER THAN ANSWERED AWAY, so
-// that the next person who wants `!cancelled()` finds the case already made instead of
-// rediscovering it (raised by a peer session, 2026-08-25, from GitHub's own documented
-// semantics rather than from a measurement). The objection: `always()` is the one condition that
-// survives workflow cancellation, `cancel-in-progress` is armed on every pull_request, so this
-// fires on the MODAL event in the repository -- and it destroys the cancelled/failed distinction
-// at the RECORD level rather than at the reader's, where nothing can recover it afterwards. That
-// ambiguity cost a peer session hours in one day, diagnosing 38 lawful supersessions as a
-// false-red epidemic.
-//
-// THAT OBJECTION IS RECORDED WITH ITS ANSWER ATTACHED, because half of it standing alone is what
-// would send a future reader back to `!cancelled()` -- and the answer is in this job's own step.
-// THE CONCLUSION LOSES THE DISTINCTION; THE ANNOTATION PRESERVES IT. The step echoes
-// `required lanes: build=$BUILD floor=$FLOOR` and repeats both values inside its `::error::`, so
-// on every single occurrence, permanently and machine-readably, the log says WHICH state each
-// lane was in. A red whose cause is printed in its own error annotation is not the ambiguity the
-// objection warns about: the hours lost that day were lost because `cancelled` and `failure` were
-// indistinguishable at the reader with NOTHING UNDERNEATH to recover, and here there is always
-// something underneath, one line away. The loss is real at conclusion grain and repaired at the
-// grain anyone actually diagnoses from. (Withdrawn to this weight by the session that raised it,
-// after reading the step body.)
-//
-// The house-style half does not survive either, and it is worth saying why rather than just
-// noting the departure: counting `!cancelled()` occurrences infers a rule from shapes, while
-// what each guard DECIDES is the fact. Every other one decides whether a step runs inside a job
-// that is already running; this one decides whether the required context exists at all.
-//
-// WHY IT IS NOT TAKEN: THE ASYMMETRY IS ABOUT WHICH HEAD PAYS. Checks are tracked per head SHA,
-// so a superseded run's red lands on a head that by construction will never be merged -- the
-// push that superseded it created the head that will. `always()` is therefore NOISY ON ABANDONED
-// HEADS. `!cancelled()` moves the cost onto the LIVE one: a lane killed with no replacement run
-// coming -- observed twice on 2026-08-25, once with `runner_name` empty and zero steps, once with
-// both lanes ended at 18:43 and no push involved -- leaves this context SKIPPED on the head that
-// is still the merge candidate, and whether a skipped required check blocks a merge is exactly
-// the unmeasured GitHub behaviour the paragraph above exists to stop depending on. Quiet-and-
-// unknown on a live head is worse than loud-and-definite on a dead one.
+// SUPERSESSION IS NOT A FAILED LANE VERDICT. The workflow concurrency authority above permits a
+// newer pull-request push to cancel the older run. Under `always()` that cancellation still armed
+// this job; the shell then applied `cancelled != success`, exited 1, and overwrote the workflow's
+// superseded conclusion with a fabricated FAILED aggregate. Every push-over-push thus emitted a
+// CI-failing alert about a head whose work had intentionally moved on.
+//
+// CANCELLATION DOES NOT PROVE SUPERSESSION. It says only that this attempt stopped. Two
+// cancellation-without-replacement cases were observed on 2026-08-25: one had an empty
+// runner_name and zero steps, and one ended both lanes at 18:43 with no push involved. Under
+// a cancelled-lane exclusion those live heads leave the required context skipped rather than
+// receiving this gate's loud refusal. The exact GitHub merge-admission treatment of that skipped
+// required context remains unmeasured; this change must not describe it as safe by construction.
+// For a manual cancel, runner eviction, workflow timeout or operator-stopped queue on the CURRENT
+// head, this is specifically fail-open: CurrentHeadUnestablished receives no aggregate context
+// even though it must block. The modal supersession case and this hazardous case share
+// LaneCancelled; only an independent head-standing observation can separate them.
+//
+// RUNG DROP, DECLARED UNDER DESIGN §4b(3). PREVIOUS RUNG: mechanically preventive -- `always()`
+// made the aggregate context exist and refuse for every stopped lane, including cancellations
+// with no replacement. TEMPORARY RUNG: mitigatable -- superseded pull-request runs no longer
+// fabricate failures, but a cancelled live attempt depends on GitHub's skipped-required-context
+// handling and an operator must rerun it rather than receiving a located aggregate refusal.
+// REASON: the current lane-result input carries cancellation but no replacement-run observation,
+// so it cannot distinguish the modal lawful supersession from an abandoned live attempt; the
+// false failure alert is removed at the only distinction currently available, accepting the
+// explicit CurrentHeadUnestablished fail-open above until the restoration lands. BOUNDED
+// POPULATION: pull_request workflow runs only -- cancel-in-progress is false for push,
+// merge_group and workflow_dispatch, and their concurrency group is unique per run. Within that
+// boundary the two abandoned cases above are the observed population; no count of future
+// cancellations is claimed. RESTORATION TRIGGER: a typed observation joins this run's PR and
+// created_at to a newer run for the same PR. Then the job returns to `always()` and distinguishes
+// replacement-present (superseded: no failure) from replacement-absent (abandoned: refuse) before
+// reading the strict lane gate. This trigger is the operator-ranked `floor-current-head-binding`:
+// FloorAttemptSubject carries pull_request, measured_head, run_id and run_attempt;
+// FloorHeadStanding is Current, Superseded or Unobservable independently of FloorLaneTerminal.
+//
+// This is deliberately NOT a relaxation of the lane gate on a non-cancelled workflow. The job
+// still runs after failed or skipped needs and the script still admits exactly `success`;
+// failure, skip, abandonment and every unknown lane result remain loud refusals there.
+data required_lanes_aggregate_cancellation_rung_drop: String = "Previous rung mechanically preventive; temporary rung mitigatable; reason a cancelled lane lacks replacement identity; population bounded to pull_request cancellation events; restore when a typed same-PR newer-run observation distinguishes superseded from abandoned."
+
+data required_lane_cancelled_result: String = "cancelled"
+
+fn required_lane_result_not_cancelled_condition(job_id: String) -> String {
+  concat("needs.", concat(job_id, concat(".result != '", concat(required_lane_cancelled_result, "'"))))
+}
+
+// `cancelled()` WAS THE WRONG OBSERVATION. Run 32935233342 proved it: floor concluded
+// `cancelled`, the workflow eventually concluded `cancelled`, yet this job's `!cancelled()`
+// condition armed and the aggregate fabricated FAILURE. The needed jobs' result fields are the
+// values the gate actually consumes, so cancellation is excluded from those same fields. The
+// leading status function remains necessary to displace GitHub's implicit success() over needs.
 fn required_lanes_aggregate_job_condition() -> String {
-  "always()"
+  concat(
+    "always() && ",
+    concat(
+      required_lane_result_not_cancelled_condition(job_id: build_lane_job_id),
+      concat(" && ", required_lane_result_not_cancelled_condition(job_id: floor_lane_job_id))
+    )
+  )
 }
 //
 // THE STEP-LEVEL `always()` STAYS, and it guards a different thing rather than restating this

dag/test/claim/witness_floor_workflow_consolidation_witness_test.dag

@@ -207,8 +207,9 @@ test fn w_RED_neither_lane_waits_on_the_other() -> Bool {
   }
 }
 
-// THE GATE RUNS AT ALL, AND THEN REFUSES. Two claims, and the first one is the one that was
-// missing -- this row's earlier form asserted only the second and went green over the defect.
+// THE GATE RUNS FOR EVERY LIVE ATTEMPT, AND THEN REFUSES A NON-SUCCESS LANE. Superseded attempts
+// are different: workflow cancellation is the verdict, so the aggregate job must not run and
+// overwrite that truthful state with a fabricated failure.
 //
 // THE DEFECT IT MISSED, kept here because the row is only trustworthy if its own blind spot is
 // on the record. It asserted `if: always()` appeared SOMEWHERE in the file. It did -- on the
@@ -237,10 +238,20 @@ test fn w_RED_neither_lane_waits_on_the_other() -> Bool {
 // discriminating, which is exactly how the job-level guard defect below went green.)
 // load-bearing in its own right: `cancelled` and `skipped` are not `success`, so a lane that
 // never produced a verdict refuses here rather than passing.
-test fn w_RED_the_gate_runs_and_refuses_on_a_failed_lane() -> Bool {
+//
+// THIS IS EMITTED-SHAPE EVIDENCE, NOT A BEHAVIOURAL GITHUB RECEIPT. It proves the job-level
+// cancelled-lane exclusions and the live-attempt refusal are both present at their distinct YAML
+// grains. It does not prove that GitHub classifies a superseded run correctly, nor what branch
+// protection does with a skipped required context after cancellation without replacement. The
+// authority's required_lanes_aggregate_cancellation_rung_drop names that uncovered boundary and
+// its restoration trigger; a string_contains witness must not be cited as having closed it.
+test fn w_RED_aggregate_skips_cancelled_lane_and_refuses_failed_lane() -> Bool {
   match expected_witness_floor_yml() {
     WitnessFloorGenerated { content: yml } =>
-      string_contains(s: yml, pattern: "\n    if: always()")
+      string_contains(
+        s: yml,
+        pattern: "\n    if: always() && needs.build.result != 'cancelled' && needs.floor.result != 'cancelled'"
+      )
         && string_contains(s: yml, pattern: "\n        if: always()")
         && string_contains(s: yml, pattern: "exit 1")
         && string_contains(s: yml, pattern: "'!=' 'success'")