aprender_contracts_cli/commands/
proof_status.rs

1use std::path::Path;
2
3use provable_contracts::binding::parse_binding;
4use provable_contracts::obligation_matrix::{format_obligation_table, obligation_matrix};
5use provable_contracts::proof_status::{format_text, proof_status_report};
6use provable_contracts::schema::{parse_contract, ContractKind};
7
8use crate::contract_walk::collect_contracts;
9
10pub fn run(
11    path: &Path,
12    binding_path: Option<&Path>,
13    verify_root: Option<&Path>,
14    format: &str,
15    table: bool,
16    kind_filter: Option<&str>,
17) -> Result<(), Box<dyn std::error::Error>> {
18    let binding = match binding_path {
19        // L5 gate: when --verify-bindings is set, downgrade any `implemented`
20        // binding whose function is absent from source, so L5 requires bindings
21        // that are VERIFIED as implemented rather than merely self-declared.
22        Some(bp) => Some(match verify_root {
23            Some(root) => parse_binding(bp)?.verified(root),
24            None => parse_binding(bp)?,
25        }),
26        None => None,
27    };
28
29    let kind = kind_filter.map(parse_kind).transpose()?;
30
31    // Collect contracts (single file or directory tree)
32    let mut contracts = Vec::new();
33    if path.is_dir() {
34        collect_contracts(path, &mut contracts);
35    } else {
36        let stem = path
37            .file_stem()
38            .and_then(|s| s.to_str())
39            .unwrap_or("unknown")
40            .to_string();
41        let c = parse_contract(path)?;
42        contracts.push((stem, c));
43    }
44
45    if let Some(k) = kind {
46        contracts.retain(|(_, c)| c.kind() == k);
47    }
48
49    contracts.sort_by(|a, b| a.0.cmp(&b.0));
50
51    let refs: Vec<(String, &provable_contracts::schema::Contract)> =
52        contracts.iter().map(|(s, c)| (s.clone(), c)).collect();
53
54    let include_classes = contracts.len() > 1;
55    let report = proof_status_report(&refs, binding.as_ref(), include_classes);
56
57    if format == "json" {
58        let json = serde_json::to_string_pretty(&report)?;
59        println!("{json}");
60    } else {
61        print!("{}", format_text(&report));
62        // Append kind breakdown when showing >1 contract.
63        if contracts.len() > 1 {
64            print_kind_breakdown(&contracts);
65        }
66    }
67
68    if table {
69        let matrices = obligation_matrix(&refs);
70        print!("{}", format_obligation_table(&matrices));
71    }
72
73    Ok(())
74}
75
76fn print_kind_breakdown(contracts: &[(String, provable_contracts::schema::Contract)]) {
77    let mut counts = std::collections::BTreeMap::<ContractKind, usize>::new();
78    for (_, c) in contracts {
79        *counts.entry(c.kind()).or_insert(0) += 1;
80    }
81    // Only print if there's > 1 kind represented.
82    if counts.len() < 2 {
83        return;
84    }
85    println!();
86    print!("By kind:");
87    for (kind, count) in &counts {
88        print!("  {kind}={count}");
89    }
90    println!();
91}
92
93fn parse_kind(s: &str) -> Result<ContractKind, Box<dyn std::error::Error>> {
94    match s.to_lowercase().as_str() {
95        "kernel" => Ok(ContractKind::Kernel),
96        "registry" => Ok(ContractKind::Registry),
97        "model-family" | "modelfamily" => Ok(ContractKind::ModelFamily),
98        "pattern" => Ok(ContractKind::Pattern),
99        "schema" => Ok(ContractKind::Schema),
100        other => Err(format!(
101            "invalid --kind value '{other}': expected one of \
102             kernel, registry, model-family, pattern, schema"
103        )
104        .into()),
105    }
106}
aprender_contracts_cli/commands/proof_status.rs

aprender_contracts_cli/commands/
proof_status.rs
