aprender-contracts 0.34.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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126

//! Design by Contract walkthrough.
//!
//! Demonstrates the core provable-contracts workflow: parse a contract
//! YAML, inspect its equations and proof obligations, diff two contract
//! versions, and check binding status from a registry.
//!
//! Run from the workspace root:
//!   cargo run --example `design_by_contract`

use std::path::Path;

use provable_contracts::binding::parse_binding_str;
use provable_contracts::diff::diff_contracts;
use provable_contracts::query::{self, ContractIndex, QueryParams};
use provable_contracts::schema::parse_contract_str;
use provable_contracts::scoring;

fn main() {
    // --- 1. Parse a contract from YAML ---
    let yaml = include_str!("../../../contracts/softmax-kernel-v1.yaml");
    let contract = parse_contract_str(yaml).expect("valid contract YAML");

    println!("Contract: {}", contract.metadata.description);
    println!("Version:  {}", contract.metadata.version);
    println!();

    // --- 2. Inspect equations ---
    println!("Equations ({}):", contract.equations.len());
    for (name, eq) in &contract.equations {
        println!("  {name}: {}", eq.formula);
        if let Some(ref domain) = eq.domain {
            println!("    domain:   {domain}");
        }
        for inv in &eq.invariants {
            println!("    invariant: {inv}");
        }
    }
    println!();

    // --- 3. Inspect proof obligations ---
    println!("Proof obligations ({}):", contract.proof_obligations.len());
    for ob in &contract.proof_obligations {
        let tol = ob
            .tolerance
            .map_or_else(String::new, |t| format!(" (tol={t})"));
        println!("  [{}] {}{tol}", ob.obligation_type, ob.property);
    }
    println!();

    // --- 4. Diff two contract versions ---
    let v2_yaml = yaml.replace("version: \"1.0.0\"", "version: \"1.1.0\"");
    let v2 = parse_contract_str(&v2_yaml).expect("v2 contract");
    let diff = diff_contracts(&contract, &v2);
    println!(
        "Diff {} -> {}: suggested bump = {}",
        diff.old_version, diff.new_version, diff.suggested_bump
    );
    println!();

    // --- 5. Check binding status ---
    let binding_yaml = r#"
version: "1.0.0"
target_crate: aprender
bindings:
  - contract: softmax-kernel-v1.yaml
    equation: softmax
    module_path: "aprender::nn::softmax"
    function: softmax_f32
    status: implemented
"#;
    let registry = parse_binding_str(binding_yaml).expect("valid binding YAML");
    println!(
        "Binding registry: {} ({} bindings)",
        registry.target_crate,
        registry.bindings.len()
    );
    for b in &registry.bindings {
        println!("  {} :: {} -> {}", b.contract, b.equation, b.status);
    }
    println!();

    // --- 6. Score the contract ---
    let score = scoring::score_contract(&contract, Some(&registry), "softmax-kernel-v1");
    print!("{score}");
    println!();

    // --- 7. Query the contract index ---
    let contracts_dir = Path::new("contracts");
    if contracts_dir.exists() {
        let index =
            ContractIndex::from_directory(contracts_dir).expect("contracts/ directory must exist");
        let params = QueryParams {
            query: "softmax numerical stability".to_string(),
            show_score: true,
            show_pagerank: true,
            limit: 3,
            ..Default::default()
        };
        let output = query::execute(&index, &params);
        println!("--- Query: \"softmax numerical stability\" (top 3) ---\n");
        print!("{output}");

        // --- 8. Tier filter: Foundation kernels only ---
        println!("--- Tier 1 (Foundation Kernels) ---\n");
        let params = QueryParams {
            query: "kernel".to_string(),
            tier_filter: Some(1),
            limit: 5,
            ..Default::default()
        };
        let output = query::execute(&index, &params);
        print!("{output}");

        // --- 9. Class filter: Llama/Mistral equivalence class ---
        println!("--- Class A (Llama/Mistral) ---\n");
        let params = QueryParams {
            query: "attention".to_string(),
            class_filter: Some('A'),
            show_score: true,
            limit: 5,
            ..Default::default()
        };
        let output = query::execute(&index, &params);
        print!("{output}");
    }
}