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//! Every claim is checked at runtime by the verifier it names. The schema
9//! has no "formally verified" level: nothing in the runtime checks a proof
10//! artifact, so no claim may report one (#1914).
11//!
12//! Design based on:
13//!   - Amazon Cedar VGD (arXiv:2407.01688)
14//!   - VERGE neurosymbolic verification (arXiv:2601.20055)
15
16use serde::{Deserialize, Serialize};
17
18#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
19#[serde(rename_all = "snake_case")]
20pub enum ClaimKind {
21    PathValidity,
22    ApiInvariant,
23    SecretPolicy,
24    TestResult,
25    TypeCheck,
26    ImportPreservation,
27    ScopeCompliance,
28    PathjailCompliance,
29    CompressionInvariant,
30    HandoffValidity,
31    Custom,
32}
33
34#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
35#[serde(rename_all = "snake_case")]
36pub enum VerifierKind {
37    Deterministic,
38    Ast,
39    PathPolicy,
40    Test,
41    TypeChecker,
42    StaticAnalysis,
43    Heuristic,
44    Unverifiable,
45}
46
47#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
48#[serde(rename_all = "snake_case")]
49pub enum ClaimStatus {
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_checked")]
65    PolicyChecked = 3,
66}
67
68#[derive(Debug, Clone, Serialize, Deserialize)]
69pub struct Claim {
70    pub id: String,
71    pub text: String,
72    pub kind: ClaimKind,
73    pub verifier: VerifierKind,
74    pub status: ClaimStatus,
75    #[serde(skip_serializing_if = "Option::is_none")]
76    pub evidence_ref: Option<String>,
77}
78
79#[derive(Debug, Clone, Serialize, Deserialize)]
80pub struct ContextProofV2 {
81    pub proof_version: String,
82    pub run_id: String,
83    pub created_at: String,
84    pub lean_ctx_version: String,
85    #[serde(skip_serializing_if = "Option::is_none")]
86    pub session_id: Option<String>,
87    pub quality_level: QualityLevel,
88    pub claims: Vec<Claim>,
89    pub summary: ProofSummary,
90}
91
92#[derive(Debug, Clone, Serialize, Deserialize)]
93pub struct ProofSummary {
94    pub total_claims: usize,
95    pub passed: usize,
96    pub failed: usize,
97    pub skipped: usize,
98    pub unverified: usize,
99}
100
101impl ContextProofV2 {
102    pub fn new(run_id: String, session_id: Option<String>) -> Self {
103        Self {
104            proof_version: "ContextProofV2".to_string(),
105            run_id,
106            created_at: chrono::Utc::now().to_rfc3339(),
107            lean_ctx_version: env!("CARGO_PKG_VERSION").to_string(),
108            session_id,
109            quality_level: QualityLevel::Provenance,
110            claims: Vec::new(),
111            summary: ProofSummary::empty(),
112        }
113    }
114
115    pub fn add_claim(&mut self, claim: Claim) {
116        self.claims.push(claim);
117        self.recompute();
118    }
119
120    pub fn recompute(&mut self) {
121        let mut passed = 0;
122        let mut failed = 0;
123        let mut skipped = 0;
124        let mut unverified = 0;
125
126        for c in &self.claims {
127            match c.status {
128                ClaimStatus::Passed => passed += 1,
129                ClaimStatus::Failed => failed += 1,
130                ClaimStatus::Skipped => skipped += 1,
131                ClaimStatus::Unverified => unverified += 1,
132            }
133        }
134
135        self.summary = ProofSummary {
136            total_claims: self.claims.len(),
137            passed,
138            failed,
139            skipped,
140            unverified,
141        };
142
143        self.quality_level = if failed > 0 {
144            QualityLevel::Provenance
145        } else if self.claims.iter().any(|c| {
146            c.kind == ClaimKind::ScopeCompliance || c.kind == ClaimKind::PathjailCompliance
147        }) {
148            QualityLevel::PolicyChecked
149        } else if self
150            .claims
151            .iter()
152            .any(|c| c.kind == ClaimKind::TestResult && c.status == ClaimStatus::Passed)
153        {
154            QualityLevel::Tested
155        } else if self
156            .claims
157            .iter()
158            .all(|c| c.status == ClaimStatus::Passed || c.status == ClaimStatus::Skipped)
159        {
160            QualityLevel::Deterministic
161        } else {
162            QualityLevel::Provenance
163        };
164    }
165}
166
167impl ProofSummary {
168    pub fn empty() -> Self {
169        Self {
170            total_claims: 0,
171            passed: 0,
172            failed: 0,
173            skipped: 0,
174            unverified: 0,
175        }
176    }
177}
178
179pub fn deterministic_claim(id: &str, text: &str, passed: bool) -> Claim {
180    Claim {
181        id: id.to_string(),
182        text: text.to_string(),
183        kind: ClaimKind::PathValidity,
184        verifier: VerifierKind::Deterministic,
185        status: if passed {
186            ClaimStatus::Passed
187        } else {
188            ClaimStatus::Failed
189        },
190        evidence_ref: None,
191    }
192}
193
194pub fn policy_claim(id: &str, text: &str, kind: ClaimKind, passed: bool) -> Claim {
195    Claim {
196        id: id.to_string(),
197        text: text.to_string(),
198        kind,
199        verifier: VerifierKind::PathPolicy,
200        status: if passed {
201            ClaimStatus::Passed
202        } else {
203            ClaimStatus::Failed
204        },
205        evidence_ref: None,
206    }
207}
208
209#[cfg(test)]
210pub mod tests {
211    use super::*;
212
213    #[test]
214    fn new_proof_starts_at_provenance() {
215        let proof = ContextProofV2::new("run_1".into(), None);
216        assert_eq!(proof.quality_level, QualityLevel::Provenance);
217        assert_eq!(proof.summary.total_claims, 0);
218    }
219
220    #[test]
221    fn adding_deterministic_claims_reaches_level_1() {
222        let mut proof = ContextProofV2::new("run_2".into(), None);
223        proof.add_claim(deterministic_claim("c1", "paths valid", true));
224        proof.add_claim(deterministic_claim("c2", "imports valid", true));
225        assert_eq!(proof.quality_level, QualityLevel::Deterministic);
226        assert_eq!(proof.summary.passed, 2);
227    }
228
229    #[test]
230    fn failed_claim_drops_to_provenance() {
231        let mut proof = ContextProofV2::new("run_3".into(), None);
232        proof.add_claim(deterministic_claim("c1", "paths valid", true));
233        proof.add_claim(deterministic_claim("c2", "imports broken", false));
234        assert_eq!(proof.quality_level, QualityLevel::Provenance);
235        assert_eq!(proof.summary.failed, 1);
236    }
237
238    #[test]
239    fn policy_claims_reach_level_3() {
240        let mut proof = ContextProofV2::new("run_5".into(), None);
241        proof.add_claim(policy_claim(
242            "c1",
243            "pathjail no escape",
244            ClaimKind::PathjailCompliance,
245            true,
246        ));
247        proof.add_claim(policy_claim(
248            "c2",
249            "scope isolation",
250            ClaimKind::ScopeCompliance,
251            true,
252        ));
253        assert_eq!(proof.quality_level, QualityLevel::PolicyChecked);
254    }
255
256    #[test]
257    fn highest_level_is_a_runtime_policy_check() {
258        let json = serde_json::to_string(&QualityLevel::PolicyChecked).unwrap();
259        assert_eq!(json, "\"3_policy_checked\"");
260        assert!(
261            serde_json::from_str::<QualityLevel>("\"4_formally_verified\"").is_err(),
262            "no claim is checked against a proof artifact, so no level may say so"
263        );
264        assert!(serde_json::from_str::<ClaimStatus>("\"proved\"").is_err());
265    }
266
267    #[test]
268    fn serialization_roundtrip() {
269        let mut proof = ContextProofV2::new("run_6".into(), Some("sess_1".into()));
270        proof.add_claim(policy_claim(
271            "api_surface_preserved",
272            "API preserved",
273            ClaimKind::ApiInvariant,
274            true,
275        ));
276        let json = serde_json::to_string_pretty(&proof).unwrap();
277        assert!(json.contains("ContextProofV2"));
278        assert!(json.contains("api_surface_preserved"));
279        let deserialized: ContextProofV2 = serde_json::from_str(&json).unwrap();
280        assert_eq!(deserialized.claims.len(), 1);
281    }
282
283    #[test]
284    fn quality_level_ordering() {
285        assert!(QualityLevel::Provenance < QualityLevel::Deterministic);
286        assert!(QualityLevel::Deterministic < QualityLevel::Tested);
287        assert!(QualityLevel::Tested < QualityLevel::PolicyChecked);
288    }
289
290    #[test]
291    fn claim_status_ordering() {
292        assert!(ClaimStatus::Passed < ClaimStatus::Failed);
293        assert!(ClaimStatus::Failed < ClaimStatus::Skipped);
294        assert!(ClaimStatus::Skipped < ClaimStatus::Unverified);
295    }
296
297    #[test]
298    fn empty_proof_summary_all_zeros() {
299        let s = ProofSummary::empty();
300        assert_eq!(s.total_claims, 0);
301        assert_eq!(s.passed, 0);
302        assert_eq!(s.failed, 0);
303        assert_eq!(s.skipped, 0);
304        assert_eq!(s.unverified, 0);
305    }
306
307    #[test]
308    fn skipped_claims_dont_trigger_failure() {
309        let mut proof = ContextProofV2::new("run_skip".into(), None);
310        proof.add_claim(Claim {
311            id: "c1".into(),
312            text: "skipped check".into(),
313            kind: ClaimKind::TestResult,
314            verifier: VerifierKind::Test,
315            status: ClaimStatus::Skipped,
316            evidence_ref: None,
317        });
318        assert_eq!(proof.summary.skipped, 1);
319        assert_eq!(proof.summary.failed, 0);
320        assert_ne!(proof.quality_level, QualityLevel::Provenance);
321    }
322
323    #[test]
324    fn unverified_claims_tracked() {
325        let mut proof = ContextProofV2::new("run_unv".into(), None);
326        proof.add_claim(Claim {
327            id: "c1".into(),
328            text: "unverified".into(),
329            kind: ClaimKind::Custom,
330            verifier: VerifierKind::Unverifiable,
331            status: ClaimStatus::Unverified,
332            evidence_ref: None,
333        });
334        assert_eq!(proof.summary.unverified, 1);
335    }
336}
lean_ctx/core/context_proof_v2.rs

lean_ctx/core/
context_proof_v2.rs
