lean_ctx/tools/
ctx_proof.rs1use 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(°radation_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 {
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("&"),
224 '<' => out.push_str("<"),
225 '>' => out.push_str(">"),
226 '"' => out.push_str("""),
227 '\'' => out.push_str("'"),
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}