fix(drv): gate the PROVIDERS enumeration against reality

[avrabe]

Closes the enumerated-list sweep started in #313.

build-gustos-components.sh enumerates five providers by hand. Unlike the other
lists found this month, that one is correct to enumerate — it defines the
published v0.4.0 composition, and a newly added provider must not silently join
the fused composite just by existing. Glob discovery would be the wrong fix.

What was missing is the check that the deliberate list still matches reality. An
enumeration nobody verifies is exactly how the Lean target list,
check-providers.sh, and build-cross-arch.sh each came to exclude the newest
thing without saying so.

Now: enumerated on purpose, and gated. A *-provider directory that is not
listed fails the script and is named. The fix is then a deliberate decision — add
it to PROVIDERS and build-fused-gustos.sh, or record why it is excluded —
rather than a silent skip.

Kill-criterion (both directions verified)

tree	result
real (5 listed, 5 present)	exit 0, no drift reported
mkdir can-provider (5 listed, 6 present)	exit 2

FATAL: PROVIDERS list has drifted from the *-provider directories.
  listed but absent:
  present but unlisted: can-provider
  Add it to PROVIDERS and build-fused-gustos.sh, or record why it is excluded.

Sweep status

gate	list was	now
Lean CI targets	7 enumerated	//proofs/lean:all
check-providers.sh	8 enumerated	discovered
build-cross-arch.sh	8 of 13	discovered (#313)
check-driver-components.py	rule excluded 3 correct drivers	rule corrected
build-gustos-components.sh	5 enumerated, unverified	enumerated + drift-gated

🤖 Generated with Claude Code

https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!