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

use crate::*;

pub trait Invariant {
    #[predicate(prophetic)]
    #[rustc_diagnostic_item = "creusot_invariant_user"]
    fn invariant(self) -> bool;
}

impl Invariant for ! {
    #[predicate(prophetic)]
    #[open]
    #[creusot::trusted_ignore_structural_inv]
    fn invariant(self) -> bool {
        false
    }
}

impl<T: ?Sized> Invariant for &T {
    #[predicate(prophetic)]
    #[open]
    #[creusot::trusted_ignore_structural_inv]
    #[creusot::trusted_is_tyinv_trivial_if_param_trivial]
    fn invariant(self) -> bool {
        inv(*self)
    }
}

impl<T: ?Sized> Invariant for &mut T {
    #[predicate(prophetic)]
    #[open]
    #[creusot::trusted_ignore_structural_inv]
    #[creusot::trusted_is_tyinv_trivial_if_param_trivial]
    fn invariant(self) -> bool {
        pearlite! { inv(*self) && inv(^self) }
    }
}

#[predicate(prophetic)]
#[trusted]
#[rustc_diagnostic_item = "creusot_invariant_internal"]
pub fn inv<T: ?Sized>(_: T) -> bool {
    true
}

#[cfg(not(creusot))]
pub fn inv<T: ?Sized>(_: &T) -> bool {
    panic!()
}