lean_ctx/tools/registered/
ctx_verify.rs

1use rmcp::ErrorData;
2use rmcp::model::Tool;
3use serde_json::{Map, Value, json};
4
5use crate::server::tool_trait::{McpTool, ToolContext, ToolOutput, get_str};
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 — tool call statistics and claim-based verification.\n\
19             WORKFLOW: action=stats to monitor tool usage; action=proof|v2 for Lean4 proof verification.\n\
20             Actions: stats|proof|v2 (format=summary|json|both, default summary).\n\
21             ANTIPATTERN: not for runtime verification during active development — use for periodic audit.",
22            json!({
23                "type": "object",
24                "properties": {
25                    "action": {
26                        "type": "string",
27                        "enum": ["stats", "proof", "v2"],
28                        "description": "stats|proof|v2"
29                    },
30                    "format": {
31                        "type": "string",
32                        "enum": ["summary", "json", "both"],
33                        "description": "Output format: summary|json|both (default summary)"
34                    }
35                }
36            }),
37        )
38    }
39
40    fn handle(
41        &self,
42        args: &Map<String, Value>,
43        _ctx: &ToolContext,
44    ) -> Result<ToolOutput, ErrorData> {
45        let action = get_str(args, "action").unwrap_or_else(|| "stats".to_string());
46        let format = get_str(args, "format");
47        match action.as_str() {
48            "stats" => {
49                let out = crate::tools::ctx_verify::handle_stats(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                    changed: false,
58                    shell_outcome: None,
59                    content_blocks: None,
60                })
61            }
62            "proof" | "v2" => {
63                let out = crate::tools::ctx_verify::handle_proof(format.as_deref())
64                    .map_err(|e| ErrorData::invalid_params(e, None))?;
65                Ok(ToolOutput {
66                    text: out,
67                    original_tokens: 0,
68                    saved_tokens: 0,
69                    mode: Some(action),
70                    path: None,
71                    changed: false,
72                    shell_outcome: None,
73                    content_blocks: None,
74                })
75            }
76            _ => Err(ErrorData::invalid_params(
77                "unsupported action (expected: stats, proof, v2)",
78                None,
79            )),
80        }
81    }
82}
lean_ctx/tools/registered/ctx_verify.rs

lean_ctx/tools/registered/
ctx_verify.rs
