ravencheck 0.4.1

Decidable verification of Rust code using relational abstraction.
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

#[crate::check_module(crate)]
#[allow(dead_code)]
mod rvn {
    #[define]
    #[derive(Clone, Debug, PartialEq, Eq)]
    enum Nat { Z, S(Box<Nat>) }

    #[define]
    #[recursive]
    fn le(a: &Nat, b: &Nat) -> bool {
        match a {
            Nat::Z => true,
            Nat::S(a_minus) => match b {
                Nat::Z => false,
                Nat::S(b_minus) => le(a_minus, b_minus),
            }
        }
    }

    #[annotate_multi]
    #[for_values(a: Nat)]
    #[for_call(le(a,a) => result1)]
    fn le_reflexive() -> bool {
        result1 == true
    }

    // This only verifies when 'le_reflexive' has been given as an
    // annotation.
    #[verify]
    fn le_reflexive_direct() -> bool {
        forall(|a: Nat| le(a,a))
    }

    #[annotate_multi]
    #[for_values(a: Nat, b: Nat)]
    #[for_call(le(a,b) => res_a_b)]
    #[for_call(le(b,a) => res_b_a)]
    fn le_total() -> bool {
        res_a_b || res_b_a
    }

    // This is marked as a 'should_fail', so it isn't actually added
    // to the assumption context for later verification tasks.
    #[annotate_multi]
    #[should_fail]
    #[for_values(a: Nat, b: Nat)]
    #[for_call(le(a,b) => res_a_b)]
    #[for_call(le(b,a) => res_b_a)]
    fn le_all_eq() -> bool {
        res_a_b && res_b_a
    }

    #[annotate_multi]
    #[for_values(a: Nat, b: Nat)]
    #[for_call(le(a,b) => res_a_b)]
    #[for_call(le(b,a) => res_b_a)]
    fn le_antireflexive() -> bool {
        implies(
            res_a_b && res_b_a,
            a == b,
        )
    }

    #[annotate_multi]
    #[for_values(a: Nat, b: Nat, c: Nat)]
    #[for_call(le(a,b) => res_a_b)]
    #[for_call(le(b,c) => res_b_c)]
    #[for_call(le(a,c) => res_a_c)]
    fn le_transitive() -> bool {
        implies(
            res_a_b && res_b_c,
            res_a_c,
        )
    }

    // A sanity check, testing the recursion guards.
    #[annotate_multi]
    #[should_fail]
    #[for_values(a: Nat, b: Nat)]
    #[for_call(le(a,b) => result1)]
    fn should_fail() -> bool {
        false
    }

    #[falsify]
    fn should_really_fail() -> bool {
        false
    }
}