assura-types 0.4.5

Type checking for the Assura contract language
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

use super::*;

fn parse_source(src: &str) -> assura_parser::ast::SourceFile {
    let (sf, errs) = assura_parser::parse(src);
    assert!(errs.is_empty(), "parse errors: {errs:?}");
    sf.unwrap()
}

#[test]
fn no_effects_clause_no_errors() {
    let sf = parse_source(r#"contract Simple { requires { true } }"#);
    assert!(run_effect_checks(&sf).is_empty());
}

#[test]
fn declared_effects_with_io_no_error() {
    let sf = parse_source(r#"contract WithIo { effects { io } requires { true } }"#);
    let errs = run_effect_checks(&sf);
    assert!(
        !errs.iter().any(|e| e.code == "A07003"),
        "unexpected undeclared effect error: {errs:?}"
    );
}

#[test]
fn test_effect_polymorphism_basic() {
    // Effect row with a variable: `effects <io | E>`
    // The variable E should NOT produce A07003 (unknown effect)
    let sf = parse_source(
        r#"contract EffPoly {
            effects <io | E>
            fn map_with_effect(f: (Int) -> Int) -> List<Int>
        }"#,
    );
    let errs = run_effect_checks(&sf);
    let a07003_errors: Vec<_> = errs.iter().filter(|e| e.code == "A07003").collect();
    assert!(
        a07003_errors.is_empty(),
        "effect variable E should not produce A07003, got: {a07003_errors:?}"
    );
}

#[test]
fn must_not_io_with_effects_io_a07003() {
    let sf = parse_source(
        r#"contract Forbidden {
            effects { io }
            must-not { io }
            requires { true }
        }"#,
    );
    let errs = run_effect_checks(&sf);
    let must_not = errs
        .iter()
        .find(|e| e.code == "A07003" && e.message.contains("must-not"))
        .expect("effects(io) + must-not(io) must be A07003");
    let suggestion = must_not
        .suggestion
        .as_deref()
        .expect("must-not A07003 must not fall back to the unknown-effect catalog Help");
    assert_eq!(
        suggestion, "Remove the effect from `effects`, or drop it from `must-not`.",
        "must-not Help must be the shipped fix text, got: {suggestion}"
    );
}

#[test]
fn must_not_database_allows_effects_io() {
    let sf = parse_source(
        r#"contract OkIo {
            effects { io }
            must-not { database }
            requires { true }
        }"#,
    );
    let errs = run_effect_checks(&sf);
    assert!(
        !errs.iter().any(|e| e.message.contains("must-not")),
        "io is not in must-not database, got: {errs:?}"
    );
}

#[test]
fn must_not_unknown_name_a07003() {
    let sf = parse_source(
        r#"contract BadForbid {
            must-not { teleport }
            requires { true }
        }"#,
    );
    let errs = run_effect_checks(&sf);
    let unknown = errs
        .iter()
        .find(|e| e.code == "A07003")
        .expect("unknown must-not name must be A07003");
    assert!(
        unknown.suggestion.is_none(),
        "unknown must-not name must keep catalog Help, got: {:?}",
        unknown.suggestion
    );
}