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

.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