ci: add ABI↔FFI conformance gate

.github/workflows/abi-ffi-gate.yml

@@ -0,0 +1,38 @@
+# SPDX-License-Identifier: MPL-2.0
+# abi-ffi-gate.yml — enforce that the Zig FFI conforms to the Idris2 ABI.
+#
+# 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.
+name: ABI-FFI Gate
+
+on:
+  pull_request:
+  push:
+    branches: [main, master]
+
+permissions:
+  contents: read
+
+jobs:
+  conformance:
+    name: ABI ↔ FFI structural conformance
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Run ABI-FFI gate
+        run: python3 scripts/abi-ffi-gate.py
+
+  zig-build:
+    name: Zig FFI builds + tests (Zig 0.14.0)
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Install Zig 0.14.0
+        run: |
+          curl -fsSL https://ziglang.org/download/0.14.0/zig-linux-x86_64-0.14.0.tar.xz -o /tmp/zig.tar.xz
+          tar -xf /tmp/zig.tar.xz -C /tmp
+          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

Justfile

@@ -128,3 +128,9 @@ crg-badge:
       D) color="orange" ;; E) color="red" ;; F) color="critical" ;; \
       *) color="lightgrey" ;; esac; \
     echo "[![CRG $$grade](https://img.shields.io/badge/CRG-$$grade-$$color?style=flat-square)](https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades)"
+
+# Install dev dependencies (invoked by the devcontainer postCreateCommand).
+# Installs the pinned Zig FFI toolchain, then warms the Cargo cache.
+deps:
+    ./scripts/install-zig.sh
+    cargo fetch

scripts/abi-ffi-gate.py

@@ -0,0 +1,103 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# abi-ffi-gate.py — fail (exit 1) if the Zig FFI does not conform to the Idris2
+# ABI. The Idris2 ABI is the source of truth. Checks, with no toolchain needed:
+#
+#   1. the Zig FFI carries no unrendered `{{...}}` template tokens;
+#   2. every `%foreign "C:<name>"` symbol declared anywhere in the ABI .idr
+#      sources is exported by the Zig FFI (`export fn <name>`);
+#   3. the Zig `Result = enum(c_int)` and the Idris `resultToInt` agree on BOTH
+#      names and integer values (the `Error`/`err` spelling is treated as one).
+#
+# Usage: python3 scripts/abi-ffi-gate.py [repo_root]   (defaults to cwd)
+
+import os
+import re
+import sys
+import glob
+
+
+def camel_to_snake(s):
+    return re.sub(r"(?<!^)(?=[A-Z])", "_", s).lower()
+
+
+def canon_rc(name):
+    n = name.lower()
+    return "error" if n in ("err", "error") else n
+
+
+def find_result_enum(zig):
+    """Return {variant: value} for the C-ABI Result enum, or {}."""
+    best = {}
+    for m in re.finditer(r"enum\s*\(\s*c_int\s*\)\s*\{(.*?)\}", zig, re.S):
+        body = m.group(1)
+        variants = {}
+        for vm in re.finditer(r'@?"?([A-Za-z_][A-Za-z0-9_]*)"?\s*=\s*(\d+)', body):
+            variants[canon_rc(vm.group(1))] = int(vm.group(2))
+        # The Result enum is the one starting at ok = 0.
+        if variants.get("ok") == 0 and len(variants) > len(best):
+            best = variants
+    return best
+
+
+def main():
+    root = sys.argv[1] if len(sys.argv) > 1 else "."
+    name = os.path.basename(os.path.abspath(root))
+    abi_dir = os.path.join(root, "src/interface/abi")
+    zig_path = os.path.join(root, "src/interface/ffi/src/main.zig")
+    errs = []
+
+    idr_files = [
+        p for p in glob.glob(os.path.join(abi_dir, "**", "*.idr"), recursive=True)
+        if os.sep + "build" + os.sep not in p
+    ]
+    if not idr_files:
+        print(f"ABI-FFI GATE: SKIP ({name}) — no Idris2 ABI .idr files under {abi_dir}")
+        return 0
+    if not os.path.exists(zig_path):
+        print(f"ABI-FFI GATE: FAIL ({name}) — no Zig FFI at {zig_path}")
+        return 1
+
+    idr = "\n".join(open(p, encoding="utf-8").read() for p in idr_files)
+    zig = open(zig_path, encoding="utf-8").read()
+
+    # 1. unrendered template tokens
+    toks = sorted(set(re.findall(r"\{\{[A-Za-z0-9_]+\}\}", zig)))
+    if toks:
+        errs.append(f"Zig FFI has unrendered template tokens: {toks}")
+
+    # 2. foreign C symbols must be exported
+    csyms = sorted(set(re.findall(r"C:([A-Za-z0-9_]+)", idr)))
+    exports = set(re.findall(r"export fn ([A-Za-z0-9_]+)", zig))
+    missing = [s for s in csyms if s not in exports]
+    if missing:
+        errs.append(f"{len(missing)} ABI function(s) not exported by the Zig FFI: {missing}")
+
+    # 3. result-code map (names + values) must agree
+    idr_rc = {}
+    for m in re.finditer(r"resultToInt\s+([A-Za-z0-9]+)\s*=\s*(\d+)", idr):
+        idr_rc[canon_rc(camel_to_snake(m.group(1)))] = int(m.group(2))
+    zig_rc = find_result_enum(zig)
+    if idr_rc and not zig_rc:
+        errs.append("no Zig `enum(c_int)` Result block (with `ok = 0`) found to compare result codes")
+    elif idr_rc and zig_rc and idr_rc != zig_rc:
+        errs.append(
+            "Result-code map differs (name or value):\n"
+            f"      Idris resultToInt: {dict(sorted(idr_rc.items()))}\n"
+            f"      Zig   Result enum: {dict(sorted(zig_rc.items()))}"
+        )
+
+    if errs:
+        print(f"ABI-FFI GATE: FAIL ({name})")
+        for e in errs:
+            print("  - " + e)
+        return 1
+    print(f"ABI-FFI GATE: OK ({name}) — {len(csyms)} ABI functions exported, "
+          f"{len(idr_rc)} result codes match")
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())

