feat(abi): prove soft-groove disconnect privacy (residue→0) — GrooveResidue (gossamer#82) by hyperpolymath · Pull Request #99 · hyperpolymath/gossamer

hyperpolymath · 2026-07-03T01:48:51Z

Summary

Closes the RC-7/RC-8 residue gap from #82 (the "teardown" finding). ResourceCleanup proves the generic residue→0 for the plain groove disconnect, but not for the soft-groove privacy wipe done by gossamer_groove_disconnect_typed. This adds the missing proof.

The FFI semantics (main.zig): for a soft groove, disconnect zeroes the whole connection slot (gc.* = .{ .target_id = 0, .groove_type = .hard }) — enforcing SoftGroove's documented "zero residual state" guarantee; a hard groove is only deactivated so its peer identity persists for auto-reconnect.

The proof — `Gossamer.ABI.GrooveResidue` (groove package)

A GrooveConn record mirrors the Zig { target_id, groove_type, active } slot; softDisconnect mirrors the typed-disconnect branch logic. Four constructive theorems (zero believe_me):

Theorem	Statement
`softWipeZeroResidue`	soft disconnect ⇒ peer identity erased (`residue = 0`) — the privacy guarantee
`softWipeFullyCleared`	soft disconnect ⇒ the whole slot resets to the canonical zero
`hardDisconnectRetainsPeer`	hard disconnect ⇒ peer retained — proving the two modes genuinely differ (not both trivially zero)
`softDisconnectIdempotent`	re-disconnecting is a no-op — matches the Zig idempotence contract, no second-wipe hazard

It's wired into gossamer-groove.ipkg and registered as a groove-layer module in the decoupling guard (so it must stay a symlink and out of the shell package).

RSR Quality Checklist

Required

Tests pass (idris2: shell + groove typecheck green; 147/147 ABI tests)
Formatted; check-abi-decoupling.sh still shellcheck-clean
Linter clean (no new warnings)
No banned language patterns (Idris2 only)
No unsafe without // SAFETY: (n/a)
No banned functions — zero believe_me/sorry/postulate in the new module
SPDX header present on the new module
No secrets

As Applicable

Documentation updated (PROOF-NEEDS.md, CHANGELOG.md)
ABI/FFI validated — the proof models the real disconnect_typed semantics; decoupling + cleave gates pass

Testing

decoupling guard (GrooveResidue = groove-layer) ... PASS
cleave gate ....................................... PASS
shell typecheck ................................... GREEN (11)
groove typecheck (5 modules incl GrooveResidue) ... GREEN
ABI test suite .................................... 147 / 147

Part of #82. Remaining there: the coverage/codegen decision (awaiting your steer) and Ephapax let! linearity (blocked on the ephapax toolchain).

🤖 Generated with Claude Code

https://claude.ai/code/session_013Zg1kEsjSRpcf1wFBZyeNj

Generated by Claude Code

…esidue (gossamer#82) ResourceCleanup proves the generic teardown residue→0 for the plain groove `disconnect`, but not for the SOFT-specific privacy wipe done by `gossamer_groove_disconnect_typed` (main.zig): for a soft groove it zeroes the whole connection slot (`gc.* = .{ .target_id = 0, .groove_type = .hard }`), enforcing the SoftGroove "zero residual state" guarantee; a hard groove is only deactivated so its peer persists for auto-reconnect. New module Gossamer.ABI.GrooveResidue (groove package) models this and proves, constructively (zero believe_me): * softWipeZeroResidue — soft disconnect erases the peer identity (residue = 0) * softWipeFullyCleared — the whole slot is reset to the canonical zero * hardDisconnectRetainsPeer — hard disconnect keeps the peer (the two modes genuinely differ; not both trivially zero) * softDisconnectIdempotent — re-disconnecting is a no-op (matches the Zig idempotence contract; no second-wipe hazard) Closes the RC-7/RC-8 gap flagged in gossamer#82. Wired into gossamer-groove.ipkg and recognised as a groove-layer module by the decoupling guard. Verified with idris2 0.8.0: shell + groove packages typecheck green, both structure gates pass, 147/147 ABI tests pass. 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 marked this pull request as ready for review July 3, 2026 01:53

hyperpolymath merged commit 982c82b into main Jul 3, 2026
21 of 22 checks passed

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

This was referenced Jul 3, 2026

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

Open

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

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat(abi): prove soft-groove disconnect privacy (residue→0) — GrooveResidue (gossamer#82)#99

feat(abi): prove soft-groove disconnect privacy (residue→0) — GrooveResidue (gossamer#82)#99
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

The proof — Gossamer.ABI.GrooveResidue (groove package)

RSR Quality Checklist

Required

As Applicable

Testing

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

The proof — `Gossamer.ABI.GrooveResidue` (groove package)