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 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
246pub 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
266pub assume_specification[ <f32 as PartialEq<f32>>::eq ](x: &f32, y: &f32) -> (o: bool)
268 ensures
269 eq_ensures::<f32>(*x, *y, o),
270;
271
272pub 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
303pub assume_specification[ <f64 as PartialEq<f64>>::eq ](x: &f64, y: &f64) -> (o: bool)
305 ensures
306 eq_ensures::<f64>(*x, *y, o),
307;
308
309pub 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}