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::ContractKind;
7
8use crate::contract_walk::{collect_corpus, require_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). PVL-1 (PMAT-1099): an
32    // empty corpus is refused (exit 2), and so is one that `--kind` filters to zero.
33    let mut contracts = collect_corpus(path)?;
34
35    if let Some(k) = kind {
36        contracts.retain(|(_, c)| c.kind() == k);
37        require_contracts(path, &contracts, kind_filter)?;
38    }
39
40    contracts.sort_by(|a, b| a.0.cmp(&b.0));
41
42    let refs: Vec<(String, &provable_contracts::schema::Contract)> =
43        contracts.iter().map(|(s, c)| (s.clone(), c)).collect();
44
45    let include_classes = contracts.len() > 1;
46    let report = proof_status_report(&refs, binding.as_ref(), include_classes);
47
48    if format == "json" {
49        let json = serde_json::to_string_pretty(&report)?;
50        println!("{json}");
51    } else {
52        print!("{}", format_text(&report));
53        // Append kind breakdown when showing >1 contract.
54        if contracts.len() > 1 {
55            print_kind_breakdown(&contracts);
56        }
57    }
58
59    if table {
60        let matrices = obligation_matrix(&refs);
61        print!("{}", format_obligation_table(&matrices));
62    }
63
64    Ok(())
65}
66
67fn print_kind_breakdown(contracts: &[(String, provable_contracts::schema::Contract)]) {
68    let mut counts = std::collections::BTreeMap::<ContractKind, usize>::new();
69    for (_, c) in contracts {
70        *counts.entry(c.kind()).or_insert(0) += 1;
71    }
72    // Only print if there's > 1 kind represented.
73    if counts.len() < 2 {
74        return;
75    }
76    println!();
77    print!("By kind:");
78    for (kind, count) in &counts {
79        print!("  {kind}={count}");
80    }
81    println!();
82}
83
84fn parse_kind(s: &str) -> Result<ContractKind, Box<dyn std::error::Error>> {
85    match s.to_lowercase().as_str() {
86        "kernel" => Ok(ContractKind::Kernel),
87        "registry" => Ok(ContractKind::Registry),
88        "model-family" | "modelfamily" => Ok(ContractKind::ModelFamily),
89        "pattern" => Ok(ContractKind::Pattern),
90        "schema" => Ok(ContractKind::Schema),
91        other => Err(format!(
92            "invalid --kind value '{other}': expected one of \
93             kernel, registry, model-family, pattern, schema"
94        )
95        .into()),
96    }
97}
aprender_contracts_cli/commands/proof_status.rs

aprender_contracts_cli/commands/
proof_status.rs
