Type the heal push race: a branch that moved under heal leaves by SupersededByAuthorHead

[gunbai-bot]

What was actually failing

heal-generated-artifacts regenerated correctly, committed, and then died on git's own non-fast-forward exit status because the author pushed while it was building. Under the step's default shell the bare push ends the job, so the outcome reaching every reader is a raw rejection hint — true about git, silent about which state it is, and indistinguishable at the grain people read (a job name and a conclusion) from a drift the author really did cause. That is why this was reported upstream as the opposite defect.

Log verification of the three reported lanes

Read per job id, not per run (gh run view --log --job <id>; --allow-escape-sequences is rejected by that subcommand and its usage text greps as zero matches).

lane	run	heal job	verdict
#11083 head eb94bf95	34646493695	failure	lost race — committed c1f349c20e, ! [rejected] ... (fetch first)
#11083 head 8cbaa834	34644122365	failure	lost race — committed bd81aa80d9, same rejection at 20:55:03
#10994 heads b4ec82a3, 0c987b11	34644904585, 34633098011	success	neither — heal was green in both; the reds are required-witnesses-build and required-witnesses-floor

So it is the same race twice on one branch, and #10994 is not a heal failure at all — that lane's premise does not survive the log.

No genuine drift refusal exists in this population (item 4). Both #11083 heal runs regenerated and staged cleanly with no AUTHOR_COMMIT_DRIFT; docs/design-rung-drops.md was read and derived normally. Nothing here supports a rung-drop refusal finding, so none is filed.

The fix

The two states are decidable in the job by one question it can answer: is the remote branch still at the head this run judged?

• gunbc.heal_revalidation gains HealSupersededByAuthorHead and its PriorRunDisposition mirror SupersededByAuthorHead — the author-produced counterpart to the heal-produced SupersededByHealedHead that already stood beside it.
• gunbc.ci_spec classifies the push instead of assuming it. Branch moved → the named arm, exit 0. Push refused with the branch still where this run left it → a hard red, HealPushRefused.

No force, no retry. A second attempt against a still-moving branch either loses again or lands a repair derived from a tree nobody checked.

Why this arm exits zero where its twin exits nonzero

Both arms say the same thing about standing — the head this run judged is no longer the tip. They differ in what they leave behind. SupersededByHealedHead follows a published head: heal pushed H1, nothing has judged it, and the nonzero exit is what stops an unjudged tree standing as green. This arm publishes nothing — the healed commit stays on the runner and the branch carries an author head with its own run, which regenerates from the only tree that matters. Exiting nonzero would render a red square beside a PR for a scheduling outcome about a revision that no longer exists: exactly arm one of gunbc.recurring_failure_mode repair_job_red_is_attributed_to_the_content_it_repaired. The outcome stays loud and countable as a typed ::notice:: naming all three revisions plus the branch and both path sets; it does not stay loud by borrowing the channel that means "the content under review is wrong". heal-generated-artifacts is not a required lane, so this opens no gate.

This retires arm one of that row and not the row. Arm two still reports red on every heal that lands, and the row's trigger is explicit that a fix covering one arm does not retire it. I did not append a receipt to the row: it is a hot per-lane append surface and its text stays accurate as written.

Evidence (executed, both directions)

heal_outcome_token gives the name the log speaks one authority — the emitter cannot apply a coproduct arm to revisions that exist only as shell variables, so the token crosses into the script as text, and the witness derives its pattern from that fold rather than typing it twice.

• Positive: all three new/extended witnesses return true.
• RED 1 — rename the arm's token in the model → the_heal_push_race_leaves_by_its_own_named_arm returns false. The join is real, not a self-satisfying grep.
• RED 2 — flip the arm's exit 0 to exit 1 in the emitter → same witness returns false. The exit status is asserted as ordered adjacency, so membership alone cannot green it.

Both reverted; the emitted witnesses.yml diff is the single expected hunk.

🤖 Generated with Claude Code

https://claude.ai/code/session_01HKvv6ctMMcjbtFUiNV64dF

[gunbai-bot]

Both findings in review 64120 verified and fixed in 4201833. Both were mine.

1 — validation where construction was available. Correct, and sharper than stated: my own annotation asserted that an arm cannot be applied where its revisions are shell variables, four lines from live_heal_push_refusal_cause_token doing exactly that. gunbc.heal_revalidation now derives the name from the arm and gunbc.ci_spec splices it.

Done for every HealOutcome / PriorRunDisposition arm the job prints, not just the new one — so the three sibling literals you named (HealNoChange, HealProduced, SupersededByHealedHead) are derived too, plus HealAuthorCommitRequired at both of its spellings. That included HealPushRefused, which this PR had itself introduced as a hand-spelled literal — the same defect, in the code written to fix it. It is now a real arm folding to PriorRunStillCurrent, since a push refused at a standing head supersedes nothing.

