aprender-contracts-cli 0.40.1

CLI for provable-contracts — validate, scaffold, verify, status, audit
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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47

//! `pv codegen` — generate Rust `debug_assert`!() from YAML contracts.

use provable_contracts::codegen;
use std::path::Path;

pub fn run(contract_dir: &Path, output: Option<&Path>) -> Result<(), Box<dyn std::error::Error>> {
    let contracts = codegen::generate_all(contract_dir);

    if contracts.is_empty() {
        println!("No contracts with preconditions/postconditions/invariants found.");
        return Ok(());
    }

    let mut total_pre = 0;
    let mut total_post = 0;
    let mut total_inv = 0;
    let mut total_lean = 0;

    for c in &contracts {
        total_pre += c.precondition_count;
        total_post += c.postcondition_count;
        total_inv += c.invariant_count;
        total_lean += c.lean_theorem_count;
    }

    println!("pv codegen — contract → Rust assertions");
    println!("========================================\n");
    println!("Contracts:      {}", contracts.len());
    println!("Preconditions:  {total_pre}");
    println!("Postconditions: {total_post}");
    println!("Invariants:     {total_inv}");
    println!("Lean theorems:  {total_lean}");

    let out_path = output.unwrap_or(Path::new("src/generated_contracts.rs"));

    // Create parent directory if it doesn't exist
    if let Some(parent) = out_path.parent() {
        if !parent.as_os_str().is_empty() {
            std::fs::create_dir_all(parent)?;
        }
    }

    codegen::write_rust_module(&contracts, out_path)?;
    println!("\nGenerated: {}", out_path.display());

    Ok(())
}