Skip to main content

lean_ctx/tools/
ctx_proof.rs

1use std::path::Path;
2
3use crate::core::context_ir::{write_project_context_ir, ContextIrV1};
4use crate::core::context_proof::{collect_v1, write_project_proof, ProofOptions, ProofSources};
5use crate::core::degradation_policy::{evaluate_v1_for_tool, write_project_degradation_policy};
6
7pub fn handle_export(
8    project_root: &str,
9    format: Option<&str>,
10    write: bool,
11    filename: Option<&str>,
12    max_evidence: Option<usize>,
13    max_ledger_files: Option<usize>,
14    sources: ProofSources,
15) -> Result<String, String> {
16    let opts = ProofOptions {
17        max_evidence: max_evidence.unwrap_or(50),
18        max_ledger_files: max_ledger_files.unwrap_or(10),
19    };
20    let proof = collect_v1(sources, opts);
21    let ir = ContextIrV1::load();
22
23    let mut out = String::new();
24    let mut written: Option<String> = None;
25    let mut written_ir: Option<String> = None;
26    let mut written_degradation: Option<String> = None;
27    let mut written_autonomy: Option<String> = None;
28    let mut written_architecture_json: Option<String> = None;
29    let mut written_architecture_html: Option<String> = None;
30    if write {
31        let root = Path::new(project_root);
32        let ts = chrono::Utc::now().format("%Y-%m-%d_%H%M%S").to_string();
33        let created_at = chrono::Utc::now().to_rfc3339();
34        let default_proof_name = format!("context-proof-v1_{ts}.json");
35        let ir_name = format!("context-ir-v1_{ts}.json");
36        let degradation_name = format!("degradation-policy-v1_{ts}.json");
37        let autonomy_name = format!("autonomy-drivers-v1_{ts}.json");
38        let architecture_json_name = format!("architecture-overview-v1_{ts}.json");
39        let architecture_html_name = format!("architecture-overview-v1_{ts}.html");
40        let proof_name = filename.unwrap_or(default_proof_name.as_str());
41
42        let path = write_project_proof(root, &proof, Some(proof_name))?;
43        written = Some(path.to_string_lossy().to_string());
44
45        let ir_path = write_project_context_ir(root, &ir, Some(&ir_name))?;
46        written_ir = Some(ir_path.to_string_lossy().to_string());
47
48        let policy = evaluate_v1_for_tool("ctx_proof", Some(&created_at));
49        let policy_path = write_project_degradation_policy(root, &policy, Some(&degradation_name))?;
50        written_degradation = Some(policy_path.to_string_lossy().to_string());
51
52        {
53            let ts = chrono::Utc::now();
54            let mut ledger = crate::core::evidence_ledger::EvidenceLedgerV1::load();
55            let _ = ledger.record_artifact_file("proof:context-proof-v1", path.as_path(), ts);
56            let _ = ledger.record_artifact_file("proof:context-ir-v1", ir_path.as_path(), ts);
57            let _ = ledger.record_artifact_file(
58                "proof:degradation-policy-v1",
59                policy_path.as_path(),
60                ts,
61            );
62            let _ = ledger.save();
63        }
64
65        let autonomy = crate::core::autonomy_drivers::AutonomyDriversV1::load();
66        let autonomy_path = crate::core::autonomy_drivers::write_project_autonomy_drivers_v1(
67            root,
68            &autonomy,
69            Some(&autonomy_name),
70        )?;
71        written_autonomy = Some(autonomy_path.to_string_lossy().to_string());
72
73        {
74            let ts = chrono::Utc::now();
75            let mut ledger = crate::core::evidence_ledger::EvidenceLedgerV1::load();
76            let _ = ledger.record_artifact_file(
77                "proof:autonomy-drivers-v1",
78                autonomy_path.as_path(),
79                ts,
80            );
81            let _ = ledger.save();
82        }
83
84        // Architecture overview proof artifacts (JSON + HTML).
85        // Prefer fresh graph when possible (CI/proof reproducibility).
86        {
87            let status =
88                crate::tools::ctx_impact::handle("status", None, project_root, None, Some("json"));
89            let freshness = serde_json::from_str::<serde_json::Value>(&status)
90                .ok()
91                .and_then(|v| {
92                    v.get("freshness")
93                        .and_then(|f| f.as_str())
94                        .map(std::string::ToString::to_string)
95                })
96                .unwrap_or_else(|| "unknown".to_string());
97            if freshness != "fresh" {
98                let _ = crate::tools::ctx_impact::handle("build", None, project_root, None, None);
99            }
100
101            let arch_json = crate::tools::ctx_architecture::handle(
102                "overview",
103                None,
104                project_root,
105                Some("json"),
106            );
107
108            let proofs_dir = root.join(".lean-ctx").join("proofs");
109            std::fs::create_dir_all(&proofs_dir).map_err(|e| e.to_string())?;
110
111            let json_path = proofs_dir.join(&architecture_json_name);
112            let json_redacted = crate::core::redaction::redact_text(&arch_json);
113            crate::config_io::write_atomic(&json_path, &json_redacted)?;
114            written_architecture_json = Some(json_path.to_string_lossy().to_string());
115
116            let html = render_architecture_overview_html(&arch_json);
117            let html_path = proofs_dir.join(&architecture_html_name);
118            let html_redacted = crate::core::redaction::redact_text(&html);
119            crate::config_io::write_atomic(&html_path, &html_redacted)?;
120            written_architecture_html = Some(html_path.to_string_lossy().to_string());
121
122            let ts = chrono::Utc::now();
123            let mut ledger = crate::core::evidence_ledger::EvidenceLedgerV1::load();
124            let _ = ledger.record_artifact_file(
125                "proof:architecture-overview-v1",
126                json_path.as_path(),
127                ts,
128            );
129            let _ = ledger.record_artifact_file(
130                "proof:architecture-overview-v1-html",
131                html_path.as_path(),
132                ts,
133            );
134            let _ = ledger.save();
135        }
136    }
137
138    match format.unwrap_or("json") {
139        "summary" => {
140            out.push_str("ContextProofV1 exported\n");
141            if let Some(p) = written {
142                out.push_str(&format!("path: {p}\n"));
143            }
144            if let Some(p) = written_ir {
145                out.push_str(&format!("context_ir_path: {p}\n"));
146            }
147            if let Some(p) = written_degradation {
148                out.push_str(&format!("degradation_policy_path: {p}\n"));
149            }
150            if let Some(p) = written_autonomy {
151                out.push_str(&format!("autonomy_drivers_path: {p}\n"));
152            }
153            if let Some(p) = written_architecture_json {
154                out.push_str(&format!("architecture_overview_json_path: {p}\n"));
155            }
156            if let Some(p) = written_architecture_html {
157                out.push_str(&format!("architecture_overview_html_path: {p}\n"));
158            }
159            out.push_str(&format!("schema_version: {}\n", proof.schema_version));
160            out.push_str(&format!(
161                "project_root_hash: {}\n",
162                proof.project.project_root_hash.clone().unwrap_or_default()
163            ));
164            out.push_str(&format!("role: {}\n", proof.role.name));
165            out.push_str(&format!("profile: {}\n", proof.profile.name));
166            out.push_str(&format!(
167                "context_ir_schema_version: {}\n",
168                ir.schema_version
169            ));
170            out.push_str(&format!("context_ir_items: {}\n", ir.items.len()));
171        }
172        "both" => {
173            if let Some(p) = &written {
174                out.push_str(&format!("[proof_path: {p}]\n\n"));
175            }
176            if let Some(p) = &written_ir {
177                out.push_str(&format!("[context_ir_path: {p}]\n\n"));
178            }
179            if let Some(p) = &written_degradation {
180                out.push_str(&format!("[degradation_policy_path: {p}]\n\n"));
181            }
182            if let Some(p) = &written_autonomy {
183                out.push_str(&format!("[autonomy_drivers_path: {p}]\n\n"));
184            }
185            if let Some(p) = &written_architecture_json {
186                out.push_str(&format!("[architecture_overview_json_path: {p}]\n\n"));
187            }
188            if let Some(p) = &written_architecture_html {
189                out.push_str(&format!("[architecture_overview_html_path: {p}]\n\n"));
190            }
191            out.push_str(&serde_json::to_string_pretty(&proof).map_err(|e| e.to_string())?);
192        }
193        _ => {
194            if let Some(p) = &written {
195                out.push_str(&format!("[proof_path: {p}]\n\n"));
196            }
197            if let Some(p) = &written_ir {
198                out.push_str(&format!("[context_ir_path: {p}]\n\n"));
199            }
200            if let Some(p) = &written_degradation {
201                out.push_str(&format!("[degradation_policy_path: {p}]\n\n"));
202            }
203            if let Some(p) = &written_autonomy {
204                out.push_str(&format!("[autonomy_drivers_path: {p}]\n\n"));
205            }
206            if let Some(p) = &written_architecture_json {
207                out.push_str(&format!("[architecture_overview_json_path: {p}]\n\n"));
208            }
209            if let Some(p) = &written_architecture_html {
210                out.push_str(&format!("[architecture_overview_html_path: {p}]\n\n"));
211            }
212            out.push_str(&serde_json::to_string_pretty(&proof).map_err(|e| e.to_string())?);
213        }
214    }
215
216    Ok(out)
217}
218
219fn escape_html(s: &str) -> String {
220    let mut out = String::with_capacity(s.len());
221    for ch in s.chars() {
222        match ch {
223            '&' => out.push_str("&amp;"),
224            '<' => out.push_str("&lt;"),
225            '>' => out.push_str("&gt;"),
226            '"' => out.push_str("&quot;"),
227            '\'' => out.push_str("&#39;"),
228            _ => out.push(ch),
229        }
230    }
231    out
232}
233
234fn render_architecture_overview_html(json_payload: &str) -> String {
235    let escaped = escape_html(json_payload);
236    format!(
237        r#"<!doctype html>
238<html lang="en">
239<head>
240  <meta charset="utf-8" />
241  <meta name="viewport" content="width=device-width, initial-scale=1" />
242  <title>LeanCTX — Architecture Overview</title>
243  <style>
244    :root {{ color-scheme: light dark; }}
245    body {{ font-family: ui-sans-serif, system-ui, -apple-system, Segoe UI, Roboto, Arial, sans-serif; margin: 24px; }}
246    h1 {{ margin: 0 0 12px 0; }}
247    p  {{ margin: 0 0 18px 0; opacity: 0.8; }}
248    pre {{ padding: 16px; border-radius: 10px; overflow: auto; }}
249  </style>
250</head>
251<body>
252  <h1>Architecture Overview (JSON)</h1>
253  <p>Generated by LeanCTX proof export. Content is redacted-by-default for CI safety.</p>
254  <pre>{escaped}</pre>
255</body>
256</html>"#
257    )
258}