aprender_contracts_cli/commands/
audit.rs

1use std::path::Path;
2
3use provable_contracts::audit::{audit_binding, audit_contract};
4use provable_contracts::binding::parse_binding;
5use provable_contracts::error::Severity;
6use provable_contracts::schema::{parse_contract, Contract};
7
8pub fn run(path: &Path, binding_path: Option<&Path>) -> Result<(), Box<dyn std::error::Error>> {
9    let contract = parse_contract(path)?;
10
11    let report = audit_contract(&contract);
12    print_traceability_header(&contract, &report);
13    print_lean_status(&contract);
14    print_coq_status(&contract);
15    print_violations(&report.violations);
16
17    let errors = count_errors(&report.violations);
18    let binding_errors = run_binding_audit(path, &contract, binding_path)?;
19
20    let total = errors + binding_errors;
21    if total > 0 {
22        return Err(format!("Audit found {total} error(s)").into());
23    }
24    Ok(())
25}
26
27fn print_traceability_header(contract: &Contract, report: &provable_contracts::audit::AuditReport) {
28    println!("Traceability Audit");
29    println!("==================");
30    println!("Equations:          {}", report.equations);
31    println!("Proof obligations:  {}", report.obligations);
32    println!("Falsification tests: {}", report.falsification_tests);
33    println!("Kani harnesses:     {}", report.kani_harnesses);
34    println!("Type invariants:    {}", contract.type_invariants.len());
35}
36
37fn print_lean_status(contract: &Contract) {
38    let lean_proved = contract
39        .verification_summary
40        .as_ref()
41        .map_or(0, |vs| vs.l4_lean_proved);
42    if lean_proved == 0 {
43        return;
44    }
45    let total = contract
46        .verification_summary
47        .as_ref()
48        .map_or(0, |vs| vs.total_obligations);
49    println!("Lean proved:        {lean_proved}/{total}");
50}
51
52fn print_coq_status(contract: &Contract) {
53    let Some(spec) = contract.coq_spec.as_ref() else {
54        return;
55    };
56    let total = spec.obligations.len();
57    let proved = spec
58        .obligations
59        .iter()
60        .filter(|o| o.status == "proved")
61        .count();
62    let admitted = spec
63        .obligations
64        .iter()
65        .filter(|o| o.status == "admitted")
66        .count();
67    let stubs = total - proved - admitted;
68    let suffix = if total > 0 {
69        format!("  {total} obligations —")
70    } else {
71        " no obligation links".to_string()
72    };
73    println!(
74        "Coq ({}):{suffix} {proved} proved, {admitted} admitted, {stubs} stub",
75        spec.module
76    );
77}
78
79fn print_violations(violations: &[provable_contracts::error::Violation]) {
80    println!();
81    if violations.is_empty() {
82        println!("No audit findings.");
83    } else {
84        for v in violations {
85            println!("{v}");
86        }
87    }
88}
89
90fn count_errors(violations: &[provable_contracts::error::Violation]) -> usize {
91    violations
92        .iter()
93        .filter(|v| v.severity == Severity::Error)
94        .count()
95}
96
97fn run_binding_audit(
98    path: &Path,
99    contract: &Contract,
100    binding_path: Option<&Path>,
101) -> Result<usize, Box<dyn std::error::Error>> {
102    let Some(bp) = binding_path else {
103        return Ok(0);
104    };
105    let binding = parse_binding(bp)?;
106    let contract_file = path
107        .file_name()
108        .and_then(|n| n.to_str())
109        .unwrap_or("unknown");
110    let binding_report = audit_binding(&[(contract_file, contract)], &binding);
111
112    println!();
113    println!("Binding Audit");
114    println!("=============");
115    println!("Total equations:    {}", binding_report.total_equations);
116    println!("Bound equations:    {}", binding_report.bound_equations);
117    println!("Implemented:        {}", binding_report.implemented);
118    println!("Partial:            {}", binding_report.partial);
119    println!("Not implemented:    {}", binding_report.not_implemented);
120    println!("Obligations total:  {}", binding_report.total_obligations);
121    println!(
122        "Obligations covered: {}",
123        binding_report.covered_obligations
124    );
125    println!();
126
127    if binding_report.violations.is_empty() {
128        println!("No binding gaps found.");
129    } else {
130        for v in &binding_report.violations {
131            println!("{v}");
132        }
133    }
134    Ok(count_errors(&binding_report.violations))
135}
aprender_contracts_cli/commands/audit.rs

aprender_contracts_cli/commands/
audit.rs
