aprender-contracts 0.33.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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65

//! Example: Lean 4 proof status across foundation kernels.
//!
//! Demonstrates the Lean integration:
//! - Lean definition + theorem generation from YAML contracts
//! - L4 proof coverage tracking (proved vs sorry)
//! - Lean-aware scoring dimension
//!
//! Run from the workspace root:
//!   cargo run --example `lean_proofs`

use std::path::Path;

use provable_contracts::lean_gen;
use provable_contracts::schema::parse_contract;
use provable_contracts::scoring;

fn main() {
    let contracts_dir = Path::new("contracts");

    // Contracts with Lean proofs
    let lean_contracts = [
        "softmax-kernel-v1",
        "rmsnorm-kernel-v1",
        "silu-kernel-v1",
        "cross-entropy-kernel-v1",
        "layernorm-kernel-v1",
        "transpose-kernel-v1",
    ];

    println!("=== Lean 4 Proof Status ===\n");

    let mut reports = Vec::new();
    for stem in &lean_contracts {
        let path = contracts_dir.join(format!("{stem}.yaml"));
        let contract = parse_contract(&path).unwrap();
        let report = lean_gen::lean_status(&contract);
        reports.push(report);
    }
    print!("{}", lean_gen::format_status_report(&reports));

    println!("\n=== Score Impact (Lean Dimension) ===\n");
    for stem in &lean_contracts {
        let path = contracts_dir.join(format!("{stem}.yaml"));
        let contract = parse_contract(&path).unwrap();
        let score = scoring::score_contract(&contract, None, stem);
        println!("{stem}");
        println!(
            "  Score: {:.2} (Grade {}) — Lean: {:.2}",
            score.composite, score.grade, score.lean_coverage
        );
    }

    println!("\n=== Generated Lean for softmax ===\n");
    let softmax = parse_contract(&contracts_dir.join("softmax-kernel-v1.yaml")).unwrap();
    let files = lean_gen::generate_lean_files(&softmax);
    for f in &files {
        println!("--- {} ---", f.path);
        // Show first 10 lines of each file
        for line in f.content.lines().take(10) {
            println!("{line}");
        }
        println!("  ...\n");
    }
    println!("{} Lean files generated for softmax", files.len());
}