vstd/std_specs/
num.rs

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            #[verifier::allow_in_spec]
174            pub assume_specification[<$uN>::checked_rem](lhs: $uN, rhs: $uN) -> Option<$uN>
175                returns (
176                    if rhs == 0 {
177                        None
178                    }
179                    else {
180                        Some((lhs % rhs) as $uN)
181                    }
182                );
183
184            #[verifier::allow_in_spec]
185            pub assume_specification[<$uN>::checked_rem_euclid](lhs: $uN, rhs: $uN) -> Option<$uN>
186                returns (
187                    if rhs == 0 {
188                        None
189                    }
190                    else {
191                        Some((lhs % rhs) as $uN)
192                    }
193                );
194
195            #[verifier::allow_in_spec]
196            pub assume_specification[<$uN>::saturating_add](x: $uN, y: $uN) -> $uN
197                returns (
198                    if x + y > <$uN>::MAX {
199                        <$uN>::MAX
200                    } else {
201                        (x + y) as $uN
202                    }
203                );
204
205            #[verifier::allow_in_spec]
206            pub assume_specification[<$uN>::saturating_sub](x: $uN, y: $uN) -> $uN
207                returns (
208                    if x - y < <$uN>::MIN {
209                        <$uN>::MIN
210                    } else {
211                        (x - y) as $uN
212                    }
213                );
214
215            #[verifier::allow_in_spec]
216            pub assume_specification[<$uN>::is_multiple_of](x: $uN, y: $uN) -> bool
217                returns (
218                    if y == 0 { x == 0 } else { x % y == 0 }
219                );
220        }
221
222        // Signed ints (i8, i16, etc.)
223
224        mod $modname_i {
225            use super::*;
226
227            pub assume_specification[<$iN as Clone>::clone](x: &$iN) -> (res: $iN)
228                ensures res == x;
229
230            impl super::super::cmp::PartialEqSpecImpl for $iN {
231                open spec fn obeys_eq_spec() -> bool {
232                    true
233                }
234
235                open spec fn eq_spec(&self, other: &$iN) -> bool {
236                    *self == *other
237                }
238            }
239
240            impl super::super::cmp::PartialOrdSpecImpl for $iN {
241                open spec fn obeys_partial_cmp_spec() -> bool {
242                    true
243                }
244
245                open spec fn partial_cmp_spec(&self, other: &$iN) -> Option<Ordering> {
246                    if *self < *other {
247                        Some(Ordering::Less)
248                    } else if *self > *other {
249                        Some(Ordering::Greater)
250                    } else {
251                        Some(Ordering::Equal)
252                    }
253                }
254            }
255
256            impl super::super::cmp::OrdSpecImpl for $iN {
257                open spec fn obeys_cmp_spec() -> bool {
258                    true
259                }
260
261                open spec fn cmp_spec(&self, other: &$iN) -> Ordering {
262                    if *self < *other {
263                        Ordering::Less
264                    } else if *self > *other {
265                        Ordering::Greater
266                    } else {
267                        Ordering::Equal
268                    }
269                }
270            }
271
272            pub assume_specification[<$iN as PartialEq<$iN>>::eq](x: &$iN, y: &$iN) -> bool;
273
274            pub assume_specification[<$iN as PartialEq<$iN>>::ne](x: &$iN, y: &$iN) -> bool;
275
276            pub assume_specification[<$iN as Ord>::cmp](x: &$iN, y: &$iN) -> Ordering;
277
278            pub assume_specification[<$iN as PartialOrd<$iN>>::partial_cmp](x: &$iN, y: &$iN) -> Option<Ordering>;
279
280            pub assume_specification[<$iN as PartialOrd<$iN>>::lt](x: &$iN, y: &$iN) -> bool;
281
282            pub assume_specification[<$iN as PartialOrd<$iN>>::le](x: &$iN, y: &$iN) -> bool;
283
284            pub assume_specification[<$iN as PartialOrd<$iN>>::gt](x: &$iN, y: &$iN) -> bool;
285
286            pub assume_specification[<$iN as PartialOrd<$iN>>::ge](x: &$iN, y: &$iN) -> bool;
287
288            #[verifier::allow_in_spec]
289            pub assume_specification[<$iN>::wrapping_add](x: $iN, y: $iN) -> $iN
290                returns (
291                    if x + y > <$iN>::MAX {
292                        (x + y - $range) as $iN
293                    } else if x + y < <$iN>::MIN {
294                        (x + y + $range) as $iN
295                    } else {
296                        (x + y) as $iN
297                    }
298                );
299
300            #[verifier::allow_in_spec]
301            pub assume_specification[<$iN>::wrapping_add_unsigned](x: $iN, y: $uN) -> $iN
302                returns (
303                    if x + y > <$iN>::MAX {
304                        (x + y - $range) as $iN
305                    } else {
306                        (x + y) as $iN
307                    }
308                );
309
310            #[verifier::allow_in_spec]
311            pub assume_specification[<$iN>::wrapping_sub](x: $iN, y: $iN) -> (res: $iN)
312                returns (
313                    if x - y > <$iN>::MAX {
314                        (x - y - $range) as $iN
315                    } else if x - y < <$iN>::MIN {
316                        (x - y + $range) as $iN
317                    } else {
318                        (x - y) as $iN
319                    }
320                );
321
322            pub open spec fn signed_crop(x: int) -> $iN {
323                if (x % ($range as int)) > (<$iN>::MAX as int) {
324                    ((x % ($range as int)) - $range) as $iN
325                } else {
326                    (x % ($range as int)) as $iN
327                }
328            }
329
330            #[verifier::allow_in_spec]
331            pub assume_specification[<$iN>::wrapping_mul](x: $iN, y: $iN) -> $iN
332                returns signed_crop(x * y);
333
334            #[verifier::allow_in_spec]
335            pub assume_specification[<$iN>::checked_add](x: $iN, y: $iN) -> Option<$iN>
336                returns (
337                    if x + y > <$iN>::MAX || x + y < <$iN>::MIN {
338                        None
339                    } else {
340                        Some((x + y) as $iN)
341                    }
342                );
343
344            #[verifier::allow_in_spec]
345            pub assume_specification[<$iN>::checked_add_unsigned](x: $iN, y: $uN) -> Option<$iN>
346                returns (
347                    if x + y > <$iN>::MAX {
348                        None
349                    } else {
350                        Some((x + y) as $iN)
351                    }
352                );
353
354            #[verifier::allow_in_spec]
355            pub assume_specification[<$iN>::checked_sub](x: $iN, y: $iN) -> Option<$iN>
356                returns (
357                    if x - y > <$iN>::MAX || x - y < <$iN>::MIN {
358                        None
359                    } else {
360                        Some((x - y) as $iN)
361                    }
362                );
363
364            #[verifier::allow_in_spec]
365            pub assume_specification[<$iN>::checked_sub_unsigned](x: $iN, y: $uN) -> Option<$iN>
366                returns (
367                    if x - y < <$iN>::MIN {
368                        None
369                    } else {
370                        Some((x - y) as $iN)
371                    }
372                );
373
374            #[verifier::allow_in_spec]
375            pub assume_specification[<$iN>::checked_mul](x: $iN, y: $iN) -> Option<$iN>
376                returns (
377                    if x * y > <$iN>::MAX || x * y < <$iN>::MIN {
378                        None
379                    } else {
380                        Some((x * y) as $iN)
381                    }
382                );
383
384            #[verifier::allow_in_spec]
385            pub assume_specification[<$iN>::checked_div](lhs: $iN, rhs: $iN) -> Option<$iN>
386                returns (
387                    if rhs == 0 {
388                        None
389                    }
390                    else {
391                        let x = lhs as int;
392                        let d = rhs as int;
393                        let output = if x == 0 {
394                            0
395                        } else if x > 0 && d > 0 {
396                            x / d
397                        } else if x < 0 && d < 0 {
398                            ((x * -1) / (d * -1))
399                        } else if x < 0 {
400                            ((x * -1) / d) * -1
401                        } else {  // d < 0
402                            (x / (d * -1)) * -1
403                        };
404                        if output < <$iN>::MIN || output > <$iN>::MAX {
405                            None
406                        } else {
407                            Some(output as $iN)
408                        }
409                    }
410                );
411
412            #[verifier::allow_in_spec]
413            pub assume_specification[<$iN>::checked_div_euclid](lhs: $iN, rhs: $iN) -> Option<$iN>
414                returns (
415                    if rhs == 0 {
416                        None
417                    }
418                    else if <$iN>::MIN <= lhs / rhs <= <$iN>::MAX {
419                        Some((lhs / rhs) as $iN)
420                    }
421                    else {
422                        None
423                    }
424                );
425
426            #[verifier::allow_in_spec]
427            pub assume_specification[<$iN>::checked_rem](lhs: $iN, rhs: $iN) -> Option<$iN>
428                returns (
429                    if rhs == 0 {
430                        None
431                    }
432                    else {
433                        let x = lhs as int;
434                        let d = rhs as int;
435                        let output = if x == 0 {
436                            0
437                        } else if x > 0 && d > 0 {
438                            x % d
439                        } else if x < 0 && d < 0 {
440                            ((x * -1) % (d * -1)) * -1
441                        } else if x < 0 {
442                            ((x * -1) % d) * -1
443                        } else {  // d < 0
444                            x % (d * -1)
445                        };
446                        if output < <$iN>::MIN || output > <$iN>::MAX {
447                            None
448                        } else {
449                            Some(output as $iN)
450                        }
451                    }
452                );
453
454            #[verifier::allow_in_spec]
455            pub assume_specification[<$iN>::checked_rem_euclid](lhs: $iN, rhs: $iN) -> Option<$iN>
456                returns (
457                    if rhs == 0 {
458                        None
459                    }
460                    else if <$iN>::MIN <= lhs % rhs <= <$iN>::MAX {
461                        Some((lhs % rhs) as $iN)
462                    }
463                    else {
464                        None
465                    }
466                );
467        }
468
469        }
470    };
471}
472
473num_specs!(u8, i8, u8_specs, i8_specs, 0x100);
474num_specs!(u16, i16, u16_specs, i16_specs, 0x1_0000);
475num_specs!(u32, i32, u32_specs, i32_specs, 0x1_0000_0000);
476num_specs!(u64, i64, u64_specs, i64_specs, 0x1_0000_0000_0000_0000);
477num_specs!(u128, i128, u128_specs, i128_specs, 0x1_0000_0000_0000_0000_0000_0000_0000_0000);
478num_specs!(usize, isize, usize_specs, isize_specs, (usize::MAX - usize::MIN + 1));
vstd/std_specs/num.rs

vstd/std_specs/
num.rs
