From 056a49410ddd7f9dc2232dd78af2676d3ddf8fc9 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 3 Jul 2026 03:28:35 +0000 Subject: [PATCH] =?UTF-8?q?feat(eph):=20make=20src/core/*.eph=20genuinely?= =?UTF-8?q?=20linear=20=E2=80=94=20verified=20by=20ephapax=20(gossamer#82)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. `ephapax check` rejected all 13. A comment is not a proof. Rewritten so the Ephapax compiler is the oracle: - 13/13 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 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 at the .eph layer; its connection linearity stays proved in Idris2 (GrooveLinearity / GrooveResidue). Only real C symbols are declared — no phantom FFI. Enforcement: - scripts/check-eph-linearity.sh — positive (all .eph type-check) + negative (drop each handle's consume, assert rejection) gate; shellcheck-clean. - .github/workflows/eph-linearity.yml — builds ephapax from source as the oracle, degrades to a notice if unreachable (estate sibling-tool pattern). - just eph-check added; just check now covers all 13 modules (was 5). Docs: CHANGELOG + PROOF-NEEDS updated. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_013Zg1kEsjSRpcf1wFBZyeNj --- .github/workflows/eph-linearity.yml | 79 +++++++++++++ CHANGELOG.md | 5 + Justfile | 12 +- PROOF-NEEDS.md | 1 + scripts/check-eph-linearity.sh | 121 +++++++++++++++++++ src/core/Bridge.eph | 91 +++++++++++---- src/core/Capabilities.eph | 124 +++++++++++--------- src/core/ClosureConversion.eph | 120 ++++++++++--------- src/core/Conf.eph | 104 +++++++++-------- src/core/Dialog.eph | 154 ++++++++++++------------ src/core/Filesystem.eph | 89 ++++++-------- src/core/Groove.eph | 154 +++++++++++------------- src/core/Module.eph | 72 +++++------- src/core/Platform.eph | 69 ++++++----- src/core/SSG.eph | 161 +++++++------------------ src/core/Shell.eph | 175 +++++++++++++--------------- src/core/ShellExec.eph | 89 ++++++++------ src/core/Tray.eph | 122 +++++++++---------- 18 files changed, 947 insertions(+), 795 deletions(-) create mode 100644 .github/workflows/eph-linearity.yml create mode 100755 scripts/check-eph-linearity.sh diff --git a/.github/workflows/eph-linearity.yml b/.github/workflows/eph-linearity.yml new file mode 100644 index 0000000..247fd31 --- /dev/null +++ b/.github/workflows/eph-linearity.yml @@ -0,0 +1,79 @@ +# SPDX-License-Identifier: MPL-2.0 +# Ephapax Linearity Gate — machine-checks that the src/core/*.eph bindings to +# the libgossamer C ABI genuinely type-check under Ephapax's linear discipline, +# and that leaking a linear resource handle is a compile error. Refs +# hyperpolymath/gossamer#82. +# +# Ephapax is a sibling estate repo (hyperpolymath/ephapax); this gate builds it +# from source to use its `check` subcommand as the oracle. If Ephapax cannot be +# cloned/built (e.g. token scope), the gate degrades to a notice rather than a +# hard failure — matching the estate's sibling-tool convention (see the Hypatia +# job in static-analysis-gate.yml). The gate is authoritative whenever the +# compiler is reachable, and `just eph-check` always runs it locally. +# +# Path-filtered and concurrency-guarded so it does not add load on unrelated +# changes. +name: Ephapax Linearity Gate + +on: + pull_request: + branches: ['**'] + paths: + - 'src/core/**/*.eph' + - 'scripts/check-eph-linearity.sh' + - '.github/workflows/eph-linearity.yml' + push: + branches: [main, master] + paths: + - 'src/core/**/*.eph' + - 'scripts/check-eph-linearity.sh' + - '.github/workflows/eph-linearity.yml' + +permissions: + contents: read + +concurrency: + group: eph-linearity-${{ github.ref }} + cancel-in-progress: true + +env: + REPO_OWNER: ${{ github.repository_owner }} + # Pinned Ephapax revision validated against these .eph files. Bump when the + # oracle is upgraded (a repo/org variable can override without editing here). + EPHAPAX_REF: ${{ vars.EPHAPAX_REF || '55d6a24cebf3e6fb4dc59212c4550e0df0544f52' }} + +jobs: + eph-linearity: + name: ephapax check + linearity (src/core/*.eph) + runs-on: ubuntu-latest + steps: + - name: Checkout repository + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + + - name: Clone and build Ephapax (the linear-type oracle) + id: build + continue-on-error: true + run: | + set -uo pipefail + git clone "https://github.com/${REPO_OWNER}/ephapax.git" "$RUNNER_TEMP/ephapax" 2>/dev/null || true + if [ ! -f "$RUNNER_TEMP/ephapax/Cargo.toml" ]; then + echo "::notice::Ephapax repo not reachable — skipping the linearity gate." + echo "ready=false" >> "$GITHUB_OUTPUT" + exit 0 + fi + cd "$RUNNER_TEMP/ephapax" + git checkout "$EPHAPAX_REF" 2>/dev/null || echo "::notice::EPHAPAX_REF $EPHAPAX_REF not found; using default branch." + # Rust stable is pre-installed on ubuntu-latest; debug build is fast enough. + if cargo build --bin ephapax; then + echo "bin=$RUNNER_TEMP/ephapax/target/debug/ephapax" >> "$GITHUB_OUTPUT" + echo "ready=true" >> "$GITHUB_OUTPUT" + else + echo "::notice::Ephapax failed to build — skipping the linearity gate." + echo "ready=false" >> "$GITHUB_OUTPUT" + fi + + - name: Run the Ephapax linearity gate + if: steps.build.outputs.ready == 'true' + env: + EPHAPAX: ${{ steps.build.outputs.bin }} + run: ./scripts/check-eph-linearity.sh diff --git a/CHANGELOG.md b/CHANGELOG.md index 6ecbc56..0b590fd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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. diff --git a/Justfile b/Justfile index a07c925..95f76e3 100644 --- a/Justfile +++ b/Justfile @@ -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: diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 137fb25..71b6f30 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -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 diff --git a/scripts/check-eph-linearity.sh b/scripts/check-eph-linearity.sh new file mode 100755 index 0000000..93bc0c5 --- /dev/null +++ b/scripts/check-eph-linearity.sh @@ -0,0 +1,121 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# 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:-}" + 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." diff --git a/src/core/Bridge.eph b/src/core/Bridge.eph index 9a4b485..7c7cf35 100644 --- a/src/core/Bridge.eph +++ b/src/core/Bridge.eph @@ -3,24 +3,73 @@ // // Gossamer.Bridge — Typed IPC channel between frontend (JS) and backend (Ephapax). // -// The IPC channel is a LINEAR resource: -// - open returns a linear channel handle (must be closed) -// - bind borrows the channel (returns it back) -// - close CONSUMES the channel handle - -// Open a typed IPC channel on the webview. -// FFI: gossamer_channel_open(webview_handle) -> channel_handle -fn open(webviewHandle: I64): I64 = - __ffi("gossamer_channel_open", webviewHandle) - -// Bind a named command handler to the IPC channel. Borrows the channel. -// FFI: gossamer_channel_bind(channel, name, callback, user_data) -> result -// user_data is passed through to callback on each invocation — enables -// language bindings (Rust, etc.) to pass closure context through the C ABI. -fn bind(channelHandle: I64, name: String, callback: I64, userData: I64): I32 = - __ffi("gossamer_channel_bind", channelHandle, name, callback, userData) - -// Close the IPC channel. CONSUMES the channel handle. -// FFI: gossamer_channel_close(channel) -> void -fn close(channelHandle: I64): () = - __ffi("gossamer_channel_close", channelHandle) +// The IPC channel is a GENUINELY LINEAR resource, enforced by the Ephapax +// type checker (`ephapax check`, default `--mode linear`): +// - `open` mints a linear `Channel` handle (an opaque host handle); +// - `bind` BORROWS the channel (`&Channel`) — it does not consume it, +// so the same channel can be bound many times, and returns the +// C result code; +// - `close` CONSUMES the channel handle (linear move; nothing returned). +// +// Because `Channel` is linear, a code path that opens a channel and forgets +// to `close` it is a COMPILE-TIME type error ("Linear variable `ch` not +// consumed"), not a silently leaked handle at runtime. The `session` driver +// below exercises exactly that lifecycle so `ephapax check` verifies it. +// +// This is the shape #82 asked for: the earlier version of this file was a +// set of `__ffi` passthroughs over raw `I64` handles with a comment CLAIMING +// linearity and zero `let!` bindings — and it did not even type-check +// (I32/I64 mismatch). Handles that are plain `I64` carry no linear +// obligation, so nothing stopped a leak. The opaque `extern` handle type + +// `let!` binding is what actually makes the checker enforce it. + +module gossamer/core/bridge + +// ── C ABI surface (single source of truth: src/interface/ffi/src/*.zig) ──── +// +// The `extern "gossamer"` block names the real libgossamer C symbols. `Channel` +// is an opaque linear handle (desugars to a host handle; the Ephapax program +// can only pass it around, never forge or duplicate it). +extern "gossamer" { + // Opaque, linear IPC channel handle. Minted by open, retired by close. + type Channel + + // gossamer_channel_open(webview_handle) -> channel_handle + fn gossamer_channel_open(webviewHandle: I64): Channel + + // gossamer_channel_bind(channel, name, callback, user_data) -> result + // Borrows the channel (&Channel): binding does not retire the handle. + // user_data is passed through to callback on each invocation — enables + // language bindings (Rust, etc.) to pass closure context through the C ABI. + fn gossamer_channel_bind(channelHandle: &Channel, name: String, callback: I64, userData: I64): I32 + + // gossamer_channel_close(channel) -> void. Linear: CONSUMES the channel. + fn gossamer_channel_close(channelHandle: Channel): Unit +} + +// ── Idiomatic wrappers (what other Ephapax modules import) ───────────────── + +// Open a typed IPC channel on the webview. Returns a linear channel handle +// that MUST eventually be `close`d. +pub fn open(webviewHandle: I64): Channel = + gossamer_channel_open(webviewHandle) + +// Bind a named command handler to the IPC channel. Borrows the channel and +// returns the C result code, so it may be called repeatedly on one channel. +pub fn bind(channelHandle: &Channel, name: String, callback: I64, userData: I64): I32 = + gossamer_channel_bind(channelHandle, name, callback, userData) + +// Close the IPC channel. Consumes the channel handle. +pub fn close(channelHandle: Channel): Unit = + gossamer_channel_close(channelHandle) + +// ── Linearity witness ────────────────────────────────────────────────────── +// +// A minimal driver that opens a channel, binds a handler (borrow), then +// closes it (consume). `ephapax check` accepts this because `ch` is consumed +// exactly once. Delete the `close(ch)` line and the checker rejects the file +// — that rejection is the machine-checked proof that the handle cannot leak. +fn session(webview: I64, callback: I64, userData: I64): Unit = + let! ch = open(webview) + let _r = bind(&ch, "cmd", callback, userData) + close(ch) diff --git a/src/core/Capabilities.eph b/src/core/Capabilities.eph index f8945ab..e300fb0 100644 --- a/src/core/Capabilities.eph +++ b/src/core/Capabilities.eph @@ -3,66 +3,82 @@ // // Gossamer.Capabilities — Linear capability tokens for permission enforcement. // -// Capability tokens are LINEAR resources: -// - grant returns a linear token (must be revoked) -// - check borrows the token (returns it back) -// - revoke CONSUMES the token +// A capability token is a GENUINELY LINEAR resource, enforced by `ephapax +// check` (default `--mode linear`): +// - `grant` mints a linear `CapToken`; +// - `check` and `resourceKind` BORROW the token (`&CapToken`); +// - `revoke` CONSUMES the token — no further use is possible. +// +// Because `CapToken` is linear, granting a capability and never revoking it is +// a compile-time type error, so a leaked (never-revoked) permission cannot +// slip through. The C ABI token is an `i64`; consumer modules (Filesystem, +// ShellExec, Conf) receive it by value as `I64` — this module owns the linear +// grant/revoke discipline. +// +// The earlier version declared the RESOURCE_* set as top-level `let X: I32 = 0` +// (not valid v2 syntax — top level is fn/type/data/extern) and declared +// `: I32` / `: ()` returns over `__ffi(...)` (typed `I64`), so it never +// type-checked. The RESOURCE_* constants are now nullary functions. + +module gossamer/core/capabilities + +// ── Resource-kind constants (matching Types.idr ResourceKind) ────────────── +pub fn resourceFilesystem(): I32 = 0 +pub fn resourceNetwork(): I32 = 1 +pub fn resourceShell(): I32 = 2 +pub fn resourceClipboard(): I32 = 3 +pub fn resourceNotification(): I32 = 4 +pub fn resourceTray(): I32 = 5 +pub fn resourceGroove(): I32 = 6 + +// ── libgossamer C ABI (source of truth: src/interface/ffi/src/*.zig) ─────── +extern "gossamer" { + // Opaque, linear capability token. + type CapToken + + // gossamer_cap_grant(resource_kind) -> token + fn gossamer_cap_grant(resourceKind: I32): CapToken + + // Borrow ops — inspect the token without retiring it. + fn gossamer_cap_check(token: &CapToken): I32 + fn gossamer_cap_resource_kind(token: &CapToken): I32 -// Resource kind constants matching Types.idr ResourceKind constructors. -// Used as the resourceKind parameter to grant(). -let RESOURCE_FILESYSTEM: I32 = 0 -let RESOURCE_NETWORK: I32 = 1 -let RESOURCE_SHELL: I32 = 2 -let RESOURCE_CLIPBOARD: I32 = 3 -let RESOURCE_NOTIFICATION: I32 = 4 -let RESOURCE_TRAY: I32 = 5 -let RESOURCE_GROOVE: I32 = 6 + // Consuming op — retire the token (adds it to the revocation set). + fn gossamer_cap_revoke(token: CapToken): Unit -// Grant a capability token for the given resource kind. -// Use the RESOURCE_* constants above for the kind parameter. -// Returns a unique token (linear — must be revoked), or 0 on failure. -// FFI: gossamer_cap_grant(resource_kind) -> token -fn grant(resourceKind: I32): I64 = - __ffi("gossamer_cap_grant", resourceKind) + // Handle-free registry configuration. + fn gossamer_cap_set_max(max: I32): I32 + fn gossamer_cap_get_max(): I32 + fn gossamer_set_max_inflight(max: I32): I32 + fn gossamer_get_max_inflight(): I32 +} -// Check a capability token before a gated operation. Borrows the token. -// Returns 0 (ok) if the token is active and not revoked, 10 (denied) otherwise. -// FFI: gossamer_cap_check(token) -> result (0=ok, 10=denied) -fn check(token: I64): I32 = - __ffi("gossamer_cap_check", token) +// ── Idiomatic wrappers (public API) ──────────────────────────────────────── -// Query the resource kind associated with a capability token. -// Returns the resource kind ordinal (0-5), or 0xFFFFFFFF if invalid. -// FFI: gossamer_cap_resource_kind(token) -> resource_kind -fn resourceKind(token: I64): I32 = - __ffi("gossamer_cap_resource_kind", token) +// Grant a capability token for the given resource kind (use the resource* +// helpers above). Returns a linear token that MUST be revoked. +pub fn grant(resourceKind: I32): CapToken = gossamer_cap_grant(resourceKind) -// Revoke a capability token. CONSUMES it — no further use possible. -// The token is added to a revocation set; future check() calls will fail. -// FFI: gossamer_cap_revoke(token) -> void -fn revoke(token: I64): () = - __ffi("gossamer_cap_revoke", token) +// Check a token before a gated operation. Borrows it. 0 = ok, 10 = denied. +pub fn check(token: &CapToken): I32 = gossamer_cap_check(token) -// Set the maximum number of active capability tokens. -// Default is 256. Increase for multi-panel apps with per-panel sandboxes. -// Maximum is 4096. Returns the actual limit after clamping. -// FFI: gossamer_cap_set_max(max) -> actual_max -fn setCapMax(max: I32): I32 = - __ffi("gossamer_cap_set_max", max) +// Query the resource kind bound to a token. Borrows it. +pub fn tokenResourceKind(token: &CapToken): I32 = gossamer_cap_resource_kind(token) -// Query the current maximum capability registry size. -// FFI: gossamer_cap_get_max() -> max -fn getCapMax(): I32 = - __ffi("gossamer_cap_get_max") +// Revoke a token. CONSUMES it. +pub fn revoke(token: CapToken): Unit = gossamer_cap_revoke(token) -// Set the maximum number of concurrent async IPC calls. -// Default is 256. Increase for high-concurrency apps. Maximum is 16384. -// Returns the actual limit after clamping. -// FFI: gossamer_set_max_inflight(max) -> actual_max -fn setMaxInflight(max: I32): I32 = - __ffi("gossamer_set_max_inflight", max) +pub fn setCapMax(max: I32): I32 = gossamer_cap_set_max(max) +pub fn getCapMax(): I32 = gossamer_cap_get_max() +pub fn setMaxInflight(max: I32): I32 = gossamer_set_max_inflight(max) +pub fn getMaxInflight(): I32 = gossamer_get_max_inflight() -// Query the current maximum inflight async IPC limit. -// FFI: gossamer_get_max_inflight() -> max -fn getMaxInflight(): I32 = - __ffi("gossamer_get_max_inflight") +// ── Linearity witness ────────────────────────────────────────────────────── +// Grant a token, check it (borrow), then revoke it (consume). Drop the +// `revoke(tok)` and `ephapax check` rejects the file: a granted capability +// cannot be silently retained. +fn session(): I32 = + let! tok = grant(resourceFilesystem()) + let r = check(&tok) + let _u = revoke(tok) + r diff --git a/src/core/ClosureConversion.eph b/src/core/ClosureConversion.eph index 39102c1..2c5fcf9 100644 --- a/src/core/ClosureConversion.eph +++ b/src/core/ClosureConversion.eph @@ -3,73 +3,71 @@ // // Gossamer.ClosureConversion — Closure representation and operations. // -// Closure conversion transforms functions with free variables into -// functions that take an explicit environment parameter. This is -// necessary for first-class functions in Ephapax since the Zig FFI -// layer uses C ABI calling conventions (no implicit captures). +// Closure conversion transforms functions with free variables into functions +// that take an explicit environment parameter — necessary for first-class +// functions over the C ABI (no implicit captures). A closure pairs a lifted +// function pointer with a heap-allocated environment holding the captures. // -// A closure is represented as a pair: -// (function_pointer: I64, environment_pointer: I64) +// A closure is a GENUINELY LINEAR resource, enforced by `ephapax check` +// (default `--mode linear`) — this is the "linear closures must be freed +// exactly once" rule the module documents, now actually type-checked: +// - `makeClosure` mints a linear `Closure` (folding in the env pointer); +// - `applyClosure` BORROWS the closure (`&Closure`); +// - `freeClosure` CONSUMES the closure and its environment. // -// The environment is a heap-allocated struct containing the captured -// variables. The function pointer points to a "lifted" version of the -// original function that takes the environment as its first argument. +// Because `Closure` is linear, building a closure and never freeing it is a +// compile-time type error. The raw environment pointer (allocClosureEnv / +// envStore / envLoad) stays `I64`: it is a construction-time scratch buffer +// that `makeClosure` takes ownership of. // -// Example transformation: -// -// let x = 42 -// let f = fn(y: I32): I32 = x + y // captures x -// -// Becomes: -// -// struct Env_f { x: I32 } -// fn f_lifted(env: *Env_f, y: I32): I32 = env.x + y -// let env = allocEnv({ x = 42 }) -// let f = makeClosure(f_lifted, env) -// -// Linear type interaction: -// Closures that capture linear resources must themselves be linear. -// The closure conversion pass tracks linearity of captured variables -// and marks the resulting closure as linear if any capture is linear. -// Linear closures must be applied exactly once (enforced by the type -// checker after conversion). +// The earlier version passed the closure as a plain `I64` and declared +// `: ()` returns over `__ffi(...)` (typed `I64`), so it never type-checked. + +module gossamer/core/closure_conversion + +// ── Ephapax runtime C ABI (closure support) ──────────────────────────────── +extern "gossamer" { + // Opaque, linear closure handle. + type Closure + + // ephapax_closure_make(fn_ptr, env_ptr) -> closure + fn ephapax_closure_make(fnPtr: I64, envPtr: I64): Closure + + // Borrow op — invoke the closure without retiring it. + fn ephapax_closure_apply(closure: &Closure, arg: I64): I64 + + // Consuming op — free the closure and its environment. + fn ephapax_closure_free(closure: Closure): Unit + + // Raw environment scratch buffer (folded into the closure by make). + fn ephapax_closure_alloc_env(sizeBytes: I32): I64 + fn ephapax_closure_env_store(envPtr: I64, offset: I32, value: I64): Unit + fn ephapax_closure_env_load(envPtr: I64, offset: I32): I64 +} -// Create a closure from a function pointer and environment pointer. -// The environment must have been allocated via allocClosureEnv. -// Returns an opaque closure handle. -// FFI: ephapax_closure_make(fn_ptr, env_ptr) -> closure -fn makeClosure(fnPtr: I64, envPtr: I64): I64 = - __ffi("ephapax_closure_make", fnPtr, envPtr) +// ── Idiomatic wrappers (public API) ──────────────────────────────────────── -// Apply a closure to an argument. -// Invokes the function pointer with (environment, argument). -// Returns the result of the function call. -// FFI: ephapax_closure_apply(closure, arg) -> result -fn applyClosure(closure: I64, arg: I64): I64 = - __ffi("ephapax_closure_apply", closure, arg) +// Create a closure from a function pointer and environment pointer. Returns a +// linear handle that MUST be freed. Takes ownership of envPtr. +pub fn makeClosure(fnPtr: I64, envPtr: I64): Closure = ephapax_closure_make(fnPtr, envPtr) -// Free a closure and its environment. -// Must be called exactly once for each closure created. -// For linear closures, the type system enforces this. -// FFI: ephapax_closure_free(closure) -> void -fn freeClosure(closure: I64): () = - __ffi("ephapax_closure_free", closure) +// Apply a closure to an argument. Borrows the closure. +pub fn applyClosure(closure: &Closure, arg: I64): I64 = ephapax_closure_apply(closure, arg) -// Allocate an environment struct for closure capture. -// size_bytes is the total size of the captured variables. -// Returns a pointer to the allocated environment. -// FFI: ephapax_closure_alloc_env(size_bytes) -> env_ptr -fn allocClosureEnv(sizeBytes: I32): I64 = - __ffi("ephapax_closure_alloc_env", sizeBytes) +// Free a closure and its environment. CONSUMES the closure. +pub fn freeClosure(closure: Closure): Unit = ephapax_closure_free(closure) -// Store a value into a closure environment at a given offset. -// Used during closure construction to populate captured variables. -// FFI: ephapax_closure_env_store(env_ptr, offset, value) -> void -fn envStore(envPtr: I64, offset: I32, value: I64): () = - __ffi("ephapax_closure_env_store", envPtr, offset, value) +pub fn allocClosureEnv(sizeBytes: I32): I64 = ephapax_closure_alloc_env(sizeBytes) +pub fn envStore(envPtr: I64, offset: I32, value: I64): Unit = ephapax_closure_env_store(envPtr, offset, value) +pub fn envLoad(envPtr: I64, offset: I32): I64 = ephapax_closure_env_load(envPtr, offset) -// Load a value from a closure environment at a given offset. -// Used inside lifted functions to access captured variables. -// FFI: ephapax_closure_env_load(env_ptr, offset) -> value -fn envLoad(envPtr: I64, offset: I32): I64 = - __ffi("ephapax_closure_env_load", envPtr, offset) +// ── Linearity witness ────────────────────────────────────────────────────── +// Allocate an environment, build a closure, apply it (borrow), then free it +// (consume). Drop `freeClosure(clo)` and `ephapax check` rejects the file: +// the closure cannot leak. +fn session(fnPtr: I64, arg: I64): I64 = + let env = allocClosureEnv(16) + let! clo = makeClosure(fnPtr, env) + let r = applyClosure(&clo, arg) + let _u = freeClosure(clo) + r diff --git a/src/core/Conf.eph b/src/core/Conf.eph index a406e41..4ed24c3 100644 --- a/src/core/Conf.eph +++ b/src/core/Conf.eph @@ -1,53 +1,63 @@ // SPDX-License-Identifier: MPL-2.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) // -// Gossamer.Conf — Read gossamer.conf.json via libgossamer's real JSON -// loader. Replaces the hand-rolled string-scan parser previously used -// by the native Zig CLI. +// Gossamer.Conf — Read gossamer.conf.json via libgossamer's real JSON loader. // -// All operations require a valid FileSystem capability token (kind=0) -// since loading the config reads from disk. Field lookups are dotted -// paths into the parsed tree: +// The parsed-config handle is a GENUINELY LINEAR resource, enforced by +// `ephapax check` (default `--mode linear`): +// - `load` mints a linear `Conf` handle (reading requires a FileSystem +// capability token, passed by value as `I64` — see Capabilities.eph); +// - the lookup ops (getString, getInt, getBool, has) BORROW the handle +// (`&Conf`); +// - `close` CONSUMES the handle, freeing the tree and every string that +// getString handed out (do not free those individually). // -// "productName" top-level string -// "build.devUrl" nested string -// "app.windows.0.width" nested int inside the first array element +// Because `Conf` is linear, loading a config and never closing it is a +// compile-time type error. Field lookups are dotted paths into the parsed +// tree ("productName", "build.devUrl", "app.windows.0.width"). // -// Strings returned by getString are owned by the Conf handle and freed -// by close — do not free them individually. - -// Load a JSON config file and return an opaque conf handle, or 0 on -// error (check Shell.lastError for details). Caller must pass the -// handle to close when done. -// FFI: gossamer_conf_load(path, cap_token) -> opaque_handle -fn load(path: String, capToken: I64): I64 = - __ffi("gossamer_conf_load", path, capToken) - -// Resolve a dotted path. Returns a null-terminated string pointer -// owned by the conf, or 0 if the path is missing or holds a non-string. -// FFI: gossamer_conf_get_string(conf, path) -> string_ptr -fn getString(conf: I64, path: String): I64 = - __ffi("gossamer_conf_get_string", conf, path) - -// Resolve a dotted path. Returns the integer value, or defaultValue if -// the path is missing or holds a non-numeric value. -// FFI: gossamer_conf_get_int(conf, path, default) -> i64 -fn getInt(conf: I64, path: String, defaultValue: I64): I64 = - __ffi("gossamer_conf_get_int", conf, path, defaultValue) - -// Resolve a dotted path. Returns 0 or 1, or defaultValue if the path -// is missing or holds a non-boolean value. -// FFI: gossamer_conf_get_bool(conf, path, default) -> i32 -fn getBool(conf: I64, path: String, defaultValue: I32): I32 = - __ffi("gossamer_conf_get_bool", conf, path, defaultValue) - -// Returns 1 if the path resolves to any value, 0 if missing. -// FFI: gossamer_conf_has(conf, path) -> i32 -fn has(conf: I64, path: String): I32 = - __ffi("gossamer_conf_has", conf, path) - -// Free a conf handle and all strings previously returned by getString. -// Safe to call with 0 (no-op). -// FFI: gossamer_conf_free(conf) -> void -fn close(conf: I64): I32 = - __ffi("gossamer_conf_free", conf) +// The earlier version passed the handle as a plain `I64` and declared +// `: I32` returns over `__ffi(...)` (typed `I64`), so it never type-checked. + +module gossamer/core/conf + +// ── libgossamer C ABI (source of truth: src/interface/ffi/src/*.zig) ─────── +extern "gossamer" { + // Opaque, linear parsed-config handle. + type Conf + + // gossamer_conf_load(path, cap_token) -> opaque_handle + fn gossamer_conf_load(path: String, capToken: I64): Conf + + // Borrow ops — resolve dotted paths without retiring the handle. + // getString returns a string pointer owned by the Conf (0 = missing). + fn gossamer_conf_get_string(conf: &Conf, path: String): I64 + fn gossamer_conf_get_int(conf: &Conf, path: String, defaultValue: I64): I64 + fn gossamer_conf_get_bool(conf: &Conf, path: String, defaultValue: I32): I32 + fn gossamer_conf_has(conf: &Conf, path: String): I32 + + // Consuming op — free the handle and every string it returned. + fn gossamer_conf_free(conf: Conf): Unit +} + +// ── Idiomatic wrappers (public API) ──────────────────────────────────────── + +// Load a JSON config file. Returns a linear handle that MUST be closed. +pub fn load(path: String, capToken: I64): Conf = gossamer_conf_load(path, capToken) + +pub fn getString(conf: &Conf, path: String): I64 = gossamer_conf_get_string(conf, path) +pub fn getInt(conf: &Conf, path: String, defaultValue: I64): I64 = gossamer_conf_get_int(conf, path, defaultValue) +pub fn getBool(conf: &Conf, path: String, defaultValue: I32): I32 = gossamer_conf_get_bool(conf, path, defaultValue) +pub fn has(conf: &Conf, path: String): I32 = gossamer_conf_has(conf, path) + +// Free the conf handle and all strings it returned. CONSUMES the handle. +pub fn close(conf: Conf): Unit = gossamer_conf_free(conf) + +// ── Linearity witness ────────────────────────────────────────────────────── +// Load a config, read a field (borrow), then close it (consume). Drop the +// `close(c)` and `ephapax check` rejects the file: the handle cannot leak. +fn session(path: String, capToken: I64): I64 = + let! c = load(path, capToken) + let v = getString(&c, "productName") + let _u = close(c) + v diff --git a/src/core/Dialog.eph b/src/core/Dialog.eph index 1159444..a59d700 100644 --- a/src/core/Dialog.eph +++ b/src/core/Dialog.eph @@ -3,103 +3,93 @@ // // Gossamer.Dialog — Native file dialog wrappers for Ephapax. // -// Provides safe, typed access to GTK file chooser dialogs via the Zig FFI. -// Each function returns a nullable result (0 = cancelled / error). +// A dialog result path is a GENUINELY LINEAR resource, enforced by `ephapax +// check` (default `--mode linear`): +// - the raw* openers mint a linear `DialogPath` (a heap C buffer; the null +// sentinel on cancel/error is carried as the same handle); +// - `readPath` BORROWS the handle (`&DialogPath`) to read the string; +// - `freePath` CONSUMES the handle (gossamer_dialog_free_path is a +// documented no-op on the null sentinel, so always-free is safe). // -// The path pointer returned by the FFI is a LINEAR resource: -// - It MUST be freed exactly once via gossamer_dialog_free_path. -// - The safe wrappers below handle this automatically, converting the -// raw pointer to an Ephapax String and freeing the C buffer. +// Because `DialogPath` is linear, opening a dialog and never freeing the +// returned buffer is a compile-time type error — no path buffer can leak. The +// high-level open/save/openDirectory/openMultiple wrappers each perform the +// open→read→free lifecycle in one linear-safe call and return the path string +// ("" = cancelled/error; openMultiple returns a newline-separated list). +// +// This drops the earlier `Option` / `List` return sugar: those +// generic types are not expressible in the current Ephapax v2 grammar, and the +// earlier file (which used them, plus `: I32` returns over `__ffi(...)` typed +// `I64`, plus an undefined `split`) never type-checked. Every symbol declared +// below is real — the gossamer_dialog_* C ABI plus the Idris2 RTS string +// reader idris2_getString the original relied on — so there is no phantom FFI. // // Filter format: "Name|ext1;ext2|Name2|ext3;ext4" // Example: "JSON files|*.json;*.yaml|All files|*" -// --------------------------------------------------------------------------- -// Raw FFI bindings (internal — use the safe wrappers below) -// --------------------------------------------------------------------------- +module gossamer/core/dialog + +// ── libgossamer C ABI (source of truth: src/interface/ffi/src/*.zig) ─────── +extern "gossamer" { + // Opaque, linear dialog-result path buffer. + type DialogPath -// Show a file open dialog (single file). -// FFI: gossamer_dialog_open(title, filters) -> path_ptr -fn rawOpen(title: String, filters: String): I64 = - __ffi("gossamer_dialog_open", title, filters) + // Openers → a path buffer (null sentinel on cancel/error). + fn gossamer_dialog_open(title: String, filters: String): DialogPath + fn gossamer_dialog_save(title: String, filters: String): DialogPath + fn gossamer_dialog_open_directory(title: String): DialogPath + fn gossamer_dialog_open_multiple(title: String, filters: String): DialogPath -// Show a file save dialog. -// FFI: gossamer_dialog_save(title, filters) -> path_ptr -fn rawSave(title: String, filters: String): I64 = - __ffi("gossamer_dialog_save", title, filters) + // Consuming op — free the buffer (no-op on the null sentinel). + fn gossamer_dialog_free_path(p: DialogPath): Unit +} -// Show a directory picker dialog. -// FFI: gossamer_dialog_open_directory(title) -> path_ptr -fn rawOpenDirectory(title: String): I64 = - __ffi("gossamer_dialog_open_directory", title) +// Idris2 RTS string reader — borrows the buffer, returns an Ephapax String +// ("" for the null sentinel). +extern "idris2" { + fn idris2_getString(p: &DialogPath): String +} -// Show a multi-file open dialog. -// FFI: gossamer_dialog_open_multiple(title, filters) -> path_ptr -fn rawOpenMultiple(title: String, filters: String): I64 = - __ffi("gossamer_dialog_open_multiple", title, filters) +// ── Raw layer (manual open → read → free control) ────────────────────────── -// Free a path string returned by a dialog function. -// FFI: gossamer_dialog_free_path(path_ptr) -> void -fn rawFreePath(pathPtr: I64): () = - __ffi("gossamer_dialog_free_path", pathPtr) +pub fn rawOpen(title: String, filters: String): DialogPath = gossamer_dialog_open(title, filters) +pub fn rawSave(title: String, filters: String): DialogPath = gossamer_dialog_save(title, filters) +pub fn rawOpenDirectory(title: String): DialogPath = gossamer_dialog_open_directory(title) +pub fn rawOpenMultiple(title: String, filters: String): DialogPath = gossamer_dialog_open_multiple(title, filters) -// Convert a C string pointer to an Ephapax String. -// FFI: idris2_getString(ptr) -> String -fn ptrToString(ptr: I64): String = - __ffi("idris2_getString", ptr) +// Read the path string from a buffer. Borrows the handle. +pub fn readPath(p: &DialogPath): String = idris2_getString(p) -// --------------------------------------------------------------------------- -// Safe wrappers — return Option, auto-free the C buffer -// --------------------------------------------------------------------------- +// Free a dialog path buffer. CONSUMES the handle. +pub fn freePath(p: DialogPath): Unit = gossamer_dialog_free_path(p) -// Show a file open dialog. -// Returns None if the user cancelled or an error occurred. +// ── Safe wrappers — open → read → free in one linear-safe call ───────────── // -// Example: -// match open("Open File", "JSON|*.json|All|*") { -// Some(path) => loadFile(path), -// None => log("User cancelled"), -// } -fn open(title: String, filters: String): Option = - let ptr = rawOpen(title, filters) in - if ptr == 0 then None - else - let path = ptrToString(ptr) in - let _ = rawFreePath(ptr) in - Some(path) +// Each returns the selected path as a String ("" = cancelled/error). Because +// the buffer is consumed by freePath on every path, none can leak. -// Show a file save dialog. -// Returns None if the user cancelled or an error occurred. -fn save(title: String, filters: String): Option = - let ptr = rawSave(title, filters) in - if ptr == 0 then None - else - let path = ptrToString(ptr) in - let _ = rawFreePath(ptr) in - Some(path) +pub fn open(title: String, filters: String): String = + let! p = rawOpen(title, filters) + let s = readPath(&p) + let _u = freePath(p) + s -// Show a directory picker dialog. -// Returns None if the user cancelled or an error occurred. -fn openDirectory(title: String): Option = - let ptr = rawOpenDirectory(title) in - if ptr == 0 then None - else - let path = ptrToString(ptr) in - let _ = rawFreePath(ptr) in - Some(path) +pub fn save(title: String, filters: String): String = + let! p = rawSave(title, filters) + let s = readPath(&p) + let _u = freePath(p) + s -// Show a multi-file open dialog. -// Returns a list of selected file paths (empty if cancelled). -// The paths are newline-separated in the raw FFI result. -fn openMultiple(title: String, filters: String): List = - let ptr = rawOpenMultiple(title, filters) in - if ptr == 0 then [] - else - let combined = ptrToString(ptr) in - let _ = rawFreePath(ptr) in - splitLines(combined) +pub fn openDirectory(title: String): String = + let! p = rawOpenDirectory(title) + let s = readPath(&p) + let _u = freePath(p) + s -// Split a string on newline characters into a list. -fn splitLines(s: String): List = - if s == "" then [] - else split(s, '\n') +// Newline-separated list of selected paths ("" if cancelled). Callers split +// on '\n'. +pub fn openMultiple(title: String, filters: String): String = + let! p = rawOpenMultiple(title, filters) + let s = readPath(&p) + let _u = freePath(p) + s diff --git a/src/core/Filesystem.eph b/src/core/Filesystem.eph index 1e1349a..f64d01d 100644 --- a/src/core/Filesystem.eph +++ b/src/core/Filesystem.eph @@ -3,61 +3,44 @@ // // Gossamer.Filesystem — File I/O operations guarded by capability tokens. // -// All filesystem operations require a valid RESOURCE_FILESYSTEM capability -// token (from Capabilities.grant). The token is borrowed (not consumed) by -// read/write operations. +// Every operation requires a valid RESOURCE_FILESYSTEM capability token, +// passed by value as `I64` and BORROWED (never consumed) by the call — its +// linear grant/revoke discipline lives in Capabilities.eph. No handle is +// created here, so these functions own no linear resource of their own. // -// These are IPC commands dispatched through the Gossamer bridge, not direct -// file I/O from the webview. The Zig FFI backend performs the actual I/O -// after validating the capability token. - -// Read a text file and return its contents as a string pointer. -// Requires a valid filesystem capability token. -// Returns 0 on error (check Shell.lastError for details). -// FFI: gossamer_fs_read_text(path, cap_token) -> string_ptr -fn readText(path: String, capToken: I64): I64 = - __ffi("gossamer_fs_read_text", path, capToken) - -// Write text to a file. Creates the file if it doesn't exist. -// Requires a valid filesystem capability token with write scope. -// Returns 0 (ok) or non-zero error code. -// FFI: gossamer_fs_write_text(path, contents, cap_token) -> result -fn writeText(path: String, contents: String, capToken: I64): I32 = - __ffi("gossamer_fs_write_text", path, contents, capToken) - -// Check if a file or directory exists. -// Requires a valid filesystem capability token. -// Returns 1 (true) or 0 (false). -// FFI: gossamer_fs_exists(path, cap_token) -> bool -fn exists(path: String, capToken: I64): I32 = - __ffi("gossamer_fs_exists", path, capToken) +// These are IPC commands dispatched through the Gossamer bridge; the Zig FFI +// backend performs the actual I/O after validating the token. +// +// The earlier version declared `: I32` returns over `__ffi(...)`, which is +// typed `I64`, so it never type-checked. The `extern` block carries the real +// return types (I64 string pointers, I32 result codes). -// List directory contents. Returns a JSON array of filenames as a -// string pointer, or 0 on error. -// Requires a valid filesystem capability token. -// FFI: gossamer_fs_list_dir(path, cap_token) -> json_ptr -fn listDir(path: String, capToken: I64): I64 = - __ffi("gossamer_fs_list_dir", path, capToken) +module gossamer/core/filesystem -// Delete a file. Requires a valid filesystem capability token with -// write scope. -// Returns 0 (ok) or non-zero error code. -// FFI: gossamer_fs_remove(path, cap_token) -> result -fn remove(path: String, capToken: I64): I32 = - __ffi("gossamer_fs_remove", path, capToken) +// ── libgossamer C ABI (source of truth: src/interface/ffi/src/*.zig) ─────── +extern "gossamer" { + // Read a text file → string pointer (0 = error). + fn gossamer_fs_read_text(path: String, capToken: I64): I64 + // Write text (creates the file) → 0 ok / non-zero error. + fn gossamer_fs_write_text(path: String, contents: String, capToken: I64): I32 + // Existence check → 1 / 0. + fn gossamer_fs_exists(path: String, capToken: I64): I32 + // List a directory → JSON-array string pointer (0 = error). + fn gossamer_fs_list_dir(path: String, capToken: I64): I64 + // Delete a file → 0 ok / non-zero error. + fn gossamer_fs_remove(path: String, capToken: I64): I32 + // mkdir -p (idempotent) → 0 ok / non-zero error. + fn gossamer_fs_mkdir_p(path: String, capToken: I64): I32 + // Copy src → dst (dst parent must exist) → 0 ok / non-zero error. + fn gossamer_fs_copy_file(src: String, dst: String, capToken: I64): I32 +} -// Create a directory and any missing parent directories (mkdir -p). -// Idempotent — returns 0 when the directory already exists. -// Requires a valid filesystem capability token with write scope. -// Returns 0 (ok) or non-zero error code. -// FFI: gossamer_fs_mkdir_p(path, cap_token) -> result -fn mkdirP(path: String, capToken: I64): I32 = - __ffi("gossamer_fs_mkdir_p", path, capToken) +// ── Idiomatic wrappers (public API) ──────────────────────────────────────── -// Copy a file from src to dst, overwriting dst if it exists. The parent -// directory of dst must already exist — call mkdirP first if needed. -// Requires a valid filesystem capability token with write scope. -// Returns 0 (ok) or non-zero error code. -// FFI: gossamer_fs_copy_file(src, dst, cap_token) -> result -fn copyFile(src: String, dst: String, capToken: I64): I32 = - __ffi("gossamer_fs_copy_file", src, dst, capToken) +pub fn readText(path: String, capToken: I64): I64 = gossamer_fs_read_text(path, capToken) +pub fn writeText(path: String, contents: String, capToken: I64): I32 = gossamer_fs_write_text(path, contents, capToken) +pub fn exists(path: String, capToken: I64): I32 = gossamer_fs_exists(path, capToken) +pub fn listDir(path: String, capToken: I64): I64 = gossamer_fs_list_dir(path, capToken) +pub fn remove(path: String, capToken: I64): I32 = gossamer_fs_remove(path, capToken) +pub fn mkdirP(path: String, capToken: I64): I32 = gossamer_fs_mkdir_p(path, capToken) +pub fn copyFile(src: String, dst: String, capToken: I64): I32 = gossamer_fs_copy_file(src, dst, capToken) diff --git a/src/core/Groove.eph b/src/core/Groove.eph index e46df1d..b8bcd3e 100644 --- a/src/core/Groove.eph +++ b/src/core/Groove.eph @@ -3,21 +3,24 @@ // // Gossamer.Groove — Lightweight capability discovery for composable integration. // -// A "groove" is a bidirectional capability interface between two systems. -// Each system works standalone but enhances the other when co-present. -// Grooves are panel-optional: they work headless, but CAN power PanLL panels. +// A "groove" is a bidirectional capability interface between two systems. Each +// works standalone but enhances the other when co-present. Grooves are +// panel-optional: they work headless but CAN power PanLL panels. // -// The Idris2 ABI (Groove.idr) provides formal proofs of: -// - Safe connect: IsSubset required offered => GrooveHandle -// - Safe disconnect: linear GrooveHandle => must be consumed exactly once -// - Safe compose: GrooveCompat a b => GroovePair a b +// LINEARITY NOTE: this .eph surface is REGISTRY-INDEXED — every operation +// addresses a groove by its `targetId: I32` into a global connection table; +// there is no per-connection handle to thread, so there is no linear resource +// to enforce at this layer. The linear discipline for a groove *connection* +// (connect yields a linear `GrooveHandle` that must be consumed exactly once +// by disconnect) is proved in the Idris2 ABI layer — see +// src/interface/abi/Groove.idr and GrooveLinearity.idr, machine-checked by +// `idris2 --typecheck` (and the soft/hard-disconnect residue proofs in +// GrooveResidue.idr). This module is the flat IPC command surface over that. // -// Discovery flow: -// 1. Gossamer probes well-known ports for groove manifests -// 2. Services respond with JSON declaring offered/consumed capabilities -// 3. Gossamer verifies compatibility via Idris2 subset proofs -// 4. Matching grooves are activated and made available via IPC -// 5. Frontend JS queries gossamer.groove_*() for active grooves +// The earlier version declared the GROOVE_* set as top-level `let X: I32 = 0` +// (not valid v2 syntax) and `: I32` / `: ()` returns over `__ffi(...)` (typed +// `I64`), so it never type-checked. The constants are now nullary functions +// and the real return types live on the `extern` block. // // Well-known groove targets (port → service → primary capability): // 6473 → Burble → voice, text, presence, spatial-audio, TTS, STT @@ -27,85 +30,62 @@ // 7800 → rpa → workflow // 8000 → PanLL → panel-ui // 8080 → VeriSimDB → octad-storage, drift-detection, temporal-versioning -// 8080 → gitbot → bot-orchestration (shares VeriSimDB port — TODO: assign unique) // 9000 → ECHIDNA → theorem-proving // 9090 → Hypatia → scanning, static-analysis -// Groove status constants (matching Groove.idr GrooveProbeResult). -let GROOVE_NOT_FOUND: I32 = 0 -let GROOVE_INCOMPATIBLE: I32 = 1 -let GROOVE_CONNECTED: I32 = 2 -let GROOVE_ACTIVE: I32 = 3 +module gossamer/core/groove -// Well-known groove target IDs (matching Groove.idr and groove.zig). -let GROOVE_BURBLE: I32 = 0 -let GROOVE_VEXT: I32 = 1 -let GROOVE_VERISIMDB: I32 = 2 -let GROOVE_HYPATIA: I32 = 3 -let GROOVE_PANLL: I32 = 4 -let GROOVE_ECHIDNA: I32 = 5 -let GROOVE_RPA: I32 = 6 -let GROOVE_CONFLOW: I32 = 7 -let GROOVE_PANIC: I32 = 8 -let GROOVE_GITBOT: I32 = 9 +// ── Status constants (matching Groove.idr GrooveProbeResult) ─────────────── +pub fn grooveNotFound(): I32 = 0 +pub fn grooveIncompatible(): I32 = 1 +pub fn grooveConnected(): I32 = 2 +pub fn grooveActive(): I32 = 3 -// Total number of well-known groove targets. -let GROOVE_TARGET_COUNT: I32 = 10 +// ── Well-known groove target IDs (matching Groove.idr and groove.zig) ────── +pub fn grooveBurble(): I32 = 0 +pub fn grooveVext(): I32 = 1 +pub fn grooveVerisimdb(): I32 = 2 +pub fn grooveHypatia(): I32 = 3 +pub fn groovePanll(): I32 = 4 +pub fn grooveEchidna(): I32 = 5 +pub fn grooveRpa(): I32 = 6 +pub fn grooveConflow(): I32 = 7 +pub fn groovePanic(): I32 = 8 +pub fn grooveGitbot(): I32 = 9 +pub fn grooveTargetCount(): I32 = 10 -// Probe all well-known groove targets. -// Returns the number of grooves successfully connected. -// FFI: gossamer_groove_discover() -> count -fn discover(): I32 = - __ffi("gossamer_groove_discover") +// ── libgossamer C ABI (source of truth: src/interface/ffi/src/*.zig) ─────── +extern "gossamer" { + // Probe all well-known targets → number connected. + fn gossamer_groove_discover(): I32 + // Status of one target → 0 not_found / 1 incompatible / 2 connected / 3 active. + fn gossamer_groove_status(targetId: I32): I32 + // Capability manifest JSON for a connected groove ("" if not connected). + fn gossamer_groove_manifest(targetId: I32): String + // Target id providing a named capability, or -1 if unavailable. + fn gossamer_groove_find_capability(capName: String): I32 + // 1 if two targets can compose, else 0. + fn gossamer_groove_check_compat(targetA: I32, targetB: I32): I32 + // Send a JSON message → 0 ok. + fn gossamer_groove_send(targetId: I32, message: String): I32 + // Receive a pending JSON message ("" if none). + fn gossamer_groove_recv(targetId: I32): String + // Summary of all connections as JSON. + fn gossamer_groove_summary(): String + // Disconnect one target / all (shutdown). + fn gossamer_groove_disconnect(targetId: I32): Unit + fn gossamer_groove_disconnect_all(): Unit +} -// Get the status of a specific groove target. -// Returns: 0=not_found, 1=incompatible, 2=connected, 3=active -// FFI: gossamer_groove_status(target_id) -> status -fn status(targetId: I32): I32 = - __ffi("gossamer_groove_status", targetId) +// ── Idiomatic wrappers (public API) ──────────────────────────────────────── -// Get the capability manifest JSON for a connected groove. -// Returns empty string if groove is not connected. -// FFI: gossamer_groove_manifest(target_id) -> json_string -fn manifest(targetId: I32): String = - __ffi("gossamer_groove_manifest", targetId) - -// Check if a specific capability is available from any connected groove. -// Capability names match Groove.idr capabilityName (e.g. "voice", "integrity"). -// Returns the target ID that provides it, or -1 if unavailable. -// FFI: gossamer_groove_find_capability(cap_name) -> target_id or -1 -fn findCapability(capName: String): I32 = - __ffi("gossamer_groove_find_capability", capName) - -// Check if two groove targets are compatible (can compose). -// Returns 1 if compatible, 0 if not. -// FFI: gossamer_groove_check_compat(target_a, target_b) -> bool -fn checkCompat(targetA: I32, targetB: I32): I32 = - __ffi("gossamer_groove_check_compat", targetA, targetB) - -// Send a JSON message to a grooved service. -// FFI: gossamer_groove_send(target_id, message) -> result (0=ok) -fn send(targetId: I32, message: String): I32 = - __ffi("gossamer_groove_send", targetId, message) - -// Receive a pending JSON message from a grooved service. -// Returns empty string if no messages waiting. -// FFI: gossamer_groove_recv(target_id) -> json_string -fn recv(targetId: I32): String = - __ffi("gossamer_groove_recv", targetId) - -// Get a summary of all groove connections as JSON. -// Returns: [{"id":0,"service":"burble","status":2,"caps":["voice","text"]}, ...] -// FFI: gossamer_groove_summary() -> json_string -fn summary(): String = - __ffi("gossamer_groove_summary") - -// Disconnect a specific groove target. -// FFI: gossamer_groove_disconnect(target_id) -> void -fn disconnect(targetId: I32): () = - __ffi("gossamer_groove_disconnect", targetId) - -// Disconnect all grooves. Call during application shutdown. -// FFI: gossamer_groove_disconnect_all() -> void -fn disconnectAll(): () = - __ffi("gossamer_groove_disconnect_all") +pub fn discover(): I32 = gossamer_groove_discover() +pub fn status(targetId: I32): I32 = gossamer_groove_status(targetId) +pub fn manifest(targetId: I32): String = gossamer_groove_manifest(targetId) +pub fn findCapability(capName: String): I32 = gossamer_groove_find_capability(capName) +pub fn checkCompat(targetA: I32, targetB: I32): I32 = gossamer_groove_check_compat(targetA, targetB) +pub fn send(targetId: I32, message: String): I32 = gossamer_groove_send(targetId, message) +pub fn recv(targetId: I32): String = gossamer_groove_recv(targetId) +pub fn summary(): String = gossamer_groove_summary() +pub fn disconnect(targetId: I32): Unit = gossamer_groove_disconnect(targetId) +pub fn disconnectAll(): Unit = gossamer_groove_disconnect_all() diff --git a/src/core/Module.eph b/src/core/Module.eph index c6b8760..40fbce1 100644 --- a/src/core/Module.eph +++ b/src/core/Module.eph @@ -3,52 +3,38 @@ // // Gossamer.Module — Multi-file compilation and module system bootstrap. // -// This module provides the FFI bindings for Ephapax's module resolution -// and multi-file compilation. It enables the `import Gossamer.Shell` syntax -// and allows the compiler to resolve and compile dependent modules. +// FFI bindings for Ephapax's module resolution and multi-file compilation: +// they back the `import Gossamer.Shell` syntax and let the compiler resolve +// and compile dependent modules. No linear resources — the resolver/compiler +// cache is owned by the runtime, not threaded through Ephapax values. // -// Module resolution strategy: -// 1. Module name (e.g. "Gossamer.Shell") maps to a file path -// (e.g. "src/core/Shell.eph") via dotted-name-to-path conversion. -// 2. The resolver searches the module path list (configurable via -// gossamer.conf.json "ephapax.modulePaths"). -// 3. Circular imports are detected via a compilation stack. -// 4. Each module is compiled exactly once (cached by module name). +// The earlier version declared `: I32` / `: String` returns over `__ffi(...)`, +// which is typed `I64`, so it never type-checked. The `extern` block carries +// the real return types. // -// This is a bootstrap module: it is loaded implicitly by the compiler -// before any user module. User modules should not import this directly. +// This is a bootstrap module: the compiler loads it implicitly before any +// user module. User modules should not import it directly. -// Resolve a module name to its file system path. -// Returns the absolute path to the .eph file, or empty string if not found. -// FFI: ephapax_module_resolve(module_name) -> path -fn resolveModule(moduleName: String): String = - __ffi("ephapax_module_resolve", moduleName) +module gossamer/core/module -// Compile a module from its file path. -// Returns 0 on success, non-zero on error. -// The compiled module is cached by name for subsequent imports. -// FFI: ephapax_compile_module(path) -> result -fn compileModule(path: String): I32 = - __ffi("ephapax_compile_module", path) +// ── Ephapax runtime C ABI (module system) ────────────────────────────────── +extern "gossamer" { + // Resolve a dotted module name to its .eph path ("" if not found). + fn ephapax_module_resolve(moduleName: String): String + // Compile a module from a path (0 = ok); result is cached by name. + fn ephapax_compile_module(path: String): I32 + // 1 if the module is already compiled/cached, else 0. + fn ephapax_module_cached(moduleName: String): I32 + // Newline-separated list of a compiled module's exported symbols. + fn ephapax_module_exports(moduleName: String): String + // Resolve → compile-if-needed → register exports (0 = ok). + fn ephapax_import_module(moduleName: String): I32 +} -// Check if a module has already been compiled (cached). -// Returns 1 if cached, 0 if not. -// FFI: ephapax_module_cached(module_name) -> bool -fn isModuleCached(moduleName: String): I32 = - __ffi("ephapax_module_cached", moduleName) +// ── Idiomatic wrappers (public API) ──────────────────────────────────────── -// Get the list of symbols exported by a compiled module. -// Returns a newline-separated list of symbol names. -// FFI: ephapax_module_exports(module_name) -> symbol_list -fn moduleExports(moduleName: String): String = - __ffi("ephapax_module_exports", moduleName) - -// Import a module by name. This is the implementation behind -// the `import Gossamer.Shell` syntax: -// 1. Check if already cached -// 2. Resolve path -// 3. Compile if needed -// 4. Register exports in the current scope -// Returns 0 on success. -fn importModule(moduleName: String): I32 = - __ffi("ephapax_import_module", moduleName) +pub fn resolveModule(moduleName: String): String = ephapax_module_resolve(moduleName) +pub fn compileModule(path: String): I32 = ephapax_compile_module(path) +pub fn isModuleCached(moduleName: String): I32 = ephapax_module_cached(moduleName) +pub fn moduleExports(moduleName: String): String = ephapax_module_exports(moduleName) +pub fn importModule(moduleName: String): I32 = ephapax_import_module(moduleName) diff --git a/src/core/Platform.eph b/src/core/Platform.eph index 0b2784b..f20d4ee 100644 --- a/src/core/Platform.eph +++ b/src/core/Platform.eph @@ -3,46 +3,43 @@ // // Gossamer.Platform — Runtime platform detection and query. // -// Provides compile-time-evaluated, zero-cost platform introspection. -// All values are string constants baked into the binary at compile time -// via Zig's comptime evaluation — no runtime cost to query. +// Zero-cost platform introspection: every value is a string constant baked +// into the binary at compile time via Zig's comptime evaluation. No linear +// resources — each query borrows nothing and owns nothing. // -// Use these functions to adapt application behaviour based on the -// host platform without preprocessor conditionals or build flags. +// The earlier version declared `: I32` / `: String` returns over `__ffi(...)`, +// which is typed `I64`, so it never type-checked. Declaring the real return +// types on the `extern` block fixes that. // // Platform strings: "linux", "macos", "windows", "freebsd", "openbsd", // "netbsd", "ios", "unknown" // Architecture: "x86_64", "aarch64", "riscv64", "wasm32", "unknown" // Webview engine: "webkitgtk", "wkwebview", "webview2", "none" -// Get the platform identifier string. -// Returns one of: "linux", "macos", "windows", "freebsd", "openbsd", -// "netbsd", "ios", or "unknown". -// FFI: gossamer_platform() -> string pointer -fn platform(): String = - __ffi("gossamer_platform") - -// Get the CPU architecture string. -// Returns one of: "x86_64", "aarch64", "riscv64", "wasm32", or "unknown". -// FFI: gossamer_arch() -> string pointer -fn arch(): String = - __ffi("gossamer_arch") - -// Get the webview engine name for the current platform. -// Returns one of: "webkitgtk", "wkwebview", "webview2", or "none". -// FFI: gossamer_webview_engine() -> string pointer -fn webviewEngine(): String = - __ffi("gossamer_webview_engine") - -// Check whether the current platform is a desktop platform. -// Returns 1 for desktop (Linux, macOS, Windows, BSD), 0 for mobile/other. -// FFI: gossamer_is_desktop() -> u8 -fn isDesktop(): I32 = - __ffi("gossamer_is_desktop") - -// Get all platform information as a JSON string. -// Includes platform, architecture, webview engine, version, and desktop flag. -// Useful for passing to the frontend JS in one call. -// FFI: gossamer_platform_json() -> string pointer -fn platformJson(): String = - __ffi("gossamer_platform_json") +module gossamer/core/platform + +// ── libgossamer C ABI (source of truth: src/interface/ffi/src/*.zig) ─────── +extern "gossamer" { + fn gossamer_platform(): String + fn gossamer_arch(): String + fn gossamer_webview_engine(): String + fn gossamer_is_desktop(): I32 + fn gossamer_platform_json(): String +} + +// ── Idiomatic wrappers (public API) ──────────────────────────────────────── + +// Platform identifier: "linux", "macos", "windows", "freebsd", ..., "unknown". +pub fn platform(): String = gossamer_platform() + +// CPU architecture: "x86_64", "aarch64", "riscv64", "wasm32", "unknown". +pub fn arch(): String = gossamer_arch() + +// Webview engine: "webkitgtk", "wkwebview", "webview2", "none". +pub fn webviewEngine(): String = gossamer_webview_engine() + +// 1 for desktop (Linux, macOS, Windows, BSD), 0 for mobile/other. +pub fn isDesktop(): I32 = gossamer_is_desktop() + +// All platform info as a single JSON string (for the frontend). +pub fn platformJson(): String = gossamer_platform_json() diff --git a/src/core/SSG.eph b/src/core/SSG.eph index 6775876..45760a3 100644 --- a/src/core/SSG.eph +++ b/src/core/SSG.eph @@ -3,120 +3,47 @@ // // Gossamer.SSG — Static Site Generator accessible from the application layer. // -// Exposes the SSG Zig FFI functions (src/interface/ffi/src/ssg.zig) through -// the Ephapax FFI bridge. Provides file I/O, front matter parsing, Markdown -// to HTML conversion, template rendering, and full site build orchestration. -// -// All returned string pointers are heap-allocated by the Zig c_allocator. -// The Ephapax runtime is responsible for freeing them. Functions that return -// I64 for string content return 0 (null) on failure. -// -// The SSG module is stateless: no linear resources are created. Each function -// call is a self-contained operation that borrows its inputs and returns a -// fresh result. -// -// Typical usage: -// 1. Read source files with readFile -// 2. Parse front matter with parseFrontMatter -// 3. Extract body with extractBody -// 4. Convert Markdown to HTML with markdownToHtml -// 5. Render templates with templateRender -// 6. Write output with writeFile -// -// Or use buildSite for the full pipeline in a single call. - -// --------------------------------------------------------------------------- -// File I/O -// --------------------------------------------------------------------------- - -// Read an entire file into a string. -// Returns a pointer to the file contents (heap-allocated, null-terminated), -// or 0 on failure (file not found, read error, exceeds 64 MiB limit). -// FFI: gossamer_ssg_read_file(path) -> string_ptr | 0 -fn readFile(path: String): I64 = - __ffi("gossamer_ssg_read_file", path) - -// Write content to a file, creating parent directories as needed. -// Returns 0 on success, 1 on failure (permission denied, disk full). -// FFI: gossamer_ssg_write_file(path, content) -> 0 | 1 -fn writeFile(path: String, content: String): I32 = - __ffi("gossamer_ssg_write_file", path, content) - -// List files in a directory matching a given extension. -// Returns a newline-separated list of file paths (heap-allocated), or 0 -// on failure. Empty string for no matches. Extension includes the dot -// (e.g. ".md", ".html"). -// FFI: gossamer_ssg_list_files(dir, extension) -> string_ptr | 0 -fn listFiles(dir: String, extension: String): I64 = - __ffi("gossamer_ssg_list_files", dir, extension) - -// --------------------------------------------------------------------------- -// Front Matter Parsing -// --------------------------------------------------------------------------- - -// Extract YAML front matter from content delimited by "---" lines. -// Returns the front matter block (without delimiters) as a heap-allocated -// string, or empty string if no front matter is present. -// The content must begin with "---\n" for front matter to be detected. -// FFI: gossamer_ssg_parse_front_matter(content) -> string_ptr -fn parseFrontMatter(content: String): I64 = - __ffi("gossamer_ssg_parse_front_matter", content) - -// Extract the body content after the front matter block. -// Returns everything after the closing "---" delimiter. If no front matter -// is present, returns the entire content unchanged. -// FFI: gossamer_ssg_parse_body(content) -> string_ptr -fn extractBody(content: String): I64 = - __ffi("gossamer_ssg_parse_body", content) - -// --------------------------------------------------------------------------- -// Markdown to HTML Conversion -// --------------------------------------------------------------------------- - -// Convert a Markdown string to HTML. -// Supported syntax: -// # through ###### headings -// **bold**, *italic* -// `inline code` -// [link text](url) -// Blank-line-separated paragraphs -// ``` code blocks (fenced) -// Returns heap-allocated HTML string. -// FFI: gossamer_ssg_md_to_html(markdown) -> string_ptr -fn markdownToHtml(markdown: String): I64 = - __ffi("gossamer_ssg_md_to_html", markdown) - -// --------------------------------------------------------------------------- -// Template Rendering -// --------------------------------------------------------------------------- - -// Substitute {{key}} placeholders in a template with values from a -// newline-separated "key=value" string. -// -// Example vars: "title=Hello World\ncontent=

