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

[hyperpolymath]

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

• 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.
• Linter is clean — shellcheck scripts/check-eph-linearity.sh clean.
• No banned language patterns — Ephapax + bash + YAML only; no TypeScript, npm/bun, Go, or Python.
• No unsafe blocks without // SAFETY: comments — none introduced.
• No banned functions (believe_me, unsafeCoerce, Obj.magic, Admitted, sorry) — none in the .eph layer.
• SPDX license headers present on all new/modified source files — MPL-2.0 on every .eph, the script, and the workflow.
• No secrets, credentials, or .env files included.

As Applicable

• Documentation updated for user-facing changes — PROOF-NEEDS.md.
• CHANGELOG or release notes updated.
• 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.ai/code/session_013Zg1kEsjSRpcf1wFBZyeNj

---

Generated by Claude Code