ravencheck 0.2.0

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
103
104
105
106
107
108
109
110
111

#[crate::check_module(crate)]
#[declare_types(u32)]
#[allow(dead_code)]
mod my_mod {
    use std::marker::PhantomData;

    #[declare]
    #[derive(Copy,Clone,PartialEq,Eq,Hash)]
    struct Nat<T>{
        value: usize,
        tag: PhantomData<T>,
    }

    impl<T> Nat<T> {
        pub fn new(n: usize) -> Nat<T> {
            Nat { value: n, tag: PhantomData }
        }
    }

    #[declare]
    fn zero<T>() -> Nat<T> { Nat::new(0) }

    #[declare]
    fn le<T>(a: Nat<T>, b: Nat<T>) -> bool {
        a.value <= b.value
    }

    #[define]
    fn lt<T>(a: Nat<T>, b: Nat<T>) -> bool
    where T: std::cmp::Eq + Copy
    {
        le::<T>(a,b) && a != b
    }

    #[define]
    fn ge<T>(a: Nat<T>, b: Nat<T>) -> bool
    {
        le::<T>(b,a)
    }

    #[define]
    fn gt<T>(a: Nat<T>, b: Nat<T>) -> bool
    where T: std::cmp::Eq + Copy
    {
        ge::<T>(a,b) && a != b
    }

    #[declare]
    fn dec<T>(a: Nat<T>) -> Nat<T> {
        if a.value == 0 {
            Nat::new(0)
        } else {
            Nat::new(a.value - 1)
        }
    }

    #[declare]
    fn inc<T>(a: Nat<T>) -> Nat<T> {
        Nat::new(a.value + 1)
    }

    #[assume((Nat<T>, T))]
    fn inc_dec<T>() -> bool {
        forall(|a: Nat<T>| {
            implies(
                a != zero::<T>(),
                inc::<T>(dec::<T>(a)) == a
            )
        })
    }

    #[define_rec]
    fn add<T>(a: Nat<T>, b: Nat<T>) -> Nat<T>
    where T: std::cmp::Eq + Copy
    {
        if a == zero::<T>() {
            b
        } else {
            inc::<T>(
                add::<T>(dec::<T>(a), b)
            )
        }
    }

    #[annotate(add)]
    fn add_trivial<T>() -> bool {
        |a: Nat<T>, b: Nat<T>|
        |c: Nat<T>|
        true
    }

    // #[annotate(add)]
    // fn add_monotonic<T>() -> bool {
    //     |a: Nat<T>, b: Nat<T>|
    //     |c: Nat<T>|
    //     le::<T>(a,c) && le::<T>(a,b)
    // }

    #[annotate(add)]
    fn add_zeros<T>() -> bool {
        |a: Nat<T>, b: Nat<T>|
        |c: Nat<T>|
        implies(a == zero::<T>(), b == c)
        && implies(b == zero::<T>(), a == c)
    }

    #[verify]
    fn simple_zeros() -> bool {
        add::<u32>(zero::<u32>(), zero::<u32>()) == zero::<u32>()
    }
}