feat(abi): ABI↔FFI cleave gate — no phantom %foreign can return (gossamer#82) by hyperpolymath · Pull Request #98 · hyperpolymath/gossamer

hyperpolymath · 2026-07-03T01:36:02Z

Summary

First concrete step on #82's CRITICAL item (the "phantom template"). #95 fixed the honest Foreign.idr; this makes that fix permanent and measurable.

The root problem #82 names: idris2 --typecheck proves the ABI internally sound but cannot see whether a %foreign "C:sym, libgossamer" resolves to a real Zig export — that linkage is only exercised at link time. That blind spot is exactly how 8 phantom symbols (gossamer_init/process/…) hid behind a green typecheck. This PR adds the missing check as a fast, toolchain-free gate.

What the gate does — `scripts/check-abi-ffi-cleave.sh`

HARD FAIL on any ABI %foreign with no matching export fn in src/interface/ffi/src/*.zig — the ABI can never again lie about the FFI.
REPORT coverage of the real C surface: 29 / 130 gossamer_* exports are declared today; the 101 uncovered are the tracked expansion work. Coverage is reported, not failed, so adding 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.

The ground truth it establishes (for #82)

	count
ABI `%foreign` C:libgossamer declarations	29
Real Zig `gossamer_*` C exports	130
Phantom (declared, not exported)	0 ✅
Covered (declared and exported)	29
Uncovered (exported, not declared)	101 — expansion work

So #82-CRITICAL splits cleanly: "no phantom symbols" is now done and gated; "the ABI describes the full real surface" is 22%, and is the next decision (see below).

RSR Quality Checklist

Required

Tests pass (idris2 flow unchanged: both packages typecheck, 147/147)
Code formatted; scripts/*.sh shellcheck-clean
Linter clean (no new warnings)
No banned language patterns (Bash / YAML / Markdown)
No unsafe without // SAFETY: (none)
No banned functions (believe_me, sorry, …) — none added
SPDX header on the new script
No secrets

As Applicable

Documentation updated (PROOF-NEEDS.md, CHANGELOG.md)
ABI/FFI change validated (the gate is the validation; run locally + negative-tested)

Testing

cleave gate on current tree ......... PASS (0 phantom; 29/130 reported)
cleave gate w/ injected phantom ..... FAIL (phantom listed)  ✓ negative test
shellcheck .......................... clean
decoupling guard .................... PASS
idris2 typecheck (shell+groove) ..... GREEN
ABI test suite ...................... 147 / 147

Next decision for #82 (not in this PR)

Closing the coverage half (declaring the 101 uncovered exports) raises #82's open architectural question — single source of truth + codegen. My recommendation: generate the %foreign block from the Zig export fn signatures (Zig FFI = SoT), so the ABI can never drift from the FFI by construction, and this gate flips from "reports 22%" to "enforces 100%". Happy to build that next if you agree on the direction — or hand-declare incrementally by module if you'd rather keep it manual.

🤖 Generated with Claude Code

https://claude.ai/code/session_013Zg1kEsjSRpcf1wFBZyeNj

Generated by Claude Code

…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. 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013Zg1kEsjSRpcf1wFBZyeNj

… (gossamer#82) (#101) ## Summary Closes the Ephapax half of gossamer#82. The 13 `src/core/*.eph` bindings to the libgossamer C ABI were `__ffi(...)` passthroughs over raw `I64` handles with comments *claiming* linearity but **zero `let!` bindings** — and, because `__ffi` is typed `I64` while the wrappers declared `: I32` / `: ()` / `String` returns, **not one of them type-checked**. `ephapax check` rejected all 13. A comment is not a proof. This PR rewrites them so the Ephapax compiler is the oracle, and adds a CI gate that re-runs the linearity proof every run. Refs gossamer#82. Complements the Idris2 ABI↔FFI cleave work (#98/#99/#100). ## Changes - **13/13 `.eph` files now type-check** under `ephapax check` (`--mode linear`), up from **0/13**. - **8 handle-owning modules are genuinely linear** via `extern` opaque handle types + `let!`: `Bridge` (`Channel`), `Shell` (`Webview`), `Tray` (`Tray`), `Capabilities` (`CapToken`), `Conf` (`Conf`), `ClosureConversion` (`Closure`), `ShellExec` (`Child`), `Dialog` (`DialogPath`). The resource is minted linear, borrowed via `&Handle` for mid-lifetime ops, and CONSUMED exactly once by its retire op — so **leaking a handle is a compile-time error** (`Linear variable not consumed`). - **5 compute modules** (`Platform`, `Module`, `Filesystem`, `SSG`, `Groove`) own no linear handle and are correctly-typed `extern` surfaces. `Groove` is registry-indexed at the `.eph` layer, so its connection linearity stays proved in Idris2 (`GrooveLinearity.idr` / `GrooveResidue.idr`). Only real C symbols are declared — **no phantom FFI**. - **`scripts/check-eph-linearity.sh`** — positive gate (all `.eph` type-check) + negative gate (drop each handle's consume, assert `ephapax check` rejects it). Shellcheck-clean. - **`.github/workflows/eph-linearity.yml`** — builds Ephapax (`hyperpolymath/ephapax`, pinned) from source as the oracle; degrades to a notice if unreachable (estate sibling-tool convention). - **`just eph-check`** added; **`just check`** now covers all 13 modules (was 5). - `CHANGELOG.md` + `PROOF-NEEDS.md` updated. ## RSR Quality Checklist ### Required - [x] Tests pass — Ephapax gate green: 13/13 type-check + 8/8 leak-rejections (`./scripts/check-eph-linearity.sh`). The `.eph` layer is not part of the Idris2 147-test suite, which is unaffected. - [ ] Code is formatted — no `.eph` formatter exists in-tree; files follow the surrounding style. - [x] Linter is clean — `shellcheck scripts/check-eph-linearity.sh` clean. - [x] No banned language patterns — Ephapax + bash + YAML only; no TypeScript, npm/bun, Go, or Python. - [x] No `unsafe` blocks without `// SAFETY:` comments — none introduced. - [x] No banned functions (`believe_me`, `unsafeCoerce`, `Obj.magic`, `Admitted`, `sorry`) — none in the `.eph` layer. - [x] SPDX license headers present on all new/modified source files — MPL-2.0 on every `.eph`, the script, and the workflow. - [x] No secrets, credentials, or `.env` files included. ### As Applicable - [x] Documentation updated for user-facing changes — `PROOF-NEEDS.md`. - [x] `CHANGELOG` or release notes updated. - [x] ABI/FFI changes validated — every `extern` declares a real `gossamer_*` (or Idris2 RTS) symbol; no phantom FFI, mirroring the Idris2 cleave gate. ## Testing Local, against the Ephapax compiler built from `hyperpolymath/ephapax` @ `55d6a24`: ``` $ ./scripts/check-eph-linearity.sh -- positive: ephapax check (linear mode) on src/core/*.eph -- type-check: 13/13 clean -- negative: drop the consume → 'Linear variable not consumed' expected -- ✓ Bridge leak REJECTED: ... Linear variable `ch` not consumed ✓ Shell leak REJECTED: ... Linear variable `w` not consumed ✓ Tray leak REJECTED: ... Linear variable `t` not consumed ✓ ShellExec leak REJECTED: ... `child` not consumed ✓ Capabilities leak REJECTED: ... `tok` not consumed ✓ Conf leak REJECTED: ... `c` not consumed ✓ ClosureConversion leak REJECTED: ... `clo` not consumed ✓ Dialog leak REJECTED: ... `p` not consumed Ephapax linearity gate: PASSED ``` The negative half deletes each module's consuming call *on the real file* and confirms the compiler rejects the leak — so a silent de-linearisation (opaque type reverted to `I64`, or `let!` downgraded to `let`) fails the gate. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_013Zg1kEsjSRpcf1wFBZyeNj --- _Generated by [Claude Code](https://claude.ai/code/session_013Zg1kEsjSRpcf1wFBZyeNj)_ Co-authored-by: Claude <noreply@anthropic.com>

hyperpolymath mentioned this pull request Jul 3, 2026

Cleave-surface audit: ABI/FFI/Ephapax/Groove drift + ranked-ownership cleave (forward plan) #82

Open

11 tasks

hyperpolymath marked this pull request as ready for review July 3, 2026 01:42

hyperpolymath merged commit 8d5743b into main Jul 3, 2026
21 of 22 checks passed

hyperpolymath deleted the claude/gossamer-95-root-cause-rlhts0 branch July 3, 2026 01:42

hyperpolymath mentioned this pull request Jul 3, 2026

feat(eph): make src/core/*.eph genuinely linear — verified by ephapax (gossamer#82) #101

Merged

11 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

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

feat(abi): ABI↔FFI cleave gate — no phantom %foreign can return (gossamer#82)#98
hyperpolymath merged 1 commit into
mainfrom
claude/gossamer-95-root-cause-rlhts0

hyperpolymath commented Jul 3, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

hyperpolymath commented Jul 3, 2026

Summary

What the gate does — scripts/check-abi-ffi-cleave.sh

The ground truth it establishes (for #82)

RSR Quality Checklist

Required

As Applicable

Testing

Next decision for #82 (not in this PR)

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

What the gate does — `scripts/check-abi-ffi-cleave.sh`