Run only the CI a pull request can affect

.ci/check-security.sh

@@ -1,30 +1,38 @@
 #!/usr/bin/env bash
 
-# Security checks for elfuse host source files (src/ only).
-# Tests are excluded -- they exercise unsafe patterns deliberately.
+# Security checks for elfuse host source files (src/ only). Tests are excluded
+# -- they exercise unsafe patterns deliberately.
 #
 # 1. Banned functions -- unsafe libc calls with safer alternatives.
 # 2. Credential / secret patterns -- catch accidental key leaks.
 # 3. Dangerous preprocessor -- detect disabled security features.
+# 4. Agent scratch markers -- labels a tool emits to flag a deliberate
+#    simplification. The rationale behind one is often worth keeping; the
+#    label is not, because it reads as a machine's note rather than the
+#    author's, and nothing else in the tree notices when one survives.
 
 set -u -o pipefail
 
 failed=0
 
-# --- Patterns ---
+# Patterns
 banned='(^|[^[:alnum:]_])(gets|sprintf|vsprintf|strcpy|stpcpy|strcat|atoi|atol|atoll|atof|mktemp|tmpnam|tempnam)[[:space:]]*\('
 secrets='(password|secret|api_key|private_key|token)[[:space:]]*=[[:space:]]*"[^"]+'
 dangerous_pp='#[[:space:]]*(undef|define)[[:space:]]+((_FORTIFY_SOURCE[[:space:]]+0)|(__SSP__))'
 comment_only='^[[:space:]]*(//|/\*|\*|\*/)'
 
+# Matched against comments too, unlike the three above, since that is the only
+# place this appears.
+scratch_marker='(^|[^[:alnum:]_])ponytail:'
+
 # Only scan elfuse host source, not tests/ or assembly shim.
 #
-# Each match uses process substitution rather than a shell pipeline:
-# under `pipefail`, an early `grep -q` exit closes its stdin, the
-# upstream filter receives SIGPIPE, and the pipeline returns non-zero
-# even when the pattern matched -- silently dropping real findings.
-# Process substitution puts the filter in a separate process whose exit
-# status doesn't feed back into the matcher.
+# Each match uses process substitution rather than a shell pipeline: under
+# `pipefail`, an early `grep -q` exit closes its stdin, the upstream filter
+# receives SIGPIPE, and the pipeline returns non-zero even when the pattern
+# matched -- silently dropping real findings. Process substitution puts the
+# filter in a separate process whose exit status doesn't feed back into the
+# matcher.
 while IFS= read -r -d '' f; do
     if grep -qE "$banned" < <(grep -vE "$comment_only" -- "$f"); then
         echo "Banned function in $f:"
@@ -41,6 +49,11 @@ while IFS= read -r -d '' f; do
         grep -nE "$dangerous_pp" -- "$f" | grep -vE "$comment_only" || true
         failed=1
     fi
+    if grep -qE "$scratch_marker" -- "$f"; then
+        echo "Agent scratch marker in $f (keep the reasoning, drop the label):"
+        grep -nE "$scratch_marker" -- "$f" || true
+        failed=1
+    fi
 done < <(git ls-files -z -- 'src/*.c' 'src/*.h' 'src/**/*.c' 'src/**/*.h')
 
 if [ $failed -eq 0 ]; then

.claude/skills/elfuse-verify/SKILL.md

@@ -1,6 +1,6 @@
 ---
 name: elfuse-verify
-description: How elfuse validates a change - choosing the lanes for the area you touched, the test matrix, make check, and the Frama-C proof targets declared in mk/analysis.mk, including how to drive the frama-c MCP server on a stuck proof. Use when adding bounds math to src/proved/, writing or repairing ACSL contracts, running or debugging make verify / verify-mutants, touching frama-c-stubs/, adding a test lane, or deciding what to run before calling work done.
+description: How elfuse validates a change - choosing the lanes for the area you touched, the test matrix, make check, and the Frama-C proof targets declared in mk/verify.mk, including how to drive the frama-c MCP server on a stuck proof. Use when adding bounds math to src/proved/, writing or repairing ACSL contracts, running or debugging make verify / verify-mutants, touching frama-c-stubs/, adding a test lane, or deciding what to run before calling work done.
 ---
 
 # Validating an elfuse change
