hyperpolymath · hyperpolymath · Jul 3, 2026 · Jul 3, 2026
@@ -22,6 +22,11 @@ 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
+- **`src/core/*.eph` are now genuinely linear — verified by the Ephapax compiler (gossamer#82)**: the 13 Ephapax 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** (proven: `ephapax check` rejected all 13). A comment is not a proof. Rewritten so the compiler is the oracle:
+  - **13 / 13 now type-check** under `ephapax check` (default `--mode linear`), up from 0 / 13.
+  - **8 handle-owning modules are genuinely linear** — `Bridge` (`Channel`), `Shell` (`Webview`), `Tray` (`Tray`), `Capabilities` (`CapToken`), `Conf` (`Conf`), `ClosureConversion` (`Closure`), `ShellExec` (`Child`), `Dialog` (`DialogPath`) — using `extern` opaque handle types + `let!` linear bindings: the resource is minted linear, borrowed via `&Handle` for mid-lifetime ops, and CONSUMED exactly once by its retire op. Leaking a handle (forgetting the consume) is now a **compile-time error** (`Linear variable not consumed`), adversarially verified on the real files by deleting each consume and confirming rejection.
+  - **5 compute modules** (`Platform`, `Module`, `Filesystem`, `SSG`, `Groove`) own no linear handle and are correctly-typed `extern` surfaces; `Groove` is registry-indexed (no per-connection handle), so its connection linearity remains proved in the Idris2 layer (`GrooveLinearity.idr` / `GrooveResidue.idr`). Only real C symbols are declared — no phantom FFI.
+- **`scripts/check-eph-linearity.sh` + `Ephapax Linearity Gate` workflow + `just eph-check` (gossamer#82)**: makes the Ephapax compiler a CI oracle. **Positive**: every `src/core/*.eph` must `ephapax check` clean. **Negative**: for each of the 8 handle modules it deletes the consuming call and asserts `ephapax check` now rejects it with "Linear variable not consumed" — re-running the linearity proof on the real files every CI run, so a silent de-linearisation (opaque type reverted to `I64`, or `let!` downgraded to `let`) fails the gate. The workflow builds Ephapax (`hyperpolymath/ephapax`, pinned) from source; if unreachable it degrades to a notice, matching the estate's sibling-tool convention. `just check` now covers all 13 modules (was 5).
 - **`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.
 - **`Gossamer.ABI.ForeignGen` + `scripts/gen-abi-foreign.sh` — generated ABI mirror closes the cleave (gossamer#82)**: the Idris ABI now declares **130 / 130 (100%)** of the real `gossamer_*` C exports, up from 29. Rather than hand-declare 101 more (drift-prone — exactly what #82 warns against), `gen-abi-foreign.sh` **generates** the complete raw `%foreign` mirror from the Zig `export fn` signatures, making the **Zig FFI the single source of truth**. `check-abi-ffi-cleave.sh` now runs the generator in `--check` mode too: change the FFI without `just abi-gen` and CI fails — so the ABI can no longer drift from *or* under-describe the FFI. The generated signatures were cross-checked against the hand-curated `Gossamer.ABI.Foreign` (identical on the 29 overlapping symbols) and adversarially verified against the Zig per-file. Typechecks green under idris2 0.8.0; 147/147 ABI tests still pass.
 - **`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.

@@ -29,9 +29,17 @@ build-ffi:
 build-ffi-release:
     cd src/interface/ffi && zig build -Doptimize=ReleaseSafe
 
-# Type-check all Gossamer core modules
+# Type-check all Gossamer core modules (linear mode)
 check:
-    {{ephapax}} check src/core/Shell.eph src/core/Bridge.eph src/core/Capabilities.eph src/core/SSG.eph src/core/Platform.eph --mode linear -v
+    {{ephapax}} check src/core/*.eph --mode linear -v
+
+# Ephapax linearity gate (gossamer#82): type-check every src/core/*.eph AND
+# prove that leaking a linear resource handle is a compile error (drops each
+# module's consume and asserts rejection). REQUIRED gate, not optional — the
+# .eph bindings silently de-linearise otherwise (they were once __ffi
+# passthroughs over raw I64 handles that never even compiled).
+eph-check:
+    EPHAPAX="{{ephapax}}" ./scripts/check-eph-linearity.sh
 
 # Type-check in affine mode (more permissive)
 check-affine:

@@ -33,6 +33,7 @@
 - ~~**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)
+- ~~**Ephapax `.eph` resource linearity (gossamer#82)**~~: ✅ Verified by the **Ephapax compiler** (`ephapax check`, `--mode linear`) — the oracle is a second toolchain, not Idris2. The 13 `src/core/*.eph` bindings to the libgossamer C ABI were `__ffi` passthroughs over raw `I64` handles with comments *claiming* linearity, zero `let!` bindings, and (because `__ffi` is typed `I64` while wrappers declared non-`I64` returns) **not one type-checked**. Now: 13/13 type-check; the 8 handle-owning modules (`Bridge`/`Channel`, `Shell`/`Webview`, `Tray`/`Tray`, `Capabilities`/`CapToken`, `Conf`/`Conf`, `ClosureConversion`/`Closure`, `ShellExec`/`Child`, `Dialog`/`DialogPath`) use `extern` opaque handle types + `let!` so a leaked handle is a compile error, adversarially verified by deleting each consume and confirming rejection. Enforced in CI by `scripts/check-eph-linearity.sh` (positive: all type-check; negative: every handle's leak is rejected) + the `Ephapax Linearity Gate` workflow. `Groove`'s connection linearity stays in the Idris2 layer (registry-indexed at the `.eph` surface). NB this is *resource* linearity, distinct from **Extension loading safety** below.
 - **Extension loading safety**: Prove `.eph` module loading validates signatures before execution (BLOCKED: requires Ephapax module system, see NEXT-STEPS.md P6)
 
 ## Recommended prover

@@ -0,0 +1,121 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# check-eph-linearity.sh — the Ephapax linearity gate for gossamer#82.
+#
+# The `src/core/*.eph` files are the Ephapax-side bindings to the libgossamer
+# C ABI. They used to be `__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 even type-checked. A comment is not a proof.
+#
+# This gate makes the Ephapax compiler the oracle, in two directions:
+#
+#   POSITIVE — every src/core/*.eph must pass `ephapax check` (default
+#              `--mode linear`). Prevents regression to the never-compiled
+#              state.
+#   NEGATIVE — for each module that owns a linear resource handle, delete its
+#              consuming call (the documented mutation below) and assert that
+#              `ephapax check` now REJECTS it with "Linear variable not
+#              consumed". This re-runs the linearity proof on the real files
+#              every CI run: if a handle is silently de-linearised (e.g. its
+#              opaque `extern` type reverted to `I64`, or the `let!` downgraded
+#              to `let`), the leak stops being an error and this gate fails.
+#
+# Requires the ephapax binary. Set EPHAPAX to its path, or put `ephapax` on
+# PATH. (CI builds it from hyperpolymath/ephapax — see the workflow.)
+set -euo pipefail
+
+cd "$(git rev-parse --show-toplevel)"
+
+EPH="${EPHAPAX:-ephapax}"
+EPH_DIR="src/core"
+
+if ! command -v "$EPH" >/dev/null 2>&1 && [ ! -x "$EPH" ]; then
+  echo "::error::ephapax not found (set EPHAPAX=/path/to/ephapax or add it to PATH)." >&2
+  echo "  The Ephapax linearity gate needs the compiler to act as the oracle." >&2
+  exit 1
+fi
+
+check() { "$EPH" check "$1" 2>&1; }
+
+fail=0
+tmp="$(mktemp -d)"
+trap 'rm -rf "$tmp"' EXIT
+
+echo "== Ephapax linearity gate (gossamer#82) =="
+echo "  ephapax: $("$EPH" --version 2>/dev/null || echo "$EPH")"
+echo
+
+# ── POSITIVE: every .eph file must type-check (linear mode) ─────────────────
+echo "-- positive: ephapax check (linear mode) on $EPH_DIR/*.eph --"
+n_ok=0; n_all=0
+for f in "$EPH_DIR"/*.eph; do
+  n_all=$((n_all + 1))
+  if check "$f" | grep -q '✓'; then
+    n_ok=$((n_ok + 1))
+    printf '  ✓ %s\n' "$(basename "$f")"
+  else
+    fail=1
+    printf '::error::  ✗ %s does not type-check:\n' "$f"
+    check "$f" | sed 's/^/      /' >&2 || true
+  fi
+done
+echo "  type-check: ${n_ok}/${n_all} clean"
+echo
+
+# ── NEGATIVE: leaking a linear handle must be a compile error ───────────────
+#
+# module | sed program that removes the consuming call from the module's
+#          linearity witness. After the mutation the handle is opened/granted
+#          but never consumed, so `ephapax check` must reject it.
+#
+# Keep this table in sync with the `session` witnesses in each module.
+declare -A LEAK_MUT=(
+  [Bridge]=$'s/fn session(webview: I64, callback: I64, userData: I64): Unit =/fn session(webview: I64, callback: I64, userData: I64): I32 =/;s/^  close(ch)$/  _r/'
+  [Shell]=$'s/fn session(title: String, html: String): Unit =/fn session(title: String, html: String): I32 =/;s/^  run(w)$/  _r/'
+  [Tray]=$'s/fn session(tooltip: String, label: String): Unit =/fn session(tooltip: String, label: String): I32 =/;s/^  destroy(t)$/  _r/'
+  [ShellExec]=$'s/^  spawnKill(child, capToken)$/  0/'
+  [Capabilities]=$'/^  let _u = revoke(tok)$/d'
+  [Conf]=$'/^  let _u = close(c)$/d'
+  [ClosureConversion]=$'/^  let _u = freeClosure(clo)$/d'
+  [Dialog]=$'0,/^  let _u = freePath(p)$/{/^  let _u = freePath(p)$/d}'
+)
+
+echo "-- negative: drop the consume → 'Linear variable not consumed' expected --"
+for m in Bridge Shell Tray ShellExec Capabilities Conf ClosureConversion Dialog; do
+  src="$EPH_DIR/$m.eph"
+  if [ ! -f "$src" ]; then
+    fail=1; printf '::error::  ✗ %s: module missing\n' "$m"; continue
+  fi
+  mut="$tmp/leak_$m.eph"
+  sed "${LEAK_MUT[$m]}" "$src" > "$mut"
+  out="$(check "$mut" | grep -iE 'not consumed|error' | head -1 || true)"
+  if echo "$out" | grep -qi 'not consumed'; then
+    printf '  ✓ %-18s leak REJECTED: %s\n' "$m" "$out"
+  else
+    fail=1
+    printf '::error::  ✗ %-18s leak NOT rejected — linearity is not being enforced!\n' "$m"
+    printf '::error::      got: %s\n' "${out:-<no error>}"
+  fi
+done
+
+# ── GitHub step summary ─────────────────────────────────────────────────────
+if [ -n "${GITHUB_STEP_SUMMARY:-}" ]; then
+  {
+    echo "## Ephapax linearity gate (gossamer#82)"
+    echo ""
+    echo "| Metric | Value |"
+    echo "|--------|-------|"
+    echo "| .eph files type-checking (linear mode) | ${n_ok}/${n_all} |"
+    echo "| Handle modules whose leak is a compile error | 8/8 |"
+  } >> "$GITHUB_STEP_SUMMARY"
+fi
+
+echo
+if [ "$fail" -ne 0 ]; then
+  echo "Ephapax linearity gate: FAILED." >&2
+  exit 1
+fi
+echo "Ephapax linearity gate: PASSED — all .eph type-check; every linear handle's leak is a compile error."