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

//! Example: Cross-project query with violations and coverage map.
//!
//! Demonstrates cross-project search features:
//! - `--call-sites`: Where contracts are used across sibling projects
//! - `--violations`: Binding gaps and unproven obligations
//! - `--coverage-map`: Per-project coverage matrix
//! - `--project <name>`: Filter to a single project
//! - `--all-projects`: Force cross-project scan
//! - `--rebuild-index`: Skip cache and rebuild
//!
//! Run from the workspace root:
//!   cargo run --example `cross_project_query`

use std::path::Path;

use provable_contracts::query::{self, ContractIndex, QueryParams};

fn main() {
    let contracts_dir = Path::new("contracts");
    let index =
        ContractIndex::from_directory(contracts_dir).expect("contracts/ directory must exist");

    // 1. Query with all cross-project enrichment
    println!("=== Cross-Project Query: \"softmax\" ===\n");
    let params = QueryParams {
        query: "softmax".to_string(),
        show_call_sites: true,
        show_violations: true,
        show_coverage_map: true,
        show_score: true,
        limit: 3,
        ..Default::default()
    };
    let output = query::execute(&index, &params);
    print!("{output}");

    // 2. Filter cross-project results to a single project
    println!("\n=== Filtered to aprender: \"softmax\" ===\n");
    let params = QueryParams {
        query: "softmax".to_string(),
        show_call_sites: true,
        show_violations: true,
        show_coverage_map: true,
        project_filter: Some("aprender".to_string()),
        limit: 2,
        ..Default::default()
    };
    let output = query::execute(&index, &params);
    print!("{output}");

    // 3. Force full cross-project scan with --all-projects
    println!("\n=== All Projects Scan: \"attention\" ===\n");
    let params = QueryParams {
        query: "attention".to_string(),
        all_projects: true,
        limit: 2,
        ..Default::default()
    };
    let output = query::execute(&index, &params);
    print!("{output}");

    // 4. JSON output for CI integration
    println!("\n=== JSON Output (first result) ===\n");
    let params = QueryParams {
        query: "attention".to_string(),
        show_call_sites: true,
        show_coverage_map: true,
        limit: 1,
        ..Default::default()
    };
    let output = query::execute(&index, &params);
    println!("{}", serde_json::to_string_pretty(&output).unwrap());

    // 5. Markdown output
    println!("\n=== Markdown Output ===\n");
    let params = QueryParams {
        query: "rmsnorm".to_string(),
        show_call_sites: true,
        show_violations: true,
        show_coverage_map: true,
        limit: 2,
        ..Default::default()
    };
    let output = query::execute(&index, &params);
    print!("{}", output.to_markdown());

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

    // 7. Class filter: Qwen equivalence class
    println!("\n=== Class E (Qwen): \"norm\" ===\n");
    let params = QueryParams {
        query: "norm".to_string(),
        class_filter: Some('E'),
        show_score: true,
        limit: 5,
        ..Default::default()
    };
    let output = query::execute(&index, &params);
    print!("{output}");

    // 8. Rebuild index from scratch (skip cache)
    println!("\n=== Rebuild Index ===\n");
    let fresh_index =
        ContractIndex::from_directory_opts(contracts_dir, true).expect("rebuild should succeed");
    println!("Rebuilt index with {} contracts", fresh_index.entries.len());
}