diff --git a/CHANGELOG.md b/CHANGELOG.md index 8192957..a864458 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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. diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 10927d1..8044af5 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -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) diff --git a/gossamer-groove.ipkg b/gossamer-groove.ipkg index bbbe9a4..d21f28d 100644 --- a/gossamer-groove.ipkg +++ b/gossamer-groove.ipkg @@ -31,6 +31,7 @@ depends = base modules = Gossamer.ABI.Groove , Gossamer.ABI.GrooveLinearity + , Gossamer.ABI.GrooveResidue , Gossamer.ABI.CapabilityAuthenticity , Gossamer.ABI.GrooveTermination diff --git a/scripts/check-abi-decoupling.sh b/scripts/check-abi-decoupling.sh index ac24d5a..4116783 100755 --- a/scripts/check-abi-decoupling.sh +++ b/scripts/check-abi-decoupling.sh @@ -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; } diff --git a/src/interface/Gossamer/ABI/GrooveResidue.idr b/src/interface/Gossamer/ABI/GrooveResidue.idr new file mode 120000 index 0000000..b1c6cc9 --- /dev/null +++ b/src/interface/Gossamer/ABI/GrooveResidue.idr @@ -0,0 +1 @@ +../../abi/GrooveResidue.idr \ No newline at end of file diff --git a/src/interface/abi/GrooveResidue.idr b/src/interface/abi/GrooveResidue.idr new file mode 100644 index 0000000..9149e0d --- /dev/null +++ b/src/interface/abi/GrooveResidue.idr @@ -0,0 +1,99 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| 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