fix(proofs+ci): repair proof corpus, unbreak Agda CI, and gate every proof in CI (#234)

## Summary

Brings the full multi-language proof corpus to compile-clean **and**
puts it
under CI so the green checkmark actually means something. **All proof
jobs are
green on this PR** (Coq, Lean 4, Agda, Idris2 ABI + validator).

### CI infrastructure (commit `6c01819`)
- **Agda meta-checker**: `--overwrite-policy=always` on `cabal install`
- **Justfile**: drop duplicate `heal` recipe in `contractile.just`

### Idris2 / Agda scope fixes (commit `7f94f89`)
- `proofs/agda/Basic.agda`,
`verification/proofs/idris2/{DispatchCorrectness,ProverKindInjectivity}.idr`

### Proof corpus repair (commit `0a190ba`)
- **Agda** `DispatchOrdering.agda`: `z<s`/`s<s` → `s≤s z≤n`
- **Coq** `nat.v`, `list.v` (`in_filter` via case-split + `congruence`),
`algebra/GroupTheory.v` (implicit `G`, rewrite directions)
- **Lean4** `Nat/List/Propositional/algebra.GroupTheory`, `ECHIDNA.lean`
- **Idris2** `Validator.idr`: `proof` → `pterm` (reserved keyword)

### 🔒 Proof CI coverage — *the gap this PR closes*

The corpus had **zero CI coverage**: `agda-meta-checker.yml` →
`meta-checker/**`,
`idris2-abi-ci.yml` → `src/abi/**`, and **no Coq/Lean workflow at all**.
So
`proofs/{coq,lean,agda}` and `src/idris` were never type-checked — a
green PR
proved nothing about the proofs.

- **New `dogfood-proofs-ci.yml`** — three jobs (Coq, Lean 4, Agda), each
calling
  a `just` recipe (RSR-H14) so local and CI run identical commands.
- **`idris2-abi-ci.yml`** extended to also type-check the `src/idris`
validator
  (adds `src/idris/**` to the trigger; reuses the Idris2 install).
- **New Justfile recipes**: `proofs{,-coq,-lean,-agda,-idris}`.

**Two latent bugs the absent CI had hidden:**
1. `proofs/lean/lakefile.lean` rooted only `ECHIDNA` (umbrella imported
4 of 6
files); `lake build` actually **failed** (`unknown module prefix
'Basic'`)
because top-level modules weren't in the lib's module space. Now every
file
   is a root and the umbrella imports the whole corpus.
2. `src/idris/echidna-validator.ipkg` declares an executable but
`Validator.idr`
had no `main` → `idris2 --build` failed. Added `main = testValidation`.

### Two CI-environment gotchas found and worked around

- **`taiki-e/install-action` reproducibly `startup_failure`s in this
workflow**
(bisected: header + checkout + `run` steps start fine; adding the action
fails
before any job runs — even though `mvp-smoke.yml` uses the same pin on
`main`).
Worked around by installing every toolchain with plain `run:` steps (apt
+
curl tarballs), matching the idris2/chapel workflows — only
`actions/checkout`
is used. *Worth a follow-up: the repo's allowed-actions policy may need
a
  look, since the same pin works on `main`.*
- **`apt-get --fix-missing` silently dropped `agda-stdlib`** (exit 0, no
library
→ `Installed libraries: (none)`). Agda now installs the binary via apt
and
fetches stdlib **v1.7.3** from GitHub (matching apt's agda 2.6.3), the
same
  deterministic pattern the meta-checker uses.

## Verified locally against real toolchains

| Assistant | Toolchain | Result |
|---|---|---|
| Coq | `coqc` 8.18.0 | 5/5 ✅ |
| Lean 4 | Lean **v4.13.0** (`lake build`) | 6 modules + umbrella ✅ |
| Agda | `agda` 2.6.3 + stdlib **v1.7.3** (fresh GitHub tarball,
isolated AGDA_DIR) | 13/13 ✅ |
| Idris2 | `idris2` 0.8.0 `--typecheck` | ✅ |

…and **green end-to-end on this PR's CI**.

https://claude.ai/code/session_01UAqDQaMwpUqWHUSZekGZWv

---------

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

Author: hyperpolymath

.github/workflows/agda-meta-checker.yml

@@ -49,7 +49,10 @@ jobs:
       - name: Install Agda
         run: |
           cabal update
-          cabal install Agda-2.7.0.1
+          # --overwrite-policy=always: the cached ~/.cabal restore already
+          # carries the agda symlink, so a plain install aborts with
+          # "Path '.../bin/agda' already exists" on a warm cache.
+          cabal install Agda-2.7.0.1 --overwrite-policy=always
 
       - name: Install Agda standard library
         run: |

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

@@ -0,0 +1,132 @@
+# SPDX-License-Identifier: MPL-2.0
+# Gates the ECHIDNA dogfood proof corpus: every theorem under proofs/{coq,lean,agda}
+# must type-check. These proofs had no CI coverage before this workflow -- the other
+# proof workflows are path-filtered to meta-checker/** (agda-meta-checker) and
+# src/abi/** (idris2-abi-ci), and there was no Coq or Lean workflow at all, so
+# regressions in proofs/ landed silently.
+#
+# Toolchains are installed with plain `run:` steps (apt / curl tarballs, matching the
+# idris2 + chapel workflows) rather than marketplace setup actions: a third-party
+# setup action (taiki-e/install-action) reproducibly tripped a startup_failure in this
+# workflow's context, so this workflow uses only actions/checkout plus run steps.
+# `just` stays the single source of truth for the commands (RSR-H14) -- CI installs it
+# and calls the same recipes a developer runs locally.
+name: Dogfood Proof Corpus
+
+on:
+  push:
+    branches: [main]
+    paths:
+      - 'proofs/**'
+      - 'Justfile'
+      - '.github/workflows/dogfood-proofs-ci.yml'
+  pull_request:
+    branches: [main]
+    paths:
+      - 'proofs/**'
+      - 'Justfile'
+      - '.github/workflows/dogfood-proofs-ci.yml'
+  workflow_dispatch:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  coq:
+    name: Coq
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      - name: Install Coq
+        run: |
+          set -euo pipefail
+          sudo apt-get update -qq || sudo apt-get update -qq --fix-missing
+          sudo apt-get install -y --fix-missing coq
+          coqc --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 Coq corpus
+        run: just proofs-coq
+
+  lean:
+    name: Lean 4
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      - name: Install elan + Lean toolchain
+        run: |
+          set -euo pipefail
+          # The toolchain version is pinned by proofs/lean/lean-toolchain; lake reads
+          # it and fetches that exact Lean on first invocation.
+          curl -fsSL --retry 3 \
+            https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            -o /tmp/elan-init.sh
+          sh /tmp/elan-init.sh -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - 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: Build Lean corpus
+        run: just proofs-lean
+
+  agda:
+    name: Agda
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      - name: Install Agda + standard library
+        run: |
+          set -euo pipefail
+          sudo apt-get update -qq
+          sudo apt-get install -y agda
+          agda --version
+          # stdlib from GitHub, pinned to v1.7.3 (the version apt ships for the
+          # agda 2.6.3 the corpus is verified against). apt's agda-stdlib is NOT
+          # used: `apt --fix-missing` can silently drop it, leaving the library
+          # unregistered ("Installed libraries: (none)"). The corpus .agda-lib in
+          # proofs/agda is auto-detected from the working dir; this registration
+          # resolves its `depend: standard-library`.
+          cd /tmp
+          curl -fsSL --retry 3 -o agda-stdlib.tar.gz \
+            https://github.com/agda/agda-stdlib/archive/refs/tags/v1.7.3.tar.gz
+          tar xzf agda-stdlib.tar.gz
+          mkdir -p ~/.agda
+          echo "/tmp/agda-stdlib-1.7.3/standard-library.agda-lib" > ~/.agda/libraries
+          echo "standard-library" > ~/.agda/defaults
+
+      - 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 Agda corpus
+        run: just proofs-agda

.github/workflows/idris2-abi-ci.yml

@@ -5,10 +5,12 @@ on:
   push:
     paths:
       - 'src/abi/**'
+      - 'src/idris/**'
       - '.github/workflows/idris2-abi-ci.yml'
   pull_request:
     paths:
       - 'src/abi/**'
+      - 'src/idris/**'
       - '.github/workflows/idris2-abi-ci.yml'
 
 # Cause-B mitigation (#77): cancel superseded runs so stacked pushes
@@ -57,6 +59,16 @@ jobs:
           idris2 --build echidnaabi.ipkg
           echo "✓ All ABI modules type-check successfully"
 
+      - name: Type-check Idris2 proof validator (src/idris)
+        run: |
+          # Mirrors `just proofs-idris`. --typecheck (not --build) so no codegen
+          # backend is required; the declared executable's `main` is exercised
+          # by `idris2 --build` locally where a backend is present.
+          cd src/idris
+          echo "=== Type-checking ECHIDNA proof validator ==="
+          idris2 --typecheck echidna-validator.ipkg
+          echo "✓ Validator modules type-check successfully"
+
       - name: Verify no dangerous patterns
         run: |
           echo "=== Scanning for dangerous patterns in ABI code ==="

.gitignore

@@ -190,6 +190,12 @@ proofs/coq/**/*.vok
 proofs/coq/**/*.glob
 proofs/coq/**/.*.aux
 proofs/agda/**/*.agdai
+proofs/agda/**/dist-newstyle/
+proofs/lean/**/.lake/
+proofs/lean/**/.lia.cache
+proofs/lean/**/.nia.cache
+.lia.cache
+.nia.cache
 proofs/metamath/.metamath*
 target/
 node_modules/

Justfile

@@ -244,6 +244,46 @@ test-s4-loop:
     @echo "Test will skip cleanly if the endpoint is unreachable."
     cargo test --features verisim --test s4_loop_closure -- --nocapture
 
+# ── Dogfood proof corpus (proofs/{coq,lean,agda} + src/idris validator) ──
+# Each recipe assumes its toolchain is already installed (see `just doctor`);
+# CI installs the toolchains first, then calls these so local and CI run the
+# exact same commands.
+
+# Type-check the whole dogfood proof corpus across every assistant.
+proofs: proofs-coq proofs-lean proofs-agda proofs-idris
+
+# Compile the Coq proof corpus (proofs/coq/**/*.v).
+proofs-coq:
+    #!/usr/bin/env bash
+    set -euo pipefail
+    cd proofs/coq
+    for f in $(find . -name '*.v' | sort); do
+        echo "coqc $f"
+        coqc -q "$f"
+    done
+    echo "Coq corpus: all files type-check"
+
+# Build the Lean 4 proof corpus via Lake (proofs/lean).
+proofs-lean:
+    cd proofs/lean && lake build
+
+# Type-check the Agda proof corpus (proofs/agda/*.agda).
+proofs-agda:
+    #!/usr/bin/env bash
+    set -euo pipefail
+    # Agda writes UTF-8 to stdout and aborts under a non-UTF-8 locale (C/POSIX).
+    export LC_ALL="${LC_ALL:-C.UTF-8}"
+    cd proofs/agda
+    for f in $(find . -name '*.agda' -not -path './_build/*' -not -path './dist-newstyle/*' | sort); do
+        echo "agda $f"
+        agda "$f"
+    done
+    echo "Agda corpus: all files type-check"
+
+# Type-check the Idris2 validator (src/idris) — --typecheck needs no codegen backend.
+proofs-idris:
+    cd src/idris && idris2 --typecheck echidna-validator.ipkg
+
 # Format code
 fmt:
     cargo fmt

contractile.just

@@ -190,13 +190,10 @@ intend-list:
     @echo ''
     @echo 'Run `cat .machine_readable/contractiles/intend/Intentfile.a2ml` for the source of truth.'
 
-# ── HEAL (recovery shortcuts referenced by bust/dust recipes) ─────────
-
-heal:
-    @echo 'just heal: workspace healing entry point'
-    @cargo --version >/dev/null 2>&1 && echo '  rust toolchain OK' || echo '  rust toolchain MISSING'
-    @julia --version >/dev/null 2>&1 && echo '  julia OK' || echo '  julia MISSING — see juliaup'
-    @echo 'For prover binaries: just heal-provers'
+# ── HEAL-PROVERS (recovery shortcut referenced by bust/dust recipes) ──
+# NB: `heal` itself is defined in the root Justfile. Defining it here too
+# made `just` abort with a duplicate-recipe error across the `import?`,
+# which broke every `just` invocation (and thus MVP Smoke's `just mvp-env`).
 
 heal-provers:
     @echo 'heal-provers: install missing Tier-1 prover binaries'

proofs/agda/Basic.agda

@@ -8,6 +8,17 @@
 
 module Basic where
 
+-- Propositional equality at module scope (used by trans-assoc, id-left, id-right)
+data _≡_ {A : Set} (x : A) : A → Set where
+  refl : x ≡ x
+
+infix 4 _≡_
+
+-- Natural numbers at module scope (used by id-nat)
+data ℕ : Set where
+  zero : ℕ
+  suc  : ℕ → ℕ
+
 --------------------------------------------------------------------------------
 -- Identity Proof
 --------------------------------------------------------------------------------
@@ -21,10 +32,6 @@ id x = x
 -- Example: identity for a specific type
 id-nat : (n : ℕ) → ℕ
 id-nat = id
-  where
-    data ℕ : Set where
-      zero : ℕ
-      suc  : ℕ → ℕ
 
 -- The identity function can also be written explicitly with a lambda
 id′ : {A : Set} → A → A
@@ -75,28 +82,14 @@ trans-assoc : {A B C D : Set}
             → (f : A → B) → (g : B → C) → (h : C → D)
             → (h ∘ (g ∘ f)) ≡ ((h ∘ g) ∘ f)
 trans-assoc f g h = refl
-  where
-    -- Propositional equality
-    data _≡_ {A : Set} (x : A) : A → Set where
-      refl : x ≡ x
-
-    infix 4 _≡_
 
 -- Proof that identity is a left identity for composition
 id-left : {A B : Set} → (f : A → B) → (id ∘ f) ≡ f
 id-left f = refl
-  where
-    data _≡_ {A : Set} (x : A) : A → Set where
-      refl : x ≡ x
-    infix 4 _≡_
 
 -- Proof that identity is a right identity for composition
 id-right : {A B : Set} → (f : A → B) → (f ∘ id) ≡ f
 id-right f = refl
-  where
-    data _≡_ {A : Set} (x : A) : A → Set where
-      refl : x ≡ x
-    infix 4 _≡_
 
 --------------------------------------------------------------------------------
 -- Additional Basic Combinators
@@ -125,13 +118,9 @@ infixr 0 _$_
 --------------------------------------------------------------------------------
 
 module CombinatorLaws where
-  data _≡_ {A : Set} (x : A) : A → Set where
-    refl : x ≡ x
-
-  infix 4 _≡_
-
   -- SKK = I (a famous combinator identity)
-  SKK : {A : Set} → (x : A) → S const const x ≡ id x
+  -- The second const needs B instantiated explicitly to resolve the implicit argument.
+  SKK : {A : Set} → (x : A) → S const (const {B = A}) x ≡ id x
   SKK x = refl
 
   -- Flip is involutive (applying it twice gets you back where you started)
@@ -164,9 +153,6 @@ uncurry f (x , y) = f x y
 
 -- Proof that curry and uncurry are inverses
 module CurryUncurryLaws where
-  data _≡_ {A : Set} (x : A) : A → Set where
-    refl : x ≡ x
-
   -- INTENTIONAL AXIOM: Function extensionality (funext)
   -- Justification: funext is consistent with Agda's type theory and is
   -- provable in Cubical Agda (--cubical). In plain Agda it must be

proofs/agda/DispatchOrdering.agda

@@ -14,7 +14,7 @@ module DispatchOrdering where
 open import Data.Fin       using (Fin; zero; suc; toℕ; _<_)
 open import Data.Fin.Properties
   using (<-irrefl; <-trans; <-cmp; <-isStrictTotalOrder)
-open import Data.Nat.Base  using (z<s; s<s)
+open import Data.Nat.Base  using (z≤n; s≤s)
 open import Relation.Binary.Definitions
   using (Irreflexive; Transitive; Trichotomous; Asymmetric)
 open import Relation.Binary.Structures
@@ -79,26 +79,26 @@ stage-strictTotalOrder = <-isStrictTotalOrder
 
 -- Integrity strictly precedes Sandbox.
 integrity-before-sandbox : Integrity < Sandbox
-integrity-before-sandbox = z<s
+integrity-before-sandbox = s≤s z≤n
 
 -- Integrity strictly precedes Verify.
 integrity-before-verify : Integrity < Verify
-integrity-before-verify = z<s
+integrity-before-verify = s≤s z≤n
 
 -- Integrity strictly precedes Certs.
 integrity-before-certs : Integrity < Certs
-integrity-before-certs = z<s
+integrity-before-certs = s≤s z≤n
 
 -- Integrity strictly precedes Axioms.
 integrity-before-axioms : Integrity < Axioms
-integrity-before-axioms = z<s
+integrity-before-axioms = s≤s z≤n
 
 -- Integrity strictly precedes Confidence.
 integrity-before-confidence : Integrity < Confidence
-integrity-before-confidence = z<s
+integrity-before-confidence = s≤s z≤n
 
 -- The general statement: for any stage that is not Integrity, Integrity precedes it.
--- We pattern-match: zero would give h refl : ⊥ (absurd); any suc s gives z<s.
+-- We pattern-match: zero would give h refl : ⊥ (absurd); any suc s gives s≤s z≤n.
 integrity-precedes : (s : Stage) → Integrity ≢ s → Integrity < s
 integrity-precedes zero    h = ⊥-elim (h refl)
-integrity-precedes (suc s) _ = z<s
+integrity-precedes (suc s) _ = s≤s z≤n