creusot_contracts/logic/
ord.rs

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

creusot_contracts/logic/
ord.rs
