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

[hyperpolymath]

Status — verified-audit correction (2026-07-01, follow-up to gossamer#96)

Re-audited against main after #96 (which de-conflated Groove from the shell ABI and restored the namespace symlinks). Every finding below was re-verified with the toolchain. Four of the five original findings STAND; one — the "Ephapax↔Zig groove-surface" HIGH — was factually wrong and is corrected here; one is refined. Evidence is inline so this issue is now an accurate work-list, not a stale snapshot.

Confirmed findings (severity-ranked, re-verified 2026-07-01)

• CRITICAL — the Idris2 ABI describes a phantom template, not the real FFI. ✅ CONFIRMED. src/interface/abi/Foreign.idr declares 11 generic placeholder %foreign "C:…, libgossamer" symbols; only 3 of the 11 actually exist among the 155 export fn C symbols in src/interface/ffi/src/*.zig: gossamer_last_error, gossamer_version, gossamer_build_info. The other 8 have no Zig definition: gossamer_init, gossamer_free, gossamer_process, gossamer_free_string, gossamer_get_string, gossamer_process_array, gossamer_register_callback, gossamer_is_initialized. idris2 --typecheck does not check %foreign linkage, so "15 modules green" ≠ "ABI matches FFI". This remains the load-bearing item.

• HIGH — the Ephapax core is not actually linear. ✅ CONFIRMED. grep -c 'let!' src/core/*.eph → 0 across all .eph files: zero let! bindings, the linear construct the whole value proposition rests on. The .eph files are still thin __ffi(...) passthroughs. "Handle leaks become compile errors" stays aspirational until the .eph bodies use let! and are compiled by ephapax.

• HIGH — third disagreeing surface (Ephapax↔Zig). ❌ CORRECTED — this finding was WRONG. The original claim (that Groove.eph calls discover/status/manifest/find_capability/send/recv/summary/disconnect_all while Zig only exports connect_typed/disconnect_typed/query_type/dock/undock) does not hold. Verified: all 10 gossamer_groove_* symbols called by src/core/Groove.eph have matching export fn definitions in src/interface/ffi/src/groove.zig — discover, status, manifest, find_capability, check_compat, send, recv, summary, disconnect, disconnect_all. The connect_typed/disconnect_typed/query_type/dock/undock symbols live in main.zig and are a complementary typed/panel-docking layer driven by the shell, not a competing surface. The groove discovery/messaging/teardown cleave is fully mapped. (Post-fix(abi): de-conflate Groove from the shell + restore namespace symlinks (gossamer#95) #96 the groove proofs also live in their own gossamer-groove.ipkg, one-way dependent on the shell.)

• HIGH → MEDIUM — the soft-groove privacy-wipe teardown is not proof-covered. ⚠️ REFINED (original framing was imprecise). Correction: ResourceCleanup.idr is wired to gossamer_groove_disconnect — its DisconnectGroove cleanup action maps to the symbol Groove.eph calls and Zig exports, and GrooveLinearity.consumeForDisconnect proves the Active→Consumed linearity. What is not proof-covered is the soft-groove path gossamer_groove_disconnect_typed (main.zig), the flat state-zeroing wipe used for soft grooves: ResourceCleanup proves the plain disconnect residue→0 descent, not the typed wipe. This is the real RC-7/RC-8 gap — extend residue→0 to cover the soft-groove disconnect_typed wipe.

• MEDIUM — doc/reality drift. ✅ CONFIRMED (partially addressed). README/TOPOLOGY historically referenced ffi/zig/ and a top-level src/ABI.idr that don't exist; the honest homes are src/interface/ffi/src/ and src/interface/abi/. The "173 integration tests" claim is stale — the honest count is 186 (test/integration_test.zig). Foreign.idr's own comment still admits a "latent error masked by the never-built module".

Correct proof-location map (unchanged — re-verified)

• Groove.idr handshakeRank/transitionDecreases = the connect ranking function (flat Nat, a DAG).
• GrooveTermination.idr = connect-handshake bounded-length (≤4), no measure — not teardown.
• ResourceCleanup.idr = the teardown/residue→0 proof (flat-Nat structural recursion) — the host to upgrade.

The forward frame (the "cleave surface")

Re-attach spec + proofs + linearity to the true cleave (the 155 real Zig symbols — was ~141 at the 2026-06-15 audit), as B-layer membrane properties, not to the phantom template. Cleave-surface layering: A discovery · B1 admissibility · B2 live-governance + lifecycle/residue · C1 logical schema · C2 framing/transport. Single-source-of-truth + codegen decision is the key open architectural choice (see handoff).

Locked decision — rupture policy (owner, 2026-06-15)

Zero-residue-on-rupture: day-one ownership shape (a survivor of the rupture owns the wipe, never the dying party's cleanup) + phased coverage (process-death/conn-drop first → host-crash → power-loss → durable-secret). Constrains the Zig handle-ownership design: resource+secret lifetime keyed to handle liveness; nothing stashed outside OS-reclaimed resources; groove membrane carries liveness/heartbeat so a peer reaps its half on the other's death.

Next actions (updated to reflect the re-audit)

• [CRITICAL] Replace Foreign.idr's 8 placeholder %foreign symbols with the real cleave, or codegen a mirror from the 155 Zig export fn — so the typechecked ABI is the real ABI.
• Extend ResourceCleanup residue→0 to cover the soft-groove disconnect_typed wipe (the real RC-7/RC-8 gap).
• Make the .eph core actually linear (let!) and compile it with ephapax; until then, reconcile/retract the linearity claim in README.
• Decide single-source-of-truth for the 155-symbol cleave + codegen-or-hand-mirror (see handoff "way forward").
• Wire gossamer_groove_disconnect_typed → ResourceCleanup descent → superseded: plain disconnect is wired; scope narrows to the typed wipe (see refined finding above).
• Adopt the Groove Ranked-Ownership Cleave spec (companion standards issue) as the B-layer normative doc.

Suggested labels: abi, ephapax, design, audit.

[hyperpolymath]

Audit workflow completed — new + corrected findings

The build-verified audit (57 agents) finished. Full brief saved to ~/developer/dev-notes/2026-06-15-gossamer-cleave-surface-AUDIT-BRIEF.md (+ raw JSON backup). It confirms the findings above and adds these:

Actionable regression (quick win)

• All 23 .eph files fail to parse on their leading # SPDX comment — the ephapax grammar only allows -- / // / /* */. They were born correct (//) and broken by SPDX sweep commit 3e4df44. One-line-per-file revert unblocks every ephapax typecheck. (A concrete instance of SPDX-sweep collateral damage.)

Linearity is deeper-broken than "no let!"

• I64 is structurally non-linear in ephapax's own is_linear() (ephapax-syntax/src/lib.rs:153-164). A let! on a bare-I64 handle degrades use-exactly-once → use-at-least-once (no double-revoke protection). Handles must become a linear newtype, not bare I64.
• __ffi always returns I64 but 48 wrappers declare : I32 ⇒ typecheck failure (independent of the # issue).
• Correction: a real ephapax compiler with a genuine linear typechecker does exist and builds clean (ephapax/target/debug/ephapax). Linearity is realized in burble's own .eph (let!/linear type/acquire/consume) and in gossamer's examples/ — the defect is specifically the shipping src/core library layer being non-linear __ffi wrappers.

Groove is broken end-to-end with burble

• Port mismatch: gossamer probes burble at 6473, burble actually binds 4020 (groove.zig:39 vs burble dev.exs:15) ⇒ discovery always returns .not_found.
• Burble's cap-IPC symbols (__gossamer_cap_grant, __gossamer_notify) have 0 Zig hits — name+arity mismatch, unbridged.
• Two disjoint groove subsystems that never share state: in-memory groove_connections[32] (main.zig) vs network grooves[] (groove.zig).
• Wire today = opaque JSON over HTTP/1.0-per-call (Connection: close each message, no framing/multiplex), hand-rolled brace-matching parser, bare Bits64 handles + u64/f64 cap tokens.

Data-protocol direction — updated (important)

Burble already speaks Bebop (binary control) + WebRTC (media); groove carries none of it. So the C-plane recommendation is not to invent a wire format — align to what burble already uses: Bebop for the control plane (gives C1 a real typed schema) and WebRTC/RTP for the media plane (already the lossy/low-latency transport). The job is to make groove carry these typed planes instead of opaque JSON.

Doc integrity

• Only v0.1.0 exists; v0.2.0/0.3.0/0.3.1 "released" claims are unbacked.
• "173 integration tests" = actually 186, mislocated, runner broken (zig test import-outside-module-path).

Suggested first tasks

• Revert # → // SPDX headers across src/core/*.eph (unblocks typecheck).
• Make webview/channel/cap handles a linear newtype (not I64); fix the I32/I64 wrapper return types.
• Fix the burble groove port (6473 → 4020) and bridge the cap-IPC symbols.
• Unify the two groove subsystems; replace opaque-JSON-over-HTTP/1.0 with Bebop control + WebRTC media.
• Reconcile/retract README release + linearity + test-count claims.

[hyperpolymath]

Updated the body from a fresh toolchain-verified re-audit against main (post-#96). Summary of what changed vs. the original:

• CRITICAL (phantom Foreign.idr) — re-confirmed: 3 of 11 %foreign symbols exist in the Zig FFI; 8 are missing. Stands.
• HIGH (Ephapax not linear) — re-confirmed: let! count is 0 across all src/core/*.eph. Stands.
• HIGH (Ephapax↔Zig groove surface) — corrected: this one was wrong. All 10 gossamer_groove_* calls in Groove.eph do have matching export fn in groove.zig; the connect_typed/dock/… set is a complementary shell-driven layer, not a competing surface.
• HIGH (teardown unwired) — refined: ResourceCleanup is wired to plain disconnect; the genuine gap is that the soft-groove disconnect_typed privacy-wipe isn't proof-covered. Severity dropped to MEDIUM and scoped accordingly.
• Refreshed the Zig symbol count (141 → 155) and the integration-test count (173 → 186).

Net: the issue is still valid and the CRITICAL item is real — only the groove-surface bullet needed retracting. Forward frame and the 2026-06-15 rupture-policy decision are preserved verbatim.

---

Generated by Claude Code

[hyperpolymath]

Progress on the CRITICAL item (phantom template)

Split it into its two halves and closed the first, with ground truth measured:

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

• "No phantom symbols" → DONE & gated. fix(abi): restore honest Foreign.idr — every %foreign resolves to a real export #95 restored the honest Foreign.idr (all 8 phantoms removed), and feat(abi): ABI↔FFI cleave gate — no phantom %foreign can return (gossamer#82) #98 adds scripts/check-abi-ffi-cleave.sh — a toolchain-free CI gate that hard-fails on any %foreign with no matching Zig export fn. Since idris2 --typecheck can't see %foreign linkage, this is the check that was missing. Phantom can't silently return now.
• "ABI describes the full real surface" → 22% (29/130). The gate reports the 101 uncovered exports rather than failing on them, so it's an honest, tracked metric instead of an invisible drift.

The open decision (this issue's "single-source-of-truth + codegen" question)

To close the coverage half, my recommendation is codegen the %foreign block from the Zig export fn signatures (Zig FFI = single source of truth) — then the ABI can't drift from the FFI by construction, and the cleave gate flips from "reports 22%" to "enforces 100%". The alternative is hand-declaring the 101 by module (tedious, drift-prone — the very thing this issue warns about). Awaiting a steer on direction before building it.

Remaining #82 items unchanged: Ephapax linearity (let!; blocked on the ephapax toolchain), and the soft-groove disconnect_typed residue proof.

---

Generated by Claude Code

[hyperpolymath]

CRITICAL item — both halves now closed

	status
No phantom %foreign	✅ done + gated (#95, #98)
ABI describes the full real surface	✅ 130/130 (100%) via #100

#100 closes the coverage half by codegen: scripts/gen-abi-foreign.py generates Gossamer.ABI.ForeignGen — one %foreign per Zig export fn gossamer_* — so the Zig FFI is the single source of truth for the ABI (the codegen path this issue recommended over hand-declaration). The cleave gate now runs the generator in --check mode, so the ABI can't drift from or under-describe the FFI: change an export without just abi-gen and CI fails. Verified idris2-green, generator output identical to the hand-written Foreign.idr on the 29 overlapping symbols, adversarially verified per-file (0 bugs), 147/147 tests.

Remaining #82 work

• Soft-groove disconnect_typed residue proof — ✅ done (feat(abi): prove soft-groove disconnect privacy (residue→0) — GrooveResidue (gossamer#82) #99, GrooveResidue).
• Ephapax linearity (let!) — ⛔ blocked on tooling: ephapax is only reachable as a local build of hyperpolymath/ephapax, which this environment's egress policy 403s (no public tarball/binary like idris2/zig). Can't compile-verify .eph changes here, so it stays open until the toolchain is reachable.

Net: the ABI/FFI/cleave core of #82 (the CRITICAL phantom+coverage item, the teardown residue proof, doc drift) is resolved and gated; the Ephapax-linearity item is the remaining open thread, blocked on toolchain access.

---

Generated by Claude Code