hyperpolymath · hyperpolymath · Jul 3, 2026 · Jul 3, 2026
@@ -22,6 +22,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - **`bindings/rescript/` retired** (`Gossamer.res`, `rescript.json`, package manifest) — superseded by the AffineScript binding above.
 
 ### Added
+- **`Gossamer.ABI.GrooveResidue` — soft-groove disconnect privacy proof (gossamer#82)**: a new module in the groove package that models `gossamer_groove_disconnect_typed` and proves the `SoftGroove` privacy guarantee `ResourceCleanup`'s plain `disconnect` did not cover: disconnecting a soft groove **erases the peer identity** (`softWipeZeroResidue`: residue = 0), clears the whole slot, retains the peer for a *hard* groove (`hardDisconnectRetainsPeer` — proving the two modes genuinely differ), and is idempotent. Closes the `RC-7`/`RC-8` gap. Zero `believe_me`; `idris2 0.8.0 --typecheck` green.
 - **`scripts/check-abi-ffi-cleave.sh` — the ABI↔FFI cleave gate (gossamer#82)**: `idris2 --typecheck` cannot see whether a `%foreign "C:sym, libgossamer"` resolves to a real Zig export (that linkage is only checked at link time), which is how the "phantom template" (8 declared symbols with no Zig definition) went unnoticed. This fast, toolchain-free gate — wired into the ABI Typecheck Gate ahead of the Idris2 build, and into `just abi-check` — **hard-fails on any phantom `%foreign`** and **reports coverage** of the real C surface (currently **29 / 130** `gossamer_*` exports declared; the 101 uncovered are the tracked expansion work in gossamer#82). Shellcheck-clean; proven to fail on an injected phantom and pass on the current tree. Together with the honest `Foreign.idr` (gossamer#95), the phantom-template class is now closed and cannot silently return.
 - **`gossamer-groove.ipkg` — the Groove protocol proofs in their own package (gossamer#95)**: 4 modules — `Groove` (capability types, manifests, handshake state machine), `GrooveLinearity` (groove-handle linearity over the shell's generic `LinearHandle`), `CapabilityAuthenticity` (no phantom capabilities; attenuation soundness), and `GrooveTermination` (handshake terminates in ≤4 steps, no privilege escalation). Declares `depends = base, gossamer-abi`, so the layering is enforced by the build: Groove depends on the shell, never the reverse.
 - **`scripts/check-abi-decoupling.sh` — structural guard for the shell/groove split (gossamer#95)**: a fast, toolchain-free check (wired into the ABI Typecheck Gate ahead of the ~15-min Idris2 build, and into `just abi-check`) that fails if any `Gossamer/ABI/*.idr` is a materialised copy instead of a symlink, or if a shell module re-imports a groove module, or if the two `.ipkg` manifests stop partitioning the modules. Shellcheck-clean; proven to fail on both regressions and pass on the fixed tree.

@@ -27,6 +27,7 @@
 - ~~**Panel isolation**~~: ✅ Proved in PanelIsolation.idr — state tokens are tag-exclusive, channels are tag-exclusive, registry isolation
 - ~~**Memory layout ABI stability**~~: ✅ Proved in LayoutStability.idr — field prefix preservation, result code stability, handle size stability, append-only rule
 - ~~**Resource cleanup on teardown**~~: ✅ Proved in ResourceCleanup.idr — every resource has cleanup action, LIFO order, panel teardown, shell teardown total
+- ~~**Soft-groove disconnect privacy (residue→0)**~~: ✅ Proved in `GrooveResidue.idr` (`gossamer#82`, groove package) — models `gossamer_groove_disconnect_typed` and proves the `SoftGroove` privacy guarantee: disconnecting a soft groove erases the peer identity (`softWipeZeroResidue`: residue = 0) and clears the whole slot, while a hard groove retains its peer (`hardDisconnectRetainsPeer` — the distinction is real), and the wipe is idempotent. Closes the `RC-7`/`RC-8` gap ResourceCleanup's plain `disconnect` did not cover. Zero `believe_me`.
 - ~~**Window state machine correctness (GS1)**~~: ✅ Proved in WindowStateMachine.idr — Closed is terminal, borrow/consuming classification, all states reachable from Created, borrow preserves Active, consuming leads to Closed (2026-04-11)
 - ~~**IPC handler type safety (GS2)**~~: ✅ Proved in IPCDispatch.idr — all 25 handlers have declared input/output types, dispatch is total, capability-guarded vs plain commands classified, distinctness witnesses (2026-04-11)
 - **Extension loading safety**: Prove `.eph` module loading validates signatures before execution (BLOCKED: requires Ephapax module system, see NEXT-STEPS.md P6)

@@ -31,6 +31,7 @@ depends = base
 
 modules = Gossamer.ABI.Groove
         , Gossamer.ABI.GrooveLinearity
+        , Gossamer.ABI.GrooveResidue
         , Gossamer.ABI.CapabilityAuthenticity
         , Gossamer.ABI.GrooveTermination
 

@@ -28,7 +28,7 @@ GROOVE_IPKG="gossamer-groove.ipkg"
 
 # The Groove-layer modules (canonical basenames). Everything else under
 # $ABI_DIR is shell and must stay groove-agnostic.
-GROOVE_MODULES=(Groove GrooveTermination GrooveLinearity CapabilityAuthenticity)
+GROOVE_MODULES=(Groove GrooveTermination GrooveLinearity GrooveResidue CapabilityAuthenticity)
 
 fail=0
 err() { printf '::error::%s\n' "$1" >&2; fail=1; }

@@ -0,0 +1 @@
+../../abi/GrooveResidue.idr
@@ -0,0 +1,99 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Soft-Groove Disconnect Residue Proof (groove layer)
+|||
+||| The FFI `gossamer_groove_disconnect_typed` (main.zig) enforces the
+||| `SoftGroove` privacy guarantee — "Transient integration — disconnects
+||| cleanly, zero residual state" (`Gossamer.ABI.Types.GrooveType`) — by
+||| zeroing the *entire* connection slot for a soft groove
+||| (`gc.* = .{ .target_id = 0, .groove_type = .hard }`), whereas a hard groove
+||| is merely deactivated so its peer identity persists for auto-reconnect.
+|||
+||| `Gossamer.ABI.ResourceCleanup` proves the generic teardown residue→0 for the
+||| plain `disconnect` descent. This module proves the SOFT-specific, stronger
+||| property that the *typed* disconnect leaves ZERO residue: the sensitive peer
+||| identity is provably erased, not merely marked inactive. This closes the
+||| `RC-7`/`RC-8` gap flagged in gossamer#82.
+|||
+||| Zero believe_me. All proofs are constructive.
+
+module Gossamer.ABI.GrooveResidue
+
+import Gossamer.ABI.Types
+
+%default total
+
+--------------------------------------------------------------------------------
+-- Connection slot (mirrors the Zig `GrooveConnection` record)
+--------------------------------------------------------------------------------
+
+||| The runtime state of one groove connection slot, mirroring the Zig
+||| `{ target_id : u32, groove_type : GrooveType, active : bool }`.
+public export
+record GrooveConn where
+  constructor MkConn
+  target : Bits32     -- peer identity — the sensitive residue
+  kind   : GrooveType
+  active : Bool
+
+||| The sensitive residue held in a slot: the raw peer identity still stored.
+||| The `SoftGroove` privacy guarantee requires this to be 0 after disconnect
+||| (a soft peer must not be recoverable from a freed slot). It is defined as
+||| the raw stored `target` — not gated on `active` — precisely because the
+||| privacy property is about erasure of the identity, not liveness.
+public export
+residue : GrooveConn -> Bits32
+residue c = target c
+
+--------------------------------------------------------------------------------
+-- The typed disconnect (`gossamer_groove_disconnect_typed`)
+--------------------------------------------------------------------------------
+
+||| Model of `gossamer_groove_disconnect_typed`:
+|||   * soft groove → wipe the whole slot (`target := 0`), matching the Zig
+|||     `gc.* = .{ .target_id = 0, .groove_type = .hard }` — the privacy wipe;
+|||   * hard groove → deactivate only, keeping `target` for auto-reconnect.
+public export
+softDisconnect : GrooveConn -> GrooveConn
+softDisconnect (MkConn _ SoftGroove _) = MkConn 0 HardGroove False
+softDisconnect (MkConn t HardGroove _) = MkConn t HardGroove False
+
+--------------------------------------------------------------------------------
+-- Proofs
+--------------------------------------------------------------------------------
+
+||| PRIVACY GUARANTEE: disconnecting a soft groove erases the peer identity —
+||| the residue is provably 0. This is the property `ResourceCleanup`'s plain
+||| `disconnect` did not establish for the typed soft wipe.
+public export
+softWipeZeroResidue : (c : GrooveConn) -> kind c = SoftGroove -> residue (softDisconnect c) = 0
+softWipeZeroResidue (MkConn _ SoftGroove _) Refl = Refl
+softWipeZeroResidue (MkConn _ HardGroove _) Refl impossible
+
+||| The soft wipe clears the *whole* slot, not just the identity: the result is
+||| the canonical zeroed connection (matching the Zig struct reset exactly).
+public export
+softWipeFullyCleared : (c : GrooveConn) -> kind c = SoftGroove
+                    -> softDisconnect c = MkConn 0 HardGroove False
+softWipeFullyCleared (MkConn _ SoftGroove _) Refl = Refl
+softWipeFullyCleared (MkConn _ HardGroove _) Refl impossible
+
+||| CONTRAST (the distinction is real): disconnecting a HARD groove retains the
+||| peer identity — residue is unchanged — which is the intended persistence for
+||| auto-reconnecting integrations. Together with `softWipeZeroResidue` this shows
+||| the two disconnect modes are genuinely different, not both trivially zero.
+public export
+hardDisconnectRetainsPeer : (c : GrooveConn) -> kind c = HardGroove
+                         -> residue (softDisconnect c) = target c
+hardDisconnectRetainsPeer (MkConn _ HardGroove _) Refl = Refl
+hardDisconnectRetainsPeer (MkConn _ SoftGroove _) Refl impossible
+
+||| IDEMPOTENCE: the typed disconnect is idempotent (matches the Zig
+||| "Idempotent" contract) — re-disconnecting an already-disconnected slot is a
+||| no-op, so there is no second-wipe hazard.
+public export
+softDisconnectIdempotent : (c : GrooveConn)
+                        -> softDisconnect (softDisconnect c) = softDisconnect c
+softDisconnectIdempotent (MkConn _ SoftGroove _) = Refl
+softDisconnectIdempotent (MkConn _ HardGroove _) = Refl