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>::saturating_mul](x: $uN, y: $uN) -> $uN
265                returns (
266                    if x * y > <$uN>::MAX {
267                        <$uN>::MAX
268                    } else {
269                        (x * y) as $uN
270                    }
271                );
272
273            #[verifier::allow_in_spec]
274            #[cfg(not(verus_verify_core))]
275            pub assume_specification[<$uN>::is_multiple_of](x: $uN, y: $uN) -> bool
276                returns (
277                    if y == 0 { x == 0 } else { x % y == 0 }
278                );
279        }
280
281        // Signed ints (i8, i16, etc.)
282
283        mod $mod_i_tmp {
284            use super::*;
285
286            pub assume_specification[<$iN as Clone>::clone](x: &$iN) -> (res: $iN)
287                ensures res == x;
288
289            impl super::super::cmp::PartialEqSpecImpl for $iN {
290                open spec fn obeys_eq_spec() -> bool {
291                    true
292                }
293
294                open spec fn eq_spec(&self, other: &$iN) -> bool {
295                    *self == *other
296                }
297            }
298
299            impl super::super::cmp::PartialOrdSpecImpl for $iN {
300                open spec fn obeys_partial_cmp_spec() -> bool {
301                    true
302                }
303
304                open spec fn partial_cmp_spec(&self, other: &$iN) -> Option<Ordering> {
305                    if *self < *other {
306                        Some(Ordering::Less)
307                    } else if *self > *other {
308                        Some(Ordering::Greater)
309                    } else {
310                        Some(Ordering::Equal)
311                    }
312                }
313            }
314
315            impl super::super::cmp::OrdSpecImpl for $iN {
316                open spec fn obeys_cmp_spec() -> bool {
317                    true
318                }
319
320                open spec fn cmp_spec(&self, other: &$iN) -> Ordering {
321                    if *self < *other {
322                        Ordering::Less
323                    } else if *self > *other {
324                        Ordering::Greater
325                    } else {
326                        Ordering::Equal
327                    }
328                }
329            }
330
331            pub assume_specification[<$iN as PartialEq<$iN>>::eq](x: &$iN, y: &$iN) -> bool;
332
333            pub assume_specification[<$iN as PartialEq<$iN>>::ne](x: &$iN, y: &$iN) -> bool;
334
335            pub assume_specification[<$iN as Ord>::cmp](x: &$iN, y: &$iN) -> Ordering;
336
337            pub assume_specification[<$iN as PartialOrd<$iN>>::partial_cmp](x: &$iN, y: &$iN) -> Option<Ordering>;
338
339            pub assume_specification[<$iN as PartialOrd<$iN>>::lt](x: &$iN, y: &$iN) -> bool;
340
341            pub assume_specification[<$iN as PartialOrd<$iN>>::le](x: &$iN, y: &$iN) -> bool;
342
343            pub assume_specification[<$iN as PartialOrd<$iN>>::gt](x: &$iN, y: &$iN) -> bool;
344
345            pub assume_specification[<$iN as PartialOrd<$iN>>::ge](x: &$iN, y: &$iN) -> bool;
346
347            #[verifier::allow_in_spec]
348            #[cfg(not(verus_verify_core))]
349            pub assume_specification[<$iN>::wrapping_add](x: $iN, y: $iN) -> $iN
350                returns $mod_i::wrapping_add(x, y)
351                opens_invariants none
352                no_unwind;
353
354            #[verifier::allow_in_spec]
355            #[cfg(not(verus_verify_core))]
356            pub assume_specification[<$iN>::wrapping_add_unsigned](x: $iN, y: $uN) -> $iN
357                returns $mod_i::wrapping_add_unsigned(x, y)
358                opens_invariants none
359                no_unwind;
360
361            #[verifier::allow_in_spec]
362            #[cfg(not(verus_verify_core))]
363            pub assume_specification[<$iN>::wrapping_sub](x: $iN, y: $iN) -> (res: $iN)
364                returns $mod_i::wrapping_sub(x, y)
365                opens_invariants none
366                no_unwind;
367
368            #[verifier::allow_in_spec]
369            #[cfg(not(verus_verify_core))]
370            pub assume_specification[<$iN>::wrapping_mul](x: $iN, y: $iN) -> $iN
371                returns $mod_i::wrapping_mul(x, y)
372                opens_invariants none
373                no_unwind;
374
375            #[verifier::allow_in_spec]
376            #[cfg(not(verus_verify_core))]
377            pub assume_specification[<$iN>::wrapping_shl](x: $iN, rhs: u32) -> $iN
378                returns $mod_i::wrapping_shl(x, rhs)
379                opens_invariants none
380                no_unwind;
381
382            #[verifier::allow_in_spec]
383            #[cfg(not(verus_verify_core))]
384            pub assume_specification[<$iN>::wrapping_shr](x: $iN, rhs: u32) -> $iN
385                returns $mod_i::wrapping_shr(x, rhs)
386                opens_invariants none
387                no_unwind;
388
389            #[verifier::allow_in_spec]
390            #[cfg(not(verus_verify_core))]
391            pub assume_specification[<$iN>::checked_add](x: $iN, y: $iN) -> Option<$iN>
392                returns (
393                    if x + y > <$iN>::MAX || x + y < <$iN>::MIN {
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_add_unsigned](x: $iN, y: $uN) -> Option<$iN>
403                returns (
404                    if x + y > <$iN>::MAX {
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](x: $iN, y: $iN) -> Option<$iN>
414                returns (
415                    if x - y > <$iN>::MAX || 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_sub_unsigned](x: $iN, y: $uN) -> Option<$iN>
425                returns (
426                    if 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_mul](x: $iN, y: $iN) -> Option<$iN>
436                returns (
437                    if x * y > <$iN>::MAX || x * y < <$iN>::MIN {
438                        None
439                    } else {
440                        Some((x * y) as $iN)
441                    }
442                );
443
444            #[verifier::allow_in_spec]
445            #[cfg(not(verus_verify_core))]
446            pub assume_specification[<$iN>::checked_div](lhs: $iN, rhs: $iN) -> Option<$iN>
447                returns (
448                    if rhs == 0 || (lhs == <$iN>::MIN && rhs == -1) {
449                        None
450                    } else {
451                        Some(rust_div(lhs as int, rhs as int) as $iN)
452                    }
453                );
454
455            #[verifier::allow_in_spec]
456            #[cfg(not(verus_verify_core))]
457            pub assume_specification[<$iN>::checked_div_euclid](lhs: $iN, rhs: $iN) -> Option<$iN>
458                returns (
459                    if rhs == 0 || (lhs == <$iN>::MIN && rhs == -1) {
460                        None
461                    } else {
462                        Some((lhs / rhs) as $iN)
463                    }
464                );
465
466            #[verifier::allow_in_spec]
467            #[cfg(not(verus_verify_core))]
468            pub assume_specification[<$iN>::checked_rem](lhs: $iN, rhs: $iN) -> Option<$iN>
469                returns (
470                    if rhs == 0 || (lhs == <$iN>::MIN && rhs == -1) {
471                        None
472                    } else {
473                        Some(rust_rem(lhs as int, rhs as int) as $iN)
474                    }
475                );
476
477            #[verifier::allow_in_spec]
478            #[cfg(not(verus_verify_core))]
479            pub assume_specification[<$iN>::checked_rem_euclid](lhs: $iN, rhs: $iN) -> Option<$iN>
480                returns (
481                    if rhs == 0 || (lhs == <$iN>::MIN && rhs == -1) {
482                        None
483                    } else {
484                        Some((lhs % rhs) as $iN)
485                    }
486                );
487        }
488
489        }
490    };
491}
492
493num_specs!(u8, i8, u8_specs_tmp, i8_specs_tmp, u8_specs, i8_specs, 0x100);
494num_specs!(u16, i16, u16_specs_tmp, i16_specs_tmp, u16_specs, i16_specs, 0x1_0000);
495num_specs!(u32, i32, u32_specs_tmp, i32_specs_tmp, u32_specs, i32_specs, 0x1_0000_0000);
496num_specs!(u64, i64, u64_specs_tmp, i64_specs_tmp, u64_specs, i64_specs, 0x1_0000_0000_0000_0000);
497num_specs!(
498    u128,
499    i128,
500    u128_specs_tmp,
501    i128_specs_tmp,
502    u128_specs,
503    i128_specs,
504    0x1_0000_0000_0000_0000_0000_0000_0000_0000
505);
506num_specs!(
507    usize,
508    isize,
509    usize_specs_tmp,
510    isize_specs_tmp,
511    usize_specs,
512    isize_specs,
513    (usize::MAX - usize::MIN + 1)
514);
vstd/std_specs/num.rs

vstd/std_specs/
num.rs
