Gate Topology audits 15 of 45 workflows and misses two live violators; coq-proofs.yml has never been green in 50 runs #5172

Re-filed from #2686. An attempt claimed that issue on 2026-09-24 and left an empty branch, and a dispatch row that has spent its retry ceiling keeps its issue for good - so no bee could take it again, however much the brief improved. The work below is carried over unchanged.

Two CI findings from the same audit. Both are about a green that does not mean what it reads as.

1. The gate that forbids branch filters audits a third of the workflows, and misses the violators

Gate Topology has run 433 times and never once gone red.

$ python3 scripts/ci/check_pr_branch_filters.py; echo EXIT=$?
merge-critical workflows checked: 15
workflow files present:           45
explicitly not merge-critical:    4

CLEAN: no merge-critical workflow filters pull_request by branch.
EXIT=0

15 checked, 4 declared out of scope, 45 present — so 26 workflows are in neither list and the gate is silent about them. Importing the checker's own MERGE_CRITICAL / NOT_MERGE_CRITICAL lists and scanning every workflow file:

branch-filtered pull_request workflows NOT covered by either list:
  corpus-ratchet.yml:      pull_request.branches=['master']   *** UNLISTED ***
  withdrawn-live-gate.yml: pull_request.branches=['master']   *** UNLISTED ***
  pr-dashboard.yml:        pull_request.branches=['master','main']   (declared not critical)

The two gates that today carry the exact filter this checker exists to forbid are in neither of its lists, and both are real working gates rather than stubs. A hardcoded allow-list is a ledger, and this one went stale the way ledgers do — silently, while printing CLEAN.

The narrow fix is to add the two. The durable one is for the checker to fail when a workflow is in neither list, so growth forces a decision instead of producing silence.

2. coq-proofs.yml has never succeeded, in 50 runs

$ gh api ".../actions/workflows/coq-proofs.yml/runs?per_page=1&status=success" --jq .total_count
0
$ ... status=failure
50
$ ... (all runs)
50

Every one of the ten most recent runs is a failure, including on master. The workflow is active and still wired to push and pull_request.

A gate that has never been green cannot distinguish "you broke it" from "it has always been like this", so it costs a red mark on every run and buys nothing. Three options, and which one is right is yours: fix it, disable it, or mark it continue-on-error with a comment saying why it is kept.

Related: tri gates dead exists to list exactly this class.

Refs #2161

Boundary

• scripts/ci/check_pr_branch_filters.py

The instruments

Every one of these reads and prints; none of them writes. Run them from the repository root, with <spec> replaced by the file in ## Boundary:

.t27 is not Rust and not Zig, and a bee fluent in either writes one by
accident. Measured 2026-09-20: a bee filled eight bodies in
specs/file/watcher.t27 with return Ok(());, Err(FileError::WatcherNotFound)
and for i in 0..watchers.length. The parse ratchet refused the whole file --
Unexpected token in expression: RParen, line 123 -- and a spec that does not
parse generates nothing, so every test it already carried stopped running.

At the top level the parser accepts exactly these eight forms, with an optional
pub, and no others:

const   var   fn   enum   struct   test   invariant   bench

There is no trait, no impl, no type X = ..., no generics, no macro. What
a bee reaches for from another language, and what happens:

• Rust's result sugar (Ok(()), Err(E::V), ?) is not a construct here.
• Rust macros (println!, format!, vec!) are not constructs here.
• A range loop (for i in 0..n) is Rust and Zig, not this language.
• Zig builtins (catch unreachable, @intCast, @constCast) are not constructs here.
• Cross-module reuse (use other::fn;) parses and then generates a comment and an unqualified call, so the Zig fails with use of undeclared identifier (use a::b; generates no import, so no spec can reuse a function from another spec #4298). It does not work yet.

t27c parse <spec> answers in one line whether what you wrote is the language.
Run it before you report, every time.

• t27c spec-status <spec> - the compiler's one-word verdict: IMPLEMENTED, PARTIAL, UNWRITTEN, NOPARSE, NOFN. Exit code is 0 whatever it says, so read the word.
• t27c symbols <spec> - every name the file declares, with its kind. Answers "does this already exist here?" before you add it.
• t27c outline <spec> - per function: its locals, what it calls, what it returns. The contract you are implementing against.
• t27c coverage <spec> - which functions have a test and which do not. The issue asks for tests; this is how you check you wrote them.
• t27c lint <spec> - style and shape warnings. It OVER-REPORTS has no test or invariant: measured 2026-09-20 over 60 specs it printed 677 of those where coverage found 190 untested functions, disagreeing on 59 of the 60 - it warns about bit_to_trit_pair in specs/base/ternary_encoding.t27, which test bit_to_trit_pair_zero calls on line 249. Read it as a hint; coverage is the answer.
• t27c typecheck <spec> - types, before generation. Prints Typecheck OK (0 errors, 0 warnings) or the errors.
• t27c test-report <spec> - builds this spec and runs its own tests, which is what the oracle does. BLOCKED means the generated Zig does not compile, with the error beside it.
• python3 tools/dupe_scan.py --name <function> - where that function already lives, if it does. 576 of 4021 bodies here are byte-identical copies.

The rest of the toolbelt is in docs/BEE_TOOLBELT.md.