vstd/std_specs/
cmp.rs

1use super::super::prelude::*;
2
3use verus as verus_;
4
5use core::cmp::{Eq, Ord, Ordering, PartialEq, PartialOrd};
6
7verus_! {
8
9#[verifier::external_trait_specification]
10#[verifier::external_trait_extension(PartialEqSpec via PartialEqSpecImpl)]
11pub trait ExPartialEq<Rhs: ?Sized = Self> {
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 {
31    type ExternalTraitSpecificationFor: Eq;
32}
33
34#[verifier::external_trait_specification]
35#[verifier::external_trait_extension(PartialOrdSpec via PartialOrdSpecImpl)]
36pub trait ExPartialOrd<Rhs: ?Sized = Self>: PartialEq<Rhs> {
37    type ExternalTraitSpecificationFor: PartialOrd<Rhs>;
38
39    spec fn obeys_partial_cmp_spec() -> bool;
40
41    spec fn partial_cmp_spec(&self, other: &Rhs) -> Option<Ordering>;
42
43    fn partial_cmp(&self, other: &Rhs) -> (r: Option<Ordering>)
44        ensures
45            Self::obeys_partial_cmp_spec() ==> r == self.partial_cmp_spec(other);
46
47    fn lt(&self, other: &Rhs) -> (r: bool)
48        ensures
49            Self::obeys_partial_cmp_spec() ==>
50                (r <==> self.partial_cmp_spec(other) == Some(Ordering::Less)),
51        default_ensures
52            exists|o: Option<Ordering>|
53                {
54                    &&& #[trigger] call_ensures(Self::partial_cmp, (self, other), o)
55                    &&& r <==> o == Some(Ordering::Less)
56                }
57    ;
58
59    fn le(&self, other: &Rhs) -> (r: bool)
60        ensures
61            Self::obeys_partial_cmp_spec() ==>
62                (r <==> self.partial_cmp_spec(other) matches Some(
63                    Ordering::Less
64                    | Ordering::Equal,
65                )),
66        default_ensures
67            exists|o: Option<Ordering>|
68                {
69                    &&& #[trigger] call_ensures(Self::partial_cmp, (self, other), o)
70                    &&& r <==> o matches Some(
71                        Ordering::Less
72                        | Ordering::Equal,
73                    )
74                }
75    ;
76
77    fn gt(&self, other: &Rhs) -> (r: bool)
78        ensures
79            Self::obeys_partial_cmp_spec() ==>
80                (r <==> self.partial_cmp_spec(other) == Some(Ordering::Greater)),
81        default_ensures
82            exists|o: Option<Ordering>|
83                {
84                    &&& #[trigger] call_ensures(Self::partial_cmp, (self, other), o)
85                    &&& r <==> o == Some(Ordering::Greater)
86                }
87    ;
88
89    fn ge(&self, other: &Rhs) -> (r: bool)
90        ensures
91            Self::obeys_partial_cmp_spec() ==>
92                (r <==> self.partial_cmp_spec(other) matches Some(
93                    Ordering::Greater
94                    | Ordering::Equal,
95                )),
96        default_ensures
97            exists|o: Option<Ordering>|
98                {
99                    &&& #[trigger] call_ensures(Self::partial_cmp, (self, other), o)
100                    &&& r <==> o matches Some(
101                        Ordering::Greater
102                        | Ordering::Equal,
103                    )
104                }
105    ;
106}
107
108#[verifier::external_trait_specification]
109#[verifier::external_trait_extension(OrdSpec via OrdSpecImpl)]
110pub trait ExOrd: Eq + PartialOrd {
111    type ExternalTraitSpecificationFor: Ord;
112
113    spec fn obeys_cmp_spec() -> bool;
114
115    spec fn cmp_spec(&self, other: &Self) -> Ordering;
116
117    fn cmp(&self, other: &Self) -> (r: Ordering)
118        ensures
119            Self::obeys_cmp_spec() ==> r == self.cmp_spec(other);
120
121    fn max(self, other: Self) -> (r: Self)
122        ensures
123            Self::obeys_cmp_spec() ==> match other.cmp_spec(&self) {
124                Ordering::Less => r == self,
125                Ordering::Equal => r == other,
126                Ordering::Greater => r == other,
127            }
128        default_ensures
129            exists|b: bool|
130                {
131                    &&& #[trigger] call_ensures(Self::lt, (&other, &self), b)
132                    &&& b ==> r == self
133                    &&& !b ==> r == other
134                }
135    ;
136
137    fn min(self, other: Self) -> (r: Self)
138        ensures
139            Self::obeys_cmp_spec() ==> match other.cmp_spec(&self) {
140                Ordering::Less => r == other,
141                Ordering::Equal => r == self,
142                Ordering::Greater => r == self,
143            }
144        default_ensures
145            exists|b: bool|
146                {
147                    &&& #[trigger] call_ensures(Self::lt, (&other, &self), b)
148                    &&& b ==> r == other
149                    &&& !b ==> r == self
150                }
151    ;
152
153    fn clamp(self, min: Self, max: Self) -> (r: Self)
154        requires
155            // There's an "assert!(min <= max)" in the provided clamp that must succeed, so:
156            Self::obeys_partial_cmp_spec(),
157            min.partial_cmp_spec(&max) matches Some(
158                Ordering::Less
159                | Ordering::Equal,
160            ),
161        ensures
162            Self::obeys_cmp_spec() ==> match (self.cmp_spec(&min), self.cmp_spec(&max)) {
163                (Ordering::Less, _) => r == min,
164                (_, Ordering::Greater) => r == max,
165                _ => r == self,
166            }
167        default_ensures
168            exists|b1: bool|
169                {
170                    &&& #[trigger] call_ensures(Self::lt, (&self, &min), b1)
171                    &&& b1 ==> r == min
172                    &&& !b1 ==> exists|b2: bool|
173                        {
174                            &&& #[trigger] call_ensures(Self::gt, (&self, &max), b2)
175                            &&& b2 ==> r == max
176                            &&& !b2 ==> r == self
177                        }
178                }
179    ;
180}
181
182pub trait PartialEqIs<Rhs: ?Sized = Self>: PartialEq<Rhs> {
183    spec fn is_eq(&self, other: &Rhs) -> bool;
184
185    spec fn is_ne(&self, other: &Rhs) -> bool;
186}
187
188pub trait PartialOrdIs<Rhs: ?Sized = Self>: PartialOrd<Rhs> {
189    spec fn is_lt(&self, other: &Rhs) -> bool;
190
191    spec fn is_le(&self, other: &Rhs) -> bool;
192
193    spec fn is_gt(&self, other: &Rhs) -> bool;
194
195    spec fn is_ge(&self, other: &Rhs) -> bool;
196}
197
198impl<A: ?Sized + PartialEq<Rhs>, Rhs: ?Sized> PartialEqIs<Rhs> for A {
199    #[verifier::inline]
200    open spec fn is_eq(&self, other: &Rhs) -> bool {
201        self.eq_spec(other)
202    }
203
204    #[verifier::inline]
205    open spec fn is_ne(&self, other: &Rhs) -> bool {
206        !self.eq_spec(other)
207    }
208}
209
210impl<A: ?Sized + PartialOrd<Rhs>, Rhs: ?Sized> PartialOrdIs<Rhs> for A {
211    #[verifier::inline]
212    open spec fn is_lt(&self, other: &Rhs) -> bool {
213        self.partial_cmp_spec(other) == Some(Ordering::Less)
214    }
215
216    #[verifier::inline]
217    open spec fn is_le(&self, other: &Rhs) -> bool {
218        matches!(self.partial_cmp_spec(other), Some(Ordering::Less | Ordering::Equal))
219    }
220
221    #[verifier::inline]
222    open spec fn is_gt(&self, other: &Rhs) -> bool {
223        self.partial_cmp_spec(other) == Some(Ordering::Greater)
224    }
225
226    #[verifier::inline]
227    open spec fn is_ge(&self, other: &Rhs) -> bool {
228        matches!(self.partial_cmp_spec(other), Some(Ordering::Greater | Ordering::Equal))
229    }
230}
231
232impl PartialEqSpecImpl for bool {
233    open spec fn obeys_eq_spec() -> bool {
234        true
235    }
236
237    open spec fn eq_spec(&self, other: &bool) -> bool {
238        *self == *other
239    }
240}
241
242pub assume_specification[ <bool as PartialEq<bool>>::eq ](x: &bool, y: &bool) -> bool;
243
244pub assume_specification[ <bool as PartialEq<bool>>::ne ](x: &bool, y: &bool) -> bool;
245
246// Note: we do not assume that floating point types have obeys_*_spec() == true
247// because Rust floating point operations are not guaranteed to be deterministic.
248// (See https://github.com/rust-lang/rfcs/blob/master/text/3514-float-semantics.md )
249// Instead, we ensure an uninterpreted function about the result,
250// which can be used to trigger user-supplied axioms.
251
252pub uninterp spec fn eq_ensures<A>(x: A, y: A, o: bool) -> bool;
253
254pub uninterp spec fn ne_ensures<A>(x: A, y: A, o: bool) -> bool;
255
256pub uninterp spec fn partial_cmp_ensures<A>(x: A, y: A, o: Option<Ordering>) -> bool;
257
258pub uninterp spec fn lt_ensures<A>(x: A, y: A, o: bool) -> bool;
259
260pub uninterp spec fn le_ensures<A>(x: A, y: A, o: bool) -> bool;
261
262pub uninterp spec fn gt_ensures<A>(x: A, y: A, o: bool) -> bool;
263
264pub uninterp spec fn ge_ensures<A>(x: A, y: A, o: bool) -> bool;
265
266// Warning: floating-point eq is not the same as spec ==
267pub assume_specification[ <f32 as PartialEq<f32>>::eq ](x: &f32, y: &f32) -> (o: bool)
268    ensures
269        eq_ensures::<f32>(*x, *y, o),
270;
271
272// Warning: floating-point ne is not the same as spec !=
273pub assume_specification[ <f32 as PartialEq<f32>>::ne ](x: &f32, y: &f32) -> (o: bool)
274    ensures
275        ne_ensures::<f32>(*x, *y, o),
276;
277
278pub assume_specification[ <f32 as PartialOrd<f32>>::partial_cmp ](x: &f32, y: &f32) -> (o: Option<Ordering>)
279    ensures
280        partial_cmp_ensures::<f32>(*x, *y, o),
281;
282
283pub assume_specification[ <f32 as PartialOrd<f32>>::lt ](x: &f32, y: &f32) -> (o: bool)
284    ensures
285        lt_ensures::<f32>(*x, *y, o),
286;
287
288pub assume_specification[ <f32 as PartialOrd<f32>>::le ](x: &f32, y: &f32) -> (o: bool)
289    ensures
290        le_ensures::<f32>(*x, *y, o),
291;
292
293pub assume_specification[ <f32 as PartialOrd<f32>>::gt ](x: &f32, y: &f32) -> (o: bool)
294    ensures
295        gt_ensures::<f32>(*x, *y, o),
296;
297
298pub assume_specification[ <f32 as PartialOrd<f32>>::ge ](x: &f32, y: &f32) -> (o: bool)
299    ensures
300        ge_ensures::<f32>(*x, *y, o),
301;
302
303// Warning: floating-point eq is not the same as spec ==
304pub assume_specification[ <f64 as PartialEq<f64>>::eq ](x: &f64, y: &f64) -> (o: bool)
305    ensures
306        eq_ensures::<f64>(*x, *y, o),
307;
308
309// Warning: floating-point ne is not the same as spec !=
310pub assume_specification[ <f64 as PartialEq<f64>>::ne ](x: &f64, y: &f64) -> (o: bool)
311    ensures
312        ne_ensures::<f64>(*x, *y, o),
313;
314
315pub assume_specification[ <f64 as PartialOrd<f64>>::partial_cmp ](x: &f64, y: &f64) -> (o: Option<Ordering>)
316    ensures
317        partial_cmp_ensures::<f64>(*x, *y, o),
318;
319
320pub assume_specification[ <f64 as PartialOrd<f64>>::lt ](x: &f64, y: &f64) -> (o: bool)
321    ensures
322        lt_ensures::<f64>(*x, *y, o),
323;
324
325pub assume_specification[ <f64 as PartialOrd<f64>>::le ](x: &f64, y: &f64) -> (o: bool)
326    ensures
327        le_ensures::<f64>(*x, *y, o),
328;
329
330pub assume_specification[ <f64 as PartialOrd<f64>>::gt ](x: &f64, y: &f64) -> (o: bool)
331    ensures
332        gt_ensures::<f64>(*x, *y, o),
333;
334
335pub assume_specification[ <f64 as PartialOrd<f64>>::ge ](x: &f64, y: &f64) -> (o: bool)
336    ensures
337        ge_ensures::<f64>(*x, *y, o),
338;
339
340} // verus!
vstd/std_specs/cmp.rs

vstd/std_specs/
cmp.rs
