hyperpolymath · hyperpolymath · Jul 1, 2026 · Jul 1, 2026
@@ -11,13 +11,19 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## [Unreleased]
 
 ### Changed
+- **Honest ABI decoupling from Groove; namespace symlinks restored (gossamer#95)**: the formal ABI now separates the webview **shell** from the **Groove** inter-service protocol at every level, fixing two root causes at source and adding gates so they cannot silently recur. Verified with `idris2 0.8.0` (Chez) end-to-end — both packages `--typecheck` green and the 147-test ABI suite passes.
+  - **Duplication → single source of truth.** `src/interface/Gossamer/ABI/<M>.idr` were committed as byte-identical *copies* of `src/interface/abi/<M>.idr` (the symlinks from `#42` had been materialised into regular files), so every module lived twice and the two trees could drift while the `.ipkg` still claimed "symlinks map the namespace". Restored all 15 namespace entries to `120000` symlinks into the canonical `src/interface/abi/` tree — one physical copy per module, nothing to drift.
+  - **Conflation → one-way layering.** The shell package `gossamer-abi.ipkg` bundled the Groove protocol proofs, and shell modules imported `Gossamer.ABI.Groove`. Those imports in `ResourceCleanup` and `IPCDispatch` were **vestigial** (their `TGroove`/`CmdGroove*` only use shell types) and were removed; `HandleLinearity`'s genuine groove use (`grooveValid`, `LinearGroove`, `allocateGroove`, `consumeForDisconnect`) was **extracted** into the new groove-layer module `Gossamer.ABI.GrooveLinearity`, which instantiates the shell's *generic* `LinearHandle` for `GrooveHandle`. The shell now type-checks without Idris2 ever compiling `Groove`. No proof was deleted — every module moved, none dropped.
+- **`gossamer-abi.ipkg` is now the groove-agnostic shell** (11 modules): `Types`, `Layout`, `Foreign`, `IPCDispatch`, `HandleLinearity`, `WindowStateMachine`, `LayoutStability`, `IPCIntegrity`, `PanelIsolation`, `ResourceCleanup`, `AndroidComponents`. `abi-check` (Justfile) and the ABI Typecheck Gate now build both packages and run the decoupling guard first.
 - **Frontend IPC binding migrated ReScript → AffineScript** (`@gossamer/api`, standards#252): the published package is now the AffineScript binding in `bindings/affinescript/`, type-checked with `affinescript check` and compiled to a standalone Deno-ESM module via `deno task build` (`affinescript compile --deno-esm`). ReScript is banned estate-wide; this completes gossamer's migration.
 - **Repository `LICENSE` corrected to `MPL-2.0`**: the top-level licence declared `AGPL-3.0-or-later` while all 394 source files and the `.ipkg` manifest are MPL-2.0 (gossamer is a sole-owner repo). Brought into line — the governance licence-consistency gate is now green.
 
 ### Removed
 - **`bindings/rescript/` retired** (`Gossamer.res`, `rescript.json`, package manifest) — superseded by the AffineScript binding above.
 
 ### Added
+- **`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.
 - **Android — `gossamer-android-services` companion: four shim base classes + real JNI (Phase 5, #71)**: Grows the Android target from "a WebView in an Activity" into a first-class mobile shell hosting the non-UI components, on the critical path for neurophone#97 (migrating a banned-Kotlin Android app onto gossamer). Owner-signed-off subclass model (issue #71).
   - `src/interface/ffi/src/jni.zig` (new) — a REAL JNI binding in pure Zig: models the `JNINativeInterface`/`JNIInvokeInterface` tables (ordinal-indexed), uses the `...A`-variant calls (no C varargs across the boundary), caches the `JavaVM` for thread attach, uses global refs, and reads `float[]` sensor samples via `Get/ReleaseFloatArrayElements`. The previous bridge declared `extern fn jni_*` symbols defined nowhere, so it could never link.
   - **Four abstract Java base classes** under `android/gossamer-android-services/src/main/java/io/gossamer/` that downstream apps EXTEND with ~5-20 lines (lifecycle methods are `final`): `services/GossamerForegroundService` (Service + SensorEventListener), `services/GossamerBootReceiver` (BroadcastReceiver), `services/GossamerAppWidgetProvider` (AppWidgetProvider), and the existing `GossamerActivity` extended with an `onIntentReceived` hook. gossamer owns every JNI call.

@@ -27,7 +27,9 @@ just test-zig-bench
 
 ## Configuration Files
 
-- **gossamer-abi.ipkg / gossamer-abi-tests.ipkg** — Idris2 ABI package and its test runner
+- **gossamer-abi.ipkg** — Idris2 formal ABI for the webview shell (groove-agnostic)
+- **gossamer-groove.ipkg** — Idris2 proofs for the Groove protocol (depends on gossamer-abi)
+- **gossamer-abi-tests.ipkg** — the ABI test runner
 - **flake.nix** — Nix development environment (fallback to guix.scm)
 - **guix.scm** — Primary Guix package definition for reproducible dev env
 - **gossamer.conf.json** — Runtime config: window size, IPC protocol, CSP, capabilities, sandbox

@@ -41,10 +41,15 @@ check-affine:
 check-example name:
     {{ephapax}} check examples/{{name}}/main.eph --mode linear -v
 
-# Type-check the formal ABI proof package (idris2 0.8.0). This is a
+# Type-check the formal ABI proof packages (idris2 0.8.0). This is a
 # REQUIRED gate, not optional: the ABI modules silently bit-rot otherwise.
+# Guards the shell/groove decoupling (gossamer#95), then type-checks the
+# groove-agnostic shell package and the groove package that depends on it.
 abi-check:
+    ./scripts/check-abi-decoupling.sh
     idris2 --typecheck gossamer-abi.ipkg
+    idris2 --install   gossamer-abi.ipkg
+    idris2 --typecheck gossamer-groove.ipkg
 
 # Build the Gossamer CLI (links libgossamer)
 build-cli: build-ffi

@@ -5,7 +5,8 @@
 - `src/interface/abi/Foreign.idr` — FFI declarations
 - `src/interface/abi/Layout.idr` — Memory layout definitions
 - `src/interface/abi/Groove.idr` — Groove protocol type definitions
-- `src/interface/abi/HandleLinearity.idr` — Handle lifecycle and uniqueness proofs
+- `src/interface/abi/GrooveLinearity.idr` — Groove-handle linearity (instantiates the shell's generic `LinearHandle` for `GrooveHandle`) ✅ NEW (gossamer#95)
+- `src/interface/abi/HandleLinearity.idr` — Handle lifecycle and uniqueness proofs (groove-agnostic)
 - `src/interface/abi/IPCIntegrity.idr` — IPC message integrity proofs
 - `src/interface/abi/PanelIsolation.idr` — Panel isolation proofs
 - `src/interface/abi/CapabilityAuthenticity.idr` — Capability authenticity proofs
@@ -14,7 +15,7 @@
 - `src/interface/abi/ResourceCleanup.idr` — Resource cleanup on teardown proofs ✅
 - `src/interface/abi/WindowStateMachine.idr` — Window state machine correctness (GS1) ✅ NEW 2026-04-11
 - `src/interface/abi/IPCDispatch.idr` — IPC handler type safety, 25 handlers (GS2) ✅ NEW 2026-04-11
-- **All 13 ABI modules above are now wired into `gossamer-abi.ipkg` and pass `idris2 0.8.0 --typecheck` cleanly** (2026-05-20, `standards#131` close-out). Prior to `gossamer#22` / `#36` / `#40` / `#41`, several modules were excluded from the ipkg and had never been built — their PROOF-NEEDS ✅ markers reflected an unverified posture; build is now the oracle.
+- **All 15 ABI modules above build green and pass `idris2 0.8.0 --typecheck` cleanly**, now split across two de-conflated packages (`gossamer#95`): the groove-agnostic **shell** `gossamer-abi.ipkg` (11 modules) and the **groove** `gossamer-groove.ipkg` (4: `Groove`, `GrooveLinearity`, `CapabilityAuthenticity`, `GrooveTermination`), which *depends on* the shell. The dependency points one way only — no shell module imports a groove module. The canonical sources live in `src/interface/abi/`; `src/interface/Gossamer/ABI/<M>.idr` are symlinks (a single source of truth, no drift). `scripts/check-abi-decoupling.sh` gates both invariants in CI. Prior to `gossamer#22` / `#36` / `#40` / `#41`, several modules were excluded from the ipkg and had never been built — their PROOF-NEEDS ✅ markers reflected an unverified posture; build is now the oracle.
 - **One class-J axiom**: `Gossamer.ABI.PanelIsolation.stringNotEqCommut` — sanctioned principled assumption over the Idris2 backend primitive `prim__eq_String` (content-symmetry on every supported backend; cannot be derived inside Idris2). `%unsafe`-annotated, `believe_me ()`-bodied, documented at the use site. Same trust posture as boj-server's `Boj.SafetyLemmas.charEqSym` and four sibling axioms over String / Char primitives. See "Class-J axioms (trusted base)" section below.
 - No other `believe_me`, `sorry`, `postulate`, or `assert_total` in the ABI layer.
 - Zig FFI layer in `src/interface/ffi/`

@@ -173,13 +173,17 @@ Gossamer’s ABI is written in Idris2 with the proof obligations audited
 in `PROOF-NEEDS.md`. Headline posture (as of `standards#131` close-out,
 2026-05-20):
 
-- **All 13 ABI proof modules build green.** `gossamer-abi.ipkg` `idris2`
-  `0.8.0` `--typecheck` passes 13/13 with `%default` `total`. Modules:
-  `Types`, `Layout`, `Foreign`, `Groove`, `CapabilityAuthenticity`,
-  `IPCDispatch`, `HandleLinearity`, `WindowStateMachine`,
-  `GrooveTermination`, `LayoutStability`, `IPCIntegrity`,
-  `PanelIsolation`, `ResourceCleanup`. Discharge ledger in
-  `PROOF-NEEDS.md`.
+- **All 15 ABI proof modules build green, across two de-conflated
+  packages** (`gossamer#95`). `idris2` `0.8.0` `--typecheck` passes with
+  `%default` `total`.
+  - **Shell** — `gossamer-abi.ipkg` (11, groove-agnostic): `Types`,
+    `Layout`, `Foreign`, `IPCDispatch`, `HandleLinearity`,
+    `WindowStateMachine`, `LayoutStability`, `IPCIntegrity`,
+    `PanelIsolation`, `ResourceCleanup`, `AndroidComponents`.
+  - **Groove** — `gossamer-groove.ipkg` (4, depends on the shell):
+    `Groove`, `GrooveLinearity`, `CapabilityAuthenticity`,
+    `GrooveTermination`. No shell module imports a groove module; the
+    dependency points one way only. Discharge ledger in `PROOF-NEEDS.md`.
 
 <!-- -->
 

@@ -15,24 +15,25 @@ version = 0.1.0
 
 authors = "Jonathan D.A. Jewell"
 
-brief = "Formally verified ABI for the Gossamer webview shell and Groove protocol"
-
--- Source files live in src/interface/abi/ but declare module Gossamer.ABI.*
--- Symlinks in src/interface/Gossamer/ABI/ map the Idris2 module namespace
--- to the physical file locations.
+brief = "Formally verified ABI for the Gossamer webview shell (groove-agnostic)"
+
+-- The canonical source files live in src/interface/abi/ and declare module
+-- Gossamer.ABI.*  Idris2 requires the on-disk path to match the module name,
+-- so src/interface/Gossamer/ABI/<M>.idr is a SYMLINK to ../../abi/<M>.idr —
+-- a single source of truth, no duplicated copies to drift.
+-- The groove protocol layer (Groove, GrooveTermination, CapabilityAuthenticity,
+-- GrooveLinearity) is de-conflated into its own package, gossamer-groove.ipkg,
+-- which depends on this one. No module listed here imports a groove module.
 sourcedir = "src/interface"
 
 depends = base
 
 modules = Gossamer.ABI.Types
         , Gossamer.ABI.Layout
         , Gossamer.ABI.Foreign
-        , Gossamer.ABI.Groove
-        , Gossamer.ABI.CapabilityAuthenticity
         , Gossamer.ABI.IPCDispatch
         , Gossamer.ABI.HandleLinearity
         , Gossamer.ABI.WindowStateMachine
-        , Gossamer.ABI.GrooveTermination
         , Gossamer.ABI.LayoutStability
         , Gossamer.ABI.IPCIntegrity
         , Gossamer.ABI.PanelIsolation
@@ -41,7 +42,6 @@ modules = Gossamer.ABI.Types
 
 -- All formerly-deferred ABI proof modules from gossamer#22's OWED list
 -- are now wired and `idris2 --typecheck` green:
---   * GrooveTermination  — discharged in gossamer#36 (MERGED)
 --   * LayoutStability    — discharged in gossamer#40 (MERGED)
 --   * IPCIntegrity       — discharged in gossamer#40 (MERGED)
 --   * PanelIsolation     — discharged in this branch via a sanctioned
@@ -51,3 +51,4 @@ modules = Gossamer.ABI.Types
 --                           posture as boj-server's `Boj.SafetyLemmas.*`.
 --   * ResourceCleanup    — discharged in this branch (missing `Data.DPair`
 --                           import + lowercase `exists` → `Exists`).
+-- GrooveTermination (gossamer#36) now lives in gossamer-groove.ipkg.
@@ -0,0 +1,43 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- Gossamer Groove — Idris2 package for the Groove inter-service protocol proofs.
+--
+-- De-conflated from the shell ABI (gossamer-abi.ipkg): Groove is a separate
+-- concern (type-safe capability discovery between services), so its proofs live
+-- in their own package that DEPENDS ON the shell, never the other way round.
+-- This layering is enforced: no gossamer-abi module imports a groove module.
+--
+-- The canonical sources live in src/interface/abi/ and declare module
+-- Gossamer.ABI.*  ; src/interface/Gossamer/ABI/<M>.idr symlinks to them so the
+-- on-disk path matches the module name (Idris2's requirement).
+--
+-- Build the shell first, then this package:
+--   idris2 --install   gossamer-abi.ipkg
+--   idris2 --typecheck gossamer-groove.ipkg
+
+package gossamer-groove
+
+version = 0.1.0
+
+authors = "Jonathan D.A. Jewell"
+
+brief = "Formally verified proofs for the Groove inter-service discovery protocol"
+
+sourcedir = "src/interface"
+
+depends = base
+        , gossamer-abi
+
+modules = Gossamer.ABI.Groove
+        , Gossamer.ABI.GrooveLinearity
+        , Gossamer.ABI.CapabilityAuthenticity
+        , Gossamer.ABI.GrooveTermination
+
+-- Groove-protocol proof modules relocated here from the shell (gossamer#95):
+--   * Groove                — capability types, manifests, handshake state machine
+--   * GrooveLinearity       — groove-handle linearity (instantiates the shell's
+--                             generic LinearHandle for GrooveHandle)
+--   * CapabilityAuthenticity — no phantom capabilities; attenuation soundness
+--   * GrooveTermination     — handshake termination + no-privilege-escalation
+--                             (discharged in gossamer#36, MERGED)