ci(proofs): gate the Idris2 verification corpus (verification/proofs/idris2) (#276)

## What

Adds CI coverage for the **Idris2 trust-pipeline property proofs** under
`verification/proofs/idris2/` (11 modules) — the last self-proof corpus
with no gate.
Follows #275 (which gated `verification/proofs/lean4`).

- **New `echidna-verif-proofs.ipkg`** listing all 11 modules with
`depends = base, echidnaabi`.
- **New Justfile recipe `proofs-verif-idris`**: installs the
`echidnaabi` package (`--install`
builds it on the way), then `idris2 --typecheck
echidna-verif-proofs.ipkg`. Added to the
  `proofs` roll-up.
- **New `verif-idris` job** in `dogfood-proofs-ci.yml` (apt idris2 +
source-bootstrap fallback,
mirroring `idris2-abi-ci.yml`) + `verification/proofs/idris2/**` path
triggers.

## Why an ipkg, not a per-file `idris2 --check` loop

Two real problems surfaced while building this (caught by *running* it,
not eyeballing):

1. **`idris2 --check` returns exit 0 even when a module fails to resolve
an import.**
   Verified: a bare `idris2 --check DispatchCorrectness.idr` prints
`Error: Module EchidnaABI.Types not found` but **exits 0** — a per-file
loop would pass CI
while broken. (Genuine *type* errors do exit 1; only module-resolution
errors don't.)
2. **`DispatchCorrectness.idr` imports `EchidnaABI.Types`** — the
`echidnaabi` package in
   `src/abi/`, unresolvable standalone.

Building through the ipkg fixes both: `depends = echidnaabi` resolves
the import, and the
package build gives a reliable aggregate exit code. The recipe
additionally fails on any
`^Error` line as a belt-and-suspenders guard.

## Verification (run, not eyeballed)

On **idris2 0.8.0**, from a clean state (`src/abi/build`, the installed
`echidnaabi` package,
and `verification/proofs/idris2/build` all removed first):

- `just proofs-verif-idris` → type-checks all 11 modules (incl.
DispatchCorrectness), **exit 0**.
- **Negative test**: injecting `n = S n` proved by `Refl` into a module
makes the ipkg
  typecheck **exit 1** — the gate actually gates.
- Corpus is **axiom-clean**: no `believe_me` / `assert_total` /
`postulate` (the two grep hits
are string literals in a `patternString` data table, not real escapes);
fully total.

## Notes

- No proof sources changed — packaging + CI wiring only.
- The `verif-idris` job mirrors `idris2-abi-ci`'s install (apt-first,
source-fallback) and uses
  `timeout-minutes: 30` to cover the source-bootstrap fallback.
- Remaining in the proof-CI sweep: a **weekly cron** for the heavier
Isabelle/Mizar corpora
  (next).

🤖 Generated with [Claude Code](https://claude.com/claude-code)


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

---------

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

Author: hyperpolymath

.github/workflows/dogfood-proofs-ci.yml

@@ -19,13 +19,15 @@ on:
     paths:
       - 'proofs/**'
       - 'verification/proofs/lean4/**'
+      - 'verification/proofs/idris2/**'
       - 'Justfile'
       - '.github/workflows/dogfood-proofs-ci.yml'
   pull_request:
     branches: [main]
     paths:
       - 'proofs/**'
       - 'verification/proofs/lean4/**'
+      - 'verification/proofs/idris2/**'
       - 'Justfile'
       - '.github/workflows/dogfood-proofs-ci.yml'
   workflow_dispatch:
@@ -167,6 +169,44 @@ jobs:
       - name: Build Lean verification corpus
         run: just proofs-verif-lean
 
+  verif-idris:
+    name: Idris2 (verification)
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    steps:
+      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+
+      - name: Install Idris2
+        run: |
+          set -euo pipefail
+          # idris2 v0.8.0 ships no prebuilt Linux release asset, so prefer the
+          # Ubuntu 24.04 universe package and fall back to a source bootstrap from
+          # the tag archive (mirrors idris2-abi-ci.yml's install).
+          sudo apt-get update -qq || sudo apt-get update -qq --fix-missing
+          sudo apt-get install -y --fix-missing idris2 2>/dev/null || {
+            IDRIS2_VER="v0.8.0"
+            sudo apt-get install -y --fix-missing chezscheme make libgmp-dev
+            curl -fsSL --max-time 300 --retry 2 -o /tmp/idris2.tar.gz \
+              "https://github.com/idris-lang/Idris2/archive/refs/tags/${IDRIS2_VER}.tar.gz"
+            mkdir -p /tmp/idris2-src
+            tar xzf /tmp/idris2.tar.gz -C /tmp/idris2-src --strip-components=1
+            (cd /tmp/idris2-src && make bootstrap SCHEME=scheme && sudo make install PREFIX=/usr/local)
+          }
+          idris2 --version
+
+      - name: Install just
+        run: |
+          set -euo pipefail
+          curl -fsSL --retry 3 \
+            "https://github.com/casey/just/releases/download/1.51.0/just-1.51.0-x86_64-unknown-linux-musl.tar.gz" \
+            -o /tmp/just.tar.gz
+          mkdir -p "$HOME/.local/bin"
+          tar xzf /tmp/just.tar.gz -C "$HOME/.local/bin" just
+          echo "$HOME/.local/bin" >> "$GITHUB_PATH"
+
+      - name: Type-check Idris2 verification corpus
+        run: just proofs-verif-idris
+
   agda:
     name: Agda
     runs-on: ubuntu-latest

Justfile

@@ -250,7 +250,7 @@ test-s4-loop:
 # exact same commands.
 
 # Type-check the whole dogfood proof corpus across every assistant.
-proofs: proofs-coq proofs-lean proofs-agda proofs-idris proofs-verif-lean
+proofs: proofs-coq proofs-lean proofs-agda proofs-idris proofs-verif-lean proofs-verif-idris
 
 # Compile the Coq proof corpus (proofs/coq/**/*.v).
 proofs-coq:
@@ -292,6 +292,25 @@ proofs-idris:
 proofs-verif-lean:
     cd verification/proofs/lean4 && lake build
 
+# DispatchCorrectness imports EchidnaABI.Types, so the echidnaabi package
+# (src/abi) is installed first (--install builds it on the way); the ipkg then
+# type-checks all 11 modules with a reliable aggregate exit code. A bare per-file
+# `idris2 --check` is unsafe here -- it exits 0 even on an unresolved import -- so
+# the ipkg build is the gate and any "Error" line is also treated as failure.
+# Type-check the Idris2 trust-pipeline property proofs (verification/proofs/idris2).
+proofs-verif-idris:
+    #!/usr/bin/env bash
+    set -euo pipefail
+    (cd src/abi && idris2 --install echidnaabi.ipkg >/dev/null)
+    cd verification/proofs/idris2
+    out=$(idris2 --typecheck echidna-verif-proofs.ipkg 2>&1)
+    printf '%s\n' "$out"
+    if printf '%s\n' "$out" | grep -qE '^Error'; then
+        echo "Idris2 verification corpus: TYPE ERRORS DETECTED" >&2
+        exit 1
+    fi
+    echo "Idris2 verification corpus: all files type-check"
+
 # Format code
 fmt:
     cargo fmt

verification/proofs/idris2/echidna-verif-proofs.ipkg

@@ -0,0 +1,32 @@
+-- SPDX-License-Identifier: MPL-2.0
+--
+-- echidna-verif-proofs — Idris2 trust-pipeline property proofs.
+--
+-- These modules formalise properties of ECHIDNA's verification pipeline
+-- (axiom completeness/policy ordering, trust-kernel monotonicity, dispatch
+-- correctness/ordering, clamp bounds, proof-state serialisation round-trips,
+-- prover-kind injectivity, trust-level soundness).
+--
+-- Type-check the whole corpus:  idris2 --typecheck echidna-verif-proofs.ipkg
+--
+-- Building via this package (rather than a per-file `idris2 --check` loop) gives
+-- a reliable aggregate exit code AND resolves DispatchCorrectness's
+-- `import EchidnaABI.Types` through `depends = echidnaabi` — the echidnaabi
+-- package must be installed first (`idris2 --install src/abi/echidnaabi.ipkg`).
+package echidna-verif-proofs
+
+sourcedir = "."
+
+depends = base, echidnaabi
+
+modules = AxiomCompleteness
+        , AxiomPolicyOrdering
+        , BasicTotality
+        , ClampTrustBounds
+        , DispatchCorrectness
+        , DispatchOrdering
+        , NatLte
+        , ProofStateSerialisation
+        , ProverKindInjectivity
+        , TrustKernelMonotonicity
+        , TrustLevelSoundness