Repository navigation
MAIN-H2: give heal's revalidation a head it can bind — workflow_dispatch input + preflight, and repoint ci_heal_dispatch off the deleted ci.yml - #10175
Conversation
…t, a preflight in every lane, and a dispatcher that names its emission A heal that repairs a branch pushes a new head H1 with the Actions job credential, and GitHub starts no run for that push. So H1 arrived carrying H0's receipts -- receipts about a tree that no longer exists -- and the job printed SupersededByHealedHead and exited nonzero, which is honest but is only a signal to a human. Nothing re-admitted H1. The modeled half of closing that already existed and was deliberately left unconsumed: #10118 refused to wire tools.ci_heal_dispatch because witnesses.yml declared no dispatch inputs, so a dispatched run could not check WHICH head it got -- it would have reported a verdict about a tree it cannot identify. That is a fabricated revalidation, worse than the honest gap. So the binding lands first here and the dispatch depends on it. THE BINDING. gunbc.witness_floor_workflow declares ci_heal_expected_healed_sha_input, projected into `on: workflow_dispatch: inputs:`. The ordinary checkout selects `${{ inputs.expected_healed_sha || github.sha }}`, and a preflight runs immediately after checkout in every ordinary-checkout lane, refusing unless BOTH github.sha and `git rev-parse HEAD` equal the expected head. Selection and comparison are different claims over two different races: `ref:` closes the window in which the branch advances between dispatch and checkout, and the github.sha comparison closes the earlier one, in which the branch advanced before GitHub resolved the ref into the run subject -- which would leave a run whose tree is H1 and whose CHECK is attached to H2. The script is v2.workflow.ci_heal_revalidation_preflight_emit, orchestration intent that was already modeled and had no consumer; it is not hand-authored yaml. An absent input is an ordinary manual dispatch and discharges no heal obligation. THE REPOINT. ci_heal_dispatch_workflow_id was the literal "ci.yml" -- a workflow the 2026-08-15 floor cut deleted -- for a fortnight, because a literal cannot go stale loudly. It now reads artifact_name(a: WitnessFloorYamlArtifact): the census is coproduct exhaustiveness, and swapping one literal for another would have closed a stale citation by authoring the next one. THE WIRE. The heal terminal invokes tools.ci_heal_dispatch inside the produced-a-heal arm, after the push and before the nonzero exit, because $HEALED_HEAD is a variable of that script. `actions: write` and GITHUB_TOKEN land WITH that consumer and nothing else widens. The job still exits nonzero: it judged the prior head and has no standing to speak for H1 whatever it dispatched. TWO DEFECTS FOUND BY READING THE EMISSION RATHER THAN TRUSTING IT, both now permanent arms. The invocation and the SupersededByHealedHead echo emitted on ONE line, and $ROOT is a per-step variable this step never stamped, so the composed invocation resolved to `/target/release/gunbc` -- a path that exists nowhere. gunbc_invoke_root_stamp_script now carries its own terminator so no caller can forget it. EVIDENCE. Ten witnesses in test.claim.heal_revalidation_binding_witness, all executed green. DISCRIMINATING RED, executed: deleting the preflight from prepared_bound_steps (four lanes lose it, rust-unit-tests keeps its own copy) reddened the per-lane adjacency row while the whole-file text row STAYED GREEN -- so those two rows are measured non-redundant, not assumed so -- with two other rows green as the positive control that the battery does not refuse everything. The mutation was reverted and the confirming regeneration reproduced the byte-identical tree digest. Regeneration is at a BYTE-grain fixed point (two rounds, identical digest over the full diff). v1_src_dag_parse: 4572 files parse-clean, citation debt 39 -- identical to origin/main's 39. NOT CLAIMED HERE, and it is the next receipt rather than this one: a live dispatched run. Dispatch acceptance is a queued run, never a verdict. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016dC4KDh8D8fTSaqpkfzBh8
…and dispatches a revalidation of the healed head Not a change to any authority. docs/plans/input-envelope-roadmap.md is a generated projection; this commit edits it WITHOUT regenerating, so the required generated-artifact phase sees drift and the heal job takes its auto-push arm. The subject was chosen against the emitted script rather than assumed: it carries a git add line and is absent from the AUTHOR_COMMIT_DRIFT population, so it exercises the PUSH arm rather than bundle-and-refuse. The heal job is expected to regenerate it, push a healed head H1, dispatch a revalidation of H1, and STILL exit nonzero. Predictions were recorded before this push. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016dC4KDh8D8fTSaqpkfzBh8
…hable from the production surface, not untested Both mismatch arms are emitted and both are asserted, but only the run-subject one has a live receipt, and a reader who found that out for themselves would reasonably read the other as an untested arm. It is not: the checkout is bound to the input, so if expected != github.sha the run-subject arm trips first, and if they are equal the checkout ref IS expected and HEAD cannot differ. Inducing it live means winning a force-push race against the runner's checkout, and making it dispatchable on demand would mean decoupling ref: from the input -- weakening the very selection that closes that race. A test runnable only by removing the protection is not a test worth having. So the disposition is defense-in-depth behind ref: selection, with the discriminating RED at the fixture boundary where the state IS authorable and IS authored, and this file's contribution named as the other half: that the comparison reached the emitted workflow rather than stopping at the model. Neither is a live receipt and neither is now described as one. The live receipts that DO exist are named by their producer rather than transcribed, including why the positive one is not decoration: a preflight that refused everything would satisfy the mismatched-sha arm permanently. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016dC4KDh8D8fTSaqpkfzBh8
… decompose the whole-file fold into two composed rows, and name what that cannot catch
FOUND BY EXECUTION, IN THE POSITIVE-ARM RUN ITSELF, not by review. Run 33706925651
required-witnesses-floor reported:
INTERRUPTED-BEFORE-VERDICT ...an_absent_input_is_an_ordinary_manual_dispatch_in_the_emitted_workflow
cpu_at_least=506ms/500ms
INTERRUPTED-BEFORE-VERDICT ...the_emitted_workflow_carries_both_mismatch_arms_and_the_pass_arm
cpu_at_least=503ms/500ms
Both called expected_witness_floor_yml(), which folds and serializes every job. BUDGET-REFUSED is
UNDECIDED -- not a weaker green, no verdict at all -- so the floor went red. My local timing showed
these rows near 1500ms and I read that as fine; it is not, against a budget I had not checked.
THE FIX IS A DECOMPOSITION, NOT A SHRINK, and the difference is what the annotation now argues.
The claim splits into two rows that compose to the same conclusion: the adjacency row already
proves this exact Step value is in every ordinary lane's job list, and a new row proves that Step's
own `run` carries both mismatch arms and the pass arm. The serializer copies that string verbatim
into the block scalar, so what the composition gives up is INDENTATION, not content.
WHAT THE COMPOSED PAIR CANNOT CATCH IS NAMED IN THE CARRIER rather than left for a reader to
discover, because from the outside this is indistinguishable from collapsing a check to fit its
transport. Both rows read the MODEL, so a serializer that DROPPED the step, emitted its `run` under
the wrong key, or produced a block scalar whose indentation changes how the shell parses would
leave both green. That blind spot is not hypothetical: workflow_dispatch_yaml discarded the ENTIRE
inputs list while the model carried it, the same class one field over. It is bounded by
the_required_workflow_declares_the_healed_sha_dispatch_input, which reads the PROJECTED YamlValue
-- but that covers the TRIGGER, not the steps, and the file does not claim otherwise.
BOUNDED BY MEASUREMENT, NOT BY TRIMMING UNTIL GREEN: 192ms and 200ms against the 500ms ceiling,
four-fold under rather than shaved to fit, so a later reader can tell a deliberate decomposition
from a check whittled down to pass. All ten rows execute green.
Also records the checkout-mismatch arm's disposition: unreachable from the production surface
rather than untested, because the checkout is bound to the input, so inducing it live would require
decoupling ref: from the input -- weakening the selection that closes that race.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016dC4KDh8D8fTSaqpkfzBh8
… a heal-pushed head is UNRELIABLE, not closed, and the attribution is unreadable from here
TWO OF THE THREE LIVE SPELLINGS OF THIS PREMISE WERE MINE, AUTHORED IN THIS PR. The claim that an
Actions-credential push starts no workflow run is carried on main at gunbc.ci_spec
gunbc_ci_heal_commit_push_script ("does not start a new workflow run") and inside gunbc.rung_drop
floor_cut_heal's trigger_fired ("An Actions-credential push starts no run"). I carried it forward
in the ci_spec rewrite and restated it fresh on gunbc.witness_floor_workflow
ci_heal_expected_healed_sha_input, in the present tense, without checking it -- and it is the
justification for the route this PR builds, so it is exactly the sentence that needed checking.
MEASURED, IT IS FALSE. Bot-authored `pull_request` runs DO appear on heal-pushed heads and most of
them execute: runs 33686753487 (head bc70468 -- gunbc#10118's OWN healed head, with
created_at == run_started_at, so zero approval delay), 33705120607 and 33703032560 all started;
only 33711005806 (head 958f743) came back action_required. Three of four. So "the repair
guarantees the block it was meant to clear" is a generalization from n=1 and is not written here.
THE REPLACEMENT IS WEAKER AND SUFFICIENT: the ordinary route is UNRELIABLE on a heal-pushed head --
it failed once for reasons unattributable from here -- and a remediator whose revalidation depends
on a gate nobody can attribute should not depend on it. That is why the dispatch is the DECLARED
path. A justification that overclaims dies to the next observation, and this one already did.
THE ONE CONTROL THAT DISCRIMINATES SURVIVES, AND IS KEPT ADJACENT TO ITS BOUND so a reader cannot
lift the pair without it: on the single sha 958f743, identity and token are constant (actor and
triggering_actor are github-actions[bot] on both) and only the EVENT varies -- 33711005806
(pull_request) was action_required while 33711101968 (workflow_dispatch) started and bound that
head in this very preflight. It shows the dispatch route was not blocked on a head where the
ordinary route happened to be; it does not generalize past that sha, which the four-run count
bounds.
ATTRIBUTION IS A DECLARED BOUNDARY OBLIGATION, UNDETERMINED BECAUSE UNREADABLE RATHER THAN
UNEXAMINED: actions/permissions and permissions/workflow both answer 403 Resource not accessible by
integration to the credential these sessions carry. Naming the 403 is the point -- unreadable names
its own remedy, unexamined names nothing.
The rung_drop clause is deliberately untouched: it is a retired row's historical record, a
different subject with its own review surface, and it is routed rather than repaired here.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016dC4KDh8D8fTSaqpkfzBh8
…nd keep the broken table as an instrument-failure row THE PREMISE WAS WRONG TWICE, IN OPPOSITE DIRECTIONS, AND BOTH ERRORS HAD ONE CAUSE: not holding created-and-held and never-created as separate states. That distinction is now at top billing on gunbc.witness_floor_workflow ci_heal_expected_healed_sha_input, with the reason it is load-bearing -- the two have different remedies (a held run has a release path, POST /actions/runs/<id>/approve; a nonexistent one has none), so a justification that cannot say which state it is in cannot say what the dispatch buys. MEASURED AT JOB GRAIN, THE BEHAVIOUR IS RELIABLE HOLDING, not the intermittent failure an earlier draft hedged against: a `pull_request` run IS created for the healed head and starts no job, 0 of 4 on attempt 1 across every heal push since gunbc#10118, and the single run that ever executed did so on attempt 2 after a release -- 1h47m from created_at to run_started_at. The hold keys on the EVENT, identity and token held constant on both arms. The measured populations live once, in gunbc.rung_drop floor_cut_heal, and are cited rather than restated. THE BROKEN TABLE IS KEPT AS A ROW RATHER THAN DELETED WITH THE CONCLUSION IT PRODUCED, because it is the sharpest specimen here of a proxy that fails toward the reading its reader wants -- and deleting it would delete the only evidence of why this wording moved twice. Both proxies are named with what they CANNOT SEE: `conclusion != action_required` cannot report "held" because a held run still concludes something (`failure` and `cancelled` are both in the table), and `created_at == run_started_at` cannot report "held" because equal timestamps are exactly what a run that never ran looks like. Neither has a state in which it says "this executed nothing", so neither was ever evidence about executing. Only attempt 1's JOB COUNT does, because zero is a value it can return. THE GENERALIZABLE RULE IS WRITTEN INTO THE CARRIER, not left in review: before accepting a refutation, ask what input would make the instrument report the other way. Read attempt 1, never the latest -- a human approving a held run leaves attempt 2 looking like an ordinary execution, which is exactly what hid the class. The attribution boundary is unchanged and still open: whether the hold follows from a repository setting is undetermined BECAUSE UNREADABLE -- actions/permissions and branches/main/protection both answer 403 to these sessions -- and the carrier states plainly that the dispatch closes the REVALIDATION gap (measured) and says nothing about the MERGE gate (unmeasured). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016dC4KDh8D8fTSaqpkfzBh8
…it, and leave the class's trigger honestly undetermined Three changes, each from a reading the first pass did not have. REVERT ci_spec. `gunbc.ci_spec` is held by #10175, which is re-examining the same premise; a second lane editing one premise from its own verdict is how one fact acquires two authorities. The annotation there still carries the refuted sentence on main, and the failure-mode row records that as an observation rather than repairing it. The repair is routed separately once #10175 lands. SCOPE, RATHER THAN ONLY CORRECT. A held run can be released, or re-run, and then judge the head -- one of the four eventually executed 6 jobs on a head heal had pushed. So "a head nothing judged" is true AT EXIT TIME and can stop being true with nobody touching anything. The exit is a claim by the run printing it about the moment it prints, never a standing property of the head. The row now says so, and states explicitly that the retirement itself stands: it retired on automatic repair of drift, observed, and revalidation was already declared not restored there -- the refuted mechanism was never its ground. THE INSTRUMENT, three levels deep and each invisible from the one above: a run's conclusion read as an execution receipt; then a job count taken on the wrong attempt; then a cross-attempt subtraction, because the run object's top-level created_at is attempt 1's while its run_started_at is attempt 2's -- two fields from two attempts, naming neither. The discriminator is not "count jobs", it is count jobs ON THE ATTEMPT THE CLAIM IS ABOUT, and the default endpoint silently answers for the latest. AND THE CLASS KEEPS AN UNDETERMINED TRIGGER. It is detectable only from outside the repository, since the refuting evidence lives in the external system, so no lens or witness reading this tree can reach it. Carrying the observation beside the claim is a necessary condition and is not known to be sufficient -- an observation of a system that changes without notice is a receipt about a past world, which is 4b's outside-the-modeled-guarantee column. Naming that row as the capability would be the artifact-for-capability substitution 4b(3) forbids. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01R422VRAe11vgYT3xNPsbQ5
…PR leaves the held path set warm-seal-35 holds three paths while gunbc#10106 gets a clean round; that lane has gone green on six consecutive heads and been knocked DIRTY before its aggregate finished every time, which is a lane that cannot converge while anything else lands in its paths. This PR touched two of the three. STRIPPING RATHER THAN DEFERRING, because the difference matters: gunbc.rung_drop floor_cut_heal lives inside a multi-kilobyte SINGLE-LINE blob, so two logically disjoint edits to that row collide TEXTUALLY and the generated-artifact merge driver refuses docs/design-rung-drops.md on top of it rather than resolving it. Sequencing three lanes onto one row still makes lanes two and three rebase into a conflict; removing a lane from the row means they never do. Both held paths are now byte-identical to origin/main, so this PR is out of the window entirely rather than waiting inside it. THE CLAUSE ITSELF IS NOT ABANDONED, it is handed to its sole lander. cool-koi-623 carries it into gunbc#10191 under the one-row-one-writer ruling, in the quote-and-append form that row's other correction already uses -- so the row does not quote one refuted sentence in place while silently replacing another. It is NOT reopened as a follow-up PR here; that would recreate the second writer the ruling exists to remove. AND IT COULD NOT HAVE LANDED TODAY IN THE FORM I WROTE. Measured by cool-koi-623 against main rather than against my description of it: the clause asserts that ci_heal_expected_healed_sha_input exists, that every ordinary-checkout lane selects and compares against it, and that the heal terminal invokes tools.ci_heal_dispatch -- and on main all three are absent, because they are this PR. A fix for a stale-tense sentence that is itself false in the tree it lands in is the same class one turn out: present tense is relative to the tree the sentence LANDS IN, not the tree the author is looking at. It carries on the merge of this PR, or as its own edit afterwards. No other path in this PR is affected; the dispatch binding, the preflight, the repoint and the witness battery are unchanged. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016dC4KDh8D8fTSaqpkfzBh8
…descent, used three times THE FINDING'S SUBSTANCE IS REAL AND IS FIXED. dispatch_input_is_declared_string folded a mapping's entries and matched every YamlValue variant, then did it again one level down and again below that -- forty lines whose actual subject was "descend three keys". That is now `yaml_key`, the descent named once and applied three times, with the predicate reading as the three keys it walks. THE FINDING'S PRESCRIPTION -- "route the query through a canonical YAML accessor" -- NAMES SOMETHING THAT DOES NOT EXIST, measured rather than assumed: extdeps.languages.yaml.types exports constructors (yaml_string, yaml_mapping, kv) and yaml_value_kind, and no lookup, getter or query of any kind. The only two carriers in the corpus with this shape are this file and the PRE-EXISTING test.claim.workflow_dispatch_input_witness on main, which hand-rolls the identical walk for the identical question. So the prescription reduces to "add an accessor to a shared extdeps module", which reaches lanes with no stake in this PR while it sits under a path hold. SO THE ACCESSOR IS LOCAL AND SAYS WHY, WITH ITS DISSOLUTION: its correct DESIGN section 3 home is beside the type it reads, and it collapses into that shared accessor the moment one exists -- taking the older triple-nested twin with it. WHAT IS DELIBERATELY NOT CHANGED, because the cheaper-reading form is the worse one. The leaf type check stays an EXHAUSTIVE match over a CLOSED coproduct, which is DESIGN section 4's own idiom, and Optional<YamlValue> is the honest shape of a lookup that can miss. A wildcard arm would read shorter and silently answer `false` when a YamlValue variant is added, instead of failing to compile -- the absorbing fallback section 5 forbids. EVIDENCE. All ten rows execute green. The reworked row reports 1712ms locally, which is NOT a cost this change introduced: the ~1.6s is the one-time witness_floor_workflow materialization paid by whichever row runs FIRST. Established by varying the order rather than by reading one number -- listed first it costs 1712ms and every_ordinary_checkout_lane costs 11ms; listed second it costs 0ms while that row pays 1644ms. The cost follows position, not the function. Regen exit 0, no projection drift, parse clean. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016dC4KDh8D8fTSaqpkfzBh8
|
Addressed in f30f18d. The substance is real and is fixed. The prescription names something that does not exist, measured rather than assumed:
So "route the query through a canonical YAML accessor" reduces to add an accessor to a shared Two things deliberately unchanged, because the cheaper-reading form is the worse one. The leaf type check stays an exhaustive match over a closed coproduct — DESIGN §4's own idiom — and On the cited authority. The finding grounds itself in "the ctrl review policy, not a Evidence. All ten rows execute green. The reworked row reports 1712ms locally; that is not a cost this change introduced. The ~1.6s is the one-time — sent from fierce-ram-670 |
Three heal_revalidation_binding_witness rows exceeded the floor's per-claim CPU ceiling on check 100530537497 -- one hard FAIL on the shared-fill guard, two INTERRUPTED-BEFORE-VERDICT at 505ms and 515ms, all three naming bash_fold_serialize_node. The previous attempt split the whole-file rows in two, which halved the population and left the cost shape untouched: each half landed nearer the line by coincidence of size, one emitted line from red. Measured with claim_batch --functions, one witness per subject, so the cost is denominated in what each row actually demands rather than in how many rows fit under the ceiling. Every one of the six lane jobs costs about 220ms; the assembled workflow costs 1569ms; required_lanes_aggregate_job alone costs 1353ms of it. That job checks out nothing and runs no witness -- its `run` is the serialized gunbc.required_lanes_gate program, the largest bash AST the workflow carries, and no row in this file says anything about it. A record is materialized whole, so asking `witness_floor_workflow` whether it declares a dispatch input was paying a second and a third to serialize a gate script. So the demand graph is minimized before its answers are materialized, per DESIGN section 2: witness_floor_triggers and witness_floor_lane_jobs are named as the parts witness_floor_workflow is assembled from, and the three rows read the part each one is about. Neither is a second authority -- the workflow is built from exactly these, so a lane added there is a lane in the emitted yaml and the "every witness-bearing lane" universal still covers it by construction. The aggregate is deliberately not a member: it joined that population only as something the checkout filter removed again. the_required_workflow_declares_the_healed_sha_dispatch_input 505ms -> 3ms the_heal_job_carries_no_revalidation_preflight 515ms -> 291ms every_ordinary_checkout_lane_preflights_before_its_first_... FAIL -> 409ms The right-hand figures are local; this container measured the same aggregate fill at 1353ms that CI measured at 497ms, so it runs about 3x slower than the runner and 409ms here is the largest row. All ten rows PASS. The regenerated .github/workflows/witnesses.yml is byte-identical, which is the control that this is demand minimization and not a change to what CI runs. cargo fmt clean; v1_src_dag_parse 4584 files parse-clean, citation debt 39, unmoved. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016dC4KDh8D8fTSaqpkfzBh8
The paragraph landed with beb4dde said the six lane jobs cost "about 220ms against a 210ms floor for reaching this module at all". There is no such floor. It was inferred from a first probe in which all six per-job subjects landed in one narrow band -- but a band across six readers is evidence of work SHARED BETWEEN them, never of a cost beneath them, and only a reader that touches almost nothing can tell those two apart. The refutation is a row in this same change: the_required_workflow_declares_the_healed_sha_dispatch_input reads witness_floor_triggers and nothing else, and costs 3ms on the same instrument that produced the band. A distribution is not a floor; the way to find one is to measure the cheapest possible reader rather than infer it from the parts that happen to be expensive. It is the wrong-subject move one layer down from the one it was correcting, and it mattered because a future author pricing a witness against this carrier would have read it as saying a cheap reader is impossible -- while the row that settles the question is a cheap reader sitting in the same commit. The bare millisecond figures go with it, in both carriers. They were taken in a session container that priced the aggregate's fill at three times what the runner priced the same fill at on check 100530537497, so the proportion transfers and the absolute numbers do not: a figure from here reads as a safety margin to anyone who does not know which machine produced it. The claim is now the shape -- one job is about seven eighths of the assembled workflow's cost, the six lane jobs together are the remaining eighth -- with the instrument named rather than its output transcribed. Annotation-only, and the control holds: a full main_wet regenerates every artifact and git reports only these two .dag files, so no emitted byte moves. cargo fmt clean; v1_src_dag_parse 4584 files parse-clean, citation debt 39. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016dC4KDh8D8fTSaqpkfzBh8
…thorities The branch did not merge. `git merge-tree --write-tree origin/main HEAD` returned rc=1 with GeneratedArtifactConcurrentDivergence on docs/design-rung-drops.md: both sides changed that generated projection since merge base 770cde7, so neither side's bytes were the projection of the merged authorities. WHAT MADE IT DANGEROUS IS THAT THERE WAS NO CONTENT CONFLICT. The branch and main hold BYTE-IDENTICAL bytes for the dashboard_merge_ready_semantic_admissibility row -- same sha256 on both sides. A plain text merge collapses an identical addition and looks clean, and GitHub does not run our merge driver, so the result would have projected neither side's authorities with nothing to say so. That is the specimen recorded inside that very row: a mechanically clean merge whose semantic answer is Refused. It was found by running the decidable instrument rather than reading a diff name listing, which is also the reason an earlier report of mine was wrong -- I reported the held-path set from what I had STRIPPED rather than from what the branch WROTE, and those are different questions. Resolved as the driver's own diagnostic sanctions: not by picking a side. The compiler was rebuilt from the merged tree FIRST, because the merge carries 23 changed src/ files and regenerating with a binary that predates them writes bytes no authority backs. Then main_wet regenerated every artifact. The regenerated projection carries 27 sections -- our 24 plus the three main declared on 2026-09-03 -- and is byte-identical to main's file, which is the expected result precisely because our only row here was already identical to one main holds. Controls, re-verified on the merged tree rather than carried over: .github/workflows/witnesses.yml is byte-identical across the merge and the regeneration, so the floor-cost argument is untouched. cargo fmt clean; v1_src_dag_parse 4589 files parse-clean, citation debt 39. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016dC4KDh8D8fTSaqpkfzBh8
…l calls the withdrawn rows measured-out Recomposed onto current main (db3caed), which moved through #10166's parser/occurrence-binding change and #10175's witness/heal machinery since this PR's last receipt. Compiler and resolution movement is material even with zero path overlap, so the prior exact-head CI no longer speaks for this tree. The recomposition also surfaces a contradiction that would have landed silently. #10181 landed a memo whose plays table says serving the shared producer across claim frames is "measured and refused", citing the same three rows this PR reclassifies as UNMEASURED. After a merge, main would carry both sentences about one subject -- a §3 meaning fork, and the more dangerous half is the memo, because a negative result is exactly the artifact a later lane cites to decide NOT to try something. Both statements were true of different serves, which is the whole point, so the repair is to say which serve each priced rather than to delete either: measured and refused AGAINST #10094's O(size) serve -- historical, still valid as that; this PR fires their re-enrol trigger, so their CURRENT state is UNMEASURED, neither admitted nor measured-out, pending a controlled present/absent pair nobody has run. That keeps the memo's conclusion (the emit near-ceiling family is not a defect) intact -- it does not rest on those three rows staying excluded -- while removing the sentence that would have let a future lane read a stale exclusion as a standing measurement. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LhF5WCbZqrZHPqsnjpkYu
…mechanism is false, and the clause needed scoping (#10191) * heal: the SupersededByHealedHead exit is right and the mechanism it was justified by is false `gunbc.rung_drop` `floor_cut_heal` and the annotation above `gunbc.ci_spec` `gunbc_ci_heal_commit_push_script` both said an Actions-credential push starts no workflow run. Measured over the whole heal-push population since #10118 restored the job (n=4), a pull_request run was CREATED 4 times out of 4. What GitHub withholds is EXECUTION: 0 of the 4 started a single job on the triggering attempt. The conclusion those carriers drew stands unchanged -- no executed verdict exists for the healed head, so heal exits nonzero rather than speak for a tree it produced. The mechanism does not, and what it concealed is the point: a HELD judge is not an ABSENT one, so the release is an approve on that specific held run rather than a re-run, and a dispatched revalidation is a second run on that head rather than the only one. The other arm is measured two-sided with the identity held constant: 0 of 500 workflow_dispatch runs held, and the entire action_required listing is event=pull_request. The hold keys on the EVENT, not the identity or the token, so the dispatched run is the only route to the healed head that executes without a human -- the second-run cost buys something measured rather than duplicating a run that would have happened anyway. Not established, and not written as if it were: whether a dispatched run's contexts clear branch protection, which is 403 to this token. The rung_drop row is ANNOTATED, not rewritten: the refuted sentence is quoted in place, and the row states that the correction moves no rung and un-retires nothing, since the capability it retired on is automatic repair and revalidation was already declared not restored there. One count, one home: ci_spec cites the row rather than restating the numbers. Files `external_mechanism_asserted_under_a_correct_conclusion` per section 4b(1). The class is the immunised variety of silent wrongness -- a mechanism about external reality asserted as the reason for a conclusion that is independently correct, so every test of the conclusion confirms the premise by association and nothing the repository can execute refutes it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01R422VRAe11vgYT3xNPsbQ5 * Scope the corrected clause to exit time, revert the fenced ci_spec edit, and leave the class's trigger honestly undetermined Three changes, each from a reading the first pass did not have. REVERT ci_spec. `gunbc.ci_spec` is held by #10175, which is re-examining the same premise; a second lane editing one premise from its own verdict is how one fact acquires two authorities. The annotation there still carries the refuted sentence on main, and the failure-mode row records that as an observation rather than repairing it. The repair is routed separately once #10175 lands. SCOPE, RATHER THAN ONLY CORRECT. A held run can be released, or re-run, and then judge the head -- one of the four eventually executed 6 jobs on a head heal had pushed. So "a head nothing judged" is true AT EXIT TIME and can stop being true with nobody touching anything. The exit is a claim by the run printing it about the moment it prints, never a standing property of the head. The row now says so, and states explicitly that the retirement itself stands: it retired on automatic repair of drift, observed, and revalidation was already declared not restored there -- the refuted mechanism was never its ground. THE INSTRUMENT, three levels deep and each invisible from the one above: a run's conclusion read as an execution receipt; then a job count taken on the wrong attempt; then a cross-attempt subtraction, because the run object's top-level created_at is attempt 1's while its run_started_at is attempt 2's -- two fields from two attempts, naming neither. The discriminator is not "count jobs", it is count jobs ON THE ATTEMPT THE CLAIM IS ABOUT, and the default endpoint silently answers for the latest. AND THE CLASS KEEPS AN UNDETERMINED TRIGGER. It is detectable only from outside the repository, since the refuting evidence lives in the external system, so no lens or witness reading this tree can reach it. Carrying the observation beside the claim is a necessary condition and is not known to be sufficient -- an observation of a system that changes without notice is a receipt about a past world, which is 4b's outside-the-modeled-guarantee column. Naming that row as the capability would be the artifact-for-capability substitution 4b(3) forbids. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01R422VRAe11vgYT3xNPsbQ5 * Review fix: the class ranks an in-repo authoring act, so it gets a derived ceiling and a named trigger codex/gpt-5.6-sol requested changes on the new failure-mode row, and the objection is correct: the row assigned a ladder rung and a ceiling to EXTERNAL REALITY, which §4b deliberately keeps off the ladder, and then declined to name a next-rung trigger while its own text conceded the separation "CAN climb" -- the untracked stall §4b(2) forbids. The repair runs opposite to the suggested one, and that is the substance rather than a quibble. The class's subject is not the external system; it is an AUTHORING ACT wholly inside this tree -- a carrier stating an unobserved mechanism as the reason for a decision. That is decidable by reading the carrier, so it ranks and is obligated to climb. Modelling it as a boundary obligation would have moved a rankable in-repository defect off the ladder, which is the same mistake the row already had, one step further along. So the row now splits two axes with different decidability: (i) THE SEPARATION -- is the mechanism claim backed by an observation? Decidable from the carrier. CEILING 4, derived: if the only construction able to express an external-system mechanism requires the observation that produced it, an unbacked claim has no constructor. Anything below 4 is a correctness gap, not a ceiling. The rung found at 1 is scoped here. (ii) THE TRUTH of the external fact -- outside the modeled guarantee, not a rung and never one, named explicitly so it cannot be mistaken for a weak implementation that should climb. TRIGGER FOR (i), a capability and not an artifact: the typed observation-carrying construction PLUS a consumer that enumerates carriers making such a claim without one. The pairing is the whole trigger -- the construction alone makes the honest form available; only the enumerating consumer makes the dishonest form unwritable rather than noticed once. §4c decides where it cannot live: semantic passes see only the annotation-erased projection, so this can never be an annotation. The asymmetry that made the class look unrankable is kept, correctly placed: the defect is visible from inside the tree, the refutation only from outside. That is why it survives review, not why it cannot climb. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01R422VRAe11vgYT3xNPsbQ5 --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
…recorded margin (#10205) Three things the margins showed once #10175 had landed and the floor logs unlocked. All ten rows pass; two sat at 392ms of a 500ms ceiling. THE CALIBRATION SENTENCE ON MAIN WAS FALSE AND IS THE URGENT HALF. The carrier said the session container runs about three times the runner. That was derived by dividing a local figure by CI's marginal_cpu_ns=496786520 -- a fill that had been INTERRUPTED AT THE BUDGET. An interrupted measurement is not a slow measurement; it is a non-measurement wearing a number, and the number it wears is approximately the ceiling that stopped it, so the ratio described the ceiling rather than the machine. It reads as data because it has units, which is the same shape as budget-refused being UNDECIDED rather than a weak green. The consequence was not cosmetic: the next author pricing a witness against that sentence would have concluded they had three times the room they have. The method that refutes it is the same-row comparison, and only that method could: 409ms local against 392ms on runner srv4-04 at check 100560747021 for the adjacency row, while a sibling measured cheaper locally than on the runner, so the runner is not uniformly faster in either direction. A cross-row ratio cannot see that. eval_steps is now cited as the portable quantity -- 148297 for that row -- because steps are host-independent where milliseconds are not. the_heal_job_carries_no_revalidation_preflight ASKED ABOUT ONE JOB AND PAID FOR SIX. It reached the heal job by folding witness_floor_lane_jobs looking for an id, materializing all six lanes and their emitted bash to answer a question about one of them -- the same defect #10175 fixed, in miniature. It now names heal_generated_artifacts_job() directly. That also deletes job_by_id, whose only caller this was, and the Absent arm, which existed only because a search can miss and could never fire against a list the workflow is assembled from. Locally 291ms -> 233ms; the remainder is the heal job itself, which carries the largest script in the workflow, so the row now costs what its subject costs. every_ordinary_checkout_lane_preflights_before_its_first_witness KEEPS ITS COST AND GETS ITS MARGIN RECORDED. Its subject IS the six lanes; a roster-backed version would be a worse artifact at any price, since a roster stops being a denominator the moment someone adds a lane. The modelled alternative was checked rather than assumed and is NOT available: required_floor_claim_cpu_- safety_limit_ms is a single constant not keyed by identity, so no row can be given its own ceiling; the interpreter's remedy sentence asks for a lane that declares a dated ceiling AND names the row as an executing consumer; and gunbc.fleet.fleet_converge_plan records that no such lane exists that executes anything, relocation into a non-executing home being the bare de-enrollment the admission ruling forbids. That work is filed at node://adhoc-cfdf3366-bc3 and is named in the carrier as this margin's trigger. Until it lands the margin is 108ms on the named runner, recorded so the next author meets a known bound rather than discovering a red. Annotation and witness-subject only: a full main_wet leaves .github/workflows/witnesses.yml byte-identical (sha256 checked before and after) and git reports only these two .dag files. cargo fmt clean; v1_src_dag_parse 4593 files parse-clean, citation debt 39. Claude-Session: https://claude.ai/code/session_016dC4KDh8D8fTSaqpkfzBh8 Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
The gap
A heal that repairs a branch pushes a new head H1 with the Actions job credential, and GitHub creates a
pull_requestrun for that push and then withholds its execution — 4/4 created, 0/4 started a single job on attempt 1 (see Executed receipts). So nothing judges H1, and it arrived carrying H0's receipts, receipts about a tree that no longer exists.Created-and-held is not never-created, and the distinction is load-bearing: a held run has a release path (
POST /actions/runs/<id>/approve) and a nonexistent one does not. The job printedSupersededByHealedHeadand exited nonzero, which is honest, but it is only a signal to a human reading a red job. Nothing re-admitted H1.The modeled half of closing that already existed and was deliberately left unconsumed. #10118 refused to wire
tools.ci_heal_dispatchbecausewitnesses.ymldeclared no dispatch inputs, so a dispatched run could not check which head it got — it would have reported a verdict about a tree it cannot identify. That is a fabricated revalidation, worse than the honest gap. Andci_heal_dispatch_workflow_idread the literal"ci.yml", a workflow the 2026-08-15 floor cut deleted: the dispatcher pointed at a file with no existence, and for a fortnight nothing said so.So the binding lands first here, and the dispatch depends on it.
What this builds
1 — the binding.
gunbc.witness_floor_workflowdeclaresci_heal_expected_healed_sha_input, projected intoon: workflow_dispatch: inputs:. The ordinary checkout selects${{ inputs.expected_healed_sha || github.sha }}, and a preflight step runs immediately after checkout in every ordinary-checkout lane, refusing unless bothgithub.shaandgit rev-parse HEADequal the expected head.Selection and comparison are different claims over two different races, and both are kept separately authorable:
expected != github.shaexpected != git rev-parse HEADA preflight carrying only the first passes the second while the job builds the wrong tree. The script is
v2.workflow.ci_heal_revalidation_preflight_emit— orchestration intent that was already modeled and had no consumer — so the refusal arms are modeled control flow, not hand-authored YAML. An absent input is an ordinary manual dispatch and discharges no heal obligation; a hand-triggered run cannot impersonate a revalidation.2 — the repoint.
ci_heal_dispatch_workflow_idnow readsartifact_name(a: WitnessFloorYamlArtifact). Deleting that variant would refuse this module at compile time; swapping"ci.yml"for"witnesses.yml"would have closed a stale citation by authoring the next one.3 — the wire. The heal terminal invokes
tools.ci_heal_dispatchinside the produced-a-heal arm, after the push and before the nonzero exit, because$HEALED_HEADis a variable of that script.actions: writeandGITHUB_TOKENland with that consumer and nothing else widens. The job still exits nonzero, deliberately — it judged the prior head and has no standing to speak for H1 whatever it dispatched. H1 earns its own admission; H0's verdict is not rewritten.The heal job carries no preflight: it checks out the triggering branch head in order to produce a healed one, and binding that checkout would refuse the job that creates the subject. And heal is not added to the required aggregate's
needs:.Two defects found by reading the emission rather than trusting it
Both are now permanent arms in the battery:
SupersededByHealedHeadecho emitted on one line — the echo would have become argv ofgunbc;$ROOTis a per-step variable and this step never stamped it, so the composed invocation resolved to/target/release/gunbc, a path that exists nowhere. The dispatch would never have run.gunbc_invoke_root_stamp_scriptnow carries its own terminator so no caller can forget it.The emitted YAML looked entirely plausible in both cases, which is the shape a witness is for.
Evidence
Ten witnesses in
test.claim.heal_revalidation_binding_witness, all executed green.Discriminating RED, executed. Deleting the preflight from
prepared_bound_steps(four lanes lose it,rust-unit-testskeeps its own copy) reddened the per-lane adjacency row — and the whole-file text row stayed green, because one surviving lane keeps every one of those strings somewhere in the file. So those two rows are measured non-redundant rather than assumed so, and that measurement is recorded in the annotation above them. Two other rows stayed green as the positive control that the battery does not refuse everything. The mutation was reverted and the confirming regeneration reproduced the byte-identical tree digest.v1_src_dag_parse: 4572 files parse-clean, citation debt 39 — identical toorigin/main's 39.Executed receipts
Predictions were written down before every run.
Refusal arm — run 33706912902, dispatched with a stale SHA. All four ordinary-checkout lanes failed at step 4; every adjudicating step after it skipped, including
Required CI: witnesses laneand all five uploads.Exactly one arm fired. The checkout arm stayed silent because
ref:selection had already put HEAD at the expected SHA — the two-race split visible in a single run.Positive arm — run 33706925651, same step, same code path: all four lanes
step4=success, proceeding into the machinery; three fully green end to end.This arm is mandatory, not decoration: a preflight that refused everything would satisfy the refusal arm permanently and is only ruled out by this.
End to end — run 33709653544, heal job:
Exactly one changed path, no blast radius. The POST went to
witnesses.yml— the workflow the variant derives; the literal it replaced would have POSTed atci.yml, a file that does not exist. That is the repoint demonstrated rather than argued. H0's verdict was not rewritten: the job still exits nonzero, after the dispatch rather than instead of it.Run 33711101968 —
event=workflow_dispatch,headSha=958f743f9e= H1, created one second after the POST — bound the healed head in its preflight.That closes the revalidation gap, and deliberately claims nothing about the merge gate. The ordinary
pull_requestrun on a healed head is created and then held: measured across every heal push since #10118, 4/4 created and 0/4 started a single job on attempt 1. The hold keys on the event, not the identity — 0 of 500 sampledworkflow_dispatchruns areaction_required(151 of them under the same bot), while all 17action_requiredruns in the repo arepull_request. But releasing a held run isPOST /actions/runs/<id>/approveon that run, andbranches/main/protectionis 403 to these sessions, so whether a dispatched green clears protection is unmeasured. The measured populations are owned bygunbc.rung_dropfloor_cut_heal; this PR's carrier cites them rather than restating them.The probe netted to zero by machine, not by hand: the healed file is byte-identical to the target derived locally before the run, and its diff against main is empty.
One defect this found, in my own change
Two witnesses called
expected_witness_floor_yml()and BUDGET-REFUSED the floor's 500ms CPU ceiling at 503ms and 506ms, goingINTERRUPTED-BEFORE-VERDICT— undecided is no verdict, so the floor went red. Fixed by decomposing the whole-file fold into two composed rows (192ms / 200ms — four-fold under, not shaved to fit), with what the pair cannot catch named in the carrier: both read the model, so a dropped step or a mangled block scalar would leave them green. That blind spot is not hypothetical —workflow_dispatch_yamlonce discarded the entire inputs list while the model carried it.Still not claimed
The checkout-mismatch arm has no live receipt and is not live-authorable through the production surface: checkout is bound to the input, so
expected != github.shatrips the run-subject arm first andexpected == github.shaforces HEAD to equal it. Inducing it means winning a force-push race; making it dispatchable would mean decouplingref:from the input — weakening the selection that closes that race. Its discriminating RED runs at the fixture boundary instead. The carrier says this, so a later reader sees an unreachable arm rather than an untested one.🤖 Generated with Claude Code
https://claude.ai/code/session_016dC4KDh8D8fTSaqpkfzBh8