vstd/std_specs/
num.rs

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

vstd/std_specs/
num.rs
