ci(diet): skip the 24-engine Kani matrix on non-code PRs (tier B)

[avrabe]

The real load win

Kani (CBMC model-checking ~38 engine harnesses) is the heaviest gate on the fleet, and it ran on every PR — including docs- and artifact-only ones that can't possibly change a harness. This skips the matrix when nothing Kani-relevant changed. A docs/artifact PR goes from ~38 Kani jobs to zero.

Deadlock-safe (Kani gate is a required check)

This is the careful part — a naïve path filter on a required check deadlocks all merges. Instead:

• New changes job (light runner, native git diff mirroring the verification-gate ci(verify-gate): scope fast-path + 90m timeout — stop false-cancelling out-of-scope PRs #298 scope check) outputs run=true/false. Fails safe to true on push: main (no PR base) and on any diff error — the required gate never silently no-ops on real code.
• The kani matrix gains needs: changes + if: needs.changes.outputs.run == 'true'.
• kani-gate (the required aggregate; already if: always()) now needs: [changes, kani] and treats a skipped matrix as PASS — so a skip reports the required "Kani gate" check green instead of leaving it pending forever. Fails closed if the scope job itself didn't succeed.

Only the non-required per-engine Kani (<engine>) checks skip; the required Kani gate always runs and reports.

Glob (generous — required gate)

All 38 harnesses live under crates/, so: crates/**, Cargo.toml, Cargo.lock, .github/workflows/kani.yml. push: main stays unfiltered (backstop).

Validation

• Fire path: this PR touches kani.yml (in-glob) → its own matrix runs → validates the new structure + kani-gate-on-success.
• Skip path (matrix skipped, Kani gate still green — the deadlock test): validated post-merge on a docs PR before this is trusted. If a docs PR's "Kani gate" ever goes pending instead of green, revert immediately.

Tier A (non-required gates) shipped in #310 and validated bidirectionally (#305 docs → all 5 skip; #309 wasm.toml → coverage+bazel fire, rocq/lean/spar skip).

🤖 Generated with Claude Code