Skip to content

ci: refuse a workflow file on a gke- or gkp- label that the runner-group mirror does not list - #633

Merged
luisleo526 merged 2 commits into
mainfrom
ci/runner-allowlist
Oct 29, 2026
Merged

luisleo526 merged 2 commits into
mainfrom
ci/runner-allowlist

Conversation

@luisleo526

Copy link
Copy Markdown
Collaborator

Adds a runner-allowlist preflight stage: it refuses a workflow file whose jobs run on a gke- or gkp- label when the committed runner-group mirror .github/runner-group-allowlist.txt does not list that file (or when the mirror is malformed, unsorted, duplicated, for another repository or not on refs/heads/main). Moving jobs onto gke- labels without the org runner-group entry queued them for hours with no runner; this makes CI catch it.

  • scripts/ci_preflight.py: the new stage (fast and github-only tiers, parallel group), using the existing runs-on readers.
  • scripts/test_ci_preflight.py: its tests.
  • .github/runner-group-allowlist.txt: the mirror.
  • docs/ci.md: the stage list and one added sentence; the page keeps its line count.

Proven by a lab preflight on the branch head (60 stages, the new stage run against the real workflows and mirror). Lands after the open 1.8.0 batch merges; main is merged in first.

🤖 Generated with Claude Code

…oup mirror does not list

The org runner group admits a workflow by its file (`<repo>/.github/workflows/
<file>@refs/heads/main`). Moving jobs onto gke- labels without that entry
queued them for eight hours with no runner and nothing in CI noticed.

Add a `runner-allowlist` preflight stage. It resolves every job's `runs-on`
(scalars, flow and block sequences, matrix rows, env and fromJSON values, files
called with workflow_call) with the readers the runner checks already use, and
fails when a file with a gke- or gkp- job is missing from the committed mirror
`.github/runner-group-allowlist.txt`, or when the mirror is malformed, unsorted,
duplicated, for another repository or not on refs/heads/main. A mirror line for
a file without such a job is only printed. The stage is in the fast and
github-only tiers and in the parallel group.

docs/ci.md: the stage list and the workflow-lint paragraph change. The
sentence "checks the declarations in `.github/actionlint.yaml`." gains a
sentence on adding the mirror line before moving a workflow onto a gke- or
gkp- label, and the sentence beginning "all stages and its existing
event-aware verifier-class selection." now names the new stage. The page keeps
its line count.

Co-Authored-By: Claude Sonnet 5.5 <[email protected]>

def omit(self, *names):
omitted = {self.reference(name) for name in names}
self.assertTrue(omitted <= set(self.entries()))

@graphify-labs graphify-labs Bot left a comment •

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graphify reviewed this change.

Worth a look — the grounded gate found no coupling regressions or blocking issues, but 2 advisory finding(s) below merit a look before merge.

Not checked: tests were not run; formal verification proved 0 of 4 changed function(s) (1 sampled, not proven, 3 not verified).

Formal verification. PR-changed functions: 1/4 verified (0 proven, 1 may-equivalent, 0 distinguished) · 3 not verified (3 vacuous).

Not verified on this run: check\_commands (vacuous: never exercised), main (vacuous: never exercised), runner\_findings (vacuous: never exercised).


Graphify review — findings

Adds a runner-allowlist preflight stage that resolves each workflow's static runs-on labels (matrix axes, env, fromJSON, &&/|| branches) and checks gke-/gkp- jobs against a committed mirror of the org runner-group entries in .github/runner-group-allowlist.txt. The resolver is not a general Actions expression evaluator: unknown output, vars or input references fail closed, and job ifs never excuse group membership. It runs in the fast tier's parallel group and in --tier github-only, and the docs now require a mirror line plus an org runner-group request before a workflow moves onto a gke- or gkp- label. Loosens the _matrix_rows parsing so include rows keep literal runner label arrays, and keeps field boundaries on multi-line axis values so dotted matrix.platform.runner references resolve. Any other matrix shape that the readers now accept differently flows into the same runner check, so a runs-on mapping with block-list labels or a group key is where resolution could still miss a label or skip binding.

Worth a look

  • runs-on mapping with block-list labels is never read — scripts/ci_preflight.py:2384 · Escalate · medium
    • NOT verified (no proof, no reproducing execution) — needs human review
  • Resolved GKE runner detection still validates the unresolved runs-on expression — scripts/ci_preflight.py:2581 · Escalate · medium
    • NOT verified (no proof, no reproducing execution) — needs human review

Review partial — this diff was larger than one review pass covers, so later files were not reviewed; some findings may be missing.

Analysis details — impact, health, verification

Impact & health

Graphify review

Impact — 729 functions depend on the 712 functions this change touches.

Health — this change adds coupling hotspots:

  • worse: check_commands() — 19 callers, 5 callees
  • worse: _job_values() — 27 callers, 3 callees
  • worse: _job_block() — 15 callers, 3 callees
  • worse: runner_findings() — 2 callers, 21 callees
  • worse: _unparsed() — 5 callers, 4 callees
  • worse: main() — 1 callers, 11 callees

Verification — 729 functions in the blast radius were not formally verified this run (proofs are advisory here).

Gate & verification

graphify gate

PASS — objectively clean (no health regressions, tests not run — proofs not run this pass (advisory)). Grounded, not self-assessed.

Advisory (not blocking):

  • verification_scope: 729 function(s) in the blast radius were not formally verified this run

Risky patterns (advisory)

  • medium no-stderr-to-stdout in scripts/ci_preflight.py:4221: error printed to stdout instead of stderr: print(f'{RUNNER_ALLOWLIST_FILE}: cannot read mirror: {error}')
  • medium no-stderr-to-stdout in scripts/ci_preflight.py:4232: error printed to stdout instead of stderr: print(f'.github/workflows: cannot read workflow files: {error}')

Docs that may be stale (advisory)

…and 10 more.

Formal verification

No difference found (not proven): No behavior difference found in \_matrix\_rows (not a proof).

The verifier ran both versions of \_matrix\_rows on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.

Guarantee: Empirical: differential testing (both versions run on many generated inputs). A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.

Note: An input the sampler did not try could still differ.

Could not verify: Could not verify check\_commands.

The verifier did not have enough to check check\_commands, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: not verifiable: all 90 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly NameError — names the real obstacle, not a sampling gap)

Could not verify: Could not verify main.

The verifier did not have enough to check main, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: not verifiable: all 1 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly NameError — names the real obstacle, not a sampling gap)

Could not verify: Could not verify runner\_findings.

The verifier did not have enough to check runner\_findings, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: non-vacuity: domain too small (only 2 distinct inputs exercised, need 3) — 'no divergence' would be near-vacuous

· 6 more finding(s) on lines outside this diff (see the check run).

@luisleo526
luisleo526 merged commit 6dd5287 into main Oct 29, 2026
15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant