lean_ctx/tools/
ctx_verify.rs

1pub fn handle_proof(format: Option<&str>) -> Result<String, String> {
2    let session = crate::core::session::SessionState::load_latest();
3    let run_id = session
4        .as_ref()
5        .map_or_else(|| "anonymous".to_string(), |s| s.id.clone());
6    let session_id = session.as_ref().map(|s| s.id.clone());
7
8    let mut extractor =
9        crate::core::claim_extractor::ClaimExtractor::new(&run_id, session_id.as_deref());
10
11    if let Some(ref sess) = session {
12        let jail_root = sess.project_root.as_ref().map_or_else(
13            || std::env::current_dir().unwrap_or_default(),
14            std::path::PathBuf::from,
15        );
16        for ft in &sess.files_touched {
17            extractor.verify_pathjail(&ft.path, &jail_root);
18        }
19    }
20
21    extractor.verify_budget_compliance();
22
23    extractor.add_lean_proof(
24        "pathjail_no_escape",
25        "PathJail prevents directory traversal outside root",
26        crate::core::context_proof_v2::ClaimKind::PathjailCompliance,
27        "LeanCtxProofs.Policy.PathJail.jail_no_escape",
28    );
29    extractor.add_lean_proof(
30        "budget_monotonic",
31        "Budget consumption is monotonically increasing",
32        crate::core::context_proof_v2::ClaimKind::BudgetCompliance,
33        "LeanCtxProofs.Policy.BudgetEnforcement.spend_monotonic",
34    );
35    extractor.add_lean_proof(
36        "terse_quality_gate",
37        "Quality gate preserves paths and identifiers",
38        crate::core::context_proof_v2::ClaimKind::CompressionInvariant,
39        "LeanCtxProofs.Compression.TerseQuality.both_ok_passes",
40    );
41    extractor.add_lean_proof(
42        "terse_filter_subset",
43        "Terse filtering produces a subset of input",
44        crate::core::context_proof_v2::ClaimKind::CompressionInvariant,
45        "LeanCtxProofs.Compression.TerseEngine.filter_subset",
46    );
47
48    let proof = extractor.finalize();
49
50    match format.unwrap_or("json") {
51        "summary" => {
52            let s = &proof.summary;
53            Ok(format!(
54                "ContextProofV2 · {} claims · Q{} ({:?})\n  proved: {} · passed: {} · failed: {} · skipped: {}",
55                s.total_claims,
56                proof.quality_level as u8,
57                proof.quality_level,
58                s.proved, s.passed, s.failed, s.skipped,
59            ))
60        }
61        _ => serde_json::to_string_pretty(&proof).map_err(|e| e.to_string()),
62    }
63}
64
65pub fn handle_stats(format: Option<&str>) -> Result<String, String> {
66    let snap = crate::core::verification_observability::snapshot_v1();
67    match format.unwrap_or("summary") {
68        "json" => Ok(serde_json::to_string_pretty(&snap).map_err(|e| e.to_string())?),
69        "both" => Ok(format!(
70            "{}\n\n{}",
71            crate::core::verification_observability::format_compact(&snap),
72            serde_json::to_string_pretty(&snap).map_err(|e| e.to_string())?
73        )),
74        _ => Ok(crate::core::verification_observability::format_compact(
75            &snap,
76        )),
77    }
78}
lean_ctx/tools/ctx_verify.rs

lean_ctx/tools/
ctx_verify.rs
