feat(abi): ABI↔FFI cleave gate — no phantom %foreign can return (gossamer#82)

CHANGELOG.md

@@ -22,6 +22,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - **`bindings/rescript/` retired** (`Gossamer.res`, `rescript.json`, package manifest) — superseded by the AffineScript binding above.
 
 ### Added
+- **`scripts/check-abi-ffi-cleave.sh` — the ABI↔FFI cleave gate (gossamer#82)**: `idris2 --typecheck` cannot see whether a `%foreign "C:sym, libgossamer"` resolves to a real Zig export (that linkage is only checked at link time), which is how the "phantom template" (8 declared symbols with no Zig definition) went unnoticed. This fast, toolchain-free gate — wired into the ABI Typecheck Gate ahead of the Idris2 build, and into `just abi-check` — **hard-fails on any phantom `%foreign`** and **reports coverage** of the real C surface (currently **29 / 130** `gossamer_*` exports declared; the 101 uncovered are the tracked expansion work in gossamer#82). Shellcheck-clean; proven to fail on an injected phantom and pass on the current tree. Together with the honest `Foreign.idr` (gossamer#95), the phantom-template class is now closed and cannot silently return.
 - **`gossamer-groove.ipkg` — the Groove protocol proofs in their own package (gossamer#95)**: 4 modules — `Groove` (capability types, manifests, handshake state machine), `GrooveLinearity` (groove-handle linearity over the shell's generic `LinearHandle`), `CapabilityAuthenticity` (no phantom capabilities; attenuation soundness), and `GrooveTermination` (handshake terminates in ≤4 steps, no privilege escalation). Declares `depends = base, gossamer-abi`, so the layering is enforced by the build: Groove depends on the shell, never the reverse.
 - **`scripts/check-abi-decoupling.sh` — structural guard for the shell/groove split (gossamer#95)**: a fast, toolchain-free check (wired into the ABI Typecheck Gate ahead of the ~15-min Idris2 build, and into `just abi-check`) that fails if any `Gossamer/ABI/*.idr` is a materialised copy instead of a symlink, or if a shell module re-imports a groove module, or if the two `.ipkg` manifests stop partitioning the modules. Shellcheck-clean; proven to fail on both regressions and pass on the fixed tree.
 - **Android — `gossamer-android-services` companion: four shim base classes + real JNI (Phase 5, #71)**: Grows the Android target from "a WebView in an Activity" into a first-class mobile shell hosting the non-UI components, on the critical path for neurophone#97 (migrating a banned-Kotlin Android app onto gossamer). Owner-signed-off subclass model (issue #71).

Justfile

@@ -47,6 +47,7 @@ check-example name:
 # groove-agnostic shell package and the groove package that depends on it.
 abi-check:
     ./scripts/check-abi-decoupling.sh
+    ./scripts/check-abi-ffi-cleave.sh
     idris2 --typecheck gossamer-abi.ipkg
     idris2 --install   gossamer-abi.ipkg
     idris2 --typecheck gossamer-groove.ipkg

PROOF-NEEDS.md

@@ -16,6 +16,7 @@
 - `src/interface/abi/WindowStateMachine.idr` — Window state machine correctness (GS1) ✅ NEW 2026-04-11
 - `src/interface/abi/IPCDispatch.idr` — IPC handler type safety, 25 handlers (GS2) ✅ NEW 2026-04-11
 - **All 15 ABI modules above build green and pass `idris2 0.8.0 --typecheck` cleanly**, now split across two de-conflated packages (`gossamer#95`): the groove-agnostic **shell** `gossamer-abi.ipkg` (11 modules) and the **groove** `gossamer-groove.ipkg` (4: `Groove`, `GrooveLinearity`, `CapabilityAuthenticity`, `GrooveTermination`), which *depends on* the shell. The dependency points one way only — no shell module imports a groove module. The canonical sources live in `src/interface/abi/`; `src/interface/Gossamer/ABI/<M>.idr` are symlinks (a single source of truth, no drift). `scripts/check-abi-decoupling.sh` gates both invariants in CI. Prior to `gossamer#22` / `#36` / `#40` / `#41`, several modules were excluded from the ipkg and had never been built — their PROOF-NEEDS ✅ markers reflected an unverified posture; build is now the oracle.
+- **ABI ↔ FFI cleave (`gossamer#82`)**: `idris2 --typecheck` proves the ABI internally sound but does **not** check that a `%foreign "C:sym, libgossamer"` resolves to a real Zig export (that linkage is only exercised at link time). The honest `Foreign.idr` (`gossamer#95`) removed all 8 phantom declarations, and `scripts/check-abi-ffi-cleave.sh` now gates it in CI: **every ABI `%foreign` resolves to a real `export fn` (phantom = 0)**. Coverage of the real C surface is **29 / 130** `gossamer_*` exports declared; the remaining **101 uncovered** exports are the open expansion work tracked in `gossamer#82` (declare-or-codegen the full cleave). The gate reports coverage but only *fails* on phantom, so new Zig exports don't break CI before their ABI declaration lands.
 - **One class-J axiom**: `Gossamer.ABI.PanelIsolation.stringNotEqCommut` — sanctioned principled assumption over the Idris2 backend primitive `prim__eq_String` (content-symmetry on every supported backend; cannot be derived inside Idris2). `%unsafe`-annotated, `believe_me ()`-bodied, documented at the use site. Same trust posture as boj-server's `Boj.SafetyLemmas.charEqSym` and four sibling axioms over String / Char primitives. See "Class-J axioms (trusted base)" section below.
 - No other `believe_me`, `sorry`, `postulate`, or `assert_total` in the ABI layer.
 - Zig FFI layer in `src/interface/ffi/`

scripts/check-abi-ffi-cleave.sh

@@ -0,0 +1,91 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# check-abi-ffi-cleave.sh — the cleave-consistency gate for gossamer#82.
+#
+# `idris2 --typecheck` proves the ABI is internally sound, but it does NOT check
+# that a `%foreign "C:sym, libgossamer"` declaration resolves to a real Zig
+# export — that linkage is only exercised at link time. So a green typecheck can
+# still describe a PHANTOM surface (gossamer#82's CRITICAL finding: the ABI once
+# declared 8 symbols that no Zig function defined).
+#
+# This gate closes that hole with a pure-text check (no toolchain needed):
+#
+#   HARD FAIL  — any %foreign "C:sym, libgossamer" in src/interface/abi/*.idr
+#                with no matching `export fn sym` in src/interface/ffi/src/*.zig.
+#                (The ABI must never lie about the FFI.)
+#   REPORT     — coverage: how many of the real gossamer_* C exports the ABI
+#                actually declares. Coverage < 100% is the open expansion work
+#                (declare/codegen the rest); it is reported, not failed, so new
+#                Zig exports don't break CI before their ABI declaration lands.
+set -euo pipefail
+
+cd "$(git rev-parse --show-toplevel)"
+
+ABI_DIR="src/interface/abi"
+FFI_DIR="src/interface/ffi/src"
+
+abi_syms="$(mktemp)"
+zig_syms="$(mktemp)"
+trap 'rm -f "$abi_syms" "$zig_syms"' EXIT
+
+# ABI-declared C:libgossamer symbols (tolerate optional space after the comma).
+grep -rhoE '%foreign "C:gossamer_[a-z_0-9]+, ?libgossamer"' "$ABI_DIR"/*.idr 2>/dev/null \
+  | sed -E 's/.*C:(gossamer_[a-z_0-9]+),.*/\1/' | sort -u > "$abi_syms" || true
+
+# Real Zig C exports (both `export fn` and `pub export fn`).
+grep -rhoE '(pub )?export fn gossamer_[a-z_0-9]+' "$FFI_DIR"/*.zig 2>/dev/null \
+  | sed -E 's/.*export fn (gossamer_[a-z_0-9]+).*/\1/' | sort -u > "$zig_syms"
+
+n_abi=$(wc -l < "$abi_syms")
+n_zig=$(wc -l < "$zig_syms")
+phantom=$(comm -23 "$abi_syms" "$zig_syms")
+covered=$(comm -12 "$abi_syms" "$zig_syms" | wc -l)
+uncovered=$(comm -13 "$abi_syms" "$zig_syms")
+n_uncovered=$(printf '%s\n' "$uncovered" | grep -c . || true)
+
+fail=0
+
+echo "== ABI <-> FFI cleave (gossamer#82) =="
+echo "  ABI %foreign C:libgossamer declarations: $n_abi"
+echo "  Zig gossamer_* C exports:                $n_zig"
+echo "  covered (declared AND exported):         $covered"
+
+# --- HARD FAIL: phantom declarations ---
+if [ -n "$phantom" ]; then
+  fail=1
+  echo "::error::ABI declares %foreign symbols with NO Zig export (phantom surface — gossamer#82):"
+  while IFS= read -r s; do
+    [ -z "$s" ] && continue
+    printf '::error::  phantom: %s (declared in %s, no export fn %s in %s)\n' \
+      "$s" "$ABI_DIR" "$s" "$FFI_DIR" >&2
+  done <<< "$phantom"
+fi
+
+# --- REPORT: coverage of the real surface ---
+pct=$(( n_zig > 0 ? covered * 100 / n_zig : 100 ))
+echo "  coverage of real FFI surface:            ${covered}/${n_zig} (${pct}%)"
+if [ "$n_uncovered" -gt 0 ]; then
+  echo "  uncovered Zig exports (no ABI %foreign):  $n_uncovered  [expansion work — gossamer#82]"
+fi
+
+# --- GitHub step summary (when running in Actions) ---
+if [ -n "${GITHUB_STEP_SUMMARY:-}" ]; then
+  {
+    echo "## ABI ↔ FFI cleave (gossamer#82)"
+    echo ""
+    echo "| Metric | Value |"
+    echo "|--------|-------|"
+    echo "| Phantom \`%foreign\` (must be 0) | $(printf '%s' "$phantom" | grep -c . || true) |"
+    echo "| ABI coverage of real FFI surface | ${covered}/${n_zig} (${pct}%) |"
+    echo "| Uncovered Zig exports (expansion work) | $n_uncovered |"
+  } >> "$GITHUB_STEP_SUMMARY"
+fi
+
+echo
+if [ "$fail" -ne 0 ]; then
+  echo "ABI/FFI cleave gate: FAILED — the ABI declares symbols the FFI does not export." >&2
+  exit 1
+fi
+echo "ABI/FFI cleave gate: PASSED — every ABI %foreign resolves to a real Zig export."