creusot_contracts/logic/
well_founded.rs

1#[cfg(creusot)]
2use crate::logic::{Mapping, such_that, unreachable};
3use crate::*;
4
5/// Instances of this trait are types which are allowed as variants of recursive definitions.
6pub trait WellFounded: Sized {
7    /// Relation used to specify well-foundedness.
8    #[logic]
9    #[intrinsic("well_founded_relation")]
10    fn well_founded_relation(self, other: Self) -> bool;
11
12    /// Being well-founded means that there is no infinitely decreasing sequence.
13    ///
14    /// If you can map your type to another that already implements `WellFounded`
15    /// (and the mapping preserves `well_founded_relation`), this lemma is quite
16    /// easy to prove:
17    ///
18    /// ```
19    /// # use creusot_contracts::{*, well_founded::WellFounded};
20    /// struct MyInt(Int);
21    /// impl WellFounded for MyInt {
22    ///     #[logic(open)]
23    ///     fn well_founded_relation(self, other: Self) -> bool {
24    ///         Int::well_founded_relation(self.0, other.0)
25    ///     }
26    ///
27    ///     #[logic]
28    ///     #[ensures(!Self::well_founded_relation(s[result], s[result + 1]))]
29    ///     fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int {
30    ///         Int::no_infinite_decreasing_sequence(|i| s[i].0)
31    ///     }
32    /// }
33    /// ```
34    #[logic]
35    #[ensures(result >= 0)]
36    #[ensures(!Self::well_founded_relation(s[result], s[result + 1]))]
37    fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int;
38}
39
40impl WellFounded for Int {
41    #[logic(open)]
42    fn well_founded_relation(self, other: Self) -> bool {
43        self >= 0 && self > other
44    }
45
46    #[trusted]
47    #[logic(opaque)]
48    #[ensures(result >= 0)]
49    #[ensures(!Self::well_founded_relation(s[result], s[result + 1]))]
50    fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int {
51        dead
52    }
53}
54
55macro_rules! impl_well_founded {
56    ($($t:ty),*) => {
57        $(
58
59        impl WellFounded for $t {
60            #[logic(open)]
61            fn well_founded_relation(self, other: Self) -> bool {
62                self > other
63            }
64
65            #[logic]
66            #[ensures(result >= 0)]
67            #[ensures(!Self::well_founded_relation(s[result], s[result + 1]))]
68            fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int {
69                pearlite! {
70                    Int::no_infinite_decreasing_sequence(|i| s[i]@ - $t::MIN@)
71                }
72            }
73        }
74
75        )*
76    };
77}
78
79impl_well_founded!(u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize);
80
81impl<T: WellFounded> WellFounded for &T {
82    #[logic(open)]
83    fn well_founded_relation(self, other: Self) -> bool {
84        T::well_founded_relation(*self, *other)
85    }
86
87    #[logic]
88    #[ensures(result >= 0)]
89    #[ensures(!Self::well_founded_relation(s[result], s[result + 1]))]
90    fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int {
91        T::no_infinite_decreasing_sequence(|i| *s[i])
92    }
93}
94
95impl<T: WellFounded> WellFounded for Box<T> {
96    #[logic(open)]
97    fn well_founded_relation(self, other: Self) -> bool {
98        T::well_founded_relation(*self, *other)
99    }
100
101    #[logic]
102    #[ensures(result >= 0)]
103    #[ensures(!Self::well_founded_relation(s[result], s[result + 1]))]
104    fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int {
105        T::no_infinite_decreasing_sequence(|i| *s[i])
106    }
107}
108
109// === Implementation of `WellFounded` for tuples up to size 8.
110
111macro_rules! impl_tuple_to_pair {
112    ( $t1:ident = $idx1:tt , $($ts:ident = $idxs:tt),+ ) => {
113        #[cfg(creusot)]
114        #[allow(unused_parens)]
115        impl<$t1, $($ts),+> TupleToPair for ($t1, $($ts),+) {
116            type Target = ($t1, ($($ts),+));
117            #[logic]
118            fn tuple_to_pair(self) -> Self::Target {
119                (self.0, ($( self . $idxs ),+))
120            }
121        }
122    };
123}
124
125macro_rules! wf_tuples {
126    ( $t:ident = $idx:tt ) => {};
127    ( $($ts:ident = $idxs:tt),+ ) => {
128        impl_tuple_to_pair!($($ts=$idxs),+);
129        wf_tuples!( @impl $($ts=$idxs),+ );
130        wf_tuples!( @pop_last [$($ts=$idxs),+] [] );
131    };
132    // its a bit hard to remove the _last_ element of a sequence in macros: we need this little helper.
133    (@pop_last [$t:ident=$idx:tt , $($ts:ident=$idxs:tt),+] [$($ts2:ident=$idxs2:tt),*]) => {
134        wf_tuples!( @pop_last [$($ts=$idxs),+] [$($ts2=$idxs2,)* $t=$idx] );
135    };
136    (@pop_last [$t:ident=$idx:tt]                           [$($ts2:ident=$idxs2:tt),*]) => {
137        wf_tuples!( $($ts2 = $idxs2),* );
138    };
139    ( @impl $($ts:ident = $idxs:tt),+ ) => {
140        impl<$($ts),+> WellFounded for ($($ts),+)
141        where $($ts : WellFounded),+
142        {
143            wf_tuples!( @wf_relation self other {} [] $($ts=$idxs)+ );
144
145            #[logic]
146            #[ensures(result >= 0)]
147            #[ensures(!Self::well_founded_relation(s[result], s[result + 1]))]
148            fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int {
149                pearlite! {
150                    if exists<r> r >= 0 && !Self::well_founded_relation(s[r], s[r + 1]) {
151                        such_that(|r| r >= 0 && !Self::well_founded_relation(s[r], s[r + 1]))
152                    } else {
153                        let _ = T0::no_infinite_decreasing_sequence(first_component_decr(|i| s[i].tuple_to_pair()));
154                        unreachable()
155                    }
156                }
157            }
158        }
159    };
160    ( @wf_relation $name1:ident $name2:ident {$($res:expr)?} [$($to_eq:tt)*] $t:ident = $idx:tt $($ts:ident = $idxs:tt)* ) => {
161        wf_tuples!{ @wf_relation $name1 $name2
162            {$($res ||)? ($(($name1 . $to_eq == $name2 . $to_eq ) &&)* $t::well_founded_relation($name1 . $idx, $name2 . $idx))}
163            [$($to_eq)* $idx]
164            $($ts=$idxs)*
165        }
166    };
167    ( @wf_relation $name1:ident $name2:ident {$res:expr} [$($to_eq:tt)*] ) => {
168        #[logic(open)]
169        fn well_founded_relation($name1, $name2: Self) -> bool {
170            $res
171        }
172    };
173}
174
175wf_tuples!(T0 = 0, T1 = 1, T2 = 2, T3 = 3, T4 = 4, T5 = 5, T6 = 6, T7 = 7);
176
177/// Convert a tuple to a pair, because the lemmas below act on pairs.
178#[cfg(creusot)]
179trait TupleToPair {
180    type Target;
181    #[logic]
182    fn tuple_to_pair(self) -> Self::Target;
183}
184
185/// Get an index > i, such that `s[index] < s[i]`.
186#[logic]
187#[requires(forall<i> 0 <= i ==> <(T1, T2)>::well_founded_relation(s[i], s[i + 1]))]
188#[requires(0 <= i)]
189#[ensures(i < result)]
190#[ensures(T1::well_founded_relation(s[i].0, s[result].0))]
191#[variant(s[i].1)]
192fn extract_next_decr<T1: WellFounded, T2: WellFounded>(s: Mapping<Int, (T1, T2)>, i: Int) -> Int {
193    if T1::well_founded_relation(s[i].0, s[i + 1].0) { i + 1 } else { extract_next_decr(s, i + 1) }
194}
195
196/// Used to construct [`first_component_decr`] below.
197#[logic]
198#[requires(forall<i> 0 <= i ==> <(T1, T2)>::well_founded_relation(s[i], s[i + 1]))]
199#[requires(0 <= i)]
200#[ensures(0 <= result)]
201#[ensures(0 < i ==> {
202    let prev = extract_nth(s, i - 1);
203    prev < result &&
204    T1::well_founded_relation(s[prev].0, s[result].0)
205})]
206#[variant(i)]
207fn extract_nth<T1: WellFounded, T2: WellFounded>(s: Mapping<Int, (T1, T2)>, i: Int) -> Int {
208    if i == 0 {
209        0
210    } else {
211        let prev = extract_nth(s, i - 1);
212        extract_next_decr(s, prev)
213    }
214}
215
216/// Prove that `s` being infinitely decreasing is contradictory, by extracting
217/// a sequence such that the first component decreases.
218#[logic]
219#[requires(forall<i> 0 <= i ==> <(T1, T2)>::well_founded_relation(s[i], s[i + 1]))]
220#[ensures(forall<i> 0 <= i ==> T1::well_founded_relation(result[i], result[i + 1]))]
221pub fn first_component_decr<T1: WellFounded, T2: WellFounded>(
222    s: Mapping<Int, (T1, T2)>,
223) -> Mapping<Int, T1> {
224    |i| if 0 <= i { s[extract_nth(s, i)].0 } else { s[i].0 }
225}
creusot_contracts/logic/well_founded.rs

creusot_contracts/logic/
well_founded.rs
