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            ({
129                &&& Self::obeys_cmp_spec()
130                &&& Self::obeys_partial_cmp_spec()
131                &&& other.partial_cmp_spec(&self) == Some(other.cmp_spec(&self))
132            }) ==> match other.cmp_spec(&self) {
133                Ordering::Less => r == self,
134                Ordering::Equal => r == other,
135                Ordering::Greater => r == other,
136            }
137        default_ensures
138            exists|b: bool|
139                {
140                    &&& #[trigger] call_ensures(Self::lt, (&other, &self), b)
141                    &&& b ==> r == self
142                    &&& !b ==> r == other
143                }
144    ;
145
146    fn min(self, other: Self) -> (r: Self)
147        ensures
148            ({
149                &&& Self::obeys_cmp_spec()
150                &&& Self::obeys_partial_cmp_spec()
151                &&& other.partial_cmp_spec(&self) == Some(other.cmp_spec(&self))
152            }) ==> match other.cmp_spec(&self) {
153                Ordering::Less => r == other,
154                Ordering::Equal => r == self,
155                Ordering::Greater => r == self,
156            }
157        default_ensures
158            exists|b: bool|
159                {
160                    &&& #[trigger] call_ensures(Self::lt, (&other, &self), b)
161                    &&& b ==> r == other
162                    &&& !b ==> r == self
163                }
164    ;
165
166    fn clamp(self, min: Self, max: Self) -> (r: Self)
167        requires
168            // There's an "assert!(min <= max)" in the provided clamp that must succeed, so:
169            Self::obeys_partial_cmp_spec(),
170            min.partial_cmp_spec(&max) matches Some(
171                Ordering::Less
172                | Ordering::Equal,
173            ),
174        ensures
175            ({
176                &&& Self::obeys_cmp_spec()
177                &&& Self::obeys_partial_cmp_spec()
178                &&& self.partial_cmp_spec(&min) == Some(self.cmp_spec(&min))
179                &&& self.partial_cmp_spec(&max) == Some(self.cmp_spec(&max))
180            }) ==> match (self.cmp_spec(&min), self.cmp_spec(&max)) {
181                (Ordering::Less, _) => r == min,
182                (_, Ordering::Greater) => r == max,
183                _ => r == self,
184            }
185        default_ensures
186            exists|b1: bool|
187                {
188                    &&& #[trigger] call_ensures(Self::lt, (&self, &min), b1)
189                    &&& b1 ==> r == min
190                    &&& !b1 ==> exists|b2: bool|
191                        {
192                            &&& #[trigger] call_ensures(Self::gt, (&self, &max), b2)
193                            &&& b2 ==> r == max
194                            &&& !b2 ==> r == self
195                        }
196                }
197    ;
198}
199
200pub trait PartialEqIs<Rhs: PointeeSized = Self>: PartialEq<Rhs> + PointeeSized {
201    spec fn is_eq(&self, other: &Rhs) -> bool;
202
203    spec fn is_ne(&self, other: &Rhs) -> bool;
204}
205
206pub trait PartialOrdIs<Rhs: PointeeSized = Self>: PartialOrd<Rhs> + PointeeSized {
207    spec fn is_lt(&self, other: &Rhs) -> bool;
208
209    spec fn is_le(&self, other: &Rhs) -> bool;
210
211    spec fn is_gt(&self, other: &Rhs) -> bool;
212
213    spec fn is_ge(&self, other: &Rhs) -> bool;
214}
215
216impl<A: PointeeSized + PartialEq<Rhs>, Rhs: PointeeSized> PartialEqIs<Rhs> for A {
217    #[verifier::inline]
218    open spec fn is_eq(&self, other: &Rhs) -> bool {
219        self.eq_spec(other)
220    }
221
222    #[verifier::inline]
223    open spec fn is_ne(&self, other: &Rhs) -> bool {
224        !self.eq_spec(other)
225    }
226}
227
228impl<A: PointeeSized + PartialOrd<Rhs>, Rhs: PointeeSized> PartialOrdIs<Rhs> for A {
229    #[verifier::inline]
230    open spec fn is_lt(&self, other: &Rhs) -> bool {
231        self.partial_cmp_spec(other) == Some(Ordering::Less)
232    }
233
234    #[verifier::inline]
235    open spec fn is_le(&self, other: &Rhs) -> bool {
236        matches!(self.partial_cmp_spec(other), Some(Ordering::Less | Ordering::Equal))
237    }
238
239    #[verifier::inline]
240    open spec fn is_gt(&self, other: &Rhs) -> bool {
241        self.partial_cmp_spec(other) == Some(Ordering::Greater)
242    }
243
244    #[verifier::inline]
245    open spec fn is_ge(&self, other: &Rhs) -> bool {
246        matches!(self.partial_cmp_spec(other), Some(Ordering::Greater | Ordering::Equal))
247    }
248}
249
250/* bool */
251
252impl PartialEqSpecImpl for bool {
253    open spec fn obeys_eq_spec() -> bool {
254        true
255    }
256
257    open spec fn eq_spec(&self, other: &bool) -> bool {
258        *self == *other
259    }
260}
261
262pub assume_specification[ <bool as PartialEq<bool>>::eq ](x: &bool, y: &bool) -> bool;
263
264pub assume_specification[ <bool as PartialEq<bool>>::ne ](x: &bool, y: &bool) -> bool;
265
266/* floating point */
267
268/*
269// Note: we do not assume that floating point types have obeys_*_spec() == true
270// because Rust floating point operations are not guaranteed to be deterministic.
271// (See https://github.com/rust-lang/rfcs/blob/master/text/3514-float-semantics.md )
272// Instead, we ensure an uninterpreted function about the result,
273// which can be used to trigger user-supplied axioms.
274*/
275
276pub uninterp spec fn eq_ensures<A>(x: A, y: A, o: bool) -> bool;
277
278pub uninterp spec fn ne_ensures<A>(x: A, y: A, o: bool) -> bool;
279
280pub uninterp spec fn partial_cmp_ensures<A>(x: A, y: A, o: Option<Ordering>) -> bool;
281
282pub uninterp spec fn lt_ensures<A>(x: A, y: A, o: bool) -> bool;
283
284pub uninterp spec fn le_ensures<A>(x: A, y: A, o: bool) -> bool;
285
286pub uninterp spec fn gt_ensures<A>(x: A, y: A, o: bool) -> bool;
287
288pub uninterp spec fn ge_ensures<A>(x: A, y: A, o: bool) -> bool;
289
290// Warning: floating-point eq is not the same as spec ==
291pub assume_specification[ <f32 as PartialEq<f32>>::eq ](x: &f32, y: &f32) -> (o: bool)
292    ensures
293        eq_ensures::<f32>(*x, *y, o),
294;
295
296// Warning: floating-point ne is not the same as spec !=
297pub assume_specification[ <f32 as PartialEq<f32>>::ne ](x: &f32, y: &f32) -> (o: bool)
298    ensures
299        ne_ensures::<f32>(*x, *y, o),
300;
301
302pub assume_specification[ <f32 as PartialOrd<f32>>::partial_cmp ](x: &f32, y: &f32) -> (o: Option<Ordering>)
303    ensures
304        partial_cmp_ensures::<f32>(*x, *y, o),
305;
306
307pub assume_specification[ <f32 as PartialOrd<f32>>::lt ](x: &f32, y: &f32) -> (o: bool)
308    ensures
309        lt_ensures::<f32>(*x, *y, o),
310;
311
312pub assume_specification[ <f32 as PartialOrd<f32>>::le ](x: &f32, y: &f32) -> (o: bool)
313    ensures
314        le_ensures::<f32>(*x, *y, o),
315;
316
317pub assume_specification[ <f32 as PartialOrd<f32>>::gt ](x: &f32, y: &f32) -> (o: bool)
318    ensures
319        gt_ensures::<f32>(*x, *y, o),
320;
321
322pub assume_specification[ <f32 as PartialOrd<f32>>::ge ](x: &f32, y: &f32) -> (o: bool)
323    ensures
324        ge_ensures::<f32>(*x, *y, o),
325;
326
327// Warning: floating-point eq is not the same as spec ==
328pub assume_specification[ <f64 as PartialEq<f64>>::eq ](x: &f64, y: &f64) -> (o: bool)
329    ensures
330        eq_ensures::<f64>(*x, *y, o),
331;
332
333// Warning: floating-point ne is not the same as spec !=
334pub assume_specification[ <f64 as PartialEq<f64>>::ne ](x: &f64, y: &f64) -> (o: bool)
335    ensures
336        ne_ensures::<f64>(*x, *y, o),
337;
338
339pub assume_specification[ <f64 as PartialOrd<f64>>::partial_cmp ](x: &f64, y: &f64) -> (o: Option<Ordering>)
340    ensures
341        partial_cmp_ensures::<f64>(*x, *y, o),
342;
343
344pub assume_specification[ <f64 as PartialOrd<f64>>::lt ](x: &f64, y: &f64) -> (o: bool)
345    ensures
346        lt_ensures::<f64>(*x, *y, o),
347;
348
349pub assume_specification[ <f64 as PartialOrd<f64>>::le ](x: &f64, y: &f64) -> (o: bool)
350    ensures
351        le_ensures::<f64>(*x, *y, o),
352;
353
354pub assume_specification[ <f64 as PartialOrd<f64>>::gt ](x: &f64, y: &f64) -> (o: bool)
355    ensures
356        gt_ensures::<f64>(*x, *y, o),
357;
358
359pub assume_specification[ <f64 as PartialOrd<f64>>::ge ](x: &f64, y: &f64) -> (o: bool)
360    ensures
361        ge_ensures::<f64>(*x, *y, o),
362;
363
364/* reference types & */
365
366impl<A: PointeeSized, B: PointeeSized> PartialEqSpecImpl<&B> for &A
367where
368    A: PartialEq<B>,
369{
370    open spec fn obeys_eq_spec() -> bool {
371        <A as PartialEqSpec<B>>::obeys_eq_spec()
372    }
373
374    open spec fn eq_spec(&self, other: &&B) -> bool {
375        <A as PartialEqSpec<B>>::eq_spec(*self, *other)
376    }
377}
378
379pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialEq<&B>>::eq ](
380    a: &&'a A,
381    b: &&B,
382) -> bool
383where
384    A: PartialEq<B>,
385;
386
387pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialEq<&B>>::ne ](
388    a: &&'a A,
389    b: &&B,
390) -> bool
391where
392    A: PartialEq<B>,
393;
394
395impl<A: PointeeSized, B: PointeeSized> PartialOrdSpecImpl<&B> for &A
396where
397    A: PartialOrd<B>,
398{
399    open spec fn obeys_partial_cmp_spec() -> bool {
400        <A as PartialOrdSpec<B>>::obeys_partial_cmp_spec()
401    }
402
403    open spec fn partial_cmp_spec(&self, other: &&B) -> Option<core::cmp::Ordering> {
404        <A as PartialOrdSpec<B>>::partial_cmp_spec(*self, *other)
405    }
406}
407
408pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialOrd<&B>>::partial_cmp ](
409    a: &&'a A,
410    b: &&B,
411) -> Option<core::cmp::Ordering>
412where
413    A: PartialOrd<B>,
414;
415
416pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialOrd<&B>>::lt ](
417    a: &&'a A,
418    b: &&B,
419) -> bool
420where
421    A: PartialOrd<B>,
422;
423
424pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialOrd<&B>>::le ](
425    a: &&'a A,
426    b: &&B,
427) -> bool
428where
429    A: PartialOrd<B>,
430;
431
432pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialOrd<&B>>::gt ](
433    a: &&'a A,
434    b: &&B,
435) -> bool
436where
437    A: PartialOrd<B>,
438;
439
440pub assume_specification<'_0, 'a, A: PointeeSized, B: PointeeSized>[ <&'a A as PartialOrd<&B>>::ge ](
441    a: &&'a A,
442    b: &&B,
443) -> bool
444where
445    A: PartialOrd<B>,
446;
447
448impl<A: PointeeSized + Ord> OrdSpecImpl for &A {
449    open spec fn obeys_cmp_spec() -> bool {
450        A::obeys_cmp_spec()
451    }
452
453    open spec fn cmp_spec(&self, other: &Self) -> core::cmp::Ordering {
454        A::cmp_spec(*self, *other)
455    }
456}
457
458pub assume_specification<'a, A: PointeeSized + Ord>[ <&'a A as Ord>::cmp ](
459    a: &&'a A,
460    b: &&'a A,
461) -> core::cmp::Ordering
462;
463
464} // verus!
465
466macro_rules! tuple_cmp_impl {
467    ($($idx:tt $T:ident, )+) => {
468        verus! {
469        impl<$($T: PartialEq + PartialEqSpec),+> PartialEqSpecImpl for ($($T,)+)
470        {
471            open spec fn obeys_eq_spec() -> bool {
472                $(&&& $T::obeys_eq_spec())+
473            }
474
475            open spec fn eq_spec(&self, other: &($($T,)+)) -> bool {
476                $(&&& $T::eq_spec(&self.$idx, &other.$idx ))+
477            }
478        }
479
480        impl<$($T: PartialOrd + PartialOrdSpec),+> PartialOrdSpecImpl for ($($T,)+)
481        {
482            open spec fn obeys_partial_cmp_spec() -> bool {
483                $(&&& $T::obeys_partial_cmp_spec())+
484            }
485
486            open spec fn partial_cmp_spec(&self, other: &($($T,)+)) -> Option<core::cmp::Ordering> {
487                lexical_partial_cmp_spec!($( self.$idx, other.$idx ),+)
488            }
489        }
490
491        impl<$($T: Ord + OrdSpec),+> OrdSpecImpl for ($($T,)+)
492        {
493            open spec fn obeys_cmp_spec() -> bool {
494                $(&&& $T::obeys_cmp_spec())+
495            }
496
497            open spec fn cmp_spec(&self, other: &($($T,)+)) -> core::cmp::Ordering {
498                lexical_cmp_spec!($( self.$idx, other.$idx ),+)
499            }
500        }
501
502        }
503    };
504}
505
506#[allow(unused)]
507macro_rules! lexical_partial_cmp_spec {
508    ($a:expr, $b:expr, $($rest_a:expr, $rest_b:expr),+) => {
509        match ($a).partial_cmp_spec(&$b) {
510            Some(core::cmp::Ordering::Equal) => lexical_partial_cmp_spec!($($rest_a, $rest_b),+),
511            ordering => ordering
512        }
513    };
514    ($a:expr, $b:expr) => { ($a).partial_cmp_spec(&$b) };
515}
516
517#[allow(unused)]
518macro_rules! lexical_cmp_spec {
519    ($a:expr, $b:expr, $($rest_a:expr, $rest_b:expr),+) => {
520        match ($a).cmp_spec(&$b) {
521            core::cmp::Ordering::Equal => lexical_cmp_spec!($($rest_a, $rest_b),+),
522            ordering => ordering
523        }
524    };
525    ($a:expr, $b:expr) => { ($a).cmp_spec(&$b) };
526}
527
528tuple_cmp_impl!(0 T, );
529tuple_cmp_impl!(0 U, 1 T, );
530tuple_cmp_impl!(0 V, 1 U, 2 T, );
531tuple_cmp_impl!(0 W, 1 V, 2 U, 3 T, );
532tuple_cmp_impl!(0 X, 1 W, 2 V, 3 U, 4 T, );
533tuple_cmp_impl!(0 Y, 1 X, 2 W, 3 V, 4 U, 5 T, );
534tuple_cmp_impl!(0 Z, 1 Y, 2 X, 3 W, 4 V, 5 U, 6 T, );
535tuple_cmp_impl!(0 A, 1 Z, 2 Y, 3 X, 4 W, 5 V, 6 U, 7 T, );
536tuple_cmp_impl!(0 B, 1 A, 2 Z, 3 Y, 4 X, 5 W, 6 V, 7 U, 8 T, );
537tuple_cmp_impl!(0 C, 1 B, 2 A, 3 Z, 4 Y, 5 X, 6 W, 7 V, 8 U, 9 T, );
538tuple_cmp_impl!(0 D, 1 C, 2 B, 3 A, 4 Z, 5 Y, 6 X, 7 W, 8 V, 9 U, 10 T, );
539tuple_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
