CI / required is red on main: ci.yml asserts Idris 2 0.7.0 but the digest-pinned image is 0.8.0 (and trope-check.yml requires 0.8.0) #83

Red on main (https://github.com/hyperpolymath/haec/actions/runs/39622697863) and identically on PR #81 (https://github.com/hyperpolymath/haec/actions/runs/40472456460). Recorded so #81, a docs-only pass, does not widen to fix it.

What happens: .github/workflows/ci.yml runs in ghcr.io/stefan-hoeck/idris2-pack@sha256:de97819… and asserts

case "$ver" in *"0.7.0"*) ;; *) echo "::error::expected Idris 2 0.7.0, got: ${ver}"; exit 1 ;; esac

The image reports Idris 2, version 0.8.0-6ca00e72e, so the job fails before idris2 --typecheck abi.ipkg runs. The same digest is used by trope-check.yml and release.yml, and trope-check.yml's comment says the repo requires 0.8.0 (0.7.0 cannot parse Trope/Fidelity.idr). The 0.7.0 assertion in ci.yml is the stale half of an earlier bump.

Fix: change the case arm to *"0.8.0"* (and update the comment above it), matching trope-check.yml. One-line; owner or a CI pass.

Also red on main, same run set: estate-rules (https://github.com/hyperpolymath/haec/actions/runs/39622698373) — scripts/check-root-shape.sh finds 5 root entries not on the allowlist: CHANGELOG.adoc, CONTRIBUTING.adoc, FUNDING, PROOF-PROGRESS.adoc, SECURITY.adoc. Either move them or add justified entries to .machine_readable/root-allow.txt (owner-only file under the Phase 0 brief).