docs: add service integration guide and middleware setup documentation

https://claude.ai/code/session_01YWxGS8PyEvMTrrG1yBcN3r

Author: claude

docs/guides/MIDDLEWARE-SETUP.adoc

@@ -0,0 +1,166 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+= PanLL Middleware Setup Guide
+:toc: macro
+:icons: font
+:source-highlighter: rouge
+
+toc::[]
+
+== Overview
+
+PanLL supports three optional middleware layers that extend its core Gossamer backend
+with additional runtime capabilities: Elixir/BEAM for fault-tolerant service supervision,
+Julia for numeric analysis and batch processing, and Idris2 for high-assurance interface
+verification. All three are optional — PanLL runs without them — but each unlocks specific
+capabilities for production or research use.
+
+== Elixir/BEAM Middleware
+
+=== Purpose
+
+The Elixir/BEAM middleware layer provides OTP supervision trees for resilient panel
+connections and service lifecycle management. It wraps the external service bridges
+(VeriSimDB, BoJ, ECHIDNA, TypeLL, Hypatia) under a supervisor hierarchy, enabling
+automatic process restart, health reporting, and fault isolation without coupling those
+concerns to the Gossamer Rust core.
+
+=== Location
+
+----
+beam/panll_beam
+----
+
+=== Setup
+
+[source,bash]
+----
+cd beam/panll_beam
+mix deps.get && mix compile
+----
+
+=== API Modes
+
+The BEAM middleware exposes three API surfaces, each toggled via the `PANLL_BEAM_APIS`
+environment variable:
+
+HTTP (Bandit/Plug)::
+  Standard HTTP endpoints served by Bandit with Plug routing. Suitable for REST-style
+  integration with the Gossamer backend or external tooling.
+
+GraphQL (Absinthe)::
+  A GraphQL schema over the panel supervision state and service health data, served
+  via Absinthe and Absinthe.Plug. Useful for Observatory panel queries and dashboards.
+
+gRPC::
+  Protocol Buffers over gRPC (via the `grpc` and `protobuf` Mix dependencies).
+  Preferred for low-latency, typed communication between the BEAM layer and
+  latency-sensitive service bridges.
+
+=== Configuration
+
+Set the `PANLL_BEAM_APIS` environment variable to a comma-separated list of the API
+modes to enable before starting the application:
+
+[source,bash]
+----
+# Enable all three API surfaces
+export PANLL_BEAM_APIS=http,graphql,grpc
+mix run --no-halt
+
+# Enable HTTP only
+export PANLL_BEAM_APIS=http
+mix run --no-halt
+----
+
+=== When to Use
+
+Use the Elixir/BEAM middleware in production deployments where fault-tolerant service
+supervision is required. The OTP supervisor model gives you per-service restart strategies,
+cascading failure isolation, and live introspection without modifying the Gossamer core.
+It is not needed for local development where all services are started manually.
+
+== Julia Middleware
+
+=== Purpose
+
+The Julia middleware layer handles numeric analysis, calibration, and batch processing
+tasks that are impractical in the Rust/ReScript stack. This includes metrics computation
+(e.g., proof complexity statistics, type-check latency distributions), statistical
+hypothesis testing over telemetry data, and data pipeline processing for research
+workflows built on PanLL's proof-carrying data.
+
+=== Location
+
+Julia scripts live alongside the analysis pipelines they serve. Batch scripts are
+colocated with the data or reporting stage that consumes them. There is no single
+top-level Julia package directory — each analysis pipeline carries its own
+`Project.toml` and `Manifest.toml`.
+
+=== Setup
+
+From the directory containing the relevant `Project.toml`:
+
+[source,bash]
+----
+julia --project=. -e 'using Pkg; Pkg.instantiate()'
+----
+
+This resolves and precompiles all declared dependencies for that pipeline's environment.
+
+=== When to Use
+
+Use Julia middleware when:
+
+* Computing aggregate metrics or statistical summaries over proof session telemetry.
+* Running statistical tests to validate performance regressions or calibration changes.
+* Processing data pipelines that feed into research publications or compliance reports
+  derived from PanLL's observability output.
+* Performing calibration passes over numeric parameters used by ECHIDNA or TypeLL.
+
+Julia is not involved in the real-time request path. All Julia processing is offline
+or batch-scheduled.
+
+== Idris2 ABI Middleware
+
+=== Purpose
+
+The Idris2 ABI middleware layer provides high-assurance interface verification for
+critical IPC boundaries. Where the circuit breaker pattern and graceful degradation
+principles give _operational_ resilience, the Idris2 layer gives _formal_ guarantees:
+machine-checked proofs that serialization and deserialization of IPC messages correctly
+implement the agreed contract at every trust boundary.
+
+=== Status
+
+[IMPORTANT]
+====
+This layer is *planned* and has not yet been implemented. The design below describes
+the intended architecture.
+====
+
+=== Goal
+
+Formally verify the IPC message serialization and deserialization contracts used by the
+Gossamer command layer. Each `invoke` command crossing the webview/backend boundary has
+a defined schema; the Idris2 ABI layer will generate or check proofs that:
+
+* Every serialized message can be round-tripped without loss of information.
+* Every deserializer rejects out-of-contract inputs with a typed error rather than
+  silently producing a wrong value.
+* Schema evolution (adding fields, deprecating variants) preserves backward compatibility
+  at the ABI level.
+
+=== When to Use
+
+Use the Idris2 ABI layer at critical trust boundaries where "probably correct" is not
+a sufficient assurance level. Typical candidates include:
+
+* The serialization boundary between the ReScript frontend and the Gossamer Rust backend
+  for commands that carry proof certificates or VCL query results.
+* Any message type used to authorize a destructive operation (e.g., workspace deletion,
+  cartridge unload).
+* Integration points with external theorem provers where a malformed message could
+  corrupt proof state.
+
+Until the Idris2 layer is implemented, these boundaries rely on property-based tests
+and the existing contract suite in `contracts/`.

