vstd/std_specs/
num.rs

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

vstd/std_specs/
num.rs
