Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
96 changes: 95 additions & 1 deletion .github/workflows/witnesses.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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=""
Expand Down Expand Up @@ -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:
Expand Down
25 changes: 13 additions & 12 deletions dag/gunbc/ci/ci_heal_credential.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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
}

Expand Down
63 changes: 36 additions & 27 deletions dag/gunbc/ci/ci_spec.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -1767,35 +1768,43 @@ fn ci_heal_shell_lines() -> List<String> {
)
}

// 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"
],
""
)
}
10 changes: 9 additions & 1 deletion dag/gunbc/instruments/ci_heal_dispatch.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading
Loading