feat(abi): codegen the full FFI cleave — ABI mirrors 130/130 Zig exports (gossamer#82)#100
Merged
Merged
Conversation
…Y 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013Zg1kEsjSRpcf1wFBZyeNj
…rts (gossamer#82) 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013Zg1kEsjSRpcf1wFBZyeNj
Owner
Author
|
Adversarial verification result (the pass the PR body said was running): 14/14 FFI source files checked, 0 confirmed mapping bugs. Each file's generated Generated by Claude Code |
Open
11 tasks
…ate-banned) 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013Zg1kEsjSRpcf1wFBZyeNj
11 tasks
hyperpolymath
added a commit
that referenced
this pull request
Jul 3, 2026
… (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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Closes the coverage half of #82's CRITICAL item and hardens the gates. Two commits:
fix(ci)— Phase A refinement found while reviewing the mergedGrooveResiduework: the decoupling gate kept a second hardcoded list of groove modules that had already drifted (GrooveResiduewas in the array but not the import-check regex, so a shell module importing it would slip through). Derived the check from the singleGROOVE_MODULESsource of truth. Negative-tested.feat(abi)— the codegen. The Idris ABI declared only 29 of 130 realgossamer_*C exports (22%); the other 101 were an honest coverage gap. Instead of hand-declaring them (drift-prone — the very thing Cleave-surface audit: ABI/FFI/Ephapax/Groove drift + ranked-ownership cleave (forward plan) #82 warns against), I generate the complete raw%foreignmirror from the Zig FFI, making Zig the single source of truth.How the cleave is closed
scripts/gen-abi-foreign.pyparses everyexport fn gossamer_*(balanced-paren aware — handles callbacks and multi-line sigs) and emitsGossamer.ABI.ForeignGen, one%foreignper symbol. The position-aware type map mirrors the hand-curatedForeign.idr: ints→same-widthBits, C string→String(param) /Bits64(char* return), pointers & fn-pointers→Bits64,Result/c_int→Bits32,void→(), allPrimIO.check-abi-ffi-cleave.shnow also runs the generator in--checkmode: change the FFI withoutjust abi-genand CI fails on a stale mirror. So the ABI cannot drift from or under-describe the FFI — the phantom-and-coverage problem of Cleave-surface audit: ABI/FFI/Ephapax/Groove drift + ranked-ownership cleave (forward plan) #82 is closed at source.Why generation, not hand-declaration
idris2 --typecheckproves the ABI internally sound but cannot see%foreignlinkage — a hand-declared binding can name a wrong type and still typecheck. Generating from the Zig signatures makes the mapping the only degree of freedom, and it's a small fixed table. Correctness of that table is what the verification below establishes.Verification
ForeignGentypechecks green; both packages green; 147/147 ABI tests pass.Foreign.idron all 29 overlapping symbols (independent human vs. generator agreement).?[*:0],callconvstripping, opaque?*Conf,?…Fncallbacks) — all correct.just abi-genregenerates; removing it restores green.RSR Quality Checklist
scripts/*.shshellcheck-clean;gen-abi-foreign.pyparses/lintsunsafewithout// SAFETY:; no banned functions (believe_me,sorry, …) —ForeignGenis raw%foreignonlyPROOF-NEEDS.md,CHANGELOG.md); ABI/FFI change validated (the gate is the validation)Not in this PR — #82's remaining items
let!): still blocked —ephapaxis only reachable as a local build ofhyperpolymath/ephapax, which the environment's egress policy 403s (no public tarball/binary like idris2/zig). I won't hand-edit.ephfiles claiming linearity I can't compile-verify. Needs the toolchain to be reachable.🤖 Generated with Claude Code
https://claude.ai/code/session_013Zg1kEsjSRpcf1wFBZyeNj
Generated by Claude Code