fix(cartridges): type-check all cartridge ABIs under Idris2 0.8.0 + gate them in CI (#191)

## What

Makes **all 104 cartridge ABI modules** type-check under the pinned
toolchain (Idris2 0.8.0, Chez) — previously 21 cartridges failed — and
adds the CI gate that was missing so they can't drift again.

Local verification: `scripts/typecheck-proofs.sh` → **PASS=105 FAIL=0**
(core ABI + 104 cartridge ABIs); `scripts/check-trusted-base.sh` → **5
sanctioned class-(J) axioms, 0 undocumented escapes**.

## Why this happened

Nothing in CI ever ran `idris2 --typecheck` on `cartridges/**/abi`:
`abi-drift.yml` only runs `iseriser`'s *structural* manifest check, and
the Justfile's `typecheck` recipe covered just **5 of ~50** cartridge
ABIs and was never wired into a workflow. So 99 ABIs rotted undetected
against 0.8.0.

## Fixes (by root cause — theorem statements & axiom budget unchanged)

- **Reserved-keyword record fields** (0.8.0 reserves these):
`total`→`totalCount` (conflow, panic-attack, reposystem),
`data`→`payload` (ephapax), `namespace`→`namespaceName` (k8s, ml),
`prefix`→`txnPrefix` (matrix).
- **Missing imports**: `Data.List` for `NonEmpty` (panic-attack,
stapeln, civic-connect, hypatia, local-coord/Protocol); `Data.Nat` for
`LTE` (pmpl).
- **`lteTransitive`→`transitive`** + explicit `{s,n}` binders (hypatia).
- **Visibility/layout**: bare `public`→`public export`; modifier on its
own line so the `where`-block isn't mis-indented vs `record`/`data`
(academic-workflow, hesiod); unqualified `interface` names.
- **Named fields are GADT-only**: `data X = MkC (n : T)` → `MkC T`
(model-router, burble-admin).
- **`octadLength`** via `Data.Vect.lengthCorrect` — `Refl` can't reduce
`length` on an abstract `Vect` (verisimdb).
- **Constructor-name collision**: `ValidTransition`'s proof-only
`Connect`/`Disconnect` → `TConnect`/`TDisconnect`, so the FFI-bearing
`PostgresqlAction` enum keeps its names (postgresql).
- **Large type-level `Nat` blowup**: `ValidPort` takes explicit `LTE`
proofs via `Data.Nat.lteReflectsLTE` (builtin-Integer path), mirroring
`SafeWebSocket`'s `FrameSizeSafeUpTo` — typecheck **>90s (OOM) → ~2s**
(local-coord).
- **`IsLoopback` giant-Nat-literal function** (`IsLoopback 5178 = ()`,
~150s) → top-level GADT (~1s), matching the other adapters (bofig,
ephapax, fireflag, sanctify).
- **Pre-existing proof bug** surfaced once the blowup cleared:
`identityDoesNotEnableFederation` relied on a nullary CAF reducing in
the unifier; restated over `LocalOnly` directly (local-coord/Identity).

## Durable gate

- `scripts/typecheck-proofs.sh` — type-checks core ABI + **every**
cartridge ABI.
- `scripts/check-trusted-base.sh` — the audit
`PROOF-NEEDS.md`/`docs/proof-debt.md` already reference but which never
existed.
- `.github/workflows/proofs.yml` — runs both, installing the pinned
Idris2 via asdf (`.tool-versions`).
- `Justfile` `typecheck`/`verify-no-believe-me` now delegate to the
scripts (one source of truth).

## Note

`e2e.yml` triggers on `cartridges/**` and is currently red on `main` for
an unrelated reason (the `/menu` + feedback-o-tron contract drift
between `openapi.yaml`, the Elixir router, and `tests/e2e_full.sh`).
That's tracked/fixed separately as deliverable-2; it is not introduced
by this PR.

🤖 Draft via Claude Code.

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

---------

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

Author: hyperpolymath

.github/workflows/proofs.yml

@@ -0,0 +1,99 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# Proofs Gate — type-check every Idris2 proof + enforce the trusted base.
+#
+# Closes the gap that let cartridge ABIs rot into non-compiling states:
+# abi-drift.yml only runs iseriser's *structural* manifest check, and nothing
+# ever ran `idris2 --typecheck` on cartridges/**/abi in CI (the Justfile's old
+# `typecheck` recipe covered only 5 of ~50 cartridge ABIs and was never wired
+# into a workflow). This gate type-checks the core ABI package AND every
+# cartridge ABI under the pinned toolchain (.tool-versions → idris2 0.8.0), and
+# runs the trusted-base audit so no new believe_me / axiom slips in.
+name: Proofs Gate
+
+on:
+  push:
+    branches: [main]
+    paths:
+      - 'src/abi/**'
+      - 'cartridges/**/abi/**'
+      - 'verification/**'
+      - 'scripts/check-trusted-base.sh'
+      - 'scripts/typecheck-proofs.sh'
+      - '.github/workflows/proofs.yml'
+      - '.tool-versions'
+  pull_request:
+    branches: [main]
+    paths:
+      - 'src/abi/**'
+      - 'cartridges/**/abi/**'
+      - 'verification/**'
+      - 'scripts/check-trusted-base.sh'
+      - 'scripts/typecheck-proofs.sh'
+      - '.github/workflows/proofs.yml'
+      - '.tool-versions'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: proofs-${{ github.ref }}
+  cancel-in-progress: ${{ github.event_name == 'pull_request' }}
+
+jobs:
+  # Cheap, dependency-free gate: scan for unsound constructs + axiom-count drift.
+  trusted-base:
+    name: Trusted-base audit (no new axioms)
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+      - name: Enforce trusted base
+        run: bash scripts/check-trusted-base.sh
+
+  # Full type-check of the core ABI + every cartridge ABI under the pinned Idris2.
+  typecheck:
+    name: Idris2 type-check (core + all cartridge ABIs)
+    runs-on: ubuntu-latest
+    timeout-minutes: 45
+    steps:
+      - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      - name: Read pinned Idris2 version
+        id: ver
+        run: echo "idris2=$(awk '/^idris2 /{print $2}' .tool-versions)" >> "$GITHUB_OUTPUT"
+
+      - name: Install build deps (Chez Scheme + GMP)
+        run: sudo apt-get update && sudo apt-get install -y chezscheme libgmp-dev build-essential
+
+      - name: Cache asdf + Idris2 toolchain
+        uses: actions/cache@d4323d4df104b026a6aa633fdb11d772146be0bf # v4.2.2
+        with:
+          path: ~/.asdf
+          key: idris2-asdf-${{ runner.os }}-${{ steps.ver.outputs.idris2 }}
+
+      - name: Install asdf + Idris2 ${{ steps.ver.outputs.idris2 }}
+        env:
+          # Ubuntu's chezscheme package installs the interpreter as `scheme`;
+          # Idris2's bootstrap Makefile reads $SCHEME (defaults to `chez`).
+          SCHEME: scheme
+        run: |
+          set -euo pipefail
+          if [ ! -f "$HOME/.asdf/asdf.sh" ]; then
+            git clone --depth 1 --branch v0.14.0 https://github.com/asdf-vm/asdf.git "$HOME/.asdf"
+          fi
+          . "$HOME/.asdf/asdf.sh"
+          asdf plugin add idris2 || true
+          asdf install idris2 "${{ steps.ver.outputs.idris2 }}"
+          asdf global  idris2 "${{ steps.ver.outputs.idris2 }}"
+
+      - name: Put Idris2 on PATH
+        run: echo "$HOME/.asdf/shims" >> "$GITHUB_PATH"
+
+      - name: Idris2 version
+        run: idris2 --version
+
+      - name: Type-check all proofs (core + cartridges)
+        run: bash scripts/typecheck-proofs.sh

Justfile

@@ -398,15 +398,8 @@ lint: verify-no-believe-me typecheck
 # `--check --package boj boj.ipkg` form is invalid — `--check` is for .idr
 # files and `--package` looks up an *installed* package, so it never ran).
 typecheck:
-    @echo "Type-checking core ABI (17 modules)..."
-    cd src/abi && idris2 --typecheck boj.ipkg
-    @echo "Type-checking cartridge ABIs..."
-    cd cartridges/fleet-mcp/abi && idris2 --typecheck fleet-mcp.ipkg
-    cd cartridges/nesy-mcp/abi && idris2 --typecheck nesy-mcp.ipkg
-    cd cartridges/database-mcp/abi && idris2 --typecheck database-mcp.ipkg
-    cd cartridges/agent-mcp/abi && idris2 --typecheck agent-mcp.ipkg
-    cd cartridges/feedback-mcp/abi && idris2 --typecheck feedback-mcp.ipkg
-    @echo "All ABI files type-check!"
+    @echo "Type-checking core ABI + every cartridge ABI (pinned Idris2)..."
+    bash scripts/typecheck-proofs.sh
 
 # Verify the trusted base: no unsound constructs beyond the sanctioned axioms.
 #
@@ -417,26 +410,7 @@ typecheck:
 # This recipe fails on any believe_me/assert_* outside that module, and also
 # fails if the audited axiom count drifts from 5 (keep the docs in sync).
 verify-no-believe-me:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    AXIOM_FILE="src/abi/Boj/SafetyLemmas.idr"
-    echo "Scanning for unsound constructs outside the sanctioned axiom module..."
-    FOUND=$(grep -rn 'believe_me\|assert_total\|assert_smaller' --include='*.idr' src/ cartridges/ 2>/dev/null \
-        | grep -v -- '--.*believe_me' | grep -v '|||.*believe_me' \
-        | grep -v -- '--.*Admitted' | grep -v '|||.*Admitted' \
-        | grep -v "^${AXIOM_FILE}:" || true)
-    if [ -n "$FOUND" ]; then
-        echo "CRITICAL: Found undocumented unsound constructs:"
-        echo "$FOUND"
-        exit 1
-    fi
-    AXIOM_COUNT=$(grep -c 'believe_me ()' "$AXIOM_FILE" 2>/dev/null || true)
-    if [ "$AXIOM_COUNT" != "5" ]; then
-        echo "CRITICAL: expected exactly 5 sanctioned class-(J) axioms in $AXIOM_FILE, found $AXIOM_COUNT."
-        echo "If this change is intentional, update PROOF-NEEDS.md and docs/proof-debt.md to match."
-        exit 1
-    fi
-    echo "OK: no undocumented unsound constructs; $AXIOM_COUNT sanctioned class-(J) axioms (all in SafetyLemmas.idr)."
+    bash scripts/check-trusted-base.sh
 
 # Full verification suite: type-check + zero believe_me + build + test
 verify: typecheck verify-no-believe-me build test

cartridges/academic-workflow-mcp/abi/AcademicWorkflow.idr

@@ -4,7 +4,8 @@
 module AcademicWorkflow
 
 ||| Paper metadata
-public record Paper where
+public export
+record Paper where
   constructor MkPaper
   title : String
   authors : List String
@@ -13,35 +14,40 @@ public record Paper where
   abstract : String
 
 ||| Citation format
-public data CitationFormat =
-  | BibTeX
+public export
+data CitationFormat
+  = BibTeX
   | CSL
   | RIS
   | EndNote
 
 ||| Proof that a citation format is supported
-public data Supported : CitationFormat -> Type where
+public export
+data Supported : CitationFormat -> Type where
   SupportedBibTeX : Supported BibTeX
   SupportedCSL : Supported CSL
   SupportedRIS : Supported RIS
   SupportedEndNote : Supported EndNote
 
 ||| Review annotation
-public record ReviewNote where
+public export
+record ReviewNote where
   constructor MkReviewNote
   page : Nat
   text : String
   category : String  -- "typo", "unclear", "question", "suggestion"
 
 ||| Zotero collection reference
-public record ZoteroCollection where
+public export
+record ZoteroCollection where
   constructor MkZoteroCollection
   id : String
   name : String
   itemCount : Nat
 
 ||| Academic workflow operations
-public interface AcademicWorkflow.Workflow (m : Type -> Type) where
+public export
+interface Workflow (m : Type -> Type) where
   ||| Search Zotero collections
   searchZotero : (query : String) -> m (List ZoteroCollection)
 
@@ -63,7 +69,8 @@ public interface AcademicWorkflow.Workflow (m : Type -> Type) where
   exportCollection : (collectionId : String) -> m String
 
 ||| Loopback proof: academic-mcp runs on 127.0.0.1:5174
-public data IsLoopback : (port : Nat) -> Type where
+public export
+data IsLoopback : (port : Nat) -> Type where
   LoopbackProof : IsLoopback 5174
 
 export

cartridges/bofig-mcp/abi/Bofig.idr

@@ -1,7 +1,7 @@
 -- SPDX-License-Identifier: MPL-2.0
 -- Bofig Cartridge ABI — Evidence graph query interface
 
-module ABI.Bofig
+module Bofig
 
 %language ElabReflection
 
@@ -75,10 +75,12 @@ interface Bofig.Graph where
   -- Get graph statistics
   getGraphStats : IO (Nat, Nat)  -- (nodes, edges)
 
-  -- Loopback proof: cartridge runs on localhost only
-  IsLoopback : (port : Nat) -> Type
-  IsLoopback 5178 = ()
 
+||| Loopback proof: cartridge binds on localhost only.
 public export
-Loopback.proof : IsLoopback 5178
-Loopback.proof = ()
+data IsLoopback : (port : Nat) -> Type where
+  LoopbackProof : IsLoopback 5178
+
+export
+loopbackInvariant : IsLoopback 5178
+loopbackInvariant = LoopbackProof

cartridges/burble-admin-mcp/abi/BurbleAdmin/Protocol.idr

@@ -48,7 +48,7 @@ data RequiresPermission : Operation -> PermLevel -> Type where
 
 ||| Room capacity is bounded (1-500 participants)
 public export
-data RoomCapacity = MkCapacity (n : Fin 500)
+data RoomCapacity = MkCapacity (Fin 500)
 
 -- ═══════════════════════════════════════════════════════════════════════
 -- C ABI Exports

cartridges/civic-connect-mcp/abi/CivicConnect/Protocol.idr

@@ -6,6 +6,7 @@
 module CivicConnect.Protocol
 
 import Data.Nat
+import Data.List
 
 ||| CivicConnect operation codes.
 public export

cartridges/conflow-mcp/abi/Conflow/Protocol.idr

@@ -42,8 +42,8 @@ record ApplyResult where
   constructor MkApplyResult
   applied : Nat
   skipped : Nat
-  total   : Nat
-  sumPrf  : applied + skipped = total
+  totalCount   : Nat
+  sumPrf  : applied + skipped = totalCount
 
 ||| Proof: a valid config with no errors has empty error list.
 export

cartridges/ephapax-mcp/abi/Ephapax.idr

@@ -1,7 +1,7 @@
 -- SPDX-License-Identifier: MPL-2.0
 -- Ephapax Cartridge ABI — Proof-compiler query interface
 
-module ABI.Ephapax
+module Ephapax
 
 %language ElabReflection
 
@@ -31,7 +31,7 @@ record QueryResult where
   constructor MkQueryResult
   success : Bool
   message : String
-  data : String
+  payload : String
 
 -- Type-checking result
 public export
@@ -56,10 +56,12 @@ interface Ephapax.Compiler where
   -- Analyze proof complexity and dependencies
   analyzeProof : String -> IO QueryResult
 
-  -- Check if cartridge port is loopback-only (compile-time proof)
-  IsLoopback : (port : Nat) -> Type
-  IsLoopback 5175 = ()
 
+||| Loopback proof: cartridge binds on localhost only.
 public export
-Loopback.proof : IsLoopback 5175
-Loopback.proof = ()
+data IsLoopback : (port : Nat) -> Type where
+  LoopbackProof : IsLoopback 5175
+
+export
+loopbackInvariant : IsLoopback 5175
+loopbackInvariant = LoopbackProof

cartridges/fireflag-mcp/abi/Fireflag.idr

@@ -1,7 +1,7 @@
 -- SPDX-License-Identifier: MPL-2.0
 -- Fireflag Cartridge ABI — Extension-to-MCP mapping interface
 
-module ABI.Fireflag
+module Fireflag
 
 %language ElabReflection
 
@@ -63,10 +63,12 @@ interface Fireflag.Mapper where
   -- Discover extensions in directory
   discoverExtensions : String -> IO (List ExtensionMetadata)
 
-  -- Loopback proof: cartridge runs on localhost only
-  IsLoopback : (port : Nat) -> Type
-  IsLoopback 5177 = ()
 
+||| Loopback proof: cartridge binds on localhost only.
 public export
-Loopback.proof : IsLoopback 5177
-Loopback.proof = ()
+data IsLoopback : (port : Nat) -> Type where
+  LoopbackProof : IsLoopback 5177
+
+export
+loopbackInvariant : IsLoopback 5177
+loopbackInvariant = LoopbackProof

cartridges/hesiod-mcp/abi/Hesiod.idr

@@ -4,8 +4,9 @@
 module Hesiod
 
 ||| DNS record type enumeration (proof-indexed)
-public data DNSRecordType =
-  | A              -- IPv4 address
+public export
+data DNSRecordType
+  = A              -- IPv4 address
   | AAAA           -- IPv6 address
   | CNAME          -- Canonical name
   | MX             -- Mail exchange
@@ -15,7 +16,8 @@ public data DNSRecordType =
   | SRV            -- Service record
 
 ||| Proof that a record type is queryable
-public data Queryable : DNSRecordType -> Type where
+public export
+data Queryable : DNSRecordType -> Type where
   QueryableA : Queryable A
   QueryableAAAA : Queryable AAAA
   QueryableCNAME : Queryable CNAME
@@ -26,23 +28,26 @@ public data Queryable : DNSRecordType -> Type where
   QueryableSRV : Queryable SRV
 
 ||| DNS response record
-public record DNSRecord where
+public export
+record DNSRecord where
   constructor MkDNSRecord
   name : String
   type : DNSRecordType
   ttl : Nat
   value : String
 
 ||| Lookup result type (success or failure)
-public data LookupResult : Type where
+public export
+data LookupResult : Type where
   Success : (records : List DNSRecord) -> LookupResult
   NotFound : (hostname : String) -> LookupResult
   NetworkError : (message : String) -> LookupResult
   Timeout : (hostname : String) -> (seconds : Nat) -> LookupResult
 
 ||| Type-safe DNS lookup interface
 ||| Proof ensures only valid record types are queried
-public interface Hesiod.Lookup (m : Type -> Type) where
+public export
+interface Lookup (m : Type -> Type) where
   ||| Query DNS records for a hostname
   ||| @hostname The domain to query
   ||| @rectype The record type to look up
@@ -59,7 +64,8 @@ public interface Hesiod.Lookup (m : Type -> Type) where
                Queryable rectype -> m (List LookupResult)
 
 ||| Loopback proof: hesiod-mcp only runs on localhost:5173
-public data IsLoopback : (port : Nat) -> Type where
+public export
+data IsLoopback : (port : Nat) -> Type where
   LoopbackProof : IsLoopback 5173
 
 export