ravencheck 0.1.2

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
90
91
92
93
94
95
96
97
98
99
100
101
102

// When using this macro within this crate, call it as:
//
// #[crate::check_module(crate)]
//
// When using it in another crate that has ravencheck as a dependency,
// call it as:
//
// #[ravencheck::check_module]
//
// If you rename the ravencheck dependency, for example as "my_dep",
// then call this macro as:
//
// #[my_dep::check_module(my_dep)]
#[crate::check_module(crate)]
pub mod my_mod {
    use std::collections::HashSet;

    #[declare]
    #[derive(PartialEq, Eq, Clone)]
    pub struct Set(pub HashSet<u32>);

    #[declare]
    pub fn empty_set() -> Set {
        Set(HashSet::new())
    }

    #[declare]
    #[derive(PartialEq, Eq, Clone, Copy)]
    pub struct Elem(u32);

    #[declare]
    pub fn member(e: Elem, s: Set) -> bool {
        s.0.contains(&e.0)
    }

    #[assume]
    fn equal_or_distinguisher() -> bool {
        forall(|a:Set,b:Set| {
            a == b || exists(|e:Elem| member(e,a) !=  member(e,b))
        })
    }

    #[assume]
    fn empty_set_no_member() -> bool {
        forall(|e: Elem| {
            !member(e, empty_set())
        })
    }

    #[declare]
    pub fn union(a: Set, b: Set) -> Set {
        let Set(s1) = a;
        let Set(s2) = b;
        let s3 = s1.union(&s2).cloned().collect();
        Set(s3)
    }

    #[annotate(union)]
    fn union_def() -> bool {
        |a: Set, b: Set|
        |c: Set|
        forall(|e: Elem| {
            member(e,c) == (member(e,a) || member(e,b))
        })
    }

    #[verify]
    fn union_preserves_member() -> bool {
        forall(|e:Elem,s:Set| {
            !member(e,s) || member(e, union(s,s))
        })
    }

    #[verify]
    fn union_self_is_self() -> bool {
        forall(|s:Set| union(s,s) == s)
    }

    #[verify]
    fn union_empty_set() -> bool {
        union(empty_set(), empty_set()) == empty_set()
    }

    #[cfg(test)]
    mod runtime_properties {
        use super::*;
    
        #[test]
        fn union_empty_set() {
            assert!(
                union(empty_set(), empty_set()) == empty_set()
            )
        }

        #[test]
        fn empty_is_empty() {
            assert!(
                !member(Elem(1), empty_set())
            )
        }
    }
}