1use std::collections::BTreeMap;
9use std::path::Path;
10
11use provable_contracts::graph::dependency_graph;
12use provable_contracts::schema::{parse_contract, Contract};
13use serde_json::Value;
14
15use crate::json_obj::obj;
16
17pub fn run(
19 contract_dir: &Path,
20 config_json: Option<&Path>,
21 output: Option<&Path>,
22) -> Result<(), Box<dyn std::error::Error>> {
23 let mut contracts = Vec::new();
24 load_yaml_recursive(contract_dir, &mut contracts)?;
25 contracts.sort_by(|a, b| a.0.cmp(&b.0));
26
27 if contracts.is_empty() {
28 eprintln!("No contracts found in {}", contract_dir.display());
29 return Ok(());
30 }
31
32 let refs: Vec<(String, &Contract)> = contracts.iter().map(|(s, c)| (s.clone(), c)).collect();
33 let graph = dependency_graph(&refs);
34 let index: BTreeMap<&str, &Contract> = contracts.iter().map(|(s, c)| (s.as_str(), c)).collect();
35
36 let (edges_total, edges_satisfied, edge_details) = verify_composition_edges(&graph, &index);
37
38 let config_proof = config_json.and_then(|cfg| analyze_config(cfg).ok());
39
40 let composition_passed = edges_total > 0 && edges_satisfied == edges_total;
41 let config_passed = config_proof.as_ref().is_none_or(|p| {
42 p.get("all_checks_pass")
43 .and_then(Value::as_bool)
44 .unwrap_or(false)
45 });
46
47 let certificate = build_certificate(
48 &contracts,
49 &graph,
50 &index,
51 edges_total,
52 edges_satisfied,
53 &edge_details,
54 config_proof.as_ref(),
55 composition_passed,
56 config_passed,
57 );
58
59 let json_str = serde_json::to_string_pretty(&certificate)?;
60
61 if let Some(out_path) = output {
62 std::fs::write(out_path, &json_str)?;
63 println!("Certificate written to: {}", out_path.display());
64 } else {
65 println!("{json_str}");
66 }
67
68 print_summary(
69 composition_passed,
70 config_passed,
71 edges_satisfied,
72 edges_total,
73 config_proof.as_ref(),
74 );
75
76 if !composition_passed {
77 std::process::exit(1);
78 }
79
80 Ok(())
81}
82
83fn verify_composition_edges(
84 graph: &provable_contracts::graph::DependencyGraph,
85 index: &BTreeMap<&str, &Contract>,
86) -> (usize, usize, Vec<serde_json::Value>) {
87 let mut edges_total = 0usize;
88 let mut edges_satisfied = 0usize;
89 let mut edge_details = Vec::new();
90
91 for stem in &graph.topo_order {
92 let Some(contract) = index.get(stem.as_str()) else {
93 continue;
94 };
95 for (eq_name, equation) in &contract.equations {
96 let Some(assumes) = &equation.assumes else {
97 continue;
98 };
99 let Some(from_contract) = &assumes.from_contract else {
100 continue;
101 };
102 edges_total += 1;
103 let from_eq = assumes.from_equation.as_deref().unwrap_or("*");
104 let satisfied = check_edge(index, from_contract, assumes.from_equation.as_deref());
105 if satisfied {
106 edges_satisfied += 1;
107 }
108 edge_details.push(obj([
109 ("downstream", Value::from(format!("{stem}.{eq_name}"))),
110 (
111 "upstream",
112 Value::from(format!("{from_contract}.{from_eq}")),
113 ),
114 ("satisfied", Value::from(satisfied)),
115 ]));
116 }
117 }
118
119 (edges_total, edges_satisfied, edge_details)
120}
121
122#[allow(clippy::too_many_arguments)]
123fn build_certificate(
124 contracts: &[(String, Contract)],
125 graph: &provable_contracts::graph::DependencyGraph,
126 index: &BTreeMap<&str, &Contract>,
127 edges_total: usize,
128 edges_satisfied: usize,
129 edge_details: &[serde_json::Value],
130 config_proof: Option<&serde_json::Value>,
131 composition_passed: bool,
132 config_passed: bool,
133) -> serde_json::Value {
134 let with_assumes = contracts
135 .iter()
136 .filter(|(_, c)| c.equations.values().any(|e| e.assumes.is_some()))
137 .count();
138 let with_guarantees = contracts
139 .iter()
140 .filter(|(_, c)| c.equations.values().any(|e| e.guarantees.is_some()))
141 .count();
142
143 obj([
144 ("version", Value::from("1.0.0")),
145 (
146 "tool",
147 Value::from(format!("pv certify v{}", env!("CARGO_PKG_VERSION"))),
148 ),
149 ("timestamp", Value::from(chrono_free_timestamp())),
150 (
151 "contracts",
152 obj([
153 ("total", Value::from(contracts.len())),
154 ("with_assumes", Value::from(with_assumes)),
155 ("with_guarantees", Value::from(with_guarantees)),
156 ("topo_depth", Value::from(graph.topo_order.len())),
157 ("cycles", Value::from(graph.cycles.len())),
158 ]),
159 ),
160 (
161 "composition",
162 obj([
163 ("edges_total", Value::from(edges_total)),
164 ("edges_satisfied", Value::from(edges_satisfied)),
165 (
166 "edges_broken",
167 Value::from(edges_total.saturating_sub(edges_satisfied)),
168 ),
169 ("passed", Value::from(composition_passed)),
170 ("edges", Value::Array(edge_details.to_vec())),
171 ]),
172 ),
173 (
174 "config_analysis",
175 config_proof.cloned().unwrap_or(Value::Null),
176 ),
177 (
178 "proofs",
179 obj([
180 (
181 "format_safety",
182 proof_status(index, "safetensors-format-safety-v1"),
183 ),
184 (
185 "config_algebra",
186 proof_status(index, "model-config-algebra-v1"),
187 ),
188 (
189 "architecture_schema",
190 proof_status(index, "apr-architecture-schema-v1"),
191 ),
192 (
193 "shape_pipeline",
194 proof_status(index, "tensor-shape-flow-v1"),
195 ),
196 ("tensor_names", proof_status(index, "tensor-names-v1")),
197 ]),
198 ),
199 (
200 "certificate_level",
201 Value::from(if composition_passed && config_passed {
202 "L3"
203 } else {
204 "L2"
205 }),
206 ),
207 ("passed", Value::from(composition_passed && config_passed)),
208 ])
209}
210
211fn print_summary(
212 composition_passed: bool,
213 config_passed: bool,
214 edges_satisfied: usize,
215 edges_total: usize,
216 config_proof: Option<&serde_json::Value>,
217) {
218 let icon = if composition_passed && config_passed {
219 "✓"
220 } else {
221 "✗"
222 };
223 eprintln!();
224 eprintln!("pv certify — {icon} {edges_satisfied}/{edges_total} composition edges satisfied",);
225 if let Some(cfg) = config_proof {
226 if let Some(tensors) = cfg.get("expected_tensors") {
227 eprintln!(" Config: {tensors} expected tensors");
228 }
229 }
230 let level = if composition_passed && config_passed {
231 "L3"
232 } else {
233 "L2"
234 };
235 eprintln!(" Certificate level: {level}");
236}
237
238fn check_edge(
239 index: &BTreeMap<&str, &Contract>,
240 from_contract: &str,
241 from_eq: Option<&str>,
242) -> bool {
243 let Some(upstream) = index.get(from_contract) else {
244 return false;
245 };
246 if let Some(eq_name) = from_eq {
247 upstream
248 .equations
249 .get(eq_name)
250 .is_some_and(|eq| eq.guarantees.is_some())
251 } else {
252 upstream
253 .equations
254 .values()
255 .any(|eq| eq.guarantees.is_some())
256 }
257}
258
259fn proof_status(index: &BTreeMap<&str, &Contract>, stem: &str) -> serde_json::Value {
260 if let Some(contract) = index.get(stem) {
261 let eq_count = contract.equations.len();
262 let has_assumes = contract
263 .equations
264 .values()
265 .filter(|e| e.assumes.is_some())
266 .count();
267 let has_guarantees = contract
268 .equations
269 .values()
270 .filter(|e| e.guarantees.is_some())
271 .count();
272 let has_kani = !contract.kani_harnesses.is_empty();
273 let has_lean = contract
274 .equations
275 .values()
276 .any(|e| e.lean_theorem.is_some());
277 obj([
278 ("found", Value::from(true)),
279 ("equations", Value::from(eq_count)),
280 ("with_assumes", Value::from(has_assumes)),
281 ("with_guarantees", Value::from(has_guarantees)),
282 ("has_kani", Value::from(has_kani)),
283 ("has_lean", Value::from(has_lean)),
284 (
285 "verdict",
286 Value::from(if has_kani || has_lean {
287 "PROVEN"
288 } else {
289 "SPECIFIED"
290 }),
291 ),
292 ])
293 } else {
294 obj([
295 ("found", Value::from(false)),
296 ("verdict", Value::from("MISSING")),
297 ])
298 }
299}
300
301pub fn analyze_config(cfg_path: &Path) -> Result<serde_json::Value, Box<dyn std::error::Error>> {
302 let content = std::fs::read_to_string(cfg_path)?;
303 let json: serde_json::Value = serde_json::from_str(&content)?;
304
305 let h = json.get("hidden_size").and_then(Value::as_u64).unwrap_or(0);
306 let l = json
307 .get("num_hidden_layers")
308 .and_then(Value::as_u64)
309 .unwrap_or(0);
310 let nh = json
311 .get("num_attention_heads")
312 .and_then(Value::as_u64)
313 .unwrap_or(0);
314 let nkv = json
315 .get("num_key_value_heads")
316 .and_then(Value::as_u64)
317 .unwrap_or(nh);
318 let v = json.get("vocab_size").and_then(Value::as_u64).unwrap_or(0);
319
320 let head_dim = if nh > 0 { h / nh } else { 0 };
321 let expected_tensors = if l > 0 { 1 + l * 9 + 2 } else { 0 };
322
323 let checks = [
324 ("hidden_size > 0", h > 0),
325 ("num_layers > 0", l > 0),
326 ("num_heads > 0", nh > 0),
327 ("vocab_size > 0", v > 0),
328 ("hidden_size % num_heads == 0", nh > 0 && h % nh == 0),
329 ("num_heads % num_kv_heads == 0", nkv > 0 && nh % nkv == 0),
330 ("head_dim % 2 == 0", head_dim % 2 == 0),
331 ];
332
333 let all_pass = checks.iter().all(|(_, ok)| *ok);
334
335 let algebra_checks: Vec<Value> = checks
336 .iter()
337 .map(|(name, ok)| obj([("check", Value::from(*name)), ("passed", Value::from(*ok))]))
338 .collect();
339
340 Ok(obj([
341 ("config_path", Value::from(cfg_path.display().to_string())),
342 ("hidden_size", Value::from(h)),
343 ("num_layers", Value::from(l)),
344 ("num_heads", Value::from(nh)),
345 ("num_kv_heads", Value::from(nkv)),
346 ("vocab_size", Value::from(v)),
347 ("head_dim", Value::from(head_dim)),
348 ("expected_tensors", Value::from(expected_tensors)),
349 ("algebra_checks", Value::Array(algebra_checks)),
350 ("all_checks_pass", Value::from(all_pass)),
351 ]))
352}
353
354fn chrono_free_timestamp() -> String {
355 let dur = std::time::SystemTime::now()
356 .duration_since(std::time::UNIX_EPOCH)
357 .unwrap_or_default();
358 format!("{}s-since-epoch", dur.as_secs())
359}
360
361fn load_yaml_recursive(
362 dir: &Path,
363 out: &mut Vec<(String, Contract)>,
364) -> Result<(), Box<dyn std::error::Error>> {
365 let entries = std::fs::read_dir(dir)?;
366 for entry in entries {
367 let entry = entry?;
368 let path = entry.path();
369 if path.is_dir() {
370 load_yaml_recursive(&path, out)?;
371 } else if path.extension().and_then(|e| e.to_str()) == Some("yaml") {
372 let stem = path
373 .file_stem()
374 .and_then(|s| s.to_str())
375 .unwrap_or("unknown")
376 .to_string();
377 if stem == "binding" || stem == "playbook.schema" || stem.contains("playbook") {
378 continue;
379 }
380 if let Ok(c) = parse_contract(&path) {
381 out.push((stem, c));
382 }
383 }
384 }
385 Ok(())
386}
387
388#[cfg(test)]
389mod tests {
390 use super::*;
391
392 #[test]
393 fn certify_on_real_contracts() {
394 let dir = std::path::Path::new(env!("CARGO_MANIFEST_DIR")).join("../../contracts");
395 if !dir.exists() {
396 return;
397 }
398 let result = run(&dir, None, None);
399 assert!(result.is_ok());
400 }
401
402 #[test]
403 fn certify_empty_dir() {
404 let tmp = tempfile::tempdir().unwrap();
405 let result = run(tmp.path(), None, None);
406 assert!(result.is_ok());
407 }
408}