vstd/arithmetic/overflow.rs
1/// This file defines structs `CheckedU8`, `CheckedU16`, etc. and
2/// their associated methods to handle `u8`, `u16`, etc. values that
3/// can overflow. Each struct includes a ghost value representing the
4/// true value (not subject to overflow), so that the `view` function
5/// can provide the true value.
6///
7/// It's a fully verified library, i.e., it contains no trusted code.
8///
9/// Here are some examples using `CheckedU64`. (See
10/// `examples/overflow.rs` for more examples, including
11/// ones for the analogous `CheckedU32`.)
12///
13/// ```
14/// fn test1()
15/// {
16/// let w = CheckedU64::new(0xFFFFFFFFFFFFFFFF);
17/// let x = w.add_value(1);
18/// assert(x.is_overflowed());
19/// assert(x.view() == 0x10000000000000000);
20///
21/// let y = CheckedU64::new(0x8000000000000000);
22/// let z = y.mul_value(2);
23/// assert(z.is_overflowed());
24/// assert(z.view() == 0x10000000000000000);
25/// }
26///
27/// fn test2(a: u64, b: u64, c: u64, d: u64) -> (e: Option<u64>)
28/// ensures
29/// match e {
30/// Some(v) => v == a * b + c * d,
31/// None => a * b + c * d > u64::MAX,
32/// }
33/// {
34/// let a_times_b = CheckedU64::new(a).mul_value(b);
35/// let c_times_d = CheckedU64::new(c).mul_value(d);
36/// let sum_of_products = a_times_b.add_checked(&c_times_d);
37/// if sum_of_products.is_overflowed() {
38/// assert(a * b + c * d > u64::MAX);
39/// None
40/// }
41/// else {
42/// let i: u64 = sum_of_products.unwrap();
43/// assert(i == a * b + c * d);
44/// Some(i)
45/// }
46/// }
47/// ```
48#[allow(unused_imports)]
49use super::super::prelude::*;
50#[allow(unused_imports)]
51use super::super::view::View;
52#[allow(unused_imports)]
53#[cfg(verus_keep_ghost)]
54use super::mul::{lemma_mul_by_zero_is_zero, lemma_mul_inequality, lemma_mul_is_commutative};
55#[allow(unused_imports)]
56use super::*;
57macro_rules! checked_uint_gen {
58 // This macro should be instantiated with the following parameters:
59 //
60 // $uty - The name of the `std` unsigned integer, e.g., `u64`
61 // $cty - The name of the checked struct to create, e.g., `CheckedU64`
62 ($uty: ty, $cty: ty) => {
63 verus! {
64
65 /// This struct represents a `$uty` value that can overflow. The `i` field
66 /// is a ghost value that represents the true value, while the `v` field
67 /// is `None` when the value has overflowed and `Some(x)` when the value
68 /// `x` fits in a `$uty`.
69 pub struct $cty {
70 i: Ghost<nat>,
71 v: Option<$uty>,
72 }
73
74 /// The view of an `$cty` instance is the true value of the instance.
75 impl View for $cty
76 {
77 type V = nat;
78
79 closed spec fn view(&self) -> nat
80 {
81 self.i@
82 }
83 }
84
85 impl Clone for $cty {
86 /// Clones the `$cty` instance.
87 /// Ensures the cloned instance has the same value as the original.
88 exec fn clone(&self) -> (result: Self)
89 ensures
90 result@ == self@
91 {
92 proof { use_type_invariant(self); }
93 Self{ i: self.i, v: self.v }
94 }
95 }
96
97 impl $cty {
98 /// This is the internal type invariant for an `$cty`.
99 /// It ensures the key invariant that relates `i` and `v`.
100 #[verifier::type_invariant]
101 spec fn well_formed(self) -> bool
102 {
103 match self.v {
104 Some(v) => self.i@ == v,
105 None => self.i@ > $uty::MAX,
106 }
107 }
108
109 /// Creates a new `$cty` instance from a `$uty` value.
110 /// Ensures the internal representation matches the provided value.
111 pub closed spec fn spec_new(v: $uty) -> $cty
112 {
113 $cty{ i: Ghost(v as nat), v: Some(v) }
114 }
115
116 /// Creates a new `$cty` instance from a `$uty` value.
117 /// Ensures the internal representation matches the provided value.
118 #[verifier::when_used_as_spec(spec_new)]
119 pub exec fn new(v: $uty) -> (result: Self)
120 ensures
121 result@ == v,
122 {
123 Self{ i: Ghost(v as nat), v: Some(v) }
124 }
125
126 /// Creates a new `$cty` instance with an overflowed value.
127 /// Requires the provided value to be greater than `$uty::MAX`.
128 /// Ensures the internal representation matches the provided value.
129 pub exec fn new_overflowed(Ghost(i): Ghost<int>) -> (result: Self)
130 requires
131 i > $uty::MAX,
132 ensures
133 result@ == i,
134 {
135 Self{ i: Ghost(i as nat), v: None }
136 }
137
138 /// Checks if the `$cty` instance is overflowed.
139 /// Returns true if the value is greater than `$uty::MAX`.
140 pub open spec fn spec_is_overflowed(&self) -> bool
141 {
142 self@ > $uty::MAX
143 }
144
145 /// Checks if the `$cty` instance is overflowed.
146 /// Returns true if the value is greater than `$uty::MAX`.
147 #[verifier::when_used_as_spec(spec_is_overflowed)]
148 pub exec fn is_overflowed(&self) -> (result: bool)
149 ensures
150 result == self.spec_is_overflowed()
151 {
152 proof { use_type_invariant(self) }
153 self.v.is_none()
154 }
155
156 /// Unwraps the `$cty` instance to get the `$uty` value.
157 /// Requires the instance to not be overflowed.
158 /// Ensures the returned value matches the internal representation.
159 pub exec fn unwrap(&self) -> (result: $uty)
160 requires
161 !self.is_overflowed(),
162 ensures
163 result == self@,
164 {
165 proof { use_type_invariant(self) }
166 self.v.unwrap()
167 }
168
169 /// Converts the `$cty` instance to an `Option<$uty>`.
170 /// Ensures the returned option matches the internal representation.
171 pub exec fn to_option(&self) -> (result: Option<$uty>)
172 ensures
173 match result {
174 Some(v) => self@ == v && v <= $uty::MAX,
175 None => self@ > $uty::MAX,
176 }
177 {
178 proof { use_type_invariant(self); }
179 self.v
180 }
181
182 /// Adds a `$uty` value to the `$cty` instance.
183 /// Ensures the resulting value matches the sum of
184 /// the internal representation and the provided
185 /// value.
186 #[inline]
187 pub exec fn add_value(&self, v2: $uty) -> (result: Self)
188 ensures
189 result@ == self@ + v2,
190 {
191 proof {
192 use_type_invariant(&self);
193 }
194 let i: Ghost<nat> = Ghost((&self@ + v2) as nat);
195 match self.v {
196 Some(v1) => Self{ i, v: v1.checked_add(v2) },
197 None => Self{ i, v: None },
198 }
199 }
200
201 /// Adds another `$cty` instance to the current
202 /// instance. Ensures the resulting value matches
203 /// the sum of the internal representations of
204 /// both instances.
205 #[inline]
206 pub exec fn add_checked(&self, v2: &$cty) -> (result: Self)
207 ensures
208 result@ == self@ + v2@,
209 {
210 proof {
211 use_type_invariant(self);
212 use_type_invariant(v2);
213 }
214 match v2.v {
215 Some(n) => self.add_value(n),
216 None => {
217 let i: Ghost<nat> = Ghost((self@ + v2@) as nat);
218 Self{ i, v: None }
219 }
220 }
221 }
222
223 /// Multiplies the `$cty` instance by a `$uty`
224 /// value. Ensures the resulting value matches the
225 /// product of the internal representation and the
226 /// provided value.
227 #[inline]
228 pub exec fn mul_value(&self, v2: $uty) -> (result: Self)
229 ensures
230 result@ == self@ as int * v2 as int,
231 {
232 proof {
233 use_type_invariant(self);
234 }
235 let i: Ghost<nat> = Ghost((self@ * v2) as nat);
236 match self.v {
237 Some(n1) => Self{ i, v: n1.checked_mul(v2) },
238 None => {
239 if v2 == 0 {
240 assert(i@ == 0) by {
241 lemma_mul_by_zero_is_zero(self@ as int);
242 }
243 Self{ i, v: Some(0) }
244 }
245 else {
246 assert(self@ * v2 >= self@ * 1 == self@) by {
247 lemma_mul_inequality(1, v2 as int, self@ as int);
248 lemma_mul_is_commutative(self@ as int, v2 as int);
249 }
250 Self{ i, v: None }
251 }
252 },
253 }
254 }
255
256 /// Multiplies the `$cty` instance by another `$cty` instance.
257 /// Ensures the resulting value matches the product of the internal
258 /// representations of both instances.
259 #[inline]
260 pub exec fn mul_checked(&self, v2: &Self) -> (result: Self)
261 ensures
262 result@ == self@ as int * v2@ as int,
263 {
264 proof {
265 use_type_invariant(self);
266 use_type_invariant(v2);
267 }
268 let i: Ghost<nat> = Ghost((self@ * v2@) as nat);
269 match v2.v {
270 Some(n) => self.mul_value(n),
271 None => {
272 match self.v {
273 Some(n1) => {
274 if n1 == 0 {
275 assert(i@ == 0) by {
276 lemma_mul_by_zero_is_zero(v2@ as int);
277 }
278 Self{ i, v: Some(0) }
279 }
280 else {
281 assert(self@ * v2@ >= 1 * v2@ == v2@) by {
282 lemma_mul_inequality(1, self@ as int, v2@ as int);
283 }
284 Self{ i, v: None }
285 }
286 },
287 None => {
288 assert(self@ * v2@ > $uty::MAX) by {
289 lemma_mul_inequality(1, self@ as int, v2@ as int);
290 }
291 Self{ i, v: None }
292 },
293 }
294 }
295 }
296 }
297 }
298 }
299 };
300}
301
302checked_uint_gen!(u8, CheckedU8);
303checked_uint_gen!(u16, CheckedU16);
304checked_uint_gen!(u32, CheckedU32);
305checked_uint_gen!(u64, CheckedU64);
306checked_uint_gen!(u128, CheckedU128);
307checked_uint_gen!(usize, CheckedUsize);