vstd/std_specs/
cmp.rs

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

vstd/std_specs/
cmp.rs
