creusot_std/logic/
well_founded.rs

1#[cfg(creusot)]
2use crate::logic::{Mapping, such_that, unreachable};
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                    if exists<r> r >= 0 && !Self::well_founded_relation(s[r], s[r + 1]) {
174                        such_that(|r| r >= 0 && !Self::well_founded_relation(s[r], s[r + 1]))
175                    } else {
176                        let _ = T0::no_infinite_decreasing_sequence(first_component_decr(|i| s[i].tuple_to_pair()));
177                        unreachable()
178                    }
179                }
180            }
181        }
182    };
183    ( @wf_relation $name1:ident $name2:ident {$($res:expr)?} [$($to_eq:tt)*] $t:ident = $idx:tt $($ts:ident = $idxs:tt)* ) => {
184        wf_tuples!{ @wf_relation $name1 $name2
185            {$($res ||)? ($(($name1 . $to_eq == $name2 . $to_eq ) &&)* $t::well_founded_relation($name1 . $idx, $name2 . $idx))}
186            [$($to_eq)* $idx]
187            $($ts=$idxs)*
188        }
189    };
190    ( @wf_relation $name1:ident $name2:ident {$res:expr} [$($to_eq:tt)*] ) => {
191        #[logic(open, inline)]
192        fn well_founded_relation($name1, $name2: Self) -> bool {
193            $res
194        }
195    };
196}
197
198wf_tuples!(T0 = 0, T1 = 1, T2 = 2, T3 = 3, T4 = 4, T5 = 5, T6 = 6, T7 = 7);
199
200/// Get an index > i, such that `s[index] < s[i]`.
201#[logic]
202#[requires(forall<i> 0 <= i ==> <(T1, T2)>::well_founded_relation(s[i], s[i + 1]))]
203#[requires(0 <= i)]
204#[ensures(i < result)]
205#[ensures(T1::well_founded_relation(s[i].0, s[result].0))]
206#[variant(s[i].1)]
207fn extract_next_decr<T1: WellFounded, T2: WellFounded>(s: Mapping<Int, (T1, T2)>, i: Int) -> Int {
208    if T1::well_founded_relation(s[i].0, s[i + 1].0) { i + 1 } else { extract_next_decr(s, i + 1) }
209}
210
211/// Used to construct [`first_component_decr`] below.
212#[logic]
213#[requires(forall<i> 0 <= i ==> <(T1, T2)>::well_founded_relation(s[i], s[i + 1]))]
214#[requires(0 <= i)]
215#[ensures(0 <= result)]
216#[ensures(0 < i ==> {
217    let prev = extract_nth(s, i - 1);
218    prev < result &&
219    T1::well_founded_relation(s[prev].0, s[result].0)
220})]
221#[variant(i)]
222fn extract_nth<T1: WellFounded, T2: WellFounded>(s: Mapping<Int, (T1, T2)>, i: Int) -> Int {
223    if i == 0 {
224        0
225    } else {
226        let prev = extract_nth(s, i - 1);
227        extract_next_decr(s, prev)
228    }
229}
230
231/// Prove that `s` being infinitely decreasing is contradictory, by extracting
232/// a sequence such that the first component decreases.
233#[logic]
234#[requires(forall<i> 0 <= i ==> <(T1, T2)>::well_founded_relation(s[i], s[i + 1]))]
235#[ensures(forall<i> 0 <= i ==> T1::well_founded_relation(result[i], result[i + 1]))]
236fn first_component_decr<T1: WellFounded, T2: WellFounded>(
237    s: Mapping<Int, (T1, T2)>,
238) -> Mapping<Int, T1> {
239    |i| if 0 <= i { s[extract_nth(s, i)].0 } else { such_that(|_| true) }
240}
creusot_std/logic/well_founded.rs

creusot_std/logic/
well_founded.rs
