lean_ctx/tools/registered/
ctx_verify.rs

1use rmcp::model::Tool;
2use rmcp::ErrorData;
3use serde_json::{json, Map, Value};
4
5use crate::server::tool_trait::{get_str, McpTool, ToolContext, ToolOutput};
6use crate::tool_defs::tool_def;
7
8pub struct CtxVerifyTool;
9
10impl McpTool for CtxVerifyTool {
11    fn name(&self) -> &'static str {
12        "ctx_verify"
13    }
14
15    fn tool_def(&self) -> Tool {
16        tool_def(
17            "ctx_verify",
18            "Verification observability. Actions: stats (tool call statistics), proof|v2 (ContextProofV2 claim-based verification with Lean4 proofs).",
19            json!({
20                "type": "object",
21                "properties": {
22                    "action": { "type": "string", "description": "stats" },
23                    "format": { "type": "string" }
24                }
25            }),
26        )
27    }
28
29    fn handle(
30        &self,
31        args: &Map<String, Value>,
32        _ctx: &ToolContext,
33    ) -> Result<ToolOutput, ErrorData> {
34        let action = get_str(args, "action").unwrap_or_else(|| "stats".to_string());
35        let format = get_str(args, "format");
36        match action.as_str() {
37            "stats" => {
38                let out = crate::tools::ctx_verify::handle_stats(format.as_deref())
39                    .map_err(|e| ErrorData::invalid_params(e, None))?;
40                Ok(ToolOutput {
41                    text: out,
42                    original_tokens: 0,
43                    saved_tokens: 0,
44                    mode: Some(action),
45                    path: None,
46                    changed: false,
47                })
48            }
49            "proof" | "v2" => {
50                let out = crate::tools::ctx_verify::handle_proof(format.as_deref())
51                    .map_err(|e| ErrorData::invalid_params(e, None))?;
52                Ok(ToolOutput {
53                    text: out,
54                    original_tokens: 0,
55                    saved_tokens: 0,
56                    mode: Some(action),
57                    path: None,
58                    changed: false,
59                })
60            }
61            _ => Err(ErrorData::invalid_params(
62                "unsupported action (expected: stats, proof, v2)",
63                None,
64            )),
65        }
66    }
67}
lean_ctx/tools/registered/ctx_verify.rs

lean_ctx/tools/registered/
ctx_verify.rs