@@ -63,7 +63,7 @@ with `-wp-rte`.
 
 Every `src/proved/` header must have a matching `make verify-<name>` target,
 but the reverse does not hold. A few targets prove a `.c` file directly, each
-for a reason stated in the comment above it in `mk/analysis.mk`; the general
+for a reason stated in the comment above it in `mk/verify.mk`; the general
 one is that the loops in question could only have been described as
 test-covered had they been split into a header.
 
@@ -85,17 +85,33 @@ Apple's 3.81.
 `verify-mutants` accepts `MUTANT_TARGET=<name>`, `MUTANT_JOBS=<n>`, and
 `MUTANT_SINCE=<rev>` for a changed-only run.
 
+`scripts/proof-scope.py` decides which targets a diff can reach, and
+`.github/workflows/verify.yml` builds its jobs from it, so a target the branch
+cannot affect gets no runner. It answers two questions: which targets to prove,
+and, with `--mutation`, which mutation sets to re-run, the second being narrower
+because a file that only schedules the run cannot change whether a target
+rejects a broken source. Every "cannot tell" answer widens back to the whole
+set, and a push to `main` always proves and mutates everything.
+
+Three things follow when adding a target or a proof input. An input reached
+through `-include` or an `-I` the scan does not use is invisible to the closure
+and belongs in `HARNESS_FILES` (or under `STUB_PREFIX`). A file that only picks
+what runs goes in `SCHEDULING_FILES`, and the self-test refuses it if it also
+carries a prover budget or a make invocation. And `proof-scope.py --self-test`,
+run by `.github/workflows/lint.yml`, is what tells you the lists are still
+honest.
+
 ### Adding to src/proved/
 
 Nothing lands there without a proof target -
-`scripts/check-proof-targets.py` (a CI job in `.github/workflows/main.yml`)
+`scripts/check-proof-targets.py` (a CI job in `.github/workflows/lint.yml`)
 fails otherwise. Callers include the header as `proved/<name>.h`.
 
 The routine:
 
 1. Extract the arithmetic into `src/proved/<name>.h` with ACSL contracts.
 2. Add the `VERIFY_<NAME>_SRC` / `VERIFY_<NAME>_MODEL` / `VERIFY_<NAME>_FCTS`
-   variables in `mk/analysis.mk` so the rule template instantiates
+   variables in `mk/verify.mk` so the rule template instantiates
    `verify-<name>`. `typed` is the default choice for a model; see below.
 3. `make verify-<name>` until it discharges with `-wp-rte`.
 4. `make verify-mutants MUTANT_TARGET=<name>` - a proof that cannot reject a
@@ -116,7 +132,7 @@ Supporting gates, all of which run per target:
 
 ### Memory models, and what no model checks
 
-Each target picks its own model via `VERIFY_<NAME>_MODEL` in `mk/analysis.mk`,
+Each target picks its own model via `VERIFY_<NAME>_MODEL` in `mk/verify.mk`,
 and the comment above it says why. Pick the model the code needs, not the
 model a neighbour target uses.
 
@@ -174,7 +190,7 @@ and two files conflict), and `macos-libc.h` for Darwin constants the modeled
 libc omits.
 
 It sits outside `src/` on purpose so a real compile, which resolves through
-`-Isrc`, cannot reach it. Only `FRAMAC_STUB_DIR` in `mk/analysis.mk` does.
+`-Isrc`, cannot reach it. Only `FRAMAC_STUB_DIR` in `mk/verify.mk` does.
 It is tracked in git because every proof target needs it to parse.
 
 A missing declaration fails with "Cannot resolve variable" - that is how the
@@ -204,5 +220,5 @@ so prefer them when the two disagree:
 
 - `docs/testing.md`, section "Validation Strategy By Change Type" - the change
   area to command mapping.
-- `mk/analysis.mk` - the per-target `_SRC` / `_MODEL` / `_FCTS` variables and
+- `mk/verify.mk` - the per-target `_SRC` / `_MODEL` / `_FCTS` variables and
   the comment above each explaining its model choice.

