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