vstd/
wrapping.rs

1//! Contains trusted specifications for wrapping arithmetic behavior on the
2//! primitive integer types.
3//!
4//! Structured as follows:
5//! To get the spec for `wrapping_add` on `u8`, for example, call `u8_specs::wrapping_add`.
6//! (The module formulation seemed cleaner than defining a `wrapping_add_u8` for every
7//! operation and type.)
8use super::prelude::*;
9
10macro_rules! wrapping_specs {
11    ([$(($uN: ty, $iN: ty, $modname_u:ident, $modname_i:ident, $range:expr),)*]) => {
12        $(
13            verus! {
14
15            pub mod $modname_u {
16                use super::*;
17
18                pub open spec fn wrapping_add(x: $uN, y: $uN) -> $uN {
19                    if x + y > <$uN>::MAX {
20                        (x + y - $range) as $uN
21                    } else {
22                        (x + y) as $uN
23                    }
24                }
25
26                pub open spec fn wrapping_add_signed(x: $uN, y: $iN) -> $uN {
27                    if x + y > <$uN>::MAX {
28                        (x + y - $range) as $uN
29                    } else if x + y < 0 {
30                        (x + y + $range) as $uN
31                    } else {
32                        (x + y) as $uN
33                    }
34                }
35
36                pub open spec fn wrapping_sub(x: $uN, y: $uN) -> $uN {
37                    if x - y < 0 {
38                        (x - y + $range) as $uN
39                    } else {
40                        (x - y) as $uN
41                    }
42                }
43
44                pub open spec fn wrapping_mul(x: $uN, y: $uN) -> $uN {
45                    ((x as nat * y as nat) % $range as nat) as $uN
46                }
47            }
48
49            pub mod $modname_i {
50                use super::*;
51
52                pub open spec fn wrapping_add(x: $iN, y: $iN) -> $iN {
53                    if x + y > <$iN>::MAX {
54                        (x + y - $range) as $iN
55                    } else if x + y < <$iN>::MIN {
56                        (x + y + $range) as $iN
57                    } else {
58                        (x + y) as $iN
59                    }
60                }
61
62                pub open spec fn wrapping_add_unsigned(x: $iN, y: $uN) -> $iN {
63                    if x + y > <$iN>::MAX {
64                        (x + y - $range) as $iN
65                    } else {
66                        (x + y) as $iN
67                    }
68                }
69
70                pub open spec fn wrapping_sub(x: $iN, y: $iN) -> $iN {
71                    if x - y > <$iN>::MAX {
72                        (x - y - $range) as $iN
73                    } else if x - y < <$iN>::MIN {
74                        (x - y + $range) as $iN
75                    } else {
76                        (x - y) as $iN
77                    }
78                }
79
80                pub open spec fn signed_crop(x: int) -> $iN {
81                    if (x % ($range as int)) > (<$iN>::MAX as int) {
82                        ((x % ($range as int)) - $range) as $iN
83                    } else {
84                        (x % ($range as int)) as $iN
85                    }
86                }
87
88                pub open spec fn wrapping_mul(x: $iN, y: $iN) -> $iN {
89                    signed_crop(x * y)
90                }
91            }
92
93            }
94            )*
95
96    }
97}
98
99wrapping_specs!([
100    (u8, i8, u8_specs, i8_specs, 0x100),
101    (u16, i16, u16_specs, i16_specs, 0x1_0000),
102    (u32, i32, u32_specs, i32_specs, 0x1_0000_0000),
103    (u64, i64, u64_specs, i64_specs, 0x1_0000_0000_0000_0000),
104    (u128, i128, u128_specs, i128_specs, 0x1_0000_0000_0000_0000_0000_0000_0000_0000),
105    (usize, isize, usize_specs, isize_specs, (usize::MAX - usize::MIN + 1)),
106]);
vstd/wrapping.rs

vstd/
wrapping.rs
