aprender-contracts 0.32.0

Papers to Math to Contracts in Code — YAML contract parsing, validation, scaffold generation, and Kani harness codegen for provable Rust kernels
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

use provable_contracts::proof_status::proof_status_report;
use provable_contracts::schema::parse_contract;
fn main() {
    let d = std::env::args().nth(1).unwrap_or_else(|| {
        eprintln!("Usage: proof_status <dir/>");
        std::process::exit(1);
    });
    let mut cs = Vec::new();
    for e in std::fs::read_dir(&d).unwrap().flatten() {
        let p = e.path();
        if p.extension().and_then(|e| e.to_str()) == Some("yaml") {
            let s = p
                .file_stem()
                .and_then(|s| s.to_str())
                .unwrap_or("x")
                .to_string();
            if let Ok(c) = parse_contract(&p) {
                cs.push((s, c));
            }
        }
    }
    cs.sort_by(|a, b| a.0.cmp(&b.0));
    let refs: Vec<_> = cs.iter().map(|(s, c)| (s.clone(), c)).collect();
    let r = proof_status_report(&refs, None, true);
    println!(
        "Contracts: {} | Obligations: {} | Kani: {} | Lean: {}",
        r.totals.contracts, r.totals.obligations, r.totals.kani_harnesses, r.totals.lean_proved
    );
}