fix(abi): de-conflate Groove from the shell + restore namespace symlinks (gossamer#95)

[hyperpolymath]

Summary

Resolves the root cause behind gossamer#95 ("restore: honest ABI decoupling from groove") — fundamentally and at source, rather than as a merge-conflict patch. Two structural defects made the ABI dishonest and fragile; both are fixed and then gated so they cannot silently recur. Everything is verified with the real toolchain (idris2 0.8.0, Chez Scheme, built to match abi-typecheck.yml): both packages --typecheck green and the 147-test ABI suite passes.

This is an alternative, clean-branch resolution of the same intent as #95 (which is currently dirty/conflicted against main). Unlike #95 it deletes no proofs — every module is preserved, one is added.

Root cause 1 — duplication (the "honest ABI" part)

src/interface/Gossamer/ABI/<M>.idr had been committed as byte-identical regular-file copies of the canonical src/interface/abi/<M>.idr. The 120000 symlinks introduced in #42 were materialised into files at some point, so every ABI module lived twice — the two trees could drift while gossamer-abi.ipkg still claimed "symlinks map the namespace to the physical files". Fix: restored all 15 namespace entries to 120000 symlinks into the canonical abi/ tree. One physical copy per module; nothing to drift.

Root cause 2 — conflation (the "decoupling from groove" part)

gossamer-abi.ipkg bundled the Groove inter-service protocol proofs into the webview shell, and shell modules imported Gossamer.ABI.Groove.

• The imports in ResourceCleanup and IPCDispatch were vestigial — their TGroove/CmdGroove* only use shell types (HandleToken is defined in HandleLinearity, not Groove). Removed.
• HandleLinearity's genuine groove use (grooveValid, LinearGroove, allocateGroove, consumeForDisconnect) was extracted into a 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. Layering points one way only: Groove depends on the shell, never the reverse.

Changes

• gossamer-abi.ipkg — groove-agnostic shell (11 modules): Types, Layout, Foreign, IPCDispatch, HandleLinearity, WindowStateMachine, LayoutStability, IPCIntegrity, PanelIsolation, ResourceCleanup, AndroidComponents.
• gossamer-groove.ipkg (new) — Groove protocol proofs (4 modules): Groove, GrooveLinearity, CapabilityAuthenticity, GrooveTermination; depends = base, gossamer-abi.
• src/interface/abi/GrooveLinearity.idr (new) — the extracted groove-handle linearity; zero believe_me, %default total.
• src/interface/abi/{HandleLinearity,IPCDispatch,ResourceCleanup}.idr — decoupled from Gossamer.ABI.Groove.
• src/interface/Gossamer/ABI/*.idr — restored to symlinks (100644 → 120000).
• scripts/check-abi-decoupling.sh (new) — fast, toolchain-free structural guard: fails if a namespace file is a materialised copy, if a shell module re-imports a groove module, or if the two .ipkgs stop partitioning the modules. Shellcheck-clean; proven to fail on both regressions and pass on the fixed tree.
• .github/workflows/abi-typecheck.yml — new abi-structure guard job (seconds, gates before the ~15-min build) + typecheck both packages.
• Justfile abi-check — runs the guard and both typechecks.
• Docs — README.md, PROOF-NEEDS.md, GETTING-STARTED.md, CHANGELOG.md.

RSR Quality Checklist

Required

• Tests pass (gossamer-abi-tests: 147 passed, 0 failed, idris2 0.8.0)
• Code is formatted (matches house style; scripts/*.sh shellcheck-clean)
• Linter is clean (no new warnings; only pre-existing benign IPCIntegrity shadowing notes)
• No banned language patterns (Idris2 / Bash / YAML / Markdown only)
• No unsafe blocks without // SAFETY: comments (none added)
• No banned functions (believe_me, unsafeCoerce, Obj.magic, Admitted, sorry) — new module has none; the one sanctioned class-J axiom in PanelIsolation is untouched
• SPDX license headers present on all new/modified source files
• No secrets, credentials, or .env files included

As Applicable

• Documentation updated for user-facing changes
• CHANGELOG updated
• ABI/FFI changes validated (src/interface/abi/ self-consistent; src/interface/ffi/ untouched)
• .machine_readable/STATE.a2ml (no state change required)

Testing

Idris2 v0.8.0 built from source with Chez Scheme (identical to abi-typecheck.yml). Clean-room run of every gate:

GATE 1/5: structural decoupling guard ......... PASSED
GATE 2/5: typecheck shell (gossamer-abi.ipkg) . GREEN (11 modules)
GATE 3/5: install shell ....................... installed
GATE 4/5: typecheck groove (gossamer-groove) .. GREEN (4 modules)
GATE 5/5: build + run ABI test suite .......... TOTAL: 147 passed, 0 failed

Guard negative-tested in both directions: injecting import Gossamer.ABI.Groove into a shell module fails Check 2; an un-staged symlink (mode 100644) fails Check 1; the correct tree passes.

🤖 Generated with Claude Code

https://claude.ai/code/session_013Zg1kEsjSRpcf1wFBZyeNj

---

Generated by Claude Code