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
238impl PartialEqSpecImpl for bool {
239    open spec fn obeys_eq_spec() -> bool {
240        true
241    }
242
243    open spec fn eq_spec(&self, other: &bool) -> bool {
244        *self == *other
245    }
246}
247
248pub assume_specification[ <bool as PartialEq<bool>>::eq ](x: &bool, y: &bool) -> bool;
249
250pub assume_specification[ <bool as PartialEq<bool>>::ne ](x: &bool, y: &bool) -> bool;
251
252// Note: we do not assume that floating point types have obeys_*_spec() == true
253// because Rust floating point operations are not guaranteed to be deterministic.
254// (See https://github.com/rust-lang/rfcs/blob/master/text/3514-float-semantics.md )
255// Instead, we ensure an uninterpreted function about the result,
256// which can be used to trigger user-supplied axioms.
257
258pub uninterp spec fn eq_ensures<A>(x: A, y: A, o: bool) -> bool;
259
260pub uninterp spec fn ne_ensures<A>(x: A, y: A, o: bool) -> bool;
261
262pub uninterp spec fn partial_cmp_ensures<A>(x: A, y: A, o: Option<Ordering>) -> bool;
263
264pub uninterp spec fn lt_ensures<A>(x: A, y: A, o: bool) -> bool;
265
266pub uninterp spec fn le_ensures<A>(x: A, y: A, o: bool) -> bool;
267
268pub uninterp spec fn gt_ensures<A>(x: A, y: A, o: bool) -> bool;
269
270pub uninterp spec fn ge_ensures<A>(x: A, y: A, o: bool) -> bool;
271
272// Warning: floating-point eq is not the same as spec ==
273pub assume_specification[ <f32 as PartialEq<f32>>::eq ](x: &f32, y: &f32) -> (o: bool)
274    ensures
275        eq_ensures::<f32>(*x, *y, o),
276;
277
278// Warning: floating-point ne is not the same as spec !=
279pub assume_specification[ <f32 as PartialEq<f32>>::ne ](x: &f32, y: &f32) -> (o: bool)
280    ensures
281        ne_ensures::<f32>(*x, *y, o),
282;
283
284pub assume_specification[ <f32 as PartialOrd<f32>>::partial_cmp ](x: &f32, y: &f32) -> (o: Option<Ordering>)
285    ensures
286        partial_cmp_ensures::<f32>(*x, *y, o),
287;
288
289pub assume_specification[ <f32 as PartialOrd<f32>>::lt ](x: &f32, y: &f32) -> (o: bool)
290    ensures
291        lt_ensures::<f32>(*x, *y, o),
292;
293
294pub assume_specification[ <f32 as PartialOrd<f32>>::le ](x: &f32, y: &f32) -> (o: bool)
295    ensures
296        le_ensures::<f32>(*x, *y, o),
297;
298
299pub assume_specification[ <f32 as PartialOrd<f32>>::gt ](x: &f32, y: &f32) -> (o: bool)
300    ensures
301        gt_ensures::<f32>(*x, *y, o),
302;
303
304pub assume_specification[ <f32 as PartialOrd<f32>>::ge ](x: &f32, y: &f32) -> (o: bool)
305    ensures
306        ge_ensures::<f32>(*x, *y, o),
307;
308
309// Warning: floating-point eq is not the same as spec ==
310pub assume_specification[ <f64 as PartialEq<f64>>::eq ](x: &f64, y: &f64) -> (o: bool)
311    ensures
312        eq_ensures::<f64>(*x, *y, o),
313;
314
315// Warning: floating-point ne is not the same as spec !=
316pub assume_specification[ <f64 as PartialEq<f64>>::ne ](x: &f64, y: &f64) -> (o: bool)
317    ensures
318        ne_ensures::<f64>(*x, *y, o),
319;
320
321pub assume_specification[ <f64 as PartialOrd<f64>>::partial_cmp ](x: &f64, y: &f64) -> (o: Option<Ordering>)
322    ensures
323        partial_cmp_ensures::<f64>(*x, *y, o),
324;
325
326pub assume_specification[ <f64 as PartialOrd<f64>>::lt ](x: &f64, y: &f64) -> (o: bool)
327    ensures
328        lt_ensures::<f64>(*x, *y, o),
329;
330
331pub assume_specification[ <f64 as PartialOrd<f64>>::le ](x: &f64, y: &f64) -> (o: bool)
332    ensures
333        le_ensures::<f64>(*x, *y, o),
334;
335
336pub assume_specification[ <f64 as PartialOrd<f64>>::gt ](x: &f64, y: &f64) -> (o: bool)
337    ensures
338        gt_ensures::<f64>(*x, *y, o),
339;
340
341pub assume_specification[ <f64 as PartialOrd<f64>>::ge ](x: &f64, y: &f64) -> (o: bool)
342    ensures
343        ge_ensures::<f64>(*x, *y, o),
344;
345
346} // verus!
vstd/std_specs/cmp.rs

vstd/std_specs/
cmp.rs
