creusot_contracts/logic/
ord.rs

1//! Definition for using orderings in pearlite.
2
3use crate::prelude::*;
4use std::cmp::Ordering;
5
6/// Trait for comparison operations (`<`, `>`, `<=`, `>=`) in pearlite.
7///
8/// Types that implement this trait must have a total order. In particular, the order
9/// must be:
10/// - [reflexive](Self::refl)
11/// - [transitive](Self::trans)
12/// - antisymmetric ([part1](Self::antisym1), [part2](Self::antisym2))
13#[allow(unused)]
14pub trait OrdLogic {
15    /// The comparison operation. Returns:
16    /// - [`Ordering::Less`] if `self` is smaller than `other`
17    /// - [`Ordering::Equal`] if `self` is equal to `other`
18    /// - [`Ordering::Greater`] if `self` is greater than `other`
19    #[logic]
20    fn cmp_log(self, other: Self) -> Ordering;
21
22    /// The logical `<=` operation.
23    #[logic(open)]
24    fn le_log(self, o: Self) -> bool {
25        pearlite! { self.cmp_log(o) != Ordering::Greater }
26    }
27
28    #[logic(law)]
29    #[ensures(x.le_log(y) == (x.cmp_log(y) != Ordering::Greater))]
30    fn cmp_le_log(x: Self, y: Self);
31
32    /// The logical `<` operation.
33    #[logic(open)]
34    fn lt_log(self, o: Self) -> bool {
35        pearlite! { self.cmp_log(o) == Ordering::Less }
36    }
37
38    #[logic(law)]
39    #[ensures(x.lt_log(y) == (x.cmp_log(y) == Ordering::Less))]
40    fn cmp_lt_log(x: Self, y: Self);
41
42    /// The logical `>=` operation.
43    #[logic(open)]
44    fn ge_log(self, o: Self) -> bool {
45        pearlite! { self.cmp_log(o) != Ordering::Less }
46    }
47
48    #[logic(law)]
49    #[ensures(x.ge_log(y) == (x.cmp_log(y) != Ordering::Less))]
50    fn cmp_ge_log(x: Self, y: Self);
51
52    /// The logical `>` operation.
53    #[logic(open)]
54    fn gt_log(self, o: Self) -> bool {
55        pearlite! { self.cmp_log(o) == Ordering::Greater }
56    }
57
58    #[logic(law)]
59    #[ensures(x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater))]
60    fn cmp_gt_log(x: Self, y: Self);
61
62    /// Reflexivity of the order
63    #[logic(law)]
64    #[ensures(x.cmp_log(x) == Ordering::Equal)]
65    fn refl(x: Self);
66
67    /// Transitivity of the order
68    #[logic(law)]
69    #[requires(x.cmp_log(y) == o)]
70    #[requires(y.cmp_log(z) == o)]
71    #[ensures(x.cmp_log(z) == o)]
72    fn trans(x: Self, y: Self, z: Self, o: Ordering);
73
74    /// Antisymmetry of the order (`x < y ==> !(y < x)`)
75    ///
76    /// The antisymmetry is in two part; here is the [second](Self::antisym2) part.
77    #[logic(law)]
78    #[requires(x.cmp_log(y) == Ordering::Less)]
79    #[ensures(y.cmp_log(x) == Ordering::Greater)]
80    fn antisym1(x: Self, y: Self);
81
82    /// Antisymmetry of the order (`x > y ==> !(y > x)`)
83    ///
84    /// The antisymmetry is in two part; here is the [first](Self::antisym1) part.
85    #[logic(law)]
86    #[requires(x.cmp_log(y) == Ordering::Greater)]
87    #[ensures(y.cmp_log(x) == Ordering::Less)]
88    fn antisym2(x: Self, y: Self);
89
90    /// Compatibility between [`Ordering::Equal`] and equality (`==`).
91    #[logic(law)]
92    #[ensures((x == y) == (x.cmp_log(y) == Ordering::Equal))]
93    fn eq_cmp(x: Self, y: Self);
94}
95
96/// A macro to easily implements the various `#[logic(law)]`s of [`OrdLogic`].
97///
98/// # Usage
99///
100/// Simply use this macro in the trait impl:
101/// ```
102/// # use creusot_contracts::{logic::ord::{OrdLogic, ord_laws_impl}, prelude::*};
103/// use std::cmp::Ordering;
104/// struct MyInt(Int);
105///
106/// impl OrdLogic for MyInt {
107///     #[logic]
108///     fn cmp_log(self, other: Self) -> Ordering { todo!() }
109///     #[logic]
110///     fn le_log(self, other: Self) -> bool { todo!() }
111///     #[logic]
112///     fn lt_log(self, other: Self) -> bool { todo!() }
113///     #[logic]
114///     fn ge_log(self, other: Self) -> bool { todo!() }
115///     #[logic]
116///     fn gt_log(self, other: Self) -> bool { todo!() }
117///
118///     ord_laws_impl! {}
119/// }
120/// ```
121#[macro_export]
122macro_rules! ord_laws_impl {
123    () => {
124        #[::creusot_contracts::macros::logic(open(self), law)]
125        #[::creusot_contracts::macros::ensures(x.le_log(y) == (x.cmp_log(y) != Ordering::Greater))]
126        fn cmp_le_log(x: Self, y: Self) {}
127
128        #[::creusot_contracts::macros::logic(open(self), law)]
129        #[::creusot_contracts::macros::ensures(x.lt_log(y) == (x.cmp_log(y) == Ordering::Less))]
130        fn cmp_lt_log(x: Self, y: Self) {}
131
132        #[::creusot_contracts::macros::logic(open(self), law)]
133        #[::creusot_contracts::macros::ensures(x.ge_log(y) == (x.cmp_log(y) != Ordering::Less))]
134        fn cmp_ge_log(x: Self, y: Self) {}
135
136        #[::creusot_contracts::macros::logic(open(self), law)]
137        #[::creusot_contracts::macros::ensures(x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater))]
138        fn cmp_gt_log(x: Self, y: Self) {}
139
140        #[::creusot_contracts::macros::logic(open(self), law)]
141        #[::creusot_contracts::macros::ensures(x.cmp_log(x) == Ordering::Equal)]
142        fn refl(x: Self) {}
143
144        #[::creusot_contracts::macros::logic(open(self), law)]
145        #[::creusot_contracts::macros::requires(x.cmp_log(y) == o)]
146        #[::creusot_contracts::macros::requires(y.cmp_log(z) == o)]
147        #[::creusot_contracts::macros::ensures(x.cmp_log(z) == o)]
148        fn trans(x: Self, y: Self, z: Self, o: Ordering) {}
149
150        #[::creusot_contracts::macros::logic(open(self), law)]
151        #[::creusot_contracts::macros::requires(x.cmp_log(y) == Ordering::Less)]
152        #[::creusot_contracts::macros::ensures(y.cmp_log(x) == Ordering::Greater)]
153        fn antisym1(x: Self, y: Self) {}
154
155        #[::creusot_contracts::macros::logic(open(self), law)]
156        #[::creusot_contracts::macros::requires(x.cmp_log(y) == Ordering::Greater)]
157        #[::creusot_contracts::macros::ensures(y.cmp_log(x) == Ordering::Less)]
158        fn antisym2(x: Self, y: Self) {}
159
160        #[::creusot_contracts::macros::logic(open(self), law)]
161        #[::creusot_contracts::macros::ensures((x == y) == (x.cmp_log(y) == Ordering::Equal))]
162        fn eq_cmp(x: Self, y: Self) {}
163    };
164}
165
166pub use ord_laws_impl;
167
168impl<T: OrdLogic> OrdLogic for &T {
169    #[logic(open)]
170    fn cmp_log(self, o: Self) -> Ordering {
171        T::cmp_log(*self, *o)
172    }
173
174    #[logic]
175    fn le_log(self, other: Self) -> bool {
176        T::le_log(*self, *other)
177    }
178
179    #[logic]
180    fn lt_log(self, other: Self) -> bool {
181        T::lt_log(*self, *other)
182    }
183
184    #[logic]
185    fn ge_log(self, other: Self) -> bool {
186        T::ge_log(*self, *other)
187    }
188
189    #[logic]
190    fn gt_log(self, other: Self) -> bool {
191        T::gt_log(*self, *other)
192    }
193
194    ord_laws_impl! {}
195}
196
197impl OrdLogic for Int {
198    #[logic(open)]
199    fn cmp_log(self, o: Self) -> Ordering {
200        if self < o {
201            Ordering::Less
202        } else if self == o {
203            Ordering::Equal
204        } else {
205            Ordering::Greater
206        }
207    }
208
209    #[logic]
210    #[builtin("mach.int.Int.(<=)")]
211    fn le_log(self, _: Self) -> bool {
212        dead
213    }
214
215    #[logic]
216    #[builtin("mach.int.Int.(<)")]
217    fn lt_log(self, _: Self) -> bool {
218        dead
219    }
220
221    #[logic]
222    #[builtin("mach.int.Int.(>=)")]
223    fn ge_log(self, _: Self) -> bool {
224        dead
225    }
226
227    #[logic]
228    #[builtin("mach.int.Int.(>)")]
229    fn gt_log(self, _: Self) -> bool {
230        dead
231    }
232
233    ord_laws_impl! {}
234}
235
236macro_rules! ord_logic_impl {
237    ($t:ty, $module:literal) => {
238        impl OrdLogic for $t {
239            #[logic(open)]
240            fn cmp_log(self, o: Self) -> Ordering {
241                if self < o {
242                    Ordering::Less
243                } else if self == o {
244                    Ordering::Equal
245                } else {
246                    Ordering::Greater
247                }
248            }
249
250            #[logic]
251            #[builtin(concat!($module, ".le"))]
252            fn le_log(self, _: Self) -> bool {
253                true
254            }
255
256            #[logic]
257            #[builtin(concat!($module, ".lt"))]
258            fn lt_log(self, _: Self) -> bool {
259                true
260            }
261
262            #[logic]
263            #[builtin(concat!($module, ".ge"))]
264            fn ge_log(self, _: Self) -> bool {
265                true
266            }
267
268            #[logic]
269            #[builtin(concat!($module, ".gt"))]
270            fn gt_log(self, _: Self) -> bool {
271                true
272            }
273
274            ord_laws_impl! {}
275        }
276    };
277}
278
279ord_logic_impl!(u8, "creusot.int.UInt8$BW$");
280ord_logic_impl!(u16, "creusot.int.UInt16$BW$");
281ord_logic_impl!(u32, "creusot.int.UInt32$BW$");
282ord_logic_impl!(u64, "creusot.int.UInt64$BW$");
283ord_logic_impl!(u128, "creusot.int.UInt128$BW$");
284#[cfg(target_pointer_width = "64")]
285ord_logic_impl!(usize, "creusot.int.UInt64$BW$");
286#[cfg(target_pointer_width = "32")]
287ord_logic_impl!(usize, "creusot.int.UInt32$BW$");
288#[cfg(target_pointer_width = "16")]
289ord_logic_impl!(usize, "creusot.int.UInt16$BW$");
290
291ord_logic_impl!(i8, "creusot.int.Int8$BW$");
292ord_logic_impl!(i16, "creusot.int.Int16$BW$");
293ord_logic_impl!(i32, "creusot.int.Int32$BW$");
294ord_logic_impl!(i64, "creusot.int.Int64$BW$");
295ord_logic_impl!(i128, "creusot.int.Int128$BW$");
296#[cfg(target_pointer_width = "64")]
297ord_logic_impl!(isize, "creusot.int.Int64$BW$");
298#[cfg(target_pointer_width = "32")]
299ord_logic_impl!(isize, "creusot.int.Int32$BW$");
300#[cfg(target_pointer_width = "16")]
301ord_logic_impl!(isize, "creusot.int.Int16$BW$");
302
303ord_logic_impl!(char, "creusot.prelude.Char");
304ord_logic_impl!(bool, "creusot.prelude.Bool");
305
306impl<A: OrdLogic, B: OrdLogic> OrdLogic for (A, B) {
307    #[logic(open)]
308    fn cmp_log(self, o: Self) -> Ordering {
309        pearlite! { {
310            let r = self.0.cmp_log(o.0);
311            if r == Ordering::Equal {
312                self.1.cmp_log(o.1)
313            } else {
314                r
315            }
316        } }
317    }
318
319    #[logic(open)]
320    fn le_log(self, o: Self) -> bool {
321        pearlite! { (self.0 == o.0 && self.1 <= o.1) || self.0 < o.0 }
322    }
323
324    #[logic(open)]
325    fn lt_log(self, o: Self) -> bool {
326        pearlite! { (self.0 == o.0 && self.1 < o.1) || self.0 < o.0 }
327    }
328
329    #[logic(open)]
330    fn ge_log(self, o: Self) -> bool {
331        pearlite! { (self.0 == o.0 && self.1 >= o.1) || self.0 > o.0 }
332    }
333
334    #[logic(open)]
335    fn gt_log(self, o: Self) -> bool {
336        pearlite! { (self.0 == o.0 && self.1 > o.1) || self.0 > o.0 }
337    }
338
339    ord_laws_impl! {}
340}
creusot_contracts/logic/ord.rs

creusot_contracts/logic/
ord.rs
