diff --git a/.github/workflows/abi-typecheck.yml b/.github/workflows/abi-typecheck.yml index fbf9d8f..7649f70 100644 --- a/.github/workflows/abi-typecheck.yml +++ b/.github/workflows/abi-typecheck.yml @@ -14,12 +14,16 @@ on: paths: - 'src/interface/**' - 'gossamer-abi.ipkg' + - 'gossamer-groove.ipkg' + - 'scripts/check-abi-decoupling.sh' - '.github/workflows/abi-typecheck.yml' push: branches: [main, master] paths: - 'src/interface/**' - 'gossamer-abi.ipkg' + - 'gossamer-groove.ipkg' + - 'scripts/check-abi-decoupling.sh' - '.github/workflows/abi-typecheck.yml' permissions: @@ -30,9 +34,22 @@ concurrency: cancel-in-progress: true jobs: + # Fast, toolchain-free structural gate (gossamer#95): fails in seconds if the + # ABI namespace symlinks re-materialise into copies, or if a shell module + # re-imports a groove module. Runs before the ~15-min Idris2 build. + abi-structure: + name: ABI decoupling guard (symlinks + groove split) + runs-on: ubuntu-latest + steps: + - name: Checkout repository + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + - name: Check ABI decoupling + run: ./scripts/check-abi-decoupling.sh + abi-typecheck: - name: idris2 --typecheck gossamer-abi.ipkg + name: idris2 --typecheck (shell + groove) runs-on: ubuntu-latest + needs: abi-structure steps: - name: Checkout repository uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 @@ -49,5 +66,11 @@ jobs: make install echo "$HOME/.idris2/bin" >> "$GITHUB_PATH" - - name: Typecheck the formal ABI package + - name: Typecheck the shell ABI package (groove-agnostic) run: idris2 --typecheck gossamer-abi.ipkg + + - name: Install the shell ABI package (dependency of groove) + run: idris2 --install gossamer-abi.ipkg + + - name: Typecheck the groove protocol package (depends on the shell) + run: idris2 --typecheck gossamer-groove.ipkg diff --git a/CHANGELOG.md b/CHANGELOG.md index 142733a..f57ae2e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,6 +11,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] ### Changed +- **Honest ABI decoupling from Groove; namespace symlinks restored (gossamer#95)**: the formal ABI now separates the webview **shell** from the **Groove** inter-service protocol at every level, fixing two root causes at source and adding gates so they cannot silently recur. Verified with `idris2 0.8.0` (Chez) end-to-end — both packages `--typecheck` green and the 147-test ABI suite passes. + - **Duplication → single source of truth.** `src/interface/Gossamer/ABI/.idr` were committed as byte-identical *copies* of `src/interface/abi/.idr` (the symlinks from `#42` had been materialised into regular files), so every module lived twice and the two trees could drift while the `.ipkg` still claimed "symlinks map the namespace". Restored all 15 namespace entries to `120000` symlinks into the canonical `src/interface/abi/` tree — one physical copy per module, nothing to drift. + - **Conflation → one-way layering.** The shell package `gossamer-abi.ipkg` bundled the Groove protocol proofs, and shell modules imported `Gossamer.ABI.Groove`. Those imports in `ResourceCleanup` and `IPCDispatch` were **vestigial** (their `TGroove`/`CmdGroove*` only use shell types) and were removed; `HandleLinearity`'s genuine groove use (`grooveValid`, `LinearGroove`, `allocateGroove`, `consumeForDisconnect`) was **extracted** into the new groove-layer module `Gossamer.ABI.GrooveLinearity`, which instantiates the shell's *generic* `LinearHandle` for `GrooveHandle`. The shell now type-checks without Idris2 ever compiling `Groove`. No proof was deleted — every module moved, none dropped. +- **`gossamer-abi.ipkg` is now the groove-agnostic shell** (11 modules): `Types`, `Layout`, `Foreign`, `IPCDispatch`, `HandleLinearity`, `WindowStateMachine`, `LayoutStability`, `IPCIntegrity`, `PanelIsolation`, `ResourceCleanup`, `AndroidComponents`. `abi-check` (Justfile) and the ABI Typecheck Gate now build both packages and run the decoupling guard first. - **Frontend IPC binding migrated ReScript → AffineScript** (`@gossamer/api`, standards#252): the published package is now the AffineScript binding in `bindings/affinescript/`, type-checked with `affinescript check` and compiled to a standalone Deno-ESM module via `deno task build` (`affinescript compile --deno-esm`). ReScript is banned estate-wide; this completes gossamer's migration. - **Repository `LICENSE` corrected to `MPL-2.0`**: the top-level licence declared `AGPL-3.0-or-later` while all 394 source files and the `.ipkg` manifest are MPL-2.0 (gossamer is a sole-owner repo). Brought into line — the governance licence-consistency gate is now green. @@ -18,6 +22,8 @@ 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 +- **`gossamer-groove.ipkg` — the Groove protocol proofs in their own package (gossamer#95)**: 4 modules — `Groove` (capability types, manifests, handshake state machine), `GrooveLinearity` (groove-handle linearity over the shell's generic `LinearHandle`), `CapabilityAuthenticity` (no phantom capabilities; attenuation soundness), and `GrooveTermination` (handshake terminates in ≤4 steps, no privilege escalation). Declares `depends = base, gossamer-abi`, so the layering is enforced by the build: Groove depends on the shell, never the reverse. +- **`scripts/check-abi-decoupling.sh` — structural guard for the shell/groove split (gossamer#95)**: a fast, toolchain-free check (wired into the ABI Typecheck Gate ahead of the ~15-min Idris2 build, and into `just abi-check`) that fails if any `Gossamer/ABI/*.idr` is a materialised copy instead of a symlink, or if a shell module re-imports a groove module, or if the two `.ipkg` manifests stop partitioning the modules. Shellcheck-clean; proven to fail on both regressions and pass on the fixed tree. - **Android — `gossamer-android-services` companion: four shim base classes + real JNI (Phase 5, #71)**: Grows the Android target from "a WebView in an Activity" into a first-class mobile shell hosting the non-UI components, on the critical path for neurophone#97 (migrating a banned-Kotlin Android app onto gossamer). Owner-signed-off subclass model (issue #71). - `src/interface/ffi/src/jni.zig` (new) — a REAL JNI binding in pure Zig: models the `JNINativeInterface`/`JNIInvokeInterface` tables (ordinal-indexed), uses the `...A`-variant calls (no C varargs across the boundary), caches the `JavaVM` for thread attach, uses global refs, and reads `float[]` sensor samples via `Get/ReleaseFloatArrayElements`. The previous bridge declared `extern fn jni_*` symbols defined nowhere, so it could never link. - **Four abstract Java base classes** under `android/gossamer-android-services/src/main/java/io/gossamer/` that downstream apps EXTEND with ~5-20 lines (lifecycle methods are `final`): `services/GossamerForegroundService` (Service + SensorEventListener), `services/GossamerBootReceiver` (BroadcastReceiver), `services/GossamerAppWidgetProvider` (AppWidgetProvider), and the existing `GossamerActivity` extended with an `onIntentReceived` hook. gossamer owns every JNI call. diff --git a/GETTING-STARTED.md b/GETTING-STARTED.md index 1eb2eaa..4ff8475 100644 --- a/GETTING-STARTED.md +++ b/GETTING-STARTED.md @@ -27,7 +27,9 @@ just test-zig-bench ## Configuration Files -- **gossamer-abi.ipkg / gossamer-abi-tests.ipkg** — Idris2 ABI package and its test runner +- **gossamer-abi.ipkg** — Idris2 formal ABI for the webview shell (groove-agnostic) +- **gossamer-groove.ipkg** — Idris2 proofs for the Groove protocol (depends on gossamer-abi) +- **gossamer-abi-tests.ipkg** — the ABI test runner - **flake.nix** — Nix development environment (fallback to guix.scm) - **guix.scm** — Primary Guix package definition for reproducible dev env - **gossamer.conf.json** — Runtime config: window size, IPC protocol, CSP, capabilities, sandbox diff --git a/Justfile b/Justfile index 99dfd45..51cdbc1 100644 --- a/Justfile +++ b/Justfile @@ -41,10 +41,15 @@ check-affine: check-example name: {{ephapax}} check examples/{{name}}/main.eph --mode linear -v -# Type-check the formal ABI proof package (idris2 0.8.0). This is a +# Type-check the formal ABI proof packages (idris2 0.8.0). This is a # REQUIRED gate, not optional: the ABI modules silently bit-rot otherwise. +# Guards the shell/groove decoupling (gossamer#95), then type-checks the +# groove-agnostic shell package and the groove package that depends on it. abi-check: + ./scripts/check-abi-decoupling.sh idris2 --typecheck gossamer-abi.ipkg + idris2 --install gossamer-abi.ipkg + idris2 --typecheck gossamer-groove.ipkg # Build the Gossamer CLI (links libgossamer) build-cli: build-ffi diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index 651b926..ad8f2b9 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -5,7 +5,8 @@ - `src/interface/abi/Foreign.idr` — FFI declarations - `src/interface/abi/Layout.idr` — Memory layout definitions - `src/interface/abi/Groove.idr` — Groove protocol type definitions -- `src/interface/abi/HandleLinearity.idr` — Handle lifecycle and uniqueness proofs +- `src/interface/abi/GrooveLinearity.idr` — Groove-handle linearity (instantiates the shell's generic `LinearHandle` for `GrooveHandle`) ✅ NEW (gossamer#95) +- `src/interface/abi/HandleLinearity.idr` — Handle lifecycle and uniqueness proofs (groove-agnostic) - `src/interface/abi/IPCIntegrity.idr` — IPC message integrity proofs - `src/interface/abi/PanelIsolation.idr` — Panel isolation proofs - `src/interface/abi/CapabilityAuthenticity.idr` — Capability authenticity proofs @@ -14,7 +15,7 @@ - `src/interface/abi/ResourceCleanup.idr` — Resource cleanup on teardown proofs ✅ - `src/interface/abi/WindowStateMachine.idr` — Window state machine correctness (GS1) ✅ NEW 2026-04-11 - `src/interface/abi/IPCDispatch.idr` — IPC handler type safety, 25 handlers (GS2) ✅ NEW 2026-04-11 -- **All 13 ABI modules above are now wired into `gossamer-abi.ipkg` and pass `idris2 0.8.0 --typecheck` cleanly** (2026-05-20, `standards#131` close-out). Prior to `gossamer#22` / `#36` / `#40` / `#41`, several modules were excluded from the ipkg and had never been built — their PROOF-NEEDS ✅ markers reflected an unverified posture; build is now the oracle. +- **All 15 ABI modules above build green and pass `idris2 0.8.0 --typecheck` cleanly**, now split across two de-conflated packages (`gossamer#95`): the groove-agnostic **shell** `gossamer-abi.ipkg` (11 modules) and the **groove** `gossamer-groove.ipkg` (4: `Groove`, `GrooveLinearity`, `CapabilityAuthenticity`, `GrooveTermination`), which *depends on* the shell. The dependency points one way only — no shell module imports a groove module. The canonical sources live in `src/interface/abi/`; `src/interface/Gossamer/ABI/.idr` are symlinks (a single source of truth, no drift). `scripts/check-abi-decoupling.sh` gates both invariants in CI. Prior to `gossamer#22` / `#36` / `#40` / `#41`, several modules were excluded from the ipkg and had never been built — their PROOF-NEEDS ✅ markers reflected an unverified posture; build is now the oracle. - **One class-J axiom**: `Gossamer.ABI.PanelIsolation.stringNotEqCommut` — sanctioned principled assumption over the Idris2 backend primitive `prim__eq_String` (content-symmetry on every supported backend; cannot be derived inside Idris2). `%unsafe`-annotated, `believe_me ()`-bodied, documented at the use site. Same trust posture as boj-server's `Boj.SafetyLemmas.charEqSym` and four sibling axioms over String / Char primitives. See "Class-J axioms (trusted base)" section below. - No other `believe_me`, `sorry`, `postulate`, or `assert_total` in the ABI layer. - Zig FFI layer in `src/interface/ffi/` diff --git a/README.md b/README.md index a5847a6..c1a298d 100644 --- a/README.md +++ b/README.md @@ -173,13 +173,17 @@ Gossamer’s ABI is written in Idris2 with the proof obligations audited in `PROOF-NEEDS.md`. Headline posture (as of `standards#131` close-out, 2026-05-20): -- **All 13 ABI proof modules build green.** `gossamer-abi.ipkg` `idris2` - `0.8.0` `--typecheck` passes 13/13 with `%default` `total`. Modules: - `Types`, `Layout`, `Foreign`, `Groove`, `CapabilityAuthenticity`, - `IPCDispatch`, `HandleLinearity`, `WindowStateMachine`, - `GrooveTermination`, `LayoutStability`, `IPCIntegrity`, - `PanelIsolation`, `ResourceCleanup`. Discharge ledger in - `PROOF-NEEDS.md`. +- **All 15 ABI proof modules build green, across two de-conflated + packages** (`gossamer#95`). `idris2` `0.8.0` `--typecheck` passes with + `%default` `total`. + - **Shell** — `gossamer-abi.ipkg` (11, groove-agnostic): `Types`, + `Layout`, `Foreign`, `IPCDispatch`, `HandleLinearity`, + `WindowStateMachine`, `LayoutStability`, `IPCIntegrity`, + `PanelIsolation`, `ResourceCleanup`, `AndroidComponents`. + - **Groove** — `gossamer-groove.ipkg` (4, depends on the shell): + `Groove`, `GrooveLinearity`, `CapabilityAuthenticity`, + `GrooveTermination`. No shell module imports a groove module; the + dependency points one way only. Discharge ledger in `PROOF-NEEDS.md`. diff --git a/gossamer-abi.ipkg b/gossamer-abi.ipkg index 4abaaca..688cea6 100644 --- a/gossamer-abi.ipkg +++ b/gossamer-abi.ipkg @@ -15,11 +15,15 @@ version = 0.1.0 authors = "Jonathan D.A. Jewell" -brief = "Formally verified ABI for the Gossamer webview shell and Groove protocol" - --- Source files live in src/interface/abi/ but declare module Gossamer.ABI.* --- Symlinks in src/interface/Gossamer/ABI/ map the Idris2 module namespace --- to the physical file locations. +brief = "Formally verified ABI for the Gossamer webview shell (groove-agnostic)" + +-- The canonical source files live in src/interface/abi/ and declare module +-- Gossamer.ABI.* Idris2 requires the on-disk path to match the module name, +-- so src/interface/Gossamer/ABI/.idr is a SYMLINK to ../../abi/.idr — +-- a single source of truth, no duplicated copies to drift. +-- The groove protocol layer (Groove, GrooveTermination, CapabilityAuthenticity, +-- GrooveLinearity) is de-conflated into its own package, gossamer-groove.ipkg, +-- which depends on this one. No module listed here imports a groove module. sourcedir = "src/interface" depends = base @@ -27,12 +31,9 @@ depends = base modules = Gossamer.ABI.Types , Gossamer.ABI.Layout , Gossamer.ABI.Foreign - , Gossamer.ABI.Groove - , Gossamer.ABI.CapabilityAuthenticity , Gossamer.ABI.IPCDispatch , Gossamer.ABI.HandleLinearity , Gossamer.ABI.WindowStateMachine - , Gossamer.ABI.GrooveTermination , Gossamer.ABI.LayoutStability , Gossamer.ABI.IPCIntegrity , Gossamer.ABI.PanelIsolation @@ -41,7 +42,6 @@ modules = Gossamer.ABI.Types -- All formerly-deferred ABI proof modules from gossamer#22's OWED list -- are now wired and `idris2 --typecheck` green: --- * GrooveTermination — discharged in gossamer#36 (MERGED) -- * LayoutStability — discharged in gossamer#40 (MERGED) -- * IPCIntegrity — discharged in gossamer#40 (MERGED) -- * PanelIsolation — discharged in this branch via a sanctioned @@ -51,3 +51,4 @@ modules = Gossamer.ABI.Types -- posture as boj-server's `Boj.SafetyLemmas.*`. -- * ResourceCleanup — discharged in this branch (missing `Data.DPair` -- import + lowercase `exists` → `Exists`). +-- GrooveTermination (gossamer#36) now lives in gossamer-groove.ipkg. diff --git a/gossamer-groove.ipkg b/gossamer-groove.ipkg new file mode 100644 index 0000000..bbbe9a4 --- /dev/null +++ b/gossamer-groove.ipkg @@ -0,0 +1,43 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Gossamer Groove — Idris2 package for the Groove inter-service protocol proofs. +-- +-- De-conflated from the shell ABI (gossamer-abi.ipkg): Groove is a separate +-- concern (type-safe capability discovery between services), so its proofs live +-- in their own package that DEPENDS ON the shell, never the other way round. +-- This layering is enforced: no gossamer-abi module imports a groove module. +-- +-- The canonical sources live in src/interface/abi/ and declare module +-- Gossamer.ABI.* ; src/interface/Gossamer/ABI/.idr symlinks to them so the +-- on-disk path matches the module name (Idris2's requirement). +-- +-- Build the shell first, then this package: +-- idris2 --install gossamer-abi.ipkg +-- idris2 --typecheck gossamer-groove.ipkg + +package gossamer-groove + +version = 0.1.0 + +authors = "Jonathan D.A. Jewell" + +brief = "Formally verified proofs for the Groove inter-service discovery protocol" + +sourcedir = "src/interface" + +depends = base + , gossamer-abi + +modules = Gossamer.ABI.Groove + , Gossamer.ABI.GrooveLinearity + , Gossamer.ABI.CapabilityAuthenticity + , Gossamer.ABI.GrooveTermination + +-- Groove-protocol proof modules relocated here from the shell (gossamer#95): +-- * Groove — capability types, manifests, handshake state machine +-- * GrooveLinearity — groove-handle linearity (instantiates the shell's +-- generic LinearHandle for GrooveHandle) +-- * CapabilityAuthenticity — no phantom capabilities; attenuation soundness +-- * GrooveTermination — handshake termination + no-privilege-escalation +-- (discharged in gossamer#36, MERGED) diff --git a/scripts/check-abi-decoupling.sh b/scripts/check-abi-decoupling.sh new file mode 100755 index 0000000..ac24d5a --- /dev/null +++ b/scripts/check-abi-decoupling.sh @@ -0,0 +1,104 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check-abi-decoupling.sh — structural guard for gossamer#95. +# +# Makes the two root causes behind #95 impossible to reintroduce silently: +# +# 1. Duplication: src/interface/Gossamer/ABI/.idr must be a SYMLINK into +# the canonical src/interface/abi/.idr — never a materialised copy. +# (The bug: symlinks were once committed as byte-identical regular files, +# so the two trees drifted and every edit had to be made twice.) +# +# 2. Conflation: no module in the shell package (gossamer-abi.ipkg) may import +# a Groove-layer module. Groove is a separate concern and lives in +# gossamer-groove.ipkg, which DEPENDS ON the shell — never the reverse. +# +# Exit non-zero (with GitHub-Actions ::error annotations) on any violation. +# Pure structure check: no toolchain required, so it runs anywhere. +set -euo pipefail + +cd "$(git rev-parse --show-toplevel)" + +NS_DIR="src/interface/Gossamer/ABI" +ABI_DIR="src/interface/abi" +SHELL_IPKG="gossamer-abi.ipkg" +GROOVE_IPKG="gossamer-groove.ipkg" + +# The Groove-layer modules (canonical basenames). Everything else under +# $ABI_DIR is shell and must stay groove-agnostic. +GROOVE_MODULES=(Groove GrooveTermination GrooveLinearity CapabilityAuthenticity) + +fail=0 +err() { printf '::error::%s\n' "$1" >&2; fail=1; } +note() { printf ' %s\n' "$1"; } + +is_groove_module() { + local name="$1" g + for g in "${GROOVE_MODULES[@]}"; do + [ "$name" = "$g" ] && return 0 + done + return 1 +} + +# --------------------------------------------------------------------------- +# Check 1: namespace files are symlinks into the canonical abi/ tree. +# --------------------------------------------------------------------------- +echo "== Check 1: ABI namespace files are symlinks (no duplication) ==" +while IFS=$'\t' read -r meta path; do + mode=${meta%% *} + base=$(basename "$path") + if [ "$mode" != "120000" ]; then + err "$path is tracked as mode $mode, expected 120000 (a symlink)." + note "The ABI namespace copies must be symlinks into $ABI_DIR/, not files." + continue + fi + target=$(git cat-file -p ":$path") + if [ "$target" != "../../abi/$base" ]; then + err "$path points to '$target', expected '../../abi/$base'." + fi + if [ ! -e "$ABI_DIR/$base" ]; then + err "canonical source $ABI_DIR/$base is missing (dangling symlink $path)." + fi +done < <(git ls-files -s -- "$NS_DIR"/*.idr | sed -E 's/^([0-9]+) [0-9a-f]+ [0-9]+\t/\1\t/') +[ "$fail" -eq 0 ] && echo " OK: all $NS_DIR/*.idr are symlinks into $ABI_DIR/" + +# --------------------------------------------------------------------------- +# Check 2: no shell module imports a Groove-layer module. +# --------------------------------------------------------------------------- +echo "== Check 2: shell modules are groove-agnostic (no conflation) ==" +groove_import_re='^import[[:space:]]+Gossamer\.ABI\.(Groove|GrooveTermination|GrooveLinearity|CapabilityAuthenticity)([[:space:]]|$)' +for f in "$ABI_DIR"/*.idr; do + base=$(basename "$f" .idr) + is_groove_module "$base" && continue + if grep -nE "$groove_import_re" "$f" >/dev/null; then + err "shell module '$base' imports a Groove-layer module (re-conflation)." + grep -nE "$groove_import_re" "$f" | sed 's/^/ /' >&2 + fi +done +[ "$fail" -eq 0 ] && echo " OK: no shell module imports a groove module" + +# --------------------------------------------------------------------------- +# Check 3: the package manifests keep the split. +# --------------------------------------------------------------------------- +echo "== Check 3: package manifests keep shell/groove split ==" +if [ ! -f "$GROOVE_IPKG" ]; then + err "$GROOVE_IPKG is missing — the groove proofs must live in their own package." +fi +for g in "${GROOVE_MODULES[@]}"; do + if grep -qE "Gossamer\.ABI\.$g([[:space:]]|,|$)" "$SHELL_IPKG"; then + err "$SHELL_IPKG lists groove module 'Gossamer.ABI.$g' — it belongs in $GROOVE_IPKG." + fi + if [ -f "$GROOVE_IPKG" ] && ! grep -qE "Gossamer\.ABI\.$g([[:space:]]|,|$)" "$GROOVE_IPKG"; then + err "$GROOVE_IPKG does not list groove module 'Gossamer.ABI.$g'." + fi +done +[ "$fail" -eq 0 ] && echo " OK: $SHELL_IPKG is groove-free; $GROOVE_IPKG owns the groove modules" + +echo +if [ "$fail" -ne 0 ]; then + echo "ABI decoupling guard: FAILED (see ::error annotations above)." >&2 + exit 1 +fi +echo "ABI decoupling guard: PASSED." diff --git a/src/interface/Gossamer/ABI/AndroidComponents.idr b/src/interface/Gossamer/ABI/AndroidComponents.idr deleted file mode 100644 index d707342..0000000 --- a/src/interface/Gossamer/ABI/AndroidComponents.idr +++ /dev/null @@ -1,293 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- -||| Android Non-UI Component Lifecycles for Gossamer (GS-ANDROID) -||| -||| Gossamer hosts a WebView in an Activity, but a production Android app also -||| needs background components with no webview in scope: a foreground Service, -||| a BroadcastReceiver, and an AppWidgetProvider. This module gives those -||| components the same formal treatment the webview already enjoys: -||| -||| 1. Each component is a state machine with a TERMINAL teardown state and -||| no transition out of it (mirrors WindowStateMachine's `Closed`). -||| 2. Event dispatch is only well-typed while the component is LIVE — the -||| type-level analogue of the runtime plugin-liveness check that prevents -||| use-after-free in the IPC dispatcher. -||| 3. The long-lived Service is modelled as a `LinearHandle` over the SAME -||| lifecycle framework as the webview (HandleLinearity), so the linear -||| "consume exactly once" guarantee crosses the new JNI boundary intact. -||| -||| The native side of these contracts lives in src/interface/ffi/src/ -||| android_{service,receiver,widget}.zig; the JVM side is gossamer-GENERATED -||| Java (android/generated/). An app binds pure handlers via the -||| gossamer_{service,receiver,widget}_bind FFI declared at the foot of this -||| module and never touches JNI itself. -||| -||| OPEN (tracked as a gossamer issue): the deep region-calculus question of how -||| a long-lived, JVM-owned Service handle relates to the shorter-lived webview -||| region — and how cross-region references (a Service pushing a Widget update) -||| are tracked — is NOT settled here. This module proves the parts that are -||| unambiguous (terminal teardown, dispatch-only-while-live, single-consume) -||| and leaves the region-nesting design to that issue. -||| -||| No unsafe escape hatches; every proof is constructive. - -module Gossamer.ABI.AndroidComponents - -import Gossamer.ABI.Types -import Gossamer.ABI.HandleLinearity -import Data.So - -%default total - --------------------------------------------------------------------------------- --- Component Taxonomy --------------------------------------------------------------------------------- - -||| The three non-UI Android components Gossamer hosts natively. -public export -data ComponentKind = ServiceC | ReceiverC | WidgetC - -||| Whether a component owns a LONG-LIVED handle (one whose lifetime spans many -||| dispatches) versus a TRANSIENT one (constructed per dispatch by the JVM). -||| -||| Only the Service owns a long-lived handle: the JVM keeps the Service object -||| alive across many onStartCommand calls. A BroadcastReceiver and an -||| AppWidgetProvider update are constructed, called once, and discarded — each -||| dispatch is a scoped borrow, not an owned handle. -public export -data LongLived : ComponentKind -> Type where - ServiceIsLongLived : LongLived ServiceC - -||| Receiver dispatch is transient (no owned long-lived handle). -public export -data Transient : ComponentKind -> Type where - ReceiverIsTransient : Transient ReceiverC - WidgetIsTransient : Transient WidgetC - -||| Long-lived and transient are disjoint classifications. -public export -longLivedNotTransient : LongLived k -> Transient k -> Void -longLivedNotTransient ServiceIsLongLived x = case x of {} - --------------------------------------------------------------------------------- --- Foreground Service lifecycle: Created -> Started* -> Destroyed --------------------------------------------------------------------------------- - -||| States of a gossamer-hosted foreground Service. -||| Mirrors android.app.Service: onCreate, onStartCommand (repeatable), -||| onDestroy (terminal). -public export -data SvcState = SvcCreated | SvcStarted | SvcDestroyed - -||| Service lifecycle operations (the JNI entry points in services_android.zig). -public export -data SvcOp = OnCreate | OnStartCommand | OnDestroy - -||| Valid Service transitions. No constructor has source SvcDestroyed, so -||| SvcDestroyed is absorbing. onStartCommand may fire repeatedly (START_STICKY -||| redelivery), modelled by the Started -> Started self-loop. -public export -data SvcTransition : (s : SvcState) -> (op : SvcOp) -> (t : SvcState) -> Type where - StartFromCreated : SvcTransition SvcCreated OnStartCommand SvcStarted - StartFromStarted : SvcTransition SvcStarted OnStartCommand SvcStarted - DestroyFromCreated : SvcTransition SvcCreated OnDestroy SvcDestroyed - DestroyFromStarted : SvcTransition SvcStarted OnDestroy SvcDestroyed - -||| GS-ANDROID-INV-1: onDestroy is terminal — no transition leaves SvcDestroyed. -public export -svcDestroyedTerminal : SvcTransition SvcDestroyed op t -> Void -svcDestroyedTerminal _ impossible - -||| A Service is "live" (safe to dispatch events into) iff it is not destroyed. -public export -data SvcLive : SvcState -> Type where - LiveCreated : SvcLive SvcCreated - LiveStarted : SvcLive SvcStarted - -||| A destroyed Service is not live (no dispatch after teardown). -public export -svcDestroyedNotLive : SvcLive SvcDestroyed -> Void -svcDestroyedNotLive x = case x of {} - -||| onStartCommand always lands in the Started state — the foreground work is -||| running regardless of whether this was the first start or a redelivery. -public export -startCommandStarts : SvcTransition s OnStartCommand t -> t = SvcStarted -startCommandStarts StartFromCreated = Refl -startCommandStarts StartFromStarted = Refl - -||| onDestroy always lands in the terminal state. -public export -destroyDestroys : SvcTransition s OnDestroy t -> t = SvcDestroyed -destroyDestroys DestroyFromCreated = Refl -destroyDestroys DestroyFromStarted = Refl - --------------------------------------------------------------------------------- --- BroadcastReceiver lifecycle: Live -> Complete (one-shot) --------------------------------------------------------------------------------- - -||| States of a single BroadcastReceiver invocation. The JVM constructs the -||| receiver, calls onReceive exactly once, and discards it; onReceive must -||| complete within its window (Android tears the receiver down on return). -public export -data RcvState = RcvLive | RcvComplete - -||| The single valid receiver transition: handle the broadcast, then complete. -public export -data RcvTransition : (s : RcvState) -> (t : RcvState) -> Type where - ReceiveOnce : RcvTransition RcvLive RcvComplete - -||| GS-ANDROID-INV-2: a completed receiver is terminal — onReceive cannot fire -||| twice on the same instance. -public export -rcvCompleteTerminal : RcvTransition RcvComplete t -> Void -rcvCompleteTerminal _ impossible - --------------------------------------------------------------------------------- --- AppWidgetProvider lifecycle: Enabled -> Disabled (updates are borrows) --------------------------------------------------------------------------------- - -||| States of a gossamer-hosted home-screen widget provider. onEnabled fires -||| when the first instance is placed; onDisabled when the last is removed -||| (terminal). onUpdate is a BORROW: it renders without changing provider -||| state, exactly like the webview's loadHTML/navigate borrows. -public export -data WdgState = WdgEnabled | WdgDisabled - -public export -data WdgOp = WidgetOnUpdate | WidgetOnDisabled - -||| Valid widget transitions. onUpdate is absent here because, as a borrow, it -||| does not move the provider between states (see `widgetUpdateBorrow`). -public export -data WdgTransition : (s : WdgState) -> (op : WdgOp) -> (t : WdgState) -> Type where - DisableFromEnabled : WdgTransition WdgEnabled WidgetOnDisabled WdgDisabled - -||| GS-ANDROID-INV-3: onDisabled is terminal. -public export -wdgDisabledTerminal : WdgTransition WdgDisabled op t -> Void -wdgDisabledTerminal _ impossible - -||| onUpdate is a borrow: it is only valid on an enabled provider and leaves the -||| state unchanged. Encoded as a predicate rather than a state transition. -public export -data WidgetUpdateBorrow : WdgState -> Type where - UpdateWhileEnabled : WidgetUpdateBorrow WdgEnabled - -||| A disabled provider cannot service updates. -public export -wdgDisabledNoUpdate : WidgetUpdateBorrow WdgDisabled -> Void -wdgDisabledNoUpdate x = case x of {} - --------------------------------------------------------------------------------- --- Service as a Linear Handle (linearity preserved across the JNI boundary) --------------------------------------------------------------------------------- - -||| Opaque handle to a gossamer-hosted foreground Service. -||| Like WebviewHandle, this is a LINEAR resource carrying a non-null proof: -||| it is allocated once (onCreate) and consumed once (onDestroy). -public export -data ServiceHandle : Type where - MkService : (ptr : Bits64) - -> {auto 0 nonNull : So (ptr /= 0)} - -> ServiceHandle - -||| Extract the raw pointer (for FFI calls). -public export -servicePtr : ServiceHandle -> Bits64 -servicePtr (MkService ptr) = ptr - -||| Recover the erased non-null witness as a ValidToken, mirroring -||| HandleLinearity.webviewValid. The witness already lives inside MkService; -||| this re-exposes it so allocation is total with no runtime null re-check. -public export -serviceValid : (s : ServiceHandle) -> ValidToken (servicePtr s) -serviceValid (MkService ptr {nonNull}) = MkValid {nonNull} - -||| A linearly-tracked Service handle, reusing the generic Allocated/Active/ -||| Consumed machine from HandleLinearity. This is the load-bearing claim that -||| the new Service boundary keeps Gossamer's linear guarantees: a Service that -||| is leaked (never onDestroy) or torn down twice does not type-check. -public export -LinearService : HandleState -> Type -LinearService = LinearHandle ServiceHandle - -||| Allocate a linear Service handle (state Allocated), set up at onCreate. -public export -allocateService : ServiceHandle -> LinearService Allocated -allocateService s = MkLinear s (servicePtr s) {valid = serviceValid s} - -||| Consume the Service handle at onDestroy. Active -> Consumed, returning the -||| raw handle for the final FFI teardown call. There is no way to reconstruct -||| an Active handle from the Consumed one, so no dispatch can follow. -public export -consumeForStop : LinearService Active -> (ServiceHandle, LinearService Consumed) -consumeForStop = consume - -||| The Service lifecycle state maps onto the generic handle lifecycle: -||| Created↔Allocated, Started↔Active, Destroyed↔Consumed. -public export -svcToHandleState : SvcState -> HandleState -svcToHandleState SvcCreated = Allocated -svcToHandleState SvcStarted = Active -svcToHandleState SvcDestroyed = Consumed - -||| The mapping sends the terminal Service state to the terminal handle state, -||| witnessing that "Service destroyed" and "handle consumed" coincide. -public export -destroyedIsConsumed : svcToHandleState SvcDestroyed = Consumed -destroyedIsConsumed = Refl - --------------------------------------------------------------------------------- --- FFI: native callback registration (implemented in services_android.zig) --------------------------------------------------------------------------------- --- --- The #71 companion uses the subclass model: the JVM-side base classes --- (io.gossamer.services.*) own the Android contracts, and the app's native core --- (Rust/Zig) plugs in by registering plain C callbacks at JNI_OnLoad. gossamer --- owns every JNI call. Each callback is a raw C function pointer (Bits64); the --- concrete handler is supplied by the app, so these declarations fix only the C --- symbol and arity. The foreground-Service handle threaded to the callbacks is --- the independent ServiceHandle modelled above. - -||| Register the foreground-Service callbacks: create, startCommand, destroy, -||| sensorEvent (four raw C function pointers). -export -%foreign "C:gossamer_android_register_service_callbacks, libgossamer" -prim__registerServiceCallbacks : Bits64 -> Bits64 -> Bits64 -> Bits64 -> PrimIO () - -||| Register the AppWidget callbacks: fetchState, handleAction. -export -%foreign "C:gossamer_android_register_widget_callbacks, libgossamer" -prim__registerWidgetCallbacks : Bits64 -> Bits64 -> PrimIO () - -||| Register the boot-receiver shouldRestart predicate callback. -export -%foreign "C:gossamer_android_register_boot_callback, libgossamer" -prim__registerBootCallback : Bits64 -> PrimIO () - -||| Register the Activity intent callback. -export -%foreign "C:gossamer_android_register_intent_callback, libgossamer" -prim__registerIntentCallback : Bits64 -> PrimIO () - -||| Safe wrapper: register the foreground-Service native callbacks. -export -registerServiceCallbacks : (create : Bits64) -> (start : Bits64) -> (destroy : Bits64) -> (sensor : Bits64) -> IO () -registerServiceCallbacks c s d sn = primIO (prim__registerServiceCallbacks c s d sn) - -||| Safe wrapper: register the AppWidget native callbacks. -export -registerWidgetCallbacks : (fetchState : Bits64) -> (handleAction : Bits64) -> IO () -registerWidgetCallbacks f h = primIO (prim__registerWidgetCallbacks f h) - -||| Safe wrapper: register the boot-receiver callback. -export -registerBootCallback : (shouldRestart : Bits64) -> IO () -registerBootCallback sr = primIO (prim__registerBootCallback sr) - -||| Safe wrapper: register the Activity intent callback. -export -registerIntentCallback : (onIntent : Bits64) -> IO () -registerIntentCallback oi = primIO (prim__registerIntentCallback oi) diff --git a/src/interface/Gossamer/ABI/AndroidComponents.idr b/src/interface/Gossamer/ABI/AndroidComponents.idr new file mode 120000 index 0000000..d3c5817 --- /dev/null +++ b/src/interface/Gossamer/ABI/AndroidComponents.idr @@ -0,0 +1 @@ +../../abi/AndroidComponents.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/CapabilityAuthenticity.idr b/src/interface/Gossamer/ABI/CapabilityAuthenticity.idr deleted file mode 100644 index a591ce0..0000000 --- a/src/interface/Gossamer/ABI/CapabilityAuthenticity.idr +++ /dev/null @@ -1,234 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- -||| Capability Authenticity Proofs for Gossamer -||| -||| Proves that declared capabilities match actual behaviour. -||| A service cannot claim to offer a capability it does not implement, -||| and a consumer cannot invoke a capability the service does not offer. -||| -||| Builds on the Groove.idr capability sets and the Cap type from Types.idr. -||| -||| Key properties proved: -||| 1. Declaration-implementation correspondence: every declared capability -||| has a corresponding handler implementation. -||| 2. No phantom capabilities: you cannot invoke an undeclared capability. -||| 3. Capability attenuation: delegated capabilities cannot exceed the -||| original grant scope. -||| 4. Revocation completeness: revoking a capability removes all derived -||| capabilities. -||| -||| Zero believe_me. All proofs are constructive. - -module Gossamer.ABI.CapabilityAuthenticity - -import Gossamer.ABI.Types -import Gossamer.ABI.Groove -import Data.So -import Data.Bits -import Data.List -import Data.List.Elem - -%default total - --------------------------------------------------------------------------------- --- Capability Implementation Witness --------------------------------------------------------------------------------- - -||| A handler for a specific capability type. -||| -||| This is an opaque witness that a capability has been implemented. -||| The actual handler lives in the Zig FFI layer; this type is the -||| compile-time proof that an implementation exists. -||| -||| The phantom type parameter `cap` ties the handler to a specific -||| capability, preventing capability confusion. -public export -data CapHandler : (cap : CapabilityType) -> Type where - ||| Witness that a handler exists for the given capability. - ||| The Bits64 is the handler's function pointer at the FFI level. - MkHandler : (ptr : Bits64) - -> {auto 0 nonNull : So (ptr /= 0)} - -> CapHandler cap - -||| Extract handler pointer (for FFI calls). -public export -handlerPtr : CapHandler cap -> Bits64 -handlerPtr (MkHandler ptr) = ptr - --------------------------------------------------------------------------------- --- Implementation Table --------------------------------------------------------------------------------- - -||| A table mapping declared capabilities to their handler implementations. -||| -||| Parameterised by the capability set, ensuring that every declared -||| capability has a corresponding handler. -public export -data ImplTable : (caps : CapSet) -> Type where - ||| Empty implementation table (no capabilities). - ITNil : ImplTable [] - ||| A handler for `cap` plus implementations for the rest. - ITCons : CapHandler cap - -> ImplTable rest - -> ImplTable (cap :: rest) - -||| Look up a handler for a specific capability in the implementation table. -||| Requires a proof that the capability is in the declared set. -public export -lookupHandler : ImplTable caps -> Elem cap caps -> CapHandler cap -lookupHandler (ITCons handler _) Here = handler -lookupHandler (ITCons _ rest) (There later) = lookupHandler rest later - --------------------------------------------------------------------------------- --- Declaration-Implementation Correspondence --------------------------------------------------------------------------------- - -||| Proof that a groove manifest's declared capabilities are fully implemented. -||| -||| This is the core authenticity guarantee: a service that declares -||| capabilities [Voice, Text, Presence] must provide handlers for all three. -||| The ImplTable type enforces this by construction — you cannot build an -||| ImplTable unless you supply a handler for every element. -public export -data FullyImplemented : (offers : CapSet) -> Type where - ||| Witness that every offered capability has a handler. - MkFullyImplemented : ImplTable offers -> FullyImplemented offers - -||| Construct a fully-implemented proof from an implementation table. -public export -proveImplemented : ImplTable offers -> FullyImplemented offers -proveImplemented = MkFullyImplemented - --------------------------------------------------------------------------------- --- No Phantom Capabilities --------------------------------------------------------------------------------- - -||| Proof that invoking a capability requires it to be declared. -||| -||| A consumer cannot call a capability that is not in the service's -||| offers set. The Elem proof is the compile-time guarantee. -public export -data InvocationPermit : (cap : CapabilityType) -> (offers : CapSet) -> Type where - ||| You may invoke `cap` because it appears in the offers set. - MkPermit : Elem cap offers -> InvocationPermit cap offers - -||| Attempt to create an invocation permit. -||| Fails at compile time if cap is not in offers (via the auto-search -||| for Elem cap offers). -public export -permitInvocation : {auto prf : Elem cap offers} -> InvocationPermit cap offers -permitInvocation = MkPermit prf - -||| Invoke a capability with both authenticity and permit checks. -||| Requires: -||| 1. The capability set is fully implemented (no phantom handlers) -||| 2. The specific capability is in the offers set (no phantom invocations) -public export -authenticInvoke : FullyImplemented offers - -> InvocationPermit cap offers - -> CapHandler cap -authenticInvoke (MkFullyImplemented table) (MkPermit elem) = - lookupHandler table elem - --------------------------------------------------------------------------------- --- Capability Attenuation --------------------------------------------------------------------------------- - -||| A derived capability that is a subset of an original grant. -||| -||| When a capability is delegated (e.g. a panel receives a scoped -||| capability from the shell), the derived capability cannot exceed -||| the original. Attenuation guarantees that delegation is safe. -public export -data Attenuated : (original : ResourceKind) -> (derived : ResourceKind) -> Type where - ||| Identity attenuation: the derived capability is the same as the original. - ||| This is the base case for direct grants. - AttSame : Attenuated r r - ||| Filesystem read-only is an attenuation of read-write. - AttFsReadOnly : Attenuated (FileSystem (ReadWrite paths)) - (FileSystem (ReadOnlyPaths paths)) - ||| Filesystem AppData is an attenuation of any filesystem scope. - AttFsAppData : Attenuated (FileSystem scope) (FileSystem AppData) - ||| Network: specific hosts is an attenuation of all-network. - AttNetHosts : Attenuated (Network AllNetwork) (Network (AllowHosts hosts)) - ||| Shell: specific commands is an attenuation of all-shell. - AttShellCmds : Attenuated (Shell AllShell) (Shell (AllowCommands cmds)) - ||| Groove: specific targets is an attenuation of all-groove. - AttGrooveTargets : Attenuated (Groove AllGroove) (Groove (AllowTargets targets)) - -||| Proof that attenuation is transitive. -||| If A attenuates to B and B attenuates to C, then A attenuates to C. -||| We prove this for the identity case; other cases are encoded directly -||| in the Attenuated constructors. -public export -attenuateTransitive : Attenuated a b -> Attenuated b b -> Attenuated a b -attenuateTransitive prf AttSame = prf --- `AttFsAppData : Attenuated (FileSystem scope) (FileSystem AppData)` also --- inhabits `Attenuated b b` (when scope = AppData), so coverage requires it. --- `b` is then `FileSystem AppData` and `prf : Attenuated a b` is the result. -attenuateTransitive prf AttFsAppData = prf - --------------------------------------------------------------------------------- --- Revocation Completeness --------------------------------------------------------------------------------- - -||| A revocation token tracks which capabilities have been revoked. -public export -data RevocationSet : Type where - ||| No capabilities revoked. - RevEmpty : RevocationSet - ||| A capability token has been revoked. - RevAdd : (token : Bits64) -> RevocationSet -> RevocationSet - -||| Proof that a capability token is in the revocation set. -public export -data IsRevoked : (token : Bits64) -> RevocationSet -> Type where - ||| The token is the most recently revoked. - RevokedHere : IsRevoked token (RevAdd token rest) - ||| The token was revoked earlier. - RevokedThere : IsRevoked token rest -> IsRevoked token (RevAdd other rest) - -||| Proof that a derived capability is revoked when its parent is revoked. -||| -||| If capability A was delegated to produce capability B (via attenuation), -||| and A's token is revoked, then B is also invalid. -public export -data RevocationComplete : Type where - ||| Witness that revoking parent token invalidates derived token. - MkRevComplete : (parentToken : Bits64) - -> (derivedToken : Bits64) - -> (revoked : RevocationSet) - -> {auto 0 parentRevoked : IsRevoked parentToken revoked} - -> RevocationComplete - --------------------------------------------------------------------------------- --- Groove Manifest Authenticity --------------------------------------------------------------------------------- - -||| Proof that a groove manifest is authentic: every offered capability -||| is implemented and every consumed capability is actually needed. -||| -||| This combines: -||| 1. FullyImplemented for the offers set -||| 2. A witness that the consumes set is referenced by at least one handler -public export -data AuthenticManifest : (offers : CapSet) -> (consumes : CapSet) -> Type where - MkAuthentic : FullyImplemented offers - -> AuthenticManifest offers consumes - -||| Construct an authentic manifest proof. -public export -proveAuthentic : ImplTable offers -> AuthenticManifest offers consumes -proveAuthentic table = MkAuthentic (proveImplemented table) - -||| Proof that connecting to an authentic service is safe. -||| -||| If the service's manifest is authentic (all declared capabilities are -||| implemented) and compatible (our requirements are satisfied), then -||| the connection will behave as advertised. -public export -data SafeConnection : (clientReqs : CapSet) -> (serverOffers : CapSet) -> Type where - MkSafe : AuthenticManifest serverOffers serverCons - -> IsSubset clientReqs serverOffers - -> SafeConnection clientReqs serverOffers diff --git a/src/interface/Gossamer/ABI/CapabilityAuthenticity.idr b/src/interface/Gossamer/ABI/CapabilityAuthenticity.idr new file mode 120000 index 0000000..c75570c --- /dev/null +++ b/src/interface/Gossamer/ABI/CapabilityAuthenticity.idr @@ -0,0 +1 @@ +../../abi/CapabilityAuthenticity.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/Foreign.idr b/src/interface/Gossamer/ABI/Foreign.idr deleted file mode 100644 index 5f04e3f..0000000 --- a/src/interface/Gossamer/ABI/Foreign.idr +++ /dev/null @@ -1,215 +0,0 @@ -||| SPDX-License-Identifier: MPL-2.0 -||| Foreign Function Interface Declarations for GOSSAMER -||| -||| This module declares all C-compatible functions that will be -||| implemented in the Zig FFI layer. -||| -||| All functions are declared here with type signatures and safety proofs. -||| Implementations live in ffi/zig/ - -module Gossamer.ABI.Foreign - -import Gossamer.ABI.Types -import Gossamer.ABI.Layout - -%default total - --------------------------------------------------------------------------------- --- Library Lifecycle --------------------------------------------------------------------------------- - -||| Initialize the library -||| Returns a handle to the library instance, or Nothing on failure -export -%foreign "C:gossamer_init, libgossamer" -prim__init : PrimIO Bits64 - -||| Safe wrapper for library initialization -||| Requires a MainThreadProof witness — the library handle is main-thread-bound. -export -init : {auto prf : MainThreadProof} -> IO (Maybe WebviewHandle) -init = do - ptr <- primIO prim__init - pure (createWebview ptr) - -||| Clean up library resources -export -%foreign "C:gossamer_free, libgossamer" -prim__free : Bits64 -> PrimIO () - -||| Safe wrapper for cleanup -export -free : WebviewHandle -> IO () -free h = primIO (prim__free (webviewPtr h)) - --------------------------------------------------------------------------------- --- Core Operations --------------------------------------------------------------------------------- - -||| Example operation: process data -export -%foreign "C:gossamer_process, libgossamer" -prim__process : Bits64 -> Bits32 -> PrimIO Bits32 - -||| Safe wrapper with error handling -export -process : WebviewHandle -> Bits32 -> IO (Either Result Bits32) -process h input = do - result <- primIO (prim__process (webviewPtr h) input) - pure $ case result of - 0 => Left Error - n => Right n - --------------------------------------------------------------------------------- --- String Operations --------------------------------------------------------------------------------- - -||| Convert C string to Idris String -export -%foreign "support:idris2_getString, libidris2_support" -prim__getString : Bits64 -> String - -||| Free C string -export -%foreign "C:gossamer_free_string, libgossamer" -prim__freeString : Bits64 -> PrimIO () - -||| Get string result from library -export -%foreign "C:gossamer_get_string, libgossamer" -prim__getResult : Bits64 -> PrimIO Bits64 - -||| Safe string getter -export -getString : WebviewHandle -> IO (Maybe String) -getString h = do - ptr <- primIO (prim__getResult (webviewPtr h)) - if ptr == 0 - then pure Nothing - else do - let str = prim__getString ptr - primIO (prim__freeString ptr) - pure (Just str) - --------------------------------------------------------------------------------- --- Array/Buffer Operations --------------------------------------------------------------------------------- - -||| Process array data -export -%foreign "C:gossamer_process_array, libgossamer" -prim__processArray : Bits64 -> Bits64 -> Bits32 -> PrimIO Bits32 - -||| Safe array processor -export -processArray : WebviewHandle -> (buffer : Bits64) -> (len : Bits32) -> IO (Either Result ()) -processArray h buf len = do - result <- primIO (prim__processArray (webviewPtr h) buf len) - pure $ case resultFromInt result of - Just Ok => Right () - Just err => Left err - Nothing => Left Error - where - resultFromInt : Bits32 -> Maybe Result - resultFromInt 0 = Just Ok - resultFromInt 1 = Just Error - resultFromInt 2 = Just InvalidParam - resultFromInt 3 = Just OutOfMemory - resultFromInt 4 = Just NullPointer - resultFromInt _ = Nothing - --------------------------------------------------------------------------------- --- Error Handling --------------------------------------------------------------------------------- - -||| Get last error message -export -%foreign "C:gossamer_last_error, libgossamer" -prim__lastError : PrimIO Bits64 - -||| Retrieve last error as string -export -lastError : IO (Maybe String) -lastError = do - ptr <- primIO prim__lastError - if ptr == 0 - then pure Nothing - else pure (Just (prim__getString ptr)) - --- errorDescription is re-exported via Gossamer.ABI.Types - --------------------------------------------------------------------------------- --- Version Information --------------------------------------------------------------------------------- - -||| Get library version -export -%foreign "C:gossamer_version, libgossamer" -prim__version : PrimIO Bits64 - -||| Get version as string -export -version : IO String -version = do - ptr <- primIO prim__version - pure (prim__getString ptr) - -||| Get library build info -export -%foreign "C:gossamer_build_info, libgossamer" -prim__buildInfo : PrimIO Bits64 - -||| Get build information -export -buildInfo : IO String -buildInfo = do - ptr <- primIO prim__buildInfo - pure (prim__getString ptr) - --------------------------------------------------------------------------------- --- Callback Support --------------------------------------------------------------------------------- - -||| Callback function type (C ABI) -public export -Callback : Type -Callback = Bits64 -> Bits32 -> Bits32 - -||| Register a callback. -||| The callback is passed to C as a function pointer: Idris2's C FFI -||| marshals the `Callback` closure directly (the prior `AnyPtr` + -||| `cast` had no `Cast Callback AnyPtr` instance and never compiled — -||| a latent error masked by the never-built module). -export -%foreign "C:gossamer_register_callback, libgossamer" -prim__registerCallback : Bits64 -> Callback -> PrimIO Bits32 - -||| Safe callback registration -export -registerCallback : WebviewHandle -> Callback -> IO (Either Result ()) -registerCallback h cb = do - result <- primIO (prim__registerCallback (webviewPtr h) cb) - pure $ case resultFromInt result of - Just Ok => Right () - Just err => Left err - Nothing => Left Error - where - resultFromInt : Bits32 -> Maybe Result - resultFromInt 0 = Just Ok - resultFromInt _ = Just Error - --------------------------------------------------------------------------------- --- Utility Functions --------------------------------------------------------------------------------- - -||| Check if library is initialized -export -%foreign "C:gossamer_is_initialized, libgossamer" -prim__isInitialized : Bits64 -> PrimIO Bits32 - -||| Check initialization status -export -isInitialized : WebviewHandle -> IO Bool -isInitialized h = do - result <- primIO (prim__isInitialized (webviewPtr h)) - pure (result /= 0) diff --git a/src/interface/Gossamer/ABI/Foreign.idr b/src/interface/Gossamer/ABI/Foreign.idr new file mode 120000 index 0000000..e9dcedb --- /dev/null +++ b/src/interface/Gossamer/ABI/Foreign.idr @@ -0,0 +1 @@ +../../abi/Foreign.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/Groove.idr b/src/interface/Gossamer/ABI/Groove.idr deleted file mode 100644 index 6453fe1..0000000 --- a/src/interface/Gossamer/ABI/Groove.idr +++ /dev/null @@ -1,527 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- -||| Gossamer Groove — Type-Safe Composable Service Discovery -||| -||| 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. -||| -||| The dependent type system guarantees: -||| 1. Safe connect — you cannot connect unless required capabilities are met -||| 2. Safe disconnect — linear types enforce proper cleanup (no dangling grooves) -||| 3. Safe compose — chaining grooves is provably sound -||| 4. No phantom capabilities — you cannot claim what you do not implement -||| -||| Architecture: -||| GrooveManifest — declares offered/consumed capabilities (plain value) -||| GrooveHandle — linear resource proving a live connection -||| GrooveComposition — proof that two grooves can be composed -||| -||| Discovery: services expose GET /.well-known/groove on their port. -||| The Zig FFI layer (groove.zig) probes these and constructs handles. -||| -||| This extends the existing Cap/ResourceKind pattern to inter-service -||| boundaries. Where Cap gates operations within a Gossamer app, -||| GrooveHandle gates operations between Gossamer and external services. - -module Gossamer.ABI.Groove - -import Gossamer.ABI.Types -import Data.So -import Data.List -import Data.List.Elem -import Data.Bits - -%default total - --------------------------------------------------------------------------------- --- Capability Types --------------------------------------------------------------------------------- - -||| Standard capability types that groove services can offer or consume. -||| Each type corresponds to a well-defined protocol interface. -public export -data CapabilityType : Type where - ||| WebRTC voice channels (Burble) - Voice : CapabilityType - ||| Real-time text messaging (Burble) - Text : CapabilityType - ||| User presence and speaking indicators (Burble) - Presence : CapabilityType - ||| Positional audio for spatial environments (Burble) - SpatialAudio : CapabilityType - ||| Server-side voice recording (Burble) - Recording : CapabilityType - ||| Text-to-speech synthesis (Burble) - TTS : CapabilityType - ||| Speech-to-text transcription (Burble) - STT : CapabilityType - ||| Cryptographic hash chain verification (Vext) - Integrity : CapabilityType - ||| Chronological feed verification (Vext) - FeedVerify : CapabilityType - ||| Merkle tree operations (Vext) - HashChain : CapabilityType - ||| Digital signature attestation (Vext/Avow) - Attestation : CapabilityType - ||| 8-modal entity storage (VeriSimDB) - OctadStorage : CapabilityType - ||| Cross-modal drift detection (VeriSimDB) - DriftDetection : CapabilityType - ||| Temporal version tracking (VeriSimDB) - TemporalVer : CapabilityType - ||| Neurosymbolic security scanning (Hypatia) - Scanning : CapabilityType - ||| Panel-based UI (PanLL) - PanelUI : CapabilityType - ||| Bot orchestration (gitbot-fleet) - BotOrch : CapabilityType - ||| Workflow automation (RPA Elysium) - Workflow : CapabilityType - ||| DNS record verification (rrecord-verity) - DNSVerify : CapabilityType - ||| Configuration orchestration (conflow) - ConfigOrch : CapabilityType - ||| Static analysis (panic-attacker) - StaticAnalysis : CapabilityType - ||| Theorem proving (ECHIDNA) - TheoremProve : CapabilityType - ||| Custom capability (extensible) - Custom : (name : String) -> CapabilityType - -||| Decidable equality for CapabilityType. -||| Required for Subset proofs. -public export -Eq CapabilityType where - Voice == Voice = True - Text == Text = True - Presence == Presence = True - SpatialAudio == SpatialAudio = True - Recording == Recording = True - TTS == TTS = True - STT == STT = True - Integrity == Integrity = True - FeedVerify == FeedVerify = True - HashChain == HashChain = True - Attestation == Attestation = True - OctadStorage == OctadStorage = True - DriftDetection == DriftDetection = True - TemporalVer == TemporalVer = True - Scanning == Scanning = True - PanelUI == PanelUI = True - BotOrch == BotOrch = True - Workflow == Workflow = True - DNSVerify == DNSVerify = True - ConfigOrch == ConfigOrch = True - StaticAnalysis == StaticAnalysis = True - TheoremProve == TheoremProve = True - (Custom a) == (Custom b) = a == b - _ == _ = False - -||| Convert capability type to its wire name (for JSON manifests). -public export -capabilityName : CapabilityType -> String -capabilityName Voice = "voice" -capabilityName Text = "text" -capabilityName Presence = "presence" -capabilityName SpatialAudio = "spatial-audio" -capabilityName Recording = "recording" -capabilityName TTS = "tts" -capabilityName STT = "stt" -capabilityName Integrity = "integrity" -capabilityName FeedVerify = "feed-verification" -capabilityName HashChain = "hash-chain" -capabilityName Attestation = "attestation" -capabilityName OctadStorage = "octad-storage" -capabilityName DriftDetection = "drift-detection" -capabilityName TemporalVer = "temporal-versioning" -capabilityName Scanning = "scanning" -capabilityName PanelUI = "panel-ui" -capabilityName BotOrch = "bot-orchestration" -capabilityName Workflow = "workflow" -capabilityName DNSVerify = "dns-verify" -capabilityName ConfigOrch = "config-orchestration" -capabilityName StaticAnalysis = "static-analysis" -capabilityName TheoremProve = "theorem-proving" -capabilityName (Custom n) = n - --------------------------------------------------------------------------------- --- Wire Protocol Types --------------------------------------------------------------------------------- - -||| Wire protocols for groove communication. -public export -data WireProtocol : Type where - WebRTC : WireProtocol - WebSocket : WireProtocol - HTTP : WireProtocol - GRPC : WireProtocol - NNTPS : WireProtocol - --------------------------------------------------------------------------------- --- Capability Sets (Type-Level) --------------------------------------------------------------------------------- - -||| A capability set is a list of capability types. -||| Used at the type level to parameterise groove manifests and handles. -public export -CapSet : Type -CapSet = List CapabilityType - -||| Proof that one capability set is a subset of another. -||| This is the core safety mechanism: you cannot connect a groove -||| unless your requirements are a subset of what the target offers. -public export -data IsSubset : (required : CapSet) -> (offered : CapSet) -> Type where - ||| Empty set is subset of anything. - SubNil : IsSubset [] offered - ||| If cap is in offered, and rest is subset of offered, - ||| then (cap :: rest) is subset of offered. - SubCons : {auto elemPrf : Elem cap offered} - -> IsSubset rest offered - -> IsSubset (cap :: rest) offered - -||| Check at runtime whether a capability list is subset of another. -||| Returns a decision — proof if true, refutation if false. -public export -checkSubset : (required : CapSet) -> (offered : CapSet) -> Bool -checkSubset [] _ = True -checkSubset (r :: rs) offered = - case elem r offered of - True => checkSubset rs offered - False => False - --------------------------------------------------------------------------------- --- Groove Manifest (Plain Value) --------------------------------------------------------------------------------- - -||| A groove manifest declares what a service offers and what it consumes. -||| This is a PLAIN VALUE — not a resource. Can be freely copied and serialised. -||| -||| The offers and consumes fields are type-level CapSets, enabling -||| compile-time verification of groove compatibility. -public export -record GrooveManifest (offers : CapSet) (consumes : CapSet) where - constructor MkManifest - ||| Service identifier (e.g. "burble", "vext", "verisimdb") - serviceId : String - ||| Service version (semver) - serviceVersion : String - ||| Port number for groove discovery - port : Bits16 - ||| Health check endpoint path - healthPath : String - -||| Well-known service manifests. -||| These define the CANONICAL capability sets for core services. -||| Any implementation claiming to be "burble" MUST offer these capabilities. - -||| Burble: voice-first communication platform. -public export -burbleManifest : GrooveManifest - [Voice, Text, Presence, SpatialAudio, Recording, TTS, STT] - [Integrity, OctadStorage, Scanning] -burbleManifest = MkManifest "burble" "0.1.0" 6473 "/health" - -||| Vext: verifiable communications protocol. -public export -vextManifest : GrooveManifest - [Integrity, FeedVerify, HashChain, Attestation] - [Voice, Text, OctadStorage] -vextManifest = MkManifest "vext" "0.1.0" 6480 "/health" - -||| VeriSimDB: cross-modal entity consistency engine. -public export -verisimdbManifest : GrooveManifest - [OctadStorage, DriftDetection, TemporalVer] - [Scanning] -verisimdbManifest = MkManifest "verisimdb" "0.1.0" 8080 "/health" - -||| Hypatia: neurosymbolic CI/CD intelligence. -public export -hypatiaManifest : GrooveManifest - [Scanning, StaticAnalysis] - [OctadStorage, Workflow] -hypatiaManifest = MkManifest "hypatia" "0.1.0" 9090 "/health" - -||| PanLL: neurosymbolic panel workspace. -public export -panllManifest : GrooveManifest - [PanelUI] - [Voice, Text, Presence, Integrity, OctadStorage, Scanning] -panllManifest = MkManifest "panll" "0.1.0" 8000 "/health" - -||| ECHIDNA: neurosymbolic theorem prover. -public export -echidnaManifest : GrooveManifest - [TheoremProve] - [OctadStorage, Scanning] -echidnaManifest = MkManifest "echidna" "0.1.0" 9000 "/health" - -||| RPA Elysium: robotic process automation. -public export -rpaManifest : GrooveManifest - [Workflow] - [Voice, Text, OctadStorage, Scanning] -rpaManifest = MkManifest "rpa-elysium" "0.1.0" 7800 "/health" - -||| Conflow: configuration orchestration. -public export -conflowManifest : GrooveManifest - [ConfigOrch] - [OctadStorage] -conflowManifest = MkManifest "conflow" "0.1.0" 7700 "/health" - -||| Panic-attacker: universal static analysis. -public export -panicManifest : GrooveManifest - [StaticAnalysis] - [OctadStorage, Workflow] -panicManifest = MkManifest "panic-attack" "0.1.0" 7600 "/health" - -||| Gitbot-fleet: automated bot coordination. -public export -gitbotManifest : GrooveManifest - [BotOrch] - [Scanning, Workflow, OctadStorage] -gitbotManifest = MkManifest "gitbot-fleet" "0.1.0" 8080 "/health" - --------------------------------------------------------------------------------- --- Groove Handle (Linear Resource) --------------------------------------------------------------------------------- - -||| A live connection to a grooved service. -||| -||| This is a LINEAR resource: it must be disconnected exactly once. -||| The type parameters carry: -||| - offers: what the connected service provides -||| - consumes: what the connected service wants from us -||| -||| You can only create a GrooveHandle by successfully probing a service -||| and verifying that its manifest satisfies your requirements. -public export -data GrooveHandle : (offers : CapSet) -> (consumes : CapSet) -> Type where - MkGroove : (ptr : Bits64) - -> {auto 0 nonNull : So (ptr /= 0)} - -> GrooveHandle offers consumes - -||| Safely create a GrooveHandle from a raw pointer. -||| Returns Nothing if the pointer is null. -public export -createGroove : Bits64 -> Maybe (GrooveHandle offers consumes) -createGroove ptr = - case choose (ptr /= 0) of - Left ok => Just (MkGroove ptr) - Right _ => Nothing - -||| Extract raw pointer from groove handle (for FFI calls). -public export -groovePtr : GrooveHandle offers consumes -> Bits64 -groovePtr (MkGroove ptr) = ptr - --------------------------------------------------------------------------------- --- Groove Composition (Type-Safe) --------------------------------------------------------------------------------- - -||| Proof that two grooves can be composed. -||| -||| Service A offers caps that service B consumes, AND -||| service B offers caps that service A consumes. -||| This is the mathematical guarantee that composing them is sound. -||| -||| Example: Burble offers [Voice, Text], Vext consumes [Voice, Text] ✓ -||| Vext offers [Integrity], Burble consumes [Integrity] ✓ -||| Therefore Burble ↔ Vext composition is sound. -public export -data GrooveCompat : (aOffers : CapSet) -> (aConsumes : CapSet) - -> (bOffers : CapSet) -> (bConsumes : CapSet) - -> Type where - MkCompat : {auto aFeedsB : IsSubset bConsumes aOffers} - -> {auto bFeedsA : IsSubset aConsumes bOffers} - -> GrooveCompat aOffers aConsumes bOffers bConsumes - -||| Runtime compatibility check between two manifests. -||| Returns True if both sides can satisfy each other's requirements. -||| Takes the capability sets as explicit arguments since the record's -||| type parameters are erased at runtime. -public export -isCompatible : (aOff, aCon, bOff, bCon : CapSet) - -> GrooveManifest aOff aCon -> GrooveManifest bOff bCon -> Bool -isCompatible aOff aCon bOff bCon _ _ = - checkSubset bCon aOff && checkSubset aCon bOff - -||| A composed groove pair — two handles that have been verified compatible. -||| Both handles are linear and must be individually disconnected. -public export -record GroovePair where - constructor MkPair - leftPtr : Bits64 - rightPtr : Bits64 - --------------------------------------------------------------------------------- --- Groove Discovery Result --------------------------------------------------------------------------------- - -||| Result of probing a groove target. -public export -data GrooveProbeResult : Type where - ||| Service not found at expected port. - NotFound : GrooveProbeResult - ||| Service found but manifest is malformed or incompatible. - Incompatible : (reason : String) -> GrooveProbeResult - ||| Service found and connected. Provides offers/consumes info. - Connected : (serviceId : String) - -> (version : String) - -> (offeredCaps : List String) - -> (consumedCaps : List String) - -> GrooveProbeResult - -||| Convert probe result to a status code for the FFI boundary. -public export -probeResultToStatus : GrooveProbeResult -> Bits32 -probeResultToStatus NotFound = 0 -probeResultToStatus (Incompatible _) = 1 -probeResultToStatus (Connected _ _ _ _) = 2 - --------------------------------------------------------------------------------- --- Groove Triad (Burble + Vext + Avow) --------------------------------------------------------------------------------- - -||| The Burble verification triad: three grooves that together provide -||| full communication integrity. -||| -||| - Burble: voice + text transport -||| - Vext: hash chain integrity (messages are chronological, uninjected) -||| - Avow: consent attestation (permissions formally verified) -||| -||| When all three are grooved, communications have: -||| 1. Low-latency delivery (Burble WebRTC) -||| 2. Cryptographic proof of integrity (Vext Merkle trees) -||| 3. Formal proof of consent (Avow Idris2 proofs) -public export -record VerificationTriad where - constructor MkTriad - ||| Burble groove handle (voice + text) - burble : Bits64 - ||| Vext groove handle (integrity) - vext : Bits64 - ||| Whether Avow attestation is available - avow : Bool - -||| Check if the full triad is active. -public export -isTriadComplete : VerificationTriad -> Bool -isTriadComplete t = t.burble /= 0 && t.vext /= 0 && t.avow - --------------------------------------------------------------------------------- --- Applicability Levels --------------------------------------------------------------------------------- - -||| Groove applicability — what scale of interaction this groove supports. -||| A groove can work at multiple levels simultaneously. -public export -data Applicability : Type where - ||| Single user, local tools (e.g. panic-attacker, empty-linter) - Individual : Applicability - ||| Small team collaboration (e.g. Burble voice, VeriSimDB) - Team : Applicability - ||| Large-scale open participation (e.g. Vext feeds, civic-connect) - MassiveOpen : Applicability - -||| Services can declare multiple applicability levels. -public export -ApplicabilitySet : Type -ApplicabilitySet = List Applicability - --------------------------------------------------------------------------------- --- Groove Handshake Termination --------------------------------------------------------------------------------- - -||| States in the groove handshake protocol. -||| -||| The handshake goes: -||| Idle -> Probing -> ManifestReceived -> CapabilityCheck -> Connected -||| -> Rejected (terminal) -||| -> Rejected (terminal) -||| -||| The protocol must terminate: every state either transitions forward -||| or reaches a terminal state. No cycles are possible. -public export -data HandshakeState : Type where - ||| Initial state — no connection attempted. - HSIdle : HandshakeState - ||| TCP connection established, HTTP GET sent. - HSProbing : HandshakeState - ||| Manifest JSON received and parsed. - HSManifestReceived : HandshakeState - ||| Capability subset check in progress. - HSCapabilityCheck : HandshakeState - ||| Handshake completed successfully. - HSConnected : HandshakeState - ||| Handshake failed (terminal state). - HSRejected : HandshakeState - -||| Valid transitions in the handshake protocol. -||| The transitions form a DAG (no cycles), guaranteeing termination. -public export -data HandshakeTransition : HandshakeState -> HandshakeState -> Type where - ||| Begin probing from idle. - BeginProbe : HandshakeTransition HSIdle HSProbing - ||| Receive manifest from probe. - ReceiveManifest : HandshakeTransition HSProbing HSManifestReceived - ||| Probe failed (network error, no manifest). - ProbeFailed : HandshakeTransition HSProbing HSRejected - ||| Begin capability check after receiving manifest. - BeginCapCheck : HandshakeTransition HSManifestReceived HSCapabilityCheck - ||| Manifest is malformed. - ManifestBad : HandshakeTransition HSManifestReceived HSRejected - ||| Capability check passed — connect. - CapCheckOk : HandshakeTransition HSCapabilityCheck HSConnected - ||| Capability check failed — reject. - CapCheckFail : HandshakeTransition HSCapabilityCheck HSRejected - -||| Proof: HSConnected is terminal (no outgoing transitions). -||| There are no HandshakeTransition constructors with source HSConnected. -public export -connectedIsTerminal : HandshakeTransition HSConnected s -> Void -connectedIsTerminal _ impossible - -||| Proof: HSRejected is terminal (no outgoing transitions). -||| There are no HandshakeTransition constructors with source HSRejected. -public export -rejectedIsTerminal : HandshakeTransition HSRejected s -> Void -rejectedIsTerminal _ impossible - -||| Proof: the handshake strictly decreases a ranking function. -||| -||| We assign ranks: Idle=5, Probing=4, ManifestReceived=3, -||| CapabilityCheck=2, Connected=0, Rejected=0. -||| Every valid transition moves to a strictly lower rank. -||| Since ranks are bounded natural numbers, the handshake terminates. -public export -handshakeRank : HandshakeState -> Nat -handshakeRank HSIdle = 5 -handshakeRank HSProbing = 4 -handshakeRank HSManifestReceived = 3 -handshakeRank HSCapabilityCheck = 2 -handshakeRank HSConnected = 0 -handshakeRank HSRejected = 0 - -||| Every handshake transition strictly decreases the rank. -public export -transitionDecreases : (t : HandshakeTransition from to) - -> LTE (S (handshakeRank to)) (handshakeRank from) --- Rank table: HSIdle 5, HSProbing 4, HSManifestReceived 3, --- HSCapabilityCheck 2, HSConnected 0, HSRejected 0. Goal is --- `LTE (S rank[to]) rank[from]`. The `-> HSRejected/HSConnected` --- (rank 0) transitions need `LTE 1 k = LTESucc LTEZero`, NOT the --- `LTE k k` terms the pre-compile draft carried (those were latent --- type errors masked by the earlier `lteRefl` scope failure). -transitionDecreases BeginProbe = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))) -- LTE 5 5 (HSIdle→HSProbing) -transitionDecreases ReceiveManifest = LTESucc (LTESucc (LTESucc (LTESucc LTEZero))) -- LTE 4 4 (HSProbing→HSManifestReceived) -transitionDecreases ProbeFailed = LTESucc LTEZero -- LTE 1 4 (HSProbing→HSRejected) -transitionDecreases BeginCapCheck = LTESucc (LTESucc (LTESucc LTEZero)) -- LTE 3 3 (HSManifestReceived→HSCapabilityCheck) -transitionDecreases ManifestBad = LTESucc LTEZero -- LTE 1 3 (HSManifestReceived→HSRejected) -transitionDecreases CapCheckOk = LTESucc LTEZero -- LTE 1 2 (HSCapabilityCheck→HSConnected) -transitionDecreases CapCheckFail = LTESucc LTEZero -- LTE 1 2 (HSCapabilityCheck→HSRejected) diff --git a/src/interface/Gossamer/ABI/Groove.idr b/src/interface/Gossamer/ABI/Groove.idr new file mode 120000 index 0000000..90298de --- /dev/null +++ b/src/interface/Gossamer/ABI/Groove.idr @@ -0,0 +1 @@ +../../abi/Groove.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/GrooveLinearity.idr b/src/interface/Gossamer/ABI/GrooveLinearity.idr new file mode 120000 index 0000000..195f051 --- /dev/null +++ b/src/interface/Gossamer/ABI/GrooveLinearity.idr @@ -0,0 +1 @@ +../../abi/GrooveLinearity.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/GrooveTermination.idr b/src/interface/Gossamer/ABI/GrooveTermination.idr deleted file mode 100644 index 1097103..0000000 --- a/src/interface/Gossamer/ABI/GrooveTermination.idr +++ /dev/null @@ -1,261 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- -||| Groove Protocol Handshake Termination Proof -||| -||| Proves that the Groove capability negotiation protocol terminates -||| and produces a valid capability set (no privilege escalation). -||| -||| The Groove handshake is a finite-state protocol: -||| 1. Initiator sends manifest (offers + consumes) -||| 2. Responder checks subset compatibility -||| 3. If compatible, responder sends acceptance + its manifest -||| 4. Initiator verifies mutual compatibility -||| 5. Connection established or rejected -||| -||| Key properties proved: -||| 1. Termination: the handshake completes in at most 4 message exchanges. -||| 2. No privilege escalation: the negotiated capability set is a subset -||| of both parties' declared offers. -||| 3. Mutual satisfaction: both parties' requirements are met. -||| 4. Determinism: the same inputs always produce the same result. -||| -||| Zero believe_me. All proofs are constructive. -||| -||| ## Relationship with `Gossamer.ABI.Groove` -||| -||| `Gossamer.ABI.Groove` models the runtime handshake at the -||| network-protocol level: 6 states (`HSIdle` … `HSConnected` / `HSRejected`) -||| connected by 7 `HandshakeTransition`s, with termination established via -||| a strictly-decreasing rank function (`handshakeRank`). -||| -||| This module proves the **bounded-length** termination property in -||| a complementary, trace-based style: 6 abstract states -||| (`Init` … `Connected` / `Rejected`) connected by 6 `TermStep`s, with -||| termination established by exhaustive case analysis on a closed-form -||| `TermTrace` (every path has length ≤ 4). The two models are not -||| isomorphic — Groove distinguishes `HSProbing` / `HSManifestReceived` / -||| `HSCapabilityCheck` while this proof collapses them to `ManifestSent` / -||| `Replied`. Both abstractions are sound; this one is the right tool for -||| the bounded-length argument and the no-escalation / determinism -||| corollaries. -||| -||| To avoid namespace ambiguity with Groove's `HandshakeState` / -||| `connectedIsTerminal` / `rejectedIsTerminal`, the symbols local to -||| this proof carry a `Term` prefix (`TermState`, `TermStep`, `TermTrace`, -||| `termConnectedTerminal`, `termRejectedTerminal`, ...). - -module Gossamer.ABI.GrooveTermination - -import Gossamer.ABI.Types -import Gossamer.ABI.Groove -import Data.So -import Data.Nat -import Data.List -import Data.List.Elem - -%default total - --------------------------------------------------------------------------------- --- Handshake States (termination-proof abstraction) --------------------------------------------------------------------------------- - -||| States of the Groove handshake protocol — termination-proof abstraction. -||| The protocol is a strict sequence — no loops, no backward transitions. -||| -||| Distinct from `Gossamer.ABI.Groove.HandshakeState` (the runtime model); -||| see the moduledoc for the relationship. -public export -data TermState : Type where - ||| Initial state — no messages exchanged yet. - Init : TermState - ||| Initiator has sent its manifest. - ManifestSent : TermState - ||| Responder has checked compatibility and replied. - Replied : TermState - ||| Initiator has verified mutual compatibility. - Verified : TermState - ||| Terminal: connection established. - Connected : TermState - ||| Terminal: handshake rejected (incompatible). - Rejected : TermState - -||| Valid transitions in the handshake protocol. -||| Each constructor witnesses a single step. There are exactly 4 possible -||| steps from Init to a terminal state, proving bounded execution. -public export -data TermStep : TermState -> TermState -> Type where - ||| Step 1: Initiator sends manifest. - SendManifest : TermStep Init ManifestSent - ||| Step 2a: Responder accepts (requirements satisfied). - AcceptReply : TermStep ManifestSent Replied - ||| Step 2b: Responder rejects (requirements not satisfied). - RejectReply : TermStep ManifestSent Rejected - ||| Step 3a: Initiator verifies mutual compatibility. - VerifyMutual : TermStep Replied Verified - ||| Step 3b: Initiator finds incompatibility. - RejectMutual : TermStep Replied Rejected - ||| Step 4: Verified handshake establishes connection. - Establish : TermStep Verified Connected - -||| Proof that Connected is a terminal state — no valid step from it. -public export -termConnectedTerminal : TermStep Connected s -> Void -termConnectedTerminal _ impossible - -||| Proof that Rejected is a terminal state — no valid step from it. -public export -termRejectedTerminal : TermStep Rejected s -> Void -termRejectedTerminal _ impossible - --------------------------------------------------------------------------------- --- Handshake Trace (Execution History) --------------------------------------------------------------------------------- - -||| A trace of handshake steps from state `start` to state `end`. -||| The length of the trace is bounded by construction — at most 4 steps. -public export -data TermTrace : TermState -> TermState -> Type where - ||| Zero steps: already at the target state. - Done : TermTrace s s - ||| One step followed by more steps. - Step : TermStep s mid -> TermTrace mid end -> TermTrace s end - -||| Count the number of steps in a trace. -public export -termLength : TermTrace s e -> Nat -termLength Done = 0 -termLength (Step _ rest) = S (termLength rest) - --------------------------------------------------------------------------------- --- Termination Proof --------------------------------------------------------------------------------- - -||| A complete handshake trace from Init to a terminal state. -public export -data TermCompleted : Type where - ||| Handshake succeeded — connection established. - TermSuccess : TermTrace Init Connected -> TermCompleted - ||| Handshake failed — rejected at some point. - TermFailure : TermTrace Init Rejected -> TermCompleted - -||| The successful handshake path: Init -> ManifestSent -> Replied -> Verified -> Connected. -||| Exactly 4 steps. -public export -termSuccessPath : TermTrace Init Connected -termSuccessPath = Step SendManifest - $ Step AcceptReply - $ Step VerifyMutual - $ Step Establish - $ Done - -||| Rejection at responder: Init -> ManifestSent -> Rejected. -||| Exactly 2 steps. -public export -termRejectAtResponder : TermTrace Init Rejected -termRejectAtResponder = Step SendManifest - $ Step RejectReply - $ Done - -||| Rejection at initiator verification: Init -> ManifestSent -> Replied -> Rejected. -||| Exactly 3 steps. -public export -termRejectAtVerify : TermTrace Init Rejected -termRejectAtVerify = Step SendManifest - $ Step AcceptReply - $ Step RejectMutual - $ Done - -||| Proof: the successful handshake takes exactly 4 steps. -public export -termSuccessIs4Steps : termLength GrooveTermination.termSuccessPath = 4 -termSuccessIs4Steps = Refl - -||| Proof: responder rejection takes exactly 2 steps. -public export -termResponderRejectIs2Steps : termLength GrooveTermination.termRejectAtResponder = 2 -termResponderRejectIs2Steps = Refl - -||| Proof: initiator rejection takes exactly 3 steps. -public export -termVerifyRejectIs3Steps : termLength GrooveTermination.termRejectAtVerify = 3 -termVerifyRejectIs3Steps = Refl - -||| Proof: ALL possible handshake paths terminate in at most 4 steps. -||| This is proved by exhaustive case analysis — the 3 possible paths -||| have lengths 4, 2, and 3 respectively. -||| Length of a completed handshake's trace (top-level so it can appear -||| in `termAllPathsBounded`'s type — a `where` block cannot, which was the -||| original parse failure). -public export -termCompletedLength : TermCompleted -> Nat -termCompletedLength (TermSuccess trace) = termLength trace -termCompletedLength (TermFailure trace) = termLength trace - -public export -termAllPathsBounded : (h : TermCompleted) -> LTE (termCompletedLength h) 4 -termAllPathsBounded (TermSuccess trace) = boundSuccess trace - where - boundSuccess : (t : TermTrace Init Connected) -> LTE (termLength t) 4 - boundSuccess (Step SendManifest (Step AcceptReply (Step VerifyMutual (Step Establish Done)))) = LTESucc (LTESucc (LTESucc (LTESucc LTEZero))) - -- Reject branches cannot end at Connected: Rejected has no outgoing - -- TermStep (`termRejectedTerminal`), so any `TermTrace Rejected Connected` - -- is uninhabited. Impossible clauses make the coverage explicit. - boundSuccess (Step SendManifest (Step RejectReply Done)) impossible - boundSuccess (Step SendManifest (Step RejectReply (Step _ _))) impossible - boundSuccess (Step SendManifest (Step AcceptReply (Step RejectMutual Done))) impossible - boundSuccess (Step SendManifest (Step AcceptReply (Step RejectMutual (Step _ _)))) impossible -termAllPathsBounded (TermFailure trace) = boundFailure trace - where - boundFailure : (t : TermTrace Init Rejected) -> LTE (termLength t) 4 - boundFailure (Step SendManifest (Step RejectReply Done)) = LTESucc (LTESucc LTEZero) - boundFailure (Step SendManifest (Step AcceptReply (Step RejectMutual Done))) = LTESucc (LTESucc (LTESucc LTEZero)) - -- Establish ends at Connected, not Rejected: any `TermTrace Connected - -- Rejected` is uninhabited (`termConnectedTerminal`). - boundFailure (Step SendManifest (Step AcceptReply (Step VerifyMutual (Step Establish Done)))) impossible - boundFailure (Step SendManifest (Step AcceptReply (Step VerifyMutual (Step Establish (Step _ _))))) impossible - --------------------------------------------------------------------------------- --- No Privilege Escalation --------------------------------------------------------------------------------- - -||| Proof that a successful handshake produces capabilities that are -||| subsets of both parties' offers. -||| -||| After negotiation: -||| - What the initiator gets ⊆ what the responder offers -||| - What the responder gets ⊆ what the initiator offers -||| This is a direct consequence of the GrooveCompat type from Groove.idr. -public export -data NegotiatedSafely : (iOffers, iConsumes, rOffers, rConsumes : CapSet) -> Type where - MkSafe : GrooveCompat iOffers iConsumes rOffers rConsumes - -> NegotiatedSafely iOffers iConsumes rOffers rConsumes - -||| The negotiation result is exactly the intersection of needs and offers. -||| No party receives capabilities they did not request. -||| No party provides capabilities they did not declare. -public export -noEscalation : NegotiatedSafely iOff iCon rOff rCon - -> (IsSubset rCon iOff, IsSubset iCon rOff) -noEscalation (MkSafe (MkCompat {aFeedsB} {bFeedsA})) = (aFeedsB, bFeedsA) - --------------------------------------------------------------------------------- --- Determinism --------------------------------------------------------------------------------- - -||| Proof that the handshake outcome is deterministic given the same manifests. -||| -||| If two handshake attempts start with the same manifests, they reach -||| the same terminal state. This follows from checkSubset being a pure -||| function with no side effects. -public export -data Deterministic : Type where - ||| Given two subset checks on the same inputs, they produce the same Bool. - MkDeterministic : (req, off : CapSet) - -> checkSubset req off = checkSubset req off - -> Deterministic - -||| Trivially, the same pure function on the same inputs yields the same result. -public export -handshakeIsDeterministic : (req, off : CapSet) -> Deterministic -handshakeIsDeterministic req off = MkDeterministic req off Refl diff --git a/src/interface/Gossamer/ABI/GrooveTermination.idr b/src/interface/Gossamer/ABI/GrooveTermination.idr new file mode 120000 index 0000000..208121b --- /dev/null +++ b/src/interface/Gossamer/ABI/GrooveTermination.idr @@ -0,0 +1 @@ +../../abi/GrooveTermination.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/HandleLinearity.idr b/src/interface/Gossamer/ABI/HandleLinearity.idr deleted file mode 100644 index cc037a6..0000000 --- a/src/interface/Gossamer/ABI/HandleLinearity.idr +++ /dev/null @@ -1,304 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- -||| Handle Linearity Proofs for Gossamer -||| -||| Proves that connection handles (webview, channel, groove, capability) -||| cannot be duplicated, must be consumed exactly once, and follow a -||| valid state machine lifecycle. -||| -||| Builds on the linear resource types in Types.idr and Groove.idr. -||| The existing WebviewHandle, Channel, GrooveHandle, and Cap types are -||| already parameterised with non-null proofs. This module adds: -||| -||| 1. Uniqueness: a handle token cannot produce two live handles. -||| 2. Lifecycle state machine: handles must transition through valid states. -||| 3. Consumption proof: a consumed handle cannot be reused. -||| 4. No-clone: there is no function that duplicates a handle. -||| -||| Zero believe_me. All proofs are constructive. - -module Gossamer.ABI.HandleLinearity - -import Gossamer.ABI.Types -import Gossamer.ABI.Groove -import Data.So -import Data.Bits - -%default total - --------------------------------------------------------------------------------- --- Handle Tokens --------------------------------------------------------------------------------- - -||| A raw handle token (the Bits64 pointer value). -||| Used as the identity for uniqueness tracking. -public export -HandleToken : Type -HandleToken = Bits64 - -||| Proof that a handle token is valid (non-null). -public export -data ValidToken : (token : HandleToken) -> Type where - MkValid : {token : HandleToken} - -> {auto 0 nonNull : So (token /= 0)} - -> ValidToken token - -||| Safely construct a validity proof. -public export -checkValid : (token : HandleToken) -> Maybe (ValidToken token) -checkValid token = - case choose (token /= 0) of - Left ok => Just (MkValid {token}) - Right _ => Nothing - -||| Recover the (erased) non-null witness carried by each handle's -||| constructor as a `ValidToken` for its raw token. The witness already -||| exists inside the handle — `MkWebview`/`MkGroove`/`MkChannel`/`MkCap` -||| each require `So (ptr /= 0)` at construction — but the `*Ptr`/`capToken` -||| projections discard it. These accessors re-expose it so allocation is -||| total and sound (no runtime null re-check needed). -public export -webviewValid : (wv : WebviewHandle) -> ValidToken (webviewPtr wv) -webviewValid (MkWebview ptr {nonNull}) = MkValid {nonNull} - -public export -grooveValid : (gh : GrooveHandle offers consumes) -> ValidToken (groovePtr gh) -grooveValid (MkGroove ptr {nonNull}) = MkValid {nonNull} - -public export -channelValid : (ch : Channel req resp) -> ValidToken (channelPtr ch) -channelValid (MkChannel ptr {nonNull}) = MkValid {nonNull} - -public export -capValid : (cap : Cap resource) -> ValidToken (capToken cap) -capValid (MkCap token {nonNull}) = MkValid {nonNull} - --------------------------------------------------------------------------------- --- Handle Lifecycle States --------------------------------------------------------------------------------- - -||| Abstract lifecycle states for any handle type. -||| Every handle in Gossamer follows this state machine: -||| -||| Allocated -> Active -> Consumed -||| -||| There is no transition from Consumed to any other state. -||| There is no transition from Active back to Allocated. -public export -data HandleState : Type where - ||| Handle has been allocated but not yet activated. - Allocated : HandleState - ||| Handle is active (in use). - Active : HandleState - ||| Handle has been consumed (freed/closed/disconnected). - Consumed : HandleState - -||| Valid transitions in the handle lifecycle. -public export -data ValidHandleTransition : HandleState -> HandleState -> Type where - ||| Allocated handles can be activated. - Activate : ValidHandleTransition Allocated Active - ||| Active handles can be consumed. - Consume : ValidHandleTransition Active Consumed - ||| Allocated handles can be directly consumed (e.g. error cleanup). - DiscardAllocated : ValidHandleTransition Allocated Consumed - -||| Proof that Consumed is a terminal state. -||| There is no valid transition from Consumed to any state. -||| This is proved by exhaustive case analysis: the only constructors -||| of ValidHandleTransition have source states Allocated or Active. -public export -consumedIsTerminal : ValidHandleTransition Consumed s -> Void -consumedIsTerminal _ impossible - --------------------------------------------------------------------------------- --- Linear Handle Wrapper --------------------------------------------------------------------------------- - -||| A linearly-tracked handle. -||| -||| Parameterised by: -||| - `inner`: the underlying handle type (WebviewHandle, Channel, etc.) -||| - `state`: the current lifecycle state -||| -||| The state transitions are enforced at the type level. A function that -||| consumes a handle must accept `LinearHandle inner Active` and there is -||| no way to reconstruct an Active handle from a Consumed one. -public export -data LinearHandle : (inner : Type) -> (state : HandleState) -> Type where - ||| Wrap a raw handle with lifecycle tracking. - MkLinear : (handle : inner) - -> (token : HandleToken) - -> {auto 0 valid : ValidToken token} - -> LinearHandle inner state - -||| Extract the inner handle (for operations that borrow, not consume). -||| Only available on Active handles. -public export -borrow : LinearHandle inner Active -> inner -borrow (MkLinear handle _) = handle - -||| Extract the token from a linear handle. -public export -linearToken : LinearHandle inner state -> HandleToken -linearToken (MkLinear _ token) = token - -||| Transition a handle from one state to another. -||| Requires a valid transition proof. -public export -transition : LinearHandle inner from - -> ValidHandleTransition from to - -> LinearHandle inner to -transition (MkLinear handle token) _ = MkLinear handle token - -||| Activate an allocated handle. -public export -activate : LinearHandle inner Allocated -> LinearHandle inner Active -activate h = transition h Activate - -||| Consume an active handle. Returns the inner handle for final use -||| (e.g. passing to a destroy function). -public export -consume : LinearHandle inner Active -> (inner, LinearHandle inner Consumed) -consume h@(MkLinear handle token) = - (handle, transition h Consume) - --------------------------------------------------------------------------------- --- Uniqueness Proofs --------------------------------------------------------------------------------- - -||| Proof that two handles with the same token cannot both be Active. -||| -||| If handle A and handle B have the same token, and A is Active, -||| then B cannot also be Active. This models the single-ownership -||| invariant: each resource has exactly one live handle. -||| -||| In practice, this is enforced by construction: the only way to get -||| a LinearHandle is from the FFI create functions, which allocate -||| unique pointers. This type expresses the invariant formally. -public export -data UniqueActive : (tokenA : HandleToken) -> (tokenB : HandleToken) -> Type where - ||| If the tokens are the same, at most one handle is Active. - ||| The proof obligation is on the caller to ensure they do not - ||| hold two Active handles with the same token. - MkUnique : {auto 0 sameToken : So (tokenA == tokenB)} - -> UniqueActive tokenA tokenB - -||| Proof that consuming a handle invalidates its token. -||| -||| After consuming a handle, any other reference to the same token -||| is invalid. This is the formal statement of "use-after-free prevention". -public export -data ConsumedInvalidates : (consumed : LinearHandle inner Consumed) - -> (token : HandleToken) -> Type where - MkInvalidated : {consumed : LinearHandle inner Consumed} - -> {auto 0 sameToken : So (linearToken consumed == token)} - -> ConsumedInvalidates consumed token - --------------------------------------------------------------------------------- --- Webview Handle Linearity --------------------------------------------------------------------------------- - -||| A linearly-tracked webview handle. -||| Specialisation of LinearHandle for WebviewHandle. -public export -LinearWebview : HandleState -> Type -LinearWebview = LinearHandle WebviewHandle - -||| Create a linear webview handle from a raw WebviewHandle. -||| The handle starts in the Allocated state. -public export -allocateWebview : WebviewHandle -> LinearWebview Allocated -allocateWebview wv = MkLinear wv (webviewPtr wv) {valid = webviewValid wv} - -||| Run a webview (consuming it). -||| The handle transitions from Active to Consumed. -||| Returns the raw WebviewHandle for the final `run` FFI call. -public export -consumeForRun : LinearWebview Active -> (WebviewHandle, LinearWebview Consumed) -consumeForRun = consume - -||| Destroy a webview without running (consuming it). -||| The handle transitions from Active to Consumed. -public export -consumeForDestroy : LinearWebview Active -> (WebviewHandle, LinearWebview Consumed) -consumeForDestroy = consume - --------------------------------------------------------------------------------- --- Groove Handle Linearity --------------------------------------------------------------------------------- - -||| A linearly-tracked groove handle. -||| Specialisation of LinearHandle for GrooveHandle. -public export -LinearGroove : (offers : CapSet) -> (consumes : CapSet) -> HandleState -> Type -LinearGroove offers consumes = LinearHandle (GrooveHandle offers consumes) - -||| Allocate a linear groove handle. -public export -allocateGroove : GrooveHandle offers consumes - -> LinearGroove offers consumes Allocated -allocateGroove gh = MkLinear gh (groovePtr gh) {valid = grooveValid gh} - -||| Disconnect a groove (consuming it). -public export -consumeForDisconnect : LinearGroove offers consumes Active - -> (GrooveHandle offers consumes, LinearGroove offers consumes Consumed) -consumeForDisconnect = consume - --------------------------------------------------------------------------------- --- Channel Handle Linearity --------------------------------------------------------------------------------- - -||| A linearly-tracked IPC channel. -public export -LinearChannel : (req : Type) -> (resp : Type) -> HandleState -> Type -LinearChannel req resp = LinearHandle (Channel req resp) - -||| Allocate a linear channel. -public export -allocateChannel : Channel req resp -> LinearChannel req resp Allocated -allocateChannel ch = MkLinear ch (channelPtr ch) {valid = channelValid ch} - -||| Close a channel (consuming it). -public export -consumeForClose : LinearChannel req resp Active - -> (Channel req resp, LinearChannel req resp Consumed) -consumeForClose = consume - --------------------------------------------------------------------------------- --- Capability Handle Linearity --------------------------------------------------------------------------------- - -||| A linearly-tracked capability token. -public export -LinearCap : (resource : ResourceKind) -> HandleState -> Type -LinearCap resource = LinearHandle (Cap resource) - -||| Allocate a linear capability. -public export -allocateCap : Cap resource -> LinearCap resource Allocated -allocateCap cap = MkLinear cap (capToken cap) {valid = capValid cap} - -||| Revoke a capability (consuming it). -public export -consumeForRevoke : LinearCap resource Active - -> (Cap resource, LinearCap resource Consumed) -consumeForRevoke = consume - --------------------------------------------------------------------------------- --- Lifecycle Composition Proof --------------------------------------------------------------------------------- - -||| Proof that a complete lifecycle is sound. -||| -||| A handle that goes through Allocated -> Active -> Consumed -||| has been properly managed. This type witnesses the full lifecycle. -public export -data CompletedLifecycle : (inner : Type) -> Type where - MkCompleted : (allocated : LinearHandle inner Allocated) - -> (active : LinearHandle inner Active) - -> (consumed : LinearHandle inner Consumed) - -> {auto 0 tokensMatch : So (linearToken allocated == linearToken consumed)} - -> CompletedLifecycle inner diff --git a/src/interface/Gossamer/ABI/HandleLinearity.idr b/src/interface/Gossamer/ABI/HandleLinearity.idr new file mode 120000 index 0000000..cdd9e04 --- /dev/null +++ b/src/interface/Gossamer/ABI/HandleLinearity.idr @@ -0,0 +1 @@ +../../abi/HandleLinearity.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/IPCDispatch.idr b/src/interface/Gossamer/ABI/IPCDispatch.idr deleted file mode 100644 index d093eae..0000000 --- a/src/interface/Gossamer/ABI/IPCDispatch.idr +++ /dev/null @@ -1,288 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- -||| IPC Handler Type Safety Proof (GS2) -||| -||| Proves that the 25 core IPC dispatch handlers are type-safe: each handler -||| accepts only inputs of the correct type and produces outputs of the correct -||| type, and the dispatch function is total (no handler is silently dropped). -||| -||| The 25 handlers correspond to the named commands bound via -||| `gossamer_channel_bind` in the Gossamer Bridge. They are grouped by module: -||| -||| Shell (5): show, hide, minimize, maximize, restore -||| Bridge (2): open, close -||| Dialog (4): open_file, save_file, open_dir, open_multi -||| Filesystem (5): read_text, write_text, exists, list_dir, remove -||| Groove (7): discover, status, manifest, summary, send, recv, disconnect -||| Platform (2): platform_info, build_info -||| -||| Properties proved: -||| 1. Every handler has a declared input type and output type. -||| 2. The dispatch function covers all 25 handlers (total function; Idris2 -||| verifies no case is missing). -||| 3. Handler dispatch is injective: distinct commands map to distinct handlers. -||| 4. Capability-guarded handlers (Filesystem, ShellExec) require a capability -||| token; plain handlers (Dialog, Platform) do not. -||| -||| Zero believe_me. All proofs are constructive. - -module Gossamer.ABI.IPCDispatch - -import Gossamer.ABI.Types -import Gossamer.ABI.Groove - -%default total - --------------------------------------------------------------------------------- --- IPC Input/Output Types --------------------------------------------------------------------------------- - -||| Abstract representation of the types that flow through the IPC channel. -||| These correspond to the JSON-serialised request/response payloads that -||| the frontend (JavaScript) sends to and receives from the Ephapax backend. -public export -data IpcType - = IpcUnit -- () — no payload - | IpcString -- String — path, URL, HTML, JS snippet, title - | IpcI32 -- Int32 — result code, width, height - | IpcBool -- Boolean — exists?, success? - | IpcStringList -- List String — directory entries, filter patterns - | IpcPlatformInfo -- { platform, engine, version, arch } record - | IpcGrooveStatus -- { target_id, connected, protocol_version } record - | IpcCapToken -- capability token (opaque Bits64) - -||| The IPC "type signature" of a handler: its input payload type and output type. -public export -record HandlerSig where - constructor MkSig - inputType : IpcType - outputType : IpcType - --------------------------------------------------------------------------------- --- The 25 IPC Commands --------------------------------------------------------------------------------- - -||| Every named IPC command that can be bound via `gossamer_channel_bind`. -||| -||| Grouped by module. Total count: 25. -public export -data IpcCommand - -- Shell (5) — window visual state management - = CmdShow -- gossamer_show: () → I32 (result) - | CmdHide -- gossamer_hide: () → I32 - | CmdMinimize -- gossamer_minimize: () → I32 - | CmdMaximize -- gossamer_maximize: () → I32 - | CmdRestore -- gossamer_restore: () → I32 - - -- Bridge (2) — IPC channel lifecycle - | CmdChannelOpen -- gossamer_channel_open: () → I32 (channel handle id) - | CmdChannelClose -- gossamer_channel_close: () → () - - -- Dialog (4) — native file picker dialogs - | CmdDialogOpen -- gossamer_dialog_open: String (filter) → String (path) - | CmdDialogSave -- gossamer_dialog_save: String (filter) → String (path) - | CmdDialogOpenDir -- gossamer_dialog_open_directory: () → String - | CmdDialogMulti -- gossamer_dialog_open_multiple: String (filter) → StringList - - -- Filesystem (5) — capability-guarded filesystem access - | CmdFsRead -- gossamer_fs_read_text: String (path) → String (contents) - | CmdFsWrite -- gossamer_fs_write_text: String (path+data) → I32 - | CmdFsExists -- gossamer_fs_exists: String (path) → Bool - | CmdFsListDir -- gossamer_fs_list_dir: String (dir) → StringList - | CmdFsRemove -- gossamer_fs_remove: String (path) → I32 - - -- Groove (7) — peer-to-peer inter-application protocol - | CmdGrooveDiscover -- gossamer_groove_discover: () → StringList (peer ids) - | CmdGrooveStatus -- gossamer_groove_status: String (target_id) → GrooveStatus - | CmdGrooveManifest -- gossamer_groove_manifest: String (target_id) → String (JSON) - | CmdGrooveSummary -- gossamer_groove_summary: () → String (JSON) - | CmdGrooveSend -- gossamer_groove_send: String (payload) → I32 - | CmdGrooveRecv -- gossamer_groove_recv: () → String (payload) - | CmdGrooveDisconnect -- gossamer_groove_disconnect: String (target_id) → I32 - - -- Platform (2) — host system information - | CmdPlatformInfo -- gossamer_platform_json: () → PlatformInfo (JSON) - | CmdBuildInfo -- gossamer_build_info: () → PlatformInfo (JSON) - --------------------------------------------------------------------------------- --- Handler Signatures (GS2-TP: input/output types for all 25 commands) --------------------------------------------------------------------------------- - -||| The declared type signature for each IPC command. -||| This function is TOTAL: Idris2 verifies all 25 constructors are covered. -public export -handlerSig : IpcCommand -> HandlerSig --- Shell -handlerSig CmdShow = MkSig IpcUnit IpcI32 -handlerSig CmdHide = MkSig IpcUnit IpcI32 -handlerSig CmdMinimize = MkSig IpcUnit IpcI32 -handlerSig CmdMaximize = MkSig IpcUnit IpcI32 -handlerSig CmdRestore = MkSig IpcUnit IpcI32 --- Bridge -handlerSig CmdChannelOpen = MkSig IpcUnit IpcI32 -handlerSig CmdChannelClose = MkSig IpcUnit IpcUnit --- Dialog -handlerSig CmdDialogOpen = MkSig IpcString IpcString -handlerSig CmdDialogSave = MkSig IpcString IpcString -handlerSig CmdDialogOpenDir = MkSig IpcUnit IpcString -handlerSig CmdDialogMulti = MkSig IpcString IpcStringList --- Filesystem -handlerSig CmdFsRead = MkSig IpcString IpcString -handlerSig CmdFsWrite = MkSig IpcString IpcI32 -handlerSig CmdFsExists = MkSig IpcString IpcBool -handlerSig CmdFsListDir = MkSig IpcString IpcStringList -handlerSig CmdFsRemove = MkSig IpcString IpcI32 --- Groove -handlerSig CmdGrooveDiscover = MkSig IpcUnit IpcStringList -handlerSig CmdGrooveStatus = MkSig IpcString IpcGrooveStatus -handlerSig CmdGrooveManifest = MkSig IpcString IpcString -handlerSig CmdGrooveSummary = MkSig IpcUnit IpcString -handlerSig CmdGrooveSend = MkSig IpcString IpcI32 -handlerSig CmdGrooveRecv = MkSig IpcUnit IpcString -handlerSig CmdGrooveDisconnect = MkSig IpcString IpcI32 --- Platform -handlerSig CmdPlatformInfo = MkSig IpcUnit IpcPlatformInfo -handlerSig CmdBuildInfo = MkSig IpcUnit IpcPlatformInfo - -||| Every command has a declared handler: dispatch is total. -||| This is the top-level type safety theorem for GS2. -public export -dispatchTotal : (cmd : IpcCommand) -> HandlerSig -dispatchTotal = handlerSig - --------------------------------------------------------------------------------- --- GS2-TP-2: Capability-guarded commands require a token --------------------------------------------------------------------------------- - -||| Predicate: this command requires a capability token to execute. -||| Filesystem commands require a Cap token; others do not. -public export -data RequiresCap : IpcCommand -> Type where - FsReadCap : RequiresCap CmdFsRead - FsWriteCap : RequiresCap CmdFsWrite - FsExistsCap : RequiresCap CmdFsExists - FsListDirCap : RequiresCap CmdFsListDir - FsRemoveCap : RequiresCap CmdFsRemove - -||| Predicate: this command does NOT require a capability token. -public export -data NoCap : IpcCommand -> Type where - NoCapShow : NoCap CmdShow - NoCapHide : NoCap CmdHide - NoCapMinimize : NoCap CmdMinimize - NoCapMaximize : NoCap CmdMaximize - NoCapRestore : NoCap CmdRestore - NoCapChannelOpen : NoCap CmdChannelOpen - NoCapChannelClose : NoCap CmdChannelClose - NoCapDialogOpen : NoCap CmdDialogOpen - NoCapDialogSave : NoCap CmdDialogSave - NoCapDialogOpenDir : NoCap CmdDialogOpenDir - NoCapDialogMulti : NoCap CmdDialogMulti - NoCapGrooveDiscover : NoCap CmdGrooveDiscover - NoCapGrooveStatus : NoCap CmdGrooveStatus - NoCapGrooveManifest : NoCap CmdGrooveManifest - NoCapGrooveSummary : NoCap CmdGrooveSummary - NoCapGrooveSend : NoCap CmdGrooveSend - NoCapGrooveRecv : NoCap CmdGrooveRecv - NoCapGrooveDisconnect : NoCap CmdGrooveDisconnect - NoCapPlatformInfo : NoCap CmdPlatformInfo - NoCapBuildInfo : NoCap CmdBuildInfo - -||| RequiresCap and NoCap are mutually exclusive. -public export -capExclusive : RequiresCap cmd -> NoCap cmd -> Void -capExclusive FsReadCap x = case x of {} -capExclusive FsWriteCap x = case x of {} -capExclusive FsExistsCap x = case x of {} -capExclusive FsListDirCap x = case x of {} -capExclusive FsRemoveCap x = case x of {} - -||| Every IPC command is either capability-guarded or not. -||| Total: Idris2 verifies all 25 constructors are covered. -public export -capClassify : (cmd : IpcCommand) -> Either (RequiresCap cmd) (NoCap cmd) -capClassify CmdShow = Right NoCapShow -capClassify CmdHide = Right NoCapHide -capClassify CmdMinimize = Right NoCapMinimize -capClassify CmdMaximize = Right NoCapMaximize -capClassify CmdRestore = Right NoCapRestore -capClassify CmdChannelOpen = Right NoCapChannelOpen -capClassify CmdChannelClose = Right NoCapChannelClose -capClassify CmdDialogOpen = Right NoCapDialogOpen -capClassify CmdDialogSave = Right NoCapDialogSave -capClassify CmdDialogOpenDir = Right NoCapDialogOpenDir -capClassify CmdDialogMulti = Right NoCapDialogMulti -capClassify CmdFsRead = Left FsReadCap -capClassify CmdFsWrite = Left FsWriteCap -capClassify CmdFsExists = Left FsExistsCap -capClassify CmdFsListDir = Left FsListDirCap -capClassify CmdFsRemove = Left FsRemoveCap -capClassify CmdGrooveDiscover = Right NoCapGrooveDiscover -capClassify CmdGrooveStatus = Right NoCapGrooveStatus -capClassify CmdGrooveManifest = Right NoCapGrooveManifest -capClassify CmdGrooveSummary = Right NoCapGrooveSummary -capClassify CmdGrooveSend = Right NoCapGrooveSend -capClassify CmdGrooveRecv = Right NoCapGrooveRecv -capClassify CmdGrooveDisconnect = Right NoCapGrooveDisconnect -capClassify CmdPlatformInfo = Right NoCapPlatformInfo -capClassify CmdBuildInfo = Right NoCapBuildInfo - --------------------------------------------------------------------------------- --- GS2-TP-3: Dispatch injectivity (distinct commands have distinct handlers) --------------------------------------------------------------------------------- - -||| Two IPC commands are definitionally equal iff they are the same constructor. -||| This uses Idris2's DecEq interface. -public export -Eq IpcCommand where - CmdShow == CmdShow = True - CmdHide == CmdHide = True - CmdMinimize == CmdMinimize = True - CmdMaximize == CmdMaximize = True - CmdRestore == CmdRestore = True - CmdChannelOpen == CmdChannelOpen = True - CmdChannelClose == CmdChannelClose = True - CmdDialogOpen == CmdDialogOpen = True - CmdDialogSave == CmdDialogSave = True - CmdDialogOpenDir == CmdDialogOpenDir = True - CmdDialogMulti == CmdDialogMulti = True - CmdFsRead == CmdFsRead = True - CmdFsWrite == CmdFsWrite = True - CmdFsExists == CmdFsExists = True - CmdFsListDir == CmdFsListDir = True - CmdFsRemove == CmdFsRemove = True - CmdGrooveDiscover == CmdGrooveDiscover = True - CmdGrooveStatus == CmdGrooveStatus = True - CmdGrooveManifest == CmdGrooveManifest = True - CmdGrooveSummary == CmdGrooveSummary = True - CmdGrooveSend == CmdGrooveSend = True - CmdGrooveRecv == CmdGrooveRecv = True - CmdGrooveDisconnect == CmdGrooveDisconnect = True - CmdPlatformInfo == CmdPlatformInfo = True - CmdBuildInfo == CmdBuildInfo = True - _ == _ = False - -||| Proof that the dispatch function does not silently unify distinct commands: -||| if two commands have the same name, they are the same command. -||| -||| Here we encode this as: every command is either identical to CmdShow or not. -||| The full injectivity proof follows from Idris2's totality checker: since -||| `handlerSig` is structurally defined with distinct RHS records for each -||| constructor, the type checker guarantees no two branches alias. -public export -data DistinctCommands : IpcCommand -> IpcCommand -> Type where - ||| Proof witness: cmd1 /= cmd2 by construction. - AreDistinct : {cmd1 : IpcCommand} -> {cmd2 : IpcCommand} - -> (cmd1 == cmd2 = False) - -> DistinctCommands cmd1 cmd2 - -||| Example: Show and Hide are distinct commands. -public export -showHideDistinct : DistinctCommands CmdShow CmdHide -showHideDistinct = AreDistinct Refl - -||| Example: Filesystem commands are distinct from Groove commands. -public export -fsReadGrooveDistinct : DistinctCommands CmdFsRead CmdGrooveDiscover -fsReadGrooveDistinct = AreDistinct Refl diff --git a/src/interface/Gossamer/ABI/IPCDispatch.idr b/src/interface/Gossamer/ABI/IPCDispatch.idr new file mode 120000 index 0000000..a54c7dc --- /dev/null +++ b/src/interface/Gossamer/ABI/IPCDispatch.idr @@ -0,0 +1 @@ +../../abi/IPCDispatch.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/IPCIntegrity.idr b/src/interface/Gossamer/ABI/IPCIntegrity.idr deleted file mode 100644 index 123ffe2..0000000 --- a/src/interface/Gossamer/ABI/IPCIntegrity.idr +++ /dev/null @@ -1,352 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- -||| IPC Integrity Proofs for Gossamer -||| -||| Proves that messages sent through Gossamer's IPC channels arrive -||| unmodified. The type system encodes message hashes and sequence numbers -||| as dependent types, making tampering detectable at compile time for -||| statically-known protocols, and at runtime for dynamic payloads. -||| -||| Key properties proved: -||| 1. Hash preservation: the hash of a received message equals the hash -||| of the sent message (if the channel is honest). -||| 2. Sequence monotonicity: message sequence numbers are strictly increasing. -||| 3. Protocol conformance: messages match the declared protocol schema. -||| 4. No phantom messages: every received message has a corresponding send. -||| -||| Zero believe_me. All proofs are constructive. -||| ChainedIntegrity uses propositional equality (=) for clean transitivity -||| via trans, avoiding the need for DecEq on Bits64. - -module Gossamer.ABI.IPCIntegrity - -import Gossamer.ABI.Types -import Data.So -import Data.Bits -import Data.Nat -import Data.List - -%default total - --------------------------------------------------------------------------------- --- Message Hash Type --------------------------------------------------------------------------------- - -||| A cryptographic hash of a message payload. -||| Represented as a pair of Bits64 values (128-bit hash). -||| The actual hash computation happens in the Zig FFI layer; -||| the Idris2 ABI tracks hashes as opaque witnesses. -public export -record MsgHash where - constructor MkHash - ||| High 64 bits of the hash - hi : Bits64 - ||| Low 64 bits of the hash - lo : Bits64 - -||| Hash equality is decidable. -public export -Eq MsgHash where - (MkHash h1 l1) == (MkHash h2 l2) = h1 == h2 && l1 == l2 - --------------------------------------------------------------------------------- --- Sequence Numbers --------------------------------------------------------------------------------- - -||| A monotonically increasing sequence number for IPC messages. -||| The Nat index tracks the sequence at the type level, enabling -||| compile-time proofs about message ordering. -public export -data SeqNum : (n : Nat) -> Type where - MkSeq : (val : Bits64) -> SeqNum n - -||| Extract the raw sequence number value. -public export -seqVal : SeqNum n -> Bits64 -seqVal (MkSeq val) = val - -||| Proof that one sequence number succeeds another. -||| Used to prove that messages are received in order. -public export -data Succeeds : SeqNum (S n) -> SeqNum n -> Type where - ||| The successor relationship is witnessed by the Nat indices. - MkSucceeds : Succeeds (MkSeq {n = S n} v2) (MkSeq {n} v1) - --------------------------------------------------------------------------------- --- Stamped Messages --------------------------------------------------------------------------------- - -||| A message with an integrity stamp: hash + sequence number. -||| -||| The stamp is computed at send time and verified at receive time. -||| The type parameters carry the hash and sequence at the type level, -||| enabling static integrity proofs for known protocols. -public export -record StampedMessage (payload : Type) (n : Nat) where - constructor MkStamped - ||| The message payload - body : payload - ||| Cryptographic hash of the serialised payload - hash : MsgHash - ||| Sequence number (type-level and value-level) - seqNum : SeqNum n - --------------------------------------------------------------------------------- --- Honest Channel Model --------------------------------------------------------------------------------- - -||| An honest channel preserves message integrity. -||| -||| This is the specification of what "integrity" means: -||| 1. The payload is unchanged (same hash) -||| 2. The sequence number is preserved -||| 3. No messages are injected or dropped -||| -||| The Zig FFI layer implements this by computing SipHash-2-4 at the -||| send boundary and verifying at the receive boundary. This Idris2 -||| module provides the type-level specification that the FFI must satisfy. -public export -data HonestChannel : (req : Type) -> (resp : Type) -> Type where - ||| An honest channel is parameterised by its request and response types. - ||| The channel guarantees hash preservation and sequence monotonicity. - MkHonest : HonestChannel req resp - -||| Proof that a message was not tampered with during transit. -||| -||| Given an honest channel, the hash of the received message equals -||| the hash of the sent message. This is the core integrity guarantee. -public export -data Untampered : (sent : StampedMessage payload n) - -> (received : StampedMessage payload n) - -> Type where - ||| Witness that sent.hash == received.hash. - ||| The Nat indices match (same sequence number), and the hash - ||| equality is carried as a So proof. - MkUntampered : {sent : StampedMessage payload n} - -> {received : StampedMessage payload n} - -> {auto 0 hashEq : So (sent.hash == received.hash)} - -> Untampered sent received - -||| Proof that a sequence of messages is ordered. -||| -||| A message log is ordered if each successive message has a strictly -||| higher sequence number than its predecessor. -public export -data Ordered : List (StampedMessage payload n) -> Type where - ||| An empty log is trivially ordered. - OrdNil : Ordered [] - ||| A singleton log is trivially ordered. - OrdOne : Ordered [msg] - --------------------------------------------------------------------------------- --- Send/Receive Protocol --------------------------------------------------------------------------------- --- --- Declared BEFORE the Hash Preservation Theorem so that `hashPreservation` --- can quantify over a `VerifiedReceive` without forward-referencing the --- type (the original module's forward-reference + inline `where`-accessor --- combination produced an unbound-implicit theorem statement; see the --- OWED note in `gossamer-abi.ipkg` for the original failure mode). - -||| A send receipt proves that a message was submitted to the channel. -||| The receipt carries the hash computed at send time, which the -||| receiver must match for integrity verification. -public export -data SendReceipt : (payload : Type) -> (n : Nat) -> Type where - MkReceipt : (msg : StampedMessage payload n) -> SendReceipt payload n - -||| Extract the hash from a send receipt (for verification). -public export -receiptHash : SendReceipt payload n -> MsgHash -receiptHash (MkReceipt msg) = msg.hash - -||| Extract the receipt's stamped message. Top-level accessor (a `where` -||| block on a `data` declaration is not valid Idris2 — this was the -||| original parse failure); used by `MkVerified`'s `Untampered` -||| obligation. -public export -receiptMsg : SendReceipt payload n -> StampedMessage payload n -receiptMsg (MkReceipt m) = m - -||| A receive verification pairs a received message with a send receipt -||| and proves that the hashes match. -public export -data VerifiedReceive : (payload : Type) -> (n : Nat) -> Type where - MkVerified : (receipt : SendReceipt payload n) - -> (received : StampedMessage payload n) - -> {auto 0 intact : Untampered (receiptMsg receipt) received} - -> VerifiedReceive payload n - -||| Extract the send receipt from a `VerifiedReceive`. Provided so that -||| theorem statements about `VerifiedReceive` can name the receipt and -||| received message without re-destructuring (the elaborator's -||| lowercase-implicit-binding heuristic otherwise turns the bare names -||| in a return type into fresh implicits and the proof obligation -||| collapses to abstract record fields — same idiom as -||| `LayoutStability.v030ExtendsV020`'s module-qualified constants). -public export -verifiedReceipt : VerifiedReceive payload n -> SendReceipt payload n -verifiedReceipt (MkVerified r _) = r - -||| Extract the received stamped message from a `VerifiedReceive`. -public export -verifiedReceived : VerifiedReceive payload n -> StampedMessage payload n -verifiedReceived (MkVerified _ rcv) = rcv - --------------------------------------------------------------------------------- --- Hash Preservation Theorem --------------------------------------------------------------------------------- - -||| Hash preservation: on an honest channel, the hash of a received -||| message MUST equal the hash of the sent message. -||| -||| This is the core integrity theorem. It states that if we have an -||| honest channel and a send receipt, any valid VerifiedReceive -||| necessarily carries an Untampered proof (by construction). -||| -||| The proof is definitional: VerifiedReceive includes Untampered as -||| an erased auto-implicit, so the type checker ensures hash equality -||| at construction time. This function witnesses that relationship. -||| -||| Restated to use the `verifiedReceipt` + `verifiedReceived` top-level -||| accessors instead of an inline `where`-defined `.msg` projector — the -||| original `Untampered (MkReceipt msg).msg received` form left `msg` -||| and `received` as unbound implicits in the return type, which Idris2 -||| would silently bind as fresh variables (and which destroyed the -||| dependency on the input `VerifiedReceive`). -||| Marked `0` — this is a type-level theorem, not a runtime function. -||| `MkVerified` binds its `intact` witness at quantity 0 (erased), so -||| a quantity-1 caller cannot extract it. Quantity-0 callers can, -||| which is exactly what proof-level use sites need. -public export -0 hashPreservation : (v : VerifiedReceive payload n) - -> Untampered (receiptMsg (verifiedReceipt v)) (verifiedReceived v) -hashPreservation (MkVerified _ _ {intact}) = intact - -||| Sequence monotonicity: for any two successive messages in a valid -||| log, the later message has a strictly greater sequence index. -||| -||| This is proved by construction: `StampedMessage` carries the -||| sequence number at the type level (Nat index), and `Succeeds` -||| witnesses that `S n > n`. The proof is `LTE n (S n)` (current -||| strictly precedes successor) — the original `LTE (S n) (S n)` was -||| reflexivity, not monotonicity, and was the silent latent defect the -||| coverage/quantity checker would have caught on first build. -||| -||| Marked `0` for the same reason as `hashPreservation`: `MkSucceeds` -||| binds `n` at quantity 0 in the data constructor, so the proof -||| `lteSuccRight reflexive` (which structurally recurses on `n`) needs -||| `n` available at quantity 1 — only a quantity-0 caller can supply -||| that. The theorem stands; only runtime invocation is prohibited. -public export -0 seqMonotonicity : Succeeds (MkSeq {n = S n} v2) (MkSeq {n} v1) -> LTE n (S n) -seqMonotonicity MkSucceeds = lteSuccRight reflexive - --------------------------------------------------------------------------------- --- No Phantom Messages --------------------------------------------------------------------------------- - -||| A message log paired with its corresponding send receipts. -||| -||| Every received message has a matching send receipt. The type-level -||| Nat indices must align pairwise, preventing phantom messages -||| (messages that appear in the receive log without a corresponding send). -public export -data CorrespondingLog : Type where - ||| An empty log has no messages. - CLNil : CorrespondingLog - ||| A message with its matching receipt, followed by the rest of the log. - CLCons : SendReceipt payload n - -> StampedMessage payload n - -> CorrespondingLog - -> CorrespondingLog - -||| Proof that every message in a CorrespondingLog has a send receipt. -||| This is definitional — the CLCons constructor requires a receipt for -||| each message, so a CorrespondingLog without receipts cannot be built. -public export -noPhantomMessages : CorrespondingLog -> Nat -noPhantomMessages CLNil = 0 -noPhantomMessages (CLCons _ _ rest) = S (noPhantomMessages rest) - --------------------------------------------------------------------------------- --- Channel Composition Integrity --------------------------------------------------------------------------------- - -||| Proof that messages routed through a chain of honest channels -||| preserve integrity end-to-end. -||| -||| If channel A is honest (frontend -> middleware) and channel B is -||| honest (middleware -> backend), then the composition A;B is honest: -||| the hash of a message entering A equals the hash exiting B. -||| -||| Uses propositional equality (=) rather than boolean So (==) so that -||| transitivity is definitional (trans), with no believe_me required. -public export -data ChainedIntegrity : Type where - MkChained : {payload : Type} - -> {n : Nat} - -> (sent : StampedMessage payload n) - -> (mid : StampedMessage payload n) - -> (recv : StampedMessage payload n) - -> (0 leg1 : sent.hash = mid.hash) - -> (0 leg2 : mid.hash = recv.hash) - -> ChainedIntegrity - -||| End-to-end hash equality for chained channels. -||| If sent.hash = mid.hash and mid.hash = recv.hash, -||| then sent.hash = recv.hash by propositional transitivity. -||| Constructive: zero believe_me, zero axioms. -public export -chainedHashPreservation : (sent : StampedMessage payload n) - -> (mid : StampedMessage payload n) - -> (recv : StampedMessage payload n) - -> (0 leg1 : sent.hash = mid.hash) - -> (0 leg2 : mid.hash = recv.hash) - -> sent.hash = recv.hash -chainedHashPreservation sent mid recv leg1 leg2 = trans leg1 leg2 - --------------------------------------------------------------------------------- --- Protocol Conformance --------------------------------------------------------------------------------- - -||| A protocol schema is a list of (command name, request type, response type). -||| This reuses the Protocol type from Types.idr but adds integrity tracking. -public export -data IntegrityProtocol : List (String, Type, Type) -> Type where - IPNil : IntegrityProtocol [] - IPCons : (name : String) -> (req : Type) -> (resp : Type) - -> IntegrityProtocol rest - -> IntegrityProtocol ((name, req, resp) :: rest) - -||| Proof that a message conforms to a specific command in the protocol. -||| -||| The message's payload type must match the command's expected request type. -||| This prevents sending a "file_read" payload on a "file_write" command. -public export -data ConformsTo : (cmdName : String) -> (payload : Type) - -> IntegrityProtocol schema -> Type where - ||| The command name matches the head of the protocol, - ||| and the payload type matches the request type. - ConformHere : ConformsTo name req (IPCons name req resp rest) - ||| The command is further down in the protocol list. - ConformThere : ConformsTo name req (IPCons other otherReq otherResp rest) - -> ConformsTo name req (IPCons other otherReq otherResp rest) - --------------------------------------------------------------------------------- --- Composition: Integrity + Isolation --------------------------------------------------------------------------------- - -||| An isolated, integrity-verified message. -||| -||| Combines panel isolation (from PanelIsolation.idr) with IPC integrity. -||| The panel tag ensures the message came from the correct panel, -||| and the hash ensures it was not tampered with. -public export -record IsolatedVerifiedMsg (tag : String) (payload : Type) (n : Nat) where - constructor MkIsolatedVerified - ||| The verified receive (hash-checked) - verified : StampedMessage payload n - ||| The hash of the sent message (for audit logging) - sentHash : MsgHash diff --git a/src/interface/Gossamer/ABI/IPCIntegrity.idr b/src/interface/Gossamer/ABI/IPCIntegrity.idr new file mode 120000 index 0000000..8e7a309 --- /dev/null +++ b/src/interface/Gossamer/ABI/IPCIntegrity.idr @@ -0,0 +1 @@ +../../abi/IPCIntegrity.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/Layout.idr b/src/interface/Gossamer/ABI/Layout.idr deleted file mode 100644 index 7c23cd9..0000000 --- a/src/interface/Gossamer/ABI/Layout.idr +++ /dev/null @@ -1,209 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- -||| Memory Layout Proofs for Gossamer -||| -||| Provides formal proofs about memory layout, alignment, and padding -||| for Gossamer's C-compatible types. Ensures the Idris2 ABI definitions -||| match the Zig FFI implementation at the byte level. -||| -||| Key types verified: -||| - GossamerHandle: opaque, pointer-sized -||| - ChannelHandle: opaque, pointer-sized -||| - WindowConfig: packed struct layout -||| - Result enum: C int (4 bytes) - -module Gossamer.ABI.Layout - -import Gossamer.ABI.Types -import Data.Vect -import Data.So - -%default total - --------------------------------------------------------------------------------- --- Alignment Utilities --------------------------------------------------------------------------------- - -||| Calculate padding needed to reach the next aligned offset. -public export -paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat -paddingFor offset alignment = - if offset `mod` alignment == 0 - then 0 - else minus alignment (offset `mod` alignment) - -||| Align an offset up to the given alignment boundary. -public export -alignUp : (offset : Nat) -> (alignment : Nat) -> Nat -alignUp offset alignment = offset + paddingFor offset alignment - --------------------------------------------------------------------------------- --- Struct Field Layout --------------------------------------------------------------------------------- - -||| A field in a C struct: name, size, and alignment. -public export -record FieldSpec where - constructor MkFieldSpec - fieldName : String - fieldSize : Nat - fieldAlign : Nat - -||| Calculate the offset of each field in a packed struct. -||| Returns a list of (field name, offset, size) triples. -public export -layoutFields : (startOffset : Nat) -> List FieldSpec -> List (String, Nat, Nat) -layoutFields _ [] = [] -layoutFields offset (f :: fs) = - let aligned = alignUp offset f.fieldAlign - in (f.fieldName, aligned, f.fieldSize) :: layoutFields (aligned + f.fieldSize) fs - -||| Total size of a struct including final padding for alignment. -public export -structSize : (structAlign : Nat) -> List FieldSpec -> Nat -structSize sAlign fields = alignUp (go 0 fields) sAlign - where - go : Nat -> List FieldSpec -> Nat - go offset [] = offset - go offset (f :: fs) = - let aligned = alignUp offset f.fieldAlign - in go (aligned + f.fieldSize) fs - --------------------------------------------------------------------------------- --- Proof: Opaque Handle Types --------------------------------------------------------------------------------- - -||| All opaque handles are pointer-sized. -||| On 64-bit platforms, this is 8 bytes. On WASM, 4 bytes. -public export -handleSize : (p : Platform) -> Nat -handleSize WASM = 4 -handleSize _ = 8 - -||| Proof that WebviewHandle is pointer-sized on the current platform. -public export -webviewHandleSize : HasSize WebviewHandle (handleSize Types.thisPlatform) -webviewHandleSize = SizeProof - -||| Proof that WebviewHandle has pointer alignment. -public export -webviewHandleAlign : HasAlignment WebviewHandle (handleSize Types.thisPlatform) -webviewHandleAlign = AlignProof - -||| Proof that Channel handles are pointer-sized. -public export -channelHandleSize : HasSize (Channel req resp) (handleSize Types.thisPlatform) -channelHandleSize = SizeProof - -||| Proof that Cap tokens are pointer-sized (Bits64 token ID). -public export -capTokenSize : HasSize (Cap resource) 8 -capTokenSize = SizeProof - --------------------------------------------------------------------------------- --- Proof: Result Enum --------------------------------------------------------------------------------- - -||| Result is represented as a C int (4 bytes on all platforms). -public export -resultSize : HasSize Result 4 -resultSize = SizeProof - -||| Result has 4-byte alignment (matching C int). -public export -resultAlign : HasAlignment Result 4 -resultAlign = AlignProof - -||| All result code values fit in a Bits32. -||| (Max value is 11 = GuardLocked, well within 0..4294967295) -public export -resultFitsInBits32 : (r : Result) -> So (resultToInt r <= 4294967295) -resultFitsInBits32 Ok = Oh -resultFitsInBits32 Error = Oh -resultFitsInBits32 InvalidParam = Oh -resultFitsInBits32 OutOfMemory = Oh -resultFitsInBits32 NullPointer = Oh -resultFitsInBits32 AlreadyConsumed = Oh -resultFitsInBits32 ResourceLeaked = Oh -resultFitsInBits32 DoubleFree = Oh -resultFitsInBits32 WebviewUnavailable = Oh -resultFitsInBits32 IPCProtocolError = Oh -resultFitsInBits32 CapabilityDenied = Oh -resultFitsInBits32 GuardLocked = Oh - --------------------------------------------------------------------------------- --- Proof: WindowConfig Layout --------------------------------------------------------------------------------- - -||| WindowConfig field specifications for C ABI layout calculation. -||| Fields: title (ptr), width (u32), height (u32), min/max bounds (u32), -||| resizable (bool/u8), decorations (bool/u8), fullscreen (bool/u8), -||| visible (bool/u8) -||| -||| Note: In the FFI, title is passed as a C string pointer, not embedded -||| in the struct. The struct layout here is for documentation and -||| verification purposes. -public export -windowConfigFields : List FieldSpec -windowConfigFields = - [ MkFieldSpec "title_ptr" 8 8 -- Pointer to title string - , MkFieldSpec "width" 4 4 -- Bits32 - , MkFieldSpec "height" 4 4 -- Bits32 - , MkFieldSpec "minWidth" 4 4 -- Bits32 (0 = unconstrained) - , MkFieldSpec "minHeight" 4 4 -- Bits32 (0 = unconstrained) - , MkFieldSpec "maxWidth" 4 4 -- Bits32 (0 = unconstrained) - , MkFieldSpec "maxHeight" 4 4 -- Bits32 (0 = unconstrained) - , MkFieldSpec "resizable" 4 4 -- Bits32 (bool as C int for alignment) - , MkFieldSpec "decorations" 4 4 -- Bits32 - , MkFieldSpec "fullscreen" 4 4 -- Bits32 - , MkFieldSpec "visible" 4 4 -- Bits32 (bool as C int for alignment) - ] - -||| WindowConfig total size: 48 bytes (8-byte aligned). -||| title_ptr(0..7) + width(8..11) + height(12..15) -||| + minWidth(16..19) + minHeight(20..23) + maxWidth(24..27) -||| + maxHeight(28..31) + resizable(32..35) + decorations(36..39) -||| + fullscreen(40..43) + visible(44..47) -||| + no trailing padding needed = 48 bytes -public export -windowConfigSize : HasSize WindowConfig 48 -windowConfigSize = SizeProof - -||| WindowConfig alignment: 8 bytes (due to pointer field). -public export -windowConfigAlign : HasAlignment WindowConfig 8 -windowConfigAlign = AlignProof - --------------------------------------------------------------------------------- --- C ABI Compliance --------------------------------------------------------------------------------- - -||| Proof that a struct's fields are all properly aligned. -public export -data FieldsAligned : List FieldSpec -> Type where - FANil : FieldsAligned [] - FACons : (f : FieldSpec) - -> So (f.fieldAlign > 0) - -> FieldsAligned rest - -> FieldsAligned (f :: rest) - -||| C ABI compliance certificate for a type. -||| A type is C ABI compliant if: -||| 1. Its size is known -||| 2. Its alignment is a power of 2 and positive -||| 3. Its size is a multiple of its alignment -public export -data CABICompliant : Type -> Nat -> Nat -> Type where - MkCompliant : {0 t : Type} - -> {size : Nat} - -> {align : Nat} - -> HasSize t size - -> HasAlignment t align - -> So (align > 0) - -> CABICompliant t size align - -||| Result is C ABI compliant (4 bytes, 4-byte aligned). -public export -resultCompliant : CABICompliant Result 4 4 -resultCompliant = MkCompliant resultSize resultAlign Oh diff --git a/src/interface/Gossamer/ABI/Layout.idr b/src/interface/Gossamer/ABI/Layout.idr new file mode 120000 index 0000000..7644222 --- /dev/null +++ b/src/interface/Gossamer/ABI/Layout.idr @@ -0,0 +1 @@ +../../abi/Layout.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/LayoutStability.idr b/src/interface/Gossamer/ABI/LayoutStability.idr deleted file mode 100644 index 9a23d99..0000000 --- a/src/interface/Gossamer/ABI/LayoutStability.idr +++ /dev/null @@ -1,238 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- -||| Memory Layout ABI Stability Proofs for Gossamer -||| -||| Proves that Layout.idr definitions are backward-compatible across versions. -||| Specifically: -||| 1. Field ordering is fixed (no silent field reordering between versions). -||| 2. Struct sizes are monotonically non-decreasing (new fields append only). -||| 3. Existing field offsets are preserved across versions. -||| 4. Alignment requirements are preserved. -||| -||| These proofs ensure that a binary compiled against ABI v0.2.0 can be -||| loaded by a runtime built with ABI v0.3.0 without layout corruption. -||| -||| Zero believe_me. All proofs are constructive. - -module Gossamer.ABI.LayoutStability - -import Gossamer.ABI.Types -import Gossamer.ABI.Layout -import Data.So -import Data.Nat -import Data.List - -%default total - --------------------------------------------------------------------------------- --- ABI Version --------------------------------------------------------------------------------- - -||| An ABI version is a (major, minor, patch) triple. -||| Backward compatibility is guaranteed within the same major version. -public export -record ABIVersion where - constructor MkVersion - major : Nat - minor : Nat - patch : Nat - -||| The current ABI version. -public export -currentVersion : ABIVersion -currentVersion = MkVersion 0 3 1 - -||| Compare ABI versions for ordering. -public export -versionLTE : ABIVersion -> ABIVersion -> Bool -versionLTE a b = - if a.major /= b.major then a.major <= b.major - else if a.minor /= b.minor then a.minor <= b.minor - else a.patch <= b.patch - --------------------------------------------------------------------------------- --- Versioned Struct Layout --------------------------------------------------------------------------------- - -||| A versioned struct layout: the field list at a specific ABI version. -public export -record VersionedLayout where - constructor MkVersioned - version : ABIVersion - fields : List FieldSpec - sAlign : Nat - -||| Proof that a newer layout is an extension of an older layout. -||| -||| An extension means: -||| 1. All old fields are preserved (same name, size, alignment, in order) -||| 2. New fields are only appended at the end -||| 3. The struct alignment is at least as strict -||| Check if one field list is a prefix of another. Two fields match if -||| name, size, and alignment are identical. Defined before -||| `IsExtensionOf` (which uses it in `MkExtension`) and given a distinct -||| name: the original `isPrefixOf` both forward-referenced this and -||| clashed with `Data.List.isPrefixOf` (`Eq a => ...`), so the GADT -||| resolved to the constrained Prelude version and demanded an -||| `Eq FieldSpec` that does not exist. -public export -fieldsArePrefixOf : List FieldSpec -> List FieldSpec -> Bool -fieldsArePrefixOf [] _ = True -fieldsArePrefixOf _ [] = False -fieldsArePrefixOf (f :: fs) (g :: gs) = - f.fieldName == g.fieldName && - f.fieldSize == g.fieldSize && - f.fieldAlign == g.fieldAlign && - fieldsArePrefixOf fs gs - -public export -data IsExtensionOf : (older : VersionedLayout) -> (newer : VersionedLayout) -> Type where - ||| Witness that newer.fields starts with older.fields (prefix relation). - MkExtension : {older, newer : VersionedLayout} - -> {auto 0 versionOrd : So (versionLTE older.version newer.version)} - -> {auto 0 isPrefix : So (fieldsArePrefixOf older.fields newer.fields)} - -> {auto 0 alignPres : So (newer.sAlign >= older.sAlign)} - -> IsExtensionOf older newer - --------------------------------------------------------------------------------- --- WindowConfig Stability Across Versions --------------------------------------------------------------------------------- - -||| WindowConfig layout at ABI v0.1.0 (initial release). -||| 6 fields: title_ptr, width, height, resizable, decorations, visible -public export -windowConfigV010 : VersionedLayout -windowConfigV010 = MkVersioned (MkVersion 0 1 0) - [ MkFieldSpec "title_ptr" 8 8 - , MkFieldSpec "width" 4 4 - , MkFieldSpec "height" 4 4 - , MkFieldSpec "resizable" 4 4 - , MkFieldSpec "decorations" 4 4 - , MkFieldSpec "visible" 4 4 - ] - 8 - -||| WindowConfig layout at ABI v0.2.0 (added min/max bounds, fullscreen). -||| 11 fields: v0.1.0 fields + minWidth, minHeight, maxWidth, maxHeight, fullscreen. -||| NOTE: The new fields were inserted between height and resizable for logical -||| grouping. This is an intentional ABI break at v0.2.0 (pre-1.0 = unstable). -||| Post-1.0, all new fields MUST be appended. -public export -windowConfigV020 : VersionedLayout -windowConfigV020 = MkVersioned (MkVersion 0 2 0) - [ MkFieldSpec "title_ptr" 8 8 - , MkFieldSpec "width" 4 4 - , MkFieldSpec "height" 4 4 - , MkFieldSpec "minWidth" 4 4 - , MkFieldSpec "minHeight" 4 4 - , MkFieldSpec "maxWidth" 4 4 - , MkFieldSpec "maxHeight" 4 4 - , MkFieldSpec "resizable" 4 4 - , MkFieldSpec "decorations" 4 4 - , MkFieldSpec "fullscreen" 4 4 - , MkFieldSpec "visible" 4 4 - ] - 8 - -||| WindowConfig layout at ABI v0.3.0 (current — no changes from v0.2.0). -public export -windowConfigV030 : VersionedLayout -windowConfigV030 = MkVersioned (MkVersion 0 3 0) - windowConfigFields -- from Layout.idr - 8 - -||| Proof: v0.3.0 layout is identical to v0.2.0 layout (no changes). -||| -||| Names are module-qualified (`LayoutStability.…`) to prevent Idris2's -||| lowercase-implicit-binding heuristic from re-interpreting the two -||| constants as fresh implicit variables (the elaborator otherwise -||| issues "is shadowing Gossamer.ABI.LayoutStability." warnings -||| and the auto-implicit `So` proofs collapse to "Can't find …" because -||| their goal is then over abstract record fields, not the concrete -||| record values — same idiom as `resultCodesStable` below). -public export -v030ExtendsV020 : IsExtensionOf LayoutStability.windowConfigV020 LayoutStability.windowConfigV030 -v030ExtendsV020 = MkExtension - --------------------------------------------------------------------------------- --- Result Enum Stability --------------------------------------------------------------------------------- - -||| Result code assignments at v0.1.0 (6 codes: Ok..DoubleFree). -public export -resultCodesV010 : List (String, Nat) -resultCodesV010 = - [ ("Ok", 0), ("Error", 1), ("InvalidParam", 2) - , ("OutOfMemory", 3), ("NullPointer", 4), ("AlreadyConsumed", 5) - , ("ResourceLeaked", 6), ("DoubleFree", 7) - ] - -||| Result code assignments at v0.3.0 (12 codes: added Webview..GuardLocked). -public export -resultCodesV030 : List (String, Nat) -resultCodesV030 = - [ ("Ok", 0), ("Error", 1), ("InvalidParam", 2) - , ("OutOfMemory", 3), ("NullPointer", 4), ("AlreadyConsumed", 5) - , ("ResourceLeaked", 6), ("DoubleFree", 7) - , ("WebviewUnavailable", 8), ("IPCProtocolError", 9) - , ("CapabilityDenied", 10), ("GuardLocked", 11) - ] - -||| True when `older` is a prefix of `newer` (same name/value pairs, in -||| order). Top-level so it can appear in `ResultCodesPreserved`'s type — -||| a `where` block on a `data` declaration is not valid Idris2 and was -||| the original parse failure. -public export -isPrefixOfCodes : List (String, Nat) -> List (String, Nat) -> Bool -isPrefixOfCodes [] _ = True -isPrefixOfCodes _ [] = False -isPrefixOfCodes ((n1, v1) :: rest1) ((n2, v2) :: rest2) = - n1 == n2 && v1 == v2 && isPrefixOfCodes rest1 rest2 - -||| Proof that existing result codes are preserved across versions. -||| New codes are only appended — old code values never change. -public export -data ResultCodesPreserved : List (String, Nat) -> List (String, Nat) -> Type where - MkPreserved : {auto 0 prf : So (isPrefixOfCodes older newer)} -> ResultCodesPreserved older newer - -||| Proof: v0.3.0 result codes preserve all v0.1.0 codes. -public export -resultCodesStable : ResultCodesPreserved LayoutStability.resultCodesV010 LayoutStability.resultCodesV030 -resultCodesStable = MkPreserved -- OWED: as above - --------------------------------------------------------------------------------- --- Handle Size Stability --------------------------------------------------------------------------------- - -||| Proof: handle sizes are platform-determined and cannot change across versions. -||| A handle is always exactly pointer-sized on its platform. -public export -data HandleSizeStable : (p : Platform) -> Type where - ||| Handle size is determined solely by platform, not ABI version. - MkHandleStable : (p : Platform) - -> handleSize p = handleSize p - -> HandleSizeStable p - -||| Handle sizes are trivially stable (same function, same input). -public export -handleSizeNeverChanges : (p : Platform) -> HandleSizeStable p -handleSizeNeverChanges p = MkHandleStable p Refl - --------------------------------------------------------------------------------- --- Append-Only Extension Rule (Post-1.0) --------------------------------------------------------------------------------- - -||| Post-1.0 ABI rule: new fields are append-only. -||| -||| This proof obligation will be enforced after 1.0.0 release. -||| For pre-1.0 (current), layout changes are permitted. -public export -data AppendOnlyRule : Type where - ||| For any two layouts with the same major version >= 1, - ||| the older layout is a prefix of the newer layout. - MkAppendOnly : (older, newer : VersionedLayout) - -> {auto 0 sameMajor : So (older.version.major == newer.version.major)} - -> {auto 0 stableApi : So (older.version.major >= 1)} - -> IsExtensionOf older newer - -> AppendOnlyRule diff --git a/src/interface/Gossamer/ABI/LayoutStability.idr b/src/interface/Gossamer/ABI/LayoutStability.idr new file mode 120000 index 0000000..a92dcc4 --- /dev/null +++ b/src/interface/Gossamer/ABI/LayoutStability.idr @@ -0,0 +1 @@ +../../abi/LayoutStability.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/PanelIsolation.idr b/src/interface/Gossamer/ABI/PanelIsolation.idr deleted file mode 100644 index c78187d..0000000 --- a/src/interface/Gossamer/ABI/PanelIsolation.idr +++ /dev/null @@ -1,348 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- -||| Panel Isolation Proofs for Gossamer -||| -||| Proves that panels in the Gossamer webview shell cannot access each -||| other's state. Each panel is parameterised by a unique phantom type tag, -||| and the type system prevents cross-panel state access at compile time. -||| -||| Key properties proved: -||| 1. State tokens are panel-scoped: a PanelState tag1 cannot be used where -||| PanelState tag2 is expected (enforced by the type system, not runtime). -||| 2. IPC channels are panel-scoped: a channel opened by panel A cannot be -||| used by panel B. -||| 3. Panel registries track unique panel identifiers with non-collision proof. -||| 4. No panel can forge another panel's state token. -||| -||| One class-J axiom: `stringNotEqCommut` — commutativity of the -||| Idris2 backend primitive `prim__eq_String`. Sanctioned principled -||| assumption over a foreign primitive (same trust posture as -||| boj-server's `Boj.SafetyLemmas.charEqSym`), not unproven debt. All -||| other proofs in this module are constructive. - -module Gossamer.ABI.PanelIsolation - -import Gossamer.ABI.Types -import Data.So -import Data.Bits -import Data.List -import Data.List.Elem -import Decidable.Equality - -%default total - --------------------------------------------------------------------------------- --- Panel Identity --------------------------------------------------------------------------------- - -||| A panel tag is a unique string identifier. -||| Panels are parameterised by their tag at the type level, so operations -||| on panel A's resources cannot accidentally target panel B. -public export -PanelTag : Type -PanelTag = String - -||| Proof that two panel tags are distinct. -||| This is the foundation of isolation: if tags differ, their resources -||| are in separate type-level namespaces. -public export -data Distinct : (a : PanelTag) -> (b : PanelTag) -> Type where - ||| Witness that two tags are not equal. - ||| The So proof is checked at construction time, ensuring correctness. - MkDistinct : {a : PanelTag} -> {b : PanelTag} - -> {auto 0 prf : So (not (a == b))} - -> Distinct a b - --------------------------------------------------------------------------------- --- Class-J axiom: String `==` commutativity (Refs standards#131 / #124) --------------------------------------------------------------------------------- - -||| AXIOM (class-J): primitive String inequality is commutative. -||| -||| The `(==)` operator on `String` is the `Eq String` instance, which -||| dispatches to Idris2's backend primitive `prim__eq_String`. The -||| primitive is an opaque foreign function with no constructors and no -||| in-language induction principle — its commutativity over content -||| equality (`a == b` ⇔ `b == a`) holds on every supported backend -||| (Chez, Racket, Node, JS — all dispatch to native string-equal which -||| is content-symmetric) but cannot be derived inside Idris2 itself. -||| -||| Same trust posture as boj-server's `Boj.SafetyLemmas.charEqSym` -||| (symmetry of `prim__eqChar`) and four sibling axioms over String / -||| Char primitives. Audited as **class-(J)** — principled assumption -||| over an Idris2 primitive, not unproven debt. See PROOF-NEEDS.md (in -||| boj-server) for the per-site convention; this is gossamer's first -||| class-J axiom and is documented at the use site rather than in a -||| dedicated `SafetyLemmas` module — that module can be lifted out -||| later if a second axiom appears. -||| -||| Soundness oracle: property-test validation against the runtime, -||| per the boj-server backend-assurance harness pattern. A reduce-the- -||| trusted-base PR can replace this axiom with a `prim__eq_String` / -||| `prim__strEq` symmetry proof once that harness exists for gossamer. -||| -||| Refs: standards#131 (PanelIsolation `distinctSym`), -||| standards#124 (proof-debt epic). -%unsafe -export -stringNotEqCommut : {a, b : String} -> So (not (a == b)) -> So (not (b == a)) -stringNotEqCommut _ = believe_me () - -||| Distinctness is symmetric: if a /= b then b /= a. -||| Constructive modulo `stringNotEqCommut` (class-J axiom above). -public export -distinctSym : Distinct a b -> Distinct b a -distinctSym (MkDistinct {a} {b} {prf}) = - MkDistinct {a=b} {b=a} {prf = stringNotEqCommut prf} - --------------------------------------------------------------------------------- --- Panel-Scoped State --------------------------------------------------------------------------------- - -||| A state token scoped to a specific panel. -||| -||| The phantom type parameter `tag` ensures that: -||| - PanelState "editor" and PanelState "terminal" are DIFFERENT types -||| - A function expecting PanelState "editor" rejects PanelState "terminal" -||| - The Idris2 type checker enforces this at compile time -||| -||| The inner Bits64 is an opaque state identifier allocated by the runtime. -||| The non-null proof guarantees the token is valid (not a default/zero value). -public export -data PanelState : (tag : PanelTag) -> Type where - MkPanelState : (token : Bits64) - -> {auto 0 nonNull : So (token /= 0)} - -> PanelState tag - -||| Extract the raw token from a panel state (for FFI calls). -public export -stateToken : PanelState tag -> Bits64 -stateToken (MkPanelState token) = token - -||| Safely create a PanelState from a raw token. -||| Returns Nothing if the token is null (zero). -public export -createPanelState : Bits64 -> Maybe (PanelState tag) -createPanelState ptr = - case choose (ptr /= 0) of - Left ok => Just (MkPanelState ptr) - Right _ => Nothing - --------------------------------------------------------------------------------- --- Panel-Scoped IPC Channel --------------------------------------------------------------------------------- - -||| An IPC channel scoped to a specific panel. -||| -||| This extends the base Channel type from Types.idr with a panel tag, -||| preventing cross-panel channel reuse. A PanelChannel "editor" req resp -||| cannot be passed to a function expecting PanelChannel "terminal" req resp. -public export -data PanelChannel : (tag : PanelTag) -> (req : Type) -> (resp : Type) -> Type where - MkPanelChannel : (ptr : Bits64) - -> {auto 0 nonNull : So (ptr /= 0)} - -> PanelChannel tag req resp - -||| Extract raw pointer from a panel channel (for FFI calls). -public export -panelChannelPtr : PanelChannel tag req resp -> Bits64 -panelChannelPtr (MkPanelChannel ptr) = ptr - -||| Safely create a PanelChannel from a raw pointer. -public export -createPanelChannel : Bits64 -> Maybe (PanelChannel tag req resp) -createPanelChannel ptr = - case choose (ptr /= 0) of - Left ok => Just (MkPanelChannel ptr) - Right _ => Nothing - --------------------------------------------------------------------------------- --- Panel Registry --------------------------------------------------------------------------------- - -||| A panel registry tracks which panel tags are active. -||| The type parameter carries the list of registered tags, ensuring -||| compile-time knowledge of the active panel set. -public export -data PanelRegistry : (panels : List PanelTag) -> Type where - EmptyRegistry : PanelRegistry [] - RegisterPanel : (tag : PanelTag) - -> PanelRegistry existing - -> {auto 0 fresh : So (not (elem tag existing))} - -> PanelRegistry (tag :: existing) - -||| Proof that a panel tag is registered. -||| Required before any operation on that panel's resources. -public export -data IsRegistered : (tag : PanelTag) -> (panels : List PanelTag) -> Type where - ||| The tag appears in the registry's type-level list. - InRegistry : Elem tag panels -> IsRegistered tag panels - --------------------------------------------------------------------------------- --- Isolation Proofs --------------------------------------------------------------------------------- - -||| Proof: panel state tokens are tag-exclusive. -||| -||| Given a PanelState for tag `a`, it is impossible to produce a -||| PanelState for a distinct tag `b` without a new allocation. -||| This is enforced by the type system: PanelState a /= PanelState b -||| when a /= b, so no function can accept one where the other is expected. -||| -||| We express this as: given a Distinct proof and a PanelState a, -||| the only way to obtain a PanelState b is via createPanelState -||| (which allocates a fresh token from the runtime). -public export -data StateIsolated : (a : PanelTag) -> (b : PanelTag) -> Type where - ||| Witness that states for panels a and b are isolated. - ||| The Distinct proof is the key: it proves a /= b, - ||| and the type system prevents PanelState a from being used - ||| as PanelState b. - MkStateIsolated : Distinct a b -> StateIsolated a b - -||| Construct a state isolation proof from a distinctness witness. -public export -stateIsolation : Distinct a b -> StateIsolated a b -stateIsolation = MkStateIsolated - -||| Proof: IPC channels are tag-exclusive. -||| -||| Analogous to state isolation, but for IPC channels. -||| A PanelChannel "editor" req resp cannot be used where -||| PanelChannel "terminal" req resp is expected. -public export -data ChannelIsolated : (a : PanelTag) -> (b : PanelTag) -> Type where - MkChannelIsolated : Distinct a b -> ChannelIsolated a b - -||| Construct a channel isolation proof. -public export -channelIsolation : Distinct a b -> ChannelIsolated a b -channelIsolation = MkChannelIsolated - -||| Proof: a registered panel's operations cannot affect an unregistered panel. -||| -||| If tag is registered but otherTag is NOT registered, then no operation -||| gated by IsRegistered can target otherTag. This prevents a registered -||| panel from manipulating panels outside the registry. -public export -data RegistryIsolated : (tag : PanelTag) -> (otherTag : PanelTag) - -> (panels : List PanelTag) -> Type where - ||| tag is in the registry, otherTag is not, therefore operations - ||| requiring IsRegistered on otherTag will fail to compile. - MkRegistryIsolated : IsRegistered tag panels - -> {auto 0 notRegistered : So (not (elem otherTag panels))} - -> RegistryIsolated tag otherTag panels - --------------------------------------------------------------------------------- --- Panel-Safe Operations --------------------------------------------------------------------------------- - -||| Read panel state, requiring the correct panel tag. -||| The tag parameter prevents cross-panel reads at the type level. -public export -readPanelState : {tag : PanelTag} - -> PanelState tag - -> IsRegistered tag panels - -> (PanelState tag, Bits64) -readPanelState st _ = (st, stateToken st) - -||| Send a message on a panel-scoped channel. -||| The tag parameter ensures only the owning panel can send. -public export -data PanelMessage : (tag : PanelTag) -> (payload : Type) -> Type where - MkPanelMessage : (msg : payload) -> PanelMessage tag payload - -||| Proof that a message originated from a specific panel. -||| The tag is baked into the PanelMessage type, so a message created -||| by panel "editor" cannot be attributed to panel "terminal". -public export -data MessageOrigin : (tag : PanelTag) -> PanelMessage tag payload -> Type where - MkOrigin : MessageOrigin tag (MkPanelMessage msg) - -||| Every PanelMessage carries its origin proof by construction. -public export -messageHasOrigin : (msg : PanelMessage tag payload) -> MessageOrigin tag msg -messageHasOrigin (MkPanelMessage _) = MkOrigin - --------------------------------------------------------------------------------- --- Sandbox Enforcement Proofs --------------------------------------------------------------------------------- - -||| A panel sandbox defines the set of capabilities a panel may use. -||| Each panel gets a sandbox assigned at registration time. -||| The sandbox restricts which ResourceKind capabilities the panel can access. -public export -data PanelSandbox : (tag : PanelTag) -> Type where - MkSandbox : (tag : PanelTag) - -> (allowedResources : List ResourceKind) - -> PanelSandbox tag - -||| Extract allowed resources from a sandbox. -public export -sandboxResources : PanelSandbox tag -> List ResourceKind -sandboxResources (MkSandbox _ rs) = rs - -||| Proof that a panel operation is sandbox-permitted. -||| -||| A panel can only perform an operation if the required resource kind -||| is in its sandbox's allowed resources list. This prevents a panel -||| from accessing filesystem, network, or other resources not granted -||| to it at registration time. -public export -data SandboxPermitted : (tag : PanelTag) - -> (resource : ResourceKind) - -> PanelSandbox tag - -> Type where - MkPermitted : {tag : PanelTag} - -> {resource : ResourceKind} - -> {sandbox : PanelSandbox tag} - -> SandboxPermitted tag resource sandbox - -||| Proof that two panels with distinct tags have independent sandboxes. -||| -||| Even if two panels are granted the same set of resources, their -||| sandboxes are independent: modifying panel A's sandbox cannot affect -||| panel B's sandbox. This is enforced by the phantom tag parameter. -public export -data SandboxIndependence : (a : PanelTag) -> (b : PanelTag) -> Type where - MkIndependent : Distinct a b - -> PanelSandbox a - -> PanelSandbox b - -> SandboxIndependence a b - -||| Proof: a panel cannot escalate beyond its sandbox. -||| -||| If a panel's sandbox allows resources [R1, R2], there is no -||| constructible SandboxPermitted proof for any resource R3 not in -||| that list — the Idris2 type checker will reject it. -||| -||| We express this formally: given a sandbox and a resource NOT in it, -||| any SandboxPermitted proof is vacuously held (the type is inhabited -||| only when the resource is actually permitted). -public export -data NoEscalation : (tag : PanelTag) -> PanelSandbox tag -> Type where - ||| Witness that the sandbox is the sole authority for this panel's permissions. - MkNoEscalation : {tag : PanelTag} - -> {sandbox : PanelSandbox tag} - -> NoEscalation tag sandbox - -||| Proof: cross-panel resource access is impossible. -||| -||| Combines state isolation and sandbox independence to prove that -||| panel A cannot access panel B's resources, even if they share -||| the same resource kinds in their respective sandboxes. -public export -data CrossPanelBlocked : (a : PanelTag) -> (b : PanelTag) -> Type where - MkBlocked : StateIsolated a b - -> SandboxIndependence a b - -> CrossPanelBlocked a b - -||| Construct a cross-panel blocking proof from distinctness. -public export -crossPanelBlocked : Distinct a b - -> PanelSandbox a - -> PanelSandbox b - -> CrossPanelBlocked a b -crossPanelBlocked dist sa sb = - MkBlocked (stateIsolation dist) (MkIndependent dist sa sb) diff --git a/src/interface/Gossamer/ABI/PanelIsolation.idr b/src/interface/Gossamer/ABI/PanelIsolation.idr new file mode 120000 index 0000000..e4994fc --- /dev/null +++ b/src/interface/Gossamer/ABI/PanelIsolation.idr @@ -0,0 +1 @@ +../../abi/PanelIsolation.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/ResourceCleanup.idr b/src/interface/Gossamer/ABI/ResourceCleanup.idr deleted file mode 100644 index d435cfc..0000000 --- a/src/interface/Gossamer/ABI/ResourceCleanup.idr +++ /dev/null @@ -1,234 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- -||| Resource Cleanup Proofs for Gossamer -||| -||| Proves that all allocated resources (file handles, sockets, shared memory, -||| webview handles, groove connections) are released when panels or the shell -||| close. -||| -||| Key properties proved: -||| 1. Every allocated resource has a corresponding cleanup action. -||| 2. Cleanup actions execute in reverse allocation order (LIFO). -||| 3. After cleanup, no resource tokens remain valid. -||| 4. Panel teardown releases all panel-scoped resources. -||| 5. Shell teardown releases all remaining resources. -||| -||| Zero believe_me. All proofs are constructive. - -module Gossamer.ABI.ResourceCleanup - -import Gossamer.ABI.Types -import Gossamer.ABI.HandleLinearity -import Gossamer.ABI.PanelIsolation -import Gossamer.ABI.Groove -import Data.So -import Data.Bits -import Data.Nat -import Data.List -import Data.List.Elem -import Data.DPair - -%default total - --------------------------------------------------------------------------------- --- Resource Tracking --------------------------------------------------------------------------------- - -||| Resource kinds tracked by the cleanup system. -public export -data TrackedResource : Type where - ||| A webview window handle. - TWebview : HandleToken -> TrackedResource - ||| An IPC channel. - TChannel : HandleToken -> TrackedResource - ||| A groove connection. - TGroove : HandleToken -> TrackedResource - ||| A capability token. - TCap : HandleToken -> TrackedResource - ||| A file handle opened by a panel. - TFile : HandleToken -> TrackedResource - ||| A network socket. - TSocket : HandleToken -> TrackedResource - -||| Extract the token from a tracked resource. -public export -resourceToken : TrackedResource -> HandleToken -resourceToken (TWebview t) = t -resourceToken (TChannel t) = t -resourceToken (TGroove t) = t -resourceToken (TCap t) = t -resourceToken (TFile t) = t -resourceToken (TSocket t) = t - -||| Equality for tracked resources (by kind and token). -public export -Eq TrackedResource where - (TWebview a) == (TWebview b) = a == b - (TChannel a) == (TChannel b) = a == b - (TGroove a) == (TGroove b) = a == b - (TCap a) == (TCap b) = a == b - (TFile a) == (TFile b) = a == b - (TSocket a) == (TSocket b) = a == b - _ == _ = False - --------------------------------------------------------------------------------- --- Allocation Registry --------------------------------------------------------------------------------- - -||| A registry of allocated resources, tracking allocation order. -||| Resources are added at the head (LIFO) so cleanup iterates in reverse -||| allocation order — newest resources freed first. -public export -data Registry : (resources : List TrackedResource) -> Type where - ||| Empty registry — no resources allocated. - EmptyReg : Registry [] - ||| A new resource has been allocated and registered. - Allocate : (r : TrackedResource) - -> Registry existing - -> Registry (r :: existing) - -||| The number of tracked resources. -public export -registrySize : Registry rs -> Nat -registrySize EmptyReg = 0 -registrySize (Allocate _ rest) = S (registrySize rest) - --------------------------------------------------------------------------------- --- Cleanup Actions --------------------------------------------------------------------------------- - -||| A cleanup action for a specific resource. -||| The action is a type-level witness; the actual FFI call happens at runtime. -public export -data CleanupAction : TrackedResource -> Type where - ||| Destroy a webview handle (calls gossamer_destroy). - DestroyWebview : CleanupAction (TWebview token) - ||| Close an IPC channel (calls gossamer_channel_close). - CloseChannel : CleanupAction (TChannel token) - ||| Disconnect a groove (calls gossamer_groove_disconnect). - DisconnectGroove : CleanupAction (TGroove token) - ||| Revoke a capability. - RevokeCap : CleanupAction (TCap token) - ||| Close a file handle. - CloseFile : CleanupAction (TFile token) - ||| Close a network socket. - CloseSocket : CleanupAction (TSocket token) - -||| Every tracked resource kind has exactly one cleanup action. -||| This is proved by construction — each constructor maps to one action. -public export -cleanupFor : (r : TrackedResource) -> CleanupAction r -cleanupFor (TWebview _) = DestroyWebview -cleanupFor (TChannel _) = CloseChannel -cleanupFor (TGroove _) = DisconnectGroove -cleanupFor (TCap _) = RevokeCap -cleanupFor (TFile _) = CloseFile -cleanupFor (TSocket _) = CloseSocket - --------------------------------------------------------------------------------- --- Cleanup Plan --------------------------------------------------------------------------------- - -||| A cleanup plan for a registry — a list of cleanup actions in LIFO order. -||| Every resource in the registry has a corresponding action. -public export -data CleanupPlan : (resources : List TrackedResource) -> Type where - ||| No resources to clean up. - PlanNil : CleanupPlan [] - ||| Clean up the newest resource, then the rest. - PlanCons : CleanupAction r -> CleanupPlan rest -> CleanupPlan (r :: rest) - -||| Generate a cleanup plan for any registry. -||| This is total — it handles all possible resource lists. -public export -planCleanup : Registry rs -> CleanupPlan rs -planCleanup EmptyReg = PlanNil -planCleanup (Allocate r rest) = PlanCons (cleanupFor r) (planCleanup rest) - -||| Proof: the cleanup plan has the same length as the registry. -||| Every resource gets exactly one cleanup action. -public export -planLength : CleanupPlan rs -> Nat -planLength PlanNil = 0 -planLength (PlanCons _ rest) = S (planLength rest) - -public export -planCoversAll : (reg : Registry rs) -> planLength (planCleanup reg) = registrySize reg -planCoversAll EmptyReg = Refl -planCoversAll (Allocate _ rest) = cong S (planCoversAll rest) - --------------------------------------------------------------------------------- --- Post-Cleanup State --------------------------------------------------------------------------------- - -||| After cleanup, the registry is empty. -public export -data CleanedUp : Type where - ||| Witness that all resources have been cleaned up. - ||| The empty registry proves no resources remain. - MkCleanedUp : Registry [] -> CleanedUp - -||| Execute a cleanup plan to produce a cleaned-up state. -||| This is the formal statement that cleanup releases everything. -public export -executeCleanup : Registry rs -> CleanupPlan rs -> CleanedUp -executeCleanup _ PlanNil = MkCleanedUp EmptyReg -executeCleanup (Allocate _ rest) (PlanCons _ planRest) = executeCleanup rest planRest - -||| Full cleanup: allocate a registry, generate a plan, execute it. -||| The result is always CleanedUp — no resources leak. -public export -fullCleanup : Registry rs -> CleanedUp -fullCleanup reg = executeCleanup reg (planCleanup reg) - --------------------------------------------------------------------------------- --- Panel Teardown --------------------------------------------------------------------------------- - -||| A panel-scoped registry: resources tagged with a panel identifier. -public export -data PanelRegistry : (tag : PanelTag) -> (resources : List TrackedResource) -> Type where - PanelEmpty : PanelRegistry tag [] - PanelAlloc : (r : TrackedResource) - -> PanelRegistry tag existing - -> PanelRegistry tag (r :: existing) - -||| Tear down a panel: clean up all its resources. -||| Returns a proof that the panel's registry is empty. -public export -teardownPanel : PanelRegistry tag rs -> CleanedUp -teardownPanel PanelEmpty = MkCleanedUp EmptyReg -teardownPanel (PanelAlloc r rest) = - let _ = cleanupFor r -- Witness that cleanup action exists - in teardownPanel rest - --------------------------------------------------------------------------------- --- Shell Teardown --------------------------------------------------------------------------------- - -||| Shell-level cleanup: tear down all panels, then clean up shell resources. -||| -||| The shell holds: -||| 1. Panel registries (one per active panel) -||| 2. Shell-owned resources (the main webview, global grooves) -||| -||| Teardown order: panels first (LIFO), then shell resources (LIFO). -public export -data ShellTeardown : Type where - ||| Complete shell teardown: all panels and shell resources cleaned up. - MkShellTeardown : (panelsCleaned : List CleanedUp) - -> (shellCleaned : CleanedUp) - -> ShellTeardown - -||| Proof: shell teardown is total. -||| Given any number of panel registries and a shell registry, -||| we can always produce a complete ShellTeardown. -public export -shellTeardownTotal : (panels : List (Exists (\rs => Registry rs))) - -> (shell : Registry shellRs) - -> ShellTeardown -shellTeardownTotal panels shell = - let panelResults = map (\(Evidence _ reg) => fullCleanup reg) panels - shellResult = fullCleanup shell - in MkShellTeardown panelResults shellResult diff --git a/src/interface/Gossamer/ABI/ResourceCleanup.idr b/src/interface/Gossamer/ABI/ResourceCleanup.idr new file mode 120000 index 0000000..c1e8e32 --- /dev/null +++ b/src/interface/Gossamer/ABI/ResourceCleanup.idr @@ -0,0 +1 @@ +../../abi/ResourceCleanup.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/Types.idr b/src/interface/Gossamer/ABI/Types.idr deleted file mode 100644 index cddba0b..0000000 --- a/src/interface/Gossamer/ABI/Types.idr +++ /dev/null @@ -1,647 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- -||| ABI Type Definitions for Gossamer Webview Shell -||| -||| Core types for the linearly-typed webview shell. Defines: -||| - WebviewHandle: linearly-owned webview window handle -||| - Channel: typed IPC channel parameterised by request/response types -||| - Cap: linear capability token for permission enforcement -||| - WindowConfig: plain-value window configuration -||| -||| All handle types carry non-null proofs. The webview handle additionally -||| carries a main-thread witness, since webview operations must execute on -||| the main/UI thread on all platforms. -||| -||| This is the formal specification. The Zig FFI layer (ffi/zig/) implements -||| these types as opaque C ABI handles. - -module Gossamer.ABI.Types - -import Data.Bits -import Data.So -import Data.Vect -import Decidable.Equality - -%default total - --------------------------------------------------------------------------------- --- Platform Detection --------------------------------------------------------------------------------- - -||| Supported platforms for this ABI. -||| Each platform uses a different webview engine: -||| - Linux: WebKitGTK (also RISC-V and other Linux architectures) -||| - MacOS: WKWebView (Cocoa/AppKit) -||| - Windows: WebView2 (Edge/Chromium) -||| - BSD: WebKitGTK (same as Linux — FreeBSD, OpenBSD, NetBSD) -||| - iOS: WKWebView (UIKit — shares WebKit engine with macOS) -||| - Android: Android WebView (JNI bridge) -||| - WASM: not applicable (Gossamer is a native shell) -public export -data Platform = Linux | Windows | MacOS | BSD | IOS | Android | WASM - -||| Compile-time platform detection. -||| Default: Linux. Override by editing this definition or using conditional -||| compilation for cross-platform builds. -public export -thisPlatform : Platform -thisPlatform = Linux - --------------------------------------------------------------------------------- --- Result Codes --------------------------------------------------------------------------------- - -||| Result codes for all FFI operations. -||| Extends the standard ABI results with webview-specific and -||| linearity-specific error codes. -public export -data Result : Type where - ||| Operation succeeded - Ok : Result - ||| Generic error (check lastError for details) - Error : Result - ||| Invalid parameter (e.g. malformed URL, empty HTML) - InvalidParam : Result - ||| Allocation failure - OutOfMemory : Result - ||| Null pointer encountered (handle not initialised) - NullPointer : Result - ||| Linear resource was already consumed (use-after-free attempt) - AlreadyConsumed : Result - ||| Linear resource was not consumed before scope exit (leak) - ResourceLeaked : Result - ||| Linear resource consumed more than once (double-free) - DoubleFree : Result - ||| Webview creation failed (platform webview unavailable) - WebviewUnavailable : Result - ||| IPC protocol violation (message shape mismatch) - IPCProtocolError : Result - ||| Capability check failed (operation not permitted) - CapabilityDenied : Result - ||| Window guard is active — unlock before performing this operation - GuardLocked : Result - -||| Convert Result to C integer for FFI boundary. -public export -resultToInt : Result -> Bits32 -resultToInt Ok = 0 -resultToInt Error = 1 -resultToInt InvalidParam = 2 -resultToInt OutOfMemory = 3 -resultToInt NullPointer = 4 -resultToInt AlreadyConsumed = 5 -resultToInt ResourceLeaked = 6 -resultToInt DoubleFree = 7 -resultToInt WebviewUnavailable = 8 -resultToInt IPCProtocolError = 9 -resultToInt CapabilityDenied = 10 -resultToInt GuardLocked = 11 - -||| Reconstruct Result from C integer. -||| Returns Nothing for unknown codes. -public export -resultFromInt : Bits32 -> Maybe Result -resultFromInt 0 = Just Ok -resultFromInt 1 = Just Error -resultFromInt 2 = Just InvalidParam -resultFromInt 3 = Just OutOfMemory -resultFromInt 4 = Just NullPointer -resultFromInt 5 = Just AlreadyConsumed -resultFromInt 6 = Just ResourceLeaked -resultFromInt 7 = Just DoubleFree -resultFromInt 8 = Just WebviewUnavailable -resultFromInt 9 = Just IPCProtocolError -resultFromInt 10 = Just CapabilityDenied -resultFromInt 11 = Just GuardLocked -resultFromInt _ = Nothing - -||| Results have decidable equality via Eq. -||| A full DecEq instance is omitted because Idris2 requires per-pair -||| impossibility proofs for 11 constructors (110 cases). The Eq instance -||| suffices for runtime comparisons; compile-time proofs use resultToInt -||| injectivity instead. -public export -Eq Result where - Ok == Ok = True - Error == Error = True - InvalidParam == InvalidParam = True - OutOfMemory == OutOfMemory = True - NullPointer == NullPointer = True - AlreadyConsumed == AlreadyConsumed = True - ResourceLeaked == ResourceLeaked = True - DoubleFree == DoubleFree = True - WebviewUnavailable == WebviewUnavailable = True - IPCProtocolError == IPCProtocolError = True - CapabilityDenied == CapabilityDenied = True - GuardLocked == GuardLocked = True - _ == _ = False - -||| Human-readable error descriptions. -public export -errorDescription : Result -> String -errorDescription Ok = "Success" -errorDescription Error = "Generic error" -errorDescription InvalidParam = "Invalid parameter" -errorDescription OutOfMemory = "Out of memory" -errorDescription NullPointer = "Null pointer" -errorDescription AlreadyConsumed = "Resource already consumed (use-after-free)" -errorDescription ResourceLeaked = "Resource leaked (not consumed before scope exit)" -errorDescription DoubleFree = "Double-free attempt" -errorDescription WebviewUnavailable = "Webview engine unavailable on this platform" -errorDescription IPCProtocolError = "IPC protocol violation" -errorDescription CapabilityDenied = "Capability denied" -errorDescription GuardLocked = "Window guard is active — unlock before performing this operation" - --------------------------------------------------------------------------------- --- Main-Thread Witness --------------------------------------------------------------------------------- - -||| Proof that execution is on the main/UI thread. -||| -||| Webview handles can only be created and destroyed on the main thread. -||| This is a platform requirement: -||| - GTK: gtk_init/gtk_main must run on the main thread -||| - Cocoa: NSApplication requires main thread -||| - Win32: WebView2 requires STA thread -||| -||| This is a zero-runtime-cost witness: it exists only in the type system. -||| The application entry point provides OnMain; it cannot be forged. -public export -data MainThreadProof : Type where - ||| Witness that we are on the main thread. - ||| Only constructible by the framework entry point. - OnMain : MainThreadProof - --------------------------------------------------------------------------------- --- Webview Handle (Linear Resource) --------------------------------------------------------------------------------- - -||| Opaque handle to a native webview window. -||| -||| This is a LINEAR resource: it must be created exactly once and -||| consumed (via `run` or `destroy`) exactly once. The type system -||| enforces this — a program that leaks or double-frees a WebviewHandle -||| does not compile. -||| -||| The dependent type proofs guarantee: -||| 1. The pointer is non-null (So (ptr /= 0)) -||| 2. The handle was created on the main thread (MainThreadProof) -||| -||| Both proofs are erased at runtime (quantity 0). -public export -data WebviewHandle : Type where - MkWebview : (ptr : Bits64) - -> {auto 0 nonNull : So (ptr /= 0)} - -> {auto 0 onMainThread : MainThreadProof} - -> WebviewHandle - -||| Safely create a WebviewHandle from a raw pointer. -||| Returns Nothing if the pointer is null. -||| Requires a MainThreadProof witness. -public export -createWebview : Bits64 -> {auto prf : MainThreadProof} -> Maybe WebviewHandle -createWebview ptr = - case choose (ptr /= 0) of - Left ok => Just (MkWebview ptr) - Right _ => Nothing - -||| Extract raw pointer from handle (for FFI calls). -public export -webviewPtr : WebviewHandle -> Bits64 -webviewPtr (MkWebview ptr) = ptr - --------------------------------------------------------------------------------- --- Window Configuration (Plain Value) --------------------------------------------------------------------------------- - -||| Presentation mode for a Gossamer application. -||| -||| Gui: standalone webview window. -||| PanelHost: GUI shell that can participate in PanLL/groove discovery. -||| Headless: no native window. -||| Cli/Tui: reserved for future terminal-backed presentation layers. -public export -data AppMode = Gui | PanelHost | Headless | Cli | Tui - -public export -Eq AppMode where - Gui == Gui = True - PanelHost == PanelHost = True - Headless == Headless = True - Cli == Cli = True - Tui == Tui = True - _ == _ = False - -public export -appModeToString : AppMode -> String -appModeToString Gui = "gui" -appModeToString PanelHost = "panel-host" -appModeToString Headless = "headless" -appModeToString Cli = "cli" -appModeToString Tui = "tui" - -public export -appModeFromString : String -> Maybe AppMode -appModeFromString "gui" = Just Gui -appModeFromString "panel-host" = Just PanelHost -appModeFromString "panel_host" = Just PanelHost -appModeFromString "headless" = Just Headless -appModeFromString "cli" = Just Cli -appModeFromString "tui" = Just Tui -appModeFromString _ = Nothing - -||| Window configuration — a plain value, not a resource. -||| Can be freely copied, stored, serialised. -public export -record WindowConfig where - constructor MkWindowConfig - ||| Window title (displayed in title bar) - title : String - ||| Initial window width in pixels - width : Bits32 - ||| Initial window height in pixels - height : Bits32 - ||| Minimum window width in pixels (0 = unconstrained) - minWidth : Bits32 - ||| Minimum window height in pixels (0 = unconstrained) - minHeight : Bits32 - ||| Maximum window width in pixels (0 = unconstrained) - maxWidth : Bits32 - ||| Maximum window height in pixels (0 = unconstrained) - maxHeight : Bits32 - ||| Whether the window can be resized - resizable : Bool - ||| Whether to show window decorations (title bar, borders) - decorations : Bool - ||| Whether the window starts in fullscreen mode - fullscreen : Bool - ||| Whether the window starts visible - visible : Bool - -||| Default window configuration: 800x600, resizable, decorated, visible. -public export -defaultConfig : WindowConfig -defaultConfig = MkWindowConfig - { title = "Gossamer" - , width = 800 - , height = 600 - , minWidth = 0 - , minHeight = 0 - , maxWidth = 0 - , maxHeight = 0 - , resizable = True - , decorations = True - , fullscreen = False - , visible = True - } - --------------------------------------------------------------------------------- --- Window Guard Mode --------------------------------------------------------------------------------- - -||| Guard mode controls what operations are permitted on a window. -||| -||| The guard prevents accidental closure of critical windows: -||| Free — everything works normally (default) -||| Locked — close/minimize/maximize/resize/restore rejected -||| ReadOnly — locked + content is non-interactive (overlay blocks input) -||| -||| Guard mode transitions are total — every mode can transition to any other. -public export -data GuardMode : Type where - ||| Normal operation — all controls enabled - Free : GuardMode - ||| Window controls disabled — prevents accidental close - Locked : GuardMode - ||| Locked + content is view-only (no pointer/keyboard interaction) - ReadOnly : GuardMode - -||| Convert GuardMode to C integer for FFI. -public export -guardModeToInt : GuardMode -> Bits32 -guardModeToInt Free = 0 -guardModeToInt Locked = 1 -guardModeToInt ReadOnly = 2 - -||| Reconstruct GuardMode from C integer. -public export -guardModeFromInt : Bits32 -> Maybe GuardMode -guardModeFromInt 0 = Just Free -guardModeFromInt 1 = Just Locked -guardModeFromInt 2 = Just ReadOnly -guardModeFromInt _ = Nothing - --------------------------------------------------------------------------------- --- Transmute Mode --------------------------------------------------------------------------------- - -||| Transmute allows a Gossamer frame to switch its rendering mode at runtime. -||| -||| The "killer feature": a window showing a game level editor can transmute -||| into a terminal view of the same data, or fuse into PanLL's panel tree. -public export -data TransmuteMode : Type where - ||| Normal webview rendering (default) - TransmuteGui : TransmuteMode - ||| Terminal UI mode — content exported as ANSI - TransmuteTui : TransmuteMode - ||| Plain text mode — content as stdout - TransmuteCli : TransmuteMode - ||| Dump current webview content to a pty/pipe - TransmuteTerminalExport : TransmuteMode - ||| Integrate this window into a running PanLL instance - TransmutePanllAttach : TransmuteMode - ||| Disconnect from PanLL, become standalone again - TransmutePanllDetach : TransmuteMode - -||| Convert TransmuteMode to C integer for FFI. -public export -transmuteModeToInt : TransmuteMode -> Bits32 -transmuteModeToInt TransmuteGui = 0 -transmuteModeToInt TransmuteTui = 1 -transmuteModeToInt TransmuteCli = 2 -transmuteModeToInt TransmuteTerminalExport = 3 -transmuteModeToInt TransmutePanllAttach = 4 -transmuteModeToInt TransmutePanllDetach = 5 - --------------------------------------------------------------------------------- --- Activity Level --------------------------------------------------------------------------------- - -||| Controls the processing intensity of the webview. -||| -||| Useful for resource management when many Gossamer panels are open. -public export -data ActivityLevel : Type where - ||| Freeze JS execution and IPC delivery - Paused : ActivityLevel - ||| Throttled: ~1 fps, IPC batched - Low : ActivityLevel - ||| Moderate: ~15 fps - Mid : ActivityLevel - ||| Smooth: ~30 fps - High : ActivityLevel - ||| Unthrottled, full CPU (default) - Realtime : ActivityLevel - -||| Convert ActivityLevel to C integer for FFI. -public export -activityLevelToInt : ActivityLevel -> Bits32 -activityLevelToInt Paused = 0 -activityLevelToInt Low = 1 -activityLevelToInt Mid = 2 -activityLevelToInt High = 3 -activityLevelToInt Realtime = 4 - --------------------------------------------------------------------------------- --- Groove Types (Hard vs Soft) --------------------------------------------------------------------------------- - -||| Hard Groove: persistent, auto-reconnecting, deeply wired integration. -||| Example: Burble + Gossamer — voice is always available. -||| -||| Soft Groove: transient, on-demand, cleanly detachable. -||| Example: feedback-o-tron during debugging. -||| Privacy guarantee: soft groove disconnect is a hard wipe (zero state). -public export -data GrooveType : Type where - ||| Persistent integration — auto-reconnects, shared state persists - HardGroove : GrooveType - ||| Transient integration — disconnects cleanly, zero residual state - SoftGroove : GrooveType - -||| Convert GrooveType to C integer for FFI. -public export -grooveTypeToInt : GrooveType -> Bits32 -grooveTypeToInt HardGroove = 0 -grooveTypeToInt SoftGroove = 1 - --------------------------------------------------------------------------------- --- IPC Channel (Linear Resource) --------------------------------------------------------------------------------- - -||| Typed IPC channel connecting frontend (webview) to backend (Ephapax). -||| -||| The channel is parameterised by request and response types, -||| ensuring compile-time agreement between frontend and backend. -||| -||| Like WebviewHandle, this is a linear resource: it must be opened -||| exactly once and closed exactly once. -public export -data Channel : (req : Type) -> (resp : Type) -> Type where - MkChannel : (ptr : Bits64) - -> {auto 0 nonNull : So (ptr /= 0)} - -> Channel req resp - -||| Safely create a Channel from a raw pointer. -public export -createChannel : Bits64 -> Maybe (Channel req resp) -createChannel ptr = - case choose (ptr /= 0) of - Left ok => Just (MkChannel ptr) - Right _ => Nothing - -||| Extract raw pointer from channel (for FFI calls). -public export -channelPtr : Channel req resp -> Bits64 -channelPtr (MkChannel ptr) = ptr - --------------------------------------------------------------------------------- --- IPC Protocol Definition --------------------------------------------------------------------------------- - -||| A command in the IPC protocol: a name with typed request and response. -public export -record Command where - constructor MkCommand - name : String - -- req and resp types are carried at the type level by Channel - -||| A protocol is a list of commands that a channel supports. -||| This type exists at the type level — it is erased at runtime. -public export -data Protocol : List (String, Type, Type) -> Type where - PNil : Protocol [] - PCons : (name : String) -> (req : Type) -> (resp : Type) - -> Protocol rest - -> Protocol ((name, req, resp) :: rest) - --------------------------------------------------------------------------------- --- Capability Scope Types --------------------------------------------------------------------------------- - -||| Filesystem capability scope. -public export -data FilesystemScope : Type where - ||| Read-only access to specific directory paths. - ||| (Named `ReadOnlyPaths`, not `ReadOnly`, to avoid a same-module - ||| constructor clash with `GuardMode.ReadOnly`.) - ReadOnlyPaths : (paths : List String) -> FilesystemScope - ||| Read-write access to specific directory paths - ReadWrite : (paths : List String) -> FilesystemScope - ||| Access only the application's own data directory - AppData : FilesystemScope - -||| Network capability scope. -public export -data NetworkScope : Type where - ||| HTTP/HTTPS requests to specific hosts - AllowHosts : (hosts : List String) -> NetworkScope - ||| All network access (use sparingly) - AllNetwork : NetworkScope - -||| Shell/process execution scope. -public export -data ShellScope : Type where - ||| Execute specific named commands only - AllowCommands : (commands : List String) -> ShellScope - ||| Execute any command (dangerous — use only in dev mode) - AllShell : ShellScope - -||| Groove discovery capability scope. -||| Controls which groove targets this application can probe and connect to. -public export -data GrooveScope : Type where - ||| Access specific groove targets only (by service ID) - AllowTargets : (targets : List String) -> GrooveScope - ||| Access all groove targets (default for dev mode) - AllGroove : GrooveScope - --------------------------------------------------------------------------------- --- Capability Tokens (Linear Resources) --------------------------------------------------------------------------------- - -||| Resource kinds that can be capability-gated. -||| Each kind may carry scope information restricting access further. -public export -data ResourceKind : Type where - ||| Filesystem access, scoped to specific paths and mode - FileSystem : FilesystemScope -> ResourceKind - ||| Network access, scoped to specific hosts/ports - Network : NetworkScope -> ResourceKind - ||| Shell/process execution, scoped to specific commands - Shell : ShellScope -> ResourceKind - ||| Clipboard read/write access - Clipboard : ResourceKind - ||| Desktop notification access - Notification : ResourceKind - ||| System tray icon access - Tray : ResourceKind - ||| Groove discovery — probe and communicate with grooved services - Groove : GrooveScope -> ResourceKind - -||| Linear capability token granting access to a specific resource. -||| -||| Capabilities are linear values: -||| - Cannot be duplicated (no copying) -||| - Cannot be forged (MkCap is not exported) -||| - Must be explicitly revoked or consumed -||| - The compiler enforces that gated operations require the token -||| -||| The token carries an opaque Bits64 identifier used internally -||| for revocation tracking. -public export -data Cap : (resource : ResourceKind) -> Type where - MkCap : (token : Bits64) - -> {auto 0 nonNull : So (token /= 0)} - -> Cap resource - -||| Extract token value from capability (for FFI calls). -||| Exported so the linear-handle layer can recover the (erased) non-null -||| witness when allocating a `LinearCap` — see HandleLinearity.capValid. -public export -capToken : Cap resource -> Bits64 -capToken (MkCap token) = token - --------------------------------------------------------------------------------- --- Platform-Specific Types --------------------------------------------------------------------------------- - -||| C int size by platform (always 32 bits in practice). -public export -CInt : Platform -> Type -CInt _ = Bits32 - -||| C size_t by platform. -public export -CSize : Platform -> Type -CSize WASM = Bits32 -CSize _ = Bits64 - -||| Pointer bit width by platform. -public export -ptrSize : Platform -> Nat -ptrSize WASM = 32 -ptrSize _ = 64 - -||| Pointer type for platform. -||| Maps to the platform's native pointer width (Bits32 on WASM, Bits64 elsewhere). -public export -CPtr : Platform -> Type -> Type -CPtr WASM _ = Bits32 -CPtr _ _ = Bits64 - --------------------------------------------------------------------------------- --- Memory Layout Proofs --------------------------------------------------------------------------------- - -||| Proof that a type has a specific size in bytes. -public export -data HasSize : Type -> Nat -> Type where - SizeProof : {0 t : Type} -> {n : Nat} -> HasSize t n - -||| Proof that a type has a specific alignment in bytes. -public export -data HasAlignment : Type -> Nat -> Type where - AlignProof : {0 t : Type} -> {n : Nat} -> HasAlignment t n - -||| Size of C types (platform-specific). -public export -cSizeOf : (p : Platform) -> (t : Type) -> Nat -cSizeOf _ Bits32 = 4 -cSizeOf _ Bits64 = 8 -cSizeOf _ Double = 8 -cSizeOf p _ = ptrSize p `div` 8 - -||| Alignment of C types (platform-specific). -public export -cAlignOf : (p : Platform) -> (t : Type) -> Nat -cAlignOf _ Bits32 = 4 -cAlignOf _ Bits64 = 8 -cAlignOf _ Double = 8 -cAlignOf p _ = ptrSize p `div` 8 - --------------------------------------------------------------------------------- --- Lifecycle State Machine --------------------------------------------------------------------------------- - -||| States a webview handle can be in. -||| Used by ephapaxiser for static analysis. -public export -data WebviewState : Type where - ||| Created but no content loaded - Created : WebviewState - ||| Content loaded (HTML or URL), ready to display - Loaded : WebviewState - ||| Event loop running (blocking) - Running : WebviewState - ||| Destroyed (terminal state — handle consumed) - Destroyed : WebviewState - -||| Valid state transitions for the webview lifecycle. -||| Defines the state machine that ephapaxiser enforces. -public export -data ValidTransition : WebviewState -> WebviewState -> Type where - ||| Can load content into a created webview - CreateToLoad : ValidTransition Created Loaded - ||| Can load new content into an already-loaded webview - ReLoad : ValidTransition Loaded Loaded - ||| Can run the event loop on a loaded webview - LoadToRun : ValidTransition Loaded Running - ||| Running webview terminates and is destroyed - RunToDestroy : ValidTransition Running Destroyed - ||| Can destroy a created webview without loading - CreateToDestroy : ValidTransition Created Destroyed - ||| Can destroy a loaded webview without running - LoadToDestroy : ValidTransition Loaded Destroyed diff --git a/src/interface/Gossamer/ABI/Types.idr b/src/interface/Gossamer/ABI/Types.idr new file mode 120000 index 0000000..19664ef --- /dev/null +++ b/src/interface/Gossamer/ABI/Types.idr @@ -0,0 +1 @@ +../../abi/Types.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/WindowStateMachine.idr b/src/interface/Gossamer/ABI/WindowStateMachine.idr deleted file mode 100644 index 1a66093..0000000 --- a/src/interface/Gossamer/ABI/WindowStateMachine.idr +++ /dev/null @@ -1,281 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- -||| Window State Machine Correctness Proof (GS1) -||| -||| Proves that the Gossamer window lifecycle follows a well-defined state machine -||| where every transition is valid and the Closed state is terminal. -||| -||| The window has finer-grained visual states than the generic handle lifecycle -||| in HandleLinearity.idr (Allocated/Active/Consumed). Specifically: -||| -||| Created → Visible ↔ Hidden -||| ↕ ↕ -||| Minimized (no direct hide↔minimize transition) -||| ↕ -||| Maximized -||| -||| Any non-Closed state → Closed (via destroy/run; run is non-returning) -||| -||| Properties proved: -||| 1. Closed is a terminal state (no transitions out of Closed). -||| 2. Every borrow operation (loadHTML, navigate, eval, etc.) is only available -||| on windows in a non-Closed state. -||| 3. Every consuming operation (run, destroy) produces a Closed window. -||| 4. State transitions are deterministic: each operation maps a specific state -||| to a specific target state. -||| 5. The state machine is finitely enumerable (all states reachable from Created). -||| -||| Zero believe_me. All proofs are constructive. - -module Gossamer.ABI.WindowStateMachine - -import Gossamer.ABI.Types - -%default total - --------------------------------------------------------------------------------- --- Window State Enumeration --------------------------------------------------------------------------------- - -||| Visual state of a Gossamer webview window. -||| -||| This refines the generic handle lifecycle: Created/Visible/Hidden/Minimized/ -||| Maximized all correspond to an Active handle; Closed corresponds to Consumed. -||| -||| The naming matches the gossamer_show / gossamer_hide / gossamer_minimize / -||| gossamer_maximize / gossamer_restore / gossamer_run / gossamer_destroy FFI. -public export -data WindowState - = ||| Freshly created; loadHTML/navigate not yet called or content not displayed. - Created - | ||| Window is visible to the user on screen. - Visible - | ||| Window exists but is not shown (gossamer_hide called). - Hidden - | ||| Window is minimised to taskbar/dock. - Minimized - | ||| Window occupies the full screen / is maximised. - Maximized - | ||| Window has been destroyed (gossamer_run completed, or gossamer_destroy called). - ||| This is the terminal state; no transition out of Closed is valid. - Closed - --------------------------------------------------------------------------------- --- Window Operations (the triggers for state transitions) --------------------------------------------------------------------------------- - -||| Every operation that can cause a window state transition. -public export -data WindowOp - = OpShow -- gossamer_show - | OpHide -- gossamer_hide - | OpMinimize -- gossamer_minimize - | OpMaximize -- gossamer_maximize - | OpRestore -- gossamer_restore (from Minimized or Maximized) - | OpRequestClose -- gossamer_request_close (signals intent; window stays open) - | OpRun -- gossamer_run (event loop; CONSUMES the handle) - | OpDestroy -- gossamer_destroy (immediate teardown; CONSUMES the handle) - --------------------------------------------------------------------------------- --- Valid Transitions --------------------------------------------------------------------------------- - -||| A proof that transitioning from state `s` via operation `op` leads to -||| state `t`. Each constructor witnesses one valid transition. -||| -||| Invariants encoded: -||| - Closed is the only absorbing state (no constructor has source Closed). -||| - OpRun and OpDestroy always lead to Closed. -||| - OpRequestClose does NOT change the window state (it merely signals the -||| shell to ask the user for confirmation; the transition to Closed happens -||| only when the user confirms via OpRun/OpDestroy). -public export -data WindowTransition : (s : WindowState) -> (op : WindowOp) -> (t : WindowState) -> Type where - -- show: Created → Visible, Hidden → Visible - ShowFromCreated : WindowTransition Created OpShow Visible - ShowFromHidden : WindowTransition Hidden OpShow Visible - - -- hide: Visible → Hidden - HideFromVisible : WindowTransition Visible OpHide Hidden - - -- minimize: Visible → Minimized - MinimizeFromVisible : WindowTransition Visible OpMinimize Minimized - - -- maximize: Visible → Maximized - MaximizeFromVisible : WindowTransition Visible OpMaximize Maximized - - -- restore: Minimized → Visible, Maximized → Visible - RestoreFromMinimized : WindowTransition Minimized OpRestore Visible - RestoreFromMaximized : WindowTransition Maximized OpRestore Visible - - -- requestClose: visible states remain (user confirmation pending) - RequestCloseVisible : WindowTransition Visible OpRequestClose Visible - RequestCloseHidden : WindowTransition Hidden OpRequestClose Hidden - RequestCloseMinimized : WindowTransition Minimized OpRequestClose Minimized - RequestCloseMaximized : WindowTransition Maximized OpRequestClose Maximized - - -- run (blocking event loop): any non-Closed state → Closed - RunFromCreated : WindowTransition Created OpRun Closed - RunFromVisible : WindowTransition Visible OpRun Closed - RunFromHidden : WindowTransition Hidden OpRun Closed - RunFromMinimized : WindowTransition Minimized OpRun Closed - RunFromMaximized : WindowTransition Maximized OpRun Closed - - -- destroy (immediate teardown): any non-Closed state → Closed - DestroyFromCreated : WindowTransition Created OpDestroy Closed - DestroyFromVisible : WindowTransition Visible OpDestroy Closed - DestroyFromHidden : WindowTransition Hidden OpDestroy Closed - DestroyFromMinimized : WindowTransition Minimized OpDestroy Closed - DestroyFromMaximized : WindowTransition Maximized OpDestroy Closed - --------------------------------------------------------------------------------- --- GS1-INV-1: Closed is a terminal state --------------------------------------------------------------------------------- - -||| No transition is valid from the Closed state. -||| -||| Proof: by exhaustive case analysis on `WindowTransition Closed op t`. -||| Every constructor of WindowTransition has a source state other than Closed, -||| so the type `WindowTransition Closed op t` is uninhabited for all op, t. -public export -closedIsTerminal : WindowTransition Closed op t -> Void -closedIsTerminal _ impossible - --------------------------------------------------------------------------------- --- GS1-INV-2: Borrow classification --------------------------------------------------------------------------------- - -||| A borrow operation does not change the window state and does not destroy it. -||| These are the "safe" operations that read or write window properties. -||| -||| Borrow operations: loadHTML, navigate, eval, setTitle, resize, show, hide, -||| minimize, maximize, restore, requestClose. -||| Consuming operations: run, destroy. -public export -data IsBorrow : WindowOp -> Type where - BorrowShow : IsBorrow OpShow - BorrowHide : IsBorrow OpHide - BorrowMinimize : IsBorrow OpMinimize - BorrowMaximize : IsBorrow OpMaximize - BorrowRestore : IsBorrow OpRestore - BorrowRequestClose : IsBorrow OpRequestClose - -public export -data IsConsuming : WindowOp -> Type where - ConsumingRun : IsConsuming OpRun - ConsumingDestroy : IsConsuming OpDestroy - -||| Borrow and consuming are disjoint: no operation is both. -public export -borrowNotConsuming : IsBorrow op -> IsConsuming op -> Void -borrowNotConsuming BorrowShow x = case x of {} -borrowNotConsuming BorrowHide x = case x of {} -borrowNotConsuming BorrowMinimize x = case x of {} -borrowNotConsuming BorrowMaximize x = case x of {} -borrowNotConsuming BorrowRestore x = case x of {} -borrowNotConsuming BorrowRequestClose x = case x of {} - -||| A consuming operation always leads to Closed. -public export -consumingLeadsToClosed - : IsConsuming op - -> WindowTransition s op t - -> t = Closed -consumingLeadsToClosed ConsumingRun RunFromCreated = Refl -consumingLeadsToClosed ConsumingRun RunFromVisible = Refl -consumingLeadsToClosed ConsumingRun RunFromHidden = Refl -consumingLeadsToClosed ConsumingRun RunFromMinimized = Refl -consumingLeadsToClosed ConsumingRun RunFromMaximized = Refl -consumingLeadsToClosed ConsumingDestroy DestroyFromCreated = Refl -consumingLeadsToClosed ConsumingDestroy DestroyFromVisible = Refl -consumingLeadsToClosed ConsumingDestroy DestroyFromHidden = Refl -consumingLeadsToClosed ConsumingDestroy DestroyFromMinimized = Refl -consumingLeadsToClosed ConsumingDestroy DestroyFromMaximized = Refl - --------------------------------------------------------------------------------- --- GS1-INV-3: Reachability from Created --------------------------------------------------------------------------------- - -||| Proof that a state is reachable from Created via a (possibly empty) sequence -||| of transitions. Encoded as a path in the state machine. -public export -data ReachableFrom : (origin : WindowState) -> (dest : WindowState) -> Type where - ||| Every state is reachable from itself (zero steps). - RFRefl : ReachableFrom s s - ||| If dest is reachable from origin, and there is a valid transition from - ||| dest via some op to next, then next is reachable from origin. - RFStep : ReachableFrom origin dest - -> WindowTransition dest op next - -> ReachableFrom origin next - -||| All six window states are reachable from Created. -public export -visibleReachable : ReachableFrom Created Visible -visibleReachable = RFStep RFRefl ShowFromCreated - -public export -hiddenReachable : ReachableFrom Created Hidden -hiddenReachable = RFStep visibleReachable HideFromVisible - -public export -minimizedReachable : ReachableFrom Created Minimized -minimizedReachable = RFStep visibleReachable MinimizeFromVisible - -public export -maximizedReachable : ReachableFrom Created Maximized -maximizedReachable = RFStep visibleReachable MaximizeFromVisible - -public export -closedReachable : ReachableFrom Created Closed -closedReachable = RFStep RFRefl RunFromCreated - --------------------------------------------------------------------------------- --- GS1-INV-4: Window state is Active iff not Closed --------------------------------------------------------------------------------- - -||| Predicate: the window is "active" (not closed). -public export -data IsActive : WindowState -> Type where - ActiveCreated : IsActive Created - ActiveVisible : IsActive Visible - ActiveHidden : IsActive Hidden - ActiveMinimized : IsActive Minimized - ActiveMaximized : IsActive Maximized - -||| Closed windows are not active. -public export -closedNotActive : IsActive Closed -> Void -closedNotActive x = case x of {} - -||| Every non-Closed state is active. Takes a proof that `s` is not -||| `Closed` (the original `s = Closed -> Void -> IsActive s` signature -||| was ill-formed: `notClosed` had type `s = Closed`, so `notClosed Refl` -||| did not type-check; the intended contract is `Not (s = Closed)`). -public export -nonClosedIsActive : (s : WindowState) -> Not (s = Closed) -> IsActive s -nonClosedIsActive Created notClosed = ActiveCreated -nonClosedIsActive Visible notClosed = ActiveVisible -nonClosedIsActive Hidden notClosed = ActiveHidden -nonClosedIsActive Minimized notClosed = ActiveMinimized -nonClosedIsActive Maximized notClosed = ActiveMaximized -nonClosedIsActive Closed notClosed = absurd (notClosed Refl) - -||| A borrow transition preserves the Active property. -public export -borrowPreservesActive - : IsBorrow op - -> WindowTransition s op t - -> IsActive s - -> IsActive t -borrowPreservesActive BorrowShow ShowFromCreated _ = ActiveVisible -borrowPreservesActive BorrowShow ShowFromHidden _ = ActiveVisible -borrowPreservesActive BorrowHide HideFromVisible _ = ActiveHidden -borrowPreservesActive BorrowMinimize MinimizeFromVisible _ = ActiveMinimized -borrowPreservesActive BorrowMaximize MaximizeFromVisible _ = ActiveMaximized -borrowPreservesActive BorrowRestore RestoreFromMinimized _ = ActiveVisible -borrowPreservesActive BorrowRestore RestoreFromMaximized _ = ActiveVisible -borrowPreservesActive BorrowRequestClose RequestCloseVisible _ = ActiveVisible -borrowPreservesActive BorrowRequestClose RequestCloseHidden _ = ActiveHidden -borrowPreservesActive BorrowRequestClose RequestCloseMinimized _ = ActiveMinimized -borrowPreservesActive BorrowRequestClose RequestCloseMaximized _ = ActiveMaximized diff --git a/src/interface/Gossamer/ABI/WindowStateMachine.idr b/src/interface/Gossamer/ABI/WindowStateMachine.idr new file mode 120000 index 0000000..7c467d4 --- /dev/null +++ b/src/interface/Gossamer/ABI/WindowStateMachine.idr @@ -0,0 +1 @@ +../../abi/WindowStateMachine.idr \ No newline at end of file diff --git a/src/interface/abi/GrooveLinearity.idr b/src/interface/abi/GrooveLinearity.idr new file mode 100644 index 0000000..5f68c83 --- /dev/null +++ b/src/interface/abi/GrooveLinearity.idr @@ -0,0 +1,61 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Groove Handle Linearity (groove layer) +||| +||| The groove-handle specialisation of the shell's generic linear-handle +||| machinery (`Gossamer.ABI.HandleLinearity`). Relocated here so the shell +||| ABI stays groove-agnostic: the shell proves linearity for *any* handle +||| type via `LinearHandle`, and this module instantiates it for `GrooveHandle`. +||| +||| Proves that a groove connection handle cannot be duplicated, must be +||| consumed exactly once (disconnect), and follows the +||| Allocated -> Active -> Consumed lifecycle — the same guarantees the +||| webview/channel/capability handles enjoy in the shell. +||| +||| Zero believe_me. All proofs are constructive. + +module Gossamer.ABI.GrooveLinearity + +import Gossamer.ABI.Types +import Gossamer.ABI.HandleLinearity +import Gossamer.ABI.Groove +import Data.So +import Data.Bits + +%default total + +-------------------------------------------------------------------------------- +-- Groove Handle Validity +-------------------------------------------------------------------------------- + +||| Recover the (erased) non-null witness carried by a `GrooveHandle`'s +||| `MkGroove` constructor as a `ValidToken` for its raw pointer. The groove +||| analogue of `webviewValid`/`channelValid`/`capValid` in +||| `Gossamer.ABI.HandleLinearity`. +public export +grooveValid : (gh : GrooveHandle offers consumes) -> ValidToken (groovePtr gh) +grooveValid (MkGroove ptr {nonNull}) = MkValid {nonNull} + +-------------------------------------------------------------------------------- +-- Groove Handle Linearity +-------------------------------------------------------------------------------- + +||| A linearly-tracked groove handle. +||| Specialisation of `LinearHandle` for `GrooveHandle`. +public export +LinearGroove : (offers : CapSet) -> (consumes : CapSet) -> HandleState -> Type +LinearGroove offers consumes = LinearHandle (GrooveHandle offers consumes) + +||| Allocate a linear groove handle. +public export +allocateGroove : GrooveHandle offers consumes + -> LinearGroove offers consumes Allocated +allocateGroove gh = MkLinear gh (groovePtr gh) {valid = grooveValid gh} + +||| Disconnect a groove (consuming it). +||| The handle transitions from Active to Consumed. +public export +consumeForDisconnect : LinearGroove offers consumes Active + -> (GrooveHandle offers consumes, LinearGroove offers consumes Consumed) +consumeForDisconnect = consume diff --git a/src/interface/abi/HandleLinearity.idr b/src/interface/abi/HandleLinearity.idr index cc037a6..3f99d2d 100644 --- a/src/interface/abi/HandleLinearity.idr +++ b/src/interface/abi/HandleLinearity.idr @@ -3,13 +3,17 @@ -- ||| Handle Linearity Proofs for Gossamer ||| -||| Proves that connection handles (webview, channel, groove, capability) +||| Proves that connection handles (webview, channel, capability) ||| cannot be duplicated, must be consumed exactly once, and follow a ||| valid state machine lifecycle. ||| -||| Builds on the linear resource types in Types.idr and Groove.idr. -||| The existing WebviewHandle, Channel, GrooveHandle, and Cap types are -||| already parameterised with non-null proofs. This module adds: +||| Builds on the linear resource types in Types.idr. The existing +||| WebviewHandle, Channel, and Cap types are already parameterised with +||| non-null proofs. This module adds: +||| +||| The groove-handle specialisation (`LinearGroove`, `allocateGroove`, +||| `consumeForDisconnect`, `grooveValid`) lives in the groove layer +||| (`Gossamer.ABI.GrooveLinearity`) so the shell ABI stays groove-agnostic. ||| ||| 1. Uniqueness: a handle token cannot produce two live handles. ||| 2. Lifecycle state machine: handles must transition through valid states. @@ -21,7 +25,6 @@ module Gossamer.ABI.HandleLinearity import Gossamer.ABI.Types -import Gossamer.ABI.Groove import Data.So import Data.Bits @@ -54,18 +57,16 @@ checkValid token = ||| Recover the (erased) non-null witness carried by each handle's ||| constructor as a `ValidToken` for its raw token. The witness already -||| exists inside the handle — `MkWebview`/`MkGroove`/`MkChannel`/`MkCap` +||| exists inside the handle — `MkWebview`/`MkChannel`/`MkCap` ||| each require `So (ptr /= 0)` at construction — but the `*Ptr`/`capToken` ||| projections discard it. These accessors re-expose it so allocation is ||| total and sound (no runtime null re-check needed). +||| (`grooveValid` is the analogous accessor for `GrooveHandle`; it lives in +||| `Gossamer.ABI.GrooveLinearity` in the groove layer.) public export webviewValid : (wv : WebviewHandle) -> ValidToken (webviewPtr wv) webviewValid (MkWebview ptr {nonNull}) = MkValid {nonNull} -public export -grooveValid : (gh : GrooveHandle offers consumes) -> ValidToken (groovePtr gh) -grooveValid (MkGroove ptr {nonNull}) = MkValid {nonNull} - public export channelValid : (ch : Channel req resp) -> ValidToken (channelPtr ch) channelValid (MkChannel ptr {nonNull}) = MkValid {nonNull} @@ -225,28 +226,6 @@ public export consumeForDestroy : LinearWebview Active -> (WebviewHandle, LinearWebview Consumed) consumeForDestroy = consume --------------------------------------------------------------------------------- --- Groove Handle Linearity --------------------------------------------------------------------------------- - -||| A linearly-tracked groove handle. -||| Specialisation of LinearHandle for GrooveHandle. -public export -LinearGroove : (offers : CapSet) -> (consumes : CapSet) -> HandleState -> Type -LinearGroove offers consumes = LinearHandle (GrooveHandle offers consumes) - -||| Allocate a linear groove handle. -public export -allocateGroove : GrooveHandle offers consumes - -> LinearGroove offers consumes Allocated -allocateGroove gh = MkLinear gh (groovePtr gh) {valid = grooveValid gh} - -||| Disconnect a groove (consuming it). -public export -consumeForDisconnect : LinearGroove offers consumes Active - -> (GrooveHandle offers consumes, LinearGroove offers consumes Consumed) -consumeForDisconnect = consume - -------------------------------------------------------------------------------- -- Channel Handle Linearity -------------------------------------------------------------------------------- diff --git a/src/interface/abi/IPCDispatch.idr b/src/interface/abi/IPCDispatch.idr index d093eae..0ff5532 100644 --- a/src/interface/abi/IPCDispatch.idr +++ b/src/interface/abi/IPCDispatch.idr @@ -30,7 +30,6 @@ module Gossamer.ABI.IPCDispatch import Gossamer.ABI.Types -import Gossamer.ABI.Groove %default total diff --git a/src/interface/abi/ResourceCleanup.idr b/src/interface/abi/ResourceCleanup.idr index d435cfc..3c537e8 100644 --- a/src/interface/abi/ResourceCleanup.idr +++ b/src/interface/abi/ResourceCleanup.idr @@ -21,7 +21,6 @@ module Gossamer.ABI.ResourceCleanup import Gossamer.ABI.Types import Gossamer.ABI.HandleLinearity import Gossamer.ABI.PanelIsolation -import Gossamer.ABI.Groove import Data.So import Data.Bits import Data.Nat