lean_ctx/core/
claim_extractor.rs

1//! Claim Extraction — decomposes context pipeline outputs into verifiable claims.
2//!
3//! Inspired by VERGE (arXiv:2601.20055): instead of verifying entire outputs
4//! monolithically, we decompose them into atomic, individually verifiable claims
5//! and route each to the appropriate verifier.
6
7use std::path::Path;
8
9use super::context_proof_v2::{
10    deterministic_claim, lean_proved_claim, policy_claim, Claim, ClaimKind, ClaimStatus,
11    ContextProofV2, VerifierKind,
12};
13
14pub struct ClaimExtractor {
15    proof: ContextProofV2,
16}
17
18impl ClaimExtractor {
19    pub fn new(run_id: &str, session_id: Option<&str>) -> Self {
20        Self {
21            proof: ContextProofV2::new(
22                run_id.to_string(),
23                session_id.map(std::string::ToString::to_string),
24            ),
25        }
26    }
27
28    pub fn verify_pathjail(&mut self, path: &str, jail_root: &Path) {
29        let resolved = crate::core::pathjail::jail_path(&std::path::PathBuf::from(path), jail_root);
30        let passed = resolved.is_ok();
31        self.proof.add_claim(policy_claim(
32            &format!("pathjail:{path}"),
33            &format!("Path '{path}' is within jail root"),
34            ClaimKind::PathjailCompliance,
35            passed,
36        ));
37    }
38
39    pub fn verify_no_secrets_in_output(&mut self, output: &str) {
40        let secret_matches = crate::core::secret_detection::detect_secrets(output);
41
42        let passed = secret_matches.is_empty();
43        let text = if passed {
44            "No secret patterns found in output".to_string()
45        } else {
46            let names: Vec<&str> = secret_matches.iter().map(|m| m.pattern_name).collect();
47            let mut unique_names: Vec<&str> = names.clone();
48            unique_names.sort_unstable();
49            unique_names.dedup();
50            format!(
51                "Secret patterns detected ({}): {}",
52                secret_matches.len(),
53                unique_names.join(", ")
54            )
55        };
56
57        self.proof.add_claim(policy_claim(
58            "no_secrets",
59            &text,
60            ClaimKind::SecretPolicy,
61            passed,
62        ));
63    }
64
65    pub fn verify_budget_compliance(&mut self) {
66        let snapshot = crate::core::budget_tracker::BudgetTracker::global().check();
67        let level = snapshot.worst_level();
68        let passed = *level != crate::core::budget_tracker::BudgetLevel::Exhausted;
69
70        self.proof.add_claim(policy_claim(
71            "budget_compliance",
72            &format!("Budget level: {level}"),
73            ClaimKind::BudgetCompliance,
74            passed,
75        ));
76    }
77
78    pub fn verify_signatures_preserved(&mut self, original: &[String], compressed: &[String]) {
79        let mut missing = Vec::new();
80        for sig in original {
81            if !compressed.iter().any(|c| c.contains(sig)) {
82                missing.push(sig.clone());
83            }
84        }
85
86        let passed = missing.is_empty();
87        let text = if passed {
88            format!("All {} signatures preserved", original.len())
89        } else {
90            format!(
91                "{} of {} signatures missing: {:?}",
92                missing.len(),
93                original.len(),
94                &missing[..missing.len().min(3)]
95            )
96        };
97
98        self.proof.add_claim(Claim {
99            id: "signatures_preserved".to_string(),
100            text,
101            kind: ClaimKind::CompressionInvariant,
102            verifier: VerifierKind::Ast,
103            status: if passed {
104                ClaimStatus::Passed
105            } else {
106                ClaimStatus::Failed
107            },
108            evidence_ref: None,
109            lean_theorem: if passed {
110                Some("pinned_items_always_preserved".to_string())
111            } else {
112                None
113            },
114            lean_axioms: None,
115        });
116    }
117
118    pub fn verify_imports_preserved(&mut self, original_imports: &[String], compressed: &str) {
119        let mut missing = Vec::new();
120        for imp in original_imports {
121            if !compressed.contains(imp) {
122                missing.push(imp.clone());
123            }
124        }
125
126        let passed = missing.is_empty();
127        let text = if passed {
128            format!("All {} imports preserved", original_imports.len())
129        } else {
130            format!(
131                "{} of {} imports missing",
132                missing.len(),
133                original_imports.len()
134            )
135        };
136
137        self.proof
138            .add_claim(deterministic_claim("imports_preserved", &text, passed));
139    }
140
141    pub fn add_lean_proof(&mut self, id: &str, text: &str, kind: ClaimKind, theorem: &str) {
142        self.proof
143            .add_claim(lean_proved_claim(id, text, kind, theorem));
144    }
145
146    pub fn add_custom_claim(&mut self, claim: Claim) {
147        self.proof.add_claim(claim);
148    }
149
150    pub fn finalize(self) -> ContextProofV2 {
151        self.proof
152    }
153}
154
155#[cfg(test)]
156mod tests {
157    use super::*;
158
159    #[test]
160    fn secret_detection_catches_aws_keys() {
161        let mut ext = ClaimExtractor::new("test_1", None);
162        ext.verify_no_secrets_in_output("const key = 'AKIAIOSFODNN7EXAMPLE'");
163        let proof = ext.finalize();
164        assert_eq!(proof.summary.failed, 1);
165    }
166
167    #[test]
168    fn clean_output_passes_secret_check() {
169        let mut ext = ClaimExtractor::new("test_2", None);
170        ext.verify_no_secrets_in_output("fn main() { println!(\"hello\"); }");
171        let proof = ext.finalize();
172        assert_eq!(proof.summary.passed, 1);
173        assert_eq!(proof.summary.failed, 0);
174    }
175
176    #[test]
177    fn signatures_preserved_check() {
178        let mut ext = ClaimExtractor::new("test_3", None);
179        let original = vec!["fn main".to_string(), "pub fn process".to_string()];
180        let compressed = vec![
181            "fn main() { ... }".to_string(),
182            "pub fn process(data: &[u8]) -> Result<(), Error>".to_string(),
183        ];
184        ext.verify_signatures_preserved(&original, &compressed);
185        let proof = ext.finalize();
186        assert_eq!(proof.summary.passed, 1);
187    }
188
189    #[test]
190    fn missing_signatures_detected() {
191        let mut ext = ClaimExtractor::new("test_4", None);
192        let original = vec!["fn main()".to_string(), "pub fn gone()".to_string()];
193        let compressed = vec!["fn main() { ... }".to_string()];
194        ext.verify_signatures_preserved(&original, &compressed);
195        let proof = ext.finalize();
196        assert_eq!(proof.summary.failed, 1);
197    }
198
199    #[test]
200    fn lean_proof_integration() {
201        let mut ext = ClaimExtractor::new("test_5", None);
202        ext.add_lean_proof(
203            "pathjail_no_escape",
204            "PathJail prevents access outside root",
205            ClaimKind::PathjailCompliance,
206            "LeanCtxProofs.Policy.PathJail.jail_no_escape",
207        );
208        let proof = ext.finalize();
209        assert_eq!(proof.summary.proved, 1);
210        assert!(proof.claims[0].lean_theorem.is_some());
211    }
212
213    #[test]
214    fn combined_extraction_computes_quality() {
215        let mut ext = ClaimExtractor::new("test_6", None);
216        ext.verify_no_secrets_in_output("clean code");
217        ext.add_lean_proof(
218            "excluded_never_rendered",
219            "Excluded items never in output",
220            ClaimKind::CompressionInvariant,
221            "LeanCtxProofs.Policy.ContextGovernance.excluded_items_never_rendered",
222        );
223        let proof = ext.finalize();
224        assert_eq!(
225            proof.quality_level,
226            super::super::context_proof_v2::QualityLevel::FormallyVerified
227        );
228    }
229
230    #[test]
231    fn detects_github_pat() {
232        let mut ext = ClaimExtractor::new("test_gh", None);
233        ext.verify_no_secrets_in_output("token = ghp_1234567890abcdef");
234        let proof = ext.finalize();
235        assert_eq!(proof.summary.failed, 1);
236    }
237
238    #[test]
239    fn detects_gitlab_pat() {
240        let mut ext = ClaimExtractor::new("test_gl", None);
241        ext.verify_no_secrets_in_output("glpat-xxxxxxxxxxxxxxxxxxxx");
242        let proof = ext.finalize();
243        assert_eq!(proof.summary.failed, 1);
244    }
245
246    #[test]
247    fn detects_pem_private_key() {
248        let mut ext = ClaimExtractor::new("test_pem", None);
249        ext.verify_no_secrets_in_output("-----BEGIN RSA PRIVATE KEY-----");
250        let proof = ext.finalize();
251        assert_eq!(proof.summary.failed, 1);
252    }
253
254    #[test]
255    fn empty_signatures_passes() {
256        let mut ext = ClaimExtractor::new("test_empty", None);
257        ext.verify_signatures_preserved(&[], &[]);
258        let proof = ext.finalize();
259        assert_eq!(proof.summary.passed, 1);
260        assert_eq!(proof.summary.failed, 0);
261    }
262
263    #[test]
264    fn empty_imports_passes() {
265        let mut ext = ClaimExtractor::new("test_imp", None);
266        ext.verify_imports_preserved(&[], "some content");
267        let proof = ext.finalize();
268        assert_eq!(proof.summary.passed, 1);
269    }
270
271    #[test]
272    fn finalize_returns_correct_run_id() {
273        let ext = ClaimExtractor::new("my_run_42", Some("sess_7"));
274        let proof = ext.finalize();
275        assert_eq!(proof.run_id, "my_run_42");
276        assert_eq!(proof.session_id, Some("sess_7".to_string()));
277    }
278
279    #[test]
280    fn multiple_secret_patterns_all_detected() {
281        let mut ext = ClaimExtractor::new("test_multi", None);
282        ext.verify_no_secrets_in_output(
283            "AKIAIOSFODNN7EXAMPLE1 and sk-abcdefghijklmnopqrstuvwx and password=longvalue1234567890extra",
284        );
285        let proof = ext.finalize();
286        assert_eq!(proof.summary.failed, 1);
287        assert!(proof.claims[0].text.contains("aws_key"));
288    }
289}
lean_ctx/core/claim_extractor.rs

lean_ctx/core/
claim_extractor.rs
