Verification Gate scope is stale: 20 of 161 feature artifacts checked, per-PR override never used

[avrabe]

Summary

The Verification Gate's scope has been stale since ~v0.11.0. It re-runs the same
20 v0.9.3/v0.10.0-era artifacts on every PR and never executes the artifacts the
PR under review actually adds or changes. The per-PR escape hatch designed to fix
this has never once been used.

Consequence: for 141 of 161 type: feature artifacts, the V-model's right
side is not mechanically closed. An artifact can be committed as
status: passing / a requirement as status: verified without its declared
fields.steps[].run ever having been executed by CI.

Evidence

.github/workflows/verification-gate.yml:66 — the default filter:

DEFAULT='(and (= type "feature") (or (has-tag "v093") (has-tag "v0100")))'

Measured against artifacts/*.yaml at c065e3d:

	count
type: feature artifacts	161
matched by the default filter	20
never executed by the gate	141

The workflow intends each PR to narrow the scope to its own artifacts with a
Verify-Filter: body line (verification-gate.yml:52-72). Checking the last ten
merged PRs — #354, #353, #352, #351, #349, #348, #346, #344, #342, #340 — none
set it. Every one ran against the stale 20.

The clearest illustration is #356, which removed TEST-LAYOUT-CERT and rewrote
three requirements. Its gate comment:

✅ 20/20 passed
Filter: (and (= type "feature") (or (has-tag "v093") (has-tag "v0100")))

A green check that verified twenty unrelated artifacts and none of the PR's own.

Why the existing escape hatch cannot work

Verify-Filter: is read from github.event.pull_request.body, which is captured
in the event payload at trigger time. So:

• adding the line after opening the PR has no effect on the run already fired;
• re-running the workflow replays the original payload, so it does not pick up an
  edited body either;
• it only takes effect on the next synchronize.

A gate scope that depends on prose typed into a description before opening the
PR, and that silently no-ops if forgotten, is not a gate. This is the same shape
as the required-check hole fixed in #353: the failure mode is silence that looks
like success.

Proposed fix

Make the scope a function of the commit instead of the description.

1. Add tools/changed_verification_artifacts.py: parse
   git show <merge-base>:artifacts/verification.yaml and the working copy, diff
   by artifact id (not by diff hunk, so a body-only edit is caught too), and
   print the ids of added-or-modified type: feature artifacts.
2. Give tools/run_verification.py an --also-ids option and union it with the
   filter results. Deliberately not expressed as a rivet filter s-expression:
   CI pins rivet to v0.7.0 (b7a17bef) while local rivet is 0.28.0, so filter
   syntax cannot be validated locally against the version that will run it. An
   explicit id list is version-independent.
3. Keep the current 20 as a floor rather than replacing them — strict improvement,
   no regression risk.
4. Retain Verify-Filter: as a manual widener for cases where a code change
   should re-verify artifacts it does not textually touch.

Cost scales with the PR, not the repo, so the 60-minute budget is unaffected in
the common case.

Deliberately not proposed

Making Verification Gate (rivet-driven) a required context. It currently is
not one of the 16. Requiring it before the scope is correct would only enforce a
gate that checks the wrong 12%, and CI already runs 2h20m–2h33m end-to-end.
Worth revisiting once the scope is diff-derived and its real cost is observed.

Adjacent, smaller

• verification-gate.yml:20 justifies the 60-minute timeout with "TEST-PROOF-
  steps run cd proofs && lake build … 25–35 min"*. d902bf2 (fix(verify-gate): keep TEST-PROOF-* on sorry-grep — lake build exceeds gate budget #230) replaced
  those steps with a file-exists + no-sorry smoke check precisely because
  lake build exceeded the budget. The comment is stale; the budget now rests on
  an obsolete rationale.
• 19 of the 161 type: feature artifacts have no runnable steps and are reported
  [SKIP], which is not counted as failed. These are descriptive FEAT-* /
  ARCH-SYS records, so skipping is correct — noting it only because
  "skipped satisfies the check" is the exact pattern ci: skip heavy jobs on artifacts/docs-only diffs #353 had to close at the
  workflow level, and it is worth being deliberate that this instance is benign.

Not a defect (checked, and I was wrong first)

I initially read TEST-PROOF-LATENCY / TEST-PROOF-ARINC653 as verifying Lean
proofs by mere file existence. They have two steps; the second is a real
no-sorry grep, and lake build is delegated to the dedicated required
"Lean proof typecheck" workflow by the documented decision in #230. No action.

[avrabe]

Confirmed by experiment: Verify-Filter: set after opened is inert

This was a prediction; it is now measured, with a control.

#357 — Verify-Filter: added to the body after the PR was opened. Gate run
30535183445:

== summary ==
passed:  20
failed:  0
skipped: 0

20 is the stale default scope, (and (= type "feature") (or (has-tag "v093") (has-tag "v0100"))). The override was ignored.

Root cause as diagnosed: verification-gate.yml resolves the filter from
github.event.pull_request.body, which is the body as captured in the event
payload at trigger time. Editing the body afterwards does not re-trigger, and a
re-run replays the original payload — so there is no way to fix it after the fact
short of closing and reopening the PR.

#359 is the control, with Verify-Filter: present in the body at creation
time and v0360 added to the disjunction. Expecting 21 (the 20 plus
TEST-GUARD-HUMAN-SCOPED). Will post the number when that run completes.

Why this makes the case for diff-derived scope stronger than I first thought

The failure isn't just "the override was missed." It's that the gate greened
without running the artifact the PR added, and reported passed: 20 / failed: 0 —
which reads exactly like success. Same shape as the two defects already filed this
round: bus_bandwidth returning 0.0 for unmeasurable (#357) and this gate
printing a clean summary over a scope that excluded the change.

Any operation that can produce "nothing relevant happened" has to render that
differently from "it worked."

So the fix wants two parts, not one:

1. Derive scope from the diff — tools/changed_verification_artifacts.py maps
   changed artifacts/*.yaml ids to gate scope, plus run_verification.py --also-ids, so a PR's own new artifacts are always in scope regardless of what
   any body line says. This is the substance of this issue.
2. Make an under-inclusive run loud. If the diff touched verification artifact
   ids that the resolved filter did not select, the gate should say so — ideally
   fail. A summary that cannot distinguish "scope was empty of your change" from
   "your change passed" is the vacuity this whole issue is about.

A hardening note on the manual path, whichever way (1) lands: reading the filter
from the PR body is inherently a trigger-time snapshot. If a manual override is
kept at all, it should come from something re-readable at run time — a label, or a
file in the diff — so that "I set it and it did not apply" stops being a silent
outcome.

[avrabe]

Confirmed by a controlled pair — the trigger-time-snapshot diagnosis holds

Both PRs have now run the gate, differing only in when the Verify-Filter: line
entered the body:

PR	Verify-Filter: set	filter the gate used	artifacts
#357	after opened (body edit)	stale default	20
#359	at creation	the one in the body	21

#359's log, verbatim:

FILTER: (and (= type "feature") (or (has-tag "v093") (has-tag "v0100") (has-tag "v0360")))
matched 21 artifacts
...
passed:  21   failed:  0   skipped: 0

and TEST-GUARD-HUMAN-SCOPED is in the matched list — so the 21 is the stale 20 plus
exactly the artifact the PR added, which is the composition predicted in #359's body
before either run existed. #357's edit-after-opened was inert, as predicted: a re-run
replays the original github.event.pull_request.body payload, so there is no way to
repair the scope from the UI.

This is worth stating precisely because it makes the failure mode worse than "the filter
was wrong": the gate reported passed: 20 / failed: 0 over a scope that excluded the
PR's own artifact. It was green because it did not look. That is the same shape as
the 0.0-for-unmeasurable defect fixed in #357 and the vacuous certificate withdrawn in
#356 — a "nothing happened" outcome rendered identically to "it worked."

So the two-part fix in this issue stands, and the second part is the load-bearing one:

1. Derive scope from the diff, not from a body line captured at trigger time.
2. Make an under-inclusive run loud. If the diff touches artifact ids that the
   resolved filter does not match, that is not a pass — the gate should name them and
   fail. A filter mechanism alone still greens on a filter that is merely stale.

[avrabe]

Triage — one correction that makes this worse, not milder.

Deliberately not proposed. Making Verification Gate (rivet-driven) a required context. It currently is not one of the 16.

It is required. Measured just now on three open PRs (#373, #376, #377) — all
report an 18-context required set including Verification Gate (rivet-driven) —
and independently confirmed against live branch protection with an admin-scoped
read:

$ tools/check_required_contexts.py --against-api
PASS: branch protection on main matches .github/required-contexts.txt (18 contexts).

(The "16" is likely a mid-flight rollup reading. Code Coverage and
Mutation Testing declare needs: [changes, test], so on a PR where Test is
still queued their check-runs do not exist yet — gh pr checks --required
then shows 16. An absent check-run is not a non-required check. I nearly filed
the same error in reverse today.)

So the situation this issue describes is not "a gate checking the wrong 12% that
we might one day require." It is a required gate reporting green for 140 of 160
type: feature artifacts it never executed. Re-measured locally:

architecture.yaml   feature=  1  matched=  0
verification.yaml   feature=159  matched= 20
TOTAL               feature=160  matched= 20   never-executed=140

(160 vs the issue's 161 — within one of the same finding, and the material
number is identical.)

That upgrades this from a scope-hygiene item to the same class as #353 and #372:
a green tick that a reader takes as a verdict, covering work nothing checked.
It's the failure shape those two closed at the workflow level, present here at
the artifact level.

Accepting the proposed fix (diff-derived scope via
tools/changed_verification_artifacts.py + --also-ids, keeping the current 20
as a floor). The reasoning for an explicit id list over a rivet filter s-expression
holds — CI pins rivet v0.7.0 (b7a17bef) while local rivet is 0.28.0, so filter
syntax can't be validated locally against the version that will run it.

Two amendments:

1. Verify-Filter: should be removed, not retained as a manual widener. This
   issue's own strongest argument is that github.event.pull_request.body is
   captured at trigger time, so the escape hatch silently no-ops on the run it
   was written for. Keeping a mechanism that fails silently — as a widener,
   where the failure is "less was verified than you asked for" — reproduces the
   defect. If a code change should re-verify artifacts it doesn't textually
   touch, that belongs in a committed file the diff can see.
2. The stale 60-minute-timeout rationale (verification-gate.yml:20, still
   citing lake build that d902bf2/fix(verify-gate): keep TEST-PROOF-* on sorry-grep — lake build exceeds gate budget #230 removed) is worth fixing in the same
   PR — it's the load-bearing-comment-gone-stale shape, and the budget currently
   rests on it.

Not scheduling this into a release yet: three open PRs touch
artifacts/requirements.yaml and the runner pool is saturated. Queued behind
them rather than opening a conflicting branch.

🤖 Generated with Claude Code