diff --git a/.github/workflows/witnesses.yml b/.github/workflows/witnesses.yml index e9784fecc0c..54436de6755 100644 --- a/.github/workflows/witnesses.yml +++ b/.github/workflows/witnesses.yml @@ -3,6 +3,11 @@ name: witnesses on: workflow_dispatch: + inputs: + expected_healed_sha: + description: Immutable healed commit required by an auto-heal revalidation run + required: false + type: string merge_group: push: branches: [main] @@ -43,6 +48,23 @@ jobs: uses: actions/checkout@v5 with: fetch-depth: 0 + ref: ${{ inputs.expected_healed_sha || github.sha }} + - name: Refuse a heal revalidation whose run subject or checkout does not name the expected healed SHA + run: | + EXPECTED_HEALED_SHA="${{ inputs.expected_healed_sha }}" + RUN_SUBJECT_HEAD="${{ github.sha }}" + if [ -n "$EXPECTED_HEALED_SHA" ]; then + ACTUAL_HEAD="$(git rev-parse HEAD)" + if ! [ "$RUN_SUBJECT_HEAD" = "$EXPECTED_HEALED_SHA" ]; then + echo "::error::heal revalidation refused: workflow run subject $RUN_SUBJECT_HEAD does not equal expected healed head $EXPECTED_HEALED_SHA" + exit 1 + fi + if ! [ "$ACTUAL_HEAD" = "$EXPECTED_HEALED_SHA" ]; then + echo "::error::heal revalidation refused: checkout head $ACTUAL_HEAD does not equal expected healed head $EXPECTED_HEALED_SHA" + exit 1 + fi + echo "heal revalidation preflight: checkout names expected healed head $EXPECTED_HEALED_SHA" + fi - name: Isolate toolchain homes run: | # dissolve-on: ci_toolchain_home_isolation_script -- orch-emitted foreign-executor prelude step wiping and setting HOME/CARGO_HOME/RUSTUP_HOME under RUNNER_TEMP so concurrent runner slots stop sharing one toolchain; leaf rm/echo strings remain until a typed per-job filesystem-and-environment effect lands on host_effect_apply (shell-to-intent Phase 2). This obligation covers THIS carrier and ci_isolate_toolchain_script, which share that terminal construction; ci_pin_rustup_default_script carries its own obligation because it does not @@ -109,6 +131,23 @@ jobs: uses: actions/checkout@v5 with: fetch-depth: 0 + ref: ${{ inputs.expected_healed_sha || github.sha }} + - name: Refuse a heal revalidation whose run subject or checkout does not name the expected healed SHA + run: | + EXPECTED_HEALED_SHA="${{ inputs.expected_healed_sha }}" + RUN_SUBJECT_HEAD="${{ github.sha }}" + if [ -n "$EXPECTED_HEALED_SHA" ]; then + ACTUAL_HEAD="$(git rev-parse HEAD)" + if ! [ "$RUN_SUBJECT_HEAD" = "$EXPECTED_HEALED_SHA" ]; then + echo "::error::heal revalidation refused: workflow run subject $RUN_SUBJECT_HEAD does not equal expected healed head $EXPECTED_HEALED_SHA" + exit 1 + fi + if ! [ "$ACTUAL_HEAD" = "$EXPECTED_HEALED_SHA" ]; then + echo "::error::heal revalidation refused: checkout head $ACTUAL_HEAD does not equal expected healed head $EXPECTED_HEALED_SHA" + exit 1 + fi + echo "heal revalidation preflight: checkout names expected healed head $EXPECTED_HEALED_SHA" + fi - name: Isolate toolchain homes run: | # dissolve-on: ci_toolchain_home_isolation_script -- orch-emitted foreign-executor prelude step wiping and setting HOME/CARGO_HOME/RUSTUP_HOME under RUNNER_TEMP so concurrent runner slots stop sharing one toolchain; leaf rm/echo strings remain until a typed per-job filesystem-and-environment effect lands on host_effect_apply (shell-to-intent Phase 2). This obligation covers THIS carrier and ci_isolate_toolchain_script, which share that terminal construction; ci_pin_rustup_default_script carries its own obligation because it does not @@ -214,6 +253,23 @@ jobs: uses: actions/checkout@v5 with: fetch-depth: 0 + ref: ${{ inputs.expected_healed_sha || github.sha }} + - name: Refuse a heal revalidation whose run subject or checkout does not name the expected healed SHA + run: | + EXPECTED_HEALED_SHA="${{ inputs.expected_healed_sha }}" + RUN_SUBJECT_HEAD="${{ github.sha }}" + if [ -n "$EXPECTED_HEALED_SHA" ]; then + ACTUAL_HEAD="$(git rev-parse HEAD)" + if ! [ "$RUN_SUBJECT_HEAD" = "$EXPECTED_HEALED_SHA" ]; then + echo "::error::heal revalidation refused: workflow run subject $RUN_SUBJECT_HEAD does not equal expected healed head $EXPECTED_HEALED_SHA" + exit 1 + fi + if ! [ "$ACTUAL_HEAD" = "$EXPECTED_HEALED_SHA" ]; then + echo "::error::heal revalidation refused: checkout head $ACTUAL_HEAD does not equal expected healed head $EXPECTED_HEALED_SHA" + exit 1 + fi + echo "heal revalidation preflight: checkout names expected healed head $EXPECTED_HEALED_SHA" + fi - name: Isolate toolchain homes run: | # dissolve-on: ci_toolchain_home_isolation_script -- orch-emitted foreign-executor prelude step wiping and setting HOME/CARGO_HOME/RUSTUP_HOME under RUNNER_TEMP so concurrent runner slots stop sharing one toolchain; leaf rm/echo strings remain until a typed per-job filesystem-and-environment effect lands on host_effect_apply (shell-to-intent Phase 2). This obligation covers THIS carrier and ci_isolate_toolchain_script, which share that terminal construction; ci_pin_rustup_default_script carries its own obligation because it does not @@ -274,6 +330,23 @@ jobs: uses: actions/checkout@v5 with: fetch-depth: 0 + ref: ${{ inputs.expected_healed_sha || github.sha }} + - name: Refuse a heal revalidation whose run subject or checkout does not name the expected healed SHA + run: | + EXPECTED_HEALED_SHA="${{ inputs.expected_healed_sha }}" + RUN_SUBJECT_HEAD="${{ github.sha }}" + if [ -n "$EXPECTED_HEALED_SHA" ]; then + ACTUAL_HEAD="$(git rev-parse HEAD)" + if ! [ "$RUN_SUBJECT_HEAD" = "$EXPECTED_HEALED_SHA" ]; then + echo "::error::heal revalidation refused: workflow run subject $RUN_SUBJECT_HEAD does not equal expected healed head $EXPECTED_HEALED_SHA" + exit 1 + fi + if ! [ "$ACTUAL_HEAD" = "$EXPECTED_HEALED_SHA" ]; then + echo "::error::heal revalidation refused: checkout head $ACTUAL_HEAD does not equal expected healed head $EXPECTED_HEALED_SHA" + exit 1 + fi + echo "heal revalidation preflight: checkout names expected healed head $EXPECTED_HEALED_SHA" + fi - name: Isolate toolchain homes run: | # dissolve-on: ci_toolchain_home_isolation_script -- orch-emitted foreign-executor prelude step wiping and setting HOME/CARGO_HOME/RUSTUP_HOME under RUNNER_TEMP so concurrent runner slots stop sharing one toolchain; leaf rm/echo strings remain until a typed per-job filesystem-and-environment effect lands on host_effect_apply (shell-to-intent Phase 2). This obligation covers THIS carrier and ci_isolate_toolchain_script, which share that terminal construction; ci_pin_rustup_default_script carries its own obligation because it does not @@ -335,6 +408,23 @@ jobs: uses: actions/checkout@v5 with: fetch-depth: 0 + ref: ${{ inputs.expected_healed_sha || github.sha }} + - name: Refuse a heal revalidation whose run subject or checkout does not name the expected healed SHA + run: | + EXPECTED_HEALED_SHA="${{ inputs.expected_healed_sha }}" + RUN_SUBJECT_HEAD="${{ github.sha }}" + if [ -n "$EXPECTED_HEALED_SHA" ]; then + ACTUAL_HEAD="$(git rev-parse HEAD)" + if ! [ "$RUN_SUBJECT_HEAD" = "$EXPECTED_HEALED_SHA" ]; then + echo "::error::heal revalidation refused: workflow run subject $RUN_SUBJECT_HEAD does not equal expected healed head $EXPECTED_HEALED_SHA" + exit 1 + fi + if ! [ "$ACTUAL_HEAD" = "$EXPECTED_HEALED_SHA" ]; then + echo "::error::heal revalidation refused: checkout head $ACTUAL_HEAD does not equal expected healed head $EXPECTED_HEALED_SHA" + exit 1 + fi + echo "heal revalidation preflight: checkout names expected healed head $EXPECTED_HEALED_SHA" + fi - name: Isolate toolchain homes run: | # dissolve-on: ci_toolchain_home_isolation_script -- orch-emitted foreign-executor prelude step wiping and setting HOME/CARGO_HOME/RUSTUP_HOME under RUNNER_TEMP so concurrent runner slots stop sharing one toolchain; leaf rm/echo strings remain until a typed per-job filesystem-and-environment effect lands on host_effect_apply (shell-to-intent Phase 2). This obligation covers THIS carrier and ci_isolate_toolchain_script, which share that terminal construction; ci_pin_rustup_default_script carries its own obligation because it does not @@ -381,7 +471,7 @@ jobs: if: github.event_name == 'pull_request' && github.event.pull_request.head.repo.full_name == github.repository && github.actor != 'dependabot[bot]' permissions: contents: write - actions: none + actions: write steps: - name: Checkout triggering branch head (heal pushes the regeneration back to this branch) uses: actions/checkout@v5 @@ -422,6 +512,7 @@ jobs: - name: Commit and push the regeneration id: heal_commit_push run: | + ROOT=$(git rev-parse --show-toplevel 2>/dev/null || pwd) git config user.name "gunbc-ci-auto-heal" git config user.email "gunbc-ci-auto-heal@users.noreply.github.com" AUTHOR_COMMIT_DRIFT="" @@ -484,12 +575,15 @@ jobs: HEALED_HEAD=$(git rev-parse HEAD) git -c core.hooksPath= push origin HEAD:${{ github.head_ref || github.ref_name }} echo "HealProduced prior_head=$PRIOR_HEAD healed_head=$HEALED_HEAD changed_artifacts=$CHANGED_ARTIFACTS" + GUNBC_HEALED_HEAD="$HEALED_HEAD" GUNBC_HEAL_BRANCH_REF="${{ github.head_ref || github.ref_name }}" "$ROOT/target/release/gunbc" run --source-root "$ROOT/dag" --source-root "$ROOT/src/v2" --entry dag/gunbc/instruments/ci_heal_dispatch.dag --function main echo "SupersededByHealedHead prior_head=$PRIOR_HEAD healed_head=$HEALED_HEAD; revalidation-required" if [ -n "$AUTHOR_COMMIT_DRIFT" ]; then echo "::error::HealAuthorCommitRequired head=$HEALED_HEAD author_commit_paths=$AUTHOR_COMMIT_DRIFT cause=ActionsJobCredentialScopeUnavailable regen_command='gunbc run --source-root dag --source-root src/v2 --entry dag/gunbc/instruments/generated_artifact_gate.dag --function main_wet'" >&2 fi exit 1 fi + env: + GITHUB_TOKEN: ${{ github.token }} - name: Upload the author-commit-required regeneration uses: actions/upload-artifact@v4 with: diff --git a/dag/gunbc/ci/ci_heal_credential.dag b/dag/gunbc/ci/ci_heal_credential.dag index 616ce76ac11..a6e2499e214 100644 --- a/dag/gunbc/ci/ci_heal_credential.dag +++ b/dag/gunbc/ci/ci_heal_credential.dag @@ -50,22 +50,23 @@ import gunbc.auth.github_credential { PushBindingInputUnsupported } -// `actions` IS NONE BECAUSE THE CAPABILITY IT WAS SCOPED FOR IS NOT BUILT. It carried -// PermWrite for exactly one consumer: github.Workflows.CreateDispatch, which the heal job -// invoked to revalidate the head it had just pushed (#7544). That dispatch is deliberately not -// restored -- the workflow it targeted does not exist and this one declares no healed-sha input, -// so a dispatch here could not bind which head it got. A permission held for a consumer that -// does not exist is a standing grant in anticipation, and the anticipated thing may never land; -// the credential surface should describe what the job DOES. -// -// WHERE IT COMES BACK, when it does: with the dispatch consumer, as that consumer's own carrier, -// at the point the grant becomes reachable. Pre-granting it here would mean the follow-up lands -// against a permission nobody re-derived. +// `actions: write` IS GRANTED, AND IT IS GRANTED WITH ITS EXECUTING CONSUMER, NOT AHEAD OF ONE. +// It stood at PermNone deliberately: the heal job wrote and pushed and dispatched nothing, so a +// write grant would have been a capability nobody exercised -- the dormant-permission shape a +// prior cut had to REMOVE, and the paragraph that stood here saying so is deleted rather than +// left in the present tense. It is now the grant the dispatch actually spends. The heal script's +// terminal invokes tools.ci_heal_dispatch, whose modeled operation is +// extdeps.github.workflows github.Workflows CreateDispatch -- the workflow-dispatches POST, +// which GitHub authorizes on the `actions` scope +// (docs.github.com/en/rest/actions/workflows#create-a-workflow-dispatch-event, read 2026-09-03). +// PermRead does not admit that POST, so the honest grant is write. NOTHING ELSE WIDENS: the other +// four stay exactly as they were, and `contents: write` remains the push authority +// gunbc.heal_push_plan resolves against. data ci_heal_job_permissions: WorkflowPermissions = WorkflowPermissions { contents: Present { value: PermWrite }, pull_requests: none, issues: none, - actions: Present { value: PermNone }, + actions: Present { value: PermWrite }, id_token: none } diff --git a/dag/gunbc/ci/ci_spec.dag b/dag/gunbc/ci/ci_spec.dag index 2efabf5f529..b154783e424 100644 --- a/dag/gunbc/ci/ci_spec.dag +++ b/dag/gunbc/ci/ci_spec.dag @@ -34,6 +34,7 @@ import v2.workflow.gunbc_invoke_step_emit { gunbc_run_step_script, gunbc_run_step_script_with_prelude, gunbc_run_invocation_script_with_env, + gunbc_invoke_root_stamp_script, gunbc_invoke_step_emit_pipeline } import gunbc.commit_workflow { @@ -1767,35 +1768,43 @@ fn ci_heal_shell_lines() -> List { ) } -// THE PUSHED HEAD IS NOT REVALIDATED BY THIS JOB, AND THE JOB SAYS SO RATHER THAN IMPLYING IT. -// A push made with the Actions job credential does not start a new workflow run -- GitHub -// suppresses that edge to stop a job from triggering itself -- so after a successful heal the -// pull request's checks describe PRIOR_HEAD and no longer describe the branch. That is a real -// gap and the arm below is the fail-closed answer to it: the job prints SupersededByHealedHead -// naming both revisions and EXITS NONZERO, so the healed head arrives with a red job whose text -// says why, and a human or a re-run decides. It does not exit zero on a head nothing has judged. +// THE PUSHED HEAD IS NOW REVALIDATED, AND THE JOB STILL EXITS NONZERO. READ THE PARAGRAPH BELOW +// IN THE PAST TENSE FOR THE GAP, AND THIS ONE FOR WHAT CLOSES IT. A healed head H1 must be judged +// on its own tree, and used to arrive carrying only H0's receipts. The precise form of the premise +// -- GitHub CREATES a run for that push and withholds its EXECUTION, so nothing judges H1 +// automatically -- and its measurement live once, on gunbc.witness_floor_workflow +// ci_heal_expected_healed_sha_input, and are not restated here. The dispatch invocation below +// runs INSIDE the produced-a-heal arm, immediately after the push and before the nonzero exit, +// because $HEALED_HEAD is a variable of this script and the immutable subject is the whole point: +// tools.ci_heal_dispatch sends the branch ref (the only thing GitHub's endpoint accepts) and that +// sha as separate inputs, and gunbc.witness_floor_workflow ci_heal_expected_healed_sha_input is +// the head every dispatched lane binds its own github.sha and checkout against before a witness +// counts. A dispatch that could not name its head would report a verdict about a tree it cannot +// identify, which is why the binding landed first and this wire depends on it. // -// WHAT WOULD CLOSE IT, named as a capability rather than as an artifact: a workflow_dispatch -// entry point on this same workflow carrying the healed sha as a declared input, which every -// dispatched run binds its own github.sha and checkout against before any witness counts. -// gunbc.ci_spec gunbc_ci_heal_dispatch_target and tools.ci_heal_dispatch are the modeled half of -// exactly that and stay unconsumed here, because the workflow they name (`ci.yml`) does not exist -// and witnesses.yml declares no dispatch inputs. Wiring the invocation without those inputs would -// dispatch a run that cannot check WHICH head it got -- the revalidation would be fabricated, not -// performed -- so this cut restores the write-and-push capability and leaves the revalidation -// half openly missing rather than apparently present. +// THE NONZERO EXIT IS NOT SOFTENED BY THE DISPATCH, and that is deliberate. This run judged +// PRIOR_HEAD; it has no standing to speak for H1 whatever it dispatched. So SupersededByHealedHead +// still prints and this job still fails -- the verdict on H1 belongs to the run now starting, not +// to this one. A dispatch refusal makes the gunbc invocation nonzero under FailFast, so the +// transport failure surfaces as a red step rather than as an unremarked absence of a run. +// +// PAST TENSE FROM HERE. That gap and the arm below were the fail-closed answer to it: the job +// printed SupersededByHealedHead naming both revisions and EXITED NONZERO, so the healed head +// arrived with a red job whose text said why, and a human or a re-run decided. It did not exit +// zero on a head nothing had judged. gunbc.ci_spec gunbc_ci_heal_dispatch_target and +// tools.ci_heal_dispatch stayed unconsumed here because the workflow they named (`ci.yml`) did not +// exist and witnesses.yml declared no dispatch inputs. fn gunbc_ci_heal_commit_push_script() -> String { - concat( - fold(ci_heal_shell_lines(), init: "", f: fn(acc, line) { concat(acc, concat(line, "\n")) }), - concat( + join( + [ + gunbc_invoke_root_stamp_script(), + fold(ci_heal_shell_lines(), init: "", f: fn(acc, line) { concat(acc, concat(line, "\n")) }), + concat(" ", concat(gunbc_ci_heal_dispatch_invoke(), "\n")), " echo \"SupersededByHealedHead prior_head=$PRIOR_HEAD healed_head=$HEALED_HEAD; revalidation-required\"\n", - concat( - " if [ -n \"$AUTHOR_COMMIT_DRIFT\" ]; then\n", - concat( - concat(" echo \"::error::HealAuthorCommitRequired head=$HEALED_HEAD author_commit_paths=$AUTHOR_COMMIT_DRIFT cause=", concat(live_heal_push_refusal_cause_token(), concat(" regen_command='", concat(ci_heal_author_commit_regen_command, "'\" >&2\n")))), - " fi\n exit 1\nfi\n" - ) - ) - ) + " if [ -n \"$AUTHOR_COMMIT_DRIFT\" ]; then\n", + concat(" echo \"::error::HealAuthorCommitRequired head=$HEALED_HEAD author_commit_paths=$AUTHOR_COMMIT_DRIFT cause=", concat(live_heal_push_refusal_cause_token(), concat(" regen_command='", concat(ci_heal_author_commit_regen_command, "'\" >&2\n")))), + " fi\n exit 1\nfi\n" + ], + "" ) } diff --git a/dag/gunbc/instruments/ci_heal_dispatch.dag b/dag/gunbc/instruments/ci_heal_dispatch.dag index f6188b31990..ab6d440b411 100644 --- a/dag/gunbc/instruments/ci_heal_dispatch.dag +++ b/dag/gunbc/instruments/ci_heal_dispatch.dag @@ -7,10 +7,18 @@ import std.process { ProcessExit, ExitSuccess, exit_failure } import std.types { CommitSha, NonEmptyStr } import extdeps.shell import extdeps.github.workflows +import gunbc.generated_artifact { WitnessFloorYamlArtifact, artifact_name } data ci_heal_dispatch_owner: String = gunbc_repository.owner data ci_heal_dispatch_repo: String = gunbc_repository.name -data ci_heal_dispatch_workflow_id: String = "ci.yml" +// THE WORKFLOW IS NAMED BY ITS ARTIFACT VARIANT, NOT BY A FILENAME LITERAL. This row read +// "ci.yml" for a fortnight after the 2026-08-15 floor cut deleted that workflow: a literal cannot +// go stale loudly, so the dispatcher pointed at a file with no existence and nothing said so. +// gunbc.generated_artifact GeneratedArtifact is the single authority for which emissions this +// repository commits and where; naming the variant means the census is coproduct exhaustiveness -- +// deleting WitnessFloorYamlArtifact would refuse this module at compile time rather than leaving a +// dangling string. The heal job is a job OF that emission, so the variant is also the true subject. +data ci_heal_dispatch_workflow_id: String = artifact_name(a: WitnessFloorYamlArtifact) // The heal job does not mint a gh-api shell call. It invokes the modeled // github.Workflows.CreateDispatch operation, whose REST transport is the realization handler. The diff --git a/dag/gunbc/witness/witness_floor_workflow.dag b/dag/gunbc/witness/witness_floor_workflow.dag index 3aa70e8f0b5..373108feb1f 100644 --- a/dag/gunbc/witness/witness_floor_workflow.dag +++ b/dag/gunbc/witness/witness_floor_workflow.dag @@ -19,6 +19,7 @@ import v2.std.algebra { FreeSemigroup, list_append, list_map, non_empty_to_list import extdeps.languages.yaml.emit { serialize_yaml } import extdeps.languages.yaml.gha_workflow { project_workflow_to_yaml } import v2.workflow.ci_workflow_run_emit { ci_toolchain_homes_isolated_or_refuse_command } +import v2.workflow.ci_heal_revalidation_preflight_emit { ci_heal_revalidation_preflight_script } import std.dissolution { DissolutionCondition, unbound_dissolution, dissolution_description } import gunbc.toolchain_home_standing { admit_workflow_toolchain_homes, @@ -411,13 +412,103 @@ fn concurrency_of_policy(policy: WitnessFloorConcurrencyPolicy, group: String) - // does not enumerate (the `.dag` side is clean and the drifted artifact is hand-authored Rust). data witness_floor_required_bins: List = ["claim_executor", "gunbc"] +// THE HEAL REVALIDATION INPUT. A heal that repairs a branch pushes a new head H1 with the Actions +// job credential, and H1 must be judged on its own tree rather than inherit H0's receipts, which +// describe a tree that no longer exists. tools.ci_heal_dispatch closes that by dispatching this +// workflow, and a dispatch that cannot say WHICH head it got would report a verdict about a head +// it cannot name: a fabricated revalidation, worse than the honest gap. +// +// CREATED-AND-HELD IS NOT NEVER-CREATED, AND THAT DISTINCTION IS AT TOP BILLING BECAUSE EVERY +// WORDING ERROR THIS CARRIER WENT THROUGH -- IN BOTH DIRECTIONS -- FOLLOWED FROM NOT HAVING THE TWO +// AS SEPARATE STATES. They have different remedies: a held run has a release path, +// POST /actions/runs//approve on THAT run, and a nonexistent one has none. A justification for +// the dispatch route that cannot say which state it is in cannot say what the dispatch buys. +// +// GITHUB WITHHOLDS EXECUTION, NOT CREATION, AND THE HOLD KEYS ON THE EVENT. A `pull_request` run IS +// created for the healed head and executes nothing; the dispatched run on the same head executes. +// So nothing judges H1 automatically by the ordinary route, and the dispatch is the DECLARED path +// because it is the only route to a healed head that runs without a human -- not because no run +// appears. THE MEASURED POPULATIONS LIVE ONCE, IN gunbc.rung_drop floor_cut_heal, whose subject is +// this actuation boundary; they are cited here and deliberately not restated, so one count has one +// authority. +// +// THE INSTRUMENT FAILURE IS KEPT AS A ROW, NOT DELETED WITH THE CONCLUSION IT PRODUCED, because it +// is the sharpest specimen in this repository of a proxy that fails toward the reading its reader +// wants. An earlier draft read this table and concluded that most such runs execute: +// +// run conclusion created -> run_started_at attempt 1 jobs +// 33686753487 failure 21:44:15 -> 21:44:15 0 +// 33705120607 cancelled 01:48:15 -> 01:58:31 0 +// 33703032560 action_required 01:17:18 -> 03:04:23 0 (attempt 2 ran, 1h47m later) +// 33711005806 action_required 03:20:33 -> 03:20:33 0 +// +// TWO PROXIES, BOTH BROKEN, BOTH IN THE SAME DIRECTION. `conclusion != action_required` cannot +// report "held", because a held run still concludes something -- `failure` and `cancelled` above. +// `created_at == run_started_at` cannot report "held" either, because equal timestamps are exactly +// what a run that never ran looks like. Neither proxy has a state in which it says "this executed +// nothing", so neither was ever evidence about executing. THE TEST THAT WOULD HAVE CAUGHT BOTH, +// and the one worth carrying past this subject: ask what input would make the instrument report the +// other way. Only ATTEMPT 1's JOB COUNT has that state, because zero is a value it can return. +// Read attempt 1, never the latest -- a human approving a held run leaves attempt 2 looking like an +// ordinary execution, which is what hid the class for 1h47m on 33703032560. +// +// SO THE BEHAVIOUR IS RELIABLE HOLDING, NOT INTERMITTENT FAILURE, and the carrier says the stronger +// simpler thing rather than the hedge the broken table once forced: 0 of 4 heal pushes started a +// job on attempt 1, and the single run that ever executed did so on attempt 2 after a release. +// +// THE ONE CONTROL THIS ROUTE RESTS ON. On sha 958f743f9e, identity and token are held CONSTANT -- +// actor and triggering_actor are github-actions[bot] on both -- and only the EVENT varies: run +// 33711005806 (pull_request) executed nothing, while run 33711101968 (workflow_dispatch) started +// and bound that head in this very preflight. +// +// THE COST THE LOOSE PREMISE CONCEALED: the dispatched run is a SECOND run on that head, so each +// heal buys a whole additional required-CI run, and its check runs land beside the held run's on +// one commit, where a reader keyed by check NAME cannot tell them apart. +// +// BOUNDARY OBLIGATION, UNDETERMINED BECAUSE UNREADABLE FROM HERE RATHER THAN UNEXAMINED, AND IT +// DECIDES A CLAIM THIS CARRIER THEREFORE DOES NOT MAKE. Releasing a held run is +// POST /actions/runs//approve on THAT run, so whether a dispatched run's green clears the PR +// depends on which contexts branch protection requires -- and branches/main/protection answers 403 +// `Resource not accessible by integration` to the credential these sessions carry, as does the +// Actions permissions surface. So: the dispatch closes the REVALIDATION gap, measured -- the healed +// head is bound and judged. It says NOTHING about the MERGE gate, and the held run is what +// protection was waiting on. Naming the 403 is the point: unreadable names its own remedy, a +// credential that can read those two surfaces; unexamined names nothing. +// So the input is the binding, not a label. The dispatch ref is necessarily a moving branch +// pointer (GitHub's endpoint accepts nothing else); this input carries the immutable subject +// beside it, and every ordinary lane binds BOTH its run subject (github.sha, which is what the +// check is attached to) and its own checkout against it before a witness can count. Absent, the +// run is an ordinary manual dispatch and claims no revalidation. +data ci_heal_expected_healed_sha_input_name: String = "expected_healed_sha" + +data ci_heal_expected_healed_sha_input: DispatchInput = DispatchInput { + name: ci_heal_expected_healed_sha_input_name, + description: Present { + value: "Immutable healed commit required by an auto-heal revalidation run" + }, + required: false, + default: none, + type: InputString +} + +// THE CHECKOUT SELECTS THE EXPECTED HEAD WHEN ONE IS NAMED, and the preflight below still compares +// -- the two are not redundant. Selecting the ref removes the window in which the branch advances +// between dispatch and checkout; comparing github.sha catches the window BEFORE that, in which the +// branch advanced before GitHub resolved the dispatch ref into the run subject. Selection alone +// would produce a run whose checkout is H1 and whose CHECK is attached to H2, which is exactly the +// silent wrong answer this input exists to make unwritable. +data ci_heal_checkout_ref_expression: String = "${{ inputs.expected_healed_sha || github.sha }}" + fn witness_floor_checkout_step() -> Step { UsesStep { name: Present { value: "Checkout" }, id: none, uses: checkout_action, with: Present { - value: [kv(key: "fetch-depth", value: yaml_int(n: 0))] + value: [ + kv(key: "fetch-depth", value: yaml_int(n: 0)), + kv(key: "ref", value: yaml_string(s: ci_heal_checkout_ref_expression)) + ] }, env: none, if_condition: none, @@ -1156,6 +1247,37 @@ fn witness_floor_tsv_upload_step(step_name: String, artifact_name: String, path: // Duplicating the narrower build in the floor lane would buy nothing: the lanes are // runtime-independent by construction (no `needs` edge, no artifact handoff), so their bootstraps // are independent CPU, not a shared prerequisite one could save. +data heal_revalidation_preflight_step_name: String = "Refuse a heal revalidation whose run subject or checkout does not name the expected healed SHA" + +// THE PREFLIGHT IS FIRST AFTER CHECKOUT IN EVERY WITNESS-BEARING LANE, and that position is the +// whole claim: a comparison that runs after a witness has already reported cannot unreport it. +// The script is v2.workflow.ci_heal_revalidation_preflight_emit -- orchestration intent, with bash +// as the GitHub Actions foreign-executor realization -- so the refusal arms are modeled control +// flow rather than hand-authored yaml. The heal job does NOT carry it: heal checks out the +// triggering branch head in order to push a repair onto it, so binding that checkout to an +// expected healed sha would refuse the very job that produces one. +fn heal_revalidation_preflight_step() -> Step { + RunStep { + name: Present { value: heal_revalidation_preflight_step_name }, + id: none, + run: ci_heal_revalidation_preflight_script(), + shell: none, + env: none, + working_directory: none, + if_condition: none, + continue_on_error: none, + timeout_minutes: none + } +} + +fn heal_revalidation_preflight_bound_step() -> WitnessFloorBoundStep { + WitnessFloorBoundStep { + step: heal_revalidation_preflight_step(), + role: capability_neutral, + step_name: heal_revalidation_preflight_step_name, + } +} + fn prepared_bound_steps(build_script: String) -> List { [ WitnessFloorBoundStep { @@ -1168,6 +1290,7 @@ fn prepared_bound_steps(build_script: String) -> List { role: capability_neutral, step_name: "Checkout", }, + heal_revalidation_preflight_bound_step(), WitnessFloorBoundStep { step: toolchain_home_isolation_step(), role: capability_neutral, @@ -1588,6 +1711,7 @@ fn rust_unit_tests_bound_steps() -> List { role: capability_neutral, step_name: "Checkout", }, + heal_revalidation_preflight_bound_step(), WitnessFloorBoundStep { step: toolchain_home_isolation_step(), role: capability_neutral, @@ -1908,13 +2032,22 @@ fn heal_repo_local_git_config_step() -> Step { data heal_commit_push_step_id: String = "heal_commit_push" +// GITHUB_TOKEN IS PROJECTED HERE BECAUSE THE DISPATCH READS IT AS A PROCESS VARIABLE, and the +// grant is added WITH its executing consumer rather than in advance of one. GitHub Actions injects +// `github.token` into `secrets.GITHUB_TOKEN` and into the checkout action's credential, but not +// into the step environment; extdeps.github.workflows github.Workflows resolves its bearer solely +// from auth_source EnvVar GITHUB_TOKEN, so without this binding CreateDispatch would refuse 401. +// This is the only step in the workflow that carries it, and it carries it because the heal +// dispatch composed into its script is the only caller. fn heal_commit_push_step() -> Step { RunStep { name: Present { value: "Commit and push the regeneration" }, id: Present { value: heal_commit_push_step_id }, run: gunbc_ci_heal_commit_push_script(), shell: none, - env: none, + env: Present { + value: [kv(key: "GITHUB_TOKEN", value: yaml_string(s: "${{ github.token }}"))] + }, working_directory: none, if_condition: none, continue_on_error: none, @@ -2424,18 +2557,71 @@ fn required_lanes_aggregate_job() -> Job { } } -data witness_floor_workflow: Workflow = { - name: witness_floor_workflow_name, - run_name: none, - on: [ - WorkflowDispatch { inputs: [] }, +// THE TRIGGERS AND THE LANE JOBS ARE NAMED SEPARATELY FROM THE WORKFLOW THEY ASSEMBLE, AND THE +// REASON IS COST, NOT TASTE. A record is materialized whole, so a reader that wants one field pays +// for every other -- and one of the other fields is `required_lanes_aggregate_job`, whose `run` is +// the serialized `gunbc.required_lanes_gate` program, the largest bash AST this workflow carries. +// Measured with `claim_batch --functions`, one witness per subject. THE ORDERING IS THE FINDING AND +// THE ABSOLUTE FIGURES ARE NOT PORTABLE: the session container this was measured in priced the +// aggregate's fill at three times what the runner priced the same fill at on check 100530537497, so +// a millisecond figure taken here would read as a safety margin to anyone who did not know which +// machine produced it. What transfers is the shape. The assembled workflow is dominated by one job: +// `required_lanes_aggregate_job` is about seven eighths of its cost and the six lane jobs together +// are the remaining eighth. So a witness asking "is the dispatch input declared" was serializing a +// gate script it says nothing about, and three such rows exceeded `v2.workflow.required_floor` +// `required_floor_claim_cpu_safety_limit_ms` on that check. +// +// AN EARLIER REVISION OF THIS PARAGRAPH CLAIMED A FIXED "FLOOR FOR REACHING THIS MODULE AT ALL", +// AND THERE IS NO SUCH FLOOR. It was inferred from a first probe in which all six per-job subjects +// landed in one narrow band, and a band across six readers is evidence of work SHARED BETWEEN them, +// never of a cost beneath them -- only a reader that touches almost nothing can tell those two +// apart. THE 3ms ROW IS THAT READER AND IT IS WHY THE QUESTION IS SETTLED: +// `test.claim.heal_revalidation_binding_witness` +// `the_required_workflow_declares_the_healed_sha_dispatch_input` reads `witness_floor_triggers` and +// nothing else, and costs two orders of magnitude less than the band on the same instrument. A +// future author pricing a witness against this carrier needs that row and not the phantom, because +// the phantom says a cheap reader is impossible and the row is one. +// +// SPLITTING THE ROWS WOULD NOT HAVE FIXED THAT AND WAS TRIED FIRST. Two rows became four, each half +// landing nearer the ceiling, and the fold they both paid was untouched -- an improvement in the +// arithmetic that was a coincidence of size, one emitted line from red again. DESIGN section 2 says +// to minimize the demand graph before materializing its answers; the demand here was for the +// aggregate's serialized text, and no consumer of these two producers asks for it. +// +// NEITHER IS A SECOND AUTHORITY FOR WHAT THE WORKFLOW IS. `witness_floor_workflow` is assembled +// from exactly these, so a lane added here is a lane in the emitted yaml, and a reader folding +// `witness_floor_lane_jobs` covers every witness-bearing lane by construction rather than by a +// hand-listed roster that could fall behind. +fn witness_floor_triggers() -> List { + [ + WorkflowDispatch { inputs: [ci_heal_expected_healed_sha_input] }, MergeGroup, Push { branches: [gunbc_default_branch_name], paths: [] }, PullRequest { branches: [gunbc_default_branch_name], types: [Opened, Synchronize, Reopened] } - ], + ] +} + +// THE AGGREGATE IS DELIBERATELY NOT A MEMBER. It checks out nothing and runs no witness: it reads +// the other lanes' results. Every consumer of this list is asking about lanes that carry a subject, +// and the aggregate joined that population only as something to filter back out. +fn witness_floor_lane_jobs() -> List { + [ + build_lane_job(), + witness_floor_job(), + rust_unit_tests_job(), + fabric_evidence_job(), + emit_copy_qualification_battery_job(), + heal_generated_artifacts_job() + ] +} + +data witness_floor_workflow: Workflow = { + name: witness_floor_workflow_name, + run_name: none, + on: witness_floor_triggers(), concurrency: Present { value: concurrency_of_policy( policy: witness_floor_concurrency_policy, @@ -2461,7 +2647,7 @@ data witness_floor_workflow: Workflow = { id_token: none } }, - jobs: [build_lane_job(), witness_floor_job(), rust_unit_tests_job(), fabric_evidence_job(), emit_copy_qualification_battery_job(), heal_generated_artifacts_job(), required_lanes_aggregate_job()] + jobs: list_append(left: witness_floor_lane_jobs(), right: [required_lanes_aggregate_job()]) } // THE CLOSURE HAS A PRODUCTION CONSUMER, which is the difference between a check and a claim. A diff --git a/dag/test/claim/heal_revalidation_binding_witness_test.dag b/dag/test/claim/heal_revalidation_binding_witness_test.dag new file mode 100644 index 00000000000..9385b5114dc --- /dev/null +++ b/dag/test/claim/heal_revalidation_binding_witness_test.dag @@ -0,0 +1,376 @@ +module test.claim.heal_revalidation_binding_witness + +import extdeps.github.actions { + Step, RunStep, UsesStep, Job, + WorkflowTrigger, WorkflowDispatch, Push, PullRequest, Schedule, WorkflowCall, + WorkflowRunCompleted, MergeGroup, + PermRead, PermWrite, PermNone +} +import extdeps.languages.yaml.gha_workflow { workflow_trigger_entry } +import extdeps.languages.yaml.types { + YamlValue, YamlNull, YamlBool, YamlString, YamlInt, YamlFloat, YamlSequence, YamlMapping +} +import gunbc.witness_floor_workflow { + heal_revalidation_preflight_step, + heal_revalidation_preflight_step_name, + ci_heal_expected_healed_sha_input_name, + ci_heal_checkout_ref_expression, + heal_generated_artifacts_job_id, + witness_floor_lane_jobs, + witness_floor_triggers +} +import gunbc.ci_spec { gunbc_ci_heal_commit_push_script, gunbc_ci_heal_dispatch_invoke } +import v2.workflow.gunbc_invoke_step_emit { gunbc_invoke_root_stamp_script } +import gunbc.ci_heal_credential { ci_heal_job_permissions } +import gunbc.generated_artifact { WitnessFloorYamlArtifact, artifact_name } +import tools.ci_heal_dispatch { ci_heal_dispatch_workflow_id } + +// THE SUBJECT IS THE BINDING, NOT THE FEATURE AROUND IT. A heal that repairs a branch pushes a new +// head and dispatches a revalidation of it; a dispatched run that cannot say WHICH head it got +// would report a verdict about a tree it cannot identify. Every row here is one half of making +// that unwritable: the input exists, the checkout selects it, the comparison runs before any +// witness in every witness-bearing lane, and the dispatcher names the workflow that carries them. +// +// WHAT THESE CANNOT SAY, stated so the green is not over-read: these read the MODELED workflow and +// the EMITTED script text. They establish the shape CI is asked to run. Whether a real dispatched +// run then refuses on a mismatched sha is a live-execution fact and is evidenced by an executed +// dispatch, not from here. + +fn step_name_or_empty(s: Step) -> String { + match s { + RunStep { + name, id: _, run: _, shell: _, env: _, working_directory: _, + if_condition: _, continue_on_error: _, timeout_minutes: _ + } => + match name { Present { value } => value Absent => "" } + UsesStep { + name, id: _, uses: _, with: _, env: _, + if_condition: _, continue_on_error: _, timeout_minutes: _ + } => + match name { Present { value } => value Absent => "" } + } +} + +fn job_step_names(j: Job) -> List { + map(j.steps, s => step_name_or_empty(s: s)) +} + +// The order fact is expressed as an ADJACENT PAIR over the step-name list rather than as two +// membership checks, because "the preflight is present" and "the preflight runs before the first +// witness" are different claims and only the second is the one that matters: a comparison that +// runs after a witness has reported cannot unreport it. +type AdjacencyScan { after_checkout: Bool, found: Bool } + +fn preflight_immediately_follows_checkout(j: Job) -> Bool { + fold(job_step_names(j: j), init: AdjacencyScan { after_checkout: false, found: false }, + f: fn(acc, n) { + AdjacencyScan { + after_checkout: n == "Checkout", + found: acc.found + || (acc.after_checkout && n == heal_revalidation_preflight_step_name) + } + }).found +} + +fn job_by_id(id: String) -> Job? { + fold(witness_floor_lane_jobs(), init: none, f: fn(acc, j) { + match acc { + Present { value: found } => Present { value: found } + Absent => if j.id == id { Present { value: j } } else { none } + } + }) +} + +fn job_has_checkout(j: Job) -> Bool { + any(job_step_names(j: j), n => n == "Checkout") +} + +// EVERY witness-bearing lane, derived from the workflow's own lane list rather than from a roster +// retyped here: a job that checks out the ordinary subject is a job whose steps can report on it, +// so the population is "carries a `Checkout` step", and adding a sixth such lane without the +// preflight reds this row instead of slipping past a hand-listed five. +// +// THE SUBJECT IS `witness_floor_lane_jobs`, NOT THE ASSEMBLED WORKFLOW, AND THAT IS A COST FACT +// WITH A RECEIPT. Reading the record forced `required_lanes_aggregate_job`, whose serialized gate +// script was about seven eighths of the assembled workflow's cost -- a subject no row in this file +// says anything about, and the reason three of them exceeded the floor's per-claim ceiling on check +// 100530537497. The figures are deliberately not restated here as milliseconds: they were taken on +// a session container measuring about three times the runner, so the proportion transfers and the +// absolute numbers do not. `gunbc.witness_floor_workflow` `witness_floor_triggers` carries the +// measurement, the instrument, and why splitting the rows was the wrong repair. +test fn every_ordinary_checkout_lane_preflights_before_its_first_witness() -> Bool { + let lanes = filter(witness_floor_lane_jobs(), j => job_has_checkout(j: j)) + lanes.length() >= 5 + && all(lanes, j => preflight_immediately_follows_checkout(j: j)) +} + +// The heal job is the one lane that must NOT bind its checkout to an expected healed head: it +// checks out the triggering branch head in order to PRODUCE one. Binding it would refuse the job +// that creates the subject every other lane is being asked to verify. +test fn the_heal_job_carries_no_revalidation_preflight() -> Bool { + match job_by_id(id: heal_generated_artifacts_job_id) { + Absent => false + Present { value: heal } => + !any(job_step_names(j: heal), n => n == heal_revalidation_preflight_step_name) + && !job_has_checkout(j: heal) + } +} + +// ONE ACCESSOR, USED THREE TIMES, INSTEAD OF THREE NESTED HAND-ROLLED WALKS. The first cut of this +// predicate folded a mapping's entries, matched every YamlValue variant, and did it again one level +// down and again below that -- forty lines whose subject was "descend three keys". `yaml_key` is +// that descent named once: it is the mapping-lookup extdeps.languages.yaml.types does not export, +// which today offers constructors and `yaml_value_kind` and no query at all. +// +// IT IS LOCAL, AND THAT IS A DELIBERATE SCOPE CHOICE RATHER THAN THE RIGHT FINAL HOME. Its proper +// home under DESIGN section 3 is beside the type it reads, in extdeps.languages.yaml.types, so +// every reader of a YamlValue shares one descent. Landing it there is a shared-module change that +// reaches lanes with no stake in this PR, so it is authored here and DISSOLVES INTO that accessor +// the moment one exists -- at which point this row and its twin in +// test.claim.workflow_dispatch_input_witness, which still carries the older triple-nested form for +// the same question, both collapse onto it. +// +// THE LEAF STILL MATCHES EXHAUSTIVELY AND MUST. `Optional` at each step is the honest +// shape of a lookup that can miss; the terminal type check is an exhaustive match over a CLOSED +// coproduct, which is DESIGN section 4's own idiom. A wildcard arm there would be cheaper to read +// and strictly worse: adding a YamlValue variant would silently answer `false` instead of failing +// to compile, which is the absorbing fallback section 5 forbids. +fn yaml_key(v: YamlValue, key: String) -> YamlValue? { + match v { + YamlMapping { entries } => + fold(entries, init: none, f: fn(acc, entry) { + match acc { + Present { value: found } => Present { value: found } + Absent => if entry.key == key { Present { value: entry.value } } else { none } + } + }) + YamlNull => none + YamlBool { value: _ } => none + YamlInt { lexeme: _ } => none + YamlFloat { lexeme: _ } => none + YamlString { value: _ } => none + YamlSequence { elements: _ } => none + } +} + +fn yaml_is_string(v: YamlValue?, expected: String) -> Bool { + match v { + Absent => false + Present { value: inner } => + match inner { + YamlString { value } => value == expected + YamlNull => false + YamlBool { value: _ } => false + YamlInt { lexeme: _ } => false + YamlFloat { lexeme: _ } => false + YamlSequence { elements: _ } => false + YamlMapping { entries: _ } => false + } + } +} + +fn yaml_key_of(v: YamlValue?, key: String) -> YamlValue? { + match v { + Absent => none + Present { value: inner } => yaml_key(v: inner, key: key) + } +} + +fn dispatch_input_is_declared_string(v: YamlValue) -> Bool { + yaml_is_string( + v: yaml_key_of( + v: yaml_key_of( + v: yaml_key(v: v, key: "inputs"), + key: ci_heal_expected_healed_sha_input_name + ), + key: "type" + ), + expected: "string" + ) +} + +fn dispatch_trigger_value() -> YamlValue { + fold(witness_floor_triggers(), init: YamlNull, f: fn(acc, t) { + match t { + WorkflowDispatch { inputs: _ } => workflow_trigger_entry(trigger: t).value + Push { branches: _, paths: _ } => acc + PullRequest { branches: _, types: _ } => acc + Schedule { cron: _ } => acc + WorkflowCall { inputs: _ } => acc + WorkflowRunCompleted { workflows: _, branches: _ } => acc + MergeGroup => acc + } + }) +} + +// This reads the PROJECTED yaml value rather than the DispatchInput row it came from: the +// serializer discarded the whole inputs list for a stretch while the model carried it, so a +// witness over the model alone would have been green across exactly that defect. +test fn the_required_workflow_declares_the_healed_sha_dispatch_input() -> Bool { + dispatch_input_is_declared_string(v: dispatch_trigger_value()) +} + +// SELECTION AND COMPARISON ARE BOTH REQUIRED AND ARE DIFFERENT CLAIMS. `ref:` closes the window in +// which the branch advances between dispatch and checkout; 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. +test fn the_ordinary_checkout_selects_the_expected_head_when_one_is_named() -> Bool { + ci_heal_checkout_ref_expression + == "$\{\{ inputs.expected_healed_sha || github.sha \}\}" +} + +// THE DISPATCH IS INSIDE THE PRODUCED-A-HEAL ARM AND BEFORE THE NONZERO EXIT, asserted as ORDERED +// ADJACENCY rather than as two `contains` calls. Membership alone would stay green with the +// invocation after the exit, where it can never run. +// +// THE ROOT STAMP ARM IS HERE BECAUSE IT ALREADY FAILED ONCE, in this cut, on the first emission: +// $ROOT is 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 emitted yaml looked entirely +// plausible, which is exactly the shape a witness is for. +test fn the_heal_terminal_dispatches_the_healed_head_before_it_exits_nonzero() -> Bool { + let script = gunbc_ci_heal_commit_push_script() + string_contains( + s: script, + pattern: concat( + gunbc_ci_heal_dispatch_invoke(), + "\n echo \"SupersededByHealedHead" + ) + ) + && string_contains(s: script, pattern: " exit 1\nfi\n") + && string_contains(s: script, pattern: concat(gunbc_invoke_root_stamp_script(), "git config user.name")) +} + +// The dispatch carries the immutable subject and the moving ref as SEPARATE inputs. One of them +// standing in for the other is the fabricated revalidation this whole cut exists to prevent. +test fn the_heal_dispatch_binds_the_healed_head_and_the_branch_ref_separately() -> Bool { + let invoke = gunbc_ci_heal_dispatch_invoke() + string_contains(s: invoke, pattern: "GUNBC_HEALED_HEAD=\"$HEALED_HEAD\"") + && string_contains(s: invoke, pattern: "GUNBC_HEAL_BRANCH_REF=") + && string_contains( + s: invoke, + pattern: "--entry dag/gunbc/instruments/ci_heal_dispatch.dag --function main" + ) +} + +// THE WORKFLOW IS NAMED BY ITS ARTIFACT VARIANT. The literal this replaces read "ci.yml" for a +// fortnight after that workflow was deleted, because a string cannot go stale loudly. The negative +// clause carries the content: an equality against the variant would also hold if someone re-typed +// the same spelling as a literal, so the row that a DELETED name has not come back is asserted too. +test fn the_dispatcher_names_the_emission_that_carries_the_heal_job() -> Bool { + ci_heal_dispatch_workflow_id == artifact_name(a: WitnessFloorYamlArtifact) + && ci_heal_dispatch_workflow_id == "witnesses.yml" + && ci_heal_dispatch_workflow_id != "ci.yml" +} + +// The grant is spent, not held. `actions: write` is what GitHub authorizes the workflow-dispatches +// POST on, and it landed with the invocation above rather than in anticipation of one. +test fn the_heal_job_grant_admits_the_dispatch_and_widens_nothing_else() -> Bool { + match ci_heal_job_permissions.actions { + Present { value: level } => + match level { PermWrite => true PermRead => false PermNone => false } + Absent => false + } + && match ci_heal_job_permissions.contents { + Present { value: level } => + match level { PermWrite => true PermRead => false PermNone => false } + Absent => false + } + && match ci_heal_job_permissions.pull_requests { Absent => true Present { value: _ } => false } + && match ci_heal_job_permissions.issues { Absent => true Present { value: _ } => false } + && match ci_heal_job_permissions.id_token { Absent => true Present { value: _ } => false } +} + +fn preflight_step_script() -> String { + match heal_revalidation_preflight_step() { + RunStep { + name: _, id: _, run, shell: _, env: _, working_directory: _, + if_condition: _, continue_on_error: _, timeout_minutes: _ + } => run + UsesStep { + name: _, id: _, uses: _, with: _, env: _, + if_condition: _, continue_on_error: _, timeout_minutes: _ + } => "" + } +} + +// THE TWO RACES ARE SEPARATELY ASSERTED, because they have different causes and only one of them +// is visible from a comparison against github.sha. `expected != github.sha` is the branch advancing +// BEFORE GitHub resolved the dispatch ref into a run subject: the check would be attached to a +// commit the operator never named. `expected == github.sha` while `git rev-parse HEAD` differs is +// the checkout diverging AFTERWARDS: the right subject, the wrong tree. A preflight carrying only +// the first passes the second while the job builds the wrong tree, which is why both +// `[ "$RUN_SUBJECT_HEAD" = ... ]` and `[ "$ACTUAL_HEAD" = ... ]` are named here. +// +// THE SUBJECT IS THE STEP THE WORKFLOW CARRIES, AND THE JOIN TO THE WORKFLOW IS THE ADJACENCY ROW +// ABOVE, NOT A SECOND WHOLE-FILE FOLD. The first cut of these two rows read +// expected_witness_floor_yml(), which generates and serializes every job; both BUDGET-REFUSED on +// the required floor at 503ms and 506ms against its 500ms CPU ceiling and went UNDECIDED -- and an +// undecided row is not a weaker green, it is no verdict at all. Composing two cheap rows reaches +// the same conclusion: this exact Step value is in every ordinary lane's job list (adjacency), and +// this Step's own `run` carries both arms (here). The serializer copies that string verbatim into +// the block scalar, so what is one step removed is the INDENTATION, not the content. +// +// WHAT THE COMPOSED PAIR CANNOT CATCH, NAMED RATHER THAN LEFT FOR A READER TO DISCOVER, because +// replacing a whole-file fold with two cheaper rows is from the outside indistinguishable from +// collapsing a check to fit its transport. BOTH rows read the MODEL -- the job list and the Step +// value -- so a serializer that DROPPED this step, emitted its `run` under the wrong key, or +// produced a block scalar whose indentation makes the shell parse differently would leave both +// green. That blind spot is not hypothetical: extdeps.languages.yaml.gha_workflow +// workflow_dispatch_yaml discarded the ENTIRE inputs list while the model carried it, which is the +// same class one field over. It is bounded here by the_required_workflow_declares_the_healed_sha_ +// dispatch_input, which reads the PROJECTED YamlValue rather than the DispatchInput row -- but +// that covers the trigger, NOT the steps, and this file does not claim otherwise. +// +// THE NARROWING WAS BOUNDED BY MEASUREMENT, NOT BY TRIMMING UNTIL GREEN: the two rows cost 192ms +// and 200ms against a 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. +// +// THE CHECKOUT-MISMATCH ARM IS UNREACHABLE FROM THE PRODUCTION SURFACE, NOT UNTESTED, AND THE +// DISTINCTION IS WRITTEN HERE SO THE NEXT READER DOES NOT HAVE TO REDERIVE IT. Both mismatch arms +// are emitted and both are asserted, but only the RUN-SUBJECT one has a live receipt, and the +// reason is the fix itself rather than a gap in diligence: the checkout is bound to the input +// (ci_heal_checkout_ref_expression). If expected != github.sha the run-subject arm trips first; if +// expected == github.sha then the checkout ref IS expected, so HEAD cannot differ. Inducing the +// checkout arm 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 ITS DISPOSITION IS DEFENSE-IN-DEPTH BEHIND ref: SELECTION, with the discriminating RED at the +// fixture boundary, where the state IS authorable and IS authored: test.claim.heal_revalidation_ +// witness expected_sha_preflight_binds_run_subject_and_checkout_exactly feeds +// classify_workflow_dispatch_preflight a checkout head that differs from a matching run subject +// and requires HealWorkflowDispatchCheckoutMismatch. This file's contribution is the other half -- +// that the comparison reached the step the workflow carries rather than stopping at the model. +// Neither is a live receipt and neither is described as one. +// +// LIVE RECEIPTS THAT DO EXIST, named by their producer rather than transcribed: a workflow_dispatch +// of gunbc.witness_floor_workflow carrying a stale sha refuses at this step in every ordinary +// checkout lane with every adjudicating step skipped, and one carrying the correct head passes the +// same step in the same lanes and proceeds into the machinery. The second is not decoration: a +// preflight that refused everything would satisfy the first arm permanently. +test fn the_preflight_step_carries_both_mismatch_arms_and_the_pass_arm() -> Bool { + let script = preflight_step_script() + string_contains(s: script, pattern: "[ \"$RUN_SUBJECT_HEAD\" = \"$EXPECTED_HEALED_SHA\" ]") + && string_contains(s: script, pattern: "heal revalidation refused: workflow run subject") + && string_contains(s: script, pattern: "[ \"$ACTUAL_HEAD\" = \"$EXPECTED_HEALED_SHA\" ]") + && string_contains(s: script, pattern: "heal revalidation refused: checkout head") + && string_contains( + s: script, + pattern: "heal revalidation preflight: checkout names expected healed head" + ) +} + +// ABSENCE MEANS ORDINARY MANUAL DISPATCH, AND A HAND-TRIGGERED RUN THEREFORE DISCHARGES NO HEAL +// OBLIGATION. The guard is what keeps that true in the emitted script; without it an ordinary +// dispatch would compare "" against github.sha and refuse every manual run, and the fix for THAT +// would be to delete the comparison -- which is how a wall becomes a decoration in two steps. +// The model half is witnessed separately, at the arm that returns OrdinaryWorkflowDispatch +// (test.claim.heal_revalidation_witness +// manual_dispatch_without_expected_sha_cannot_masquerade_as_heal_revalidation). +test fn an_absent_input_is_an_ordinary_manual_dispatch_in_the_preflight_step() -> Bool { + string_contains( + s: preflight_step_script(), + pattern: "if [ -n \"$EXPECTED_HEALED_SHA\" ]; then" + ) +} diff --git a/src/v2/workflow/gunbc_invoke_step_emit.dag b/src/v2/workflow/gunbc_invoke_step_emit.dag index c89898426e7..1eebd67e14f 100644 --- a/src/v2/workflow/gunbc_invoke_step_emit.dag +++ b/src/v2/workflow/gunbc_invoke_step_emit.dag @@ -294,6 +294,24 @@ fn gunbc_run_step_script_with_prelude( ) } +// THE STAMP ON ITS OWN, for a step that is not a gunbc-run step but composes one into its own +// script (the heal dispatch wire). Without it $ROOT is empty in that step and the invocation +// resolves to /target/release/gunbc, which exists nowhere -- a dispatch that cannot run at all. +// It is exported rather than re-spelled at the call site so `ROOT=` keeps ONE definition: +// ci_repo_root_shell, the same authority every ordinary step stamps from. +// THE TERMINATOR IS PART OF THE FRAGMENT, not the caller's to remember. The pipeline emitter joins +// its steps with newlines and does not terminate the last one, which is right for a whole step and +// wrong for a fragment something else continues: the first emission of this ran the stamp and the +// next command together on one line. A caller cannot get that wrong if the line arrives complete. +fn gunbc_invoke_root_stamp_script() -> String { + concat( + gunbc_invoke_step_emit_pipeline( + p: Pipeline { steps: [gunbc_invoke_root_stamp_step()], on_failure: FailFast } + ), + "\n" + ) +} + // Same root for a call site that carries env bindings on the invocation itself and // inherits ROOT from the step it is composed into (the heal dispatch wire). The bindings // are the orchestration EnvBinding carrier, not a hand-spelled "NAME=value " prefix.