From 953e2dc15677c44275b6882cbf7b6dc75afe93e0 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 3 Jul 2026 02:11:02 +0000 Subject: [PATCH 1/3] fix(ci): derive the groove-import check from GROOVE_MODULES (close DRY gap) check-abi-decoupling.sh Check 2 hand-maintained a second alternation of the groove module names, separate from the GROOVE_MODULES array. They already drifted: GrooveResidue (added in #99) was in the array but not the import regex, so a shell module importing Gossamer.ABI.GrooveResidue would have slipped the conflation check. Derive the regex from the single GROOVE_MODULES source of truth so the two can never diverge again. Verified: shellcheck clean; passes on current tree; a shell module importing GrooveResidue is now correctly flagged (was the gap). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_013Zg1kEsjSRpcf1wFBZyeNj --- scripts/check-abi-decoupling.sh | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/scripts/check-abi-decoupling.sh b/scripts/check-abi-decoupling.sh index 4116783..a456fae 100755 --- a/scripts/check-abi-decoupling.sh +++ b/scripts/check-abi-decoupling.sh @@ -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 From 9f76db05c33fcf3cbe77f22d6dfc0136290c6333 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 3 Jul 2026 02:24:02 +0000 Subject: [PATCH 2/3] =?UTF-8?q?feat(abi):=20codegen=20the=20full=20FFI=20c?= =?UTF-8?q?leave=20=E2=80=94=20ABI=20mirrors=20130/130=20Zig=20exports=20(?= =?UTF-8?q?gossamer#82)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes the coverage half of #82's CRITICAL item. The Idris ABI declared only 29 of the 130 real gossamer_* C exports (22%); the other 101 were an honest coverage gap. Rather than hand-declare them (drift-prone — exactly what #82 warns against), generate the complete raw %foreign mirror from the Zig FFI so the Zig `export fn` surface is the SINGLE SOURCE OF TRUTH for the ABI. - scripts/gen-abi-foreign.py — parses every `export fn gossamer_*` in src/interface/ffi/src/*.zig (balanced-paren aware, handles callbacks/multiline) and emits Gossamer.ABI.ForeignGen with one %foreign per symbol. Position-aware type map mirrors the hand-curated Foreign.idr (proven to typecheck): ints -> Bits of same width, C string -> String (param) / Bits64 (char* return), pointers & fn-pointers -> Bits64, Result/c_int -> Bits32, void -> (), PrimIO. - src/interface/abi/ForeignGen.idr (generated) + namespace symlink; wired into gossamer-abi.ipkg. Coverage: 130/130 (100%). - check-abi-ffi-cleave.sh now also runs the generator in --check mode: change the FFI without `just abi-gen` and CI fails (stale mirror) — so the ABI can no longer drift from OR under-describe the FFI. `just abi-gen` regenerates. Verified with idris2 0.8.0: ForeignGen typechecks green; the generated signatures are byte-identical to the hand-written Foreign.idr on all 29 overlapping symbols; tricky cases (string return vs param, nullable, callconv, opaque ptr, callbacks) spot-checked; guards + both packages green; 147/147 ABI tests pass. Negative- tested: adding a Zig export makes the gate fail until regenerated. Curated safe wrappers (MainThreadProof etc.) stay hand-written in Gossamer.ABI.Foreign; ForeignGen is the complete raw layer beneath them. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_013Zg1kEsjSRpcf1wFBZyeNj --- .github/workflows/abi-typecheck.yml | 2 + CHANGELOG.md | 1 + Justfile | 7 + PROOF-NEEDS.md | 5 +- gossamer-abi.ipkg | 1 + scripts/check-abi-ffi-cleave.sh | 12 + scripts/gen-abi-foreign.py | 181 ++++++++ src/interface/Gossamer/ABI/ForeignGen.idr | 1 + src/interface/abi/ForeignGen.idr | 536 ++++++++++++++++++++++ 9 files changed, 745 insertions(+), 1 deletion(-) create mode 100644 scripts/gen-abi-foreign.py create mode 120000 src/interface/Gossamer/ABI/ForeignGen.idr create mode 100644 src/interface/abi/ForeignGen.idr diff --git a/.github/workflows/abi-typecheck.yml b/.github/workflows/abi-typecheck.yml index 33b483f..40996c4 100644 --- a/.github/workflows/abi-typecheck.yml +++ b/.github/workflows/abi-typecheck.yml @@ -19,6 +19,7 @@ on: - 'gossamer-abi-tests.ipkg' - 'scripts/check-abi-decoupling.sh' - 'scripts/check-abi-ffi-cleave.sh' + - 'scripts/gen-abi-foreign.py' - '.github/workflows/abi-typecheck.yml' push: branches: [main, master] @@ -30,6 +31,7 @@ on: - 'gossamer-abi-tests.ipkg' - 'scripts/check-abi-decoupling.sh' - 'scripts/check-abi-ffi-cleave.sh' + - 'scripts/gen-abi-foreign.py' - '.github/workflows/abi-typecheck.yml' permissions: diff --git a/CHANGELOG.md b/CHANGELOG.md index a864458..13b6315 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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.py` — 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.py` **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. diff --git a/Justfile b/Justfile index 3d4c02d..bf9f362 100644 --- a/Justfile +++ b/Justfile @@ -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: + python3 scripts/gen-abi-foreign.py + # Build the Gossamer CLI (links libgossamer) build-cli: build-ffi cd cli && zig build diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 8044af5..4528941 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -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/.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.py` 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/` diff --git a/gossamer-abi.ipkg b/gossamer-abi.ipkg index 688cea6..974e789 100644 --- a/gossamer-abi.ipkg +++ b/gossamer-abi.ipkg @@ -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 diff --git a/scripts/check-abi-ffi-cleave.sh b/scripts/check-abi-ffi-cleave.sh index d2bf470..d08caed 100755 --- a/scripts/check-abi-ffi-cleave.sh +++ b/scripts/check-abi-ffi-cleave.sh @@ -70,6 +70,18 @@ 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 command -v python3 >/dev/null 2>&1; then + if ! python3 scripts/gen-abi-foreign.py --check; then + fail=1 + fi +else + echo " (python3 unavailable — skipping ForeignGen freshness check)" +fi + # --- GitHub step summary (when running in Actions) --- if [ -n "${GITHUB_STEP_SUMMARY:-}" ]; then { diff --git a/scripts/gen-abi-foreign.py b/scripts/gen-abi-foreign.py new file mode 100644 index 0000000..8af2006 --- /dev/null +++ b/scripts/gen-abi-foreign.py @@ -0,0 +1,181 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# gen-abi-foreign.py — generate the complete raw %foreign mirror of the +# libgossamer C ABI (Gossamer.ABI.ForeignGen) from the Zig `export fn` +# declarations. This makes the Zig FFI the SINGLE SOURCE OF TRUTH for the ABI +# surface (gossamer#82): the Idris ABI can no longer drift from — or lie about — +# the real exports, because it is generated from them and checked fresh in CI. +# +# Usage: +# scripts/gen-abi-foreign.py # write src/interface/abi/ForeignGen.idr +# scripts/gen-abi-foreign.py --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 the same width, C strings -> +# String as a parameter / Bits64 (char* pointer) as a return, all pointers and +# function pointers -> Bits64, void -> (), every call wrapped in PrimIO. +import glob +import os +import re +import sys + +ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) +FFI_GLOB = os.path.join(ROOT, "src/interface/ffi/src/*.zig") +OUT = os.path.join(ROOT, "src/interface/abi/ForeignGen.idr") + +# Integer / scalar Zig types -> Idris Bits* (bit-accurate; signedness is a +# wrapper concern, and the curated Foreign.idr proves Bits* work over %foreign). +SCALAR = { + "void": "()", + "bool": "Bits8", + "u8": "Bits8", "i8": "Bits8", + "u16": "Bits16", "i16": "Bits16", + "u32": "Bits32", "i32": "Bits32", "c_int": "Bits32", "c_uint": "Bits32", + "u64": "Bits64", "i64": "Bits64", "usize": "Bits64", "isize": "Bits64", + "c_long": "Bits64", "c_ulong": "Bits64", + "f32": "Double", "f64": "Double", +} +CSTR = {"[*:0]const u8", "?[*:0]const u8", "[*c]const u8", "?[*c]const u8"} + + +def strip_comment(s: str) -> str: + return re.sub(r"//.*$", "", s).strip() + + +def map_type(z: str, is_return: bool) -> str: + z = strip_comment(z).rstrip(",").strip() + if not z: + return "()" + nospace = z.replace(" ", "") + # function pointer (callback) -> raw pointer value + if "fn(" in nospace: + return "Bits64" + # C strings: String as a parameter, char* pointer (Bits64) as a return + if z in CSTR: + return "Bits64" if is_return else "String" + # any other pointer / many-item pointer / slice / optional pointer -> Bits64 + if re.match(r"^\??\*", z) or re.match(r"^\??\[\*", z): + return "Bits64" + if z in SCALAR: + return SCALAR[z] + # Named enums backed by c_int (the Result enum, possibly module-qualified). + if z == "Result" or z.endswith(".Result"): + return "Bits32" + # Named function-pointer typedefs (Zig convention: `*Fn` / `?*Fn`) -> pointer. + bare = z[1:].strip() if z.startswith("?") else z + if bare.endswith("Fn"): + return "Bits64" + # Unknown type — fail loudly rather than emit a silent wrong binding. + raise SystemExit(f"gen-abi-foreign: unmapped Zig type {z!r} — extend SCALAR/rules") + + +def split_params(param_src: str): + """Split a Zig parameter list on top-level commas (paren-depth aware, so + function-pointer params like `?*const fn(...) callconv(.c) void` stay whole).""" + out, depth, cur = [], 0, "" + for ch in param_src: + if ch in "([{": + depth += 1 + elif ch in ")]}": + depth -= 1 + if ch == "," and depth == 0: + out.append(cur) + cur = "" + else: + cur += ch + if cur.strip(): + out.append(cur) + return [p for p in (x.strip() for x in out) if p] + + +def param_type(p: str) -> str: + # "name: TYPE" -> TYPE (a param has exactly one top-level colon) + m = re.match(r"^[A-Za-z_][A-Za-z0-9_]*\s*:\s*(.+)$", strip_comment(p), re.S) + return (m.group(1) if m else p).strip() + + +def parse_exports(text: str): + """Yield (symbol, [param_types], return_type) for each `export fn gossamer_*`, + scanning balanced parens so multi-line and callback signatures parse cleanly.""" + for m in re.finditer(r"(?:pub\s+)?export\s+fn\s+(gossamer_[A-Za-z0-9_]+)\s*\(", text): + name = m.group(1) + i = m.end() # just past the '(' + depth, start = 1, i + while i < len(text) and depth: + if text[i] == "(": + depth += 1 + elif text[i] == ")": + depth -= 1 + i += 1 + params_src = text[start:i - 1] + rest = text[i:] + rm = re.match(r"\s*(?:callconv\([^)]*\)\s*)?([^\{;]+?)\s*\{", rest, re.S) + ret = strip_comment(rm.group(1)) if rm else "void" + yield name, [param_type(p) for p in split_params(params_src)], ret + + +def idris_sig(params, ret) -> str: + pts = [map_type(p, False) for p in params] + r = map_type(ret, True) + arrow = "".join(f"{t} -> " for t in pts) + return f"{arrow}PrimIO {r}" + + +HEADER = """-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| GENERATED FILE — DO NOT EDIT BY HAND. +||| Regenerate with `just abi-gen` (scripts/gen-abi-foreign.py); CI fails if this +||| file is stale (scripts/check-abi-ffi-cleave.sh --check-generated). +||| +||| 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 +""" + + +def generate() -> str: + syms = {} + for path in sorted(glob.glob(FFI_GLOB)): + with open(path, encoding="utf-8") as f: + for name, params, ret in parse_exports(f.read()): + syms[name] = (params, ret) # last def wins; symbols are unique + lines = [HEADER] + for name in sorted(syms): + params, ret = syms[name] + lines.append(f'export\n%foreign "C:{name}, libgossamer"\n' + f'prim__{name} : {idris_sig(params, ret)}\n') + return "\n".join(lines) + "\n" if False else "\n".join(lines).rstrip() + "\n" + + +def main(): + content = generate() + if "--check" in sys.argv or "--check-generated" in sys.argv: + try: + with open(OUT, encoding="utf-8") as f: + current = f.read() + except FileNotFoundError: + current = None + if current != content: + print("::error::ForeignGen.idr is stale — run `just abi-gen` and commit " + "(the Zig FFI surface changed but the generated ABI mirror did not).", + file=sys.stderr) + sys.exit(1) + print("ForeignGen.idr is up to date with the Zig FFI surface.") + return + with open(OUT, "w", encoding="utf-8") as f: + f.write(content) + n = content.count("%foreign") + print(f"wrote {OUT} ({n} %foreign declarations)") + + +if __name__ == "__main__": + main() diff --git a/src/interface/Gossamer/ABI/ForeignGen.idr b/src/interface/Gossamer/ABI/ForeignGen.idr new file mode 120000 index 0000000..6a2aa6c --- /dev/null +++ b/src/interface/Gossamer/ABI/ForeignGen.idr @@ -0,0 +1 @@ +../../abi/ForeignGen.idr \ No newline at end of file diff --git a/src/interface/abi/ForeignGen.idr b/src/interface/abi/ForeignGen.idr new file mode 100644 index 0000000..8bc5fdd --- /dev/null +++ b/src/interface/abi/ForeignGen.idr @@ -0,0 +1,536 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| GENERATED FILE — DO NOT EDIT BY HAND. +||| Regenerate with `just abi-gen` (scripts/gen-abi-foreign.py); CI fails if this +||| file is stale (scripts/check-abi-ffi-cleave.sh --check-generated). +||| +||| 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 + +export +%foreign "C:gossamer_activity_get, libgossamer" +prim__gossamer_activity_get : Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_activity_set, libgossamer" +prim__gossamer_activity_set : Bits64 -> Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_android_register_boot_callback, libgossamer" +prim__gossamer_android_register_boot_callback : Bits64 -> PrimIO () + +export +%foreign "C:gossamer_android_register_intent_callback, libgossamer" +prim__gossamer_android_register_intent_callback : Bits64 -> PrimIO () + +export +%foreign "C:gossamer_android_register_service_callbacks, libgossamer" +prim__gossamer_android_register_service_callbacks : Bits64 -> Bits64 -> Bits64 -> Bits64 -> PrimIO () + +export +%foreign "C:gossamer_android_register_widget_callbacks, libgossamer" +prim__gossamer_android_register_widget_callbacks : Bits64 -> Bits64 -> PrimIO () + +export +%foreign "C:gossamer_arch, libgossamer" +prim__gossamer_arch : PrimIO Bits64 + +export +%foreign "C:gossamer_arrange, libgossamer" +prim__gossamer_arrange : Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_async_inflight_count, libgossamer" +prim__gossamer_async_inflight_count : PrimIO Bits32 + +export +%foreign "C:gossamer_broadcast, libgossamer" +prim__gossamer_broadcast : String -> String -> PrimIO Bits32 + +export +%foreign "C:gossamer_build_info, libgossamer" +prim__gossamer_build_info : PrimIO Bits64 + +export +%foreign "C:gossamer_cap_check, libgossamer" +prim__gossamer_cap_check : Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_cap_get_max, libgossamer" +prim__gossamer_cap_get_max : PrimIO Bits32 + +export +%foreign "C:gossamer_cap_grant, libgossamer" +prim__gossamer_cap_grant : Bits32 -> PrimIO Bits64 + +export +%foreign "C:gossamer_cap_resource_kind, libgossamer" +prim__gossamer_cap_resource_kind : Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_cap_revoke, libgossamer" +prim__gossamer_cap_revoke : Bits64 -> PrimIO () + +export +%foreign "C:gossamer_cap_set_max, libgossamer" +prim__gossamer_cap_set_max : Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_channel_bind, libgossamer" +prim__gossamer_channel_bind : Bits64 -> String -> Bits64 -> Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_channel_bind_async, libgossamer" +prim__gossamer_channel_bind_async : Bits64 -> String -> Bits64 -> Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_channel_close, libgossamer" +prim__gossamer_channel_close : Bits64 -> PrimIO () + +export +%foreign "C:gossamer_channel_open, libgossamer" +prim__gossamer_channel_open : Bits64 -> PrimIO Bits64 + +export +%foreign "C:gossamer_channel_register_defaults, libgossamer" +prim__gossamer_channel_register_defaults : Bits64 -> Bits64 -> PrimIO () + +export +%foreign "C:gossamer_clipboard_read, libgossamer" +prim__gossamer_clipboard_read : Bits64 -> Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_clipboard_write, libgossamer" +prim__gossamer_clipboard_write : String -> PrimIO Bits32 + +export +%foreign "C:gossamer_conf_free, libgossamer" +prim__gossamer_conf_free : Bits64 -> PrimIO () + +export +%foreign "C:gossamer_conf_get_bool, libgossamer" +prim__gossamer_conf_get_bool : Bits64 -> String -> Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_conf_get_int, libgossamer" +prim__gossamer_conf_get_int : Bits64 -> String -> Bits64 -> PrimIO Bits64 + +export +%foreign "C:gossamer_conf_get_string, libgossamer" +prim__gossamer_conf_get_string : Bits64 -> String -> PrimIO Bits64 + +export +%foreign "C:gossamer_conf_has, libgossamer" +prim__gossamer_conf_has : Bits64 -> String -> PrimIO Bits32 + +export +%foreign "C:gossamer_conf_load, libgossamer" +prim__gossamer_conf_load : String -> Bits64 -> PrimIO Bits64 + +export +%foreign "C:gossamer_create, libgossamer" +prim__gossamer_create : String -> Bits32 -> Bits32 -> Bits8 -> Bits8 -> Bits8 -> PrimIO Bits64 + +export +%foreign "C:gossamer_create_ex, libgossamer" +prim__gossamer_create_ex : String -> Bits32 -> Bits32 -> Bits32 -> Bits32 -> Bits32 -> Bits32 -> Bits8 -> Bits8 -> Bits8 -> Bits8 -> PrimIO Bits64 + +export +%foreign "C:gossamer_debug_close, libgossamer" +prim__gossamer_debug_close : Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_debug_open, libgossamer" +prim__gossamer_debug_open : Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_debug_toggle, libgossamer" +prim__gossamer_debug_toggle : Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_destroy, libgossamer" +prim__gossamer_destroy : Bits64 -> PrimIO () + +export +%foreign "C:gossamer_dialog_free_path, libgossamer" +prim__gossamer_dialog_free_path : Bits64 -> PrimIO () + +export +%foreign "C:gossamer_dialog_open, libgossamer" +prim__gossamer_dialog_open : String -> String -> PrimIO Bits64 + +export +%foreign "C:gossamer_dialog_open_directory, libgossamer" +prim__gossamer_dialog_open_directory : String -> PrimIO Bits64 + +export +%foreign "C:gossamer_dialog_open_multiple, libgossamer" +prim__gossamer_dialog_open_multiple : String -> String -> PrimIO Bits64 + +export +%foreign "C:gossamer_dialog_save, libgossamer" +prim__gossamer_dialog_save : String -> String -> PrimIO Bits64 + +export +%foreign "C:gossamer_emit, libgossamer" +prim__gossamer_emit : Bits64 -> String -> String -> PrimIO Bits32 + +export +%foreign "C:gossamer_emit_binary, libgossamer" +prim__gossamer_emit_binary : Bits64 -> String -> Bits64 -> Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_eval, libgossamer" +prim__gossamer_eval : Bits64 -> String -> PrimIO Bits32 + +export +%foreign "C:gossamer_fs_copy_file, libgossamer" +prim__gossamer_fs_copy_file : String -> String -> Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_fs_exists, libgossamer" +prim__gossamer_fs_exists : String -> Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_fs_list_dir, libgossamer" +prim__gossamer_fs_list_dir : String -> Bits64 -> PrimIO Bits64 + +export +%foreign "C:gossamer_fs_mkdir_p, libgossamer" +prim__gossamer_fs_mkdir_p : String -> Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_fs_read_text, libgossamer" +prim__gossamer_fs_read_text : String -> Bits64 -> PrimIO Bits64 + +export +%foreign "C:gossamer_fs_remove, libgossamer" +prim__gossamer_fs_remove : String -> Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_fs_write_text, libgossamer" +prim__gossamer_fs_write_text : String -> String -> Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_get_max_inflight, libgossamer" +prim__gossamer_get_max_inflight : PrimIO Bits32 + +export +%foreign "C:gossamer_groove_check_compat, libgossamer" +prim__gossamer_groove_check_compat : Bits32 -> Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_groove_connect_typed, libgossamer" +prim__gossamer_groove_connect_typed : Bits32 -> Bits32 -> Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_groove_disconnect, libgossamer" +prim__gossamer_groove_disconnect : Bits32 -> PrimIO () + +export +%foreign "C:gossamer_groove_disconnect_all, libgossamer" +prim__gossamer_groove_disconnect_all : PrimIO () + +export +%foreign "C:gossamer_groove_disconnect_typed, libgossamer" +prim__gossamer_groove_disconnect_typed : Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_groove_discover, libgossamer" +prim__gossamer_groove_discover : PrimIO Bits32 + +export +%foreign "C:gossamer_groove_dock, libgossamer" +prim__gossamer_groove_dock : Bits64 -> String -> Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_groove_find_capability, libgossamer" +prim__gossamer_groove_find_capability : String -> PrimIO Bits32 + +export +%foreign "C:gossamer_groove_manifest, libgossamer" +prim__gossamer_groove_manifest : Bits32 -> PrimIO Bits64 + +export +%foreign "C:gossamer_groove_query_type, libgossamer" +prim__gossamer_groove_query_type : Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_groove_recv, libgossamer" +prim__gossamer_groove_recv : Bits32 -> PrimIO Bits64 + +export +%foreign "C:gossamer_groove_send, libgossamer" +prim__gossamer_groove_send : Bits32 -> String -> PrimIO Bits32 + +export +%foreign "C:gossamer_groove_signing_active, libgossamer" +prim__gossamer_groove_signing_active : PrimIO Bits32 + +export +%foreign "C:gossamer_groove_status, libgossamer" +prim__gossamer_groove_status : Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_groove_summary, libgossamer" +prim__gossamer_groove_summary : PrimIO Bits64 + +export +%foreign "C:gossamer_groove_tls_enabled, libgossamer" +prim__gossamer_groove_tls_enabled : PrimIO Bits32 + +export +%foreign "C:gossamer_groove_undock, libgossamer" +prim__gossamer_groove_undock : Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_group_add, libgossamer" +prim__gossamer_group_add : Bits32 -> Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_group_apply, libgossamer" +prim__gossamer_group_apply : Bits32 -> Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_group_create, libgossamer" +prim__gossamer_group_create : String -> PrimIO Bits32 + +export +%foreign "C:gossamer_group_destroy, libgossamer" +prim__gossamer_group_destroy : Bits32 -> PrimIO () + +export +%foreign "C:gossamer_group_remove, libgossamer" +prim__gossamer_group_remove : Bits32 -> Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_guard_get, libgossamer" +prim__gossamer_guard_get : Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_guard_set, libgossamer" +prim__gossamer_guard_set : Bits64 -> Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_hide, libgossamer" +prim__gossamer_hide : Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_is_desktop, libgossamer" +prim__gossamer_is_desktop : PrimIO Bits8 + +export +%foreign "C:gossamer_last_error, libgossamer" +prim__gossamer_last_error : PrimIO Bits64 + +export +%foreign "C:gossamer_load_html, libgossamer" +prim__gossamer_load_html : Bits64 -> String -> PrimIO Bits32 + +export +%foreign "C:gossamer_lower, libgossamer" +prim__gossamer_lower : Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_maximize, libgossamer" +prim__gossamer_maximize : Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_minimize, libgossamer" +prim__gossamer_minimize : Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_navigate, libgossamer" +prim__gossamer_navigate : Bits64 -> String -> PrimIO Bits32 + +export +%foreign "C:gossamer_notify, libgossamer" +prim__gossamer_notify : String -> String -> PrimIO Bits32 + +export +%foreign "C:gossamer_platform, libgossamer" +prim__gossamer_platform : PrimIO Bits64 + +export +%foreign "C:gossamer_platform_json, libgossamer" +prim__gossamer_platform_json : PrimIO Bits64 + +export +%foreign "C:gossamer_plugin_list, libgossamer" +prim__gossamer_plugin_list : PrimIO Bits64 + +export +%foreign "C:gossamer_plugin_load, libgossamer" +prim__gossamer_plugin_load : Bits64 -> String -> PrimIO Bits32 + +export +%foreign "C:gossamer_plugin_unload, libgossamer" +prim__gossamer_plugin_unload : Bits32 -> PrimIO () + +export +%foreign "C:gossamer_raise, libgossamer" +prim__gossamer_raise : Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_registry_add, libgossamer" +prim__gossamer_registry_add : Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_registry_count, libgossamer" +prim__gossamer_registry_count : PrimIO Bits32 + +export +%foreign "C:gossamer_registry_remove, libgossamer" +prim__gossamer_registry_remove : Bits64 -> PrimIO () + +export +%foreign "C:gossamer_request_close, libgossamer" +prim__gossamer_request_close : Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_resize, libgossamer" +prim__gossamer_resize : Bits64 -> Bits32 -> Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_restore, libgossamer" +prim__gossamer_restore : Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_run, libgossamer" +prim__gossamer_run : Bits64 -> PrimIO () + +export +%foreign "C:gossamer_send_to, libgossamer" +prim__gossamer_send_to : Bits32 -> String -> String -> PrimIO Bits32 + +export +%foreign "C:gossamer_set_csp, libgossamer" +prim__gossamer_set_csp : Bits64 -> String -> PrimIO Bits32 + +export +%foreign "C:gossamer_set_max_inflight, libgossamer" +prim__gossamer_set_max_inflight : Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_set_title, libgossamer" +prim__gossamer_set_title : Bits64 -> String -> PrimIO Bits32 + +export +%foreign "C:gossamer_shell_kill, libgossamer" +prim__gossamer_shell_kill : Bits64 -> Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_shell_spawn, libgossamer" +prim__gossamer_shell_spawn : String -> Bits64 -> PrimIO Bits64 + +export +%foreign "C:gossamer_show, libgossamer" +prim__gossamer_show : Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_ssg_build_site, libgossamer" +prim__gossamer_ssg_build_site : String -> String -> String -> PrimIO Bits32 + +export +%foreign "C:gossamer_ssg_list_files, libgossamer" +prim__gossamer_ssg_list_files : String -> String -> PrimIO Bits64 + +export +%foreign "C:gossamer_ssg_md_to_html, libgossamer" +prim__gossamer_ssg_md_to_html : String -> PrimIO Bits64 + +export +%foreign "C:gossamer_ssg_parse_body, libgossamer" +prim__gossamer_ssg_parse_body : String -> PrimIO Bits64 + +export +%foreign "C:gossamer_ssg_parse_front_matter, libgossamer" +prim__gossamer_ssg_parse_front_matter : String -> PrimIO Bits64 + +export +%foreign "C:gossamer_ssg_read_file, libgossamer" +prim__gossamer_ssg_read_file : String -> PrimIO Bits64 + +export +%foreign "C:gossamer_ssg_template_substitute, libgossamer" +prim__gossamer_ssg_template_substitute : String -> String -> PrimIO Bits64 + +export +%foreign "C:gossamer_ssg_write_file, libgossamer" +prim__gossamer_ssg_write_file : String -> String -> PrimIO Bits32 + +export +%foreign "C:gossamer_transmute, libgossamer" +prim__gossamer_transmute : Bits64 -> Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_transmute_get, libgossamer" +prim__gossamer_transmute_get : Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_tray_add_item, libgossamer" +prim__gossamer_tray_add_item : Bits64 -> String -> Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_tray_add_separator, libgossamer" +prim__gossamer_tray_add_separator : Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_tray_clear_window, libgossamer" +prim__gossamer_tray_clear_window : PrimIO () + +export +%foreign "C:gossamer_tray_create, libgossamer" +prim__gossamer_tray_create : String -> PrimIO Bits64 + +export +%foreign "C:gossamer_tray_destroy, libgossamer" +prim__gossamer_tray_destroy : Bits64 -> PrimIO () + +export +%foreign "C:gossamer_tray_set_callback, libgossamer" +prim__gossamer_tray_set_callback : Bits64 -> Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_tray_set_icon, libgossamer" +prim__gossamer_tray_set_icon : Bits64 -> String -> PrimIO Bits32 + +export +%foreign "C:gossamer_tray_set_icon_from_file, libgossamer" +prim__gossamer_tray_set_icon_from_file : Bits64 -> String -> PrimIO Bits32 + +export +%foreign "C:gossamer_tray_set_tooltip, libgossamer" +prim__gossamer_tray_set_tooltip : Bits64 -> String -> PrimIO Bits32 + +export +%foreign "C:gossamer_tray_set_visible, libgossamer" +prim__gossamer_tray_set_visible : Bits64 -> Bits32 -> PrimIO Bits32 + +export +%foreign "C:gossamer_tray_set_window, libgossamer" +prim__gossamer_tray_set_window : Bits64 -> Bits64 -> PrimIO Bits32 + +export +%foreign "C:gossamer_version, libgossamer" +prim__gossamer_version : PrimIO Bits64 + +export +%foreign "C:gossamer_watcher_start, libgossamer" +prim__gossamer_watcher_start : Bits64 -> String -> String -> PrimIO Bits64 + +export +%foreign "C:gossamer_watcher_stop, libgossamer" +prim__gossamer_watcher_stop : Bits64 -> PrimIO () + +export +%foreign "C:gossamer_webview_engine, libgossamer" +prim__gossamer_webview_engine : PrimIO Bits64 From d3d8791227e33b32f1c7cbf58cd66a8b1feb9645 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 3 Jul 2026 02:30:42 +0000 Subject: [PATCH 3/3] fix(abi): rewrite the FFI-cleave generator in bash+awk (Python is estate-banned) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The "Language / package anti-pattern policy" gate flagged scripts/gen-abi-foreign.py — Python is banned estate-wide (the base commit had no .py files). Rewrote it as scripts/gen-abi-foreign.sh (bash + awk, matching the scripts/*.awk precedent), parsing the Zig export fns with balanced-paren handling for the multi-line callback signatures (channel_bind / channel_bind_async / tray_set_callback have inline ?*const fn(...) params) under the same position-aware type map. Verified: the bash+awk output is BYTE-IDENTICAL to the (idris2-green, adversarially-verified) Python output on all 130 declarations — only the two header lines naming the generator differ. ForeignGen.idr typechecks green; guards + both packages green; 147/147 tests; the --check freshness gate and the negative test (new Zig export -> stale -> fail) both work. Updated the cleave gate, Justfile, workflow path filter and docs to the .sh; removed the .py. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_013Zg1kEsjSRpcf1wFBZyeNj --- .github/workflows/abi-typecheck.yml | 4 +- CHANGELOG.md | 2 +- Justfile | 2 +- PROOF-NEEDS.md | 2 +- scripts/check-abi-ffi-cleave.sh | 8 +- scripts/gen-abi-foreign.py | 181 ---------------------------- scripts/gen-abi-foreign.sh | 129 ++++++++++++++++++++ src/interface/abi/ForeignGen.idr | 4 +- 8 files changed, 138 insertions(+), 194 deletions(-) delete mode 100644 scripts/gen-abi-foreign.py create mode 100755 scripts/gen-abi-foreign.sh diff --git a/.github/workflows/abi-typecheck.yml b/.github/workflows/abi-typecheck.yml index 40996c4..8649dda 100644 --- a/.github/workflows/abi-typecheck.yml +++ b/.github/workflows/abi-typecheck.yml @@ -19,7 +19,7 @@ on: - 'gossamer-abi-tests.ipkg' - 'scripts/check-abi-decoupling.sh' - 'scripts/check-abi-ffi-cleave.sh' - - 'scripts/gen-abi-foreign.py' + - 'scripts/gen-abi-foreign.sh' - '.github/workflows/abi-typecheck.yml' push: branches: [main, master] @@ -31,7 +31,7 @@ on: - 'gossamer-abi-tests.ipkg' - 'scripts/check-abi-decoupling.sh' - 'scripts/check-abi-ffi-cleave.sh' - - 'scripts/gen-abi-foreign.py' + - 'scripts/gen-abi-foreign.sh' - '.github/workflows/abi-typecheck.yml' permissions: diff --git a/CHANGELOG.md b/CHANGELOG.md index 13b6315..6ecbc56 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -23,7 +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.py` — 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.py` **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. +- **`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. diff --git a/Justfile b/Justfile index bf9f362..a07c925 100644 --- a/Justfile +++ b/Justfile @@ -57,7 +57,7 @@ abi-check: # 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: - python3 scripts/gen-abi-foreign.py + ./scripts/gen-abi-foreign.sh # Build the Gossamer CLI (links libgossamer) build-cli: build-ffi diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 4528941..137fb25 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -17,7 +17,7 @@ - `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`) — 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.py` 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%)**. + - **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. diff --git a/scripts/check-abi-ffi-cleave.sh b/scripts/check-abi-ffi-cleave.sh index d08caed..c9d93b6 100755 --- a/scripts/check-abi-ffi-cleave.sh +++ b/scripts/check-abi-ffi-cleave.sh @@ -74,12 +74,8 @@ fi # 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 command -v python3 >/dev/null 2>&1; then - if ! python3 scripts/gen-abi-foreign.py --check; then - fail=1 - fi -else - echo " (python3 unavailable — skipping ForeignGen freshness check)" +if ! scripts/gen-abi-foreign.sh --check; then + fail=1 fi # --- GitHub step summary (when running in Actions) --- diff --git a/scripts/gen-abi-foreign.py b/scripts/gen-abi-foreign.py deleted file mode 100644 index 8af2006..0000000 --- a/scripts/gen-abi-foreign.py +++ /dev/null @@ -1,181 +0,0 @@ -#!/usr/bin/env python3 -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# gen-abi-foreign.py — generate the complete raw %foreign mirror of the -# libgossamer C ABI (Gossamer.ABI.ForeignGen) from the Zig `export fn` -# declarations. This makes the Zig FFI the SINGLE SOURCE OF TRUTH for the ABI -# surface (gossamer#82): the Idris ABI can no longer drift from — or lie about — -# the real exports, because it is generated from them and checked fresh in CI. -# -# Usage: -# scripts/gen-abi-foreign.py # write src/interface/abi/ForeignGen.idr -# scripts/gen-abi-foreign.py --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 the same width, C strings -> -# String as a parameter / Bits64 (char* pointer) as a return, all pointers and -# function pointers -> Bits64, void -> (), every call wrapped in PrimIO. -import glob -import os -import re -import sys - -ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) -FFI_GLOB = os.path.join(ROOT, "src/interface/ffi/src/*.zig") -OUT = os.path.join(ROOT, "src/interface/abi/ForeignGen.idr") - -# Integer / scalar Zig types -> Idris Bits* (bit-accurate; signedness is a -# wrapper concern, and the curated Foreign.idr proves Bits* work over %foreign). -SCALAR = { - "void": "()", - "bool": "Bits8", - "u8": "Bits8", "i8": "Bits8", - "u16": "Bits16", "i16": "Bits16", - "u32": "Bits32", "i32": "Bits32", "c_int": "Bits32", "c_uint": "Bits32", - "u64": "Bits64", "i64": "Bits64", "usize": "Bits64", "isize": "Bits64", - "c_long": "Bits64", "c_ulong": "Bits64", - "f32": "Double", "f64": "Double", -} -CSTR = {"[*:0]const u8", "?[*:0]const u8", "[*c]const u8", "?[*c]const u8"} - - -def strip_comment(s: str) -> str: - return re.sub(r"//.*$", "", s).strip() - - -def map_type(z: str, is_return: bool) -> str: - z = strip_comment(z).rstrip(",").strip() - if not z: - return "()" - nospace = z.replace(" ", "") - # function pointer (callback) -> raw pointer value - if "fn(" in nospace: - return "Bits64" - # C strings: String as a parameter, char* pointer (Bits64) as a return - if z in CSTR: - return "Bits64" if is_return else "String" - # any other pointer / many-item pointer / slice / optional pointer -> Bits64 - if re.match(r"^\??\*", z) or re.match(r"^\??\[\*", z): - return "Bits64" - if z in SCALAR: - return SCALAR[z] - # Named enums backed by c_int (the Result enum, possibly module-qualified). - if z == "Result" or z.endswith(".Result"): - return "Bits32" - # Named function-pointer typedefs (Zig convention: `*Fn` / `?*Fn`) -> pointer. - bare = z[1:].strip() if z.startswith("?") else z - if bare.endswith("Fn"): - return "Bits64" - # Unknown type — fail loudly rather than emit a silent wrong binding. - raise SystemExit(f"gen-abi-foreign: unmapped Zig type {z!r} — extend SCALAR/rules") - - -def split_params(param_src: str): - """Split a Zig parameter list on top-level commas (paren-depth aware, so - function-pointer params like `?*const fn(...) callconv(.c) void` stay whole).""" - out, depth, cur = [], 0, "" - for ch in param_src: - if ch in "([{": - depth += 1 - elif ch in ")]}": - depth -= 1 - if ch == "," and depth == 0: - out.append(cur) - cur = "" - else: - cur += ch - if cur.strip(): - out.append(cur) - return [p for p in (x.strip() for x in out) if p] - - -def param_type(p: str) -> str: - # "name: TYPE" -> TYPE (a param has exactly one top-level colon) - m = re.match(r"^[A-Za-z_][A-Za-z0-9_]*\s*:\s*(.+)$", strip_comment(p), re.S) - return (m.group(1) if m else p).strip() - - -def parse_exports(text: str): - """Yield (symbol, [param_types], return_type) for each `export fn gossamer_*`, - scanning balanced parens so multi-line and callback signatures parse cleanly.""" - for m in re.finditer(r"(?:pub\s+)?export\s+fn\s+(gossamer_[A-Za-z0-9_]+)\s*\(", text): - name = m.group(1) - i = m.end() # just past the '(' - depth, start = 1, i - while i < len(text) and depth: - if text[i] == "(": - depth += 1 - elif text[i] == ")": - depth -= 1 - i += 1 - params_src = text[start:i - 1] - rest = text[i:] - rm = re.match(r"\s*(?:callconv\([^)]*\)\s*)?([^\{;]+?)\s*\{", rest, re.S) - ret = strip_comment(rm.group(1)) if rm else "void" - yield name, [param_type(p) for p in split_params(params_src)], ret - - -def idris_sig(params, ret) -> str: - pts = [map_type(p, False) for p in params] - r = map_type(ret, True) - arrow = "".join(f"{t} -> " for t in pts) - return f"{arrow}PrimIO {r}" - - -HEADER = """-- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- -||| GENERATED FILE — DO NOT EDIT BY HAND. -||| Regenerate with `just abi-gen` (scripts/gen-abi-foreign.py); CI fails if this -||| file is stale (scripts/check-abi-ffi-cleave.sh --check-generated). -||| -||| 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 -""" - - -def generate() -> str: - syms = {} - for path in sorted(glob.glob(FFI_GLOB)): - with open(path, encoding="utf-8") as f: - for name, params, ret in parse_exports(f.read()): - syms[name] = (params, ret) # last def wins; symbols are unique - lines = [HEADER] - for name in sorted(syms): - params, ret = syms[name] - lines.append(f'export\n%foreign "C:{name}, libgossamer"\n' - f'prim__{name} : {idris_sig(params, ret)}\n') - return "\n".join(lines) + "\n" if False else "\n".join(lines).rstrip() + "\n" - - -def main(): - content = generate() - if "--check" in sys.argv or "--check-generated" in sys.argv: - try: - with open(OUT, encoding="utf-8") as f: - current = f.read() - except FileNotFoundError: - current = None - if current != content: - print("::error::ForeignGen.idr is stale — run `just abi-gen` and commit " - "(the Zig FFI surface changed but the generated ABI mirror did not).", - file=sys.stderr) - sys.exit(1) - print("ForeignGen.idr is up to date with the Zig FFI surface.") - return - with open(OUT, "w", encoding="utf-8") as f: - f.write(content) - n = content.count("%foreign") - print(f"wrote {OUT} ({n} %foreign declarations)") - - -if __name__ == "__main__": - main() diff --git a/scripts/gen-abi-foreign.sh b/scripts/gen-abi-foreign.sh new file mode 100755 index 0000000..39d27f0 --- /dev/null +++ b/scripts/gen-abi-foreign.sh @@ -0,0 +1,129 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# 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) +-- +||| 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 "symbolidris-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 diff --git a/src/interface/abi/ForeignGen.idr b/src/interface/abi/ForeignGen.idr index 8bc5fdd..5ff2c55 100644 --- a/src/interface/abi/ForeignGen.idr +++ b/src/interface/abi/ForeignGen.idr @@ -2,8 +2,8 @@ -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -- ||| GENERATED FILE — DO NOT EDIT BY HAND. -||| Regenerate with `just abi-gen` (scripts/gen-abi-foreign.py); CI fails if this -||| file is stale (scripts/check-abi-ffi-cleave.sh --check-generated). +||| 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,