echidna-verify: required context `Idris2 — a2ml proofs` is vacuously green on every PR and red on every cron

[hyperpolymath]

Summary

.github/workflows/echidna-verify.yml verifies zero proofs in this repo, in two different ways, and one of them props up a required status check.

The proof corpora were evicted from standards but the jobs that verify them stayed. All four filtered paths are now absent from main:

Path referenced by the workflow	Status on main
lol/proofs/**	404
a2ml/src/**, a2ml/a2ml-core.ipkg	404
avow-protocol/avow-lib/src/abi/*.idr	404 (avow-protocol/ holds only BINDING.adoc)

This is a partially-completed repair, not a fresh bug

idris2-avow was already fixed — and its own comment (L249-252) records exactly what happened:

repo avow-protocol/ holds only BINDING.adoc - the proofs live in the avow-protocol repository - so the cd always failed and this job was permanently red. It only became visible once the workflow began running on pull requests.

It now guards:

if [ ! -d avow-protocol/avow-lib ]; then
  echo "::notice title=AVOW proofs::...Nothing to type-check."
  exit 0
fi

agda-lol and idris2-a2ml have the identical disease and never got the guard, because their failure is invisible where people look.

The two failure modes

On pull_request — detect-proof-changes greps the changed-file list for the evicted paths (L72), so it can only ever emit proofs=false. All three jobs carry if: needs.detect-proof-changes.outputs.proofs == 'true', so all three are skipped — and GitHub counts a skipped required check as satisfied.

On schedule — the detector is bypassed, the jobs run, and they die on the missing directories:

Agda — lol/proofs:      find: 'lol/proofs/theories': No such file or directory   -> exit 1
Idris2 — a2ml proofs:   cd a2ml   (set -euo pipefail, L176-178)                  -> exit 1

idris2-a2ml burns ~18 minutes bootstrapping Idris2 via pack (136 base modules build fine) and then cds into a directory that does not exist. The dead giveaway in the log is No files were found with the provided path: idris2-a2ml.log — the step died before it could write one.

Last 40 runs: 38 success + 1 cancelled on pull_request, 1 failure on schedule (run 34091039282).

Why this matters: a required context is vacuously green

Idris2 — a2ml proofs is a required status check in ruleset 14285635 (Optimus-Branch).

Live witness — on the three currently-BLOCKED PRs, all three proof contexts report SKIPPED, and none of them appears among the blocking reasons:

PR	Agda — lol/proofs	Idris2 — a2ml proofs	Idris2 — AVOW consent proofs
#745	SKIPPED	SKIPPED	SKIPPED
#746	SKIPPED	SKIPPED	SKIPPED
#747	SKIPPED	SKIPPED	SKIPPED

So the formal-verification gate on this repo currently proves nothing, while reporting that it does.

Caution on the obvious fix

Copying the AVOW guard into the other two jobs stops the weekly red but makes the fake green complete and silent. exit 0 on "no proofs found" is a fail-open gate — and this one is load-bearing on a required context. That is a policy decision, not a mechanical one.

Options (owner decision — no ruleset change made)

1. Re-point at the real homes. The proofs exist: hyperpolymath/lol carries theories/, specs/, echidna.toml and POSTULATE-AUDIT.adoc. Verification could move to those repos and be consumed here as a required cross-repo signal.
2. Un-require and retire. Drop Idris2 — a2ml proofs from ruleset 14285635 and delete the dead jobs, so the absence of proof CI in standards is honest rather than concealed.
3. Guard + keep required, accepting a documented fail-open gate. Cheapest, and the worst of the three: it preserves the appearance of formal verification with none of the substance.
4. Guard + assert non-empty. Guard the cd, but make the job fail if the expected corpus is missing rather than exit 0 — a check that is honestly red until re-pointed.

Whichever is chosen, the push: trigger paths (L14-19) also reference the evicted paths and should be updated in the same change.

Not filed elsewhere

The a2ml half of this touches hyperpolymath/a2ml / a2ml-ecosystem, which another agent is actively working. Deliberately not filed there — routing is the owner's call.

_{Evidence: scheduled run 34091039282; ruleset 14285635; PR heads #745/#746/#747; contents API 404s on all four filtered paths, 2026-09-08.}