fix(abi): restore honest Foreign.idr — every %foreign resolves to a real export by hyperpolymath · Pull Request #95 · hyperpolymath/gossamer

hyperpolymath · 2026-07-01T10:08:51Z

Summary

Restores honest %foreign resolution in src/interface/abi/Foreign.idr: replaces the placeholder ABI surface — where 8 of 11 declared %foreign symbols (gossamer_init / free / process / get_string / process_array / register_callback / is_initialized) had no Zig definition (the "phantom template" that is the CRITICAL item of #82) — with the real exported C-ABI symbols. All 25 C:libgossamer %foreign declarations now resolve to an actual export fn in src/interface/ffi/src/*.zig (verified 25/25 against main).

Scope change (rebased onto current `main`)

This PR was originally a ~292-file sweep (ABI de-conflation + standards CI adoption + governance docs + .machine_readable reorg + licensing). Since it was opened, main merged equivalent-or-newer work that supersedes almost all of it:

ABI de-conflation + namespace symlinks + package split → landed via fix(abi): de-conflate Groove from the shell + restore namespace symlinks (gossamer#95) #96 (the "preserve proofs / split packages" approach).
MPL-2.0 licensing → chore(licence): normalise to MPL-2.0 + CC-BY-SA-4.0 (canonical pair) #87 / test(ci): wire the 147 Idris2 + 186 Zig integration tests into CI; clear RSR template drift #97.
Reusable CI workflows → ci: refresh standards reusable pins to current HEAD (d7c2271) #93.
Wiki → docs(wiki): add Home page — component map, status, governance #78.

Merging the original sweep now would regress that merged work (e.g. it reverts the copyright-header standardization and re-introduces older workflow/licensing patterns), and produced 54 merge conflicts. So the branch has been rebased onto main and reduced to its one non-superseded contribution: the honest Foreign.idr. The original 13 commits remain in this PR's force-push history if any other piece is wanted later.

Verification (idris2 0.8.0, Chez — matches CI)

gossamer-abi.ipkg + gossamer-groove.ipkg --typecheck green
ABI test suite: 147 / 147 pass
ABI decoupling guard: pass
%foreign symbol mapping: 25 / 25 resolve to a real Zig export fn

Addresses the CRITICAL item of #82.

…nks (gossamer#95) (#96) ## Summary Resolves the root cause behind **gossamer#95** ("restore: honest ABI decoupling from groove") — fundamentally and at source, rather than as a merge-conflict patch. Two structural defects made the ABI dishonest and fragile; both are fixed and then **gated so they cannot silently recur**. Everything is verified with the real toolchain (`idris2 0.8.0`, Chez Scheme, built to match `abi-typecheck.yml`): both packages `--typecheck` green and the 147-test ABI suite passes. This is an alternative, clean-branch resolution of the same intent as #95 (which is currently `dirty`/conflicted against `main`). Unlike #95 it **deletes no proofs** — every module is preserved, one is added. ### Root cause 1 — duplication (the "honest ABI" part) `src/interface/Gossamer/ABI/<M>.idr` had been committed as **byte-identical regular-file copies** of the canonical `src/interface/abi/<M>.idr`. The `120000` symlinks introduced in `#42` were materialised into files at some point, so every ABI module lived **twice** — the two trees could drift while `gossamer-abi.ipkg` still claimed *"symlinks map the namespace to the physical files"*. **Fix:** restored all 15 namespace entries to `120000` symlinks into the canonical `abi/` tree. One physical copy per module; nothing to drift. ### Root cause 2 — conflation (the "decoupling from groove" part) `gossamer-abi.ipkg` bundled the Groove inter-service protocol proofs into the webview **shell**, and shell modules imported `Gossamer.ABI.Groove`. - The imports in `ResourceCleanup` and `IPCDispatch` were **vestigial** — their `TGroove`/`CmdGroove*` only use shell types (`HandleToken` is defined in `HandleLinearity`, not Groove). Removed. - `HandleLinearity`'s **genuine** groove use (`grooveValid`, `LinearGroove`, `allocateGroove`, `consumeForDisconnect`) was **extracted** into a new groove-layer module `Gossamer.ABI.GrooveLinearity`, which instantiates the shell's *generic* `LinearHandle` for `GrooveHandle`. The shell now type-checks **without Idris2 ever compiling `Groove`**. Layering points one way only: Groove depends on the shell, never the reverse. ## Changes - **`gossamer-abi.ipkg`** — groove-agnostic shell (11 modules): `Types`, `Layout`, `Foreign`, `IPCDispatch`, `HandleLinearity`, `WindowStateMachine`, `LayoutStability`, `IPCIntegrity`, `PanelIsolation`, `ResourceCleanup`, `AndroidComponents`. - **`gossamer-groove.ipkg`** (new) — Groove protocol proofs (4 modules): `Groove`, `GrooveLinearity`, `CapabilityAuthenticity`, `GrooveTermination`; `depends = base, gossamer-abi`. - **`src/interface/abi/GrooveLinearity.idr`** (new) — the extracted groove-handle linearity; zero `believe_me`, `%default total`. - **`src/interface/abi/{HandleLinearity,IPCDispatch,ResourceCleanup}.idr`** — decoupled from `Gossamer.ABI.Groove`. - **`src/interface/Gossamer/ABI/*.idr`** — restored to symlinks (`100644` → `120000`). - **`scripts/check-abi-decoupling.sh`** (new) — fast, toolchain-free structural guard: fails if a namespace file is a materialised copy, if a shell module re-imports a groove module, or if the two `.ipkg`s stop partitioning the modules. Shellcheck-clean; proven to fail on both regressions and pass on the fixed tree. - **`.github/workflows/abi-typecheck.yml`** — new `abi-structure` guard job (seconds, gates before the ~15-min build) + typecheck **both** packages. - **`Justfile`** `abi-check` — runs the guard and both typechecks. - **Docs** — `README.md`, `PROOF-NEEDS.md`, `GETTING-STARTED.md`, `CHANGELOG.md`. ## RSR Quality Checklist ### Required - [x] Tests pass (`gossamer-abi-tests`: **147 passed, 0 failed**, idris2 0.8.0) - [x] Code is formatted (matches house style; `scripts/*.sh` shellcheck-clean) - [x] Linter is clean (no new warnings; only pre-existing benign `IPCIntegrity` shadowing notes) - [x] No banned language patterns (Idris2 / Bash / YAML / Markdown only) - [x] No `unsafe` blocks without `// SAFETY:` comments (none added) - [x] No banned functions (`believe_me`, `unsafeCoerce`, `Obj.magic`, `Admitted`, `sorry`) — new module has none; the one sanctioned class-J axiom in `PanelIsolation` is untouched - [x] SPDX license headers present on all new/modified source files - [x] No secrets, credentials, or `.env` files included ### As Applicable - [x] Documentation updated for user-facing changes - [x] `CHANGELOG` updated - [x] ABI/FFI changes validated (`src/interface/abi/` self-consistent; `src/interface/ffi/` untouched) - [ ] `.machine_readable/STATE.a2ml` (no state change required) ## Testing Idris2 v0.8.0 built from source with Chez Scheme (identical to `abi-typecheck.yml`). Clean-room run of every gate: ``` GATE 1/5: structural decoupling guard ......... PASSED GATE 2/5: typecheck shell (gossamer-abi.ipkg) . GREEN (11 modules) GATE 3/5: install shell ....................... installed GATE 4/5: typecheck groove (gossamer-groove) .. GREEN (4 modules) GATE 5/5: build + run ABI test suite .......... TOTAL: 147 passed, 0 failed ``` Guard negative-tested in both directions: injecting `import Gossamer.ABI.Groove` into a shell module fails Check 2; an un-staged symlink (mode `100644`) fails Check 1; the correct tree passes. 🤖 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>

…eal export Rebases PR #95's honest-Foreign.idr fix (was 070010f) onto current main. Replaces the placeholder %foreign surface — 8 of the 11 declared symbols had no Zig definition (gossamer_init/free/process/get_string/process_array/ register_callback/is_initialized), the "phantom template" flagged as the CRITICAL item of gossamer#82 — with the real exported C-ABI symbols. All 25 C:libgossamer %foreign declarations now resolve to an actual `export fn` in src/interface/ffi/src/*.zig (verified 25/25 against main's Zig). The remainder of PR #95 (ABI de-conflation, standards CI adoption, governance docs, .machine_readable reorg, licensing) is superseded by work already merged to main — #96 (de-conflation + split packages), #87/#97 (MPL-2.0 licensing), #93 (reusable workflows), #78 (wiki) — and merging it as-is regresses those. This reduces #95 to its one non-superseded contribution so it merges without conflict or regression. Verified with idris2 0.8.0: gossamer-abi + gossamer-groove --typecheck green, 147/147 ABI tests pass, ABI decoupling guard passes. Addresses the CRITICAL item of gossamer#82. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013Zg1kEsjSRpcf1wFBZyeNj

hyperpolymath · 2026-07-01T14:21:30Z

Unstuck this by rebasing the branch onto current main rather than force-merging the superseded sweep.

Why not a straight merge: the bulk of the original scope (ABI de-conflation, standards CI adoption, governance docs, .machine_readable reorg, licensing) is already on main via #96 / #87 / #97 / #93 / #78. A merge main produced 54 conflicts and, worse, would have pulled in ~233 files of now-superseded churn that regresses recent merged work (it reverts the estate-wide copyright-header standardization and re-introduces older workflow/licensing patterns).

So I kept the one piece main doesn't have — the honest Foreign.idr (your 070010f, authorship preserved) — verified 25/25 %foreign → real Zig export fn, idris2 green, 147/147 tests. The branch is now main + Foreign.idr and shows mergeable (unstable = no conflicts; the only red is the chronic Validate Hypatia Baseline governance gate, a pre-existing estate-infra failure unrelated to this change — it's been red on the last several main commits too).

The original 13 commits are recoverable from the force-push history if you want to cherry-pick anything else out of the old scope. This also closes the CRITICAL item of #82.

Generated by Claude Code

…amer#82) (#98) ## 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 - [x] Tests pass (idris2 flow unchanged: both packages typecheck, **147/147**) - [x] Code formatted; `scripts/*.sh` **shellcheck-clean** - [x] Linter clean (no new warnings) - [x] No banned language patterns (Bash / YAML / Markdown) - [x] No `unsafe` without `// SAFETY:` (none) - [x] No banned functions (`believe_me`, `sorry`, …) — none added - [x] SPDX header on the new script - [x] No secrets ### As Applicable - [x] Documentation updated (`PROOF-NEEDS.md`, `CHANGELOG.md`) - [x] 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.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 enabled auto-merge (squash) July 1, 2026 10:09

hyperpolymath disabled auto-merge July 1, 2026 11:31

hyperpolymath enabled auto-merge (squash) July 1, 2026 11:43

hyperpolymath mentioned this pull request Jul 1, 2026

fix(abi): de-conflate Groove from the shell + restore namespace symlinks (gossamer#95) #96

Merged

12 tasks

hyperpolymath disabled auto-merge July 1, 2026 13:16

hyperpolymath enabled auto-merge (rebase) July 1, 2026 13:16

hyperpolymath disabled auto-merge July 1, 2026 13:35

hyperpolymath force-pushed the restore/honest-abi-decouple-groove branch from c63c6c5 to fe56303 Compare July 1, 2026 14:20

hyperpolymath changed the title ~~restore: honest ABI decoupling from groove~~ fix(abi): restore honest Foreign.idr — every %foreign resolves to a real export Jul 1, 2026

hyperpolymath merged commit e1b2564 into main Jul 1, 2026
21 of 22 checks passed

hyperpolymath deleted the restore/honest-abi-decouple-groove branch July 1, 2026 14:36

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

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

fix(abi): restore honest Foreign.idr — every %foreign resolves to a real export#95

fix(abi): restore honest Foreign.idr — every %foreign resolves to a real export#95
hyperpolymath merged 1 commit into
mainfrom
restore/honest-abi-decouple-groove

hyperpolymath commented Jul 1, 2026 •

edited

Loading

Uh oh!

hyperpolymath commented Jul 1, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

hyperpolymath commented Jul 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Scope change (rebased onto current main)

Verification (idris2 0.8.0, Chez — matches CI)

Uh oh!

hyperpolymath commented Jul 1, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

hyperpolymath commented Jul 1, 2026 •

edited

Loading

Scope change (rebased onto current `main`)