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
84            #[verifier::allow_in_spec]
85            #[cfg(not(verus_verify_core))]
86            pub assume_specification[<$uN>::wrapping_add_signed](x: $uN, y: $iN) -> $uN
87                returns $mod_u::wrapping_add_signed(x, y);
88
89            #[verifier::allow_in_spec]
90            #[cfg(not(verus_verify_core))]
91            pub assume_specification[<$uN>::wrapping_sub](x: $uN, y: $uN) -> $uN
92                returns $mod_u::wrapping_sub(x, y);
93
94            #[verifier::allow_in_spec]
95            #[cfg(not(verus_verify_core))]
96            pub assume_specification[<$uN>::wrapping_mul](x: $uN, y: $uN) -> $uN
97                returns $mod_u::wrapping_mul(x, y);
98
99            #[verifier::allow_in_spec]
100            #[cfg(not(verus_verify_core))]
101            pub assume_specification[<$uN>::wrapping_shl](x: $uN, rhs: u32) -> $uN
102                returns $mod_u::wrapping_shl(x, rhs);
103
104            #[verifier::allow_in_spec]
105            #[cfg(not(verus_verify_core))]
106            pub assume_specification[<$uN>::wrapping_shr](x: $uN, rhs: u32) -> $uN
107                returns $mod_u::wrapping_shr(x, rhs);
108
109            #[verifier::allow_in_spec]
110            #[cfg(not(verus_verify_core))]
111            pub assume_specification[<$uN>::checked_add](x: $uN, y: $uN) -> Option<$uN>
112                returns (
113                    if x + y > <$uN>::MAX {
114                        None
115                    } else {
116                        Some((x + y) as $uN)
117                    }
118                );
119
120            #[verifier::allow_in_spec]
121            #[cfg(not(verus_verify_core))]
122            pub assume_specification[<$uN>::checked_add_signed](x: $uN, y: $iN) -> Option<$uN>
123                returns (
124                    if x + y > <$uN>::MAX || x + y < 0 {
125                        None
126                    } else {
127                        Some((x + y) as $uN)
128                    }
129                );
130
131            #[verifier::allow_in_spec]
132            #[cfg(not(verus_verify_core))]
133            pub assume_specification[<$uN>::checked_sub](x: $uN, y: $uN) -> Option<$uN>
134                returns (
135                    if x - y < 0 {
136                        None
137                    } else {
138                        Some((x - y) as $uN)
139                    }
140                );
141
142            #[verifier::allow_in_spec]
143            #[cfg(not(verus_verify_core))]
144            pub assume_specification[<$uN>::checked_mul](x: $uN, y: $uN) -> Option<$uN>
145                returns (
146                    if x * y > <$uN>::MAX {
147                        None
148                    } else {
149                        Some((x * y) as $uN)
150                    }
151                );
152
153            pub open spec fn checked_div(x: $uN, y: $uN) -> Option<$uN> {
154                if y == 0 {
155                    None
156                } else {
157                    Some(x / y)
158                }
159            }
160
161            #[verifier::when_used_as_spec(checked_div)]
162            #[cfg(not(verus_verify_core))]
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            #[cfg(not(verus_verify_core))]
169            pub assume_specification[<$uN>::checked_div_euclid](lhs: $uN, rhs: $uN) -> (result: Option<$uN>)
170                ensures
171                    // checked_div is the same as checked_div_euclid for unsigned ints
172                    result == checked_div(lhs, rhs);
173
174            #[verifier::allow_in_spec]
175            #[cfg(not(verus_verify_core))]
176            pub assume_specification[<$uN>::checked_rem](lhs: $uN, rhs: $uN) -> Option<$uN>
177                returns (
178                    if rhs == 0 {
179                        None
180                    }
181                    else {
182                        Some((lhs % rhs) as $uN)
183                    }
184                );
185
186            #[verifier::allow_in_spec]
187            #[cfg(not(verus_verify_core))]
188            pub assume_specification[<$uN>::checked_rem_euclid](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>::saturating_add](x: $uN, y: $uN) -> $uN
201                returns (
202                    if x + y > <$uN>::MAX {
203                        <$uN>::MAX
204                    } else {
205                        (x + y) as $uN
206                    }
207                );
208
209            #[verifier::allow_in_spec]
210            #[cfg(not(verus_verify_core))]
211            pub assume_specification[<$uN>::saturating_sub](x: $uN, y: $uN) -> $uN
212                returns (
213                    if x - y < <$uN>::MIN {
214                        <$uN>::MIN
215                    } else {
216                        (x - y) as $uN
217                    }
218                );
219
220            #[verifier::allow_in_spec]
221            #[cfg(not(verus_verify_core))]
222            pub assume_specification[<$uN>::is_multiple_of](x: $uN, y: $uN) -> bool
223                returns (
224                    if y == 0 { x == 0 } else { x % y == 0 }
225                );
226        }
227
228        // Signed ints (i8, i16, etc.)
229
230        mod $mod_i_tmp {
231            use super::*;
232
233            pub assume_specification[<$iN as Clone>::clone](x: &$iN) -> (res: $iN)
234                ensures res == x;
235
236            impl super::super::cmp::PartialEqSpecImpl for $iN {
237                open spec fn obeys_eq_spec() -> bool {
238                    true
239                }
240
241                open spec fn eq_spec(&self, other: &$iN) -> bool {
242                    *self == *other
243                }
244            }
245
246            impl super::super::cmp::PartialOrdSpecImpl for $iN {
247                open spec fn obeys_partial_cmp_spec() -> bool {
248                    true
249                }
250
251                open spec fn partial_cmp_spec(&self, other: &$iN) -> Option<Ordering> {
252                    if *self < *other {
253                        Some(Ordering::Less)
254                    } else if *self > *other {
255                        Some(Ordering::Greater)
256                    } else {
257                        Some(Ordering::Equal)
258                    }
259                }
260            }
261
262            impl super::super::cmp::OrdSpecImpl for $iN {
263                open spec fn obeys_cmp_spec() -> bool {
264                    true
265                }
266
267                open spec fn cmp_spec(&self, other: &$iN) -> Ordering {
268                    if *self < *other {
269                        Ordering::Less
270                    } else if *self > *other {
271                        Ordering::Greater
272                    } else {
273                        Ordering::Equal
274                    }
275                }
276            }
277
278            pub assume_specification[<$iN as PartialEq<$iN>>::eq](x: &$iN, y: &$iN) -> bool;
279
280            pub assume_specification[<$iN as PartialEq<$iN>>::ne](x: &$iN, y: &$iN) -> bool;
281
282            pub assume_specification[<$iN as Ord>::cmp](x: &$iN, y: &$iN) -> Ordering;
283
284            pub assume_specification[<$iN as PartialOrd<$iN>>::partial_cmp](x: &$iN, y: &$iN) -> Option<Ordering>;
285
286            pub assume_specification[<$iN as PartialOrd<$iN>>::lt](x: &$iN, y: &$iN) -> bool;
287
288            pub assume_specification[<$iN as PartialOrd<$iN>>::le](x: &$iN, y: &$iN) -> bool;
289
290            pub assume_specification[<$iN as PartialOrd<$iN>>::gt](x: &$iN, y: &$iN) -> bool;
291
292            pub assume_specification[<$iN as PartialOrd<$iN>>::ge](x: &$iN, y: &$iN) -> bool;
293
294            #[verifier::allow_in_spec]
295            #[cfg(not(verus_verify_core))]
296            pub assume_specification[<$iN>::wrapping_add](x: $iN, y: $iN) -> $iN
297                returns $mod_i::wrapping_add(x, y);
298
299            #[verifier::allow_in_spec]
300            #[cfg(not(verus_verify_core))]
301            pub assume_specification[<$iN>::wrapping_add_unsigned](x: $iN, y: $uN) -> $iN
302                returns $mod_i::wrapping_add_unsigned(x, y);
303
304            #[verifier::allow_in_spec]
305            #[cfg(not(verus_verify_core))]
306            pub assume_specification[<$iN>::wrapping_sub](x: $iN, y: $iN) -> (res: $iN)
307                returns $mod_i::wrapping_sub(x, y);
308
309            #[verifier::allow_in_spec]
310            #[cfg(not(verus_verify_core))]
311            pub assume_specification[<$iN>::wrapping_mul](x: $iN, y: $iN) -> $iN
312                returns $mod_i::wrapping_mul(x, y);
313
314            #[verifier::allow_in_spec]
315            #[cfg(not(verus_verify_core))]
316            pub assume_specification[<$iN>::wrapping_shl](x: $iN, rhs: u32) -> $iN
317                returns $mod_i::wrapping_shl(x, rhs);
318
319            #[verifier::allow_in_spec]
320            #[cfg(not(verus_verify_core))]
321            pub assume_specification[<$iN>::wrapping_shr](x: $iN, rhs: u32) -> $iN
322                returns $mod_i::wrapping_shr(x, rhs);
323
324            #[verifier::allow_in_spec]
325            #[cfg(not(verus_verify_core))]
326            pub assume_specification[<$iN>::checked_add](x: $iN, y: $iN) -> Option<$iN>
327                returns (
328                    if x + y > <$iN>::MAX || x + y < <$iN>::MIN {
329                        None
330                    } else {
331                        Some((x + y) as $iN)
332                    }
333                );
334
335            #[verifier::allow_in_spec]
336            #[cfg(not(verus_verify_core))]
337            pub assume_specification[<$iN>::checked_add_unsigned](x: $iN, y: $uN) -> Option<$iN>
338                returns (
339                    if x + y > <$iN>::MAX {
340                        None
341                    } else {
342                        Some((x + y) as $iN)
343                    }
344                );
345
346            #[verifier::allow_in_spec]
347            #[cfg(not(verus_verify_core))]
348            pub assume_specification[<$iN>::checked_sub](x: $iN, y: $iN) -> Option<$iN>
349                returns (
350                    if x - y > <$iN>::MAX || x - y < <$iN>::MIN {
351                        None
352                    } else {
353                        Some((x - y) as $iN)
354                    }
355                );
356
357            #[verifier::allow_in_spec]
358            #[cfg(not(verus_verify_core))]
359            pub assume_specification[<$iN>::checked_sub_unsigned](x: $iN, y: $uN) -> Option<$iN>
360                returns (
361                    if x - y < <$iN>::MIN {
362                        None
363                    } else {
364                        Some((x - y) as $iN)
365                    }
366                );
367
368            #[verifier::allow_in_spec]
369            #[cfg(not(verus_verify_core))]
370            pub assume_specification[<$iN>::checked_mul](x: $iN, y: $iN) -> Option<$iN>
371                returns (
372                    if x * y > <$iN>::MAX || x * y < <$iN>::MIN {
373                        None
374                    } else {
375                        Some((x * y) as $iN)
376                    }
377                );
378
379            #[verifier::allow_in_spec]
380            #[cfg(not(verus_verify_core))]
381            pub assume_specification[<$iN>::checked_div](lhs: $iN, rhs: $iN) -> Option<$iN>
382                returns (
383                    if rhs == 0 {
384                        None
385                    }
386                    else {
387                        let x = lhs as int;
388                        let d = rhs as int;
389                        let output = if x == 0 {
390                            0
391                        } else if x > 0 && d > 0 {
392                            x / d
393                        } else if x < 0 && d < 0 {
394                            ((x * -1) / (d * -1))
395                        } else if x < 0 {
396                            ((x * -1) / d) * -1
397                        } else {  // d < 0
398                            (x / (d * -1)) * -1
399                        };
400                        if output < <$iN>::MIN || output > <$iN>::MAX {
401                            None
402                        } else {
403                            Some(output as $iN)
404                        }
405                    }
406                );
407
408            #[verifier::allow_in_spec]
409            #[cfg(not(verus_verify_core))]
410            pub assume_specification[<$iN>::checked_div_euclid](lhs: $iN, rhs: $iN) -> Option<$iN>
411                returns (
412                    if rhs == 0 {
413                        None
414                    }
415                    else if <$iN>::MIN <= lhs / rhs <= <$iN>::MAX {
416                        Some((lhs / rhs) as $iN)
417                    }
418                    else {
419                        None
420                    }
421                );
422
423            #[verifier::allow_in_spec]
424            #[cfg(not(verus_verify_core))]
425            pub assume_specification[<$iN>::checked_rem](lhs: $iN, rhs: $iN) -> Option<$iN>
426                returns (
427                    if rhs == 0 {
428                        None
429                    }
430                    else {
431                        let x = lhs as int;
432                        let d = rhs as int;
433                        let output = if x == 0 {
434                            0
435                        } else if x > 0 && d > 0 {
436                            x % d
437                        } else if x < 0 && d < 0 {
438                            ((x * -1) % (d * -1)) * -1
439                        } else if x < 0 {
440                            ((x * -1) % d) * -1
441                        } else {  // d < 0
442                            x % (d * -1)
443                        };
444                        if output < <$iN>::MIN || output > <$iN>::MAX {
445                            None
446                        } else {
447                            Some(output as $iN)
448                        }
449                    }
450                );
451
452            #[verifier::allow_in_spec]
453            #[cfg(not(verus_verify_core))]
454            pub assume_specification[<$iN>::checked_rem_euclid](lhs: $iN, rhs: $iN) -> Option<$iN>
455                returns (
456                    if rhs == 0 {
457                        None
458                    }
459                    else if <$iN>::MIN <= lhs % rhs <= <$iN>::MAX {
460                        Some((lhs % rhs) as $iN)
461                    }
462                    else {
463                        None
464                    }
465                );
466        }
467
468        }
469    };
470}
471
472num_specs!(u8, i8, u8_specs_tmp, i8_specs_tmp, u8_specs, i8_specs, 0x100);
473num_specs!(u16, i16, u16_specs_tmp, i16_specs_tmp, u16_specs, i16_specs, 0x1_0000);
474num_specs!(u32, i32, u32_specs_tmp, i32_specs_tmp, u32_specs, i32_specs, 0x1_0000_0000);
475num_specs!(u64, i64, u64_specs_tmp, i64_specs_tmp, u64_specs, i64_specs, 0x1_0000_0000_0000_0000);
476num_specs!(
477    u128,
478    i128,
479    u128_specs_tmp,
480    i128_specs_tmp,
481    u128_specs,
482    i128_specs,
483    0x1_0000_0000_0000_0000_0000_0000_0000_0000
484);
485num_specs!(
486    usize,
487    isize,
488    usize_specs_tmp,
489    isize_specs_tmp,
490    usize_specs,
491    isize_specs,
492    (usize::MAX - usize::MIN + 1)
493);
vstd/std_specs/num.rs

vstd/std_specs/
num.rs
