creusot_contracts/std/
cmp.rs1use crate::{logic::OrdLogic, prelude::*};
2use std::cmp::*;
3
4#[cfg(creusot)]
5pub use creusot_contracts_proc::PartialEq;
6
7#[cfg(not(creusot))]
8pub use std::cmp::PartialEq;
9
10extern_spec! {
11 mod std {
12 mod cmp {
13 trait PartialEq<Rhs> {
14 #[ensures(result == (self.deep_model() == rhs.deep_model()))]
15 fn eq(&self, rhs: &Rhs) -> bool
16 where
17 Self: DeepModel,
18 Rhs: DeepModel<DeepModelTy = Self::DeepModelTy>;
19
20 #[ensures(result == (self.deep_model() != rhs.deep_model()))]
21 fn ne(&self, rhs: &Rhs) -> bool
22 where
23 Self: DeepModel,
24 Rhs: DeepModel<DeepModelTy = Self::DeepModelTy> {
25 !(self == rhs)
26 }
27 }
28
29 trait PartialOrd<Rhs>
31 where Self: DeepModel,
32 Rhs: DeepModel<DeepModelTy = Self::DeepModelTy>,
33 Self::DeepModelTy: OrdLogic
34 {
35 #[ensures(result == Some((*self).deep_model().cmp_log((*rhs).deep_model())))]
36 fn partial_cmp(&self, rhs: &Rhs) -> Option<Ordering>;
37
38 #[ensures(result == (self.deep_model() < other.deep_model()))]
39 fn lt(&self, other: &Rhs) -> bool {
40 match self.partial_cmp(other) {
41 Some(Ordering::Less) => true,
42 _ => false,
43 }
44 }
45
46 #[ensures(result == (self.deep_model() <= other.deep_model()))]
47 fn le(&self, other: &Rhs) -> bool {
48 match self.partial_cmp(other) {
49 Some(Ordering::Less | Ordering::Equal) => true,
50 _ => false,
51 }
52 }
53
54 #[ensures(result == (self.deep_model() > other.deep_model()))]
55 fn gt(&self, other: &Rhs) -> bool {
56 match self.partial_cmp(other) {
57 Some(Ordering::Greater) => true,
58 _ => false,
59 }
60 }
61
62 #[ensures(result == (self.deep_model() >= other.deep_model()))]
63 fn ge(&self, other: &Rhs) -> bool {
64 match self.partial_cmp(other) {
65 Some(Ordering::Greater | Ordering::Equal) => true,
66 _ => false,
67 }
68 }
69 }
70
71 trait Ord
72 where Self: DeepModel,
73 Self::DeepModelTy: OrdLogic
74 {
75 #[ensures(result == (*self).deep_model().cmp_log((*rhs).deep_model()))]
76 fn cmp(&self, rhs: &Self) -> Ordering;
77
78 #[ensures(result.deep_model() >= self.deep_model())]
79 #[ensures(result.deep_model() >= o.deep_model())]
80 #[ensures(result == self || result == o)]
81 #[ensures(self.deep_model() <= o.deep_model() ==> result == o)]
82 #[ensures(o.deep_model() < self.deep_model() ==> result == self)]
83 fn max(self, o: Self) -> Self where Self: Sized {
84 if self <= o { o } else { self }
85 }
86
87 #[ensures(result.deep_model() <= self.deep_model())]
88 #[ensures(result.deep_model() <= o.deep_model())]
89 #[ensures(result == self || result == o)]
90 #[ensures(self.deep_model() < o.deep_model() ==> result == self)]
91 #[ensures(o.deep_model() <= self.deep_model() ==> result == o)]
92 fn min(self, o: Self) -> Self where Self: Sized {
93 if self < o { self } else { o }
94 }
95
96 #[requires(min.deep_model() <= max.deep_model())]
97 #[ensures(result.deep_model() >= min.deep_model())]
98 #[ensures(result.deep_model() <= max.deep_model())]
99 #[ensures(result == self || result == min || result == max)]
100 #[ensures(if self.deep_model() > max.deep_model() {
101 result == max
102 } else if self.deep_model() < min.deep_model() {
103 result == min
104 } else { result == self })]
105 fn clamp(self, min: Self, max: Self) -> Self where Self: Sized {
106 if self > max { max } else if self < min { min } else { self }
107 }
108 }
109
110 #[ensures(result.deep_model() >= v1.deep_model())]
111 #[ensures(result.deep_model() >= v2.deep_model())]
112 #[ensures(result == v1 || result == v2)]
113 #[ensures(v1.deep_model() <= v2.deep_model() ==> result == v2)]
114 #[ensures(v2.deep_model() < v1.deep_model() ==> result == v1)]
115 fn max<T>(v1: T, v2: T) -> T
116 where T: Ord + DeepModel, T::DeepModelTy: OrdLogic
117 {
118 <T as Ord>::max(v1, v2)
119 }
120
121 #[ensures(result.deep_model() <= v1.deep_model())]
122 #[ensures(result.deep_model() <= v2.deep_model())]
123 #[ensures(result == v1 || result == v2)]
124 #[ensures(v1.deep_model() < v2.deep_model() ==> result == v1)]
125 #[ensures(v2.deep_model() <= v1.deep_model() ==> result == v2)]
126 fn min<T>(v1: T, v2: T) -> T
127 where T: Ord + DeepModel, T::DeepModelTy: OrdLogic
128 {
129 <T as Ord>::min(v1, v2)
130 }
131 }
132 }
133}
134
135macro_rules! impl_cmp_int {
137 ($($t:ty)*) => {
138$(
139
140extern_spec! {
141 impl PartialEq<$t> for $t {
142 #[check(ghost)]
143 #[ensures(result == (self.deep_model() == rhs.deep_model()))]
144 fn eq(&self, rhs: &$t) -> bool;
145
146 #[check(ghost)]
147 #[ensures(result == (self.deep_model() != rhs.deep_model()))]
148 fn ne(&self, rhs: &$t) -> bool;
149 }
150
151 impl PartialOrd<$t> for $t
152 {
153 #[check(ghost)]
154 #[ensures(result == Some((*self).deep_model().cmp_log((*rhs).deep_model())))]
155 fn partial_cmp(&self, rhs: &$t) -> Option<Ordering>;
156
157 #[check(ghost)]
158 #[ensures(result == (self.deep_model() < other.deep_model()))]
159 fn lt(&self, other: &$t) -> bool {
160 match self.partial_cmp(other) {
161 Some(Ordering::Less) => true,
162 _ => false,
163 }
164 }
165
166 #[check(ghost)]
167 #[ensures(result == (self.deep_model() <= other.deep_model()))]
168 fn le(&self, other: &$t) -> bool {
169 match self.partial_cmp(other) {
170 Some(Ordering::Less | Ordering::Equal) => true,
171 _ => false,
172 }
173 }
174
175 #[check(ghost)]
176 #[ensures(result == (self.deep_model() > other.deep_model()))]
177 fn gt(&self, other: &$t) -> bool {
178 match self.partial_cmp(other) {
179 Some(Ordering::Greater) => true,
180 _ => false,
181 }
182 }
183
184 #[check(ghost)]
185 #[ensures(result == (self.deep_model() >= other.deep_model()))]
186 fn ge(&self, other: &$t) -> bool {
187 match self.partial_cmp(other) {
188 Some(Ordering::Greater | Ordering::Equal) => true,
189 _ => false,
190 }
191 }
192 }
193
194 impl Ord for $t
195 {
196 #[check(ghost)]
197 #[ensures(result == (*self).deep_model().cmp_log((*rhs).deep_model()))]
198 fn cmp(&self, rhs: &Self) -> Ordering;
199
200 }
233}
234
235)* };
236
237}
238
239impl_cmp_int!(i8 i16 i32 i64 i128 isize u8 u16 u32 u64 u128 usize);
240
241impl<T: DeepModel> DeepModel for Reverse<T> {
242 type DeepModelTy = Reverse<T::DeepModelTy>;
243
244 #[logic(open, inline)]
245 fn deep_model(self) -> Self::DeepModelTy {
246 pearlite! { Reverse(self.0.deep_model()) }
247 }
248}
249
250impl<T: OrdLogic> OrdLogic for Reverse<T> {
251 #[logic(open)]
252 fn cmp_log(self, o: Self) -> Ordering {
253 match self.0.cmp_log(o.0) {
254 Ordering::Equal => Ordering::Equal,
255 Ordering::Less => Ordering::Greater,
256 Ordering::Greater => Ordering::Less,
257 }
258 }
259
260 #[logic(open, law)]
261 #[ensures(x.le_log(y) == (x.cmp_log(y) != Ordering::Greater))]
262 fn cmp_le_log(x: Self, y: Self) {}
263
264 #[logic(open, law)]
265 #[ensures(x.lt_log(y) == (x.cmp_log(y) == Ordering::Less))]
266 fn cmp_lt_log(x: Self, y: Self) {}
267
268 #[logic(open, law)]
269 #[ensures(x.ge_log(y) == (x.cmp_log(y) != Ordering::Less))]
270 fn cmp_ge_log(x: Self, y: Self) {}
271
272 #[logic(open, law)]
273 #[ensures(x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater))]
274 fn cmp_gt_log(x: Self, y: Self) {}
275
276 #[logic(open, law)]
277 #[ensures(x.cmp_log(x) == Ordering::Equal)]
278 fn refl(x: Self) {}
279
280 #[logic(open, law)]
281 #[requires(x.cmp_log(y) == o)]
282 #[requires(y.cmp_log(z) == o)]
283 #[ensures(x.cmp_log(z) == o)]
284 fn trans(x: Self, y: Self, z: Self, o: Ordering) {}
285
286 #[logic(open, law)]
287 #[requires(x.cmp_log(y) == Ordering::Less)]
288 #[ensures(y.cmp_log(x) == Ordering::Greater)]
289 fn antisym1(x: Self, y: Self) {}
290
291 #[logic(open, law)]
292 #[requires(x.cmp_log(y) == Ordering::Greater)]
293 #[ensures(y.cmp_log(x) == Ordering::Less)]
294 fn antisym2(x: Self, y: Self) {}
295
296 #[logic(open, law)]
297 #[ensures((x == y) == (x.cmp_log(y) == Ordering::Equal))]
298 fn eq_cmp(x: Self, y: Self) {}
299}