From edd14bc30e3f6080256675fbf7ba7a31ffcf5789 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Thu, 2 Jul 2026 13:11:35 +0000
Subject: [PATCH] ci(abi): typecheck the Idris2 ABI in CI (G34)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The ABI-FFI gate did a Julia structural conformance check and a Zig FFI
build, but nothing ever ran idris2 on the ABI itself — so the 8 proof
modules (Types, Layout, Foreign, Proofs, Semantics, Invariants, FfiSeam,
Capstone) were authored and locally verified against Idris2 0.7.0 but
never compiler-checked in CI. A future edit could break a proof and the
gate would stay green.

Adds an idris2-abi job running 'idris2 --typecheck julianiser-abi.ipkg'
in the SHA-pinned stefan-hoeck/idris2-pack container (same image Axiom.jl
uses), and uncomments idris2 0.7.0 in .tool-versions for local asdf use.
Verified locally: both --build and --typecheck exit 0 on all 8 modules.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UPFC9YQ7g9gc3VnRox42Q1
---
 .github/workflows/abi-ffi-gate.yml | 20 +++++++++++++++++++-
 .tool-versions                     |  5 ++++-
 2 files changed, 23 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/abi-ffi-gate.yml b/.github/workflows/abi-ffi-gate.yml
index f647ba6..f10d0d1 100644
--- a/.github/workflows/abi-ffi-gate.yml
+++ b/.github/workflows/abi-ffi-gate.yml
@@ -4,7 +4,10 @@
 # The Idris2 ABI (src/interface/abi) is the source of truth. This gate fails if
 # the Zig FFI (src/interface/ffi) drifts from it: a declared C function with no
 # export, a mismatched result-code map, or an unrendered template token. A
-# second job builds + tests the Zig FFI under the pinned Zig 0.14.0.
+# second job builds + tests the Zig FFI under the pinned Zig 0.14.0. A third job
+# typechecks the Idris2 ABI itself (idris2 --typecheck) so the proofs cannot rot
+# into a non-compiling state while the structural gate stays green — the ABI was
+# authored and locally verified but never compiler-checked in CI (G34).
 name: ABI-FFI Gate
 
 on:
@@ -43,3 +46,18 @@ jobs:
           echo "/tmp/zig-linux-x86_64-0.14.0" >> "$GITHUB_PATH"
       - name: zig test FFI
         run: zig test src/interface/ffi/src/main.zig -lc
+
+  idris2-abi:
+    name: Idris2 ABI typecheck (Idris2 0.7.0)
+    runs-on: ubuntu-latest
+    # Prebuilt pack image (SHA-pinned) — avoids a ~10-min Chez/Idris2 source
+    # build. Same image the Axiom.jl idris2-abi-check job runs against.
+    container:
+      image: ghcr.io/stefan-hoeck/idris2-pack@sha256:de9781906050dc44704ec6de0108c86f899ef17b2642932b79e00245d613b8ad
+    steps:
+      - uses: actions/checkout@v4
+      - name: idris2 --version
+        run: idris2 --version
+      - name: Typecheck ABI package (Types, Layout, Foreign, Proofs, Semantics, Invariants, FfiSeam, Capstone)
+        working-directory: src/interface/abi
+        run: idris2 --typecheck julianiser-abi.ipkg
diff --git a/.tool-versions b/.tool-versions
index f8af37b..af41c6d 100644
--- a/.tool-versions
+++ b/.tool-versions
@@ -6,4 +6,7 @@
 # elixir 1.18.0
 # erlang 27.2
 # zig 0.14.0
-# idris2 0.7.0
+# Uncommented: the ABI (src/interface/abi) is typechecked in CI (abi-ffi-gate.yml
+# :: idris2-abi) and locally via `asdf install`. Pinned to the version the proofs
+# were verified against.
+idris2 0.7.0