assura 0.2.0

Contract-first AI-native language. Write what it should do. AI proves it does.
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

//! Unit tests for check / SMT Unknown classification.

#[test]
fn success_summary_distinguishes_vacuous_cases() {
    use super::report::success_summary_message;

    assert!(
        success_summary_message(true, false, false, 0)
            .contains("no contracts or functions to verify")
    );
    assert!(success_summary_message(false, true, false, 0).contains("no verifiable clauses"));
    assert!(success_summary_message(false, true, true, 0).contains("no SMT proof obligations"));
    assert_eq!(
        success_summary_message(false, false, false, 0),
        "check passed (no errors)"
    );
    assert_eq!(
        success_summary_message(false, false, false, 2),
        "check passed (2 warnings)"
    );
}

#[test]
fn unknown_classification_known_limitation_is_warning() {
    assert!(assura_smt::is_known_smt_limitation(
        "clause uses features not yet encoded in SMT (method call, deep field chain)"
    ));
}

#[test]
fn unknown_classification_solver_reason_is_error() {
    assert!(!assura_smt::is_known_smt_limitation(
        "non-linear arithmetic"
    ));
    assert!(!assura_smt::is_known_smt_limitation(
        "Z3 not available (compiled without z3-verify feature)"
    ));
    assert!(!assura_smt::is_known_smt_limitation(
        "could not encode clause to SMT-LIB2"
    ));
    assert!(!assura_smt::is_known_smt_limitation(
        "no result from solver"
    ));
}

#[test]
fn unknown_classification_boundary_near_miss() {
    assert!(!assura_smt::is_known_smt_limitation(
        "clause not encoded in SMT yet"
    ));
    assert!(!assura_smt::is_known_smt_limitation(
        "not yet supported in SMT"
    ));
    assert!(!assura_smt::is_known_smt_limitation("features not encoded"));
}

#[test]
fn unknown_classification_diagnostic_output() {
    let filename = "test.assura";
    let clause_desc = "TestContract: ensures";

    // Warning path: known limitation -> A05102
    let reason = "clause uses features not yet encoded in SMT (method call)";
    let mut has_errors = false;
    let diag = if assura_smt::is_known_smt_limitation(reason) {
        assura_diagnostics::Diagnostic::warning(
            "A05102",
            format!("verification skipped for {clause_desc}: {reason}"),
            0..0,
        )
        .with_file(filename)
    } else {
        has_errors = true;
        assura_diagnostics::Diagnostic::error(
            "A05103",
            format!("verification inconclusive for {clause_desc}: {reason}"),
            0..0,
        )
        .with_file(filename)
    };
    assert!(!has_errors, "known limitation should not set has_errors");
    assert!(diag.message.starts_with("verification skipped"));
    assert_eq!(diag.code, "A05102", "known limitation should use A05102");

    // Error path: solver inconclusive -> A05103
    let reason2 = "non-linear arithmetic";
    let mut has_errors2 = false;
    let diag2 = if assura_smt::is_known_smt_limitation(reason2) {
        assura_diagnostics::Diagnostic::warning(
            "A05102",
            format!("verification skipped for {clause_desc}: {reason2}"),
            0..0,
        )
        .with_file(filename)
    } else {
        has_errors2 = true;
        assura_diagnostics::Diagnostic::error(
            "A05103",
            format!("verification inconclusive for {clause_desc}: {reason2}"),
            0..0,
        )
        .with_file(filename)
    };
    assert!(has_errors2, "solver inconclusive should set has_errors");
    assert!(diag2.message.starts_with("verification inconclusive"));
    assert_eq!(
        diag2.code, "A05103",
        "solver inconclusive should use A05103"
    );
}