lean_ctx/core/
context_proof.rs

1use chrono::TimeZone;
2use serde::Serialize;
3use std::path::{Path, PathBuf};
4use std::sync::atomic::{AtomicU64, Ordering};
5
6static PROOFS_COLLECTED: AtomicU64 = AtomicU64::new(0);
7static PROOFS_WRITTEN: AtomicU64 = AtomicU64::new(0);
8static LAST_WRITTEN_UNIX_MS: AtomicU64 = AtomicU64::new(0);
9
10#[derive(Debug, Clone, Serialize)]
11pub struct ProofStatsSnapshot {
12    pub collected: u64,
13    pub written: u64,
14    pub last_written_at: Option<String>,
15}
16
17pub(crate) fn proof_stats_snapshot() -> ProofStatsSnapshot {
18    let collected = PROOFS_COLLECTED.load(Ordering::Relaxed);
19    let written = PROOFS_WRITTEN.load(Ordering::Relaxed);
20    let last_ms = LAST_WRITTEN_UNIX_MS.load(Ordering::Relaxed);
21    let last_written_at = if last_ms == 0 {
22        None
23    } else {
24        chrono::Utc
25            .timestamp_millis_opt(last_ms as i64)
26            .single()
27            .map(|t| t.to_rfc3339())
28    };
29    ProofStatsSnapshot {
30        collected,
31        written,
32        last_written_at,
33    }
34}
35
36#[derive(Debug, Clone, Serialize)]
37pub struct ContextProofV1 {
38    pub schema_version: u32,
39    pub created_at: String,
40    pub lean_ctx_version: String,
41    pub session_id: Option<String>,
42    pub project: ProjectIdentity,
43    pub role: RoleIdentity,
44    pub profile: ProfileIdentity,
45    /// Kept for the proof's wire shape. Per-layer metrics are not collected,
46    /// so this is `runs: 0` unless a legacy `pipeline_stats.json` exists.
47    pub pipeline: crate::core::pipeline::PipelineStats,
48    pub verification: crate::core::output_verification::VerificationSnapshot,
49    pub ledger: LedgerSummary,
50    pub evidence: Vec<EvidenceReceipt>,
51}
52
53#[derive(Debug, Clone, Serialize)]
54pub struct ProjectIdentity {
55    pub project_root_hash: Option<String>,
56    pub project_identity_hash: Option<String>,
57}
58
59#[derive(Debug, Clone, Serialize)]
60pub struct RoleIdentity {
61    pub name: String,
62    /// BLAKE3 hex; the serialized name keeps its historical `_md5` suffix.
63    #[serde(rename = "policy_md5")]
64    pub policy_blake3: String,
65}
66
67#[derive(Debug, Clone, Serialize)]
68pub struct ProfileIdentity {
69    pub name: String,
70    /// BLAKE3 hex; the serialized name keeps its historical `_md5` suffix.
71    #[serde(rename = "policy_md5")]
72    pub policy_blake3: String,
73}
74
75#[derive(Debug, Clone, Serialize)]
76pub struct LedgerSummary {
77    pub window_size: usize,
78    pub entries: usize,
79    pub total_tokens_sent: usize,
80    pub total_tokens_saved: usize,
81    pub compression_ratio: f64,
82    pub top_files_by_sent_tokens: Vec<LedgerFileSummary>,
83}
84
85#[derive(Debug, Clone, Serialize)]
86pub struct LedgerFileSummary {
87    pub path: String,
88    pub mode: String,
89    pub sent_tokens: usize,
90    pub original_tokens: usize,
91}
92
93#[derive(Debug, Clone, Serialize)]
94pub struct EvidenceReceipt {
95    pub tool: Option<String>,
96    pub input_md5: Option<String>,
97    pub output_md5: Option<String>,
98    pub agent_id: Option<String>,
99    pub client_name: Option<String>,
100    pub timestamp: String,
101}
102
103#[derive(Debug, Clone, Copy, Default)]
104pub struct ProofOptions {
105    pub max_evidence: usize,
106    pub max_ledger_files: usize,
107}
108
109#[derive(Debug, Clone, Default)]
110pub struct ProofSources {
111    pub project_root: Option<String>,
112    pub session: Option<crate::core::session::SessionState>,
113    pub pipeline: Option<crate::core::pipeline::PipelineStats>,
114    pub ledger: Option<crate::core::context_ledger::ContextLedger>,
115}
116
117pub fn collect_v1(sources: ProofSources, opts: ProofOptions) -> ContextProofV1 {
118    PROOFS_COLLECTED.fetch_add(1, Ordering::Relaxed);
119    let created_at = chrono::Utc::now().to_rfc3339();
120
121    let role_name = crate::core::roles::active_role_name();
122    let role = crate::core::roles::active_role();
123
124    let profile_name = crate::core::profiles::active_profile_name();
125    let profile = crate::core::profiles::active_profile();
126
127    let role_policy_blake3 =
128        crate::core::hasher::hash_str(&serde_json::to_string(&role).unwrap_or_default());
129    let profile_policy_blake3 =
130        crate::core::hasher::hash_str(&serde_json::to_string(&profile).unwrap_or_default());
131
132    let project_root = sources.project_root.clone().or_else(|| {
133        sources
134            .session
135            .as_ref()
136            .and_then(|s| s.project_root.clone())
137    });
138
139    let (project_root_hash, project_identity_hash) = if let Some(ref root) = project_root {
140        let root_hash = crate::core::project_hash::hash_project_root(root);
141        let identity = crate::core::project_hash::project_identity(root);
142        let identity_hash = identity.as_deref().map(crate::core::hasher::hash_str);
143        (Some(root_hash), identity_hash)
144    } else {
145        (None, None)
146    };
147
148    let verification = crate::core::output_verification::stats_snapshot();
149
150    let pipeline = sources
151        .pipeline
152        .unwrap_or_else(crate::core::pipeline::PipelineStats::load);
153
154    let ledger = sources
155        .ledger
156        .unwrap_or_else(crate::core::context_ledger::ContextLedger::load);
157
158    let top_files = ledger
159        .files_by_token_cost()
160        .into_iter()
161        .take(opts.max_ledger_files.max(1))
162        .filter_map(|(path, _)| ledger.entries.iter().find(|e| e.path == path).cloned())
163        .map(|e| LedgerFileSummary {
164            path: e.path,
165            mode: e.mode,
166            sent_tokens: e.sent_tokens,
167            original_tokens: e.original_tokens,
168        })
169        .collect::<Vec<_>>();
170
171    let ledger_summary = LedgerSummary {
172        window_size: ledger.window_size,
173        entries: ledger.entries.len(),
174        total_tokens_sent: ledger.total_tokens_sent,
175        total_tokens_saved: ledger.total_tokens_saved,
176        compression_ratio: ledger.compression_ratio(),
177        top_files_by_sent_tokens: top_files,
178    };
179
180    let session = sources.session.or_else(|| {
181        project_root
182            .as_deref()
183            .and_then(crate::core::session::SessionState::load_latest_for_project_root)
184            .or_else(crate::core::session::SessionState::load_latest)
185    });
186
187    let (session_id, evidence) = if let Some(s) = session {
188        let mut receipts = s
189            .evidence
190            .into_iter()
191            .filter(|e| matches!(e.kind, crate::core::session::EvidenceKind::ToolCall))
192            .rev()
193            .take(opts.max_evidence.max(1))
194            .map(|e| EvidenceReceipt {
195                tool: e.tool,
196                input_md5: e.input_md5,
197                output_md5: e.output_md5,
198                agent_id: e.agent_id,
199                client_name: e.client_name,
200                timestamp: e.timestamp.to_rfc3339(),
201            })
202            .collect::<Vec<_>>();
203        receipts.reverse();
204        (Some(s.id), receipts)
205    } else {
206        (None, Vec::new())
207    };
208
209    ContextProofV1 {
210        schema_version: crate::core::contracts::CONTEXT_PROOF_V1_SCHEMA_VERSION,
211        created_at,
212        lean_ctx_version: env!("CARGO_PKG_VERSION").to_string(),
213        session_id,
214        project: ProjectIdentity {
215            project_root_hash,
216            project_identity_hash,
217        },
218        role: RoleIdentity {
219            name: role_name,
220            policy_blake3: role_policy_blake3,
221        },
222        profile: ProfileIdentity {
223            name: profile_name,
224            policy_blake3: profile_policy_blake3,
225        },
226        pipeline,
227        verification,
228        ledger: ledger_summary,
229        evidence,
230    }
231}
232
233/// A checked destination for a proof artifact: `<project>/.lean-ctx/proofs/<name>`.
234///
235/// Every proof-shaped artifact (context proof, context IR, architecture
236/// overview, A2A snapshot, handoff bundle) is written through here.
237/// `.lean-ctx`, `proofs` and the file itself must not be symlinks, and the
238/// write walks the path without following one (see
239/// [`crate::core::pathjail_write`]).
240#[derive(Debug, Clone)]
241pub struct ProofDestination {
242    project_root: PathBuf,
243    rel: PathBuf,
244    path: PathBuf,
245}
246
247impl ProofDestination {
248    /// The path the artifact is written to.
249    pub fn path(&self) -> &Path {
250        &self.path
251    }
252
253    /// Write `content`; refuses (writes nothing) when a component is or
254    /// became a symlink.
255    pub fn write(&self, content: &str) -> Result<PathBuf, String> {
256        crate::core::pathjail_write::write_project_data(
257            &self.project_root,
258            &self.rel,
259            content.as_bytes(),
260        )
261    }
262}
263
264/// The destination for the proof artifact `name` of `project_root`.
265///
266/// `name` comes from tool callers: only a bare file name is accepted
267/// (`Path::join` drops the base for an absolute path, and `..` would walk out
268/// of `proofs/`).
269pub fn proof_destination(project_root: &Path, name: &str) -> Result<ProofDestination, String> {
270    let mut components = Path::new(name).components();
271    match (components.next(), components.next()) {
272        (Some(std::path::Component::Normal(_)), None) => {}
273        _ => return Err(format!("filename must be a plain file name: {name}")),
274    }
275    let rel = Path::new("proofs").join(name);
276    let path = crate::core::pathjail_write::project_data_destination(project_root, &rel)?;
277    Ok(ProofDestination {
278        project_root: project_root.to_path_buf(),
279        rel,
280        path,
281    })
282}
283
284pub fn write_project_proof(
285    project_root: &Path,
286    proof: &ContextProofV1,
287    filename: Option<&str>,
288) -> Result<PathBuf, String> {
289    let ts = chrono::Utc::now().format("%Y-%m-%d_%H%M%S");
290    let name = filename.map_or_else(|| format!("context-proof-v1_{ts}.json"), str::to_string);
291    let destination = proof_destination(project_root, &name)?;
292
293    let json = serde_json::to_string_pretty(proof).map_err(|e| e.to_string())?;
294    // Proof artifacts may be attached to CI logs; always redact (even for admin).
295    let json = crate::core::redaction::redact_text(&json);
296    let path = destination.write(&json)?;
297
298    PROOFS_WRITTEN.fetch_add(1, Ordering::Relaxed);
299    let ms = std::time::SystemTime::now()
300        .duration_since(std::time::SystemTime::UNIX_EPOCH)
301        .map_or(0, |d| d.as_millis() as u64);
302    LAST_WRITTEN_UNIX_MS.store(ms, Ordering::Relaxed);
303
304    Ok(path)
305}
306
307#[cfg(test)]
308mod tests {
309    use super::*;
310
311    #[test]
312    fn proof_has_required_fields() {
313        let proof = collect_v1(
314            ProofSources {
315                project_root: Some(".".to_string()),
316                ..Default::default()
317            },
318            ProofOptions {
319                max_evidence: 5,
320                max_ledger_files: 3,
321            },
322        );
323        let v = serde_json::to_value(&proof).unwrap();
324        assert_eq!(v["schema_version"], 1);
325        assert!(v["created_at"].as_str().unwrap_or_default().contains('T'));
326        assert!(v["lean_ctx_version"].as_str().unwrap_or_default().len() >= 3);
327        // The BLAKE3 policy hashes keep their historical wire name.
328        assert!(v["role"]["policy_md5"].is_string(), "{v}");
329        assert!(v["profile"]["policy_md5"].is_string(), "{v}");
330    }
331
332    #[test]
333    fn write_project_proof_creates_file() {
334        let dir = tempfile::tempdir().unwrap();
335        let proof = collect_v1(
336            ProofSources {
337                project_root: Some(dir.path().to_string_lossy().to_string()),
338                ..Default::default()
339            },
340            ProofOptions {
341                max_evidence: 3,
342                max_ledger_files: 2,
343            },
344        );
345        let path = write_project_proof(dir.path(), &proof, None).unwrap();
346        assert!(path.exists());
347        let content = std::fs::read_to_string(path).unwrap();
348        assert!(content.contains("\"schema_version\": 1"));
349    }
350
351    #[test]
352    fn write_project_proof_rejects_filenames_outside_proofs_dir() {
353        let dir = tempfile::tempdir().unwrap();
354        let project = dir.path().join("proj");
355        std::fs::create_dir_all(&project).unwrap();
356        let proof = collect_v1(
357            ProofSources {
358                project_root: Some(project.to_string_lossy().to_string()),
359                ..Default::default()
360            },
361            ProofOptions {
362                max_evidence: 1,
363                max_ledger_files: 1,
364            },
365        );
366        let outside = dir.path().join("outside.json");
367        let outside_abs = outside.to_string_lossy().to_string();
368        for name in [
369            "../../../outside.json",
370            outside_abs.as_str(),
371            "sub/dir.json",
372            "..",
373            ".",
374            "",
375        ] {
376            assert!(
377                write_project_proof(&project, &proof, Some(name)).is_err(),
378                "filename {name:?} must be rejected"
379            );
380        }
381        assert!(!outside.exists(), "nothing may be written outside proofs/");
382
383        let path = write_project_proof(&project, &proof, Some("named.json")).unwrap();
384        assert_eq!(path.file_name().unwrap(), "named.json");
385        assert!(path.parent().unwrap().ends_with("proofs"));
386    }
387
388    #[cfg(unix)]
389    fn sample_proof(project: &Path) -> ContextProofV1 {
390        collect_v1(
391            ProofSources {
392                project_root: Some(project.to_string_lossy().to_string()),
393                ..Default::default()
394            },
395            ProofOptions {
396                max_evidence: 1,
397                max_ledger_files: 1,
398            },
399        )
400    }
401
402    #[cfg(unix)]
403    #[test]
404    fn write_project_proof_refuses_a_symlinked_proofs_dir() {
405        let dir = tempfile::tempdir().unwrap();
406        let project = dir.path().join("proj");
407        let outside = dir.path().join("outside");
408        std::fs::create_dir_all(project.join(".lean-ctx")).unwrap();
409        std::fs::create_dir_all(&outside).unwrap();
410        std::os::unix::fs::symlink(&outside, project.join(".lean-ctx/proofs")).unwrap();
411        let proof = sample_proof(&project);
412        let err = write_project_proof(&project, &proof, Some("p.json")).unwrap_err();
413        assert!(err.contains("symlink"), "{err}");
414        assert!(!outside.join("p.json").exists());
415    }
416
417    #[cfg(unix)]
418    #[test]
419    fn write_project_proof_refuses_a_symlinked_target_file() {
420        let dir = tempfile::tempdir().unwrap();
421        let project = dir.path().join("proj");
422        std::fs::create_dir_all(project.join(".lean-ctx/proofs")).unwrap();
423        let victim = dir.path().join("victim");
424        std::fs::write(&victim, "keep").unwrap();
425        std::os::unix::fs::symlink(&victim, project.join(".lean-ctx/proofs/p.json")).unwrap();
426        let proof = sample_proof(&project);
427        // The victim lies inside $HOME: the dotfile write-through rule of
428        // config writes must not apply to project data.
429        let _guard = crate::core::data_dir::test_env_lock();
430        let previous = std::env::var_os("HOME");
431        crate::test_env::set_var("HOME", dir.path());
432        let result = write_project_proof(&project, &proof, Some("p.json"));
433        match previous {
434            Some(home) => crate::test_env::set_var("HOME", home),
435            None => crate::test_env::remove_var("HOME"),
436        }
437        assert!(result.is_err());
438        assert_eq!(std::fs::read_to_string(&victim).unwrap(), "keep");
439    }
440
441    #[cfg(unix)]
442    #[test]
443    fn write_project_proof_refuses_a_dangling_data_dir_link() {
444        let dir = tempfile::tempdir().unwrap();
445        let project = dir.path().join("proj");
446        std::fs::create_dir_all(&project).unwrap();
447        let missing = dir.path().join("not-yet");
448        std::os::unix::fs::symlink(&missing, project.join(".lean-ctx")).unwrap();
449        let proof = sample_proof(&project);
450        assert!(write_project_proof(&project, &proof, Some("p.json")).is_err());
451        assert!(
452            !missing.exists(),
453            "a dangling link must not be created through"
454        );
455
456        // A dangling target-file link into $HOME is not created through
457        // either (the dotfile write-through rule of config writes would).
458        let project = dir.path().join("proj2");
459        std::fs::create_dir_all(project.join(".lean-ctx/proofs")).unwrap();
460        let planted = dir.path().join("planted.json");
461        std::os::unix::fs::symlink(&planted, project.join(".lean-ctx/proofs/p.json")).unwrap();
462        let _guard = crate::core::data_dir::test_env_lock();
463        let previous = std::env::var_os("HOME");
464        crate::test_env::set_var("HOME", dir.path());
465        let result = write_project_proof(&project, &proof, Some("p.json"));
466        match previous {
467            Some(home) => crate::test_env::set_var("HOME", home),
468            None => crate::test_env::remove_var("HOME"),
469        }
470        assert!(result.is_err());
471        assert!(
472            !planted.exists(),
473            "a dangling file link must not be created through"
474        );
475    }
476}
lean_ctx/core/context_proof.rs

lean_ctx/core/
context_proof.rs