The control: the emitted witnesses.yml is byte-identical across the conversion (81469 bytes, empty diff). The derivation reproduces all six names exactly, so this changes authority and not output.

The annotation is narrowed regardless, as you asked, because "every token the job prints" would still overstate it: HealRepairDeclarationMissing is a step-integrity refusal belonging to the emitter's own protocol with no arm here, and it is left alone deliberately rather than pulled into the coproduct to make the sentence tidier. The claim now reads "every HealOutcome and PriorRunDisposition arm the job prints" and says what it excludes.

The string-contains witness is re-scoped to what it still discriminates. Its token half can no longer go red — that is §4b(4) dissolution on a climb — so it is annotated as a regression control that the construction stays in place, and the wall it still carries is the shape around the name: ordered adjacency of the exit 0, the hard-red twin, and the absence of any force/lease flag. That half still reddens (verified by flipping the arm's exit status).

2 — a row's status asserted in a foreign annotation. Correct. Nothing can read an annotation, and a status parked in another module rots away from the row that owns it. The claim is deleted from the annotation; the receipt is now written on gunbc.recurring_failure_mode.repair_job_red_is_attributed_to_the_content_it_repaired itself, recording that arm one leaves by a named arm, that the row stays open on arm two, and that the trigger's own words say why a one-arm fix is not sufficient. The combined markdown projection is not a committed merge surface (DESIGN), so there is no artifact to regenerate; the row renders correctly under tools.docs_projection_gate regen.

Witnesses re-run after the change: all four return true.

— sent from vivid-fox-409

[gunbai-bot]

Both findings in review 64162 verified and fixed in 26e3c78.

1 — the nickname and its collision. Correct. I took a different repair than the one suggested, because the collision names its own cause.

Spelling the arm out in heal_outcome_token ends the fork but leaves the log asymmetric: the job would print SupersededByHealedHead beside HealSupersededByAuthorHead for the same kind of statement. A supersede line answers what standing the prior head now has — that is PriorRunDisposition, and SupersededByHealedHead was already emitted from that fold. Sourcing its author-side twin from HealOutcome instead is what bought the short name and created the clash in the first place.

So both halves:

• each fold now maps every arm to its own spelling character for character (HealSupersededByAuthorHead in HealOutcome, SupersededByAuthorHead in PriorRunDisposition) — no token is recoverable to two arms;
• the notice line draws superseded_by_author_head_token from the disposition fold, where its sibling already lives.

The emitted witnesses.yml is unchanged (81469 bytes, empty diff): the log word and its symmetry survive, the fork does not.

2 — the hand-typed literal. Correct, and the sharper reading of it is that it was the copy that survives a rename and greens anyway. It consumes heal_push_refused_token now.

The wall your first finding implies, added. Nothing in a total match refuses two arms returning one string — both typecheck perfectly, which is exactly why this shipped past a fold that is otherwise closed. no_heal_token_names_two_arms asserts all eight tokens across both folds are pairwise distinct. It lives in the witness rather than in either fold because it is a property of the pair; each fold alone is blind to it.

Executed both directions: green as written, and false when the shipped nickname is restored (reverted). Rung stated honestly — mechanically preventable, not structural: a colliding spelling is still writable, and this witness is what refuses it.

Full sweep after the change: emission unchanged, all five witnesses return true.

— sent from vivid-fox-409

[gunbai-bot]

Thanks — taking the approval and not pushing over it, but one of your two non-findings is worth recording rather than leaving implicit, because it is a case of a test reading as more coverage than it carries.

You are right that count(all_tokens) == 8 is not an oracle violation (the universe is the test's own list, not a live population) and right that the exhaustive match is what catches a new arm with no token. The part worth stating plainly: all_tokens is a hand-built roster, so the disjointness wall covers collisions among the tokens listed there and is not a coverage guarantee over the coproducts. A new arm added with a token but not added to the roster passes silently — and the == 8 conjunct does not catch that either, since it only reds once someone has already extended the list. So that conjunct is a "you changed the roster deliberately" ratchet, not a completeness check, and I would rather it be read that way than as the wall.

The real wall against a missing token stays the exhaustive match, as you say. Deriving the roster from the arms is what would close the gap properly, and there is no reflection to do it with today, so it is a manual roster by construction rather than by oversight.

Not pushing a comment-only change over a green approval to say this — it is recorded here, and it belongs in the witness's annotation whenever that file is next opened for a substantive reason.

— sent from vivid-fox-409