creusot_std/logic/
ord.rs

1//! Definition for using orderings in pearlite.
2
3use crate::prelude::*;
4use core::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_std::{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///
122/// Additionally, you can define instructions that will be injected in every generated
123/// law's body. This can be useful to apply a lemma to every law:
124///
125/// ```
126/// # use creusot_std::{logic::ord::{OrdLogic, ord_laws_impl}, prelude::*};
127/// #[opaque]
128/// pub struct MyInt(());
129///
130/// impl View for MyInt {
131///     type ViewTy = Int;
132///     #[logic(opaque)] fn view(self) -> Int { dead }
133/// }
134///
135/// impl MyInt {
136///     #[trusted]
137///     #[logic]
138///     #[ensures(self@ == other@ ==> self == other)]
139///     fn view_inj(self, other: Self) {}
140/// }
141///
142/// impl OrdLogic for MyInt {
143///     #[logic(open)]
144///     fn cmp_log(self, other: Self) -> Ordering { pearlite! { self@.cmp_log(other@) } }
145/// #    #[logic]
146/// #    fn le_log(self, other: Self) -> bool { todo!() }
147/// #    #[logic]
148/// #    fn lt_log(self, other: Self) -> bool { todo!() }
149/// #    #[logic]
150/// #    fn ge_log(self, other: Self) -> bool { todo!() }
151/// #    #[logic]
152/// #    fn gt_log(self, other: Self) -> bool { todo!() }
153///     // ...
154///
155///     ord_laws_impl! { let _ = MyInt::view_inj; }
156/// }
157/// ```
158#[macro_export]
159macro_rules! ord_laws_impl {
160    ( $($lemma:stmt)* ) => {
161        #[::creusot_std::macros::logic(open(self), law)]
162        #[::creusot_std::macros::ensures(x.le_log(y) == (x.cmp_log(y) != Ordering::Greater))]
163        fn cmp_le_log(x: Self, y: Self) {
164            $($lemma)*
165        }
166
167        #[::creusot_std::macros::logic(open(self), law)]
168        #[::creusot_std::macros::ensures(x.lt_log(y) == (x.cmp_log(y) == Ordering::Less))]
169        fn cmp_lt_log(x: Self, y: Self) {
170            $($lemma)*
171        }
172
173        #[::creusot_std::macros::logic(open(self), law)]
174        #[::creusot_std::macros::ensures(x.ge_log(y) == (x.cmp_log(y) != Ordering::Less))]
175        fn cmp_ge_log(x: Self, y: Self) {
176            $($lemma)*
177        }
178
179        #[::creusot_std::macros::logic(open(self), law)]
180        #[::creusot_std::macros::ensures(x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater))]
181        fn cmp_gt_log(x: Self, y: Self) {
182            $($lemma)*
183        }
184
185        #[::creusot_std::macros::logic(open(self), law)]
186        #[::creusot_std::macros::ensures(x.cmp_log(x) == Ordering::Equal)]
187        fn refl(x: Self) {
188            $($lemma)*
189        }
190
191        #[::creusot_std::macros::logic(open(self), law)]
192        #[::creusot_std::macros::requires(x.cmp_log(y) == o)]
193        #[::creusot_std::macros::requires(y.cmp_log(z) == o)]
194        #[::creusot_std::macros::ensures(x.cmp_log(z) == o)]
195        fn trans(x: Self, y: Self, z: Self, o: Ordering) {
196            $($lemma)*
197        }
198
199        #[::creusot_std::macros::logic(open(self), law)]
200        #[::creusot_std::macros::requires(x.cmp_log(y) == Ordering::Less)]
201        #[::creusot_std::macros::ensures(y.cmp_log(x) == Ordering::Greater)]
202        fn antisym1(x: Self, y: Self) {
203            $($lemma)*
204        }
205
206        #[::creusot_std::macros::logic(open(self), law)]
207        #[::creusot_std::macros::requires(x.cmp_log(y) == Ordering::Greater)]
208        #[::creusot_std::macros::ensures(y.cmp_log(x) == Ordering::Less)]
209        fn antisym2(x: Self, y: Self) {
210            $($lemma)*
211        }
212
213        #[::creusot_std::macros::logic(open(self), law)]
214        #[::creusot_std::macros::ensures((x == y) == (x.cmp_log(y) == Ordering::Equal))]
215        fn eq_cmp(x: Self, y: Self) {
216            $($lemma)*
217        }
218    };
219}
220
221pub use ord_laws_impl;
222
223impl<T: OrdLogic> OrdLogic for &T {
224    #[logic(open)]
225    fn cmp_log(self, o: Self) -> Ordering {
226        T::cmp_log(*self, *o)
227    }
228
229    #[logic]
230    fn le_log(self, other: Self) -> bool {
231        T::le_log(*self, *other)
232    }
233
234    #[logic]
235    fn lt_log(self, other: Self) -> bool {
236        T::lt_log(*self, *other)
237    }
238
239    #[logic]
240    fn ge_log(self, other: Self) -> bool {
241        T::ge_log(*self, *other)
242    }
243
244    #[logic]
245    fn gt_log(self, other: Self) -> bool {
246        T::gt_log(*self, *other)
247    }
248
249    ord_laws_impl! {}
250}
251
252impl OrdLogic for Int {
253    #[logic(open)]
254    fn cmp_log(self, o: Self) -> Ordering {
255        if self < o {
256            Ordering::Less
257        } else if self == o {
258            Ordering::Equal
259        } else {
260            Ordering::Greater
261        }
262    }
263
264    #[logic]
265    #[builtin("int.Int.(<=)")]
266    fn le_log(self, _: Self) -> bool {
267        dead
268    }
269
270    #[logic]
271    #[builtin("int.Int.(<)")]
272    fn lt_log(self, _: Self) -> bool {
273        dead
274    }
275
276    #[logic]
277    #[builtin("int.Int.(>=)")]
278    fn ge_log(self, _: Self) -> bool {
279        dead
280    }
281
282    #[logic]
283    #[builtin("int.Int.(>)")]
284    fn gt_log(self, _: Self) -> bool {
285        dead
286    }
287
288    ord_laws_impl! {}
289}
290
291macro_rules! ord_logic_impl {
292    ($t:ty, $module:literal) => {
293        impl OrdLogic for $t {
294            #[logic(open)]
295            fn cmp_log(self, o: Self) -> Ordering {
296                if self < o {
297                    Ordering::Less
298                } else if self == o {
299                    Ordering::Equal
300                } else {
301                    Ordering::Greater
302                }
303            }
304
305            #[logic]
306            #[builtin(concat!($module, ".le"))]
307            fn le_log(self, _: Self) -> bool {
308                true
309            }
310
311            #[logic]
312            #[builtin(concat!($module, ".lt"))]
313            fn lt_log(self, _: Self) -> bool {
314                true
315            }
316
317            #[logic]
318            #[builtin(concat!($module, ".ge"))]
319            fn ge_log(self, _: Self) -> bool {
320                true
321            }
322
323            #[logic]
324            #[builtin(concat!($module, ".gt"))]
325            fn gt_log(self, _: Self) -> bool {
326                true
327            }
328
329            ord_laws_impl! {}
330        }
331    };
332}
333
334ord_logic_impl!(u8, "creusot.int.UInt8$BW$");
335ord_logic_impl!(u16, "creusot.int.UInt16$BW$");
336ord_logic_impl!(u32, "creusot.int.UInt32$BW$");
337ord_logic_impl!(u64, "creusot.int.UInt64$BW$");
338ord_logic_impl!(u128, "creusot.int.UInt128$BW$");
339#[cfg(target_pointer_width = "64")]
340ord_logic_impl!(usize, "creusot.int.UInt64$BW$");
341#[cfg(target_pointer_width = "32")]
342ord_logic_impl!(usize, "creusot.int.UInt32$BW$");
343#[cfg(target_pointer_width = "16")]
344ord_logic_impl!(usize, "creusot.int.UInt16$BW$");
345
346ord_logic_impl!(i8, "creusot.int.Int8$BW$");
347ord_logic_impl!(i16, "creusot.int.Int16$BW$");
348ord_logic_impl!(i32, "creusot.int.Int32$BW$");
349ord_logic_impl!(i64, "creusot.int.Int64$BW$");
350ord_logic_impl!(i128, "creusot.int.Int128$BW$");
351#[cfg(target_pointer_width = "64")]
352ord_logic_impl!(isize, "creusot.int.Int64$BW$");
353#[cfg(target_pointer_width = "32")]
354ord_logic_impl!(isize, "creusot.int.Int32$BW$");
355#[cfg(target_pointer_width = "16")]
356ord_logic_impl!(isize, "creusot.int.Int16$BW$");
357
358ord_logic_impl!(char, "creusot.prelude.Char");
359ord_logic_impl!(bool, "creusot.prelude.Bool");
360
361impl<A: OrdLogic, B: OrdLogic> OrdLogic for (A, B) {
362    #[logic(open)]
363    fn cmp_log(self, o: Self) -> Ordering {
364        pearlite! { {
365            let r = self.0.cmp_log(o.0);
366            if r == Ordering::Equal {
367                self.1.cmp_log(o.1)
368            } else {
369                r
370            }
371        } }
372    }
373
374    #[logic(open)]
375    fn le_log(self, o: Self) -> bool {
376        pearlite! { (self.0 == o.0 && self.1 <= o.1) || self.0 < o.0 }
377    }
378
379    #[logic(open)]
380    fn lt_log(self, o: Self) -> bool {
381        pearlite! { (self.0 == o.0 && self.1 < o.1) || self.0 < o.0 }
382    }
383
384    #[logic(open)]
385    fn ge_log(self, o: Self) -> bool {
386        pearlite! { (self.0 == o.0 && self.1 >= o.1) || self.0 > o.0 }
387    }
388
389    #[logic(open)]
390    fn gt_log(self, o: Self) -> bool {
391        pearlite! { (self.0 == o.0 && self.1 > o.1) || self.0 > o.0 }
392    }
393
394    ord_laws_impl! {}
395}
creusot_std/logic/ord.rs

creusot_std/logic/
ord.rs
