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

[hyperpolymath]

Cleave-surface audit — ABI/FFI/Ephapax/Groove drift + forward plan

Tracking issue from the 2026-06-15 cleave-surface investigation. Full narrative + decisions in ~/developer/dev-notes/2026-06-15-gossamer-cleave-surface-session-handoff.adoc. Findings below were established by reading the tree and partly verified by running idris2 --typecheck / zig build; a deeper audit workflow was still finishing at session close (its consolidated brief to be appended on pickup).

Confirmed findings (severity-ranked)

• CRITICAL — the Idris2 ABI describes a phantom template, not the real ABI. src/interface/abi/Foreign.idr declares ~10 generic placeholder %foreign symbols (gossamer_init, gossamer_process, gossamer_process_array, gossamer_get_string, gossamer_register_callback, gossamer_is_initialized …). Only 3 (last_error, version, build_info) exist among the 141 real export fn C symbols in src/interface/ffi/src/*.zig. A green idris2 --typecheck does not mean the ABI matches the FFI — %foreign linkage is not checked at typecheck time. The "13/13 modules green" claim is technically true and practically meaningless for the real surface.
• HIGH — the Ephapax core is not actually linear. All 13 src/core/*.eph files contain zero let! bindings (the linear construct the whole value proposition rests on). They are thin __ffi(...) passthroughs returning bare I64. ephapax-cli is not installed in the dev env, so these .eph files have likely never been compiled. "Handle leaks become compile errors" is currently aspirational.
• HIGH — third disagreeing surface (Ephapax↔Zig). src/core/Groove.eph calls gossamer_groove_discover/status/manifest/find_capability/send/recv/summary/disconnect_all; the Zig exports gossamer_groove_connect_typed/disconnect_typed/query_type/dock/undock. The .eph references symbols the native layer does not export.
• HIGH — the one real teardown proof is unwired from disconnect. ResourceCleanup.idr proves LIFO residue→0, but gossamer_groove_disconnect_typed (main.zig:1878) is a flat wipe that never calls that descent. Per the Ranked-Ownership Cleave spec this violates RC-7/RC-8. First conformance task: wire disconnect to the proven ResourceCleanup descent.
• MEDIUM — doc/reality drift. README/TOPOLOGY reference ffi/zig/ as the implementation home (only ffi/README.adoc exists; real Zig is src/interface/ffi/src/) and a top-level src/ABI.idr (absent). "173 integration tests" / version claims need an honest recount. Foreign.idr itself admits a "latent error masked by the never-built module."

Correct proof-location map (verified — corrects an earlier mis-statement)

• Groove.idr:503 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 141 real Zig symbols), 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 (first few)

• Wire gossamer_groove_disconnect_typed → ResourceCleanup descent (closes the RC-7/RC-8 gap).
• Decide single-source-of-truth for the 141-symbol cleave + codegen-or-hand-mirror (see handoff "way forward").
• Reconcile/retract the linearity claim in README until .eph actually uses let! and compiles.
• Adopt the Groove Ranked-Ownership Cleave spec (see 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.