hyperpolymath · hyperpolymath · Jul 3, 2026 · Jul 3, 2026 · Jul 3, 2026 · Jul 3, 2026
@@ -23,6 +23,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Added
 - **`Gossamer.ABI.GrooveResidue` — soft-groove disconnect privacy proof (gossamer#82)**: a new module in the groove package that models `gossamer_groove_disconnect_typed` and proves the `SoftGroove` privacy guarantee `ResourceCleanup`'s plain `disconnect` did not cover: disconnecting a soft groove **erases the peer identity** (`softWipeZeroResidue`: residue = 0), clears the whole slot, retains the peer for a *hard* groove (`hardDisconnectRetainsPeer` — proving the two modes genuinely differ), and is idempotent. Closes the `RC-7`/`RC-8` gap. Zero `believe_me`; `idris2 0.8.0 --typecheck` green.
+- **`Gossamer.ABI.ForeignGen` + `scripts/gen-abi-foreign.sh` — generated ABI mirror closes the cleave (gossamer#82)**: the Idris ABI now declares **130 / 130 (100%)** of the real `gossamer_*` C exports, up from 29. Rather than hand-declare 101 more (drift-prone — exactly what #82 warns against), `gen-abi-foreign.sh` **generates** the complete raw `%foreign` mirror from the Zig `export fn` signatures, making the **Zig FFI the single source of truth**. `check-abi-ffi-cleave.sh` now runs the generator in `--check` mode too: change the FFI without `just abi-gen` and CI fails — so the ABI can no longer drift from *or* under-describe the FFI. The generated signatures were cross-checked against the hand-curated `Gossamer.ABI.Foreign` (identical on the 29 overlapping symbols) and adversarially verified against the Zig per-file. Typechecks green under idris2 0.8.0; 147/147 ABI tests still pass.
 - **`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.

@@ -52,6 +52,13 @@ abi-check:
     idris2 --install   gossamer-abi.ipkg
     idris2 --typecheck gossamer-groove.ipkg
 
+# Regenerate the raw %foreign ABI mirror (Gossamer.ABI.ForeignGen) from the Zig
+# `export fn gossamer_*` surface. The Zig FFI is the single source of truth for
+# the ABI (gossamer#82); run this after adding/changing an FFI export, then
+# commit — CI (`check-abi-ffi-cleave.sh`) fails if the mirror is stale.
+abi-gen:
+    ./scripts/gen-abi-foreign.sh
+
 # Build the Gossamer CLI (links libgossamer)
 build-cli: build-ffi
     cd cli && zig build

@@ -16,7 +16,10 @@
 - `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.
+- **ABI ↔ FFI cleave (`gossamer#82`) — closed.** `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). This is now closed at source:
+  - **No phantom, no drift.** `Gossamer.ABI.ForeignGen` is a **generated** raw `%foreign` mirror of the C ABI — `scripts/gen-abi-foreign.sh` emits one declaration per `export fn gossamer_*` in `src/interface/ffi/src/*.zig`, making the **Zig FFI the single source of truth**. Coverage is **130 / 130 (100%)**.
+  - **Enforced in CI.** `scripts/check-abi-ffi-cleave.sh` hard-fails on any phantom `%foreign` *and* runs the generator in `--check` mode: if a Zig export is added/changed/removed and `ForeignGen.idr` isn't regenerated (`just abi-gen`), CI fails. The ABI therefore cannot drift from — or lie about — the FFI.
+  - Curated safe wrappers over the core subset (with `MainThreadProof` etc.) remain hand-written in `Gossamer.ABI.Foreign`; `ForeignGen` is the complete raw layer beneath them.
 - **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/`

@@ -31,6 +31,7 @@ depends = base
 modules = Gossamer.ABI.Types
         , Gossamer.ABI.Layout
         , Gossamer.ABI.Foreign
+        , Gossamer.ABI.ForeignGen
         , Gossamer.ABI.IPCDispatch
         , Gossamer.ABI.HandleLinearity
         , Gossamer.ABI.WindowStateMachine

@@ -68,7 +68,12 @@ done < <(git ls-files -s -- "$NS_DIR"/*.idr | sed -E 's/^([0-9]+) [0-9a-f]+ [0-9
 # Check 2: no shell module imports a Groove-layer module.
 # ---------------------------------------------------------------------------
 echo "== Check 2: shell modules are groove-agnostic (no conflation) =="
-groove_import_re='^import[[:space:]]+Gossamer\.ABI\.(Groove|GrooveTermination|GrooveLinearity|CapabilityAuthenticity)([[:space:]]|$)'
+# Derive the import-detection alternation from the single GROOVE_MODULES source
+# of truth above, so a newly-added groove module cannot be silently missed here
+# (as GrooveResidue was when the alternation was hand-maintained). The array and
+# this check can never drift apart now.
+groove_alt=$(IFS='|'; printf '%s' "${GROOVE_MODULES[*]}")
+groove_import_re="^import[[:space:]]+Gossamer\.ABI\.(${groove_alt})([[:space:]]|\$)"
 for f in "$ABI_DIR"/*.idr; do
   base=$(basename "$f" .idr)
   is_groove_module "$base" && continue

@@ -70,6 +70,14 @@ if [ "$n_uncovered" -gt 0 ]; then
   echo "  uncovered Zig exports (no ABI %foreign):  $n_uncovered  [expansion work — gossamer#82]"
 fi
 
+# --- ENFORCE: the generated ABI mirror (ForeignGen.idr) is fresh vs the Zig FFI.
+# This turns coverage from "reported" into "enforced": add/change/remove a Zig
+# `export fn gossamer_*` and the committed ForeignGen.idr goes stale, failing CI
+# until `just abi-gen` regenerates it — so the ABI cannot drift from the FFI.
+if ! scripts/gen-abi-foreign.sh --check; then
+  fail=1
+fi
+
 # --- GitHub step summary (when running in Actions) ---
 if [ -n "${GITHUB_STEP_SUMMARY:-}" ]; then
   {

@@ -0,0 +1,129 @@
+#!/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>
+#
+# gen-abi-foreign.sh — generate the complete raw %foreign mirror of the
+# libgossamer C ABI (Gossamer.ABI.ForeignGen) from the Zig `export fn`
+# declarations, making the Zig FFI the SINGLE SOURCE OF TRUTH for the ABI
+# (gossamer#82). Bash + AWK (Python is estate-banned).
+#
+# Usage:
+#   scripts/gen-abi-foreign.sh            # write src/interface/abi/ForeignGen.idr
+#   scripts/gen-abi-foreign.sh --check    # exit 1 if the committed file is stale
+#
+# Type mapping (position-aware) mirrors the hand-curated Gossamer.ABI.Foreign,
+# which is proven to typecheck: integers -> Bits of same width, C string ->
+# String (parameter) / Bits64 (char* return), pointers & function pointers ->
+# Bits64, Result/c_int -> Bits32, void -> (), every call wrapped in PrimIO.
+set -euo pipefail
+
+cd "$(git rev-parse --show-toplevel)"
+OUT="src/interface/abi/ForeignGen.idr"
+
+read -r -d '' HEADER <<'EOF' || true
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| GENERATED FILE — DO NOT EDIT BY HAND.
+||| Regenerate with `just abi-gen` (scripts/gen-abi-foreign.sh); CI fails if this
+||| file is stale (scripts/check-abi-ffi-cleave.sh runs it with --check).
+|||
+||| Complete raw %foreign mirror of the libgossamer C ABI: EVERY `export fn
+||| gossamer_*` in src/interface/ffi/src/*.zig has a matching declaration here,
+||| so the Idris ABI describes the *real, whole* FFI surface (gossamer#82) and is
+||| generated FROM it — it cannot drift or go phantom. Curated safe wrappers over
+||| the core subset live in `Gossamer.ABI.Foreign`; these are the raw bindings.
+
+module Gossamer.ABI.ForeignGen
+
+%default total
+EOF
+
+# AWK parses every `export fn gossamer_*` (accumulating multi-line signatures up
+# to the body `{`) and prints one "symbol<TAB>idris-signature" line per export.
+gen_body() {
+  awk '
+    function strip(s){ sub(/\/\/.*/,"",s); gsub(/^[ \t]+|[ \t]+$/,"",s); return s }
+    function map(z, isret,    nz, bare){
+      z=strip(z); sub(/,$/,"",z); gsub(/^[ \t]+|[ \t]+$/,"",z)
+      if (z=="") return "()"
+      nz=z; gsub(/ /,"",nz)
+      if (index(nz,"fn(")>0) return "Bits64"
+      if (z=="[*:0]const u8"||z=="?[*:0]const u8"||z=="[*c]const u8"||z=="?[*c]const u8")
+        return isret ? "Bits64" : "String"
+      if (z ~ /^\??\*/ || z ~ /^\??\[\*/) return "Bits64"
+      if (z=="void") return "()"
+      if (z=="bool"||z=="u8"||z=="i8") return "Bits8"
+      if (z=="u16"||z=="i16") return "Bits16"
+      if (z=="u32"||z=="i32"||z=="c_int"||z=="c_uint") return "Bits32"
+      if (z=="u64"||z=="i64"||z=="usize"||z=="isize"||z=="c_long"||z=="c_ulong") return "Bits64"
+      if (z=="f32"||z=="f64") return "Double"
+      if (z=="Result" || z ~ /\.Result$/) return "Bits32"
+      bare=z; sub(/^\?/,"",bare)
+      if (bare ~ /Fn$/) return "Bits64"
+      printf("gen-abi-foreign: unmapped Zig type %s\n", z) > "/dev/stderr"; EXIT=1; return "Bits64"
+    }
+    # split s on TOP-LEVEL commas (paren/bracket-depth aware, so a callback
+    # param like `?*const fn(a: T, b: U) callconv(.c) void` stays one element).
+    function split_top(s, arr,    i, c, depth, cur, n){
+      depth=0; cur=""; n=0
+      for (i=1;i<=length(s);i++){
+        c=substr(s,i,1)
+        if (c=="("||c=="["||c=="{") depth++
+        else if (c==")"||c=="]"||c=="}") depth--
+        if (c=="," && depth==0){ arr[++n]=cur; cur="" } else cur=cur c
+      }
+      if (cur ~ /[^ \t]/) arr[++n]=cur
+      return n
+    }
+    function emit(buf,    name, popen, pclose, i, c, depth, params, ret, n, arr, sig, t){
+      if (match(buf, /gossamer_[A-Za-z0-9_]+/)==0) return
+      name=substr(buf, RSTART, RLENGTH)
+      popen=index(buf, "(")                       # first ( = param-list open
+      depth=0; pclose=0
+      for (i=popen; i<=length(buf); i++){         # scan for its MATCHING close paren
+        c=substr(buf,i,1)
+        if (c=="(") depth++
+        else if (c==")"){ depth--; if (depth==0){ pclose=i; break } }
+      }
+      params=substr(buf, popen+1, pclose-popen-1)
+      ret=substr(buf, pclose+1)                   # after the param list
+      sub(/callconv\([^)]*\)/, "", ret)           # drop callconv(...)
+      ret=substr(ret, 1, index(ret,"{")>0 ? index(ret,"{")-1 : length(ret))
+      ret=strip(ret); if (ret=="") ret="void"
+      sig=""
+      n=split_top(params, arr)
+      for (i=1;i<=n;i++){
+        t=arr[i]; sub(/^[^:]*:/, "", t)           # drop "name:" -> TYPE
+        if (strip(t)!="") sig = sig map(t,0) " -> "
+      }
+      print name "\t" sig "PrimIO " map(ret,1)
+    }
+    /export fn gossamer_/ { collecting=1; buf="" }
+    collecting {
+      buf = buf " " $0
+      if (index($0,"{")>0){ emit(buf); collecting=0 }
+    }
+    END { if (EXIT) exit 1 }
+  ' src/interface/ffi/src/*.zig
+}
+
+render() {
+  printf '%s\n' "$HEADER"
+  # sort by symbol (unique), format each as a 3-line %foreign block
+  gen_body | sort -u -t$'\t' -k1,1 | while IFS=$'\t' read -r name sig; do
+    [ -z "$name" ] && continue
+    printf '\nexport\n%%foreign "C:%s, libgossamer"\nprim__%s : %s\n' "$name" "$name" "$sig"
+  done
+}
+
+if [ "${1:-}" = "--check" ] || [ "${1:-}" = "--check-generated" ]; then
+  if ! diff -q <(render) "$OUT" >/dev/null 2>&1; then
+    echo "::error::ForeignGen.idr is stale — run \`just abi-gen\` and commit (the Zig FFI surface changed but the generated ABI mirror did not)." >&2
+    exit 1
+  fi
+  echo "ForeignGen.idr is up to date with the Zig FFI surface."
+else
+  render > "$OUT"
+  echo "wrote $OUT ($(grep -c '%foreign' "$OUT") %foreign declarations)"
+fi
@@ -0,0 +1 @@
+../../abi/ForeignGen.idr