From 466e9b68ea3767b9ba203603c8a4605cff8b7f8b Mon Sep 17 00:00:00 2001
From: Allaun Silverfox <28494262+allaunthefox@users.noreply.github.com>
Date: Tue, 26 May 2026 17:42:33 -0500
Subject: [PATCH] feat(runtime): load MCP tools list from Lean manifest JSON
 (shim-only)

---
 .../crates/runtime/src/lean_mcp_manifest.rs   | 119 ++++++++++++++++++
 1 file changed, 119 insertions(+)
 create mode 100644 1-Distributed-Systems/agents/claw/rust/crates/runtime/src/lean_mcp_manifest.rs

diff --git a/1-Distributed-Systems/agents/claw/rust/crates/runtime/src/lean_mcp_manifest.rs b/1-Distributed-Systems/agents/claw/rust/crates/runtime/src/lean_mcp_manifest.rs
new file mode 100644
index 00000000..0db5f4b8
--- /dev/null
+++ b/1-Distributed-Systems/agents/claw/rust/crates/runtime/src/lean_mcp_manifest.rs
@@ -0,0 +1,119 @@
+//! Lean-first MCP manifest loader.
+//!
+//! This is a boundary shim: it loads the published MCP tool list from a Lean-owned
+//! JSON manifest (generated by `Semantics.McpSurfaceManifest`).
+//!
+//! Semantics are NOT defined here: this module only parses JSON into runtime
+//! `McpTool` descriptors.
+
+use std::process::Command;
+
+use serde_json::Value as JsonValue;
+
+use crate::mcp_stdio::McpTool;
+
+/// Load tool descriptors from a JSON value shaped like `{ "tools": [...] }`.
+pub fn tools_from_json(value: &JsonValue) -> Result<Vec<McpTool>, String> {
+    let tools = value
+        .get("tools")
+        .and_then(|v| v.as_array())
+        .ok_or_else(|| "Lean MCP manifest missing 'tools' array".to_string())?;
+
+    let mut parsed = Vec::with_capacity(tools.len());
+    for tool in tools {
+        let name = tool
+            .get("name")
+            .and_then(|v| v.as_str())
+            .ok_or_else(|| "Lean MCP manifest tool missing 'name'".to_string())?
+            .to_string();
+        let description = tool
+            .get("description")
+            .and_then(|v| v.as_str())
+            .map(|s| s.to_string());
+        let input_schema = tool.get("inputSchema").cloned();
+
+        parsed.push(McpTool {
+            name,
+            description,
+            input_schema,
+            annotations: None,
+            meta: None,
+        });
+    }
+
+    Ok(parsed)
+}
+
+/// Run an external command that prints the Lean-owned tools list JSON to stdout.
+///
+/// The command is provided as a vector to avoid shell injection.
+pub fn tools_from_lean_command(command: &[String]) -> Result<Vec<McpTool>, String> {
+    if command.is_empty() {
+        return Err("Lean MCP manifest command is empty".to_string());
+    }
+
+    let mut cmd = Command::new(&command[0]);
+    if command.len() > 1 {
+        cmd.args(&command[1..]);
+    }
+
+    let output = cmd
+        .output()
+        .map_err(|error| format!("failed to spawn Lean MCP manifest command: {error}"))?;
+
+    if !output.status.success() {
+        return Err(format!(
+            "Lean MCP manifest command failed (status={}): {}",
+            output.status,
+            String::from_utf8_lossy(&output.stderr)
+        ));
+    }
+
+    let json: JsonValue = serde_json::from_slice(&output.stdout)
+        .map_err(|error| format!("failed to parse Lean MCP manifest JSON: {error}"))?;
+
+    tools_from_json(&json)
+}
+
+/// Load the Lean manifest using environment variables.
+///
+/// - `CLAW_LEAN_MCP_MANIFEST_CMD`: a JSON array of strings, e.g.
+///   `["bash","-lc","cd 0-Core-Formalism/otom/tools/lean/Semantics && lake env lean -R Semantics -E 'import Semantics.McpSurfaceManifest; open Semantics.McpSurfaceManifest; #eval instanceToolsJson'"]`
+///
+/// This stays shim-only: the env var provides *how* to invoke Lean; the manifest
+/// itself is the tool truth.
+pub fn tools_from_env() -> Result<Option<Vec<McpTool>>, String> {
+    let cmd = std::env::var("CLAW_LEAN_MCP_MANIFEST_CMD").ok();
+    let Some(cmd) = cmd else {
+        return Ok(None);
+    };
+
+    let command: Vec<String> = serde_json::from_str(&cmd)
+        .map_err(|error| format!("CLAW_LEAN_MCP_MANIFEST_CMD must be JSON array: {error}"))?;
+
+    Ok(Some(tools_from_lean_command(&command)?))
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use serde_json::json;
+
+    #[test]
+    fn parses_tools_from_lean_json_shape() {
+        let manifest = json!({
+            "tools": [
+                {
+                    "name": "connector_health",
+                    "description": "Return connector manifest + readiness state.",
+                    "inputSchema": {"type": "object", "properties": {}}
+                }
+            ]
+        });
+
+        let tools = tools_from_json(&manifest).expect("tools parse");
+        assert_eq!(tools.len(), 1);
+        assert_eq!(tools[0].name, "connector_health");
+        assert!(tools[0].input_schema.is_some());
+    }
+}