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
149            #[verifier::allow_in_spec]
150            #[cfg(not(verus_verify_core))]
151            pub assume_specification[<$uN>::checked_add_signed](x: $uN, y: $iN) -> Option<$uN>
152                returns (
153                    if x + y > <$uN>::MAX || x + y < 0 {
154                        None
155                    } else {
156                        Some((x + y) as $uN)
157                    }
158                );
159
160            #[verifier::allow_in_spec]
161            #[cfg(not(verus_verify_core))]
162            pub assume_specification[<$uN>::checked_sub](x: $uN, y: $uN) -> Option<$uN>
163                returns (
164                    if x - y < 0 {
165                        None
166                    } else {
167                        Some((x - y) as $uN)
168                    }
169                );
170
171            #[verifier::allow_in_spec]
172            #[cfg(not(verus_verify_core))]
173            pub assume_specification[<$uN>::checked_mul](x: $uN, y: $uN) -> Option<$uN>
174                returns (
175                    if x * y > <$uN>::MAX {
176                        None
177                    } else {
178                        Some((x * y) as $uN)
179                    }
180                );
181
182            #[verifier::allow_in_spec]
183            #[cfg(not(verus_verify_core))]
184            pub assume_specification[<$uN>::checked_next_multiple_of](x: $uN, rhs: $uN) -> Option<$uN>
185                returns (
186                    if rhs == 0 {
187                        None
188                    } else if next_multiple_of(x as int, rhs as int) > <$uN>::MAX {
189                        None
190                    } else {
191                        Some(next_multiple_of(x as int, rhs as int) as $uN)
192                    }
193                );
194
195            pub open spec fn checked_div(x: $uN, y: $uN) -> Option<$uN> {
196                if y == 0 {
197                    None
198                } else {
199                    Some(x / y)
200                }
201            }
202
203            #[verifier::when_used_as_spec(checked_div)]
204            #[cfg(not(verus_verify_core))]
205            pub assume_specification[<$uN>::checked_div](lhs: $uN, rhs: $uN) -> (result: Option<$uN>)
206                ensures
207                    result == checked_div(lhs, rhs);
208
209            #[verifier::when_used_as_spec(checked_div)]
210            #[cfg(not(verus_verify_core))]
211            pub assume_specification[<$uN>::checked_div_euclid](lhs: $uN, rhs: $uN) -> (result: Option<$uN>)
212                ensures
213                    // checked_div is the same as checked_div_euclid for unsigned ints
214                    result == checked_div(lhs, rhs);
215
216            #[verifier::allow_in_spec]
217            #[cfg(not(verus_verify_core))]
218            pub assume_specification[<$uN>::checked_rem](lhs: $uN, rhs: $uN) -> Option<$uN>
219                returns (
220                    if rhs == 0 {
221                        None
222                    }
223                    else {
224                        Some((lhs % rhs) as $uN)
225                    }
226                );
227
228            #[verifier::allow_in_spec]
229            #[cfg(not(verus_verify_core))]
230            pub assume_specification[<$uN>::checked_rem_euclid](lhs: $uN, rhs: $uN) -> Option<$uN>
231                returns (
232                    if rhs == 0 {
233                        None
234                    }
235                    else {
236                        Some((lhs % rhs) as $uN)
237                    }
238                );
239
240            #[verifier::allow_in_spec]
241            #[cfg(not(verus_verify_core))]
242            pub assume_specification[<$uN>::saturating_add](x: $uN, y: $uN) -> $uN
243                returns (
244                    if x + y > <$uN>::MAX {
245                        <$uN>::MAX
246                    } else {
247                        (x + y) as $uN
248                    }
249                );
250
251            #[verifier::allow_in_spec]
252            #[cfg(not(verus_verify_core))]
253            pub assume_specification[<$uN>::saturating_sub](x: $uN, y: $uN) -> $uN
254                returns (
255                    if x - y < <$uN>::MIN {
256                        <$uN>::MIN
257                    } else {
258                        (x - y) as $uN
259                    }
260                );
261
262            #[verifier::allow_in_spec]
263            #[cfg(not(verus_verify_core))]
264            pub assume_specification[<$uN>::is_multiple_of](x: $uN, y: $uN) -> bool
265                returns (
266                    if y == 0 { x == 0 } else { x % y == 0 }
267                );
268        }
269
270        // Signed ints (i8, i16, etc.)
271
272        mod $mod_i_tmp {
273            use super::*;
274
275            pub assume_specification[<$iN as Clone>::clone](x: &$iN) -> (res: $iN)
276                ensures res == x;
277
278            impl super::super::cmp::PartialEqSpecImpl for $iN {
279                open spec fn obeys_eq_spec() -> bool {
280                    true
281                }
282
283                open spec fn eq_spec(&self, other: &$iN) -> bool {
284                    *self == *other
285                }
286            }
287
288            impl super::super::cmp::PartialOrdSpecImpl for $iN {
289                open spec fn obeys_partial_cmp_spec() -> bool {
290                    true
291                }
292
293                open spec fn partial_cmp_spec(&self, other: &$iN) -> Option<Ordering> {
294                    if *self < *other {
295                        Some(Ordering::Less)
296                    } else if *self > *other {
297                        Some(Ordering::Greater)
298                    } else {
299                        Some(Ordering::Equal)
300                    }
301                }
302            }
303
304            impl super::super::cmp::OrdSpecImpl for $iN {
305                open spec fn obeys_cmp_spec() -> bool {
306                    true
307                }
308
309                open spec fn cmp_spec(&self, other: &$iN) -> Ordering {
310                    if *self < *other {
311                        Ordering::Less
312                    } else if *self > *other {
313                        Ordering::Greater
314                    } else {
315                        Ordering::Equal
316                    }
317                }
318            }
319
320            pub assume_specification[<$iN as PartialEq<$iN>>::eq](x: &$iN, y: &$iN) -> bool;
321
322            pub assume_specification[<$iN as PartialEq<$iN>>::ne](x: &$iN, y: &$iN) -> bool;
323
324            pub assume_specification[<$iN as Ord>::cmp](x: &$iN, y: &$iN) -> Ordering;
325
326            pub assume_specification[<$iN as PartialOrd<$iN>>::partial_cmp](x: &$iN, y: &$iN) -> Option<Ordering>;
327
328            pub assume_specification[<$iN as PartialOrd<$iN>>::lt](x: &$iN, y: &$iN) -> bool;
329
330            pub assume_specification[<$iN as PartialOrd<$iN>>::le](x: &$iN, y: &$iN) -> bool;
331
332            pub assume_specification[<$iN as PartialOrd<$iN>>::gt](x: &$iN, y: &$iN) -> bool;
333
334            pub assume_specification[<$iN as PartialOrd<$iN>>::ge](x: &$iN, y: &$iN) -> bool;
335
336            #[verifier::allow_in_spec]
337            #[cfg(not(verus_verify_core))]
338            pub assume_specification[<$iN>::wrapping_add](x: $iN, y: $iN) -> $iN
339                returns $mod_i::wrapping_add(x, y)
340                opens_invariants none
341                no_unwind;
342
343            #[verifier::allow_in_spec]
344            #[cfg(not(verus_verify_core))]
345            pub assume_specification[<$iN>::wrapping_add_unsigned](x: $iN, y: $uN) -> $iN
346                returns $mod_i::wrapping_add_unsigned(x, y)
347                opens_invariants none
348                no_unwind;
349
350            #[verifier::allow_in_spec]
351            #[cfg(not(verus_verify_core))]
352            pub assume_specification[<$iN>::wrapping_sub](x: $iN, y: $iN) -> (res: $iN)
353                returns $mod_i::wrapping_sub(x, y)
354                opens_invariants none
355                no_unwind;
356
357            #[verifier::allow_in_spec]
358            #[cfg(not(verus_verify_core))]
359            pub assume_specification[<$iN>::wrapping_mul](x: $iN, y: $iN) -> $iN
360                returns $mod_i::wrapping_mul(x, y)
361                opens_invariants none
362                no_unwind;
363
364            #[verifier::allow_in_spec]
365            #[cfg(not(verus_verify_core))]
366            pub assume_specification[<$iN>::wrapping_shl](x: $iN, rhs: u32) -> $iN
367                returns $mod_i::wrapping_shl(x, rhs)
368                opens_invariants none
369                no_unwind;
370
371            #[verifier::allow_in_spec]
372            #[cfg(not(verus_verify_core))]
373            pub assume_specification[<$iN>::wrapping_shr](x: $iN, rhs: u32) -> $iN
374                returns $mod_i::wrapping_shr(x, rhs)
375                opens_invariants none
376                no_unwind;
377
378            #[verifier::allow_in_spec]
379            #[cfg(not(verus_verify_core))]
380            pub assume_specification[<$iN>::checked_add](x: $iN, y: $iN) -> Option<$iN>
381                returns (
382                    if x + y > <$iN>::MAX || x + y < <$iN>::MIN {
383                        None
384                    } else {
385                        Some((x + y) as $iN)
386                    }
387                );
388
389            #[verifier::allow_in_spec]
390            #[cfg(not(verus_verify_core))]
391            pub assume_specification[<$iN>::checked_add_unsigned](x: $iN, y: $uN) -> Option<$iN>
392                returns (
393                    if x + y > <$iN>::MAX {
394                        None
395                    } else {
396                        Some((x + y) as $iN)
397                    }
398                );
399
400            #[verifier::allow_in_spec]
401            #[cfg(not(verus_verify_core))]
402            pub assume_specification[<$iN>::checked_sub](x: $iN, y: $iN) -> Option<$iN>
403                returns (
404                    if x - y > <$iN>::MAX || x - y < <$iN>::MIN {
405                        None
406                    } else {
407                        Some((x - y) as $iN)
408                    }
409                );
410
411            #[verifier::allow_in_spec]
412            #[cfg(not(verus_verify_core))]
413            pub assume_specification[<$iN>::checked_sub_unsigned](x: $iN, y: $uN) -> Option<$iN>
414                returns (
415                    if x - y < <$iN>::MIN {
416                        None
417                    } else {
418                        Some((x - y) as $iN)
419                    }
420                );
421
422            #[verifier::allow_in_spec]
423            #[cfg(not(verus_verify_core))]
424            pub assume_specification[<$iN>::checked_mul](x: $iN, y: $iN) -> Option<$iN>
425                returns (
426                    if x * y > <$iN>::MAX || x * y < <$iN>::MIN {
427                        None
428                    } else {
429                        Some((x * y) as $iN)
430                    }
431                );
432
433            #[verifier::allow_in_spec]
434            #[cfg(not(verus_verify_core))]
435            pub assume_specification[<$iN>::checked_div](lhs: $iN, rhs: $iN) -> Option<$iN>
436                returns (
437                    if rhs == 0 || (lhs == <$iN>::MIN && rhs == -1) {
438                        None
439                    } else {
440                        Some(rust_div(lhs as int, rhs as int) as $iN)
441                    }
442                );
443
444            #[verifier::allow_in_spec]
445            #[cfg(not(verus_verify_core))]
446            pub assume_specification[<$iN>::checked_div_euclid](lhs: $iN, rhs: $iN) -> Option<$iN>
447                returns (
448                    if rhs == 0 || (lhs == <$iN>::MIN && rhs == -1) {
449                        None
450                    } else {
451                        Some((lhs / rhs) as $iN)
452                    }
453                );
454
455            #[verifier::allow_in_spec]
456            #[cfg(not(verus_verify_core))]
457            pub assume_specification[<$iN>::checked_rem](lhs: $iN, rhs: $iN) -> Option<$iN>
458                returns (
459                    if rhs == 0 || (lhs == <$iN>::MIN && rhs == -1) {
460                        None
461                    } else {
462                        Some(rust_rem(lhs as int, rhs as int) as $iN)
463                    }
464                );
465
466            #[verifier::allow_in_spec]
467            #[cfg(not(verus_verify_core))]
468            pub assume_specification[<$iN>::checked_rem_euclid](lhs: $iN, rhs: $iN) -> Option<$iN>
469                returns (
470                    if rhs == 0 || (lhs == <$iN>::MIN && rhs == -1) {
471                        None
472                    } else {
473                        Some((lhs % rhs) as $iN)
474                    }
475                );
476        }
477
478        }
479    };
480}
481
482num_specs!(u8, i8, u8_specs_tmp, i8_specs_tmp, u8_specs, i8_specs, 0x100);
483num_specs!(u16, i16, u16_specs_tmp, i16_specs_tmp, u16_specs, i16_specs, 0x1_0000);
484num_specs!(u32, i32, u32_specs_tmp, i32_specs_tmp, u32_specs, i32_specs, 0x1_0000_0000);
485num_specs!(u64, i64, u64_specs_tmp, i64_specs_tmp, u64_specs, i64_specs, 0x1_0000_0000_0000_0000);
486num_specs!(
487    u128,
488    i128,
489    u128_specs_tmp,
490    i128_specs_tmp,
491    u128_specs,
492    i128_specs,
493    0x1_0000_0000_0000_0000_0000_0000_0000_0000
494);
495num_specs!(
496    usize,
497    isize,
498    usize_specs_tmp,
499    isize_specs_tmp,
500    usize_specs,
501    isize_specs,
502    (usize::MAX - usize::MIN + 1)
503);
vstd/std_specs/num.rs

vstd/std_specs/
num.rs
