vstd/std_specs/
num.rs

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

vstd/std_specs/
num.rs
