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 = ctx
50            .resolved_path("project_root")
51            .unwrap_or(&ctx.project_root)
52            .to_string();
53        let format = get_str(args, "format");
54        let write = get_bool(args, "write").unwrap_or(true);
55        let filename = get_str(args, "filename");
56        let max_evidence = get_int(args, "max_evidence").map(|v| v as usize);
57        let max_ledger_files = get_int(args, "max_ledger_files").map(|v| v as usize);
58
59        let session_data = ctx
60            .session
61            .as_ref()
62            .map(|s| tokio::task::block_in_place(|| s.blocking_read()).clone());
63        let pipeline_data = ctx
64            .pipeline_stats
65            .as_ref()
66            .map(|p| tokio::task::block_in_place(|| p.blocking_read()).clone());
67        let ledger_data = ctx
68            .ledger
69            .as_ref()
70            .map(|l| tokio::task::block_in_place(|| l.blocking_read()).clone());
71
72        let sources = crate::core::context_proof::ProofSources {
73            project_root: Some(root.clone()),
74            session: session_data,
75            pipeline: pipeline_data,
76            ledger: ledger_data,
77        };
78
79        let out = crate::tools::ctx_proof::handle_export(
80            &root,
81            format.as_deref(),
82            write,
83            filename.as_deref(),
84            max_evidence,
85            max_ledger_files,
86            sources,
87        )
88        .map_err(|e| ErrorData::invalid_params(e, None))?;
89
90        Ok(ToolOutput {
91            text: out,
92            original_tokens: 0,
93            saved_tokens: 0,
94            mode: Some(action),
95            path: Some(root),
96            changed: false,
97        })
98    }
99}
lean_ctx/tools/registered/ctx_proof.rs

lean_ctx/tools/registered/
ctx_proof.rs
