lean_ctx/core/
context_proof_v2.rs

1//! ContextProofV2 — Claim-based verification schema.
2//!
3//! Extends ContextProofV1 with structured claims that decompose LLM
4//! output verification into individually verifiable assertions. Each
5//! claim is routed to the appropriate verifier and tagged with its
6//! verification status and evidence.
7//!
8//! Design based on:
9//!   - Amazon Cedar VGD (arXiv:2407.01688)
10//!   - VERGE neurosymbolic verification (arXiv:2601.20055)
11//!   - VeriGuard formal safety (arXiv:2510.05156)
12
13use serde::{Deserialize, Serialize};
14
15#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
16#[serde(rename_all = "snake_case")]
17pub enum ClaimKind {
18    PathValidity,
19    ApiInvariant,
20    SecretPolicy,
21    TestResult,
22    TypeCheck,
23    ImportPreservation,
24    BudgetCompliance,
25    ScopeCompliance,
26    PathjailCompliance,
27    CompressionInvariant,
28    HandoffValidity,
29    Custom,
30}
31
32#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
33#[serde(rename_all = "snake_case")]
34pub enum VerifierKind {
35    Deterministic,
36    Ast,
37    PathPolicy,
38    Test,
39    TypeChecker,
40    LeanProof,
41    StaticAnalysis,
42    Heuristic,
43    Unverifiable,
44}
45
46#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
47#[serde(rename_all = "snake_case")]
48pub enum ClaimStatus {
49    Proved,
50    Passed,
51    Failed,
52    Skipped,
53    Unverified,
54}
55
56#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
57pub enum QualityLevel {
58    #[serde(rename = "0_provenance")]
59    Provenance = 0,
60    #[serde(rename = "1_deterministic")]
61    Deterministic = 1,
62    #[serde(rename = "2_tested")]
63    Tested = 2,
64    #[serde(rename = "3_policy_proved")]
65    PolicyProved = 3,
66    #[serde(rename = "4_formally_verified")]
67    FormallyVerified = 4,
68}
69
70#[derive(Debug, Clone, Serialize, Deserialize)]
71pub struct Claim {
72    pub id: String,
73    pub text: String,
74    pub kind: ClaimKind,
75    pub verifier: VerifierKind,
76    pub status: ClaimStatus,
77    #[serde(skip_serializing_if = "Option::is_none")]
78    pub evidence_ref: Option<String>,
79    #[serde(skip_serializing_if = "Option::is_none")]
80    pub lean_theorem: Option<String>,
81    #[serde(skip_serializing_if = "Option::is_none")]
82    pub lean_axioms: Option<Vec<String>>,
83}
84
85#[derive(Debug, Clone, Serialize, Deserialize)]
86pub struct ContextProofV2 {
87    pub proof_version: String,
88    pub run_id: String,
89    pub created_at: String,
90    pub lean_ctx_version: String,
91    #[serde(skip_serializing_if = "Option::is_none")]
92    pub session_id: Option<String>,
93    pub quality_level: QualityLevel,
94    pub claims: Vec<Claim>,
95    pub summary: ProofSummary,
96}
97
98#[derive(Debug, Clone, Serialize, Deserialize)]
99pub struct ProofSummary {
100    pub total_claims: usize,
101    pub proved: usize,
102    pub passed: usize,
103    pub failed: usize,
104    pub skipped: usize,
105    pub unverified: usize,
106}
107
108impl ContextProofV2 {
109    pub fn new(run_id: String, session_id: Option<String>) -> Self {
110        Self {
111            proof_version: "ContextProofV2".to_string(),
112            run_id,
113            created_at: chrono::Utc::now().to_rfc3339(),
114            lean_ctx_version: env!("CARGO_PKG_VERSION").to_string(),
115            session_id,
116            quality_level: QualityLevel::Provenance,
117            claims: Vec::new(),
118            summary: ProofSummary::empty(),
119        }
120    }
121
122    pub fn add_claim(&mut self, claim: Claim) {
123        self.claims.push(claim);
124        self.recompute();
125    }
126
127    pub fn recompute(&mut self) {
128        let mut proved = 0;
129        let mut passed = 0;
130        let mut failed = 0;
131        let mut skipped = 0;
132        let mut unverified = 0;
133
134        for c in &self.claims {
135            match c.status {
136                ClaimStatus::Proved => proved += 1,
137                ClaimStatus::Passed => passed += 1,
138                ClaimStatus::Failed => failed += 1,
139                ClaimStatus::Skipped => skipped += 1,
140                ClaimStatus::Unverified => unverified += 1,
141            }
142        }
143
144        self.summary = ProofSummary {
145            total_claims: self.claims.len(),
146            proved,
147            passed,
148            failed,
149            skipped,
150            unverified,
151        };
152
153        self.quality_level = if failed > 0 {
154            QualityLevel::Provenance
155        } else if proved > 0 {
156            QualityLevel::FormallyVerified
157        } else if self.claims.iter().any(|c| {
158            c.kind == ClaimKind::ScopeCompliance
159                || c.kind == ClaimKind::PathjailCompliance
160                || c.kind == ClaimKind::BudgetCompliance
161        }) && self.claims.iter().all(|c| c.status != ClaimStatus::Failed)
162        {
163            QualityLevel::PolicyProved
164        } else if self
165            .claims
166            .iter()
167            .any(|c| c.kind == ClaimKind::TestResult && c.status == ClaimStatus::Passed)
168        {
169            QualityLevel::Tested
170        } else if self
171            .claims
172            .iter()
173            .all(|c| c.status == ClaimStatus::Passed || c.status == ClaimStatus::Skipped)
174        {
175            QualityLevel::Deterministic
176        } else {
177            QualityLevel::Provenance
178        };
179    }
180}
181
182impl ProofSummary {
183    pub fn empty() -> Self {
184        Self {
185            total_claims: 0,
186            proved: 0,
187            passed: 0,
188            failed: 0,
189            skipped: 0,
190            unverified: 0,
191        }
192    }
193}
194
195pub fn deterministic_claim(id: &str, text: &str, passed: bool) -> Claim {
196    Claim {
197        id: id.to_string(),
198        text: text.to_string(),
199        kind: ClaimKind::PathValidity,
200        verifier: VerifierKind::Deterministic,
201        status: if passed {
202            ClaimStatus::Passed
203        } else {
204            ClaimStatus::Failed
205        },
206        evidence_ref: None,
207        lean_theorem: None,
208        lean_axioms: None,
209    }
210}
211
212pub fn policy_claim(id: &str, text: &str, kind: ClaimKind, passed: bool) -> Claim {
213    Claim {
214        id: id.to_string(),
215        text: text.to_string(),
216        kind,
217        verifier: VerifierKind::PathPolicy,
218        status: if passed {
219            ClaimStatus::Passed
220        } else {
221            ClaimStatus::Failed
222        },
223        evidence_ref: None,
224        lean_theorem: None,
225        lean_axioms: None,
226    }
227}
228
229pub fn lean_proved_claim(id: &str, text: &str, kind: ClaimKind, theorem: &str) -> Claim {
230    Claim {
231        id: id.to_string(),
232        text: text.to_string(),
233        kind,
234        verifier: VerifierKind::LeanProof,
235        status: ClaimStatus::Proved,
236        evidence_ref: None,
237        lean_theorem: Some(theorem.to_string()),
238        lean_axioms: Some(vec![
239            "propext".to_string(),
240            "Classical.choice".to_string(),
241            "Quot.sound".to_string(),
242        ]),
243    }
244}
245
246#[cfg(test)]
247mod tests {
248    use super::*;
249
250    #[test]
251    fn new_proof_starts_at_provenance() {
252        let proof = ContextProofV2::new("run_1".into(), None);
253        assert_eq!(proof.quality_level, QualityLevel::Provenance);
254        assert_eq!(proof.summary.total_claims, 0);
255    }
256
257    #[test]
258    fn adding_deterministic_claims_reaches_level_1() {
259        let mut proof = ContextProofV2::new("run_2".into(), None);
260        proof.add_claim(deterministic_claim("c1", "paths valid", true));
261        proof.add_claim(deterministic_claim("c2", "imports valid", true));
262        assert_eq!(proof.quality_level, QualityLevel::Deterministic);
263        assert_eq!(proof.summary.passed, 2);
264    }
265
266    #[test]
267    fn failed_claim_drops_to_provenance() {
268        let mut proof = ContextProofV2::new("run_3".into(), None);
269        proof.add_claim(deterministic_claim("c1", "paths valid", true));
270        proof.add_claim(deterministic_claim("c2", "imports broken", false));
271        assert_eq!(proof.quality_level, QualityLevel::Provenance);
272        assert_eq!(proof.summary.failed, 1);
273    }
274
275    #[test]
276    fn lean_proof_reaches_level_4() {
277        let mut proof = ContextProofV2::new("run_4".into(), None);
278        proof.add_claim(deterministic_claim("c1", "paths valid", true));
279        proof.add_claim(lean_proved_claim(
280            "c2",
281            "excluded items never rendered",
282            ClaimKind::CompressionInvariant,
283            "excluded_items_never_rendered",
284        ));
285        assert_eq!(proof.quality_level, QualityLevel::FormallyVerified);
286        assert_eq!(proof.summary.proved, 1);
287        assert_eq!(proof.summary.passed, 1);
288    }
289
290    #[test]
291    fn policy_claims_reach_level_3() {
292        let mut proof = ContextProofV2::new("run_5".into(), None);
293        proof.add_claim(policy_claim(
294            "c1",
295            "pathjail no escape",
296            ClaimKind::PathjailCompliance,
297            true,
298        ));
299        proof.add_claim(policy_claim(
300            "c2",
301            "scope isolation",
302            ClaimKind::ScopeCompliance,
303            true,
304        ));
305        assert_eq!(proof.quality_level, QualityLevel::PolicyProved);
306    }
307
308    #[test]
309    fn serialization_roundtrip() {
310        let mut proof = ContextProofV2::new("run_6".into(), Some("sess_1".into()));
311        proof.add_claim(lean_proved_claim(
312            "c1",
313            "API preserved",
314            ClaimKind::ApiInvariant,
315            "api_surface_preserved",
316        ));
317        let json = serde_json::to_string_pretty(&proof).unwrap();
318        assert!(json.contains("ContextProofV2"));
319        assert!(json.contains("api_surface_preserved"));
320        let deserialized: ContextProofV2 = serde_json::from_str(&json).unwrap();
321        assert_eq!(deserialized.claims.len(), 1);
322    }
323
324    #[test]
325    fn quality_level_ordering() {
326        assert!(QualityLevel::Provenance < QualityLevel::Deterministic);
327        assert!(QualityLevel::Deterministic < QualityLevel::Tested);
328        assert!(QualityLevel::Tested < QualityLevel::PolicyProved);
329        assert!(QualityLevel::PolicyProved < QualityLevel::FormallyVerified);
330    }
331
332    #[test]
333    fn claim_status_ordering() {
334        assert!(ClaimStatus::Proved < ClaimStatus::Passed);
335        assert!(ClaimStatus::Passed < ClaimStatus::Failed);
336        assert!(ClaimStatus::Failed < ClaimStatus::Skipped);
337        assert!(ClaimStatus::Skipped < ClaimStatus::Unverified);
338    }
339
340    #[test]
341    fn empty_proof_summary_all_zeros() {
342        let s = ProofSummary::empty();
343        assert_eq!(s.total_claims, 0);
344        assert_eq!(s.proved, 0);
345        assert_eq!(s.passed, 0);
346        assert_eq!(s.failed, 0);
347        assert_eq!(s.skipped, 0);
348        assert_eq!(s.unverified, 0);
349    }
350
351    #[test]
352    fn lean_axioms_are_standard() {
353        let claim = lean_proved_claim("t", "test", ClaimKind::ApiInvariant, "thm");
354        let axioms = claim.lean_axioms.unwrap();
355        assert_eq!(axioms.len(), 3);
356        assert!(axioms.contains(&"propext".to_string()));
357        assert!(axioms.contains(&"Classical.choice".to_string()));
358        assert!(axioms.contains(&"Quot.sound".to_string()));
359    }
360
361    #[test]
362    fn skipped_claims_dont_trigger_failure() {
363        let mut proof = ContextProofV2::new("run_skip".into(), None);
364        proof.add_claim(Claim {
365            id: "c1".into(),
366            text: "skipped check".into(),
367            kind: ClaimKind::TestResult,
368            verifier: VerifierKind::Test,
369            status: ClaimStatus::Skipped,
370            evidence_ref: None,
371            lean_theorem: None,
372            lean_axioms: None,
373        });
374        assert_eq!(proof.summary.skipped, 1);
375        assert_eq!(proof.summary.failed, 0);
376        assert_ne!(proof.quality_level, QualityLevel::Provenance);
377    }
378
379    #[test]
380    fn unverified_claims_tracked() {
381        let mut proof = ContextProofV2::new("run_unv".into(), None);
382        proof.add_claim(Claim {
383            id: "c1".into(),
384            text: "unverified".into(),
385            kind: ClaimKind::Custom,
386            verifier: VerifierKind::Unverifiable,
387            status: ClaimStatus::Unverified,
388            evidence_ref: None,
389            lean_theorem: None,
390            lean_axioms: None,
391        });
392        assert_eq!(proof.summary.unverified, 1);
393    }
394}
lean_ctx/core/context_proof_v2.rs

lean_ctx/core/
context_proof_v2.rs
