diff --git a/Cargo.lock b/Cargo.lock index 211c7e2..99c4e63 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -530,18 +530,18 @@ dependencies = [ [[package]] name = "capnp" -version = "0.20.6" +version = "0.25.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "053b81915c2ce1629b8fb964f578b18cb39b23ef9d5b24120d0dfc959569a1d9" +checksum = "63da65e5e9ffc3b8f993d4ad222a548152549351a643f6b850a7773cb6ff2809" dependencies = [ "embedded-io", ] [[package]] name = "capnpc" -version = "0.20.1" +version = "0.25.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1aa3d5f01e69ed11656d2c7c47bf34327ea9bfb5c85c7de787fcd7b6c5e45b61" +checksum = "fca02be865c8c5a78bfc24b9819006ab6b59bef238467203928e26459557af93" dependencies = [ "capnp", ] @@ -989,6 +989,12 @@ dependencies = [ "syn", ] +[[package]] +name = "dyn-clone" +version = "1.0.20" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d0881ea181b1df73ff77ffaaf9c7544ecc11e82fba9b5f27b262a3c73a332555" + [[package]] name = "echidna" version = "2.1.0" @@ -1070,6 +1076,20 @@ dependencies = [ "uuid", ] +[[package]] +name = "echidna-mcp" +version = "0.1.0" +dependencies = [ + "anyhow", + "rmcp", + "schemars", + "serde", + "serde_json", + "tokio", + "tracing", + "tracing-subscriber", +] + [[package]] name = "echidna-rest" version = "0.1.0" @@ -1108,9 +1128,9 @@ checksum = "48c757948c5ede0e46177b7add2e67155f70e33c07fea8284df6576da70b3719" [[package]] name = "embedded-io" -version = "0.6.1" +version = "0.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "edd0f118536f44f5ccd48bcb8b111bdc3de888b58c74639dfb034a357d0f206d" +checksum = "9eb1aa714776b75c7e67e1da744b81a129b3ff919c8712b5e1b32252c1f07cc7" [[package]] name = "encode_unicode" @@ -2177,6 +2197,12 @@ dependencies = [ "windows-link", ] +[[package]] +name = "pastey" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b867cad97c0791bbd3aaa6472142568c6c9e8f71937e98379f584cfb0cf35bec" + [[package]] name = "percent-encoding" version = "2.3.2" @@ -2632,6 +2658,26 @@ dependencies = [ "bitflags", ] +[[package]] +name = "ref-cast" +version = "1.0.25" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f354300ae66f76f1c85c5f84693f0ce81d747e2c3f21a45fef496d89c960bf7d" +dependencies = [ + "ref-cast-impl", +] + +[[package]] +name = "ref-cast-impl" +version = "1.0.25" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b7186006dcb21920990093f30e3dea63b7d6e977bf1256be20c3563a5db070da" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "regex" version = "1.12.3" @@ -2719,6 +2765,41 @@ dependencies = [ "windows-sys 0.52.0", ] +[[package]] +name = "rmcp" +version = "1.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "67d69668de0b0ccd9cc435f700f3b39a7861863cf37a15e1f304ea78688a4826" +dependencies = [ + "async-trait", + "base64", + "chrono", + "futures", + "pastey", + "pin-project-lite", + "rmcp-macros", + "schemars", + "serde", + "serde_json", + "thiserror", + "tokio", + "tokio-util", + "tracing", +] + +[[package]] +name = "rmcp-macros" +version = "1.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "48fdc01c81097b0aed18633e676e269fefa3a78ec1df56b4fe597c1241b92025" +dependencies = [ + "darling 0.23.0", + "proc-macro2", + "quote", + "serde_json", + "syn", +] + [[package]] name = "rust-embed" version = "8.11.0" @@ -2881,6 +2962,32 @@ dependencies = [ "windows-sys 0.61.2", ] +[[package]] +name = "schemars" +version = "1.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a2b42f36aa1cd011945615b92222f6bf73c599a102a300334cd7f8dbeec726cc" +dependencies = [ + "chrono", + "dyn-clone", + "ref-cast", + "schemars_derive", + "serde", + "serde_json", +] + +[[package]] +name = "schemars_derive" +version = "1.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7d115b50f4aaeea07e79c1912f645c7513d81715d0420f8bc77a18c6260b307f" +dependencies = [ + "proc-macro2", + "quote", + "serde_derive_internals", + "syn", +] + [[package]] name = "scopeguard" version = "1.2.0" @@ -2946,6 +3053,17 @@ dependencies = [ "syn", ] +[[package]] +name = "serde_derive_internals" +version = "0.29.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "18d26a20a969b9e3fdf2fc2d9f21eda6c40e2de84c9408bb5d3b05d499aae711" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "serde_json" version = "1.0.149" diff --git a/Cargo.toml b/Cargo.toml index f110bf1..f1a5182 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -112,6 +112,7 @@ harness = false [workspace] members = [ + "crates/echidna-mcp", "crates/echidna-wire", "crates/typed_wasm", "src/interfaces/graphql", diff --git a/crates/echidna-mcp/Cargo.toml b/crates/echidna-mcp/Cargo.toml new file mode 100644 index 0000000..0d666b7 --- /dev/null +++ b/crates/echidna-mcp/Cargo.toml @@ -0,0 +1,24 @@ +# SPDX-License-Identifier: PMPL-1.0-or-later + +[package] +name = "echidna-mcp" +version = "0.1.0" +edition = "2021" +authors = ["Jonathan D.A. Jewell "] +license = "PMPL-1.0-or-later" +description = "Model Context Protocol server exposing ECHIDNA to AI coding agents (Claude Code, Claude API, etc.)" +repository = "https://github.com/hyperpolymath/echidna" + +[[bin]] +name = "echidna-mcp" +path = "src/main.rs" + +[dependencies] +rmcp = { version = "1", features = ["server", "macros", "transport-io"] } +serde = { version = "1", features = ["derive"] } +serde_json = "1" +schemars = "1" +tokio = { version = "1", features = ["rt-multi-thread", "macros", "process", "io-util"] } +anyhow = "1" +tracing = "0.1" +tracing-subscriber = { version = "0.3", features = ["env-filter"] } diff --git a/crates/echidna-mcp/src/main.rs b/crates/echidna-mcp/src/main.rs new file mode 100644 index 0000000..01541a1 --- /dev/null +++ b/crates/echidna-mcp/src/main.rs @@ -0,0 +1,194 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later + +//! ECHIDNA MCP Server — exposes the `echidna` CLI as Model Context Protocol +//! tools so Claude Code / Claude API agents can call on the 105-prover +//! portfolio as first-class tool-use actions. +//! +//! # Running +//! +//! ```sh +//! echidna-mcp # serves on stdio (default MCP transport) +//! ECHIDNA_BIN=/abs/path/echidna echidna-mcp +//! ``` +//! +//! # Claude Code integration +//! +//! Add to `.claude/settings.json`: +//! +//! ```json +//! { "mcpServers": { "echidna": { "command": "echidna-mcp" } } } +//! ``` + +use rmcp::{ + handler::server::{router::tool::ToolRouter, wrapper::Parameters}, + model::{ServerCapabilities, ServerInfo}, + schemars::JsonSchema, + tool, tool_handler, tool_router, + transport::stdio, + ServerHandler, ServiceExt, +}; +use serde::{Deserialize, Serialize}; +use tokio::process::Command; + +fn echidna_bin() -> String { + std::env::var("ECHIDNA_BIN").unwrap_or_else(|_| "echidna".to_string()) +} + +#[derive(Debug, Deserialize, Serialize, JsonSchema)] +struct ProveParams { + /// Absolute path to the proof file. Accepted formats depend on the + /// chosen prover: SMT-LIB `.smt2` for Z3/CVC5/etc., Lean `.lean` for + /// Lean 4, Coq `.v` for Coq/Rocq, Agda `.agda`, Isabelle `.thy`, + /// Mizar `.miz`, F* `.fst`, SPASS DFG `.dfg`, Metamath `.mm`, etc. + pub file: String, + + /// Prover backend name (case-sensitive). Common values: `Z3`, `Lean`, + /// `Coq`, `Agda`, `Isabelle`, `Mizar`, `FStar`, `SPASS`, `Vampire`, + /// `CVC5`, `Metamath`. If omitted, ECHIDNA auto-detects from the file + /// extension. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub prover: Option, + + /// Timeout in seconds for the prover invocation. Default 300. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub timeout_secs: Option, +} + +#[derive(Debug, Serialize)] +struct ProveResult { + verified: bool, + message: String, + prover: Option, + raw_output: String, + stderr: String, +} + +#[derive(Clone)] +struct EchidnaMcp { + tool_router: ToolRouter, +} + +impl EchidnaMcp { + pub fn new() -> Self { + Self { + tool_router: Self::tool_router(), + } + } +} + +#[tool_router(router = tool_router)] +impl EchidnaMcp { + /// Prove a theorem using one of ECHIDNA's 105 prover backends. + #[tool( + name = "prove", + description = "Prove a theorem from a file using ECHIDNA's 105-prover \ + portfolio. Returns a JSON object with {verified, message, \ + prover, raw_output, stderr}. Common provers: Z3, Lean, Coq, \ + Agda, Isabelle, Mizar, FStar, SPASS, Metamath." + )] + pub async fn prove(&self, params: Parameters) -> String { + let ProveParams { + file, + prover, + timeout_secs, + } = params.0; + + let mut cmd = Command::new(echidna_bin()); + cmd.arg("prove").arg(&file).arg("--format").arg("json"); + if let Some(p) = prover.as_deref() { + cmd.arg("-p").arg(p); + } + let timeout = timeout_secs.unwrap_or(300); + cmd.arg("-t").arg(timeout.to_string()); + + let output = match cmd.output().await { + Ok(o) => o, + Err(e) => { + let result = ProveResult { + verified: false, + message: format!("Failed to invoke echidna: {e}"), + prover, + raw_output: String::new(), + stderr: String::new(), + }; + return serde_json::to_string_pretty(&result).unwrap_or_default(); + } + }; + + let stdout = String::from_utf8_lossy(&output.stdout).into_owned(); + let stderr = String::from_utf8_lossy(&output.stderr).into_owned(); + + let verified = stdout.contains("\"level\": \"success\"") + || stdout.contains("\"level\":\"success\""); + let message = extract_first_message(&stdout).unwrap_or_else(|| { + if stderr.is_empty() { + "(no output)".to_string() + } else { + stderr.lines().take(5).collect::>().join("\n") + } + }); + + let result = ProveResult { + verified, + message, + prover, + raw_output: stdout, + stderr, + }; + serde_json::to_string_pretty(&result).unwrap_or_default() + } +} + +#[tool_handler(router = self.tool_router)] +impl ServerHandler for EchidnaMcp { + fn get_info(&self) -> ServerInfo { + let mut info = ServerInfo::default(); + info.capabilities = ServerCapabilities::builder().enable_tools().build(); + info.instructions = Some( + "ECHIDNA MCP server. Call `prove` with a proof-file path and \ + (optionally) a prover name to run a theorem prover from \ + ECHIDNA's 105-backend portfolio." + .into(), + ); + info + } +} + +/// Parse the first `"message": "..."` value out of ECHIDNA's stdout. +fn extract_first_message(stdout: &str) -> Option { + let needle = "\"message\""; + let start = stdout.find(needle)?; + let rest = &stdout[start + needle.len()..]; + let colon = rest.find(':')?; + let after_colon = &rest[colon + 1..]; + let q1 = after_colon.find('"')?; + let after_q1 = &after_colon[q1 + 1..]; + let bytes = after_q1.as_bytes(); + let mut end = 0; + while end < bytes.len() { + if bytes[end] == b'\\' && end + 1 < bytes.len() { + end += 2; + continue; + } + if bytes[end] == b'"' { + break; + } + end += 1; + } + Some(after_q1[..end].to_string()) +} + +#[tokio::main] +async fn main() -> anyhow::Result<()> { + tracing_subscriber::fmt() + .with_env_filter( + tracing_subscriber::EnvFilter::try_from_default_env() + .unwrap_or_else(|_| tracing_subscriber::EnvFilter::new("echidna_mcp=info")), + ) + .with_writer(std::io::stderr) + .init(); + + let service = EchidnaMcp::new().serve(stdio()).await?; + service.waiting().await?; + Ok(()) +} diff --git a/crates/echidna-wire/Cargo.toml b/crates/echidna-wire/Cargo.toml index bcfb8e3..8d49a9f 100644 --- a/crates/echidna-wire/Cargo.toml +++ b/crates/echidna-wire/Cargo.toml @@ -11,7 +11,7 @@ repository = "https://github.com/hyperpolymath/echidna" build = "build.rs" [dependencies] -capnp = "0.20" +capnp = "0.25" [build-dependencies] -capnpc = "0.20" +capnpc = "0.25" diff --git a/docs/handover/TODO.md b/docs/handover/TODO.md index 50e4f94..b28cde4 100644 --- a/docs/handover/TODO.md +++ b/docs/handover/TODO.md @@ -40,6 +40,16 @@ Handover hints live in `.machine_readable/6a2/STATE.a2ml [wave-3-handover-hints] Mizar, Nuprl, PVS, Minlog, Dedukti, Arend, KeY, Prism, UPPAAL, ViPER, NuSMV, Spin, TLC, CBMC, Seahorn, dReal, Boogie, Kissat, Alloy. Retain as mock-only unless a maintainer volunteers a Containerfile. Document why each stays mock in a per-backend one-liner. +### Wave-5 (new backend targets, no adapter yet) + +Backends not yet scaffolded in `src/rust/provers/`; ProverKind enum, factory dispatch, `kind_to_u8` discriminant, Idris2 injectivity proof, FFI table all need entries before any CI work. Tracked here so they are not forgotten: + +| Backend | Scaffold plan | Accessibility | +|---------|---------------|---------------| +| Andromeda | New `provers/andromeda.rs` adapter shelling out to `andromeda` CLI; OCaml source build required | Open-source (MIT), build from source | +| Theorema | Deferred — requires Mathematica licence (commercial) | Access-blocked in OSS CI; revisit if a maintainer has a licence | +| Globular | Not a CLI prover (web UI for higher category theory) — skipped unless scoped to graphical proof capture | N/A | + ### L3 hygiene - **Dafny deep-wiring upgrade** — `src/rust/provers/dafny.rs` is 165 LoC; live version-check passes but subprocess wrapper is stub-ish. Upgrade during L3 so live test measures real wiring, not a broken wrapper.