creusot_std/logic/
well_founded.rs

1#[cfg(creusot)]
2use crate::logic::{Mapping, any, try_such_that};
3use crate::prelude::*;
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_std::{prelude::*, well_founded::WellFounded};
20    /// struct MyInt(Int);
21    /// impl WellFounded for MyInt {
22    ///     #[logic(open, inline)]
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, inline)]
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, inline)]
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, inline)]
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
95#[cfg(feature = "std")]
96impl<T: WellFounded> WellFounded for Box<T> {
97    #[logic(open, inline)]
98    fn well_founded_relation(self, other: Self) -> bool {
99        T::well_founded_relation(*self, *other)
100    }
101
102    #[logic]
103    #[ensures(result >= 0)]
104    #[ensures(!Self::well_founded_relation(s[result], s[result + 1]))]
105    fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int {
106        T::no_infinite_decreasing_sequence(|i| *s[i])
107    }
108}
109
110// === Implementation of `WellFounded` for tuples up to size 8.
111
112impl WellFounded for () {
113    #[logic(open, inline)]
114    fn well_founded_relation(self, _: Self) -> bool {
115        false
116    }
117
118    #[logic]
119    #[ensures(result >= 0)]
120    #[ensures(!Self::well_founded_relation(s[result], s[result + 1]))]
121    fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int {
122        0
123    }
124}
125
126macro_rules! impl_tuple_to_pair {
127    ( $t1:ident = $idx1:tt, $($ts:ident = $idxs:tt,)* ) => {
128        #[cfg(creusot)]
129        #[allow(unused_parens)]
130        impl<$t1, $($ts),*> TupleToPair for ($t1, $($ts,)*) {
131            type Target = ($t1, ($($ts,)*));
132            #[logic]
133            fn tuple_to_pair(self) -> Self::Target {
134                (self.0, ($( self . $idxs, )*))
135            }
136        }
137    };
138}
139
140/// Convert a tuple to a pair, because the lemmas below act on pairs.
141#[cfg(creusot)]
142trait TupleToPair {
143    type Target;
144    #[logic]
145    fn tuple_to_pair(self) -> Self::Target;
146}
147
148macro_rules! wf_tuples {
149    () => {};
150    ( $($ts:ident = $idxs:tt),+ ) => {
151        impl_tuple_to_pair!($($ts=$idxs,)+);
152        wf_tuples!( @impl $($ts=$idxs),+ );
153        wf_tuples!( @pop_last [$($ts=$idxs),+] [] );
154    };
155    // its a bit hard to remove the _last_ element of a sequence in macros: we need this little helper.
156    (@pop_last [$t:ident=$idx:tt , $($ts:ident=$idxs:tt),+] [$($ts2:ident=$idxs2:tt),*]) => {
157        wf_tuples!( @pop_last [$($ts=$idxs),+] [$($ts2=$idxs2,)* $t=$idx] );
158    };
159    (@pop_last [$t:ident=$idx:tt]                           [$($ts2:ident=$idxs2:tt),*]) => {
160        wf_tuples!( $($ts2 = $idxs2),* );
161    };
162    ( @impl $($ts:ident = $idxs:tt),+ ) => {
163        impl<$($ts),+> WellFounded for ($($ts,)+)
164        where $($ts : WellFounded),+
165        {
166            wf_tuples!( @wf_relation self other {} [] $($ts=$idxs)+ );
167
168            #[logic]
169            #[ensures(result >= 0)]
170            #[ensures(!Self::well_founded_relation(s[result], s[result + 1]))]
171            fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int {
172                pearlite! {
173                    match try_such_that(|r| r >= 0 && !Self::well_founded_relation(s[r], s[r + 1])) {
174                        Some(r) => r,
175                        None => {
176                            let _ = T0::no_infinite_decreasing_sequence(first_component_decr(|i| s[i].tuple_to_pair()));
177                            any()
178                        }
179                    }
180                }
181            }
182        }
183    };
184    ( @wf_relation $name1:ident $name2:ident {$($res:expr)?} [$($to_eq:tt)*] $t:ident = $idx:tt $($ts:ident = $idxs:tt)* ) => {
185        wf_tuples!{ @wf_relation $name1 $name2
186            {$($res ||)? ($(($name1 . $to_eq == $name2 . $to_eq ) &&)* $t::well_founded_relation($name1 . $idx, $name2 . $idx))}
187            [$($to_eq)* $idx]
188            $($ts=$idxs)*
189        }
190    };
191    ( @wf_relation $name1:ident $name2:ident {$res:expr} [$($to_eq:tt)*] ) => {
192        #[logic(open, inline)]
193        fn well_founded_relation($name1, $name2: Self) -> bool {
194            $res
195        }
196    };
197}
198
199wf_tuples!(T0 = 0, T1 = 1, T2 = 2, T3 = 3, T4 = 4, T5 = 5, T6 = 6, T7 = 7);
200
201/// Get an index > i, such that `s[index] < s[i]`.
202#[logic]
203#[requires(forall<i> 0 <= i ==> <(T1, T2)>::well_founded_relation(s[i], s[i + 1]))]
204#[requires(0 <= i)]
205#[ensures(i < result)]
206#[ensures(T1::well_founded_relation(s[i].0, s[result].0))]
207#[variant(s[i].1)]
208fn extract_next_decr<T1: WellFounded, T2: WellFounded>(s: Mapping<Int, (T1, T2)>, i: Int) -> Int {
209    if T1::well_founded_relation(s[i].0, s[i + 1].0) { i + 1 } else { extract_next_decr(s, i + 1) }
210}
211
212/// Used to construct [`first_component_decr`] below.
213#[logic]
214#[requires(forall<i> 0 <= i ==> <(T1, T2)>::well_founded_relation(s[i], s[i + 1]))]
215#[requires(0 <= i)]
216#[ensures(0 <= result)]
217#[ensures(0 < i ==> {
218    let prev = extract_nth(s, i - 1);
219    prev < result &&
220    T1::well_founded_relation(s[prev].0, s[result].0)
221})]
222#[variant(i)]
223fn extract_nth<T1: WellFounded, T2: WellFounded>(s: Mapping<Int, (T1, T2)>, i: Int) -> Int {
224    if i == 0 {
225        0
226    } else {
227        let prev = extract_nth(s, i - 1);
228        extract_next_decr(s, prev)
229    }
230}
231
232/// Prove that `s` being infinitely decreasing is contradictory, by extracting
233/// a sequence such that the first component decreases.
234#[logic]
235#[requires(forall<i> 0 <= i ==> <(T1, T2)>::well_founded_relation(s[i], s[i + 1]))]
236#[ensures(forall<i> 0 <= i ==> T1::well_founded_relation(result[i], result[i + 1]))]
237fn first_component_decr<T1: WellFounded, T2: WellFounded>(
238    s: Mapping<Int, (T1, T2)>,
239) -> Mapping<Int, T1> {
240    |i| if 0 <= i { s[extract_nth(s, i)].0 } else { any() }
241}
creusot_std/logic/well_founded.rs

creusot_std/logic/
well_founded.rs
