Shelfware oracles: 57/130 differentials are unreferenced, and nothing distinguishes 'manual by design' from 'forgotten'

[avrabe]

The pattern, third instance in one release

v0.53's audit lane (#879) found two differential oracles that existed but were
never CI-wired — gpio_thin_846_differential.py (behind the v0.50.1 and v0.52.0
headline size claims) and rv32_data_798_boot_differential.py. Both were fixed.

Then the same release produced a third: vfp_spill_881_differential.py, the
oracle behind the "falcon reaches the M7" claim, was written, committed, and
referenced nowhere. git grep found no ci.yml entry and no other caller. The PR
board was green with its central gate inert, so the claim was hand-checked only.

The mechanism is consistent and has nothing to do with care: writing an oracle
and wiring an oracle are separate steps, and the second is the one that gets
dropped when a contributor (or an agent) runs out of budget. In the #881 case
the lane died on a session limit with the wiring step still pending.

Measured scale

On main today:

differential scripts in scripts/repro/: 130
NOT referenced in .github/workflows/ci.yml:  57  (44%)

Important honesty caveat: 57 is not 57 broken gates. Many are legitimately
manual — they need external fixtures (gale's pinned wasm drops), a licensed
input, real hardware, or a toolchain CI doesn't install. The v0.53 L4 lane
independently confirmed this while sweeping all 129 scripts: the non-passing ones
were "all non-CI-wired manual-setup scripts."

That ambiguity IS the defect. Nothing in the repo distinguishes:

• "manual by design, and here's why" from
• "meant to be wired, and someone ran out of time."

So a forgotten gate is indistinguishable from an intentional one, and the only
way to tell is to read each script and reason about it — which is precisely the
audit that keeps finding new instances one at a time.

Proposed fix — make the distinction explicit and gate it

1. Require every scripts/repro/*_differential.py to declare its intended
   status, e.g. a header line or a small manifest:
   # ci-status: wired or # ci-status: manual — needs gale's pinned loom.wasm (#757).
2. Add a check that fails when a script declares wired but no workflow
   references it, and when a script declares nothing at all.
3. Report the manual set as a visible count, so it can be argued down over
   time instead of silently accumulating.

This is deliberately the same shape as the #880 fix: the previous gates verified
an artifact's output and never its content, so wrong content stayed green.
Here CI verifies the oracles it runs and never notices the ones it doesn't,
so an absent gate stays green. In both cases the invisible half is where the
defect lives — and, as with #867's uncovered-instruction complement, the
complement is the valuable half.

Anti-vacuity note for whoever implements this

The #879 fix established the discipline that any new wiring must use
set -o pipefail (a bare | tee reports tee's exit status, always 0) and
must assert a non-zero check count from the script's own summary, because
exit 0 alone is not trusted — the "0 ops accepted PASS" lesson. The #881 wiring
follows it and was verified red-first by mutation (0 rows → caught; a silent
6-of-7 export decline → caught). A meta-gate that itself passes vacuously would
be a poor joke.

Found while gating v0.53 lane L1 (#885).

[avrabe]

Re-measured during the v0.53.0 cold review, on the release branch:

69 of 150 differential scripts are unreferenced in .github/workflows/*.yml — up from the 57/130 in the original report. The ratio is essentially flat (44 % → 46 %), but the absolute count grew: v0.53 added scripts faster than it wired them, even in a release that explicitly wired three.

Newly noted in the unwired set: wcet_phase3_778_compose_soundness.py, wcet_phase4_49_recursion_soundness.py, wcet_phase5_778_masked_loop_soundness.py — the three cross-checks CLAUDE.md cites as the soundness evidence for the WCET bound composition, recursion-depth and masked-ceiling certificates. (crates/synth-cli/tests/wcet_bound_gate.rs does run under cargo test --workspace, so the capability is not ungated — but the claimed evidence chain does not reach it. See also the F5 finding recorded in v0.53.0's CHANGELOG: SYNTH-MATRIX-WCET-COMPOSITION is the one matrix pin with no oracle binding and no ci.yml count-min.)

Caveat on the 69: it is an upper bound. The sweep only grepped .github/workflows/*.yml, so a script invoked indirectly (via a shell wrapper or another script) would be counted as unwired.

This strengthens the original argument rather than changing it: the fix is not to wire 69 scripts, it is to make the distinction explicit — a declared ci-status: wired | manual — <reason> per script, gated so a wired script with no workflow reference fails, and the manual set is reported as a visible count that can be argued down instead of silently accumulating.