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

#[crate::check_module(crate)]
#[declare_types(usize)]
#[allow(dead_code)]
mod rvn {
    #[declare]
    type List = Vec<usize>;

    #[declare]
    fn has_length(l: &List, n: usize) -> bool {
        l.len() == n
    }

    // If you remove the #[total] option here, then the
    // 'always_a_length' property fails to verify.
    #[declare]
    #[total]
    fn length(l: &List) -> usize {
        l.len()
    }

    #[assume]
    fn lengths_agree() -> bool {
        forall(|l: List| has_length(l, length(l)))
    }

    #[verify]
    fn always_a_length() -> bool {
        forall(|l: List| exists(|n: usize| has_length(l,n)))
    }

    // We can also use #[total] on a recursive-defined function.

    #[define]
    enum Nat {
        Z,
        S(Box<Nat>),
    }

    #[define]
    enum ListR {
        Nil,
        Cons(usize, Box<ListR>),
    }

    #[declare]
    fn has_length_r(l: &ListR, n: &Nat) -> bool {
        todo!()
    }

    // If you remove the #[total] option here, then the
    // 'always_a_length_r' property fails to verify.
    #[define]
    #[recursive]
    #[total]
    fn length_r(l: &ListR) -> Nat {
        match l {
            ListR::Nil => Nat::Z,
            ListR::Cons(n, l2) => Nat::S(Box::new(length_r(l2)))
        }
    }

    #[assume]
    fn lengths_agree() -> bool {
        forall(|l: ListR| has_length_r(l, length_r(l)))
    }

    #[verify]
    fn always_a_length_r() -> bool {
        forall(|l: ListR| exists(|n: Nat| has_length_r(l,n)))
    }

}