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

creusot_contracts/logic/
well_founded.rs
