15 of 18 required contexts declare no timeout-minutes — a hung merge gate is a 6-hour blind wait

[avrabe]

Measured 2026-08-07 against the live branch protection (18 required contexts) and
.github/workflows/*.yml.

Across the repo, 28 of 36 jobs declare no timeout-minutes. Restricted to the
jobs that actually gate the merge:

required context	timeout
Lean proof typecheck (lake build)	90 min
Mutation Testing	240 min
Verification Gate (rivet-driven)	60 min
the other 15	(none — inherits GitHub's 360 min default)

The 15: Bench compile smoke, Cargo Deny, Clippy, Code Coverage, Codegen compile
oracle, Detect changed paths, Detect changed paths (proofs), Format, Fuzz smoke
(60s/target), Miri, Proptest (extended), Rivet validate (artifacts), Security
Audit (RustSec), Supply Chain (cargo-vet), Test.

Why it matters

This is not a wrong-green — it is an indefinite block with no signal. A wedged
job leaves the PR showing "Expected — waiting for status to be reported", which
looks identical to "still running", for six hours. Meanwhile it holds a
self-hosted runner the whole time, and with strict = true every other open PR
queues behind it.

Several of these are seconds of real work (Detect changed paths, Format),
so a 360-minute ceiling is four orders of magnitude off. Detect changed paths
is the worst of the set: it gates 10 of the other 17, so wedging it stalls the
entire suite.

Precedent: the same defect was fixed for the fixture-VM workflows, where a hung
guest produced exactly this 6-hour blind wait before both jobs were bounded.

Suggested fix

Give every required-context job a timeout-minutes sized to a few multiples of
its observed p95, e.g. classifier/format/deny in single digits, Test / Clippy /
Miri / Coverage in the 30-60 range. Observed durations are in the run history;
these should be measured, not guessed.

Worth a guardrail in the same family as check_required_contexts.py: every job
backing a required context must declare timeout-minutes. That is a pure YAML
check with no build, and it fails closed if the workflow set cannot be read.

NOT claimed: that any job currently hangs. This is about the blast radius when
one does.

🤖 Generated with Claude Code

[avrabe]

Opened #411 (branch feat/required-context-timeouts-398) implementing the guardrail this issue proposes.

What shipped

• tools/check_job_timeouts.py — a sibling of check_required_contexts.py that reuses its restricted, PyYAML---cross-checked workflow reader. Every GATEABLE job (exactly the set that gate proves must be required) must declare a static timeout-minutes in (0, 360): missing, ${{ }}-templated, <=0, and >=360 all fail; advisory/undeliverable jobs are out of scope. Runs as a step of rivet-validate, self-test first — same steps-of-this-job rationale you noted for check_required_contexts.py (a new job would itself be gateable and need admin-token branch-protection sync).
• The 15 missing values, sized to a few multiples of each job's observed p95 (cold-cache worst case), read from run history and cited per-job in the workflow comments: classifiers/fmt/deny/vet → 5, audit → 15, test/proptest/bench/coverage/miri/fuzz → 30, clippy/rivet-validate → 45, codegen-oracle → 60.
• REQ-GUARD-CONTEXT-TIMEOUT-001 / TEST-GUARD-CONTEXT-TIMEOUT (real steps + satisfies/verifies links). rivet validate: 0 broken cross-refs.

Oracle (executed, non-vacuous). A 9-row decision table flips a verdict each way (valid→0, missing/templated/zero/non-int/>=360→1, 359→0, advisory/undeliverable-no-timeout→0) plus two fail-closed corpus assertions (zero-gateable and glob-misses-.yaml). Demonstrated live: before, the check exits 1 naming all 15 unbounded contexts; after, exit 0 with "18 gateable job(s)".

Clean-room. An independent pass re-derived 15/18, proved non-vacuity by sabotaging validate_timeout (self-test then fails), and checked PROVEN-vs-ASSUMED honesty — no over-claim.

Honest scoping. PROVEN: every required-context job now declares a static bound in (0, 360) and the gate fails closed. NOT mechanically checked (stated as ASSUMED in the REQ): that the chosen values are well-sized; that GitHub actually cancels at the declared minute; that the GATEABLE set equals the branch-protection-enforced set (the admin-token gap this inherits from check_required_contexts.py). NOT claimed: advisory jobs (e.g. kani, no timeout) are bounded — they can't wedge the merge gate; left to a successor.

Required checks (incl. ~2h Mutation Testing, ~90m Lean) are pending; will merge + cut the release once green.

---

Generated by Claude Code