docs/guides/SERVICE-INTEGRATION.adoc

@@ -0,0 +1,178 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
+= PanLL Service Integration Guide
+:author: Jonathan D.A. Jewell
+:toc: macro
+:icons: font
+:source-highlighter: rouge
+
+toc::[]
+
+== Overview
+
+PanLL connects to multiple backend services to deliver its neurosymbolic development
+environment. These services handle proof storage, cartridge dispatch, type checking,
+theorem proving, and static analysis. Each service runs as an independent process,
+typically on localhost, and is accessed by the Gossamer IPC command layer in
+`src-gossamer/`.
+
+Because any service may be unavailable — due to a crash, a slow startup, a network
+partition, or deliberate teardown during development — every service bridge must
+implement a defined failure mode rather than blocking the UI or propagating an
+unhandled error to the user.
+
+== Service Inventory
+
+[cols="1,1,2,2", options="header"]
+|===
+| Service | Port | Purpose | Failure Mode
+
+| VeriSimDB
+| 8080
+| 8-modality versioned database for proof-carrying data; stores octads, VCL queries,
+  and proof certificates.
+| Fall back to `localStorage` cache. Serve last-known-good octad snapshots until the
+  service reconnects.
+
+| BoJ
+| 7700
+| Cartridge server and protocol gateway; loads and invokes `.boj` cartridge modules,
+  exposes health and topology endpoints.
+| Queue outgoing commands in memory. Replay the queue on reconnect. Surface a
+  degraded-mode banner in the Observatory panel.
+
+| ECHIDNA
+| 9000
+| Theorem prover dispatch; selects tactics, manages the prover pool, and returns
+  proof results and tactic recommendations.
+| Degrade to cached proofs stored in `localStorage`. Mark obligations as
+  "proof pending — ECHIDNA offline" rather than failing the session.
+
+| TypeLL
+| 7800
+| Type verification kernel; checks expressions against PanLL's dependent type
+  system, evaluates type-level computations.
+| Skip active type checks and warn the user with a visible indicator. Re-queue
+  pending checks when the service comes back online.
+
+| Hypatia
+| (dynamic)
+| Static analysis; performs code quality analysis, linting, and pattern detection
+  across the active workspace.
+| Degrade gracefully. Continue showing the last successfully computed analysis
+  results, marked as stale, until a fresh run completes.
+|===
+
+== Circuit Breaker Pattern
+
+Each service bridge in `src-gossamer/` should implement the standard three-state
+circuit breaker pattern to prevent cascading failures and eliminate repeated
+wait-for-timeout overhead when a backend is down.
+
+=== States
+
+Closed (normal operation)::
+  Requests pass through to the service. Failure count is tracked. If the failure
+  rate exceeds a threshold within a rolling window, the breaker trips to *Open*.
+
+Open (service assumed failed)::
+  All calls to this service are rejected immediately without attempting a network
+  round-trip. A deadline timer is started. The panel receives the degraded-mode
+  fallback response without blocking. When the timer expires, the breaker moves
+  to *Half-Open*.
+
+Half-Open (probing for recovery)::
+  A single probe request is sent to the service. If it succeeds, the breaker
+  resets to *Closed* and normal operation resumes. If it fails, the breaker
+  returns to *Open* and resets the timer.
+
+=== Implementation Guidance
+
+All live service modules (`boj_live.rs`, `verisim_live.rs`, `echidna_live.rs`, and
+any future service bridges) should wrap their `ServiceEndpoint` calls with a
+shared circuit breaker guard. The shared HTTP client in `src-gossamer/src/http_client.rs`
+provides the low-level timeout infrastructure; the circuit breaker layer sits above
+it and consults the breaker state before handing a request to `http_client::get_json`
+or `http_client::post_json`.
+
+State for each breaker (failure count, state enum, next-probe timestamp) should be
+held in an `Arc<Mutex<BreakerState>>` registered in the Gossamer application context
+at startup, so that all panels share a consistent view of each service's health.
+
+== Graceful Degradation Principles
+
+The following principles apply to all service integrations in PanLL:
+
+* *Never block the UI on a service call.* All service requests must be asynchronous.
+  The Gossamer command layer runs these on a Tokio runtime; commands must return
+  immediately with a pending/cached response if the service is unavailable.
+
+* *Always show last-known-good state.* Panels must cache the most recent successful
+  response for each service query and display it when the live call fails or is
+  short-circuited by an open breaker. Stale results must be visually marked.
+
+* *Surface service health in the Observatory panel.* The Observatory panel
+  (`PanelObservatory`, clade `observatory`) is the designated home for cross-panel
+  health and resource status. Each service bridge should emit health events that
+  the Observatory can display, including the current breaker state.
+
+* *Log failures to the BoJ latency log for observability.* Service call failures,
+  breaker state transitions, and degraded-mode activations must be recorded via
+  the observability subsystem so that developers can diagnose intermittent issues
+  after the fact.
+
+== Example: Gossamer Command Handler with Service Failure Handling
+
+The following pseudocode (Rust-like syntax) illustrates how a Gossamer command
+handler should interact with a service bridge that has a circuit breaker.
+
+[source,rust]
+----
+// In src-gossamer/src/verisim_live.rs (or a wrapper command module):
+
+pub async fn cmd_get_octad_summary(params: Value) -> String {
+    let id = params["id"].as_str().unwrap_or("");
+
+    // 1. Check circuit breaker state.
+    let breaker = VERISIMDB_BREAKER.lock().unwrap();
+    if breaker.is_open() {
+        // Fast-reject: return cached result without touching the network.
+        log_service_event("verisimdb", "circuit_open", "fast-reject");
+        return cached_octad_summary(id)
+            .map(|v| mark_stale(v))
+            .unwrap_or_else(|| json!({"error": "VeriSimDB unavailable", "stale": true}).to_string());
+    }
+    drop(breaker);
+
+    // 2. Attempt the live call.
+    match verisim_live_get_octad(id).await {
+        Ok(summary) => {
+            // Success: reset failure count, store in cache.
+            VERISIMDB_BREAKER.lock().unwrap().record_success();
+            store_cached_octad_summary(id, &summary);
+            summary
+        }
+        Err(e) => {
+            // Failure: record it; breaker may trip to Open.
+            let tripped = VERISIMDB_BREAKER.lock().unwrap().record_failure();
+            log_service_event("verisimdb", "call_failed", &e);
+            if tripped {
+                log_service_event("verisimdb", "circuit_tripped", "now open");
+            }
+            // Fall back to cache.
+            cached_octad_summary(id)
+                .map(|v| mark_stale(v))
+                .unwrap_or_else(|| json!({"error": e, "stale": true}).to_string())
+        }
+    }
+}
+----
+
+Key points:
+
+* The breaker guard is checked *before* any I/O.
+* The fallback path never panics or returns an empty string — it always gives the
+  panel something renderable.
+* Failures are logged before returning the fallback, ensuring the BoJ latency log
+  and Observatory panel receive the signal.
+* The cache write happens on the success path, keeping last-known-good state fresh.