scripts/install-zig.sh

@@ -0,0 +1,59 @@
+#!/bin/sh
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# install-zig.sh — install the pinned Zig toolchain (the Zig FFI bridge half of
+# the ABI-FFI standard). Idempotent and fail-soft: it never aborts the caller.
+#
+# Egress note: Zig is NOT distributed via GitHub releases, so it is fetched from
+# ziglang.org. Inside a Claude Code session, outbound HTTPS goes through the
+# policy-enforcing agent proxy; github.com is allowlisted by default but
+# ziglang.org must be added explicitly, or this download returns 403. We use the
+# system CA store the proxy already populated — never pass --insecure.
+set -eu
+
+ZIG_VERSION="${ZIG_VERSION:-0.14.0}"
+PREFIX="${ZIG_PREFIX:-/usr/local}"
+
+# Already at the pinned version? Done.
+if command -v zig >/dev/null 2>&1 && [ "$(zig version 2>/dev/null)" = "$ZIG_VERSION" ]; then
+  echo "install-zig: zig $ZIG_VERSION already installed"
+  exit 0
+fi
+
+# Map host arch/OS to Zig's release naming.
+case "$(uname -m)" in
+  x86_64|amd64)   zarch="x86_64" ;;
+  aarch64|arm64)  zarch="aarch64" ;;
+  *) echo "install-zig: unsupported arch $(uname -m); install Zig $ZIG_VERSION manually" >&2; exit 0 ;;
+esac
+case "$(uname -s)" in
+  Linux)   zos="linux" ;;
+  Darwin)  zos="macos" ;;
+  *) echo "install-zig: unsupported OS $(uname -s); install Zig $ZIG_VERSION manually" >&2; exit 0 ;;
+esac
+
+tarball="zig-${zos}-${zarch}-${ZIG_VERSION}.tar.xz"
+url="https://ziglang.org/download/${ZIG_VERSION}/${tarball}"
+dest="${PREFIX}/lib/zig-${ZIG_VERSION}"
+
+tmp="$(mktemp -d)"
+trap 'rm -rf "$tmp"' EXIT
+
+echo "install-zig: fetching $url"
+if ! curl -fsSL --retry 2 -o "$tmp/$tarball" "$url"; then
+  echo "install-zig: download failed (HTTP error or blocked host)." >&2
+  echo "install-zig: if this is a Claude Code session, add 'ziglang.org' to the" >&2
+  echo "             egress allowlist — github.com is allowed but ziglang.org is not." >&2
+  exit 0   # fail-soft: a missing Zig must not block setup or session start
+fi
+
+mkdir -p "$dest" "${PREFIX}/bin"
+tar -xJf "$tmp/$tarball" -C "$dest" --strip-components=1
+ln -sf "$dest/zig" "${PREFIX}/bin/zig"
+
+if command -v zig >/dev/null 2>&1 && [ "$(zig version 2>/dev/null)" = "$ZIG_VERSION" ]; then
+  echo "install-zig: installed zig $(zig version)"
+else
+  echo "install-zig: installed to ${PREFIX}/bin/zig — ensure ${PREFIX}/bin is on PATH" >&2
+fi

setup.sh

@@ -194,6 +194,15 @@ main() {
     printf "%sStep 1: Install task runner%s\n" "$BOLD" "$RESET"
     install_just || { fail "Cannot proceed without just"; exit 1; }
     printf "\n"
+    # Step 1b: Install the pinned Zig toolchain (the Zig FFI bridge half of the
+    # ABI-FFI standard). Best-effort — see scripts/install-zig.sh.
+    printf "%sStep 1b: Install Zig toolchain%s\n" "$BOLD" "$RESET"
+    if [ -x ./scripts/install-zig.sh ]; then
+        ./scripts/install-zig.sh || warn "Zig install skipped (see scripts/install-zig.sh)"
+    else
+        warn "scripts/install-zig.sh not found — skipping Zig install"
+    fi
+    printf "\n"
 
     # Step 2: Check if we're in the repo directory
     if [ ! -f "Justfile" ] && [ ! -f "justfile" ]; then