From f4f3a4ca1e872a51e2d61ccb0054f64953357196 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Thu, 23 Jul 2026 17:53:58 +0200
Subject: [PATCH] ci(diet): skip the 24-engine Kani matrix on non-code PRs
 (tier B)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The real load win. Kani model-checks Rust harnesses under crates/**, so a PR
touching only docs, rivet artifacts, wit, or proofs cannot change any harness —
yet every such PR was running all ~38 engine jobs (CBMC model-checking, the
heaviest gate on the fleet). This skips the matrix when nothing Kani-relevant
changed.

Deadlock-safe (Kani gate is a REQUIRED check, so this is done carefully):
- New `changes` job (light runner, native git-diff mirroring verification-gate
  #298) 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`.
- `kani-gate` (the required aggregate, always runs) now `needs: [changes, kani]`
  and treats a `skipped` matrix as PASS — so a skip reports the required check
  green instead of leaving it pending (the deadlock). Fails closed if the scope
  job itself didn't succeed.

Glob is generous (all 38 harnesses live under crates/): crates/**, Cargo.toml,
Cargo.lock, kani.yml. push:main stays unfiltered as the backstop. Net: a
docs/artifact PR goes from ~38 Kani jobs to zero.

Validation: this PR touches kani.yml (in-glob) so its own matrix RUNS (fire path
+ kani-gate-on-success). The SKIP path (matrix skipped, Kani gate still green) is
validated post-merge on a docs PR before trusting it.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
---
 .github/workflows/kani.yml | 64 ++++++++++++++++++++++++++++++++++++--
 1 file changed, 61 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index e560a35..d15e2e4 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -24,8 +24,52 @@ concurrency:
   cancel-in-progress: ${{ github.ref != 'refs/heads/main' }}
 
 jobs:
+  # CI diet (tier B): decide whether the 24-engine matrix needs to run at all.
+  # Kani model-checks Rust harnesses under crates/**, so a PR touching only docs,
+  # rivet artifacts, wit, or proofs cannot change any harness — skip the matrix
+  # and let kani-gate (below) report the required check as pass. On push:main (no
+  # PR base) and on any diff failure this FAILS SAFE to run=true — the required
+  # gate never silently no-ops on a real code change. Native git-diff (no
+  # third-party action), mirroring verification-gate.yml's #298 scope check.
+  changes:
+    name: Detect engine changes
+    runs-on: [self-hosted, linux, x64, light]
+    outputs:
+      run: ${{ steps.scope.outputs.run }}
+    steps:
+      - uses: actions/checkout@v7
+        with:
+          fetch-depth: 0
+      - name: Scope check (do any Kani-relevant files change?)
+        id: scope
+        env:
+          BASE_SHA: ${{ github.event.pull_request.base.sha }}
+        shell: bash
+        run: |
+          if [ -z "${BASE_SHA:-}" ]; then
+            echo "no base sha (push/manual) — run the full matrix (backstop)"
+            echo "run=true" >>"$GITHUB_OUTPUT"; exit 0
+          fi
+          CHANGED=$(git diff --name-only "$BASE_SHA"...HEAD || echo "__diff_failed__")
+          if [ "$CHANGED" = "__diff_failed__" ]; then
+            echo "diff failed — fail-safe to run"
+            echo "run=true" >>"$GITHUB_OUTPUT"; exit 0
+          fi
+          # Kani-relevant: any crate source (all 38 harnesses live under
+          # crates/<engine>/plain/), workspace deps, or this workflow.
+          if printf '%s\n' "$CHANGED" | grep -qE '^(crates/|Cargo\.toml|Cargo\.lock|\.github/workflows/kani\.yml)'; then
+            echo "Kani-relevant files changed — run the matrix"
+            echo "run=true" >>"$GITHUB_OUTPUT"
+          else
+            echo "no Kani-relevant files changed — SKIP the matrix (kani-gate reports pass)"
+            printf 'changed:\n%s\n' "$CHANGED"
+            echo "run=false" >>"$GITHUB_OUTPUT"
+          fi
+
   kani:
     name: Kani (${{ matrix.engine }})
+    needs: changes
+    if: needs.changes.outputs.run == 'true'
     runs-on: [self-hosted, linux, x64, rust-cpu]
     strategy:
       fail-fast: false
@@ -109,9 +153,23 @@ jobs:
   kani-gate:
     name: Kani gate
     runs-on: [self-hosted, linux, x64, light]
-    needs: kani
+    needs: [changes, kani]
     if: always()
     steps:
-      - name: All Kani engines green?
+      - name: All Kani engines green (or correctly skipped)?
+        env:
+          CHANGES_RESULT: ${{ needs.changes.result }}
+          KANI_RESULT: ${{ needs.kani.result }}
         run: |
-          [ "${{ needs.kani.result }}" = "success" ] || { echo "Kani matrix result: ${{ needs.kani.result }}"; exit 1; }
+          # The scope job must have succeeded — otherwise we can't trust the
+          # skip decision, so fail closed.
+          if [ "$CHANGES_RESULT" != "success" ]; then
+            echo "scope (changes) job did not succeed: $CHANGES_RESULT"; exit 1
+          fi
+          # matrix skipped == no Kani-relevant files changed == pass (CI diet,
+          # tier B); the push:main backstop always runs the full matrix.
+          case "$KANI_RESULT" in
+            success) echo "Kani matrix: all engines verified" ;;
+            skipped) echo "Kani matrix: skipped (no Kani-relevant files changed) — OK" ;;
+            *) echo "Kani matrix result: $KANI_RESULT"; exit 1 ;;
+          esac