.github/actions/framac/action.yml

@@ -0,0 +1,111 @@
+# Frama-C, Alt-Ergo and Z3 on a macOS runner, ready for "make verify".
+#
+# Two jobs in verify.yml need this identically: the one that proves, and each
+# leg of the mutation matrix. Actions has no other way to share steps between
+# jobs, and the alternative is a forty-line copy that drifts the first time
+# either half is touched.
+#
+# The caller still has to "eval $(opam env --switch=...)" in its own run steps,
+# since a composite action cannot export shell state to them. The switch name
+# comes back as an output so nothing has to spell it twice.
+#
+# The toolchain pins live here rather than in the callers. They are inputs with
+# defaults, so a job can still override one, but nothing has to repeat them:
+# two jobs each carrying their own copy is how the proving half and the
+# mutating half end up on different analyzers with no output saying so.
+name: Set up Frama-C
+description: Install Frama-C and the provers, from cache when the pins are unchanged
+
+inputs:
+  framac-version:
+    description: Frama-C version to install
+    # 33.0, checked rather than assumed: the whole set discharges 803 of 803
+    # obligations across all 17 targets on it, with these same two provers, and
+    # the mutation gate still bites on the targets sampled. A proof that stops
+    # discharging on a newer analyzer is a real signal, so the pin exists to
+    # make the version an explicit decision, not to freeze it. Bumping any of
+    # the three is a cold opam build, since the cache key is keyed on all of
+    # them, and that first run is the one at risk of a job timeout.
+    #
+    # Defaults rather than required inputs because both callers want the same
+    # analyzer: proving on one Frama-C while mutating on another is an
+    # inconsistency no output would name.
+    default: "33.0"
+  alt-ergo-version:
+    description: Alt-Ergo version to install
+    default: "2.6.3"
+  z3-version:
+    description: Z3 version to install
+    default: "4.16.0"
+  brew-packages:
+    description: Homebrew packages the opam build needs
+    default: opam gmp pkg-config graphviz llvm@17 zlib
+
+outputs:
+  switch:
+    description: The opam switch name to eval into
+    value: frama-c-elfuse
+
+runs:
+  using: composite
+  steps:
+    - name: Point opam at a cacheable root
+      shell: bash
+      run: |
+        set -euo pipefail
+        echo "OPAMROOT=${{ github.workspace }}/.opam" >> "$GITHUB_ENV"
+        echo "OPAMCONFIRMLEVEL=unsafe-yes" >> "$GITHUB_ENV"
+        echo "HOMEBREW_NO_INSTALL_CLEANUP=1" >> "$GITHUB_ENV"
+        echo "HOMEBREW_NO_AUTO_UPDATE=1" >> "$GITHUB_ENV"
+
+    - name: Cache Homebrew downloads
+      uses: actions/cache@v6
+      with:
+        path: ~/Library/Caches/Homebrew/downloads
+        # Keyed on the package list, not just the workflow: changing what gets
+        # installed has to change the key or the cache serves the old set.
+        key: brew-${{ runner.os }}-${{ runner.arch }}-${{ inputs.brew-packages }}
+
+    - name: Install Homebrew packages
+      shell: bash
+      env:
+        BREW_PKGS: ${{ inputs.brew-packages }}
+      run: |
+        set -euo pipefail
+        # BREW_PKGS is a space-separated list, so it must stay unquoted.
+        # shellcheck disable=SC2086
+        brew install --quiet $BREW_PKGS
+
+    # Every job sharing this action shares one key, so a warm cache costs one
+    # restore each. Nothing primes it: on a miss they all build Frama-C and the
+    # provers from source at once, which is the whole cost of bumping any of
+    # the three pins, and the first run after such a bump is the one at risk of
+    # a job timeout. A prime job would trade that for a barrier in front of
+    # every run; the versions move rarely enough that the miss is cheaper.
+    - name: Cache opam switch
+      id: opam-cache
+      uses: actions/cache@v6
+      with:
+        path: ${{ env.OPAMROOT }}
+        key: opam-${{ runner.os }}-${{ runner.arch }}-frama-c${{ inputs.framac-version }}-ae${{ inputs.alt-ergo-version }}-z3${{ inputs.z3-version }}
+
+    - name: Install Frama-C, Alt-Ergo, Z3
+      if: steps.opam-cache.outputs.cache-hit != 'true'
+      shell: bash
+      run: |
+        set -euo pipefail
+        opam init -y --bare --disable-sandboxing
+        opam switch create frama-c-elfuse 4.14.1
+        eval "$(opam env --switch=frama-c-elfuse)"
+        opam install -y \
+          frama-c.${{ inputs.framac-version }} \
+          alt-ergo.${{ inputs.alt-ergo-version }} \
+          z3.${{ inputs.z3-version }}
+
+    - name: Report the toolchain
+      shell: bash
+      run: |
+        set -euo pipefail
+        eval "$(opam env --switch=frama-c-elfuse)"
+        why3 config detect
+        frama-c -version

