vstd/std_specs/
num.rs

Help
1#![allow(unused_imports)]
2use super::super::prelude::*;
3
4use core::cmp::Ordering;
5
6macro_rules! num_specs {
7    ($uN: ty, $iN: ty, $modname_u:ident, $modname_i:ident, $range:expr) => {
8        verus! {
9
10        // Unsigned ints (u8, u16, etc.)
11
12        // Put in separate module to avoid name collisions.
13        // Names don't matter - the user uses the stdlib functions.
14        mod $modname_u {
15            use super::*;
16
17            pub assume_specification[<$uN as Clone>::clone](x: &$uN) -> (res: $uN)
18                ensures res == x;
19
20            impl super::super::cmp::PartialEqSpecImpl for $uN {
21                open spec fn obeys_eq_spec() -> bool {
22                    true
23                }
24
25                open spec fn eq_spec(&self, other: &$uN) -> bool {
26                    *self == *other
27                }
28            }
29
30            impl super::super::cmp::PartialOrdSpecImpl for $uN {
31                open spec fn obeys_partial_cmp_spec() -> bool {
32                    true
33                }
34
35                open spec fn partial_cmp_spec(&self, other: &$uN) -> Option<Ordering> {
36                    if *self < *other {
37                        Some(Ordering::Less)
38                    } else if *self > *other {
39                        Some(Ordering::Greater)
40                    } else {
41                        Some(Ordering::Equal)
42                    }
43                }
44            }
45
46            impl super::super::cmp::OrdSpecImpl for $uN {
47                open spec fn obeys_cmp_spec() -> bool {
48                    true
49                }
50
51                open spec fn cmp_spec(&self, other: &$uN) -> Ordering {
52                    if *self < *other {
53                        Ordering::Less
54                    } else if *self > *other {
55                        Ordering::Greater
56                    } else {
57                        Ordering::Equal
58                    }
59                }
60            }
61
62            pub assume_specification[<$uN as PartialEq<$uN>>::eq](x: &$uN, y: &$uN) -> bool;
63
64            pub assume_specification[<$uN as PartialEq<$uN>>::ne](x: &$uN, y: &$uN) -> bool;
65
66            pub assume_specification[<$uN as Ord>::cmp](x: &$uN, y: &$uN) -> Ordering;
67
68            pub assume_specification[<$uN as PartialOrd<$uN>>::partial_cmp](x: &$uN, y: &$uN) -> Option<Ordering>;
69
70            pub assume_specification[<$uN as PartialOrd<$uN>>::lt](x: &$uN, y: &$uN) -> bool;
71
72            pub assume_specification[<$uN as PartialOrd<$uN>>::le](x: &$uN, y: &$uN) -> bool;
73
74            pub assume_specification[<$uN as PartialOrd<$uN>>::gt](x: &$uN, y: &$uN) -> bool;
75
76            pub assume_specification[<$uN as PartialOrd<$uN>>::ge](x: &$uN, y: &$uN) -> bool;
77
78            #[verifier::allow_in_spec]
79            pub assume_specification[<$uN>::wrapping_add](x: $uN, y: $uN) -> $uN
80                returns (
81                    if x + y > <$uN>::MAX {
82                        (x + y - $range) as $uN
83                    } else {
84                        (x + y) as $uN
85                    }
86                );
87
88            #[verifier::allow_in_spec]
89            pub assume_specification[<$uN>::wrapping_add_signed](x: $uN, y: $iN) -> $uN
90                returns (
91                    if x + y > <$uN>::MAX {
92                        (x + y - $range) as $uN
93                    } else if x + y < 0 {
94                        (x + y + $range) as $uN
95                    } else {
96                        (x + y) as $uN
97                    }
98                );
99
100            #[verifier::allow_in_spec]
101            pub assume_specification[<$uN>::wrapping_sub](x: $uN, y: $uN) -> $uN
102                returns (
103                    if x - y < 0 {
104                        (x - y + $range) as $uN
105                    } else {
106                        (x - y) as $uN
107                    }
108                );
109
110            #[verifier::allow_in_spec]
111            pub assume_specification[<$uN>::wrapping_mul](x: $uN, y: $uN) -> $uN
112                returns ((x as nat * y as nat) % $range as nat) as $uN;
113
114            #[verifier::allow_in_spec]
115            pub assume_specification[<$uN>::checked_add](x: $uN, y: $uN) -> Option<$uN>
116                returns (
117                    if x + y > <$uN>::MAX {
118                        None
119                    } else {
120                        Some((x + y) as $uN)
121                    }
122                );
123
124            #[verifier::allow_in_spec]
125            pub assume_specification[<$uN>::checked_add_signed](x: $uN, y: $iN) -> Option<$uN>
126                returns (
127                    if x + y > <$uN>::MAX || x + y < 0 {
128                        None
129                    } else {
130                        Some((x + y) as $uN)
131                    }
132                );
133
134            #[verifier::allow_in_spec]
135            pub assume_specification[<$uN>::checked_sub](x: $uN, y: $uN) -> Option<$uN>
136                returns (
137                    if x - y < 0 {
138                        None
139                    } else {
140                        Some((x - y) as $uN)
141                    }
142                );
143
144            #[verifier::allow_in_spec]
145            pub assume_specification[<$uN>::checked_mul](x: $uN, y: $uN) -> Option<$uN>
146                returns (
147                    if x * y > <$uN>::MAX {
148                        None
149                    } else {
150                        Some((x * y) as $uN)
151                    }
152                );
153
154            pub open spec fn checked_div(x: $uN, y: $uN) -> Option<$uN> {
155                if y == 0 {
156                    None
157                } else {
158                    Some(x / y)
159                }
160            }
161
162            #[verifier::when_used_as_spec(checked_div)]
163            pub assume_specification[<$uN>::checked_div](lhs: $uN, rhs: $uN) -> (result: Option<$uN>)
164                ensures
165                    result == checked_div(lhs, rhs);
166
167            #[verifier::when_used_as_spec(checked_div)]
168            pub assume_specification[<$uN>::checked_div_euclid](lhs: $uN, rhs: $uN) -> (result: Option<$uN>)
169                ensures
170                    // checked_div is the same as checked_div_euclid for unsigned ints
171                    result == checked_div(lhs, rhs);
172        }
173
174        // Signed ints (i8, i16, etc.)
175
176        mod $modname_i {
177            use super::*;
178
179            pub assume_specification[<$iN as Clone>::clone](x: &$iN) -> (res: $iN)
180                ensures res == x;
181
182            impl super::super::cmp::PartialEqSpecImpl for $iN {
183                open spec fn obeys_eq_spec() -> bool {
184                    true
185                }
186
187                open spec fn eq_spec(&self, other: &$iN) -> bool {
188                    *self == *other
189                }
190            }
191
192            impl super::super::cmp::PartialOrdSpecImpl for $iN {
193                open spec fn obeys_partial_cmp_spec() -> bool {
194                    true
195                }
196
197                open spec fn partial_cmp_spec(&self, other: &$iN) -> Option<Ordering> {
198                    if *self < *other {
199                        Some(Ordering::Less)
200                    } else if *self > *other {
201                        Some(Ordering::Greater)
202                    } else {
203                        Some(Ordering::Equal)
204                    }
205                }
206            }
207
208            impl super::super::cmp::OrdSpecImpl for $iN {
209                open spec fn obeys_cmp_spec() -> bool {
210                    true
211                }
212
213                open spec fn cmp_spec(&self, other: &$iN) -> Ordering {
214                    if *self < *other {
215                        Ordering::Less
216                    } else if *self > *other {
217                        Ordering::Greater
218                    } else {
219                        Ordering::Equal
220                    }
221                }
222            }
223
224            pub assume_specification[<$iN as PartialEq<$iN>>::eq](x: &$iN, y: &$iN) -> bool;
225
226            pub assume_specification[<$iN as PartialEq<$iN>>::ne](x: &$iN, y: &$iN) -> bool;
227
228            pub assume_specification[<$iN as Ord>::cmp](x: &$iN, y: &$iN) -> Ordering;
229
230            pub assume_specification[<$iN as PartialOrd<$iN>>::partial_cmp](x: &$iN, y: &$iN) -> Option<Ordering>;
231
232            pub assume_specification[<$iN as PartialOrd<$iN>>::lt](x: &$iN, y: &$iN) -> bool;
233
234            pub assume_specification[<$iN as PartialOrd<$iN>>::le](x: &$iN, y: &$iN) -> bool;
235
236            pub assume_specification[<$iN as PartialOrd<$iN>>::gt](x: &$iN, y: &$iN) -> bool;
237
238            pub assume_specification[<$iN as PartialOrd<$iN>>::ge](x: &$iN, y: &$iN) -> bool;
239
240            #[verifier::allow_in_spec]
241            pub assume_specification[<$iN>::wrapping_add](x: $iN, y: $iN) -> $iN
242                returns (
243                    if x + y > <$iN>::MAX {
244                        (x + y - $range) as $iN
245                    } else if x + y < <$iN>::MIN {
246                        (x + y + $range) as $iN
247                    } else {
248                        (x + y) as $iN
249                    }
250                );
251
252            #[verifier::allow_in_spec]
253            pub assume_specification[<$iN>::wrapping_add_unsigned](x: $iN, y: $uN) -> $iN
254                returns (
255                    if x + y > <$iN>::MAX {
256                        (x + y - $range) as $iN
257                    } else {
258                        (x + y) as $iN
259                    }
260                );
261
262            #[verifier::allow_in_spec]
263            pub assume_specification[<$iN>::wrapping_sub](x: $iN, y: $iN) -> (res: $iN)
264                returns (
265                    if x - y > <$iN>::MAX {
266                        (x - y - $range) as $iN
267                    } else if x - y < <$iN>::MIN {
268                        (x - y + $range) as $iN
269                    } else {
270                        (x - y) as $iN
271                    }
272                );
273
274            pub open spec fn signed_crop(x: int) -> $iN {
275                if (x % ($range as int)) > (<$iN>::MAX as int) {
276                    ((x % ($range as int)) - $range) as $iN
277                } else {
278                    (x % ($range as int)) as $iN
279                }
280            }
281
282            #[verifier::allow_in_spec]
283            pub assume_specification[<$iN>::wrapping_mul](x: $iN, y: $iN) -> $iN
284                returns signed_crop(x * y);
285
286            #[verifier::allow_in_spec]
287            pub assume_specification[<$iN>::checked_add](x: $iN, y: $iN) -> Option<$iN>
288                returns (
289                    if x + y > <$iN>::MAX || x + y < <$iN>::MIN {
290                        None
291                    } else {
292                        Some((x + y) as $iN)
293                    }
294                );
295
296            #[verifier::allow_in_spec]
297            pub assume_specification[<$iN>::checked_add_unsigned](x: $iN, y: $uN) -> Option<$iN>
298                returns (
299                    if x + y > <$iN>::MAX {
300                        None
301                    } else {
302                        Some((x + y) as $iN)
303                    }
304                );
305
306            #[verifier::allow_in_spec]
307            pub assume_specification[<$uN>::saturating_add](x: $uN, y: $uN) -> $uN
308                returns (
309                    if x + y > <$uN>::MAX {
310                        <$uN>::MAX
311                    } else {
312                        (x + y) as $uN
313                    }
314                );
315
316            #[verifier::allow_in_spec]
317            pub assume_specification[<$iN>::checked_sub](x: $iN, y: $iN) -> Option<$iN>
318                returns (
319                    if x - y > <$iN>::MAX || x - y < <$iN>::MIN {
320                        None
321                    } else {
322                        Some((x - y) as $iN)
323                    }
324                );
325
326            #[verifier::allow_in_spec]
327            pub assume_specification[<$iN>::checked_sub_unsigned](x: $iN, y: $uN) -> Option<$iN>
328                returns (
329                    if x - y < <$iN>::MIN {
330                        None
331                    } else {
332                        Some((x - y) as $iN)
333                    }
334                );
335
336            #[verifier::allow_in_spec]
337            pub assume_specification[<$iN>::checked_mul](x: $iN, y: $iN) -> Option<$iN>
338                returns (
339                    if x * y > <$iN>::MAX || x * y < <$iN>::MIN {
340                        None
341                    } else {
342                        Some((x * y) as $iN)
343                    }
344                );
345        }
346
347        }
348    };
349}
350
351num_specs!(u8, i8, u8_specs, i8_specs, 0x100);
352num_specs!(u16, i16, u16_specs, i16_specs, 0x1_0000);
353num_specs!(u32, i32, u32_specs, i32_specs, 0x1_0000_0000);
354num_specs!(u64, i64, u64_specs, i64_specs, 0x1_0000_0000_0000_0000);
355num_specs!(u128, i128, u128_specs, i128_specs, 0x1_0000_0000_0000_0000_0000_0000_0000_0000);
356num_specs!(usize, isize, usize_specs, isize_specs, (usize::MAX - usize::MIN + 1));
357
358verus! {
359
360// TODO move all these into the num_specs! macro to handle them for other integer widths
361// == u32 methods ==
362pub assume_specification[ u32::checked_rem ](lhs: u32, rhs: u32) -> (result: Option<u32>)
363    ensures
364        rhs == 0 ==> result is None,
365        rhs != 0 ==> result == Some((lhs % rhs) as u32),
366;
367
368pub assume_specification[ u32::checked_rem_euclid ](lhs: u32, rhs: u32) -> (result: Option<u32>)
369    ensures
370        rhs == 0 ==> result is None,
371        rhs != 0 ==> result == Some((lhs % rhs) as u32),
372;
373
374// == i32 methods ==
375pub assume_specification[ i32::checked_div ](lhs: i32, rhs: i32) -> (result: Option<i32>)
376    ensures
377        rhs == 0 ==> result is None,
378        ({
379            let x = lhs as int;
380            let d = rhs as int;
381            let output = if x == 0 {
382                0
383            } else if x > 0 && d > 0 {
384                x / d
385            } else if x < 0 && d < 0 {
386                ((x * -1) / (d * -1))
387            } else if x < 0 {
388                ((x * -1) / d) * -1
389            } else {  // d < 0
390                (x / (d * -1)) * -1
391            };
392            if output < i32::MIN || output > i32::MAX {
393                result is None
394            } else {
395                result == Some(output as i32)
396            }
397        }),
398;
399
400pub assume_specification[ i32::checked_div_euclid ](lhs: i32, rhs: i32) -> (result: Option<i32>)
401    ensures
402        rhs == 0 ==> result is None,
403        lhs / rhs < i32::MIN || lhs / rhs > i32::MAX ==> result is None,
404        i32::MIN <= lhs / rhs <= i32::MAX ==> result == Some((lhs / rhs) as i32),
405;
406
407pub assume_specification[ i32::checked_rem ](lhs: i32, rhs: i32) -> (result: Option<i32>)
408    ensures
409        rhs == 0 ==> result is None,
410        ({
411            let x = lhs as int;
412            let d = rhs as int;
413            let output = if x == 0 {
414                0
415            } else if x > 0 && d > 0 {
416                x % d
417            } else if x < 0 && d < 0 {
418                ((x * -1) % (d * -1)) * -1
419            } else if x < 0 {
420                ((x * -1) % d) * -1
421            } else {  // d < 0
422                x % (d * -1)
423            };
424            if output < i32::MIN || output > i32::MAX {
425                result is None
426            } else {
427                result == Some(output as i32)
428            }
429        }),
430;
431
432pub assume_specification[ i32::checked_rem_euclid ](lhs: i32, rhs: i32) -> (result: Option<i32>)
433    ensures
434        rhs == 0 ==> result is None,
435        lhs % rhs < i32::MIN || lhs % rhs > i32::MAX ==> result is None,
436        i32::MIN <= lhs % rhs <= i32::MAX ==> result == Some((lhs % rhs) as i32),
437;
438
439} // verus!
vstd/std_specs/num.rs

vstd/std_specs/
num.rs
