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 satisfy some properties (see [`PartialOrd`] trait in Rust).
9///
10/// In particular, the order must be:
11/// - [irreflexive](Self::irreflexive)
12/// - [transitive](Self::transitive)
13///
14pub trait PartialOrdLogic {
15    /// The logical `<` operation.
16    #[logic]
17    fn lt_log(self, other: Self) -> bool;
18
19    /// The logical `>` operation.
20    #[logic(open, inline, sealed)]
21    fn gt_log(self, other: Self) -> bool {
22        other < self
23    }
24
25    /// The logical `<=` operation.
26    #[logic(open, inline)]
27    fn le_log(self, other: Self) -> bool {
28        pearlite! { self < other || self == other }
29    }
30
31    /// The logical `>=` operation.
32    #[logic(open, inline, sealed)]
33    fn ge_log(self, other: Self) -> bool {
34        other <= self
35    }
36
37    #[logic(law)]
38    #[ensures(!(self < self))]
39    fn irreflexive(self);
40
41    #[logic(law)]
42    #[requires(x < y)]
43    #[requires(y < z)]
44    #[ensures(x < z)]
45    fn transitive(x: Self, y: Self, z: Self);
46
47    #[logic(law)]
48    #[ensures((self <= other) == (self < other || self == other))]
49    fn le_lt_log(self, other: Self);
50
51    #[logic(open, sealed)]
52    fn partial_cmp_log(self, other: Self) -> Option<Ordering> {
53        if self == other {
54            Some(Ordering::Equal)
55        } else if self < other {
56            Some(Ordering::Less)
57        } else if other < self {
58            Some(Ordering::Greater)
59        } else {
60            None
61        }
62    }
63}
64
65/// Types that implement this trait must have a total order ([`Ord`] trait in Rust).
66#[allow(unused)]
67pub trait OrdLogic: PartialOrdLogic {
68    /// The order is total
69    #[logic(law)]
70    #[ensures(self < other || self == other || other < self)]
71    fn lt_log_total(self, other: Self);
72
73    /// The comparison operation.
74    #[logic(open, sealed)]
75    fn cmp_log(self, other: Self) -> Ordering {
76        if self == other {
77            Ordering::Equal
78        } else if self < other {
79            Ordering::Less
80        } else {
81            Ordering::Greater
82        }
83    }
84}
85
86/// A macro to easily implements the various `#[logic(law)]`s of [`PartialOrdLogic`].
87///
88/// # Usage
89///
90/// Simply use this macro in the trait impl:
91/// ```
92/// # use creusot_std::{logic::ord::{PartialOrdLogic, partial_ord_laws_impl}, prelude::*};
93/// use std::cmp::Ordering;
94/// struct MyInt(Int);
95///
96/// impl PartialOrdLogic for MyInt {
97///     #[logic(open)]
98///     fn lt_log(self, other: Self) -> bool { todo!() }
99///
100///     partial_ord_laws_impl! {}
101/// }
102///
103/// impl OrdLogic for MyInt {
104///     #[logic(law)]
105///     #[ensures(self < other || self == other || other < self)]
106///     fn lt_log_total(self, other: Self) {}
107/// }
108/// ```
109///
110/// Additionally, you can define instructions that will be injected in every generated
111/// law's body. This can be useful to apply a lemma to every law:
112///
113/// ```
114/// # use creusot_std::{logic::ord::{PartialOrdLogic, partial_ord_laws_impl}, prelude::*};
115/// #[opaque]
116/// pub struct MyInt(());
117///
118/// impl View for MyInt {
119///     type ViewTy = Int;
120///     #[logic(opaque)] fn view(self) -> Int { dead }
121/// }
122///
123/// impl MyInt {
124///     #[trusted]
125///     #[logic]
126///     #[ensures(self@ == other@ ==> self == other)]
127///     fn view_inj(self, other: Self) {}
128/// }
129///
130/// impl PartialOrdLogic for MyInt {
131///     #[logic(open)]
132///     fn lt_log(self, other: Self) -> bool { todo!() }
133///
134///     partial_ord_laws_impl! { let _ = MyInt::view_inj; }
135/// }
136/// ```
137#[macro_export]
138macro_rules! partial_ord_laws_impl {
139    ( $($lemma:stmt)* ) => {
140        #[::creusot_std::macros::logic(law)]
141        #[::creusot_std::macros::ensures(!(self < self))]
142        fn irreflexive(self) {
143            $($lemma)*
144        }
145
146        #[::creusot_std::macros::logic(law)]
147        #[::creusot_std::macros::requires(x < y)]
148        #[::creusot_std::macros::requires(y < z)]
149        #[::creusot_std::macros::ensures(x < z)]
150        fn transitive(x: Self, y: Self, z: Self) {
151            $($lemma)*
152        }
153
154        #[::creusot_std::macros::logic(law)]
155        #[::creusot_std::macros::ensures((self <= other) == (self < other || self == other))]
156        fn le_lt_log(self, other: Self) {
157            $($lemma)*
158        }
159    };
160}
161
162pub use partial_ord_laws_impl;
163
164impl<T: PartialOrdLogic> PartialOrdLogic for &T {
165    #[logic(open, inline)]
166    fn lt_log(self, other: Self) -> bool {
167        *self < *other
168    }
169
170    #[logic(open, inline)]
171    fn le_log(self, other: Self) -> bool {
172        *self <= *other
173    }
174
175    partial_ord_laws_impl! {}
176}
177
178impl<T: OrdLogic> OrdLogic for &T {
179    #[logic]
180    #[ensures(self < other || self == other || other < self)]
181    fn lt_log_total(self, other: Self) {
182        let _ = T::lt_log_total;
183    }
184}
185
186impl PartialOrdLogic for Int {
187    #[logic]
188    #[builtin("int.Int.(<=)")]
189    fn le_log(self, _: Self) -> bool {
190        dead
191    }
192
193    #[logic]
194    #[builtin("int.Int.(<)")]
195    fn lt_log(self, _: Self) -> bool {
196        dead
197    }
198
199    #[logic]
200    #[ensures(!(self < self))]
201    fn irreflexive(self) {}
202
203    #[logic]
204    #[requires(x < y)]
205    #[requires(y < z)]
206    #[ensures(x < z)]
207    fn transitive(x: Self, y: Self, z: Self) {}
208
209    #[logic]
210    #[ensures((self <= other) == (self < other || self == other))]
211    fn le_lt_log(self, other: Self) {}
212}
213
214impl OrdLogic for Int {
215    #[logic]
216    #[ensures(self < other || self == other || other < self)]
217    fn lt_log_total(self, other: Self) {}
218}
219
220macro_rules! ord_logic_impl {
221    ($t:ty, $module:literal) => {
222        impl PartialOrdLogic for $t {
223            #[logic]
224            #[builtin(concat!($module, ".le"))]
225            fn le_log(self, _: Self) -> bool {
226                dead
227            }
228
229            #[logic]
230            #[builtin(concat!($module, ".lt"))]
231            fn lt_log(self, _: Self) -> bool {
232                dead
233            }
234
235            #[logic]
236            #[ensures(!(self < self))]
237            fn irreflexive(self) {}
238
239            #[logic]
240            #[requires(x < y)]
241            #[requires(y < z)]
242            #[ensures(x < z)]
243            fn transitive(x: Self, y: Self, z: Self) {}
244
245            #[logic]
246            #[ensures((self <= other) == (self < other || self == other))]
247            fn le_lt_log(self, other: Self) {}
248        }
249
250        impl OrdLogic for $t {
251            #[logic]
252            #[ensures(self < other || self == other || other < self)]
253            fn lt_log_total(self, other: Self) {}
254        }
255    };
256}
257
258impl PartialOrdLogic for f32 {
259    /// Note: the implementation of `f32::le_log` is not the `<=` operator in Rust,
260    /// because it is reflexive.
261    #[logic]
262    #[builtin("creusot.float.Float32.lt")]
263    fn lt_log(self, _: Self) -> bool {
264        dead
265    }
266
267    #[logic]
268    #[ensures(!(self < self))]
269    fn irreflexive(self) {}
270
271    #[logic]
272    #[requires(x < y)]
273    #[requires(y < z)]
274    #[ensures(x < z)]
275    fn transitive(x: Self, y: Self, z: Self) {}
276
277    #[logic]
278    #[ensures((self <= other) == (self < other || self == other))]
279    fn le_lt_log(self, other: Self) {}
280}
281
282impl PartialOrdLogic for f64 {
283    /// Note: the implementation of `f64::le_log` is not the `<=` operator in Rust,
284    /// because it is reflexive.
285    #[logic]
286    #[builtin("creusot.float.Float64.lt")]
287    fn lt_log(self, _: Self) -> bool {
288        dead
289    }
290
291    #[logic]
292    #[ensures(!(self < self))]
293    fn irreflexive(self) {}
294
295    #[logic]
296    #[requires(x < y)]
297    #[requires(y < z)]
298    #[ensures(x < z)]
299    fn transitive(x: Self, y: Self, z: Self) {}
300
301    #[logic]
302    #[ensures((self <= other) == (self < other || self == other))]
303    fn le_lt_log(self, other: Self) {}
304}
305
306ord_logic_impl!(u8, "creusot.int.UInt8$BW$");
307ord_logic_impl!(u16, "creusot.int.UInt16$BW$");
308ord_logic_impl!(u32, "creusot.int.UInt32$BW$");
309ord_logic_impl!(u64, "creusot.int.UInt64$BW$");
310ord_logic_impl!(u128, "creusot.int.UInt128$BW$");
311#[cfg(target_pointer_width = "64")]
312ord_logic_impl!(usize, "creusot.int.UInt64$BW$");
313#[cfg(target_pointer_width = "32")]
314ord_logic_impl!(usize, "creusot.int.UInt32$BW$");
315#[cfg(target_pointer_width = "16")]
316ord_logic_impl!(usize, "creusot.int.UInt16$BW$");
317
318ord_logic_impl!(i8, "creusot.int.Int8$BW$");
319ord_logic_impl!(i16, "creusot.int.Int16$BW$");
320ord_logic_impl!(i32, "creusot.int.Int32$BW$");
321ord_logic_impl!(i64, "creusot.int.Int64$BW$");
322ord_logic_impl!(i128, "creusot.int.Int128$BW$");
323#[cfg(target_pointer_width = "64")]
324ord_logic_impl!(isize, "creusot.int.Int64$BW$");
325#[cfg(target_pointer_width = "32")]
326ord_logic_impl!(isize, "creusot.int.Int32$BW$");
327#[cfg(target_pointer_width = "16")]
328ord_logic_impl!(isize, "creusot.int.Int16$BW$");
329
330ord_logic_impl!(char, "creusot.prelude.Char");
331ord_logic_impl!(bool, "creusot.prelude.Bool");
332
333impl<A: PartialOrdLogic, B: PartialOrdLogic> PartialOrdLogic for (A, B) {
334    #[logic(open)]
335    fn lt_log(self, o: Self) -> bool {
336        self.0 == o.0 && self.1 < o.1 || self.0 < o.0
337    }
338
339    #[logic(open)]
340    fn le_log(self, o: Self) -> bool {
341        self.0 == o.0 && self.1 <= o.1 || self.0 < o.0
342    }
343
344    partial_ord_laws_impl! {}
345}
346
347impl<A: OrdLogic, B: OrdLogic> OrdLogic for (A, B) {
348    #[logic]
349    #[ensures(self < other || self == other || other < self)]
350    fn lt_log_total(self, other: Self) {
351        let _ = A::lt_log_total;
352        let _ = B::lt_log_total;
353    }
354}
creusot_std/logic/ord.rs

creusot_std/logic/
ord.rs
