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_patterns = [
41            "AKIA",       // AWS access key
42            "sk-",        // OpenAI key
43            "ghp_",       // GitHub PAT
44            "glpat-",     // GitLab PAT
45            "-----BEGIN", // PEM private keys
46            "password=",
47            "secret_key=",
48        ];
49
50        let mut found_secrets = Vec::new();
51        for pattern in &secret_patterns {
52            if output.contains(pattern) {
53                found_secrets.push(*pattern);
54            }
55        }
56
57        let passed = found_secrets.is_empty();
58        let text = if passed {
59            "No secret patterns found in output".to_string()
60        } else {
61            format!("Secret patterns detected: {}", found_secrets.join(", "))
62        };
63
64        self.proof.add_claim(policy_claim(
65            "no_secrets",
66            &text,
67            ClaimKind::SecretPolicy,
68            passed,
69        ));
70    }
71
72    pub fn verify_budget_compliance(&mut self) {
73        let snapshot = crate::core::budget_tracker::BudgetTracker::global().check();
74        let level = snapshot.worst_level();
75        let passed = *level != crate::core::budget_tracker::BudgetLevel::Exhausted;
76
77        self.proof.add_claim(policy_claim(
78            "budget_compliance",
79            &format!("Budget level: {level}"),
80            ClaimKind::BudgetCompliance,
81            passed,
82        ));
83    }
84
85    pub fn verify_signatures_preserved(&mut self, original: &[String], compressed: &[String]) {
86        let mut missing = Vec::new();
87        for sig in original {
88            if !compressed.iter().any(|c| c.contains(sig)) {
89                missing.push(sig.clone());
90            }
91        }
92
93        let passed = missing.is_empty();
94        let text = if passed {
95            format!("All {} signatures preserved", original.len())
96        } else {
97            format!(
98                "{} of {} signatures missing: {:?}",
99                missing.len(),
100                original.len(),
101                &missing[..missing.len().min(3)]
102            )
103        };
104
105        self.proof.add_claim(Claim {
106            id: "signatures_preserved".to_string(),
107            text,
108            kind: ClaimKind::CompressionInvariant,
109            verifier: VerifierKind::Ast,
110            status: if passed {
111                ClaimStatus::Passed
112            } else {
113                ClaimStatus::Failed
114            },
115            evidence_ref: None,
116            lean_theorem: if passed {
117                Some("pinned_items_always_preserved".to_string())
118            } else {
119                None
120            },
121            lean_axioms: None,
122        });
123    }
124
125    pub fn verify_imports_preserved(&mut self, original_imports: &[String], compressed: &str) {
126        let mut missing = Vec::new();
127        for imp in original_imports {
128            if !compressed.contains(imp) {
129                missing.push(imp.clone());
130            }
131        }
132
133        let passed = missing.is_empty();
134        let text = if passed {
135            format!("All {} imports preserved", original_imports.len())
136        } else {
137            format!(
138                "{} of {} imports missing",
139                missing.len(),
140                original_imports.len()
141            )
142        };
143
144        self.proof
145            .add_claim(deterministic_claim("imports_preserved", &text, passed));
146    }
147
148    pub fn add_lean_proof(&mut self, id: &str, text: &str, kind: ClaimKind, theorem: &str) {
149        self.proof
150            .add_claim(lean_proved_claim(id, text, kind, theorem));
151    }
152
153    pub fn add_custom_claim(&mut self, claim: Claim) {
154        self.proof.add_claim(claim);
155    }
156
157    pub fn finalize(self) -> ContextProofV2 {
158        self.proof
159    }
160}
161
162#[cfg(test)]
163mod tests {
164    use super::*;
165
166    #[test]
167    fn secret_detection_catches_aws_keys() {
168        let mut ext = ClaimExtractor::new("test_1", None);
169        ext.verify_no_secrets_in_output("const key = 'AKIAIOSFODNN7EXAMPLE'");
170        let proof = ext.finalize();
171        assert_eq!(proof.summary.failed, 1);
172    }
173
174    #[test]
175    fn clean_output_passes_secret_check() {
176        let mut ext = ClaimExtractor::new("test_2", None);
177        ext.verify_no_secrets_in_output("fn main() { println!(\"hello\"); }");
178        let proof = ext.finalize();
179        assert_eq!(proof.summary.passed, 1);
180        assert_eq!(proof.summary.failed, 0);
181    }
182
183    #[test]
184    fn signatures_preserved_check() {
185        let mut ext = ClaimExtractor::new("test_3", None);
186        let original = vec!["fn main".to_string(), "pub fn process".to_string()];
187        let compressed = vec![
188            "fn main() { ... }".to_string(),
189            "pub fn process(data: &[u8]) -> Result<(), Error>".to_string(),
190        ];
191        ext.verify_signatures_preserved(&original, &compressed);
192        let proof = ext.finalize();
193        assert_eq!(proof.summary.passed, 1);
194    }
195
196    #[test]
197    fn missing_signatures_detected() {
198        let mut ext = ClaimExtractor::new("test_4", None);
199        let original = vec!["fn main()".to_string(), "pub fn gone()".to_string()];
200        let compressed = vec!["fn main() { ... }".to_string()];
201        ext.verify_signatures_preserved(&original, &compressed);
202        let proof = ext.finalize();
203        assert_eq!(proof.summary.failed, 1);
204    }
205
206    #[test]
207    fn lean_proof_integration() {
208        let mut ext = ClaimExtractor::new("test_5", None);
209        ext.add_lean_proof(
210            "pathjail_no_escape",
211            "PathJail prevents access outside root",
212            ClaimKind::PathjailCompliance,
213            "LeanCtxProofs.Policy.PathJail.jail_no_escape",
214        );
215        let proof = ext.finalize();
216        assert_eq!(proof.summary.proved, 1);
217        assert!(proof.claims[0].lean_theorem.is_some());
218    }
219
220    #[test]
221    fn combined_extraction_computes_quality() {
222        let mut ext = ClaimExtractor::new("test_6", None);
223        ext.verify_no_secrets_in_output("clean code");
224        ext.add_lean_proof(
225            "excluded_never_rendered",
226            "Excluded items never in output",
227            ClaimKind::CompressionInvariant,
228            "LeanCtxProofs.Policy.ContextGovernance.excluded_items_never_rendered",
229        );
230        let proof = ext.finalize();
231        assert_eq!(
232            proof.quality_level,
233            super::super::context_proof_v2::QualityLevel::FormallyVerified
234        );
235    }
236
237    #[test]
238    fn detects_github_pat() {
239        let mut ext = ClaimExtractor::new("test_gh", None);
240        ext.verify_no_secrets_in_output("token = ghp_1234567890abcdef");
241        let proof = ext.finalize();
242        assert_eq!(proof.summary.failed, 1);
243    }
244
245    #[test]
246    fn detects_gitlab_pat() {
247        let mut ext = ClaimExtractor::new("test_gl", None);
248        ext.verify_no_secrets_in_output("glpat-xxxxxxxxxxxxxxxxxxxx");
249        let proof = ext.finalize();
250        assert_eq!(proof.summary.failed, 1);
251    }
252
253    #[test]
254    fn detects_pem_private_key() {
255        let mut ext = ClaimExtractor::new("test_pem", None);
256        ext.verify_no_secrets_in_output("-----BEGIN RSA PRIVATE KEY-----");
257        let proof = ext.finalize();
258        assert_eq!(proof.summary.failed, 1);
259    }
260
261    #[test]
262    fn empty_signatures_passes() {
263        let mut ext = ClaimExtractor::new("test_empty", None);
264        ext.verify_signatures_preserved(&[], &[]);
265        let proof = ext.finalize();
266        assert_eq!(proof.summary.passed, 1);
267        assert_eq!(proof.summary.failed, 0);
268    }
269
270    #[test]
271    fn empty_imports_passes() {
272        let mut ext = ClaimExtractor::new("test_imp", None);
273        ext.verify_imports_preserved(&[], "some content");
274        let proof = ext.finalize();
275        assert_eq!(proof.summary.passed, 1);
276    }
277
278    #[test]
279    fn finalize_returns_correct_run_id() {
280        let ext = ClaimExtractor::new("my_run_42", Some("sess_7"));
281        let proof = ext.finalize();
282        assert_eq!(proof.run_id, "my_run_42");
283        assert_eq!(proof.session_id, Some("sess_7".to_string()));
284    }
285
286    #[test]
287    fn multiple_secret_patterns_all_detected() {
288        let mut ext = ClaimExtractor::new("test_multi", None);
289        ext.verify_no_secrets_in_output("AKIAIOSFODNN7 and sk-abc123 and password=foo");
290        let proof = ext.finalize();
291        assert_eq!(proof.summary.failed, 1);
292        assert!(proof.claims[0].text.contains("AKIA"));
293    }
294}
lean_ctx/core/claim_extractor.rs

lean_ctx/core/
claim_extractor.rs
