ci(diet): path-filter the non-required heavy gates on PRs (tier A)

.github/workflows/bazel.yml

@@ -14,8 +14,25 @@ name: Bazel
 on:
   push:
     branches: [main]
+  # PR runs are path-filtered (CI diet): the Bazel build + Component Model
+  # cascade compose the flight component (wasm/cm/flight) and build the
+  # crates/proofs via Bazel. Generous globs — a too-narrow filter would let a
+  # breaking PR skip this and redden main. NON-REQUIRED check; skip never blocks
+  # a merge. push:main stays UNFILTERED (backstop).
   pull_request:
     branches: [main]
+    paths:
+      - 'crates/**'
+      - 'wasm/**'
+      - 'embedded/**'
+      - 'proofs/**'
+      - 'wit/**'
+      - '**/BUILD.bazel'
+      - '**/*.bzl'
+      - 'MODULE.bazel'
+      - 'MODULE.bazel.lock'
+      - '.bazelrc'
+      - '.github/workflows/bazel.yml'
 
 # Group key: head_ref (PR branch name) for pull_request events; ref
 # (e.g. refs/heads/main) for push events — unique per branch/PR.

.github/workflows/coverage.yml

@@ -15,7 +15,19 @@ name: Coverage
 on:
   push:
     branches: [main]
+  # PR runs are path-filtered (CI diet): coverage is a Rust-source concern, so
+  # skip it on PRs that touch no code (docs, artifacts, wit). NON-REQUIRED
+  # check, so a skip never blocks a merge. The push:main trigger above stays
+  # UNFILTERED — every main commit still produces the DO-178C/EN-50128 coverage
+  # evidence record (the backstop).
   pull_request:
+    paths:
+      - 'crates/**'
+      - 'wasm/**'
+      - 'embedded/**'
+      - 'Cargo.toml'
+      - 'Cargo.lock'
+      - '.github/workflows/coverage.yml'
 
 # PRs and non-main branch pushes: cancel superseded runs.
 # Main pushes: never cancel — coverage artifact is the DO-178C/EN-50128

.github/workflows/lean.yml

@@ -17,8 +17,14 @@ name: Lean
 on:
   push:
     branches: [main]
+  # PR runs are path-filtered (CI diet): the Lean proofs (Lyapunov/WCET) are
+  # self-contained under proofs/lean. NON-REQUIRED check; skip never blocks a
+  # merge. push:main stays UNFILTERED (backstop).
   pull_request:
     branches: [main]
+    paths:
+      - 'proofs/lean/**'
+      - '.github/workflows/lean.yml'
 
 concurrency:
   # PRs and non-main branch pushes: cancel superseded runs.

.github/workflows/rocq.yml

@@ -16,8 +16,18 @@ name: Rocq
 on:
   push:
     branches: [main]
+  # PR runs are path-filtered (CI diet): the Rocq/Gappa proofs cover the
+  # relay-math FP kernels, so re-run on proof changes AND on relay-math changes
+  # (drift catch — the proofs hardcode the kernel coefficients). NON-REQUIRED
+  # check; skip never blocks a merge. push:main stays UNFILTERED (backstop).
   pull_request:
     branches: [main]
+    paths:
+      - 'proofs/rocq/**'
+      - 'proofs/gappa/**'
+      - 'crates/relay-math/**'
+      - 'MODULE.bazel'
+      - '.github/workflows/rocq.yml'
 
 concurrency:
   group: rocq-${{ github.head_ref || github.ref }}

.github/workflows/spar.yml

@@ -10,8 +10,15 @@ name: Spar
 on:
   push:
     branches: [main]
+  # PR runs are path-filtered (CI diet): the Spar AADL->WIT drift gate concerns
+  # the architecture models and the generated WIT. NON-REQUIRED check; skip
+  # never blocks a merge. push:main stays UNFILTERED (backstop).
   pull_request:
     branches: [main]
+    paths:
+      - 'spar/**'
+      - 'wit/**'
+      - '.github/workflows/spar.yml'
 
 concurrency:
   # PRs / non-main pushes: cancel superseded runs. Main: never cancel — every