vstd/std_specs/
cmp.rs

1use super::super::prelude::*;
2
3use core::cmp::{Eq, Ord, Ordering, PartialEq, PartialOrd};
4use core::marker::PointeeSized;
5
6use verus as verus_skip_verusfmt;
7verus_skip_verusfmt! {
8
9#[verifier::external_trait_specification]
10#[verifier::external_trait_extension(PartialEqSpec via PartialEqSpecImpl)]
11pub trait ExPartialEq<Rhs: PointeeSized = Self>: PointeeSized {
12    type ExternalTraitSpecificationFor: PartialEq<Rhs>;
13
14    spec fn obeys_eq_spec() -> bool;
15
16    spec fn eq_spec(&self, other: &Rhs) -> bool;
17
18    fn eq(&self, other: &Rhs) -> (r: bool)
19        ensures
20            Self::obeys_eq_spec() ==> r == self.eq_spec(other);
21
22    fn ne(&self, other: &Rhs) -> (r: bool)
23        ensures
24            Self::obeys_eq_spec() ==> r == !self.eq_spec(other),
25        default_ensures
26            call_ensures(Self::eq, (self, other), !r);
27}
28
29#[verifier::external_trait_specification]
30pub trait ExEq: PartialEq + PointeeSized {
31    type ExternalTraitSpecificationFor: Eq;
32}
33
34#[verifier::external_type_specification]
35#[verifier::external_body]
36#[verifier::accept_recursive_types(T)]
37pub struct ExAssertParamIsEq<T: Eq + PointeeSized>(core::cmp::AssertParamIsEq<T>);
38
39#[verifier::external_trait_specification]
40#[verifier::external_trait_extension(PartialOrdSpec via PartialOrdSpecImpl)]
41pub trait ExPartialOrd<Rhs: PointeeSized = Self>: PartialEq<Rhs> + PointeeSized {
42    type ExternalTraitSpecificationFor: PartialOrd<Rhs>;
43
44    spec fn obeys_partial_cmp_spec() -> bool;
45
46    spec fn partial_cmp_spec(&self, other: &Rhs) -> Option<Ordering>;
47
48    fn partial_cmp(&self, other: &Rhs) -> (r: Option<Ordering>)
49        ensures
50            Self::obeys_partial_cmp_spec() ==> r == self.partial_cmp_spec(other);
51
52    fn lt(&self, other: &Rhs) -> (r: bool)
53        ensures
54            Self::obeys_partial_cmp_spec() ==>
55                (r <==> self.partial_cmp_spec(other) == Some(Ordering::Less)),
56        default_ensures
57            exists|o: Option<Ordering>|
58                {
59                    &&& #[trigger] call_ensures(Self::partial_cmp, (self, other), o)
60                    &&& r <==> o == Some(Ordering::Less)
61                }
62    ;
63
64    fn le(&self, other: &Rhs) -> (r: bool)
65        ensures
66            Self::obeys_partial_cmp_spec() ==>
67                (r <==> self.partial_cmp_spec(other) matches Some(
68                    Ordering::Less
69                    | Ordering::Equal,
70                )),
71        default_ensures
72            exists|o: Option<Ordering>|
73                {
74                    &&& #[trigger] call_ensures(Self::partial_cmp, (self, other), o)
75                    &&& r <==> o matches Some(
76                        Ordering::Less
77                        | Ordering::Equal,
78                    )
79                }
80    ;
81
82    fn gt(&self, other: &Rhs) -> (r: bool)
83        ensures
84            Self::obeys_partial_cmp_spec() ==>
85                (r <==> self.partial_cmp_spec(other) == Some(Ordering::Greater)),
86        default_ensures
87            exists|o: Option<Ordering>|
88                {
89                    &&& #[trigger] call_ensures(Self::partial_cmp, (self, other), o)
90                    &&& r <==> o == Some(Ordering::Greater)
91                }
92    ;
93
94    fn ge(&self, other: &Rhs) -> (r: bool)
95        ensures
96            Self::obeys_partial_cmp_spec() ==>
97                (r <==> self.partial_cmp_spec(other) matches Some(
98                    Ordering::Greater
99                    | Ordering::Equal,
100                )),
101        default_ensures
102            exists|o: Option<Ordering>|
103                {
104                    &&& #[trigger] call_ensures(Self::partial_cmp, (self, other), o)
105                    &&& r <==> o matches Some(
106                        Ordering::Greater
107                        | Ordering::Equal,
108                    )
109                }
110    ;
111}
112
113#[verifier::external_trait_specification]
114#[verifier::external_trait_extension(OrdSpec via OrdSpecImpl)]
115pub trait ExOrd: Eq + PartialOrd + PointeeSized {
116    type ExternalTraitSpecificationFor: Ord;
117
118    spec fn obeys_cmp_spec() -> bool;
119
120    spec fn cmp_spec(&self, other: &Self) -> Ordering;
121
122    fn cmp(&self, other: &Self) -> (r: Ordering)
123        ensures
124            Self::obeys_cmp_spec() ==> r == self.cmp_spec(other);
125
126    fn max(self, other: Self) -> (r: Self)
127        ensures
128            Self::obeys_cmp_spec() ==> match other.cmp_spec(&self) {
129                Ordering::Less => r == self,
130                Ordering::Equal => r == other,
131                Ordering::Greater => r == other,
132            }
133        default_ensures
134            exists|b: bool|
135                {
136                    &&& #[trigger] call_ensures(Self::lt, (&other, &self), b)
137                    &&& b ==> r == self
138                    &&& !b ==> r == other
139                }
140    ;
141
142    fn min(self, other: Self) -> (r: Self)
143        ensures
144            Self::obeys_cmp_spec() ==> match other.cmp_spec(&self) {
145                Ordering::Less => r == other,
146                Ordering::Equal => r == self,
147                Ordering::Greater => r == self,
148            }
149        default_ensures
150            exists|b: bool|
151                {
152                    &&& #[trigger] call_ensures(Self::lt, (&other, &self), b)
153                    &&& b ==> r == other
154                    &&& !b ==> r == self
155                }
156    ;
157
158    fn clamp(self, min: Self, max: Self) -> (r: Self)
159        requires
160            // There's an "assert!(min <= max)" in the provided clamp that must succeed, so:
161            Self::obeys_partial_cmp_spec(),
162            min.partial_cmp_spec(&max) matches Some(
163                Ordering::Less
164                | Ordering::Equal,
165            ),
166        ensures
167            Self::obeys_cmp_spec() ==> match (self.cmp_spec(&min), self.cmp_spec(&max)) {
168                (Ordering::Less, _) => r == min,
169                (_, Ordering::Greater) => r == max,
170                _ => r == self,
171            }
172        default_ensures
173            exists|b1: bool|
174                {
175                    &&& #[trigger] call_ensures(Self::lt, (&self, &min), b1)
176                    &&& b1 ==> r == min
177                    &&& !b1 ==> exists|b2: bool|
178                        {
179                            &&& #[trigger] call_ensures(Self::gt, (&self, &max), b2)
180                            &&& b2 ==> r == max
181                            &&& !b2 ==> r == self
182                        }
183                }
184    ;
185}
186
187pub trait PartialEqIs<Rhs: PointeeSized = Self>: PartialEq<Rhs> + PointeeSized {
188    spec fn is_eq(&self, other: &Rhs) -> bool;
189
190    spec fn is_ne(&self, other: &Rhs) -> bool;
191}
192
193pub trait PartialOrdIs<Rhs: PointeeSized = Self>: PartialOrd<Rhs> + PointeeSized {
194    spec fn is_lt(&self, other: &Rhs) -> bool;
195
196    spec fn is_le(&self, other: &Rhs) -> bool;
197
198    spec fn is_gt(&self, other: &Rhs) -> bool;
199
200    spec fn is_ge(&self, other: &Rhs) -> bool;
201}
202
203impl<A: PointeeSized + PartialEq<Rhs>, Rhs: PointeeSized> PartialEqIs<Rhs> for A {
204    #[verifier::inline]
205    open spec fn is_eq(&self, other: &Rhs) -> bool {
206        self.eq_spec(other)
207    }
208
209    #[verifier::inline]
210    open spec fn is_ne(&self, other: &Rhs) -> bool {
211        !self.eq_spec(other)
212    }
213}
214
215impl<A: PointeeSized + PartialOrd<Rhs>, Rhs: PointeeSized> PartialOrdIs<Rhs> for A {
216    #[verifier::inline]
217    open spec fn is_lt(&self, other: &Rhs) -> bool {
218        self.partial_cmp_spec(other) == Some(Ordering::Less)
219    }
220
221    #[verifier::inline]
222    open spec fn is_le(&self, other: &Rhs) -> bool {
223        matches!(self.partial_cmp_spec(other), Some(Ordering::Less | Ordering::Equal))
224    }
225
226    #[verifier::inline]
227    open spec fn is_gt(&self, other: &Rhs) -> bool {
228        self.partial_cmp_spec(other) == Some(Ordering::Greater)
229    }
230
231    #[verifier::inline]
232    open spec fn is_ge(&self, other: &Rhs) -> bool {
233        matches!(self.partial_cmp_spec(other), Some(Ordering::Greater | Ordering::Equal))
234    }
235}
236
237/* bool */
238
239impl PartialEqSpecImpl for bool {
240    open spec fn obeys_eq_spec() -> bool {
241        true
242    }
243
244    open spec fn eq_spec(&self, other: &bool) -> bool {
245        *self == *other
246    }
247}
248
249pub assume_specification[ <bool as PartialEq<bool>>::eq ](x: &bool, y: &bool) -> bool;
250
251pub assume_specification[ <bool as PartialEq<bool>>::ne ](x: &bool, y: &bool) -> bool;
252
253/* floating point */
254
255/*
256// Note: we do not assume that floating point types have obeys_*_spec() == true
257// because Rust floating point operations are not guaranteed to be deterministic.
258// (See https://github.com/rust-lang/rfcs/blob/master/text/3514-float-semantics.md )
259// Instead, we ensure an uninterpreted function about the result,
260// which can be used to trigger user-supplied axioms.
261*/
262
263pub uninterp spec fn eq_ensures<A>(x: A, y: A, o: bool) -> bool;
264
265pub uninterp spec fn ne_ensures<A>(x: A, y: A, o: bool) -> bool;
266
267pub uninterp spec fn partial_cmp_ensures<A>(x: A, y: A, o: Option<Ordering>) -> bool;
268
269pub uninterp spec fn lt_ensures<A>(x: A, y: A, o: bool) -> bool;
270
271pub uninterp spec fn le_ensures<A>(x: A, y: A, o: bool) -> bool;
272
273pub uninterp spec fn gt_ensures<A>(x: A, y: A, o: bool) -> bool;
274
275pub uninterp spec fn ge_ensures<A>(x: A, y: A, o: bool) -> bool;
276
277// Warning: floating-point eq is not the same as spec ==
278pub assume_specification[ <f32 as PartialEq<f32>>::eq ](x: &f32, y: &f32) -> (o: bool)
279    ensures
280        eq_ensures::<f32>(*x, *y, o),
281;
282
283// Warning: floating-point ne is not the same as spec !=
284pub assume_specification[ <f32 as PartialEq<f32>>::ne ](x: &f32, y: &f32) -> (o: bool)
285    ensures
286        ne_ensures::<f32>(*x, *y, o),
287;
288
289pub assume_specification[ <f32 as PartialOrd<f32>>::partial_cmp ](x: &f32, y: &f32) -> (o: Option<Ordering>)
290    ensures
291        partial_cmp_ensures::<f32>(*x, *y, o),
292;
293
294pub assume_specification[ <f32 as PartialOrd<f32>>::lt ](x: &f32, y: &f32) -> (o: bool)
295    ensures
296        lt_ensures::<f32>(*x, *y, o),
297;
298
299pub assume_specification[ <f32 as PartialOrd<f32>>::le ](x: &f32, y: &f32) -> (o: bool)
300    ensures
301        le_ensures::<f32>(*x, *y, o),
302;
303
304pub assume_specification[ <f32 as PartialOrd<f32>>::gt ](x: &f32, y: &f32) -> (o: bool)
305    ensures
306        gt_ensures::<f32>(*x, *y, o),
307;
308
309pub assume_specification[ <f32 as PartialOrd<f32>>::ge ](x: &f32, y: &f32) -> (o: bool)
310    ensures
311        ge_ensures::<f32>(*x, *y, o),
312;
313
314// Warning: floating-point eq is not the same as spec ==
315pub assume_specification[ <f64 as PartialEq<f64>>::eq ](x: &f64, y: &f64) -> (o: bool)
316    ensures
317        eq_ensures::<f64>(*x, *y, o),
318;
319
320// Warning: floating-point ne is not the same as spec !=
321pub assume_specification[ <f64 as PartialEq<f64>>::ne ](x: &f64, y: &f64) -> (o: bool)
322    ensures
323        ne_ensures::<f64>(*x, *y, o),
324;
325
326pub assume_specification[ <f64 as PartialOrd<f64>>::partial_cmp ](x: &f64, y: &f64) -> (o: Option<Ordering>)
327    ensures
328        partial_cmp_ensures::<f64>(*x, *y, o),
329;
330
331pub assume_specification[ <f64 as PartialOrd<f64>>::lt ](x: &f64, y: &f64) -> (o: bool)
332    ensures
333        lt_ensures::<f64>(*x, *y, o),
334;
335
336pub assume_specification[ <f64 as PartialOrd<f64>>::le ](x: &f64, y: &f64) -> (o: bool)
337    ensures
338        le_ensures::<f64>(*x, *y, o),
339;
340
341pub assume_specification[ <f64 as PartialOrd<f64>>::gt ](x: &f64, y: &f64) -> (o: bool)
342    ensures
343        gt_ensures::<f64>(*x, *y, o),
344;
345
346pub assume_specification[ <f64 as PartialOrd<f64>>::ge ](x: &f64, y: &f64) -> (o: bool)
347    ensures
348        ge_ensures::<f64>(*x, *y, o),
349;
350
351/* reference types & */
352
353impl<A: PointeeSized, B: PointeeSized> PartialEqSpecImpl<&B> for &A
354where
355    A: PartialEq<B>,
356{
357    open spec fn obeys_eq_spec() -> bool {
358        <A as PartialEqSpec<B>>::obeys_eq_spec()
359    }
360
361    open spec fn eq_spec(&self, other: &&B) -> bool {
362        <A as PartialEqSpec<B>>::eq_spec(*self, *other)
363    }
364}
365
366pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialEq<&B>>::eq ](
367    a: &&'a A,
368    b: &&B,
369) -> bool
370where
371    A: PartialEq<B>,
372;
373
374pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialEq<&B>>::ne ](
375    a: &&'a A,
376    b: &&B,
377) -> bool
378where
379    A: PartialEq<B>,
380;
381
382impl<A: PointeeSized, B: PointeeSized> PartialOrdSpecImpl<&B> for &A
383where
384    A: PartialOrd<B>,
385{
386    open spec fn obeys_partial_cmp_spec() -> bool {
387        <A as PartialOrdSpec<B>>::obeys_partial_cmp_spec()
388    }
389
390    open spec fn partial_cmp_spec(&self, other: &&B) -> Option<core::cmp::Ordering> {
391        <A as PartialOrdSpec<B>>::partial_cmp_spec(*self, *other)
392    }
393}
394
395pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialOrd<&B>>::partial_cmp ](
396    a: &&'a A,
397    b: &&B,
398) -> Option<core::cmp::Ordering>
399where
400    A: PartialOrd<B>,
401;
402
403pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialOrd<&B>>::lt ](
404    a: &&'a A,
405    b: &&B,
406) -> bool
407where
408    A: PartialOrd<B>,
409;
410
411pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialOrd<&B>>::le ](
412    a: &&'a A,
413    b: &&B,
414) -> bool
415where
416    A: PartialOrd<B>,
417;
418
419pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialOrd<&B>>::gt ](
420    a: &&'a A,
421    b: &&B,
422) -> bool
423where
424    A: PartialOrd<B>,
425;
426
427pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialOrd<&B>>::ge ](
428    a: &&'a A,
429    b: &&B,
430) -> bool
431where
432    A: PartialOrd<B>,
433;
434
435impl<A: PointeeSized + Ord> OrdSpecImpl for &A {
436    open spec fn obeys_cmp_spec() -> bool {
437        A::obeys_cmp_spec()
438    }
439
440    open spec fn cmp_spec(&self, other: &Self) -> core::cmp::Ordering {
441        A::cmp_spec(*self, *other)
442    }
443}
444
445pub assume_specification<'a, A: PointeeSized + Ord>[ <&'a A as Ord>::cmp ](
446    a: &&'a A,
447    b: &&'a A,
448) -> core::cmp::Ordering
449;
450
451} // verus!
452
453macro_rules! tuple_cmp_impl {
454    ($($idx:tt $T:ident, )+) => {
455        verus! {
456        impl<$($T: PartialEq + PartialEqSpec),+> PartialEqSpecImpl for ($($T,)+)
457        {
458            open spec fn obeys_eq_spec() -> bool {
459                $(&&& $T::obeys_eq_spec())+
460            }
461
462            open spec fn eq_spec(&self, other: &($($T,)+)) -> bool {
463                $(&&& $T::eq_spec(&self.$idx, &other.$idx ))+
464            }
465        }
466
467        impl<$($T: PartialOrd + PartialOrdSpec),+> PartialOrdSpecImpl for ($($T,)+)
468        {
469            open spec fn obeys_partial_cmp_spec() -> bool {
470                $(&&& $T::obeys_partial_cmp_spec())+
471            }
472
473            open spec fn partial_cmp_spec(&self, other: &($($T,)+)) -> Option<core::cmp::Ordering> {
474                lexical_partial_cmp_spec!($( self.$idx, other.$idx ),+)
475            }
476        }
477
478        impl<$($T: Ord + OrdSpec),+> OrdSpecImpl for ($($T,)+)
479        {
480            open spec fn obeys_cmp_spec() -> bool {
481                $(&&& $T::obeys_cmp_spec())+
482            }
483
484            open spec fn cmp_spec(&self, other: &($($T,)+)) -> core::cmp::Ordering {
485                lexical_cmp_spec!($( self.$idx, other.$idx ),+)
486            }
487        }
488
489        }
490    };
491}
492
493#[allow(unused)]
494macro_rules! lexical_partial_cmp_spec {
495    ($a:expr, $b:expr, $($rest_a:expr, $rest_b:expr),+) => {
496        match ($a).partial_cmp_spec(&$b) {
497            Some(core::cmp::Ordering::Equal) => lexical_partial_cmp_spec!($($rest_a, $rest_b),+),
498            ordering => ordering
499        }
500    };
501    ($a:expr, $b:expr) => { ($a).partial_cmp_spec(&$b) };
502}
503
504#[allow(unused)]
505macro_rules! lexical_cmp_spec {
506    ($a:expr, $b:expr, $($rest_a:expr, $rest_b:expr),+) => {
507        match ($a).cmp_spec(&$b) {
508            core::cmp::Ordering::Equal => lexical_cmp_spec!($($rest_a, $rest_b),+),
509            ordering => ordering
510        }
511    };
512    ($a:expr, $b:expr) => { ($a).cmp_spec(&$b) };
513}
514
515tuple_cmp_impl!(0 T, );
516tuple_cmp_impl!(0 U, 1 T, );
517tuple_cmp_impl!(0 V, 1 U, 2 T, );
518tuple_cmp_impl!(0 W, 1 V, 2 U, 3 T, );
519tuple_cmp_impl!(0 X, 1 W, 2 V, 3 U, 4 T, );
520tuple_cmp_impl!(0 Y, 1 X, 2 W, 3 V, 4 U, 5 T, );
521tuple_cmp_impl!(0 Z, 1 Y, 2 X, 3 W, 4 V, 5 U, 6 T, );
522tuple_cmp_impl!(0 A, 1 Z, 2 Y, 3 X, 4 W, 5 V, 6 U, 7 T, );
523tuple_cmp_impl!(0 B, 1 A, 2 Z, 3 Y, 4 X, 5 W, 6 V, 7 U, 8 T, );
524tuple_cmp_impl!(0 C, 1 B, 2 A, 3 Z, 4 Y, 5 X, 6 W, 7 V, 8 U, 9 T, );
525tuple_cmp_impl!(0 D, 1 C, 2 B, 3 A, 4 Z, 5 Y, 6 X, 7 W, 8 V, 9 U, 10 T, );
526tuple_cmp_impl!(0 E, 1 D, 2 C, 3 B, 4 A, 5 Z, 6 Y, 7 X, 8 W, 9 V, 10 U, 11 T, );
vstd/std_specs/cmp.rs

vstd/std_specs/
cmp.rs
