vstd/std_specs/
num.rs

1#![allow(unused_imports)]
2use super::super::prelude::*;
3
4use core::cmp::Ordering;
5
6macro_rules! num_specs {
7    ($uN: ty, $iN: ty, $modname_u:ident, $modname_i:ident, $range:expr) => {
8        verus! {
9
10        // Unsigned ints (u8, u16, etc.)
11
12        // Put in separate module to avoid name collisions.
13        // Names don't matter - the user uses the stdlib functions.
14        mod $modname_u {
15            use super::*;
16
17            pub assume_specification[<$uN as Clone>::clone](x: &$uN) -> (res: $uN)
18                ensures res == x;
19
20            impl super::super::cmp::PartialEqSpecImpl for $uN {
21                open spec fn obeys_eq_spec() -> bool {
22                    true
23                }
24
25                open spec fn eq_spec(&self, other: &$uN) -> bool {
26                    *self == *other
27                }
28            }
29
30            impl super::super::cmp::PartialOrdSpecImpl for $uN {
31                open spec fn obeys_partial_cmp_spec() -> bool {
32                    true
33                }
34
35                open spec fn partial_cmp_spec(&self, other: &$uN) -> Option<Ordering> {
36                    if *self < *other {
37                        Some(Ordering::Less)
38                    } else if *self > *other {
39                        Some(Ordering::Greater)
40                    } else {
41                        Some(Ordering::Equal)
42                    }
43                }
44            }
45
46            impl super::super::cmp::OrdSpecImpl for $uN {
47                open spec fn obeys_cmp_spec() -> bool {
48                    true
49                }
50
51                open spec fn cmp_spec(&self, other: &$uN) -> Ordering {
52                    if *self < *other {
53                        Ordering::Less
54                    } else if *self > *other {
55                        Ordering::Greater
56                    } else {
57                        Ordering::Equal
58                    }
59                }
60            }
61
62            pub assume_specification[<$uN as PartialEq<$uN>>::eq](x: &$uN, y: &$uN) -> bool;
63
64            pub assume_specification[<$uN as PartialEq<$uN>>::ne](x: &$uN, y: &$uN) -> bool;
65
66            pub assume_specification[<$uN as Ord>::cmp](x: &$uN, y: &$uN) -> Ordering;
67
68            pub assume_specification[<$uN as PartialOrd<$uN>>::partial_cmp](x: &$uN, y: &$uN) -> Option<Ordering>;
69
70            pub assume_specification[<$uN as PartialOrd<$uN>>::lt](x: &$uN, y: &$uN) -> bool;
71
72            pub assume_specification[<$uN as PartialOrd<$uN>>::le](x: &$uN, y: &$uN) -> bool;
73
74            pub assume_specification[<$uN as PartialOrd<$uN>>::gt](x: &$uN, y: &$uN) -> bool;
75
76            pub assume_specification[<$uN as PartialOrd<$uN>>::ge](x: &$uN, y: &$uN) -> bool;
77
78            #[verifier::allow_in_spec]
79            pub assume_specification[<$uN>::wrapping_add](x: $uN, y: $uN) -> $uN
80                returns (
81                    if x + y > <$uN>::MAX {
82                        (x + y - $range) as $uN
83                    } else {
84                        (x + y) as $uN
85                    }
86                );
87
88            #[verifier::allow_in_spec]
89            pub assume_specification[<$uN>::wrapping_add_signed](x: $uN, y: $iN) -> $uN
90                returns (
91                    if x + y > <$uN>::MAX {
92                        (x + y - $range) as $uN
93                    } else if x + y < 0 {
94                        (x + y + $range) as $uN
95                    } else {
96                        (x + y) as $uN
97                    }
98                );
99
100            #[verifier::allow_in_spec]
101            pub assume_specification[<$uN>::wrapping_sub](x: $uN, y: $uN) -> $uN
102                returns (
103                    if x - y < 0 {
104                        (x - y + $range) as $uN
105                    } else {
106                        (x - y) as $uN
107                    }
108                );
109
110            #[verifier::allow_in_spec]
111            pub assume_specification[<$uN>::wrapping_mul](x: $uN, y: $uN) -> $uN
112                returns ((x as nat * y as nat) % $range as nat) as $uN;
113
114            #[verifier::allow_in_spec]
115            pub assume_specification[<$uN>::checked_add](x: $uN, y: $uN) -> Option<$uN>
116                returns (
117                    if x + y > <$uN>::MAX {
118                        None
119                    } else {
120                        Some((x + y) as $uN)
121                    }
122                );
123
124            #[verifier::allow_in_spec]
125            pub assume_specification[<$uN>::checked_add_signed](x: $uN, y: $iN) -> Option<$uN>
126                returns (
127                    if x + y > <$uN>::MAX || x + y < 0 {
128                        None
129                    } else {
130                        Some((x + y) as $uN)
131                    }
132                );
133
134            #[verifier::allow_in_spec]
135            pub assume_specification[<$uN>::checked_sub](x: $uN, y: $uN) -> Option<$uN>
136                returns (
137                    if x - y < 0 {
138                        None
139                    } else {
140                        Some((x - y) as $uN)
141                    }
142                );
143
144            #[verifier::allow_in_spec]
145            pub assume_specification[<$uN>::checked_mul](x: $uN, y: $uN) -> Option<$uN>
146                returns (
147                    if x * y > <$uN>::MAX {
148                        None
149                    } else {
150                        Some((x * y) as $uN)
151                    }
152                );
153
154            pub open spec fn checked_div(x: $uN, y: $uN) -> Option<$uN> {
155                if y == 0 {
156                    None
157                } else {
158                    Some(x / y)
159                }
160            }
161
162            #[verifier::when_used_as_spec(checked_div)]
163            pub assume_specification[<$uN>::checked_div](lhs: $uN, rhs: $uN) -> (result: Option<$uN>)
164                ensures
165                    result == checked_div(lhs, rhs);
166
167            #[verifier::when_used_as_spec(checked_div)]
168            pub assume_specification[<$uN>::checked_div_euclid](lhs: $uN, rhs: $uN) -> (result: Option<$uN>)
169                ensures
170                    // checked_div is the same as checked_div_euclid for unsigned ints
171                    result == checked_div(lhs, rhs);
172
173            #[verifier::allow_in_spec]
174            pub assume_specification[<$uN>::is_multiple_of](x: $uN, y: $uN) -> bool
175                returns (
176                    if y == 0 { x == 0 } else { x % y == 0 }
177                );
178        }
179
180        // Signed ints (i8, i16, etc.)
181
182        mod $modname_i {
183            use super::*;
184
185            pub assume_specification[<$iN as Clone>::clone](x: &$iN) -> (res: $iN)
186                ensures res == x;
187
188            impl super::super::cmp::PartialEqSpecImpl for $iN {
189                open spec fn obeys_eq_spec() -> bool {
190                    true
191                }
192
193                open spec fn eq_spec(&self, other: &$iN) -> bool {
194                    *self == *other
195                }
196            }
197
198            impl super::super::cmp::PartialOrdSpecImpl for $iN {
199                open spec fn obeys_partial_cmp_spec() -> bool {
200                    true
201                }
202
203                open spec fn partial_cmp_spec(&self, other: &$iN) -> Option<Ordering> {
204                    if *self < *other {
205                        Some(Ordering::Less)
206                    } else if *self > *other {
207                        Some(Ordering::Greater)
208                    } else {
209                        Some(Ordering::Equal)
210                    }
211                }
212            }
213
214            impl super::super::cmp::OrdSpecImpl for $iN {
215                open spec fn obeys_cmp_spec() -> bool {
216                    true
217                }
218
219                open spec fn cmp_spec(&self, other: &$iN) -> Ordering {
220                    if *self < *other {
221                        Ordering::Less
222                    } else if *self > *other {
223                        Ordering::Greater
224                    } else {
225                        Ordering::Equal
226                    }
227                }
228            }
229
230            pub assume_specification[<$iN as PartialEq<$iN>>::eq](x: &$iN, y: &$iN) -> bool;
231
232            pub assume_specification[<$iN as PartialEq<$iN>>::ne](x: &$iN, y: &$iN) -> bool;
233
234            pub assume_specification[<$iN as Ord>::cmp](x: &$iN, y: &$iN) -> Ordering;
235
236            pub assume_specification[<$iN as PartialOrd<$iN>>::partial_cmp](x: &$iN, y: &$iN) -> Option<Ordering>;
237
238            pub assume_specification[<$iN as PartialOrd<$iN>>::lt](x: &$iN, y: &$iN) -> bool;
239
240            pub assume_specification[<$iN as PartialOrd<$iN>>::le](x: &$iN, y: &$iN) -> bool;
241
242            pub assume_specification[<$iN as PartialOrd<$iN>>::gt](x: &$iN, y: &$iN) -> bool;
243
244            pub assume_specification[<$iN as PartialOrd<$iN>>::ge](x: &$iN, y: &$iN) -> bool;
245
246            #[verifier::allow_in_spec]
247            pub assume_specification[<$iN>::wrapping_add](x: $iN, y: $iN) -> $iN
248                returns (
249                    if x + y > <$iN>::MAX {
250                        (x + y - $range) as $iN
251                    } else if x + y < <$iN>::MIN {
252                        (x + y + $range) as $iN
253                    } else {
254                        (x + y) as $iN
255                    }
256                );
257
258            #[verifier::allow_in_spec]
259            pub assume_specification[<$iN>::wrapping_add_unsigned](x: $iN, y: $uN) -> $iN
260                returns (
261                    if x + y > <$iN>::MAX {
262                        (x + y - $range) as $iN
263                    } else {
264                        (x + y) as $iN
265                    }
266                );
267
268            #[verifier::allow_in_spec]
269            pub assume_specification[<$iN>::wrapping_sub](x: $iN, y: $iN) -> (res: $iN)
270                returns (
271                    if x - y > <$iN>::MAX {
272                        (x - y - $range) as $iN
273                    } else if x - y < <$iN>::MIN {
274                        (x - y + $range) as $iN
275                    } else {
276                        (x - y) as $iN
277                    }
278                );
279
280            pub open spec fn signed_crop(x: int) -> $iN {
281                if (x % ($range as int)) > (<$iN>::MAX as int) {
282                    ((x % ($range as int)) - $range) as $iN
283                } else {
284                    (x % ($range as int)) as $iN
285                }
286            }
287
288            #[verifier::allow_in_spec]
289            pub assume_specification[<$iN>::wrapping_mul](x: $iN, y: $iN) -> $iN
290                returns signed_crop(x * y);
291
292            #[verifier::allow_in_spec]
293            pub assume_specification[<$iN>::checked_add](x: $iN, y: $iN) -> Option<$iN>
294                returns (
295                    if x + y > <$iN>::MAX || x + y < <$iN>::MIN {
296                        None
297                    } else {
298                        Some((x + y) as $iN)
299                    }
300                );
301
302            #[verifier::allow_in_spec]
303            pub assume_specification[<$iN>::checked_add_unsigned](x: $iN, y: $uN) -> Option<$iN>
304                returns (
305                    if x + y > <$iN>::MAX {
306                        None
307                    } else {
308                        Some((x + y) as $iN)
309                    }
310                );
311
312            #[verifier::allow_in_spec]
313            pub assume_specification[<$uN>::saturating_add](x: $uN, y: $uN) -> $uN
314                returns (
315                    if x + y > <$uN>::MAX {
316                        <$uN>::MAX
317                    } else {
318                        (x + y) as $uN
319                    }
320                );
321
322            #[verifier::allow_in_spec]
323            pub assume_specification[<$uN>::saturating_sub](x: $uN, y: $uN) -> $uN
324                returns (
325                    if x - y < <$uN>::MIN {
326                        <$uN>::MIN
327                    } else {
328                        (x - y) as $uN
329                    }
330                );
331
332            #[verifier::allow_in_spec]
333            pub assume_specification[<$iN>::checked_sub](x: $iN, y: $iN) -> Option<$iN>
334                returns (
335                    if x - y > <$iN>::MAX || x - y < <$iN>::MIN {
336                        None
337                    } else {
338                        Some((x - y) as $iN)
339                    }
340                );
341
342            #[verifier::allow_in_spec]
343            pub assume_specification[<$iN>::checked_sub_unsigned](x: $iN, y: $uN) -> Option<$iN>
344                returns (
345                    if x - y < <$iN>::MIN {
346                        None
347                    } else {
348                        Some((x - y) as $iN)
349                    }
350                );
351
352            #[verifier::allow_in_spec]
353            pub assume_specification[<$iN>::checked_mul](x: $iN, y: $iN) -> Option<$iN>
354                returns (
355                    if x * y > <$iN>::MAX || x * y < <$iN>::MIN {
356                        None
357                    } else {
358                        Some((x * y) as $iN)
359                    }
360                );
361        }
362
363        }
364    };
365}
366
367num_specs!(u8, i8, u8_specs, i8_specs, 0x100);
368num_specs!(u16, i16, u16_specs, i16_specs, 0x1_0000);
369num_specs!(u32, i32, u32_specs, i32_specs, 0x1_0000_0000);
370num_specs!(u64, i64, u64_specs, i64_specs, 0x1_0000_0000_0000_0000);
371num_specs!(u128, i128, u128_specs, i128_specs, 0x1_0000_0000_0000_0000_0000_0000_0000_0000);
372num_specs!(usize, isize, usize_specs, isize_specs, (usize::MAX - usize::MIN + 1));
373
374verus! {
375
376// TODO move all these into the num_specs! macro to handle them for other integer widths
377// == u32 methods ==
378pub assume_specification[ u32::checked_rem ](lhs: u32, rhs: u32) -> (result: Option<u32>)
379    ensures
380        rhs == 0 ==> result is None,
381        rhs != 0 ==> result == Some((lhs % rhs) as u32),
382;
383
384pub assume_specification[ u32::checked_rem_euclid ](lhs: u32, rhs: u32) -> (result: Option<u32>)
385    ensures
386        rhs == 0 ==> result is None,
387        rhs != 0 ==> result == Some((lhs % rhs) as u32),
388;
389
390// == i32 methods ==
391pub assume_specification[ i32::checked_div ](lhs: i32, rhs: i32) -> (result: Option<i32>)
392    ensures
393        rhs == 0 ==> result is None,
394        ({
395            let x = lhs as int;
396            let d = rhs as int;
397            let output = if x == 0 {
398                0
399            } else if x > 0 && d > 0 {
400                x / d
401            } else if x < 0 && d < 0 {
402                ((x * -1) / (d * -1))
403            } else if x < 0 {
404                ((x * -1) / d) * -1
405            } else {  // d < 0
406                (x / (d * -1)) * -1
407            };
408            if output < i32::MIN || output > i32::MAX {
409                result is None
410            } else {
411                result == Some(output as i32)
412            }
413        }),
414;
415
416pub assume_specification[ i32::checked_div_euclid ](lhs: i32, rhs: i32) -> (result: Option<i32>)
417    ensures
418        rhs == 0 ==> result is None,
419        lhs / rhs < i32::MIN || lhs / rhs > i32::MAX ==> result is None,
420        i32::MIN <= lhs / rhs <= i32::MAX ==> result == Some((lhs / rhs) as i32),
421;
422
423pub assume_specification[ i32::checked_rem ](lhs: i32, rhs: i32) -> (result: Option<i32>)
424    ensures
425        rhs == 0 ==> result is None,
426        ({
427            let x = lhs as int;
428            let d = rhs as int;
429            let output = if x == 0 {
430                0
431            } else if x > 0 && d > 0 {
432                x % d
433            } else if x < 0 && d < 0 {
434                ((x * -1) % (d * -1)) * -1
435            } else if x < 0 {
436                ((x * -1) % d) * -1
437            } else {  // d < 0
438                x % (d * -1)
439            };
440            if output < i32::MIN || output > i32::MAX {
441                result is None
442            } else {
443                result == Some(output as i32)
444            }
445        }),
446;
447
448pub assume_specification[ i32::checked_rem_euclid ](lhs: i32, rhs: i32) -> (result: Option<i32>)
449    ensures
450        rhs == 0 ==> result is None,
451        lhs % rhs < i32::MIN || lhs % rhs > i32::MAX ==> result is None,
452        i32::MIN <= lhs % rhs <= i32::MAX ==> result == Some((lhs % rhs) as i32),
453;
454
455} // verus!
vstd/std_specs/num.rs

vstd/std_specs/
num.rs