.github/workflows/build.yml

@@ -9,20 +9,56 @@
 # Apple Silicon runners; the hosted job stops at build.
 name: Build
 
+# paths-ignore skips the run only when EVERY changed file matches, so the list
+# below is what cannot reach a build or a test: prose, editor and agent
+# configuration, the Frama-C stubs (reached only through mk/verify.mk, never
+# through -Isrc), and the other workflows. Everything else, src/ and tests/ and
+# mk/ and scripts/ and this file included, still runs the full job. Adding a
+# path here says "no build or test input can depend on this"; anything new is
+# unlisted and therefore builds, which is the safe direction. .gitignore is NOT
+# listed for that reason: checkout's git clean -ffdx wipes exactly what it
+# names, which is why the fixture-restore step further down exists at all.
+#
+# On pull_request only. Actions does not expand YAML anchors, so a filter on
+# push too would be a second copy with nothing keeping the two in step, and a
+# drift between them means a branch and its own merge commit run different
+# checks. The cost of dropping it is one build on a doc-only merge to main.
+# verify.yml keeps its push filter instead, and the asymmetry is the price:
+# the same doc-only merge would start seventeen macOS proof legs there.
+#
+# The failure directions differ from the proof scoping in proof-scope.py, which
+# is why that one needs a self-test and this one does not: a stale entry here
+# (path renamed) matches nothing and the workflow runs MORE, while a stale
+# entry in HARNESS_FILES widens nothing and the proofs run LESS.
+#
+# One condition on all of that: main carries no branch protection and no
+# ruleset today, so a run that never starts blocks nothing. A path filter skips
+# the whole run rather than reporting a skipped job, and a REQUIRED check that
+# never reports stays pending forever. Whoever makes these checks required has
+# to move the filtering into the jobs (a cheap classifier job plus "if:" on the
+# expensive ones) at the same time.
 on:
   push:
     branches: [main]
-    paths-ignore:
-      - '**.md'
-      - 'docs/**'
-      - 'LICENSE'
   pull_request:
     branches: [main]
     paths-ignore:
       - '**.md'
       - 'docs/**'
       - 'LICENSE'
+      - '.agents/**'
+      - '.claude/**'
+      - '.editorconfig'
+      - '.clang-format'
+      - 'frama-c-stubs/**'
+      - '.github/workflows/lint.yml'
+      - '.github/workflows/static-analysis.yml'
+      - '.github/workflows/verify.yml'
   workflow_dispatch:
+  # A merge queue runs the merged result, not the PR, and merge_group carries
+  # no path filter and no pull_request payload: every check runs in full there.
+  # Without this trigger a queue would merge with nothing having run at all.
+  merge_group:
 
 # Cancel in-progress runs for the same PR; keep main runs going.
 concurrency:
@@ -96,7 +132,8 @@ jobs:
     if: >
       github.repository == 'sysprog21/elfuse' &&
       (github.event_name == 'push' || github.event_name == 'pull_request' ||
-      github.event_name == 'workflow_dispatch')
+      github.event_name == 'workflow_dispatch' ||
+      github.event_name == 'merge_group')
     runs-on: [self-hosted, macOS, arm64]
     # Sanitizer builds run several times slower than the release build, so the
     # job budget and the per-test TEST_TIMEOUT are set per leg. Without