|
| 1 | +// SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | +// |
| 4 | +//! Gossamer Groove endpoint for ECHIDNA. |
| 5 | +//! |
| 6 | +//! Exposes ECHIDNA's formal proof verification capabilities via the Groove |
| 7 | +//! discovery protocol. Any groove-aware system (Gossamer, PanLL, Hypatia, |
| 8 | +//! etc.) can discover ECHIDNA by probing `GET /.well-known/groove` on port |
| 9 | +//! 9000. |
| 10 | +//! |
| 11 | +//! ECHIDNA is a neurosymbolic theorem proving platform supporting 48 prover |
| 12 | +//! backends with a comprehensive verification pipeline, LLM integration, |
| 13 | +//! dodeca-API, and Prover Wars. |
| 14 | +//! |
| 15 | +//! The groove connector types are formally verified in Gossamer's Groove.idr: |
| 16 | +//! - `IsSubset` proves consumers can only connect if ECHIDNA satisfies their |
| 17 | +//! needs |
| 18 | +//! - `GrooveHandle` is linear: consumers MUST disconnect (no dangling grooves) |
| 19 | +//! |
| 20 | +//! ## Groove Protocol |
| 21 | +//! |
| 22 | +//! - `GET /.well-known/groove` — Capability manifest (JSON) |
| 23 | +//! - `GET /health` — Simple health check |
| 24 | +//! |
| 25 | +//! ## Capabilities Offered |
| 26 | +//! |
| 27 | +//! - `proof-verification` — Formal proof verification engine with LLM |
| 28 | +//! integration, dodeca-API, and Prover Wars |
| 29 | +//! |
| 30 | +//! ## Capabilities Consumed (enhanced when available) |
| 31 | +//! |
| 32 | +//! - `octad-storage` (from VeriSimDB) — Persist proof artifacts as octad |
| 33 | +//! entities |
| 34 | +
|
| 35 | +use axum::{routing::get, Json, Router}; |
| 36 | +use serde_json::json; |
| 37 | + |
| 38 | +/// Default port for the ECHIDNA groove endpoint. |
| 39 | +pub const GROOVE_PORT: u16 = 9000; |
| 40 | + |
| 41 | +/// Build the groove manifest JSON for ECHIDNA. |
| 42 | +/// |
| 43 | +/// Returns a `serde_json::Value` containing the standard Groove capability |
| 44 | +/// manifest. The manifest advertises ECHIDNA's `proof-verification` |
| 45 | +/// capability and declares that it can consume `octad-storage` from |
| 46 | +/// VeriSimDB when available. |
| 47 | +fn manifest() -> serde_json::Value { |
| 48 | + json!({ |
| 49 | + "groove_version": "1", |
| 50 | + "service_id": "echidna", |
| 51 | + "service_version": env!("CARGO_PKG_VERSION"), |
| 52 | + "capabilities": { |
| 53 | + "proof_verification": { |
| 54 | + "type": "proof-verification", |
| 55 | + "description": "Formal proof verification engine with LLM integration, dodeca-API, and Prover Wars", |
| 56 | + "protocol": "http", |
| 57 | + "endpoint": "/api/v1/prove", |
| 58 | + "requires_auth": false, |
| 59 | + "panel_compatible": true |
| 60 | + } |
| 61 | + }, |
| 62 | + "consumes": ["octad-storage"], |
| 63 | + "endpoints": { |
| 64 | + "api": format!("http://localhost:{}/api", GROOVE_PORT), |
| 65 | + "health": format!("http://localhost:{}/health", GROOVE_PORT) |
| 66 | + }, |
| 67 | + "health": "/health", |
| 68 | + "applicability": ["individual", "team"] |
| 69 | + }) |
| 70 | +} |
| 71 | + |
| 72 | +/// Axum handler for `GET /.well-known/groove`. |
| 73 | +/// |
| 74 | +/// Returns the Groove capability manifest as JSON so that groove-aware |
| 75 | +/// systems (Gossamer, PanLL, Hypatia, etc.) can discover ECHIDNA via |
| 76 | +/// standard port probing. |
| 77 | +async fn groove_manifest() -> Json<serde_json::Value> { |
| 78 | + Json(manifest()) |
| 79 | +} |
| 80 | + |
| 81 | +/// Axum handler for `GET /health`. |
| 82 | +/// |
| 83 | +/// Returns a minimal JSON health check response. Groove consumers use |
| 84 | +/// this to verify the service is responsive before attempting capability |
| 85 | +/// negotiation. |
| 86 | +async fn health_check() -> Json<serde_json::Value> { |
| 87 | + Json(json!({ |
| 88 | + "status": "ok", |
| 89 | + "service": "echidna", |
| 90 | + "version": env!("CARGO_PKG_VERSION") |
| 91 | + })) |
| 92 | +} |
| 93 | + |
| 94 | +/// Build an axum `Router` containing the groove discovery endpoints. |
| 95 | +/// |
| 96 | +/// The router exposes two routes: |
| 97 | +/// - `GET /.well-known/groove` — Capability manifest |
| 98 | +/// - `GET /health` — Health check |
| 99 | +/// |
| 100 | +/// Callers can merge this router into a larger application or serve it |
| 101 | +/// standalone via [`run`]. |
| 102 | +pub fn router() -> Router { |
| 103 | + Router::new() |
| 104 | + .route("/.well-known/groove", get(groove_manifest)) |
| 105 | + .route("/health", get(health_check)) |
| 106 | +} |
| 107 | + |
| 108 | +/// Run the standalone groove discovery server on `GROOVE_PORT`. |
| 109 | +/// |
| 110 | +/// Binds to `127.0.0.1:9000` and serves the groove manifest and health |
| 111 | +/// check endpoints. This function blocks until the server is shut down. |
| 112 | +/// |
| 113 | +/// # Errors |
| 114 | +/// |
| 115 | +/// Returns an error if the TCP listener cannot bind to the port (e.g. |
| 116 | +/// the port is already in use). |
| 117 | +pub async fn run() -> anyhow::Result<()> { |
| 118 | + run_on_port(GROOVE_PORT).await |
| 119 | +} |
| 120 | + |
| 121 | +/// Run the groove discovery server on a caller-specified port. |
| 122 | +/// |
| 123 | +/// This variant is useful for tests or when the default port is |
| 124 | +/// unavailable. |
| 125 | +/// |
| 126 | +/// # Errors |
| 127 | +/// |
| 128 | +/// Returns an error if the TCP listener cannot bind to the given port. |
| 129 | +pub async fn run_on_port(port: u16) -> anyhow::Result<()> { |
| 130 | + let addr = format!("127.0.0.1:{}", port); |
| 131 | + tracing::info!("[groove] echidna groove endpoint listening on {}", addr); |
| 132 | + tracing::info!( |
| 133 | + "[groove] Probe: curl http://localhost:{}/.well-known/groove", |
| 134 | + port |
| 135 | + ); |
| 136 | + |
| 137 | + let listener = tokio::net::TcpListener::bind(&addr).await?; |
| 138 | + axum::serve(listener, router()).await?; |
| 139 | + |
| 140 | + Ok(()) |
| 141 | +} |
| 142 | + |
| 143 | +#[cfg(test)] |
| 144 | +mod tests { |
| 145 | + use super::*; |
| 146 | + |
| 147 | + /// The manifest must contain the required top-level fields. |
| 148 | + #[test] |
| 149 | + fn manifest_has_required_fields() { |
| 150 | + let m = manifest(); |
| 151 | + assert_eq!(m["groove_version"], "1"); |
| 152 | + assert_eq!(m["service_id"], "echidna"); |
| 153 | + assert!(m["service_version"].is_string()); |
| 154 | + assert!(m["capabilities"]["proof_verification"].is_object()); |
| 155 | + assert_eq!( |
| 156 | + m["capabilities"]["proof_verification"]["type"], |
| 157 | + "proof-verification" |
| 158 | + ); |
| 159 | + assert!(m["consumes"].is_array()); |
| 160 | + assert_eq!(m["consumes"][0], "octad-storage"); |
| 161 | + assert_eq!(m["health"], "/health"); |
| 162 | + } |
| 163 | + |
| 164 | + /// The GROOVE_PORT constant must match the assigned echidna port. |
| 165 | + #[test] |
| 166 | + fn groove_port_is_9000() { |
| 167 | + assert_eq!(GROOVE_PORT, 9000); |
| 168 | + } |
| 169 | +} |
0 commit comments