Body

\ndate=2026-03-28" -// -// Unknown placeholders are preserved verbatim in the output. -// Returns heap-allocated rendered string. -// FFI: gossamer_ssg_template_substitute(template, vars) -> string_ptr -fn templateRender(template: String, vars: String): I64 = - __ffi("gossamer_ssg_template_substitute", template, vars) - -// --------------------------------------------------------------------------- -// Full Site Build -// --------------------------------------------------------------------------- - -// Build an entire static site from a content directory, a template file, -// and an output directory. -// -// Process for each .md file in contentDir: -// 1. Read the file -// 2. Extract front matter (title, date) -// 3. Extract body and convert Markdown to HTML -// 4. Substitute {{title}}, {{content}}, {{date}} into the template -// 5. Write the result as .html in outDir -// -// Creates outDir and any parent directories if they do not exist. -// Returns 0 on success, 1 on failure. -// FFI: gossamer_ssg_build_site(contentDir, templateFile, outDir) -> 0 | 1 -fn buildSite(contentDir: String, templateFile: String, outDir: String): I32 = - __ffi("gossamer_ssg_build_site", contentDir, templateFile, outDir) +// Exposes the SSG Zig FFI (src/interface/ffi/src/ssg.zig): file I/O, front +// matter parsing, Markdown→HTML, template rendering, and full-site build. +// +// The SSG module is STATELESS: no linear resources are created. Each call is +// a self-contained operation that borrows its inputs and returns a fresh +// result (I64 = heap-allocated string pointer, 0 on failure; I32 = 0/1 code). +// +// The earlier version declared `: I32` returns over `__ffi(...)`, which is +// typed `I64`, so it never type-checked. The `extern` block carries the real +// return types. +// +// Pipeline: readFile → parseFrontMatter → extractBody → markdownToHtml → +// templateRender → writeFile, or buildSite for the whole thing in one call. + +module gossamer/core/ssg + +// ── libgossamer C ABI (source of truth: src/interface/ffi/src/ssg.zig) ───── +extern "gossamer" { + // File I/O. + fn gossamer_ssg_read_file(path: String): I64 + fn gossamer_ssg_write_file(path: String, content: String): I32 + fn gossamer_ssg_list_files(dir: String, extension: String): I64 + // Front matter. + fn gossamer_ssg_parse_front_matter(content: String): I64 + fn gossamer_ssg_parse_body(content: String): I64 + // Markdown → HTML. + fn gossamer_ssg_md_to_html(markdown: String): I64 + // Template rendering ({{key}} substitution). + fn gossamer_ssg_template_substitute(template: String, vars: String): I64 + // Full-site build → 0 ok / 1 fail. + fn gossamer_ssg_build_site(contentDir: String, templateFile: String, outDir: String): I32 +} + +// ── Idiomatic wrappers (public API) ──────────────────────────────────────── + +pub fn readFile(path: String): I64 = gossamer_ssg_read_file(path) +pub fn writeFile(path: String, content: String): I32 = gossamer_ssg_write_file(path, content) +pub fn listFiles(dir: String, extension: String): I64 = gossamer_ssg_list_files(dir, extension) +pub fn parseFrontMatter(content: String): I64 = gossamer_ssg_parse_front_matter(content) +pub fn extractBody(content: String): I64 = gossamer_ssg_parse_body(content) +pub fn markdownToHtml(markdown: String): I64 = gossamer_ssg_md_to_html(markdown) +pub fn templateRender(template: String, vars: String): I64 = gossamer_ssg_template_substitute(template, vars) +pub fn buildSite(contentDir: String, templateFile: String, outDir: String): I32 = + gossamer_ssg_build_site(contentDir, templateFile, outDir) diff --git a/src/core/Shell.eph b/src/core/Shell.eph index 3e9e763..b4a18f6 100644 --- a/src/core/Shell.eph +++ b/src/core/Shell.eph @@ -3,98 +3,89 @@ // // Gossamer.Shell — Webview window lifecycle management. // -// The webview handle is a LINEAR resource: -// - create returns a linear handle (must be consumed) -// - loadHTML borrows the handle (returns it back) -// - navigate borrows the handle (returns it back) -// - run CONSUMES the handle (window is destroyed) -// - destroy CONSUMES the handle (alternative to run) - -// FFI declarations — these are implemented in ffi/zig/src/main.zig -// and linked as libgossamer.so - -// Create a webview window. Returns a linear handle. -// FFI: gossamer_create(title, width, height, resizable, decorations, fullscreen) -> handle -fn create(title: String, width: I32, height: I32): I64 = - __ffi("gossamer_create", title, width, height, 1, 1, 0) - -// Load HTML content into the webview. Borrows the handle. -// FFI: gossamer_load_html(handle, html) -> result -fn loadHTML(h: I64, html: String): I32 = - __ffi("gossamer_load_html", h, html) - -// Navigate to a URL. Borrows the handle. -// FFI: gossamer_navigate(handle, url) -> result -fn navigate(h: I64, url: String): I32 = - __ffi("gossamer_navigate", h, url) - -// Evaluate JavaScript in the webview. Borrows the handle. -// FFI: gossamer_eval(handle, js) -> result -fn eval(h: I64, js: String): I32 = - __ffi("gossamer_eval", h, js) - -// Set the window title. Borrows the handle. -// FFI: gossamer_set_title(handle, title) -> result -fn setTitle(h: I64, title: String): I32 = - __ffi("gossamer_set_title", h, title) +// The webview handle is a GENUINELY LINEAR resource, enforced by the Ephapax +// type checker (`ephapax check`, default `--mode linear`): +// - `create` mints a linear `Webview` handle; +// - the borrow ops (loadHTML, navigate, eval, setTitle, resize, show, hide, +// minimize, maximize, restore, requestClose) take `&Webview` — they use +// the window without retiring it; +// - `run` CONSUMES the handle (the event loop owns then destroys the window); +// - `destroy` CONSUMES the handle (teardown without running). +// +// Because `Webview` is linear, a path that creates a window and never `run`s +// or `destroy`s it is a COMPILE-TIME type error. The earlier version of this +// file passed the handle around as a plain `I64` (no linear obligation) and +// declared `: I32` / `: ()` returns over `__ffi(...)`, which is typed `I64` — +// so it never type-checked at all. The opaque `extern` handle type is what +// makes the checker enforce the lifecycle. + +module gossamer/core/shell + +// ── libgossamer C ABI (source of truth: src/interface/ffi/src/main.zig) ──── +extern "gossamer" { + // Opaque, linear webview window handle. + type Webview + + // gossamer_create(title, width, height, resizable, decorations, fullscreen) -> handle + fn gossamer_create(title: String, width: I32, height: I32, resizable: I32, decorations: I32, fullscreen: I32): Webview + + // Borrow ops — use the window, return a C result code, do not retire it. + fn gossamer_load_html(h: &Webview, html: String): I32 + fn gossamer_navigate(h: &Webview, url: String): I32 + fn gossamer_eval(h: &Webview, js: String): I32 + fn gossamer_set_title(h: &Webview, title: String): I32 + fn gossamer_resize(h: &Webview, width: I32, height: I32): I32 + fn gossamer_show(h: &Webview): I32 + fn gossamer_hide(h: &Webview): I32 + fn gossamer_minimize(h: &Webview): I32 + fn gossamer_maximize(h: &Webview): I32 + fn gossamer_restore(h: &Webview): I32 + fn gossamer_request_close(h: &Webview): I32 + + // Consuming ops — retire the handle. + fn gossamer_run(h: Webview): Unit + fn gossamer_destroy(h: Webview): Unit + + // Handle-free diagnostics (string pointers / no window). + fn gossamer_last_error(): I64 + fn gossamer_version(): I64 + fn gossamer_build_info(): I64 +} + +// ── Idiomatic wrappers (public API; other Ephapax modules import these) ──── + +// Create a webview window. Returns a linear handle that MUST be consumed +// (via run or destroy). Defaults: resizable, decorated, not fullscreen. +pub fn create(title: String, width: I32, height: I32): Webview = + gossamer_create(title, width, height, 1, 1, 0) + +pub fn loadHTML(h: &Webview, html: String): I32 = gossamer_load_html(h, html) +pub fn navigate(h: &Webview, url: String): I32 = gossamer_navigate(h, url) +pub fn eval(h: &Webview, js: String): I32 = gossamer_eval(h, js) +pub fn setTitle(h: &Webview, title: String): I32 = gossamer_set_title(h, title) +pub fn resize(h: &Webview, width: I32, height: I32): I32 = gossamer_resize(h, width, height) +pub fn show(h: &Webview): I32 = gossamer_show(h) +pub fn hide(h: &Webview): I32 = gossamer_hide(h) +pub fn minimize(h: &Webview): I32 = gossamer_minimize(h) +pub fn maximize(h: &Webview): I32 = gossamer_maximize(h) +pub fn restore(h: &Webview): I32 = gossamer_restore(h) +pub fn requestClose(h: &Webview): I32 = gossamer_request_close(h) // Run the event loop. CONSUMES the handle — window is destroyed after. -// FFI: gossamer_run(handle) -> void -fn run(h: I64): () = - __ffi("gossamer_run", h) - -// Resize the webview window. Borrows the handle. -// FFI: gossamer_resize(handle, width, height) -> result -fn resize(h: I64, width: I32, height: I32): I32 = - __ffi("gossamer_resize", h, width, height) - -// Show the webview window. Borrows the handle. -// FFI: gossamer_show(handle) -> result -fn show(h: I64): I32 = - __ffi("gossamer_show", h) - -// Hide the webview window. Borrows the handle. -// FFI: gossamer_hide(handle) -> result -fn hide(h: I64): I32 = - __ffi("gossamer_hide", h) - -// Minimize the webview window. Borrows the handle. -// FFI: gossamer_minimize(handle) -> result -fn minimize(h: I64): I32 = - __ffi("gossamer_minimize", h) - -// Maximize the webview window. Borrows the handle. -// FFI: gossamer_maximize(handle) -> result -fn maximize(h: I64): I32 = - __ffi("gossamer_maximize", h) - -// Restore the webview window. Borrows the handle. -// FFI: gossamer_restore(handle) -> result -fn restore(h: I64): I32 = - __ffi("gossamer_restore", h) - -// Request that the window close. Borrows the handle. -// FFI: gossamer_request_close(handle) -> result -fn requestClose(h: I64): I32 = - __ffi("gossamer_request_close", h) - +pub fn run(h: Webview): Unit = gossamer_run(h) // Destroy the webview without running. CONSUMES the handle. -// FFI: gossamer_destroy(handle) -> void -fn destroy(h: I64): () = - __ffi("gossamer_destroy", h) - -// Get the last error message from the FFI layer. -// Returns a pointer to the error string, or 0 if no error. -// FFI: gossamer_last_error() -> ptr -fn lastError(): I64 = - __ffi("gossamer_last_error") - -// Get the library version string (e.g. "0.1.0"). -// FFI: gossamer_version() -> ptr -fn version(): I64 = - __ffi("gossamer_version") - -// Get build information string. -// FFI: gossamer_build_info() -> ptr -fn buildInfo(): I64 = - __ffi("gossamer_build_info") +pub fn destroy(h: Webview): Unit = gossamer_destroy(h) + +pub fn lastError(): I64 = gossamer_last_error() +pub fn version(): I64 = gossamer_version() +pub fn buildInfo(): I64 = gossamer_build_info() + +// ── Linearity witness ────────────────────────────────────────────────────── +// Create a window, load HTML into it (borrow), then run the loop (consume). +// `ephapax check` accepts this because `w` is consumed exactly once; drop the +// `run(w)` and the file is rejected — that rejection is the machine-checked +// proof the window handle cannot leak. +fn session(title: String, html: String): Unit = + let! w = create(title, 800, 600) + let _r = loadHTML(&w, html) + run(w) diff --git a/src/core/ShellExec.eph b/src/core/ShellExec.eph index fc1352a..3bf19f3 100644 --- a/src/core/ShellExec.eph +++ b/src/core/ShellExec.eph @@ -3,39 +3,58 @@ // // Gossamer.ShellExec — Shell command execution guarded by capability tokens. // -// All shell operations require a valid RESOURCE_SHELL capability token. -// The token is borrowed (not consumed) by execute operations. +// All operations require a valid RESOURCE_SHELL capability token, passed by +// value as `I64` (its linear grant/revoke discipline lives in Capabilities.eph). // -// This module is named ShellExec to avoid collision with Shell (webview lifecycle). - -// Execute a shell command and return stdout as a string pointer. -// Requires a valid shell capability token. -// Returns 0 on error (check Shell.lastError for details). -// FFI: gossamer_shell_execute(program, args_json, cap_token) -> result_json_ptr -fn execute(program: String, argsJson: String, capToken: I64): I64 = - __ffi("gossamer_shell_execute", program, argsJson, capToken) - -// Open a URL or file with the system's default handler. -// Requires a valid shell capability token. -// Uses xdg-open (Linux), open (macOS), or start (Windows). -// FFI: gossamer_shell_open(url, cap_token) -> result -fn openUrl(url: String, capToken: I64): I32 = - __ffi("gossamer_shell_open", url, capToken) - -// Spawn a shell command in the background and return an opaque child -// handle. The command runs via /bin/sh -c (POSIX) or cmd /c (Windows) -// with stdin/stdout/stderr inherited from the caller. The handle is -// only valid until passed to spawnKill; do not use it for anything else. -// Requires a valid shell capability token. -// Returns 0 on error (check Shell.lastError for details). -// FFI: gossamer_shell_spawn(command, cap_token) -> opaque_handle -fn spawn(command: String, capToken: I64): I64 = - __ffi("gossamer_shell_spawn", command, capToken) - -// Terminate a previously-spawned background child and wait for it to -// exit. Idempotent on 0 (no-op). The handle is invalid after this call. -// Requires a valid shell capability token. -// Returns 0 (ok) or non-zero error code. -// FFI: gossamer_shell_kill(opaque_handle, cap_token) -> result -fn spawnKill(handle: I64, capToken: I64): I32 = - __ffi("gossamer_shell_kill", handle, capToken) +// The spawned background child is a GENUINELY LINEAR resource, enforced by +// `ephapax check` (default `--mode linear`): +// - `spawn` mints a linear `Child` handle; +// - `spawnKill` CONSUMES the handle (terminates and reaps the child). +// +// Because `Child` is linear, spawning a background command and never killing +// it is a compile-time type error — no orphaned child can leak. `execute` and +// `openUrl` are one-shot and own no handle. +// +// Named ShellExec to avoid collision with Shell (webview lifecycle). The +// earlier version passed the child as a plain `I64` and declared `: I32` +// returns over `__ffi(...)` (typed `I64`), so it never type-checked. + +module gossamer/core/shell_exec + +// ── libgossamer C ABI (source of truth: src/interface/ffi/src/*.zig) ─────── +extern "gossamer" { + // Opaque, linear background-child handle. + type Child + + // One-shot ops (no handle). execute returns a result-json string pointer. + fn gossamer_shell_execute(program: String, argsJson: String, capToken: I64): I64 + fn gossamer_shell_open(url: String, capToken: I64): I32 + + // gossamer_shell_spawn(command, cap_token) -> opaque_handle + fn gossamer_shell_spawn(command: String, capToken: I64): Child + + // Consuming op — terminate and reap the child; returns a C result code. + fn gossamer_shell_kill(child: Child, capToken: I64): I32 +} + +// ── Idiomatic wrappers (public API) ──────────────────────────────────────── + +// Execute a shell command and return stdout as a result-json pointer (0 = err). +pub fn execute(program: String, argsJson: String, capToken: I64): I64 = + gossamer_shell_execute(program, argsJson, capToken) + +// Open a URL/file with the system default handler. +pub fn openUrl(url: String, capToken: I64): I32 = gossamer_shell_open(url, capToken) + +// Spawn a background command. Returns a linear handle that MUST be killed. +pub fn spawn(command: String, capToken: I64): Child = gossamer_shell_spawn(command, capToken) + +// Terminate a spawned child and wait for exit. CONSUMES the handle. +pub fn spawnKill(child: Child, capToken: I64): I32 = gossamer_shell_kill(child, capToken) + +// ── Linearity witness ────────────────────────────────────────────────────── +// Spawn a background child, then kill it (consume). Drop `spawnKill(...)` and +// `ephapax check` rejects the file: the child cannot be orphaned. +fn session(command: String, capToken: I64): I32 = + let! child = spawn(command, capToken) + spawnKill(child, capToken) diff --git a/src/core/Tray.eph b/src/core/Tray.eph index fd0ae6b..22c7433 100644 --- a/src/core/Tray.eph +++ b/src/core/Tray.eph @@ -3,80 +3,72 @@ // // Gossamer.Tray — System tray lifecycle management. // -// The tray handle is a LINEAR resource: -// - create returns a linear handle (must be consumed) -// - addItem borrows the handle (returns it back) -// - addSeparator borrows the handle (returns it back) -// - setIcon borrows the handle (returns it back) -// - setTooltip borrows the handle (returns it back) -// - destroy CONSUMES the handle (tray is removed) +// The tray handle is a GENUINELY LINEAR resource, enforced by `ephapax check` +// (default `--mode linear`): +// - `create` mints a linear `Tray` handle; +// - the borrow ops (addItem, addSeparator, setCallback, setIcon, +// setIconFromFile, setTooltip, setVisible, setWindow) take `&Tray`; +// - `destroy` CONSUMES the handle (the icon leaves the notification area). // -// The tray persists in the system notification area (KDE Plasma tray) -// for the lifetime of the application. It provides: -// - Right-click context menu with custom items -// - Left-click to toggle main window -// - Tooltip with status information -// - Icon changes to reflect system state -// - Desktop notifications via notify-send +// `notify` needs no tray handle — it routes a desktop notification through +// notify-send → xdg-desktop-portal → the KDE notification daemon. +// +// Because `Tray` is linear, creating a tray and never destroying it is a +// compile-time type error. The earlier version passed the handle as a plain +// `I64` and declared `: I32` / `: ()` returns over `__ffi(...)` (typed `I64`), +// so it never type-checked. -// Create a system tray icon. Returns a LINEAR handle. -// The tray appears in the KDE Plasma system tray area. -// FFI: gossamer_tray_create(tooltip) -> handle -fn create(tooltip: String): I64 = - __ffi("gossamer_tray_create", tooltip) +module gossamer/core/tray -// Destroy the tray icon. CONSUMES the handle. -// FFI: gossamer_tray_destroy(handle) -> void -fn destroy(h: I64): () = - __ffi("gossamer_tray_destroy", h) +// ── libgossamer C ABI (source of truth: src/interface/ffi/src/*.zig) ─────── +extern "gossamer" { + // Opaque, linear system-tray handle. + type Tray -// Add an item to the tray right-click context menu. BORROWS the handle. -// item_id is passed to the callback when the item is clicked. -// FFI: gossamer_tray_add_item(handle, label, item_id) -> result -fn addItem(h: I64, label: String, itemId: I32): I32 = - __ffi("gossamer_tray_add_item", h, label, itemId) + // gossamer_tray_create(tooltip) -> handle + fn gossamer_tray_create(tooltip: String): Tray -// Add a separator line to the context menu. BORROWS the handle. -// FFI: gossamer_tray_add_separator(handle) -> result -fn addSeparator(h: I64): I32 = - __ffi("gossamer_tray_add_separator", h) + // Borrow ops — mutate the tray, return a C result code, do not retire it. + fn gossamer_tray_add_item(h: &Tray, label: String, itemId: I32): I32 + fn gossamer_tray_add_separator(h: &Tray): I32 + fn gossamer_tray_set_callback(h: &Tray, callback: I64): I32 + fn gossamer_tray_set_icon(h: &Tray, iconName: String): I32 + fn gossamer_tray_set_icon_from_file(h: &Tray, path: String): I32 + fn gossamer_tray_set_tooltip(h: &Tray, tooltip: String): I32 + fn gossamer_tray_set_visible(h: &Tray, visible: I32): I32 + fn gossamer_tray_set_window(h: &Tray, window: I64): I32 -// Set the callback invoked when a menu item is clicked. -// The callback receives the item_id of the clicked item. -// FFI: gossamer_tray_set_callback(handle, callback) -> result -fn setCallback(h: I64, callback: I64): I32 = - __ffi("gossamer_tray_set_callback", h, callback) + // Consuming op — retire the handle. + fn gossamer_tray_destroy(h: Tray): Unit -// Set the tray icon by theme icon name. BORROWS the handle. -// Standard names: "network-server", "network-offline", -// "dialog-information", "dialog-warning", "dialog-error" -// FFI: gossamer_tray_set_icon(handle, icon_name) -> result -fn setIcon(h: I64, iconName: String): I32 = - __ffi("gossamer_tray_set_icon", h, iconName) + // Handle-free desktop notification. + fn gossamer_notify(title: String, body: String): I32 +} -// Set the tray icon from a file path. BORROWS the handle. -// FFI: gossamer_tray_set_icon_from_file(handle, path) -> result -fn setIconFromFile(h: I64, path: String): I32 = - __ffi("gossamer_tray_set_icon_from_file", h, path) +// ── Idiomatic wrappers (public API) ──────────────────────────────────────── -// Update the tooltip text. BORROWS the handle. -// FFI: gossamer_tray_set_tooltip(handle, tooltip) -> result -fn setTooltip(h: I64, tooltip: String): I32 = - __ffi("gossamer_tray_set_tooltip", h, tooltip) +// Create a system tray icon. Returns a LINEAR handle that MUST be destroyed. +pub fn create(tooltip: String): Tray = gossamer_tray_create(tooltip) -// Show or hide the tray icon. BORROWS the handle. -// FFI: gossamer_tray_set_visible(handle, visible) -> result -fn setVisible(h: I64, visible: I32): I32 = - __ffi("gossamer_tray_set_visible", h, visible) +pub fn addItem(h: &Tray, label: String, itemId: I32): I32 = gossamer_tray_add_item(h, label, itemId) +pub fn addSeparator(h: &Tray): I32 = gossamer_tray_add_separator(h) +pub fn setCallback(h: &Tray, callback: I64): I32 = gossamer_tray_set_callback(h, callback) +pub fn setIcon(h: &Tray, iconName: String): I32 = gossamer_tray_set_icon(h, iconName) +pub fn setIconFromFile(h: &Tray, path: String): I32 = gossamer_tray_set_icon_from_file(h, path) +pub fn setTooltip(h: &Tray, tooltip: String): I32 = gossamer_tray_set_tooltip(h, tooltip) +pub fn setVisible(h: &Tray, visible: I32): I32 = gossamer_tray_set_visible(h, visible) +pub fn setWindow(h: &Tray, window: I64): I32 = gossamer_tray_set_window(h, window) + +// Destroy the tray icon. CONSUMES the handle. +pub fn destroy(h: Tray): Unit = gossamer_tray_destroy(h) -// Attach a main window handle so left-click toggles show/hide. -// Passing 0 detaches the window and restores the menu callback fallback. -// FFI: gossamer_tray_set_window(tray, window) -> result -fn setWindow(h: I64, window: I64): I32 = - __ffi("gossamer_tray_set_window", h, window) +// Show a desktop notification (no tray handle required). +pub fn notify(title: String, body: String): I32 = gossamer_notify(title, body) -// Show a desktop notification (does not require a tray handle). -// Routes through notify-send → xdg-desktop-portal → KDE notification daemon. -// FFI: gossamer_notify(title, body) -> result -fn notify(title: String, body: String): I32 = - __ffi("gossamer_notify", title, body) +// ── Linearity witness ────────────────────────────────────────────────────── +// Create a tray, add a menu item (borrow), then destroy it (consume). Drop +// `destroy(t)` and `ephapax check` rejects the file: the tray cannot leak. +fn session(tooltip: String, label: String): Unit = + let! t = create(tooltip) + let _r = addItem(&t, label, 1) + destroy(t)