From b504f37f98a83ec9c8b094e84e693b440168daae Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 3 Jul 2026 01:35:33 +0000 Subject: [PATCH] =?UTF-8?q?feat(abi):=20add=20ABI=E2=86=94FFI=20cleave=20g?= =?UTF-8?q?ate=20=E2=80=94=20no=20phantom=20%foreign=20can=20return=20(gos?= =?UTF-8?q?samer#82)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `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. That blind spot is how gossamer#82's "phantom template" (8 declared symbols with no Zig definition) went unnoticed behind a green typecheck. #95's honest Foreign.idr fixed the declarations; this gate makes the fix permanent. scripts/check-abi-ffi-cleave.sh (toolchain-free, shellcheck-clean): * HARD FAIL on any ABI %foreign with no matching `export fn` in src/interface/ffi/src/*.zig (the ABI must never lie about the FFI). * REPORT coverage of the real surface — 29/130 gossamer_* exports declared; the 101 uncovered are the expansion work still tracked in #82. Coverage is reported, not failed, so a new Zig export doesn't break CI before its ABI declaration lands. Wired into the abi-structure job (ahead of the ~15-min Idris2 build) and `just abi-check`. Verified: passes on the current tree (0 phantom), fails on an injected phantom, idris2 flow still green (both packages typecheck, 147/147 tests). Closes the phantom-template half of #82's CRITICAL item. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_013Zg1kEsjSRpcf1wFBZyeNj --- .github/workflows/abi-typecheck.yml | 16 +++-- CHANGELOG.md | 1 + Justfile | 1 + PROOF-NEEDS.md | 1 + scripts/check-abi-ffi-cleave.sh | 91 +++++++++++++++++++++++++++++ 5 files changed, 105 insertions(+), 5 deletions(-) create mode 100755 scripts/check-abi-ffi-cleave.sh diff --git a/.github/workflows/abi-typecheck.yml b/.github/workflows/abi-typecheck.yml index 4638c3a..33b483f 100644 --- a/.github/workflows/abi-typecheck.yml +++ b/.github/workflows/abi-typecheck.yml @@ -18,6 +18,7 @@ on: - 'gossamer-groove.ipkg' - 'gossamer-abi-tests.ipkg' - 'scripts/check-abi-decoupling.sh' + - 'scripts/check-abi-ffi-cleave.sh' - '.github/workflows/abi-typecheck.yml' push: branches: [main, master] @@ -28,6 +29,7 @@ on: - 'gossamer-groove.ipkg' - 'gossamer-abi-tests.ipkg' - 'scripts/check-abi-decoupling.sh' + - 'scripts/check-abi-ffi-cleave.sh' - '.github/workflows/abi-typecheck.yml' permissions: @@ -38,17 +40,21 @@ concurrency: cancel-in-progress: true jobs: - # Fast, toolchain-free structural gate (gossamer#95): fails in seconds if the - # ABI namespace symlinks re-materialise into copies, or if a shell module - # re-imports a groove module. Runs before the ~15-min Idris2 build. + # Fast, toolchain-free structural gates. Run in seconds before the ~15-min + # Idris2 build: + # * decoupling guard (gossamer#95) — symlinks intact, no shell->groove import + # * cleave gate (gossamer#82) — every ABI %foreign resolves to a real + # Zig export (typecheck can't see %foreign linkage) abi-structure: - name: ABI decoupling guard (symlinks + groove split) + name: ABI structure gates (decoupling + cleave) runs-on: ubuntu-latest steps: - name: Checkout repository uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 - - name: Check ABI decoupling + - name: Check ABI decoupling (symlinks + groove split) run: ./scripts/check-abi-decoupling.sh + - name: Check ABI/FFI cleave (no phantom %foreign) + run: ./scripts/check-abi-ffi-cleave.sh abi-typecheck: name: idris2 typecheck + test (shell + groove) diff --git a/CHANGELOG.md b/CHANGELOG.md index f57ae2e..8192957 100644 --- a/CHANGELOG.md +++ b/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). diff --git a/Justfile b/Justfile index 51cdbc1..3d4c02d 100644 --- a/Justfile +++ b/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 diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index ad8f2b9..10927d1 100644 --- a/PROOF-NEEDS.md +++ b/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/.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/` diff --git a/scripts/check-abi-ffi-cleave.sh b/scripts/check-abi-ffi-cleave.sh new file mode 100755 index 0000000..d2bf470 --- /dev/null +++ b/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) +# +# 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."