diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 963941652cf..6e662f7154b 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,6 +1,11 @@ name: ci on: workflow_dispatch: + inputs: + expected_healed_sha: + description: Immutable healed commit required by an auto-heal revalidation run + required: false + type: string push: branches: [main] pull_request: @@ -25,6 +30,18 @@ jobs: uses: actions/checkout@v5 with: fetch-depth: 0 + ref: ${{ inputs.expected_healed_sha || github.sha }} + - name: Refuse a heal revalidation checkout that does not name the expected healed SHA + run: | + EXPECTED_HEALED_SHA="${{ inputs.expected_healed_sha }}" + if [ -n "$EXPECTED_HEALED_SHA" ]; then + ACTUAL_HEAD="$(git rev-parse HEAD)" + 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 dirs run: | rm -rf "$RUNNER_TEMP/rustup" "$RUNNER_TEMP/cargo" @@ -123,6 +140,18 @@ jobs: uses: actions/checkout@v5 with: fetch-depth: 0 + ref: ${{ inputs.expected_healed_sha || github.sha }} + - name: Refuse a heal revalidation checkout that does not name the expected healed SHA + run: | + EXPECTED_HEALED_SHA="${{ inputs.expected_healed_sha }}" + if [ -n "$EXPECTED_HEALED_SHA" ]; then + ACTUAL_HEAD="$(git rev-parse HEAD)" + 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: Setup Rust (floor gate toolchain — batch-4 emit_host/self_host gates need cargo/rustfmt; no isolated rustup) uses: actions-rust-lang/setup-rust-toolchain@v1.16.0 with: @@ -182,6 +211,18 @@ jobs: uses: actions/checkout@v5 with: fetch-depth: 0 + ref: ${{ inputs.expected_healed_sha || github.sha }} + - name: Refuse a heal revalidation checkout that does not name the expected healed SHA + run: | + EXPECTED_HEALED_SHA="${{ inputs.expected_healed_sha }}" + if [ -n "$EXPECTED_HEALED_SHA" ]; then + ACTUAL_HEAD="$(git rev-parse HEAD)" + 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: Setup Rust (floor gate toolchain — batch-4 emit_host/self_host gates need cargo/rustfmt; no isolated rustup) uses: actions-rust-lang/setup-rust-toolchain@v1.16.0 with: @@ -244,6 +285,18 @@ jobs: uses: actions/checkout@v5 with: fetch-depth: 0 + ref: ${{ inputs.expected_healed_sha || github.sha }} + - name: Refuse a heal revalidation checkout that does not name the expected healed SHA + run: | + EXPECTED_HEALED_SHA="${{ inputs.expected_healed_sha }}" + if [ -n "$EXPECTED_HEALED_SHA" ]; then + ACTUAL_HEAD="$(git rev-parse HEAD)" + 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: Download release-bins artifact uses: actions/download-artifact@v4 with: @@ -269,6 +322,7 @@ jobs: if: github.event_name == 'pull_request' permissions: contents: write + actions: write steps: - name: Checkout triggering branch head (heal pushes the regeneration back to this branch) uses: actions/checkout@v5 @@ -409,11 +463,23 @@ jobs: if [ -e "docs/plans/fleet-acceptance-criteria.md" ]; then git add "docs/plans/fleet-acceptance-criteria.md"; else echo "chore-heal: registered generated artifact absent on this tree, not staging: docs/plans/fleet-acceptance-criteria.md"; fi if [ -e "docs/plans/structural-quadratic-wall-coverage-audit.md" ]; then git add "docs/plans/structural-quadratic-wall-coverage-audit.md"; else echo "chore-heal: registered generated artifact absent on this tree, not staging: docs/plans/structural-quadratic-wall-coverage-audit.md"; fi if [ -e "docs/plans/ci-performance-tanking-evidence.md" ]; then git add "docs/plans/ci-performance-tanking-evidence.md"; else echo "chore-heal: registered generated artifact absent on this tree, not staging: docs/plans/ci-performance-tanking-evidence.md"; fi + PRIOR_HEAD=$(git rev-parse HEAD) if git diff --cached --quiet; then - echo "chore-heal: no generated-artifact drift on this tree; nothing to commit" + echo "HealNoChange head=$PRIOR_HEAD" + exit 0 else + CHANGED_ARTIFACTS=$(git diff --cached --name-only) git commit -m "chore: regenerate drifted generated artifacts (ci auto-heal)" + HEALED_HEAD=$(git rev-parse HEAD) git push origin HEAD:${{ github.head_ref || github.ref_name }} - echo "chore-heal: pushed regenerated generated artifacts to the triggering branch" + echo "HealProduced prior_head=$PRIOR_HEAD healed_head=$HEALED_HEAD changed_artifacts=$CHANGED_ARTIFACTS" + ROOT=$(git rev-parse --show-toplevel) + if ! GUNBC_HEALED_HEAD="$HEALED_HEAD" "$ROOT/target/release/gunbc" run --source-root "$ROOT/dag" --source-root "$ROOT/src/v2" --entry dag/tools/ci_heal_dispatch.dag --function main + then + echo "::error::HealDispatchRefused healed_head=$HEALED_HEAD cause=CreateWorkflowDispatchFailed" >&2 + exit 1 + fi + echo "SupersededByHealedHead prior_head=$PRIOR_HEAD healed_head=$HEALED_HEAD; revalidation-required" + exit 1 fi timeout-minutes: 5 diff --git a/dag/extdeps/github/workflows.dag b/dag/extdeps/github/workflows.dag new file mode 100644 index 00000000000..19a1f5d46c3 --- /dev/null +++ b/dag/extdeps/github/workflows.dag @@ -0,0 +1,74 @@ +module extdeps.github.workflows + +import extdeps.github.github { default_api_base } +import extdeps.github.errors { GitHubErrorShape } +import std.credentials { EnvVar } +import std.types { CommitSha, NonEmptyStr } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "docs.github.com/en/rest/actions/workflows#create-a-workflow-dispatch-event" + } +} + +data workflows_api_version: NonEmptyStr = "2026-03-10" + +data create_dispatch_version_fidelity_note: String = "Create Workflow Dispatch has two live response contracts across GitHub REST versions. Requests without X-GitHub-Api-Version default to 2022-11-28 and return 204 No Content. Version 2026-03-10 returns 200 with workflow_run_id, run_url, and html_url. This service explicitly pins 2026-03-10 in the transport header, so WorkflowDispatchReceipt is the cited response rather than a fabricated body projected from an unversioned 204. Authority: docs.github.com/en/rest/about-the-rest-api/api-versions and the Create a workflow dispatch event response schema, read 2026-08-01." + +data create_dispatch_ref_authority_note: String = "The dispatch ref parameter may name a branch, tag, or commit SHA (Create a workflow dispatch event — docs.github.com/en/rest/actions/workflows#create-a-workflow-dispatch-event). Heal revalidation dispatches on the healed commit SHA so the workflow run subject and executed checkout bind to one immutable head; a branch ref would let a later push advance the named ref while CI executed an older tree." + +type WorkflowDispatchReceipt { + workflow_run_id: Int + run_url: NonEmptyStr + html_url: NonEmptyStr +} + +service github.Workflows { + config { + endpoint: default_api_base + auth: Bearer + auth_source: EnvVar { name: "GITHUB_TOKEN" } + + rate_limit: { requests: 5000, per: hour, scope: core } + + retry: { max_attempts: 1, backoff: none, retry_on: [] } + } + + operation CreateDispatch { + input { + owner: String + repo: String + workflow_id: String + ref: String + expected_healed_sha: CommitSha + } + output { + workflow_run_id: Int + run_url: NonEmptyStr + html_url: NonEmptyStr + } + transport rest { + method: POST, + path: "/repos/\{owner\}/\{repo\}/actions/workflows/\{workflow_id\}/dispatches", + headers: { "X-GitHub-Api-Version": workflows_api_version }, + body: { + ref: ref, + inputs: { expected_healed_sha: expected_healed_sha } + } + } + response { + 200 => WorkflowDispatchReceipt + 401 => GitHubErrorShape + 403 => GitHubErrorShape + 404 => GitHubErrorShape + 422 => GitHubErrorShape + 429 => GitHubErrorShape + 5xx => GitHubErrorShape + } + } +} + +data create_dispatch_retry_policy_note: String = "CreateDispatch is intentionally single-attempt. Once the heal push has created a new subject, a dispatch refusal must be visible as HealDispatchRefused and leave revalidation required; silently retrying a permission, rate-limit, or server refusal into apparent success would erase the classification operators need. The owning workflow may be retriggered deliberately after diagnosis, but this operation never assumes that the GITHUB_TOKEN push created a run." diff --git a/dag/extdeps/languages/yaml/gha_workflow.dag b/dag/extdeps/languages/yaml/gha_workflow.dag index a3b4c098d0c..6b27794152e 100644 --- a/dag/extdeps/languages/yaml/gha_workflow.dag +++ b/dag/extdeps/languages/yaml/gha_workflow.dag @@ -11,6 +11,7 @@ import extdeps.cron.schedule_model { render_cron_schedule } import extdeps.github.actions { Workflow, Job, Step, RunStep, UsesStep, ActionRef, WorkflowTrigger, Push, PullRequest, WorkflowDispatch, Schedule, MergeGroup, + DispatchInput, DispatchInputType, InputString, InputBoolean, InputChoice, InputEnvironment, PullRequestActivity, Opened, Synchronize, Reopened, ReadyForReview, Closed, WorkflowPermissions, PermissionLevel, PermRead, PermWrite, PermNone, ConcurrencySpec, ConcurrencyScalar, ConcurrencyMappingQueueMax, ConcurrencyMappingQueueNotMax, @@ -88,10 +89,57 @@ fn push_trigger_yaml(branches: List, paths: List) -> YamlKeyValu kv(key: "push", value: yaml_mapping(entries: entries)) } +fn dispatch_input_type_label(t: DispatchInputType) -> String { + match t { + InputString => "string" + InputBoolean => "boolean" + InputChoice => "choice" + InputEnvironment => "environment" + } +} + +fn dispatch_input_optional_string(key: String, value: String?) -> List { + match value { + Present { value: s } => [kv(key: key, value: yaml_string(s: s))] + Absent => [] + } +} + +fn dispatch_input_yaml(input: DispatchInput) -> YamlKeyValue { + kv( + key: input.name, + value: yaml_mapping(entries: concat( + dispatch_input_optional_string(key: "description", value: input.description), + concat( + [kv(key: "required", value: yaml_bool(b: input.required))], + concat( + dispatch_input_optional_string(key: "default", value: input.default), + [kv(key: "type", value: yaml_string(s: dispatch_input_type_label(t: input.type)))] + ) + ) + )) + ) +} + +fn workflow_dispatch_yaml(inputs: List) -> YamlValue { + if length(inputs) == 0 { + YamlNull + } else { + yaml_mapping(entries: [ + kv( + key: "inputs", + value: yaml_mapping(entries: map(inputs, input => dispatch_input_yaml(input: input))) + ) + ]) + } +} + +data workflow_dispatch_input_projection_note: String = "WorkflowDispatch.inputs was modeled in extdeps.github.actions but this serializer discarded the entire list and emitted workflow_dispatch: null. That specification-without-execution gap is now closed: every modeled input is projected into the workflow syntax, while the empty list deliberately retains the compact null form. The CI heal revalidation input is the first production consumer and its witness reads the projected YamlValue rather than trusting generated text." + fn workflow_trigger_entry(trigger: WorkflowTrigger) -> YamlKeyValue { match trigger { - WorkflowDispatch { inputs: _ } => - kv(key: "workflow_dispatch", value: YamlNull) + WorkflowDispatch { inputs: inputs } => + kv(key: "workflow_dispatch", value: workflow_dispatch_yaml(inputs: inputs)) Push { branches: bs, paths: ps } => push_trigger_yaml(branches: bs, paths: ps) PullRequest { branches: bs, types: ts } => diff --git a/dag/gunbc/ci_materialization_gate.dag b/dag/gunbc/ci_materialization_gate.dag index c262e6d2454..69797e1130d 100644 --- a/dag/gunbc/ci_materialization_gate.dag +++ b/dag/gunbc/ci_materialization_gate.dag @@ -1,11 +1,14 @@ module gunbc.ci_materialization_gate - -data ci_materialization_gate_note: String = "The live binding: the ladder run over the ACTUAL emitted workflow (gunbc.ci_workflow data row), never a fixture copy of it. Demands, exemption identities, and fresh-effect scripts are all resolved against the same authority the ci.yml is emitted from, so a workflow edit that introduces cross-job duplication without a covering provider reds the enrolled witness in the same CI run that would have paid the duplication. Post-fold reality (ci_regen job folded into the ci job 2026-07-11): the workflow now has a SINGLE building job, so the release build is one demand -> AcceptedSingleRecompute (state 5: a single undeclared demand needs no provider, a cache there is dead weight), and the ladder holds WITH AND WITHOUT the sccache provider. The cross-job duplication the ladder refutes is now carried as the discriminating RED control by the synthetic placement_grain witness (two independently-building jobs -> AuthoredDuplication/RefusedNoProvider), which the live witness's demand==1 / discharged==0 pins guard against reintroducing. Fresh effects: the floor cgroup-peak measurement scripts (a memory.peak read is a new fact each run, never memoizable — the rust_tests cgroup-peak measurement was the prior subject; it retired with the rust_tests job 2026-07-11, and the ci-job floor peak pre/post reads are the same measurement category) and every deploy stage script (a deploy is the effect being the use); all resolved by projection, not copied strings." +data ci_materialization_gate_note: String = "The live binding: the ladder run over the ACTUAL emitted workflow (gunbc.ci_workflow data row), never a fixture copy of it. Demands, exemption identities, and fresh-effect scripts are all resolved against the same authority the ci.yml is emitted from, so a workflow edit that introduces cross-job duplication without a covering provider reds the enrolled witness in the same CI run that would have paid the duplication. Post-fold reality (ci_regen job folded into the ci job 2026-07-11): the workflow now has a SINGLE building job, so the release build is one demand -> AcceptedSingleRecompute (state 5: a single undeclared demand needs no provider, a cache there is dead weight), and the ladder holds WITH AND WITHOUT the sccache provider. The cross-job duplication the ladder refutes is now carried as the discriminating RED control by the synthetic placement_grain witness (two independently-building jobs -> AuthoredDuplication/RefusedNoProvider), which the live witness's demand==1 / discharged==0 pins guard against reintroducing. Fresh effects: the floor cgroup-peak measurement scripts (a memory.peak read is a new fact each run, never memoizable — the rust_tests cgroup-peak measurement was the prior subject; it retired with the rust_tests job 2026-07-11, and the ci-job floor peak pre/post reads are the same measurement category), every deploy stage script (a deploy is the effect being the use), and the heal-revalidation exact-head preflight (git HEAD is a new checkout fact in each isolated job and must be observed there, never memoized or discharged from another job); all resolved by projection, not copied strings." fn ci_fresh_effect_scripts() -> List { concat( - [step_run_script(s: ci_floor_peak_pre_step()), step_run_script(s: ci_floor_peak_post_step())], + [ + step_run_script(s: ci_floor_peak_pre_step()), + step_run_script(s: ci_floor_peak_post_step()), + ci_heal_revalidation_preflight_script(), + ], map(gunbc_ci_deploy_stages, s => gunbc_ci_deploy_invoke(stage: s)) ) } @@ -131,6 +134,17 @@ fn ci_exempt_fresh_verdict_count() -> Int { |> count() } +fn ci_heal_revalidation_preflight_is_fresh_effect() -> Bool { + let identity = ci_heal_revalidation_preflight_script() + let demand_count = ci_materialization_demands() + |> filter(d => d.identity == identity) + |> count() + let verdict_count = ci_materialization_verdicts() + |> filter(v => verdict_is_exempt_fresh(v: v, identity: identity)) + |> count() + demand_count > 1 && verdict_count == 1 +} + fn ci_uses_steps_skipped_count() -> Int { workflow_uses_steps_count(w: ci_workflow) } diff --git a/dag/gunbc/ci_spec.dag b/dag/gunbc/ci_spec.dag index 3bcdf1664d8..970a6b159a6 100644 --- a/dag/gunbc/ci_spec.dag +++ b/dag/gunbc/ci_spec.dag @@ -479,6 +479,24 @@ fn gunbc_ci_heal_regen_invoke() -> String { ) } +data ci_heal_dispatch_entry: String = "dag/tools/ci_heal_dispatch.dag" +data ci_heal_dispatch_function: String = "main" + +fn gunbc_ci_heal_dispatch_invoke() -> String { + concat( + "GUNBC_HEALED_HEAD=\"$HEALED_HEAD\" ", + gunbc_run_shell( + source_roots: witness_layer_roots, + entry: ci_heal_dispatch_entry, + function: ci_heal_dispatch_function, + rooted: true, + claim_run: false + ) + ) +} + +data ci_heal_dispatch_invoke_note: String = "After a successful push the heal invokes tools.ci_heal_dispatch, which binds the modeled github.Workflows.CreateDispatch operation with ref=HEALED_HEAD (immutable commit SHA) and expected_healed_sha=HEALED_HEAD so the run subject and executed tree cannot diverge if the branch advances. A transport refusal makes the gunbc invocation nonzero; the surrounding heal script classifies HealDispatchRefused, keeps revalidation required, and fails loudly. There is deliberately no fallback to the ordinary push event and no silent retry." + data ci_heal_binary_source_skew_note: String = "THE PAIRING THE HEAL JOB NEVER MODELED (incident 2026-07-29). A generated artifact's identity is (authority source x compiler), and this job silently pairs TWO DIFFERENT REVISIONS of that product: the release binary comes from `build`, which uses the default pull_request checkout — the MERGE ref (main + PR) — while this job checks out `github.head_ref`, the BRANCH HEAD, because it pushes the regeneration back (ci_heal_branch_checkout_note reasons carefully about the push semantics and never about the binary's provenance; it calls build's output 'the release gunbc binary', treating a projection of one revision as a context-free tool). The skew is latent until a seed change adds a Rust->.dag call: then the merge-ref binary invokes a `.dag` function the branch-head tree does not contain, `lookup_fn` misses, and the run dies mid-regen. Live receipt: #7348 landed the scoped-run observation seed, whose Rust calls gunbc.observation_seed_render.scoped_run_begin_write_measured; every open PR whose branch head predated it went red at once (#7392, #7394, #7395 — identical failure, none of them at fault), while main stayed green because ci_regen_heal_if skips this job on push. Reproduced by execution: ONE binary built from the merge ref, run against a pre-#7348 tree -> the exact CI failure; run against the same tree with origin/main merged in -> ExitSuccess, zero drift. The guard below refuses the unsound pairing instead of discovering it as a mid-regen crash." data ci_heal_binary_source_skew_guard_note: String = "THE COMPARAND IS THE BUILT-FROM REVISION, NOT A BRANCH NAME (operator ruling 2026-07-29). The first cut of this guard compared against `origin/main`, and that was wrong on the operator's own objection: `origin/main` names several different things — the one on this runner, the one on a developer's machine, and the actual source of truth — so a guard keyed on it asserts a relationship between the tree and WHICHEVER main this box last fetched, and can even race an advance mid-run. There is no ambiguity to resolve because the question was never about main: it is 'was this binary compiled from a revision this tree can satisfy'. `github.sha` answers it exactly — on a pull_request it IS the merge commit the build job checked out, so the guard compares the tree against the binary's own provenance, in the same workflow run, with no floating ref anywhere. The guard fails closed if that revision cannot be resolved: an unverifiable provenance is a refusal, never an assumed-fine.\n\nPRECISION IS ALSO THE POINT (DESIGN §5 — refuse, never widen; and never manufacture friction the defect does not warrant). A blanket 'tree must equal the built-from revision' would red nearly every PR to catch a rare pairing — a wall priced in other people's time. The DECIDABLE condition that actually matters is narrower: the binary is unsound against this tree exactly when the built-from revision carries SEED commits (src/v1 — the Rust the binary is compiled from) this tree lacks, because only those can introduce a Rust->.dag expectation the tree cannot satisfy. `git rev-list HEAD..$BUILT_FROM -- src/v1` is exactly that set: empty on the overwhelming majority of PRs (a .dag-only advance cannot skew a compiled binary), non-empty precisely in the #7348 shape. VERIFIED BY EXECUTION on the incident itself: at the pre-#7348 branch point the set is two commits and one of them IS 445bac31c (#7348), so the guard names the responsible commit in its own refusal; at current main and at the same branch after the advance was merged in, the set is empty and the guard is silent — the heal that went green on #7395 is the live receipt for the passing arm. On non-empty the step REFUSES rather than regenerating with a compiler that disagrees with the tree, which is the fabricated-plausible-output arm §5 forbids: main_wet would write whatever artifacts that mismatched pair produces and the commit-push step would push them to the branch. NOT IN SCOPE: preventing a stale branch from MERGING at all. That is merge-admission policy, it needs a source-of-truth model this repo does not have yet (operator: the SCM lane after v1 deletion), and this guard deliberately does not pretend to supply one — it protects the one pairing this job has agency over." @@ -489,7 +507,7 @@ fn gunbc_ci_heal_binary_source_skew_guard_script() -> String { ci_heal_binary_source_skew_guard_script() } -data ci_heal_commit_push_note: String = "The heal COMMIT+PUSH step: a GitHub Actions run: foreign-executor context (the shell-intent design's bootstrap/foreign-executor case that renders through bash), so the git commit/push is a hand-authored shell string like the deploy invoke and the release-bins unpack script beside it. COMMIT SCOPE IS ARTIFACT-ONLY BY CONSTRUCTION (review 41703, DESIGN §5 no-silent-widen): staging is `git add` over EXACTLY committed_generated_artifact_paths() (the registry the drift gate guards and the exact set main_wet writes) — never `git add -A`, so an incidental dirty file on the runner (checkout residue, line-ending normalization, leftover state) can never be swept into an unattended push. Each path is guarded by a `[ -e ]` existence test (ci_heal_git_add_lines): a registered artifact that is absent on this tree — e.g. one a later PR deleted while its registry row lingered (the #7121 FleetConvergeArtifact incident) — is loudly echoed and skipped, never an exit-128 `git add` pathspec error that fails the whole heal; the drift gate remains the wall for a registered-but-missing artifact, the heal just commits what main_wet actually produced. The commit fires ONLY when `git diff --cached --quiet` reports a staged change — i.e. only when main_wet actually healed a registry artifact — so a clean tree is a no-op, and the byte-idempotent fixed point makes the healed commit's own re-run a no-op that terminates the loop. The push target is the TRIGGERING branch, not hardcoded main: `git push origin HEAD:${{ github.head_ref || github.ref_name }}` resolves to the PR source branch on a pull_request and to main on a push (operator-directed 2026-07-23: heal pushes to PRs so drift is repaired on the PR branch before it reaches main). The push authenticates with the job's GITHUB_TOKEN (persisted by actions/checkout, which checked out that same branch head) and needs the job-scoped contents:write grant. Loop termination is NOT a re-run of CI on the healed commit: a push made with the workflow's GITHUB_TOKEN does NOT trigger a new workflow run (GitHub's cascade-prevention is by design), so the healed commit fires no follow-on run — termination is guaranteed instead by the byte-idempotent fixed point itself, PROVEN pre-merge by generated_artifact_drift_test.witness_committed_is_fixed_point (committed bytes == artifact_generate) with its RED control, so a second heal would be a no-op even if one were triggered (review 41782 correction: the earlier 'verified by execution on the healed commit' claim was wrong — no such run exists). The healed artifacts are re-validated by the batch-0 drift gate on the NEXT unrelated PR/push, not on the heal commit, which is correct-by-construction (it is main_wet's own output). A concurrent advance on the target branch makes the push a non-fast-forward that fails LOUDLY (never a force-push), and the next run on that branch retries. A fork PR's branch is not writable by the workflow GITHUB_TOKEN, so a fork heal push fails loudly rather than silently — fork heals are out of scope; the fleet's PR model is same-repo session branches, which are pushable." +data ci_heal_commit_push_note: String = "The heal COMMIT+PUSH+DISPATCH step creates and classifies a new subject. COMMIT SCOPE remains artifact-only: staging is exactly committed_generated_artifact_paths(), never git add -A, and missing registered paths are loudly skipped. Before mutation it captures PRIOR_HEAD; after the artifact-only commit it captures HEALED_HEAD and the changed artifact population, pushes non-force to the triggering PR branch, then explicitly invokes github.Workflows.CreateDispatch with ref=HEALED_HEAD (commit SHA) and expected_healed_sha=HEALED_HEAD so GitHub's run subject matches the executed tree. A clean staged diff is HealNoChange and exits successfully. A mutation is HealProduced, makes the prior run SupersededByHealedHead, and the old run exits nonzero even after a successful dispatch: no result from tree A can authorize tree B. If push or dispatch fails, the job fails loudly; dispatch failure emits HealDispatchRefused and never assumes the GITHUB_TOKEN push produced an event. The dispatched workflow excludes this heal job, checks out the immutable expected SHA, and refuses on a byte mismatch before witnesses. The byte-idempotent fixed point still proves loop safety, but it is no longer used as a substitute for executing revalidation on the healed head." data ci_heal_commit_push_shell_emit_scaffold: Disposition = Scaffold { dissolves_to: SingleAuthority, @@ -516,18 +534,34 @@ fn ci_heal_shell_lines() -> List { concat( ci_heal_git_add_lines(), [ + "PRIOR_HEAD=$(git rev-parse HEAD)", "if git diff --cached --quiet; then", - " echo \"chore-heal: no generated-artifact drift on this tree; nothing to commit\"", + " echo \"HealNoChange head=$PRIOR_HEAD\"", + " exit 0", "else", + " CHANGED_ARTIFACTS=$(git diff --cached --name-only)", " git commit -m \"chore: regenerate drifted generated artifacts (ci auto-heal)\"", + " HEALED_HEAD=$(git rev-parse HEAD)", " git push origin HEAD:${{ github.head_ref || github.ref_name }}", - " echo \"chore-heal: pushed regenerated generated artifacts to the triggering branch\"", - "fi" + " echo \"HealProduced prior_head=$PRIOR_HEAD healed_head=$HEALED_HEAD changed_artifacts=$CHANGED_ARTIFACTS\"", + " ROOT=$(git rev-parse --show-toplevel)" ] ) ) } fn gunbc_ci_heal_commit_push_script() -> String { - fold(ci_heal_shell_lines(), init: "", f: fn(acc, line) { concat(acc, concat(line, "\n")) }) + concat( + fold(ci_heal_shell_lines(), init: "", f: fn(acc, line) { concat(acc, concat(line, "\n")) }), + concat( + concat(" if ! ", gunbc_ci_heal_dispatch_invoke()), + concat( + " then\n echo \"::error::HealDispatchRefused healed_head=$HEALED_HEAD cause=CreateWorkflowDispatchFailed\" >&2\n exit 1\n fi\n", + concat( + " echo \"SupersededByHealedHead prior_head=$PRIOR_HEAD healed_head=$HEALED_HEAD; revalidation-required\"\n", + " exit 1\nfi\n" + ) + ) + ) + ) } diff --git a/dag/gunbc/ci_workflow.dag b/dag/gunbc/ci_workflow.dag index 6d300c1e7d1..c3d01f761f4 100644 --- a/dag/gunbc/ci_workflow.dag +++ b/dag/gunbc/ci_workflow.dag @@ -17,6 +17,9 @@ import gunbc.ci_spec { import v2.workflow.ci_merge_admission_gate_emit { ci_merge_admission_gate_script, } +import v2.workflow.ci_heal_revalidation_preflight_emit { + ci_heal_revalidation_preflight_script, +} import gunbc.ci_workflow_expressions { ci_deploy_push_to_main_if, ci_regen_heal_if } import gunbc.commit_workflow { commit_gate_roster, project_ci_floor_gates, project_ci_floor_witness_entries } import gunbc.ci_runner_target { gunbc_ci_selected_runner_spec, ci_runner_target_ram_speed_budget, selected_ci_runner_target } @@ -42,6 +45,7 @@ import gunbc.repo_identity { gunbc_default_branch_name } import extdeps.github.actions { Workflow, Job, Step, RunStep, UsesStep, WorkflowTrigger, Push, PullRequest, WorkflowDispatch, MergeGroup, + DispatchInput, InputString, PullRequestActivity, Opened, Synchronize, Reopened, ReadyForReview, WorkflowPermissions, PermRead, PermWrite, ConcurrencySpec, ConcurrencyMappingQueueNotMax, CancelInProgressBool, CancelInProgressExpression, @@ -64,6 +68,38 @@ fn ci_checkout_step() -> Step { } } +fn ci_heal_revalidation_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)), + kv(key: "ref", value: yaml_string(s: "${{ inputs.expected_healed_sha || github.sha }}")) + ] + }, + env: none, + if_condition: none, + continue_on_error: none, + timeout_minutes: none + } +} + +fn ci_heal_revalidation_preflight_step() -> Step { + RunStep { + name: Present { value: "Refuse a heal revalidation checkout that does not name the expected healed SHA" }, + 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 + } +} + data ci_heal_branch_ref_expr: String = "${{ github.head_ref || github.ref_name }}" data ci_heal_branch_checkout_note: String = "The generated-artifact heal checks out the PR SOURCE branch head (github.head_ref) rather than the default detached PR-merge ref, because the heal pushes a regeneration commit BACK to that branch. The heal runs on pull_request only (ci_regen_heal_if), so github.head_ref is always the PR source branch; the `|| github.ref_name` fallback is retained as a defensive no-op for that expression. push (main), merge_group, and workflow_dispatch are excluded by ci_regen_heal_if — main is not auto-healed (its ci drift gate reds instead) and a queue ref (gh-readonly-queue/*) is not a pushable branch." @@ -132,9 +168,10 @@ fn ci_native_cache_prelude_order_bridge() -> String { data ci_native_cache_prelude_order_bridge_note: String = "Adjacency-as-proxy ordering witness (not a structural Step-order predicate): ci_native_cache_prelude_order_bridge builds the setup-rust HOME env line immediately followed by the native-cache step name at the emitter's six-space yaml indent. witness_prelude_native_cache_root_step_follows_setup_rust asserts expected_ci_yml/falsifier_yml contain that substring. The real invariant is only that segment derivation runs after setup-rust-toolchain installs rustc; this check over-constrains to textual adjacency and can false-RED on a legitimate step inserted between setup-rust and native-cache, emitter yaml reformatting, or setup-rust gaining fields after HOME — but not false-green if ordering regresses. A hand-rolled match on Step would be the structural alternative; non-fold-residue forbids the wildcard arms that predicate would need (receipt: nfr floor on 14bc815db4). Dissolves when prelude ordering is witnessed without coproduct-residue match arms." -fn ci_prelude_steps() -> List { +fn ci_prelude_steps_with_checkout(checkout: Step, exact_head_preflight: List) -> List { [ - ci_checkout_step(), + checkout, + ] |> concat(exact_head_preflight) |> concat([ ci_isolate_toolchain_step(), UsesStep { name: Present { value: "Setup Rust" }, @@ -182,7 +219,18 @@ fn ci_prelude_steps() -> List { continue_on_error: none, timeout_minutes: none } - ] + ]) +} + +fn ci_prelude_steps() -> List { + ci_prelude_steps_with_checkout(checkout: ci_checkout_step(), exact_head_preflight: []) +} + +fn ci_heal_revalidation_prelude_steps() -> List { + ci_prelude_steps_with_checkout( + checkout: ci_heal_revalidation_checkout_step(), + exact_head_preflight: [ci_heal_revalidation_preflight_step()] + ) } data ci_artifact_consumer_prelude_note: String = "Checkout-only prelude for deploy jobs that consume the build job's release-bins artifact. Rust release-bin build + isolated rustup stay on build only — deploy verifies and runs prebuilt binaries." @@ -209,11 +257,11 @@ fn ci_floor_gate_toolchain_step() -> Step { } fn ci_artifact_consumer_prelude_steps() -> List { - [ci_checkout_step()] + [ci_heal_revalidation_checkout_step(), ci_heal_revalidation_preflight_step()] } fn ci_floor_job_prelude_steps() -> List { - [ci_checkout_step(), ci_floor_gate_toolchain_step()] + [ci_heal_revalidation_checkout_step(), ci_heal_revalidation_preflight_step(), ci_floor_gate_toolchain_step()] } fn ci_floor_spec_from_roster() -> CiSpec { @@ -548,7 +596,7 @@ fn ci_heal_commit_push_step() -> Step { } } -data ci_heal_job_note: String = "CI auto-heal for the DERIVABLE red class (ci-chores lane, operator-directed 2026-07-23: 'i would regen push to PRs please — convenience in general, by the time it gets to main this should be green regardless'). A generated-artifact drift is a red whose remedy is a pure function of the tree — regenerate the projection from its .dag authority — so the pipeline heals it without a human. The job runs on pull_request ONLY (ci_regen_heal_if), needs only build (the release gunbc binary), and is deliberately independent of the ci job's verdict: the drift gate lives IN ci, so a heal gated on ci passing would be skipped exactly when it is needed. It checks out the PR SOURCE branch head (ci_heal_branch_head_checkout_step — github.head_ref), downloads+unpacks the release bins, runs main_wet to rewrite drifted artifacts, then commits+pushes the fix back to THAT branch ONLY if git diff shows a change — so a drifted PR is repaired on its own branch before it can reach main. main is deliberately NOT auto-healed (operator-directed 2026-07-23: 'i think we can disable main pushes for now — i don't expect this to be needed on main — we can just fail CI on main if regen somehow fails there'): main is protected by a ruleset requiring the 'ci' check, so a heal push to main is rejected (GH013, receipt 2026-07-23), and it is not wanted anyway — on main the ci job's own drift gate reds honestly if regen ever drifts, which is the correct main behavior since a change reaching main should already be green from its PR heal. contents:write is scoped to THIS job (least privilege, DESIGN §5): the workflow default stays contents:read, so the whole-corpus ci floor never runs with a push-capable token — only this regen+push job does. Fail-closed: main_wet stops on the first write failure, and the git add stages ONLY registered artifact paths that exist on the tree (ci_heal_git_add_lines — a registered-but-absent artifact, e.g. one deleted by a later PR while its registry row lingered, is loudly skipped and counted, never an exit-128 that fails the whole heal). The loop terminates by construction, NOT by a re-run — a GITHUB_TOKEN-pushed commit does not trigger a new workflow (GitHub's cascade-prevention), so there is no self-verifying second run; loop-safety rests on the byte-idempotent fixed point proven pre-merge by witness_committed_is_fixed_point (generated_artifact_drift_test.dag) with its RED control, so a heal that regenerated a still-drifting artifact would already have failed the drift gate before landing. KNOWN CAVEAT (drift gate still in ci floor): because the heal push does not re-trigger CI, the run that FIRST observes drift still shows the ci job's drift gate red on its pre-heal checkout even though the branch is now auto-fixed; the next push/run is green, and main relies on the PR having healed before merge. Making even that first run green requires moving drift from a ci-floor validation gate to construction (regen owns it), a separate merge-admission change. Judgment-class reds (producer bugs, roster staleness) are untouched — this job only re-derives what the registry already declares generatable, never a human decision. Same-repo session branches (the fleet's PR model) are pushable with the job's GITHUB_TOKEN; a fork PR's branch is not writable by GITHUB_TOKEN and the push would fail loudly (never silently), which is correct — fork heals are out of scope." +data ci_heal_job_note: String = "CI auto-heal for the DERIVABLE red class remains pull_request-only and independent of ci, because the drift gate that triggers it can stop ci's dependent witness population. When regeneration changes a registered artifact, the job pushes the new PR head and explicitly workflow_dispatches CI with expected_healed_sha. The old run is SupersededByHealedHead and deliberately remains non-success; the dispatched run checks out and preflights the immutable SHA before any gate. A dispatch refusal leaves revalidation required and fails loudly. contents:write and actions:write are scoped to this job: contents is needed for the repair push, and Actions write is the narrowest GitHub permission that can invoke CreateWorkflowDispatch (it can start workflows, so it is not granted to build/regen/ci or the workflow default). The heal job is excluded from workflow_dispatch, preventing a dispatch loop. Main is not auto-healed. Judgment-class reds and the separate compile timeout are untouched." fn ci_heal_generated_artifacts_job() -> Job { Job { @@ -571,7 +619,7 @@ fn ci_heal_generated_artifacts_job() -> Job { contents: Present { value: PermWrite }, pull_requests: none, issues: none, - actions: none, + actions: Present { value: PermWrite }, id_token: none } } @@ -583,7 +631,7 @@ fn ci_build_job() -> Job { id: "build", name: none, runner: gunbc_ci_selected_runner_spec(), - steps: concat(ci_prelude_steps(), [ci_fmt_gate_step(), ci_v1_compiler_tests_compile_gate_step(), ci_release_build_step(), ci_release_bins_pack_step(), ci_release_bins_upload_step()]), + steps: concat(ci_heal_revalidation_prelude_steps(), [ci_fmt_gate_step(), ci_v1_compiler_tests_compile_gate_step(), ci_release_build_step(), ci_release_bins_pack_step(), ci_release_bins_upload_step()]), needs: [], env: none, outputs: none, @@ -650,7 +698,17 @@ data ci_merge_group_trigger_note: String = "merge_group trigger: the merge queue data ci_workflow: Workflow = { name: "ci", on: [ - WorkflowDispatch { inputs: [] }, + WorkflowDispatch { + inputs: [ + DispatchInput { + name: "expected_healed_sha", + description: Present { value: "Immutable healed commit required by an auto-heal revalidation run" }, + required: false, + default: none, + type: InputString + } + ] + }, Push { branches: [gunbc_default_branch_name], paths: [] }, PullRequest { branches: [gunbc_default_branch_name], diff --git a/dag/gunbc/heal_revalidation.dag b/dag/gunbc/heal_revalidation.dag new file mode 100644 index 00000000000..7e7d2afe202 --- /dev/null +++ b/dag/gunbc/heal_revalidation.dag @@ -0,0 +1,156 @@ +module gunbc.heal_revalidation + +import std.types { CommitSha, ContentHash, NonEmptyStr } +import gunbc.merge_admission { + CheckCoverage, + check_coverage_admits +} + +type HealOutcome + = HealNoChange { head: CommitSha } + | HealProduced { + prior_head: CommitSha, + healed_head: CommitSha, + changed_artifacts: List + } + +type HealDispatchOutcome + = HealDispatchPending { healed_head: CommitSha } + | HealDispatchAccepted { + healed_head: CommitSha, + run: NonEmptyStr + } + | HealDispatchRefused { + healed_head: CommitSha, + cause: NonEmptyStr + } + +type PriorRunDisposition + = PriorRunStillCurrent { head: CommitSha } + | SupersededByHealedHead { + prior_head: CommitSha, + healed_head: CommitSha + } + +type HealRevalidationState + = HealRevalidationNotRequired { head: CommitSha } + | HealRevalidationRequired { + prior_head: CommitSha, + healed_head: CommitSha, + changed_artifacts: List, + dispatch: HealDispatchOutcome + } + | HealRevalidationCoverageObserved { + prior_head: CommitSha, + healed_head: CommitSha, + changed_artifacts: List, + coverage: CheckCoverage + } + +type HealRevalidationAdmissionVerdict + = HealRevalidationAdmittedNoChange { head: CommitSha } + | HealRevalidationAdmittedExactCoverage { healed_head: CommitSha } + | HealRevalidationDeniedRequired { healed_head: CommitSha, dispatch: HealDispatchOutcome } + | HealRevalidationDeniedCoverage { + healed_head: CommitSha, + coverage: CheckCoverage + } + +type WorkflowDispatchPreflight + = OrdinaryWorkflowDispatch { checkout_head: CommitSha } + | HealWorkflowDispatchHeadMatched { expected_head: CommitSha } + | HealWorkflowDispatchHeadMismatch { + expected_head: CommitSha, + checkout_head: CommitSha + } + +data heal_revalidation_subject_universe_note: String = "HEAL REVALIDATION IS A TOTAL CLASSIFICATION OVER EVERY HEAD THE HEAL CAN PRODUCE (operator mandate 2026-08-01). HealNoChange creates no new subject. HealProduced creates an immutable healed_head, immediately supersedes prior_head, and starts in HealRevalidationRequired; Pending, Accepted, and Refused dispatches all remain refusals until CheckCoverageComplete for that exact healed head and the current nonempty roster admits through gunbc.merge_admission. Adding a heal path means adding a HealOutcome arm, which turns the exhaustive folds red until that new subject is classified. There is no unknown-head arm and no rerun-everything fallback." + +data heal_revalidation_external_boundary_note: String = "This module and the CI workflow close the in-repository model/realization loop: a produced heal explicitly dispatches a new run and exact-head coverage is required. The external dashboard readout that historically treated an absent run as ok, and its separate aggregate conflation of Cancelled superseded runs with failed runs, live outside this repository and are not fixed or claimed fixed here." + +fn heal_revalidation_initial(outcome: HealOutcome) -> HealRevalidationState { + match outcome { + HealNoChange { head } => HealRevalidationNotRequired { head: head } + HealProduced { prior_head, healed_head, changed_artifacts } => + HealRevalidationRequired { + prior_head: prior_head, + healed_head: healed_head, + changed_artifacts: changed_artifacts, + dispatch: HealDispatchPending { healed_head: healed_head } + } + } +} + +fn prior_run_disposition(outcome: HealOutcome) -> PriorRunDisposition { + match outcome { + HealNoChange { head } => PriorRunStillCurrent { head: head } + HealProduced { prior_head, healed_head, changed_artifacts: _ } => + SupersededByHealedHead { prior_head: prior_head, healed_head: healed_head } + } +} + +fn classify_workflow_dispatch_preflight( + expected_healed_head: CommitSha?, + checkout_head: CommitSha, +) -> WorkflowDispatchPreflight { + match expected_healed_head { + Absent => OrdinaryWorkflowDispatch { checkout_head: checkout_head } + Present { value: expected } => + if expected == checkout_head { + HealWorkflowDispatchHeadMatched { expected_head: expected } + } else { + HealWorkflowDispatchHeadMismatch { + expected_head: expected, + checkout_head: checkout_head + } + } + } +} + +fn classify_heal_revalidation_admission( + state: HealRevalidationState, + required_roster: ContentHash, + required_gates: List, +) -> HealRevalidationAdmissionVerdict { + match state { + HealRevalidationNotRequired { head } => + HealRevalidationAdmittedNoChange { head: head } + HealRevalidationRequired { + prior_head: _, healed_head, changed_artifacts: _, dispatch + } => + HealRevalidationDeniedRequired { healed_head: healed_head, dispatch: dispatch } + HealRevalidationCoverageObserved { + prior_head: _, healed_head, changed_artifacts: _, coverage + } => + if check_coverage_admits( + coverage: coverage, + required_head: healed_head, + required_roster: required_roster, + required_gates: required_gates + ) { + HealRevalidationAdmittedExactCoverage { healed_head: healed_head } + } else { + HealRevalidationDeniedCoverage { + healed_head: healed_head, + coverage: coverage + } + } + } +} + +fn heal_revalidation_admits( + state: HealRevalidationState, + required_roster: ContentHash, + required_gates: List, +) -> Bool { + match classify_heal_revalidation_admission( + state: state, + required_roster: required_roster, + required_gates: required_gates + ) { + HealRevalidationAdmittedNoChange { head: _ } => true + HealRevalidationAdmittedExactCoverage { healed_head: _ } => true + HealRevalidationDeniedRequired { healed_head: _, dispatch: _ } => false + HealRevalidationDeniedCoverage { healed_head: _, coverage: _ } => false + } +} diff --git a/dag/gunbc/merge_admission.dag b/dag/gunbc/merge_admission.dag index 394c5894e0b..9f6bbd0d157 100644 --- a/dag/gunbc/merge_admission.dag +++ b/dag/gunbc/merge_admission.dag @@ -183,7 +183,7 @@ type CheckCoverage data check_coverage_subject_universe_note: String = "CHECK COVERAGE IS A TOTAL CLASSIFICATION OVER AN EXPLICIT SUBJECT UNIVERSE (operator mandate 2026-08-01). The subject is (required PR head, required gate-roster identity, nonempty required gate population). No check runs is CheckCoverageAbsent, never an empty list that all() can call green. A run still executing is Running. A dependency stop is Stopped and carries both the completed and UNEXECUTED populations plus a cause, so batch-1 drift stopping the witness batches cannot masquerade as a witness verdict. Complete is the only arm admission examines for success. Stale carries both observed and required identities; it is not repaired by relabeling the observation. Adding a coverage state requires a new coproduct arm and turns every exhaustive consumer red until classified — unclassified is structurally unavailable." -data check_coverage_external_consumer_boundary_note: String = "BOUNDARY, NOT AN END-TO-END CLOSURE CLAIM. This module is the repository's admission authority and now makes the correct semantics representable and executable. The live fail-open observed 2026-08-01 was in the external dashboard readout: it reported no failing or pending checks with ok=true when the healed head had NO run. That consumer lives outside this repository and is not changed here. Until it conforms to classify_check_coverage_admission, the operational rule is stricter than its readout: never merge unless an executing run explicitly names the current PR head and reaches every required witness; an auto-heal head with no subsequent run is untested." +data check_coverage_external_consumer_boundary_note: String = "BOUNDARY, NOT AN END-TO-END CLOSURE CLAIM. This module is the repository's admission authority and now makes the correct semantics representable and executable. The live fail-open observed 2026-08-01 was in the external dashboard readout: it reported no failing or pending checks with ok=true when the healed head had NO run. That consumer lives in ctrl session-dashboard (lib/summarize_checks.mjs + merge gate helpers); gunbc records the adoption requirement here, ctrl carries the consumer fix. Until the dashboard conforms to classify_check_coverage_admission, the operational rule is stricter than its readout: never merge unless an executing run explicitly names the current PR head and reaches every required witness; an auto-heal head with no subsequent run is untested." type CheckCoverageAdmissionVerdict = CheckCoverageAdmitted diff --git a/dag/test/claim/ci_heal_job_witness_test.dag b/dag/test/claim/ci_heal_job_witness_test.dag index e2bec10f94d..879c94e1aa5 100644 --- a/dag/test/claim/ci_heal_job_witness_test.dag +++ b/dag/test/claim/ci_heal_job_witness_test.dag @@ -14,12 +14,14 @@ import extdeps.languages.yaml.types { import gunbc.ci_spec { ci_heal_generated_artifact_regen_function, ci_heal_generated_artifact_gate_entry, + ci_heal_dispatch_entry, gunbc_ci_heal_commit_push_script } import gunbc.generated_artifact { committed_generated_artifact_paths, CiYamlArtifact, artifact_path } import gunbc.ci_workflow_expressions { ci_regen_heal_if } import extdeps.github.actions { Job, Workflow, WorkflowPermissions, PermissionLevel, PermWrite, PermRead, + WorkflowDispatch, Push, PullRequest, Schedule, WorkflowCall, MergeGroup, Step, UsesStep, RunStep } @@ -49,6 +51,22 @@ fn job_has_no_write(j: Job) -> Bool { } } +fn job_actions_is_write(j: Job) -> Bool { + match j.permissions { + Present { value: wp } => + match wp.actions { Present { value: l } => perm_is_write(p: l) Absent => false } + Absent => false + } +} + +fn job_has_no_actions_write(j: Job) -> Bool { + match j.permissions { + Absent => true + Present { value: wp } => + match wp.actions { Present { value: l } => !perm_is_write(p: l) Absent => true } + } +} + fn workflow_contents_is_read(w: Workflow) -> Bool { match w.permissions { Present { value: wp } => @@ -86,6 +104,28 @@ test fn contents_write_is_scoped_to_heal_only() -> Bool { && job_contents_is_write(j: ci_heal_generated_artifacts_job()) } +test fn actions_write_is_scoped_to_heal_only() -> Bool { + job_has_no_actions_write(j: ci_build_job()) + && job_has_no_actions_write(j: ci_job()) + && job_actions_is_write(j: ci_heal_generated_artifacts_job()) +} + +test fn workflow_dispatch_carries_optional_exact_healed_sha_input() -> Bool { + fold(ci_workflow.on, init: false, f: fn(acc, trigger) { + acc || match trigger { + WorkflowDispatch { inputs } => + fold(inputs, init: false, f: fn(found, row) { + found || (row.name == "expected_healed_sha" && !row.required) + }) + Push { branches: _, paths: _ } => false + PullRequest { branches: _, types: _ } => false + Schedule { cron: _ } => false + WorkflowCall { inputs: _ } => false + MergeGroup => false + } + }) +} + test fn heal_regen_targets_generated_artifact_main_wet() -> Bool { (ci_heal_generated_artifact_regen_function == "main_wet") && (ci_heal_generated_artifact_gate_entry == "dag/tools/generated_artifact_gate.dag") @@ -111,6 +151,25 @@ test fn heal_push_targets_triggering_branch() -> Bool { && !string_contains(s: script, pattern: "git push origin HEAD:main") } +test fn heal_produced_dispatches_and_supersedes_old_run() -> Bool { + let script = gunbc_ci_heal_commit_push_script() + (ci_heal_dispatch_entry == "dag/tools/ci_heal_dispatch.dag") + && string_contains(s: script, pattern: "PRIOR_HEAD=$(git rev-parse HEAD)") + && string_contains(s: script, pattern: "HEALED_HEAD=$(git rev-parse HEAD)") + && string_contains(s: script, pattern: "GUNBC_HEALED_HEAD=\"$HEALED_HEAD\"") + && !string_contains(s: script, pattern: "GUNBC_HEAL_BRANCH_REF") + && string_contains(s: script, pattern: "SupersededByHealedHead") + && string_contains(s: script, pattern: "revalidation-required") + && string_contains(s: script, pattern: "exit 1") +} + +test fn dispatch_failure_is_loud_and_has_no_push_event_fallback() -> Bool { + let script = gunbc_ci_heal_commit_push_script() + string_contains(s: script, pattern: "HealDispatchRefused") + && string_contains(s: script, pattern: "CreateWorkflowDispatchFailed") + && !string_contains(s: script, pattern: "workflow will be triggered by push") +} + fn yaml_value_is_branch_ref(v: YamlValue) -> Bool { match v { YamlString { value: s } => s == ci_heal_branch_ref_expr @@ -142,4 +201,3 @@ fn step_checks_out_branch(s: Step) -> Bool { test fn heal_checks_out_triggering_branch() -> Bool { fold(ci_heal_generated_artifacts_job().steps, init: false, f: (acc, s) => acc || step_checks_out_branch(s: s)) } - diff --git a/dag/test/claim/ci_materialization_witness_test.dag b/dag/test/claim/ci_materialization_witness_test.dag index 65314f800c4..6909c7b31c5 100644 --- a/dag/test/claim/ci_materialization_witness_test.dag +++ b/dag/test/claim/ci_materialization_witness_test.dag @@ -5,6 +5,7 @@ import gunbc.ci_materialization { ci_catalog_projection_refusals } import gunbc.ci_materialization_gate { ci_materialization_ladder_holds_live, ci_materialization_holds_without_sccache, + ci_heal_revalidation_preflight_is_fresh_effect, } import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } @@ -23,3 +24,7 @@ test fn ci_ladder_holds_without_sccache_single_build() -> Bool { test fn ci_catalog_projection_has_no_refusals() -> Bool { ci_catalog_projection_refusals() == 0 } + +test fn ci_heal_revalidation_preflight_is_a_fresh_checkout_observation() -> Bool { + ci_heal_revalidation_preflight_is_fresh_effect() +} diff --git a/dag/test/claim/heal_revalidation_integration_witness_test.dag b/dag/test/claim/heal_revalidation_integration_witness_test.dag new file mode 100644 index 00000000000..d5545928e67 --- /dev/null +++ b/dag/test/claim/heal_revalidation_integration_witness_test.dag @@ -0,0 +1,45 @@ +module test.claim.heal_revalidation_integration_witness + +import test.claim.heal_revalidation_witness { + heal_no_change_creates_no_revalidation_obligation, + heal_produced_is_immediately_revalidation_required, + produced_head_supersedes_prior_run, + accepted_dispatch_is_not_revalidation, + refused_dispatch_stays_required_and_located, + only_exact_healed_head_complete_coverage_admits, + manual_dispatch_without_expected_sha_cannot_masquerade_as_heal_revalidation, + expected_sha_preflight_matches_or_refuses_exactly +} +import test.claim.workflow_dispatch_input_witness { + workflow_dispatch_nonempty_inputs_are_realized_not_dropped, + workflow_dispatch_empty_inputs_preserve_null_projection +} +import test.claim.ci_heal_job_witness { + actions_write_is_scoped_to_heal_only, + workflow_dispatch_carries_optional_exact_healed_sha_input, + heal_produced_dispatches_and_supersedes_old_run, + dispatch_failure_is_loud_and_has_no_push_event_fallback +} +import v2.workflow.ci_heal_revalidation_preflight_emit_test { + preflight_is_exact_head_and_precedes_any_witness, + preflight_absent_input_is_ordinary_manual_ci +} + +test fn heal_revalidation_integration_witnesses_hold() -> Bool { + heal_no_change_creates_no_revalidation_obligation() + && heal_produced_is_immediately_revalidation_required() + && produced_head_supersedes_prior_run() + && accepted_dispatch_is_not_revalidation() + && refused_dispatch_stays_required_and_located() + && only_exact_healed_head_complete_coverage_admits() + && manual_dispatch_without_expected_sha_cannot_masquerade_as_heal_revalidation() + && expected_sha_preflight_matches_or_refuses_exactly() + && workflow_dispatch_nonempty_inputs_are_realized_not_dropped() + && workflow_dispatch_empty_inputs_preserve_null_projection() + && actions_write_is_scoped_to_heal_only() + && workflow_dispatch_carries_optional_exact_healed_sha_input() + && heal_produced_dispatches_and_supersedes_old_run() + && dispatch_failure_is_loud_and_has_no_push_event_fallback() + && preflight_is_exact_head_and_precedes_any_witness() + && preflight_absent_input_is_ordinary_manual_ci() +} diff --git a/dag/test/claim/heal_revalidation_witness_test.dag b/dag/test/claim/heal_revalidation_witness_test.dag new file mode 100644 index 00000000000..0bc2b7ee5fa --- /dev/null +++ b/dag/test/claim/heal_revalidation_witness_test.dag @@ -0,0 +1,175 @@ +module test.claim.heal_revalidation_witness + +import std.content_hash { content_hash_atom } +import std.types { CommitSha, ContentHash } +import extdeps.github.checks { Success } +import gunbc.merge_admission { + CheckCoverageComplete, + CoveredGateConclusion +} +import gunbc.heal_revalidation { + HealOutcome, HealNoChange, HealProduced, + HealDispatchPending, HealDispatchAccepted, HealDispatchRefused, + HealRevalidationNotRequired, HealRevalidationRequired, HealRevalidationCoverageObserved, + PriorRunStillCurrent, SupersededByHealedHead, + OrdinaryWorkflowDispatch, HealWorkflowDispatchHeadMatched, HealWorkflowDispatchHeadMismatch, + HealRevalidationAdmittedNoChange, HealRevalidationAdmittedExactCoverage, + HealRevalidationDeniedRequired, HealRevalidationDeniedCoverage, + heal_revalidation_initial, + prior_run_disposition, + classify_workflow_dispatch_preflight, + classify_heal_revalidation_admission, + heal_revalidation_admits +} + +data prior_head: CommitSha = "1111111111111111111111111111111111111111" +data healed_head: CommitSha = "2222222222222222222222222222222222222222" +data other_head: CommitSha = "3333333333333333333333333333333333333333" +data required_roster: ContentHash = content_hash_atom(value: "heal-roster") +data required_gate: ContentHash = content_hash_atom(value: "heal-gate") + +fn produced() -> HealOutcome { + HealProduced { + prior_head: prior_head, + healed_head: healed_head, + changed_artifacts: [".github/workflows/ci.yml"] + } +} + +fn successful_coverage(head: CommitSha) -> gunbc.merge_admission.CheckCoverage { + CheckCoverageComplete { + head: head, + roster: required_roster, + conclusions: [CoveredGateConclusion { gate: required_gate, conclusion: Success }] + } +} + +test fn heal_no_change_creates_no_revalidation_obligation() -> Bool { + heal_revalidation_admits( + state: heal_revalidation_initial(outcome: HealNoChange { head: prior_head }), + required_roster: required_roster, + required_gates: [required_gate] + ) +} + +test fn heal_produced_is_immediately_revalidation_required() -> Bool { + let state = heal_revalidation_initial(outcome: produced()) + match state { + HealRevalidationRequired { prior_head: prior, healed_head: healed, changed_artifacts, dispatch } => + prior == prior_head + && healed == healed_head + && changed_artifacts == [".github/workflows/ci.yml"] + && match dispatch { + HealDispatchPending { healed_head: pending } => pending == healed_head + HealDispatchAccepted { healed_head: _, run: _ } => false + HealDispatchRefused { healed_head: _, cause: _ } => false + } + HealRevalidationNotRequired { head: _ } => false + HealRevalidationCoverageObserved { prior_head: _, healed_head: _, changed_artifacts: _, coverage: _ } => false + } +} + +test fn produced_head_supersedes_prior_run() -> Bool { + match prior_run_disposition(outcome: produced()) { + SupersededByHealedHead { prior_head: prior, healed_head: healed } => + prior == prior_head && healed == healed_head + PriorRunStillCurrent { head: _ } => false + } +} + +test fn accepted_dispatch_is_not_revalidation() -> Bool { + !heal_revalidation_admits( + state: HealRevalidationRequired { + prior_head: prior_head, + healed_head: healed_head, + changed_artifacts: [".github/workflows/ci.yml"], + dispatch: HealDispatchAccepted { healed_head: healed_head, run: "run-42" } + }, + required_roster: required_roster, + required_gates: [required_gate] + ) +} + +test fn refused_dispatch_stays_required_and_located() -> Bool { + let verdict = classify_heal_revalidation_admission( + state: HealRevalidationRequired { + prior_head: prior_head, + healed_head: healed_head, + changed_artifacts: [".github/workflows/ci.yml"], + dispatch: HealDispatchRefused { + healed_head: healed_head, + cause: "CreateWorkflowDispatch permission denied" + } + }, + required_roster: required_roster, + required_gates: [required_gate] + ) + match verdict { + HealRevalidationDeniedRequired { healed_head: denied, dispatch } => + denied == healed_head && match dispatch { + HealDispatchRefused { healed_head: refused, cause } => + refused == healed_head && string_contains(s: cause, pattern: "permission denied") + HealDispatchPending { healed_head: _ } => false + HealDispatchAccepted { healed_head: _, run: _ } => false + } + HealRevalidationAdmittedNoChange { head: _ } => false + HealRevalidationAdmittedExactCoverage { healed_head: _ } => false + HealRevalidationDeniedCoverage { healed_head: _, coverage: _ } => false + } +} + +test fn only_exact_healed_head_complete_coverage_admits() -> Bool { + heal_revalidation_admits( + state: HealRevalidationCoverageObserved { + prior_head: prior_head, + healed_head: healed_head, + changed_artifacts: [".github/workflows/ci.yml"], + coverage: successful_coverage(head: healed_head) + }, + required_roster: required_roster, + required_gates: [required_gate] + ) && !heal_revalidation_admits( + state: HealRevalidationCoverageObserved { + prior_head: prior_head, + healed_head: healed_head, + changed_artifacts: [".github/workflows/ci.yml"], + coverage: successful_coverage(head: prior_head) + }, + required_roster: required_roster, + required_gates: [required_gate] + ) +} + +test fn manual_dispatch_without_expected_sha_cannot_masquerade_as_heal_revalidation() -> Bool { + match classify_workflow_dispatch_preflight( + expected_healed_head: none, + checkout_head: healed_head + ) { + OrdinaryWorkflowDispatch { checkout_head } => checkout_head == healed_head + HealWorkflowDispatchHeadMatched { expected_head: _ } => false + HealWorkflowDispatchHeadMismatch { expected_head: _, checkout_head: _ } => false + } +} + +test fn expected_sha_preflight_matches_or_refuses_exactly() -> Bool { + let matched = classify_workflow_dispatch_preflight( + expected_healed_head: Present { value: healed_head }, + checkout_head: healed_head + ) + let mismatch = classify_workflow_dispatch_preflight( + expected_healed_head: Present { value: healed_head }, + checkout_head: other_head + ) + match matched { + HealWorkflowDispatchHeadMatched { expected_head } => expected_head == healed_head + OrdinaryWorkflowDispatch { checkout_head: _ } => false + HealWorkflowDispatchHeadMismatch { expected_head: _, checkout_head: _ } => false + } && match mismatch { + HealWorkflowDispatchHeadMismatch { expected_head, checkout_head } => + expected_head == healed_head && checkout_head == other_head + OrdinaryWorkflowDispatch { checkout_head: _ } => false + HealWorkflowDispatchHeadMatched { expected_head: _ } => false + } +} + +data heal_revalidation_closed_denominator_witness_note: String = "These executing witnesses enumerate both current HealOutcome arms and every HealDispatchOutcome arm through exhaustive matches. A newly added heal path or dispatch classification makes this file and the admission folds fail to compile until it is explicitly classified; unclassified cannot become success. The RED controls discriminate dispatch accepted from coverage complete, refused dispatch from an in-flight run, old-head green from healed-head green, and ordinary manual dispatch from heal revalidation." diff --git a/dag/test/claim/workflow_dispatch_input_witness_test.dag b/dag/test/claim/workflow_dispatch_input_witness_test.dag new file mode 100644 index 00000000000..9f45031f52e --- /dev/null +++ b/dag/test/claim/workflow_dispatch_input_witness_test.dag @@ -0,0 +1,79 @@ +module test.claim.workflow_dispatch_input_witness + +import extdeps.github.actions { + WorkflowDispatch, DispatchInput, InputString +} +import extdeps.languages.yaml.gha_workflow { workflow_trigger_entry } +import extdeps.languages.yaml.types { + YamlValue, YamlNull, YamlBool, YamlString, YamlInt, YamlFloat, YamlSequence, YamlMapping +} + +fn value_is_expected_input(v: YamlValue) -> Bool { + match v { + YamlMapping { entries } => + fold(entries, init: false, f: fn(acc, entry) { + acc || (entry.key == "inputs" && match entry.value { + YamlMapping { entries: inputs } => + fold(inputs, init: false, f: fn(found, row) { + found || (row.key == "expected_healed_sha" && match row.value { + YamlMapping { entries: fields } => + fold(fields, init: false, f: fn(has_type, field) { + has_type || (field.key == "type" && match field.value { + YamlString { value } => value == "string" + YamlNull => false + YamlBool { value: _ } => false + YamlInt { lexeme: _ } => false + YamlFloat { lexeme: _ } => false + YamlSequence { elements: _ } => false + YamlMapping { entries: _ } => false + }) + }) + YamlNull => false + YamlBool { value: _ } => false + YamlInt { lexeme: _ } => false + YamlFloat { lexeme: _ } => false + YamlString { value: _ } => false + YamlSequence { elements: _ } => false + }) + }) + YamlNull => false + YamlBool { value: _ } => false + YamlInt { lexeme: _ } => false + YamlFloat { lexeme: _ } => false + YamlString { value: _ } => false + YamlSequence { elements: _ } => false + }) + }) + YamlNull => false + YamlBool { value: _ } => false + YamlInt { lexeme: _ } => false + YamlFloat { lexeme: _ } => false + YamlString { value: _ } => false + YamlSequence { elements: _ } => false + } +} + +test fn workflow_dispatch_nonempty_inputs_are_realized_not_dropped() -> Bool { + let entry = workflow_trigger_entry(trigger: WorkflowDispatch { + inputs: [DispatchInput { + name: "expected_healed_sha", + description: Present { value: "immutable subject" }, + required: false, + default: none, + type: InputString + }] + }) + entry.key == "workflow_dispatch" && value_is_expected_input(v: entry.value) +} + +test fn workflow_dispatch_empty_inputs_preserve_null_projection() -> Bool { + match workflow_trigger_entry(trigger: WorkflowDispatch { inputs: [] }).value { + YamlNull => true + YamlBool { value: _ } => false + YamlInt { lexeme: _ } => false + YamlFloat { lexeme: _ } => false + YamlString { value: _ } => false + YamlSequence { elements: _ } => false + YamlMapping { entries: _ } => false + } +} diff --git a/dag/tools/ci_heal_dispatch.dag b/dag/tools/ci_heal_dispatch.dag new file mode 100644 index 00000000000..a40ca8f869f --- /dev/null +++ b/dag/tools/ci_heal_dispatch.dag @@ -0,0 +1,40 @@ +module tools.ci_heal_dispatch + +import std.process { ProcessExit, ExitSuccess, exit_failure } +import std.types { CommitSha, NonEmptyStr } +import extdeps.shell +import extdeps.github.workflows + +data ci_heal_dispatch_owner: String = "gunb-ai" +data ci_heal_dispatch_repo: String = "gunbc" +data ci_heal_dispatch_workflow_id: String = "ci.yml" + +data ci_heal_dispatch_authority_note: String = "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. CreateDispatch ref is the healed commit SHA (GitHub REST: ref may be a branch, tag, or commit SHA), not the PR branch pointer, so the workflow run subject and executed tree bind to the same immutable head. expected_healed_sha repeats that SHA as the workflow input; checkout and preflight refuse on byte mismatch. GITHUB_TOKEN is resolved solely by the service's auth_source; CreateDispatch has no unused caller-supplied auth_token input and this tool passes no empty sentinel." + +fn required_env(name: NonEmptyStr) -> String? { + let observed = shell.Env.Get(name: name) + match observed.value { + Present { value: raw } => + if trim(raw) == "" { none } else { Present { value: trim(raw) } } + Absent => none + } +} + +func main() -> ProcessExit { + let healed_head = match required_env(name: "GUNBC_HEALED_HEAD") { + Present { value: value } => value as CommitSha + Absent => return exit_failure(reason: "HealDispatchRefused: GUNBC_HEALED_HEAD is absent") + } + let receipt = github.Workflows.CreateDispatch( + owner: ci_heal_dispatch_owner, + repo: ci_heal_dispatch_repo, + workflow_id: ci_heal_dispatch_workflow_id, + ref: healed_head, + expected_healed_sha: healed_head + ) + if receipt.workflow_run_id > 0 { + ExitSuccess + } else { + exit_failure(reason: "HealDispatchRefused: dispatch response carried no workflow run identity") + } +} diff --git a/src/v2/workflow/ci_heal_revalidation_preflight_emit.dag b/src/v2/workflow/ci_heal_revalidation_preflight_emit.dag new file mode 100644 index 00000000000..5b75733b756 --- /dev/null +++ b/src/v2/workflow/ci_heal_revalidation_preflight_emit.dag @@ -0,0 +1,96 @@ +module v2.workflow.ci_heal_revalidation_preflight_emit + +import v2.workflow.orchestration_bash_emit_support { orch_bash_emit_pipeline } +import v2.std.orchestration { + Do, + Exit, + ExprCmdSubst, + ExprLit, + FailFast, + If, + Let, + Not, + Pipeline, + PipelineStep, + Run, + StrEq, + StrNonempty +} +import extdeps.git { shape_git_rev_parse_head_args } + +data ci_heal_expected_head_input_expr: String = "\"${{ inputs.expected_healed_sha }}\"" + +data ci_heal_revalidation_preflight_refused_poison: String = "__GUNBC_ORCH_EMIT_REFUSED__ heal revalidation exact-head preflight emission was rejected; this marker is not valid workflow shell, so generated CI drift refuses rather than widening\n" + +data ci_heal_revalidation_preflight_note: String = "Heal revalidation dispatches on the healed commit SHA (ref and expected_healed_sha), so github.sha and checkout should already name the immutable subject. This preflight still observes git.Core.HeadCommit through extdeps.git's argv shape and compares byte-for-byte before any witness can count — a second binding that refuses if checkout ever diverges from expected_healed_sha. An absent input is an ordinary manual dispatch and does not claim heal revalidation. Control flow is v2.std.orchestration intent and bash is only the GitHub Actions foreign-executor realization." + +fn ci_heal_revalidation_diag(text: String) -> PipelineStep { + Do { + run: Run { + command: concat("echo \"", concat(text, "\"")), + env: [], + redirect: Absent, + capture: Absent + } + } +} + +fn ci_heal_revalidation_mismatch_arm() -> Pipeline { + Pipeline { + steps: [ + ci_heal_revalidation_diag(text: "::error::heal revalidation refused: checkout head $ACTUAL_HEAD does not equal expected healed head $EXPECTED_HEALED_SHA"), + Exit { status: "1" } + ], + on_failure: FailFast + } +} + +fn ci_heal_revalidation_expected_arm() -> Pipeline { + Pipeline { + steps: [ + Let { + name: "ACTUAL_HEAD", + value: ExprCmdSubst { + callee: "git", + args: shape_git_rev_parse_head_args() + } + }, + If { + cond: Not { + inner: StrEq { + lhs: "\"$ACTUAL_HEAD\"", + rhs: "\"$EXPECTED_HEALED_SHA\"" + } + }, + then_: ci_heal_revalidation_mismatch_arm(), + else_: Absent + }, + ci_heal_revalidation_diag(text: "heal revalidation preflight: checkout names expected healed head $EXPECTED_HEALED_SHA") + ], + on_failure: FailFast + } +} + +fn ci_heal_revalidation_preflight_intent() -> Pipeline { + Pipeline { + steps: [ + Let { + name: "EXPECTED_HEALED_SHA", + value: ExprLit { spelling: ci_heal_expected_head_input_expr } + }, + If { + cond: StrNonempty { operand: "\"$EXPECTED_HEALED_SHA\"" }, + then_: ci_heal_revalidation_expected_arm(), + else_: Absent + } + ], + on_failure: FailFast + } +} + +fn ci_heal_revalidation_preflight_script() -> String { + orch_bash_emit_pipeline( + p: ci_heal_revalidation_preflight_intent(), + refused_poison: ci_heal_revalidation_preflight_refused_poison + ) +} diff --git a/src/v2/workflow/ci_heal_revalidation_preflight_emit_test.dag b/src/v2/workflow/ci_heal_revalidation_preflight_emit_test.dag new file mode 100644 index 00000000000..e3c3f2978ae --- /dev/null +++ b/src/v2/workflow/ci_heal_revalidation_preflight_emit_test.dag @@ -0,0 +1,20 @@ +module v2.workflow.ci_heal_revalidation_preflight_emit_test + +import v2.workflow.ci_heal_revalidation_preflight_emit { + ci_heal_revalidation_preflight_script, + ci_heal_revalidation_preflight_refused_poison +} + +test fn preflight_is_exact_head_and_precedes_any_witness() -> Bool { + let script = ci_heal_revalidation_preflight_script() + string_contains(s: script, pattern: "EXPECTED_HEALED_SHA=\"${{ inputs.expected_healed_sha }}\"") + && string_contains(s: script, pattern: "ACTUAL_HEAD=\"$(git rev-parse HEAD)\"") + && string_contains(s: script, pattern: "[ \"$ACTUAL_HEAD\" = \"$EXPECTED_HEALED_SHA\" ]") + && string_contains(s: script, pattern: "heal revalidation refused") + && !string_contains(s: script, pattern: ci_heal_revalidation_preflight_refused_poison) +} + +test fn preflight_absent_input_is_ordinary_manual_ci() -> Bool { + let script = ci_heal_revalidation_preflight_script() + string_contains(s: script, pattern: "[ -n \"$EXPECTED_HEALED_SHA\" ]") +}