lean_ctx/tools/registered/
ctx_proof.rs

1use rmcp::model::Tool;
2use rmcp::ErrorData;
3use serde_json::{json, Map, Value};
4
5use crate::server::tool_trait::{get_bool, get_int, get_str, McpTool, ToolContext, ToolOutput};
6use crate::tool_defs::tool_def;
7
8pub struct CtxProofTool;
9
10impl McpTool for CtxProofTool {
11    fn name(&self) -> &'static str {
12        "ctx_proof"
13    }
14
15    fn tool_def(&self) -> Tool {
16        tool_def(
17            "ctx_proof",
18            "Export a machine-readable ContextProofV1 (Verifier + SLO + Pipeline + Provenance). Writes to .lean-ctx/proofs/ by default.",
19            json!({
20                "type": "object",
21                "properties": {
22                    "action": { "type": "string", "description": "export (required)" },
23                    "project_root": { "type": "string", "description": "Project root for proof output (default: .)" },
24                    "format": { "type": "string", "description": "json|summary|both (default: json)" },
25                    "write": { "type": "boolean", "description": "Write proof file under .lean-ctx/proofs/ (default: true)" },
26                    "filename": { "type": "string", "description": "Optional output filename" },
27                    "max_evidence": { "type": "integer", "description": "Max tool receipts to include (default: 50)" },
28                    "max_ledger_files": { "type": "integer", "description": "Max context ledger top files to include (default: 10)" }
29                },
30                "required": ["action"]
31            }),
32        )
33    }
34
35    fn handle(
36        &self,
37        args: &Map<String, Value>,
38        ctx: &ToolContext,
39    ) -> Result<ToolOutput, ErrorData> {
40        let action = get_str(args, "action")
41            .ok_or_else(|| ErrorData::invalid_params("action is required", None))?;
42        if action != "export" {
43            return Err(ErrorData::invalid_params(
44                "unsupported action (expected: export)",
45                None,
46            ));
47        }
48
49        let root = if let Some(p) = ctx.resolved_path("project_root") {
50            p.to_string()
51        } else if let Some(err) = ctx.path_error("project_root") {
52            return Err(ErrorData::invalid_params(
53                format!("project_root: {err}"),
54                None,
55            ));
56        } else {
57            ctx.project_root.clone()
58        };
59        let format = get_str(args, "format");
60        let write = get_bool(args, "write").unwrap_or(true);
61        let filename = get_str(args, "filename");
62        let max_evidence = get_int(args, "max_evidence").map(|v| v as usize);
63        let max_ledger_files = get_int(args, "max_ledger_files").map(|v| v as usize);
64
65        let session_data = ctx
66            .session
67            .as_ref()
68            .map(|s| tokio::task::block_in_place(|| s.blocking_read()).clone());
69        let pipeline_data = ctx
70            .pipeline_stats
71            .as_ref()
72            .map(|p| tokio::task::block_in_place(|| p.blocking_read()).clone());
73        let ledger_data = ctx
74            .ledger
75            .as_ref()
76            .map(|l| tokio::task::block_in_place(|| l.blocking_read()).clone());
77
78        let sources = crate::core::context_proof::ProofSources {
79            project_root: Some(root.clone()),
80            session: session_data,
81            pipeline: pipeline_data,
82            ledger: ledger_data,
83        };
84
85        let out = crate::tools::ctx_proof::handle_export(
86            &root,
87            format.as_deref(),
88            write,
89            filename.as_deref(),
90            max_evidence,
91            max_ledger_files,
92            sources,
93        )
94        .map_err(|e| ErrorData::invalid_params(e, None))?;
95
96        Ok(ToolOutput {
97            text: out,
98            original_tokens: 0,
99            saved_tokens: 0,
100            mode: Some(action),
101            path: Some(root),
102            changed: false,
103        })
104    }
105}
lean_ctx/tools/registered/ctx_proof.rs

lean_ctx/tools/registered/
ctx_proof.rs
