ci(idris): add fast proof-check gate over all Proofs.idr (#145) (#147)

## Summary

Addresses the source-fixable half of #145. Adds a dedicated
**`proof-check`** job to `idris2-ci.yml` that type-checks **every**
`src/**/Proofs.idr` (glob-discovered, so new proof files are
auto-covered) with `idris2 -p contrib -p network --check`, running in
parallel with the slow full `build`.

## Why

#127's swapped-arg `appendLengthInc` (`lengthSnoc arr v` — but contrib
`lengthSnoc` is element-first) failed to type-check and blocked the
**entire** `SafeJson.Proofs` module, yet reached `main`. Two gaps let it
through:

1. The only job compiling proof modules was the full `idris2 --build
proven.ipkg` (~12-20 min warm) — manual merges routinely outrace it
while it sits `queued`.
2. The explicit per-module `--check` list in `idris2-ci.yml` covered
**zero** `Proofs.idr` files — exactly the modules the Phase-3 discharge
campaign edits each PR.

## What it does

- New `proof-check` job: globs `find src -name 'Proofs.idr'`, checks
each, emits `::error file=…::` annotations, fails if any fail.
- Caches only the Idris2 compiler; **never** `idris2 --install
proven.ipkg`, **never** caches `build/` — so a stale cache cannot mask a
source-level break.
- Documents the decision as **ADR-004** in `META.a2ml`.

## Remaining (admin, tracked in #145)

This job is necessary but not sufficient. Closing the gate needs
`proof-check` made a **required status check** on `main` via branch
protection — only the repo admin can toggle that. Until then, "merged"
still doesn't imply "CI passed" under the solo-admin-merge posture.

## Verification

- Both files parse (`yaml.safe_load` → jobs `build, proof-check, docs`;
`tomllib` → ADR-001..004).
- The `Proofs.idr` check loop was validated locally on a clean
idris2-0.8.0 + contrib install (SafeJson/SafeMath/SafeString proof
cones, 0 errors).
- This PR touches `idris2-ci.yml`, which is in the CI path filter — so
the new `proof-check` job runs on this PR and proves itself before
merge.

Refs #145, #144, #127.

---
_Generated by [Claude
Code](https://claude.ai/code/session_01MN5vzRR4MK2dkDNaHqqRDy)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/idris2-ci.yml

@@ -94,6 +94,76 @@ jobs:
           idris2 --check src/Proven/SafeDateTime.idr
           idris2 --check src/Proven/SafeNetwork.idr
 
+  # Fast, targeted gate over every Proofs.idr companion module.
+  #
+  # Rationale (issue #145): the swapped-arg `appendLengthInc` break (#127)
+  # reached main because the only job that compiles the proof modules is the
+  # slow full `build` above (~12-20 min on a warm runner), which merges
+  # routinely outrace. The explicit "Type check all modules" list above
+  # covers zero Proofs.idr files — exactly the modules the discharge campaign
+  # keeps editing. This job type-checks ALL of them, independently and in
+  # parallel with `build`, so a non-compiling proof is caught fast. Make THIS
+  # job a required status check on main (branch protection) to close the gate.
+  proof-check:
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    strategy:
+      matrix:
+        idris2-version: ['0.8.0']
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
+
+      - name: Install Idris 2 dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y chezscheme libgmp-dev
+
+      # Cache the Idris2 compiler + bundled packages (base/contrib/network)
+      # only. This job never runs `idris2 --install proven.ipkg` and never
+      # caches `build/`, so every run type-checks the CURRENT source of each
+      # Proofs.idr — a stale cache cannot mask a source-level break.
+      - name: Cache Idris 2
+        id: cache-idris2
+        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0
+        with:
+          path: |
+            ~/.idris2
+            ~/idris2-${{ matrix.idris2-version }}
+          key: idris2-${{ matrix.idris2-version }}-${{ runner.os }}
+
+      - name: Install Idris 2
+        if: steps.cache-idris2.outputs.cache-hit != 'true'
+        run: |
+          git clone --depth 1 --branch v${{ matrix.idris2-version }} https://github.com/idris-lang/Idris2.git ~/idris2-${{ matrix.idris2-version }}
+          cd ~/idris2-${{ matrix.idris2-version }}
+          make bootstrap SCHEME=chezscheme
+          make install
+
+      - name: Add Idris 2 to PATH
+        run: echo "$HOME/.idris2/bin" >> $GITHUB_PATH
+
+      - name: Type check every Proofs.idr
+        run: |
+          set -uo pipefail
+          rm -rf build
+          fail=0
+          checked=0
+          while IFS= read -r f; do
+            checked=$((checked + 1))
+            echo "::group::idris2 --check $f"
+            if idris2 -p contrib -p network --check "$f"; then
+              echo "PASS  $f"
+            else
+              echo "::error file=$f::idris2 --check failed"
+              fail=1
+            fi
+            echo "::endgroup::"
+          done < <(find src -name 'Proofs.idr' | sort)
+          echo "Checked $checked Proofs.idr module(s); fail=$fail"
+          exit "$fail"
+
   docs:
     runs-on: ubuntu-latest
     needs: build