lean-ctx-server 3.12.3

The LeanCTX MCP server and its tools on top of LeanCTX | OSS.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83

// SPDX-License-Identifier: Apache-2.0
pub fn handle_proof(format: Option<&str>) -> Result<String, String> {
    // The caller's own session: a proof never covers another agent's (I07).
    let session = lean_ctx::core::session::caller::with(Clone::clone);
    let run_id = session
        .as_ref()
        .map_or_else(|| "anonymous".to_string(), |s| s.id.clone());
    let session_id = session.as_ref().map(|s| s.id.clone());

    let mut extractor =
        lean_ctx::core::claim_extractor::ClaimExtractor::new(&run_id, session_id.as_deref());

    if let Some(ref sess) = session {
        let jail_root = sess.project_root.as_ref().map_or_else(
            || std::env::current_dir().unwrap_or_default(),
            std::path::PathBuf::from,
        );
        for ft in &sess.files_touched {
            extractor.verify_pathjail(&ft.path, &jail_root);
        }
    }

    let proof = extractor.finalize();

    match format.unwrap_or("json") {
        "summary" => {
            let s = &proof.summary;
            Ok(format!(
                "ContextProofV2 · {} claims · Q{} ({:?})\n  passed: {} · failed: {} · skipped: {}",
                s.total_claims,
                proof.quality_level as u8,
                proof.quality_level,
                s.passed,
                s.failed,
                s.skipped,
            ))
        }
        _ => serde_json::to_string_pretty(&proof).map_err(|e| e.to_string()),
    }
}

pub fn handle_stats(format: Option<&str>) -> Result<String, String> {
    let snap = lean_ctx::core::verification_observability::snapshot_v1();
    match format.unwrap_or("summary") {
        "json" => Ok(serde_json::to_string_pretty(&snap).map_err(|e| e.to_string())?),
        "both" => Ok(format!(
            "{}\n\n{}",
            lean_ctx::core::verification_observability::format_compact(&snap),
            serde_json::to_string_pretty(&snap).map_err(|e| e.to_string())?
        )),
        _ => Ok(lean_ctx::core::verification_observability::format_compact(
            &snap,
        )),
    }
}

#[cfg(test)]
mod tests {
    use super::handle_proof;

    /// The proof carries PathJail claims only; the description promised
    /// budget claims that were never produced.
    #[test]
    fn description_promises_no_budget_claims() {
        use crate::server::tool_trait::McpTool;
        let def = crate::tools::registered::ctx_verify::CtxVerifyTool.tool_def();
        let text = serde_json::to_string(&def).unwrap();
        assert!(!text.contains("budget"), "{text}");
    }

    #[test]
    fn proof_reports_only_claims_checked_at_runtime() {
        let _data = lean_ctx::core::data_dir::isolated_data_dir();
        let json = handle_proof(Some("json")).unwrap();
        let proof: serde_json::Value = serde_json::from_str(&json).unwrap();
        for claim in proof["claims"].as_array().unwrap() {
            assert_eq!(claim["verifier"], "path_policy", "{claim}");
        }
        for unchecked in ["proved", "lean_theorem", "lean_axioms", "formally_verified"] {
            assert!(!json.contains(unchecked), "{unchecked} in {json}");
        }
    }
}