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, $bits: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                pub open spec fn wrapping_shl(x: $uN, shift: u32) -> $uN {
49                    x << (shift % $bits)
50                }
51                pub open spec fn wrapping_shr(x: $uN, shift: u32) -> $uN {
52                    x >> (shift % $bits)
53                }
54
55            }
56            pub mod $modname_i {
57                use super::*;
58
59                pub open spec fn wrapping_add(x: $iN, y: $iN) -> $iN {
60                    if x + y > <$iN>::MAX {
61                        (x + y - $range) as $iN
62                    } else if x + y < <$iN>::MIN {
63                        (x + y + $range) as $iN
64                    } else {
65                        (x + y) as $iN
66                    }
67                }
68
69                pub open spec fn wrapping_add_unsigned(x: $iN, y: $uN) -> $iN {
70                    if x + y > <$iN>::MAX {
71                        (x + y - $range) as $iN
72                    } else {
73                        (x + y) as $iN
74                    }
75                }
76
77                pub open spec fn wrapping_sub(x: $iN, y: $iN) -> $iN {
78                    if x - y > <$iN>::MAX {
79                        (x - y - $range) as $iN
80                    } else if x - y < <$iN>::MIN {
81                        (x - y + $range) as $iN
82                    } else {
83                        (x - y) as $iN
84                    }
85                }
86
87                pub open spec fn signed_crop(x: int) -> $iN {
88                    if (x % ($range as int)) > (<$iN>::MAX as int) {
89                        ((x % ($range as int)) - $range) as $iN
90                    } else {
91                        (x % ($range as int)) as $iN
92                    }
93                }
94
95                pub open spec fn wrapping_mul(x: $iN, y: $iN) -> $iN {
96                    signed_crop(x * y)
97                }
98
99                pub open spec fn wrapping_shl(x: $iN, shift: u32) -> $iN {
100                    x << (shift % $bits)
101                }
102                pub open spec fn wrapping_shr(x: $iN, shift: u32) -> $iN {
103                    x >> (shift % $bits)
104                }
105
106            }
107        }
108            )*
109    }
110}
111wrapping_specs!([
112    (u8, i8, u8_specs, i8_specs, 0x100, 8u32),
113    (u16, i16, u16_specs, i16_specs, 0x1_0000, 16u32),
114    (u32, i32, u32_specs, i32_specs, 0x1_0000_0000, 32u32),
115    (u64, i64, u64_specs, i64_specs, 0x1_0000_0000_0000_0000, 64u32),
116    (u128, i128, u128_specs, i128_specs, 0x1_0000_0000_0000_0000_0000_0000_0000_0000, 128u32),
117    (usize, isize, usize_specs, isize_specs, (usize::MAX - usize::MIN + 1), usize::BITS),
118]);
vstd/wrapping.rs

vstd/
wrapping.rs
