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                })
47            }
48            "proof" | "v2" => {
49                let out = crate::tools::ctx_verify::handle_proof(format.as_deref())
50                    .map_err(|e| ErrorData::invalid_params(e, None))?;
51                Ok(ToolOutput {
52                    text: out,
53                    original_tokens: 0,
54                    saved_tokens: 0,
55                    mode: Some(action),
56                    path: None,
57                })
58            }
59            _ => Err(ErrorData::invalid_params(
60                "unsupported action (expected: stats, proof, v2)",
61                None,
62            )),
63        }
64    }
65}
lean_ctx/tools/registered/ctx_verify.rs

lean_ctx/tools/registered/
ctx_verify.rs
