fix(guard): the changed-path classifier cannot fail open (#384)

[avrabe]

Closes #384. REQ-GUARD-GATE-EVIDENCE-002 obligation (e) — the fifth of six.

Detect changed paths decides whether 10 of the 18 required status checks
run, and the same logic cloned into proofs.yml gates an 11th
(Lean proof typecheck (lake build)). It could be made to answer "no code
changed" two different ways, and in both the error path produced the
permissive verdict with the step exiting 0.

skipped satisfies a required context. A skipped required check and a passed
one are the same green on the merge button.

The two mechanisms

A — the allow-list was scoped by prefix, not by file type.

allow='^(artifacts/.*\.ya?ml|safety/.*|docs/.*|rivet\.yaml|[^/]*\.md|.*/.*\.md)$'

artifacts/ and the two *.md entries name the extensions they admit.
safety/.* and docs/.* do not — they admit anything under those trees,
including .rs, .sh and .toml. docs/research/forge-replication/ already
holds run_trial.sh, tasks.json, descriptor.sexp and descriptor.aadl, so
this was one git mv from live rather than theoretical.

B — the error path failed open.

n_code=$(printf '%s\n' "$changed" | grep -cvE "$allow" || true)
if [ "$n_code" -gt 0 ]; then ... else echo "code=false" ...

If grep failed for any reason other than a zero count it wrote nothing,
n_code became the empty string, and [ "" -gt 0 ] exited 2. Inside an if
condition set -e is inert, so bash read that non-zero as false and took the
code=false branch. Two error messages printed and the step still exited 0,
having skipped the suite.

The || true was not simply removable: grep -c also exits 1 on a legitimate
zero count. Success and failure arrived identically, which is what made the
suppression both load-bearing and catastrophic.

What replaces it

One script, tools/classify_changed_paths.py, called from both workflows.

• Type-scoped allow-list. Every entry names its extensions. A path matching
  nothing is code — a classifier that cannot recognise a file has not shown it
  is inert.
• No error path emits a verdict at all. Any failure raises, prints, and
  exits non-zero.
• The script owns $GITHUB_OUTPUT and appends to it directly. This is its
  only emission mode on purpose: echo "code=$(script ...)" would put mechanism
  B straight back into the glue — script dies, echo succeeds, code= lands
  empty, every == 'true' dependent skips, exit 0. Neither changes job now
  contains a subshell, ||, -gt or grep.
• The self-test runs first, like the other guardrail self-tests: a
  classifier whose own tests fail must not decide which required checks run.

Why exiting non-zero is safe here — and why that is not obvious

A failing changes job means its dependents are skipped, and skipped
satisfies a required context. Exiting non-zero would normally be worse than
failing open.

It is safe only because Detect changed paths and Detect changed paths (proofs) are themselves required contexts, so the classifier going red blocks
the merge on its own. That was read from the branch-protection API, not assumed.
Two further facts were checked rather than trusted:

• every consumer of outputs.code tests == 'true', so no job runs on the
  inverse and an absent output cannot trigger anything;
• python3 is present on [self-hosted, linux, x64, light] — ci.yml::fmt
  already runs check_fmt_workspaces.py on that exact label.

If Detect changed paths is ever dropped from the required contexts this
design becomes unsafe. check_required_contexts.py (REQ-GUARD-GATE-EVIDENCE-001)
is what stops that happening quietly, and the module docstring says so.

One deliberate behaviour change

The two copies had already drifted: ci.yml gained rivet.yaml in #379 and
proofs.yml never did. Single-sourcing gives the proofs side that entry, so a
rivet.yaml-only PR now also skips the Lean job. Safe for the same reason #379
gave — nothing under proofs/ reads rivet.yaml — and it is exactly the
divergence single-sourcing exists to end. Called out rather than absorbed
silently, because it is a loosening.

Evidence

• 25 self-test cases, run as step 2 of both changes jobs.
• The detector is a property, not the cases: for every directory prefix in
  the allow-list, no pattern may match <prefix>/evil.rs, .sh, .toml or
  Makefile. Someone re-broadening an entry back to prefix scope fails without
  anyone having remembered to add a case for them.
• Mutation-tested, 5 mutants, all caught, each by the test that should catch
  it: unknown→non-code, emit() ignoring its argument, restoring the old
  exception handler, re-broadening safety/, re-adding docs/.*. The harness
  asserts each substitution changed the file before drawing a conclusion — a
  mutation that silently fails to apply reports as "not caught" and is worthless.
• Measured on real history: 7db7f0e6 (two artifact YAMLs) still emits
  code=false, so the classifier was tightened without becoming uselessly
  always-true; c8c0450e (8 files, 6 code) emits code=true.
• The fixture repo pins core.hooksPath=/dev/null. The self-test shells out
  to git init/commit, and it is step 2 of a required context gating 11
  others, so a machine with a global core.hooksPath would run foreign hooks
  and turn that context red for every PR in the repo. Verified load-bearing:
  under a simulated hostile global hooksPath the unpinned copy fails 3 of 25,
  the pinned one passes 25.

NOT claimed: that skipping is correct for any particular file. This only
ensures a skip is caused by a match against a declared, type-scoped pattern and
never by a crash.

🤖 Generated with Claude Code

[github-actions]

Rivet verification gate

✅ 20/20 passed

	count
Passed	20
Failed	0
Skipped (no steps)	0

Filter: (and (= type "feature") (or (has-tag "v093") (has-tag "v0100")))

Failed artifacts

(none)

_{Updated automatically by tools/post_verification_comment.py. Source of truth: artifacts/verification.yaml.}

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!