Claude/echidna mcp

.containerization/Containerfile.mcp

@@ -0,0 +1,149 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# ECHIDNA MCP Container — exposes ECHIDNA as a Model Context Protocol server
+# over stdio so any MCP-capable AI agent (Claude Code, Claude Desktop, Claude
+# API with tool use, other clients) can call `prove({file, prover, timeout_secs})`
+# and get a real solver verdict.
+#
+# Bundled MVP prover set: Z3, CVC5, Coq, Agda, Metamath, SPASS (all apt), plus
+# Lean 4 (via elan), Isabelle, F*, and Mizar where upstream distributions
+# cooperate with an unprivileged build environment.
+#
+# Build:  podman build -f .containerization/Containerfile.mcp -t echidna:mcp .
+# Run:    podman run --rm -i echidna:mcp           # stdio MCP transport
+# Use:    {"mcpServers":{"echidna":{"command":"podman",
+#           "args":["run","--rm","-i","echidna:mcp"]}}}
+
+# =============================================================================
+# Stage 1: Rust builder — echidna + echidna-mcp + echidna-wire + typed_wasm
+# =============================================================================
+FROM docker.io/library/rust:1.85-slim-bookworm AS rust-builder
+
+RUN apt-get update && apt-get install -y --no-install-recommends \
+        build-essential \
+        pkg-config \
+        libssl-dev \
+        capnproto \
+    && rm -rf /var/lib/apt/lists/*
+
+WORKDIR /build
+
+COPY Cargo.toml Cargo.lock ./
+COPY src/rust ./src/rust
+COPY src/interfaces ./src/interfaces
+COPY crates ./crates
+COPY benches ./benches
+
+# Build both the CLI (echidna) and the MCP server (echidna-mcp). The MCP
+# server shells out to the CLI via the ECHIDNA_BIN env var.
+RUN cargo build --release --bin echidna -p echidna-mcp
+
+# =============================================================================
+# Stage 2: MVP prover installer (Debian apt-available set)
+# =============================================================================
+FROM docker.io/library/debian:bookworm-slim AS mvp-installer
+
+RUN apt-get update && apt-get install -y --no-install-recommends \
+        z3 \
+        cvc5 \
+        coq \
+        agda-bin \
+        metamath \
+        spass \
+    && rm -rf /var/lib/apt/lists/*
+
+# =============================================================================
+# Stage 3: Lean 4 installer (elan + stable toolchain)
+# =============================================================================
+FROM docker.io/library/debian:bookworm-slim AS lean-installer
+RUN apt-get update && apt-get install -y --no-install-recommends \
+        curl ca-certificates bash \
+    && rm -rf /var/lib/apt/lists/*
+RUN curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+        | bash -s -- -y --default-toolchain stable \
+    && . "$HOME/.elan/env" \
+    && lean --version
+
+# =============================================================================
+# Stage 4: Isabelle 2025 installer (tarball + pre-built Main heap)
+# =============================================================================
+FROM docker.io/library/debian:bookworm-slim AS isabelle-installer
+RUN apt-get update && apt-get install -y --no-install-recommends \
+        curl ca-certificates perl fontconfig \
+    && rm -rf /var/lib/apt/lists/*
+RUN curl -fsSL --retry 3 \
+        "https://isabelle.in.tum.de/dist/Isabelle2025-2_linux.tar.gz" \
+        -o /tmp/isabelle.tar.gz \
+    && tar -xzf /tmp/isabelle.tar.gz -C /opt/ \
+    && rm /tmp/isabelle.tar.gz \
+    && rm -rf /opt/Isabelle2025-2/doc \
+    && /opt/Isabelle2025-2/bin/isabelle version \
+    && /opt/Isabelle2025-2/bin/isabelle build -b Main \
+    && rm -rf /root/.isabelle/Isabelle2025-2/log \
+              /root/.isabelle/Isabelle2025-2/browser_info
+
+# =============================================================================
+# Stage 5: F* installer (binary release)
+# =============================================================================
+FROM docker.io/library/debian:bookworm-slim AS fstar-installer
+RUN apt-get update && apt-get install -y --no-install-recommends \
+        curl ca-certificates jq tar gzip \
+    && rm -rf /var/lib/apt/lists/*
+# Resolve the latest F* Linux x86_64 release tarball via the GitHub API
+# (asset naming varies between releases; don't hard-code a version).
+RUN set -eu; \
+    url=$(curl -fsSL https://api.github.com/repos/FStarLang/FStar/releases/latest \
+            | jq -r '.assets[]|select(.name|test("Linux|linux.*x86_64"))|.browser_download_url' \
+            | head -1); \
+    if [ -n "$url" ]; then \
+        curl -fsSL "$url" -o /tmp/fstar.tar.gz \
+        && mkdir -p /opt/fstar \
+        && tar -xzf /tmp/fstar.tar.gz -C /opt/fstar --strip-components=1 \
+        && /opt/fstar/bin/fstar.exe --version || true; \
+    else \
+        mkdir -p /opt/fstar/bin; \
+        echo "WARN: no F* linux asset found; stage empty" >&2; \
+    fi
+
+# =============================================================================
+# Stage 6: Runtime image
+# =============================================================================
+FROM docker.io/library/debian:bookworm-slim
+
+LABEL maintainer="Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
+LABEL org.opencontainers.image.source="https://github.com/hyperpolymath/echidna"
+LABEL org.opencontainers.image.description="ECHIDNA MCP server — AI-agent-callable theorem proving over stdio"
+LABEL org.opencontainers.image.licenses="PMPL-1.0-or-later"
+LABEL org.opencontainers.image.version="2.1.0"
+
+# Runtime deps: the MVP provers + dynamic libs + perl/fontconfig for Isabelle.
+RUN apt-get update && apt-get install -y --no-install-recommends \
+        ca-certificates \
+        libssl3 \
+        libgmp10 \
+        libstdc++6 \
+        perl \
+        fontconfig \
+        z3 \
+        cvc5 \
+        coq \
+        agda-bin \
+        metamath \
+        spass \
+    && rm -rf /var/lib/apt/lists/*
+
+WORKDIR /app
+
+COPY --from=rust-builder  /build/target/release/echidna     /app/bin/echidna
+COPY --from=rust-builder  /build/target/release/echidna-mcp /app/bin/echidna-mcp
+COPY --from=lean-installer /root/.elan                      /opt/elan
+COPY --from=isabelle-installer /opt/Isabelle2025-2          /opt/Isabelle2025-2
+COPY --from=isabelle-installer /root/.isabelle              /root/.isabelle
+COPY --from=fstar-installer /opt/fstar                      /opt/fstar
+
+ENV PATH="/app/bin:/opt/elan/toolchains/stable/bin:/opt/Isabelle2025-2/bin:/opt/fstar/bin:${PATH}"
+ENV ECHIDNA_BIN="/app/bin/echidna"
+
+# Stdio transport — no ports. The client connects via podman run -i.
+ENTRYPOINT ["/app/bin/echidna-mcp"]

src/rust/provers/abc.rs

@@ -414,20 +414,34 @@ impl ProverBackend for AbcBackend {
             .context("Failed to read ABC input file")?;
 
         let extension = path.extension().and_then(|e| e.to_str());
-        self.parse_design(&content, extension)
+        let mut state = self.parse_design(&content, extension)?;
+        state.metadata.insert(
+            "abc_source".to_string(),
+            serde_json::Value::String(content.clone()),
+        );
+        state.metadata.insert(
+            "source_path".to_string(),
+            serde_json::Value::String(path.to_string_lossy().into_owned()),
+        );
+        Ok(state)
     }
 
     async fn parse_string(&self, content: &str) -> Result<ProofState> {
         // Without file extension context, try ABC command script first,
         // then fall back to AIGER ASCII if header starts with "aag"/"aig"
         let trimmed = content.trim();
-        if trimmed.starts_with("aag") || trimmed.starts_with("aig") {
-            self.parse_design(content, Some("aig"))
+        let mut state = if trimmed.starts_with("aag") || trimmed.starts_with("aig") {
+            self.parse_design(content, Some("aig"))?
         } else if trimmed.starts_with(".model") || trimmed.starts_with(".inputs") {
-            self.parse_design(content, Some("blif"))
+            self.parse_design(content, Some("blif"))?
         } else {
-            self.parse_design(content, None)
-        }
+            self.parse_design(content, None)?
+        };
+        state.metadata.insert(
+            "abc_source".to_string(),
+            serde_json::Value::String(content.to_string()),
+        );
+        Ok(state)
     }
 
     async fn apply_tactic(&self, state: &ProofState, tactic: &Tactic) -> Result<TacticResult> {
@@ -567,6 +581,131 @@ impl ProverBackend for AbcBackend {
     }
 
     async fn verify_proof(&self, state: &ProofState) -> Result<bool> {
+        // Prefer the original source — parsing ABC/BLIF/AIGER into the
+        // generic Term IR and reconstructing via `to_abc_script` loses
+        // structure for anything beyond a one-command script.
+        let method = state
+            .metadata
+            .get("abc_method")
+            .and_then(|v| v.as_str())
+            .unwrap_or("pdr");
+        let bmc_bound = state
+            .metadata
+            .get("bmc_bound")
+            .and_then(|v| v.as_str())
+            .unwrap_or("100");
+        let verify_cmd = match method {
+            "bmc" | "bmc3" => format!("bmc3 -F {}", bmc_bound),
+            "int" => "int".to_string(),
+            "dprove" => "dprove".to_string(),
+            "dsec" => "dsec".to_string(),
+            "cec" => "cec".to_string(),
+            _ => "pdr".to_string(),
+        };
+
+        if let Some(path) = state.metadata.get("source_path").and_then(|v| v.as_str()) {
+            let p = std::path::Path::new(path);
+            let read_cmd = match p.extension().and_then(|e| e.to_str()) {
+                Some("aig") => format!("read_aiger {}", path),
+                Some("blif") => format!("read_blif {}", path),
+                Some("v") => format!("read_verilog {}", path),
+                _ => format!("read {}", path),
+            };
+            let script = format!("{}\n{}\nprint_status\nquit\n", read_cmd, verify_cmd);
+            let tmp_dir =
+                tempfile::tempdir().context("Failed to create temporary directory for ABC")?;
+            let tmp_file = tmp_dir.path().join("verify.abc");
+            tokio::fs::write(&tmp_file, &script)
+                .await
+                .context("Failed to write temporary ABC script file")?;
+            let output = tokio::time::timeout(
+                tokio::time::Duration::from_secs(self.config.timeout),
+                Command::new(&self.config.executable)
+                    .arg("-f")
+                    .arg(&tmp_file)
+                    .stdout(Stdio::piped())
+                    .stderr(Stdio::piped())
+                    .output(),
+            )
+            .await
+            .map_err(|_| anyhow!("ABC timed out after {} seconds", self.config.timeout))?
+            .context("Failed to execute ABC")?;
+            let stdout = String::from_utf8_lossy(&output.stdout);
+            let stderr = String::from_utf8_lossy(&output.stderr);
+            let combined = format!("{}\n{}", stdout, stderr);
+            return self.parse_result(&combined);
+        }
+
+        if let Some(source) = state.metadata.get("abc_source").and_then(|v| v.as_str()) {
+            let trimmed = source.trim();
+            let (ext, read_cmd_base) =
+                if trimmed.starts_with("aag") || trimmed.starts_with("aig") {
+                    (".aig", "read_aiger")
+                } else if trimmed.starts_with(".model") || trimmed.starts_with(".inputs") {
+                    (".blif", "read_blif")
+                } else {
+                    // Inline script — just execute it directly.
+                    ("", "")
+                };
+            let tmp_dir =
+                tempfile::tempdir().context("Failed to create temporary directory for ABC")?;
+            if ext.is_empty() {
+                let tmp_file = tmp_dir.path().join("verify.abc");
+                let script = format!("{}\n{}\nprint_status\nquit\n", source, verify_cmd);
+                tokio::fs::write(&tmp_file, &script)
+                    .await
+                    .context("Failed to write temporary ABC script file")?;
+                let output = tokio::time::timeout(
+                    tokio::time::Duration::from_secs(self.config.timeout),
+                    Command::new(&self.config.executable)
+                        .arg("-f")
+                        .arg(&tmp_file)
+                        .stdout(Stdio::piped())
+                        .stderr(Stdio::piped())
+                        .output(),
+                )
+                .await
+                .map_err(|_| anyhow!("ABC timed out after {} seconds", self.config.timeout))?
+                .context("Failed to execute ABC")?;
+                let stdout = String::from_utf8_lossy(&output.stdout);
+                let stderr = String::from_utf8_lossy(&output.stderr);
+                let combined = format!("{}\n{}", stdout, stderr);
+                return self.parse_result(&combined);
+            } else {
+                let design_file = tmp_dir.path().join(format!("design{}", ext));
+                tokio::fs::write(&design_file, source)
+                    .await
+                    .context("Failed to write temporary ABC design file")?;
+                let script_file = tmp_dir.path().join("verify.abc");
+                let script = format!(
+                    "{} {}\n{}\nprint_status\nquit\n",
+                    read_cmd_base,
+                    design_file.display(),
+                    verify_cmd
+                );
+                tokio::fs::write(&script_file, &script)
+                    .await
+                    .context("Failed to write temporary ABC script file")?;
+                let output = tokio::time::timeout(
+                    tokio::time::Duration::from_secs(self.config.timeout),
+                    Command::new(&self.config.executable)
+                        .arg("-f")
+                        .arg(&script_file)
+                        .stdout(Stdio::piped())
+                        .stderr(Stdio::piped())
+                        .output(),
+                )
+                .await
+                .map_err(|_| anyhow!("ABC timed out after {} seconds", self.config.timeout))?
+                .context("Failed to execute ABC")?;
+                let stdout = String::from_utf8_lossy(&output.stdout);
+                let stderr = String::from_utf8_lossy(&output.stderr);
+                let combined = format!("{}\n{}", stdout, stderr);
+                return self.parse_result(&combined);
+            }
+        }
+
+        // Fallback: reconstruct an ABC script from the parsed IR.
         let abc_script = self.to_abc_script(state)?;
 
         // ABC can execute commands via -c flag or from a script file.