Repository navigation
ci: refuse a workflow file on a gke- or gkp- label that the runner-group mirror does not list - #633
Conversation
…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())) |
There was a problem hiding this comment.
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-stdoutinscripts/ci_preflight.py:4221: error printed to stdout instead of stderr: print(f'{RUNNER_ALLOWLIST_FILE}: cannot read mirror: {error}') - medium
no-stderr-to-stdoutinscripts/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)
CHANGELOG.md§ Storage building block (lines 185-195): references changed symbolsentriesCHANGELOG.md§ 1.6.0 — 2026-10-17 (lines 1301-1466): references changed symbolsfailuresCHANGELOG.md§ 1.6.0-rc.1 — 2026-10-14 (lines 1467-1583): references changed symbolsfailuresCHANGELOG.md§ Pine adapter corrections that can change trades ([#350], [#352]) (lines 1757-1815): references changed symbolsentriesbenchmarks/README.md§ Layout (lines 170-198): references changed symbolscombineci/cr150-source-reading.md§ Top block (lines 3-12): references changed symbolsentriesdocker/README.md§ PINEFORGE_OVERRIDES keys (lines 123-176): references changed symbolsentriesdocker/README.md§ The failure line (lines 361-498): references changed symbolsmissingdocs/README.md§ Layout (lines 8-44): references changed symbolsreferencedocs/coverage.md§ External request.* variants (lines 943-967): references changed symbolsexpression
…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).
Adds a
runner-allowlistpreflight 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.txtdoes 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