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>::checked_add](x: $uN, y: $uN) -> Option<$uN>
102                returns (
103                    if x + y > <$uN>::MAX {
104                        None
105                    } else {
106                        Some((x + y) as $uN)
107                    }
108                );
109
110            #[verifier::allow_in_spec]
111            #[cfg(not(verus_verify_core))]
112            pub assume_specification[<$uN>::checked_add_signed](x: $uN, y: $iN) -> Option<$uN>
113                returns (
114                    if x + y > <$uN>::MAX || x + y < 0 {
115                        None
116                    } else {
117                        Some((x + y) as $uN)
118                    }
119                );
120
121            #[verifier::allow_in_spec]
122            #[cfg(not(verus_verify_core))]
123            pub assume_specification[<$uN>::checked_sub](x: $uN, y: $uN) -> Option<$uN>
124                returns (
125                    if x - y < 0 {
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_mul](x: $uN, y: $uN) -> Option<$uN>
135                returns (
136                    if x * y > <$uN>::MAX {
137                        None
138                    } else {
139                        Some((x * y) as $uN)
140                    }
141                );
142
143            pub open spec fn checked_div(x: $uN, y: $uN) -> Option<$uN> {
144                if y == 0 {
145                    None
146                } else {
147                    Some(x / y)
148                }
149            }
150
151            #[verifier::when_used_as_spec(checked_div)]
152            #[cfg(not(verus_verify_core))]
153            pub assume_specification[<$uN>::checked_div](lhs: $uN, rhs: $uN) -> (result: Option<$uN>)
154                ensures
155                    result == checked_div(lhs, rhs);
156
157            #[verifier::when_used_as_spec(checked_div)]
158            #[cfg(not(verus_verify_core))]
159            pub assume_specification[<$uN>::checked_div_euclid](lhs: $uN, rhs: $uN) -> (result: Option<$uN>)
160                ensures
161                    // checked_div is the same as checked_div_euclid for unsigned ints
162                    result == checked_div(lhs, rhs);
163
164            #[verifier::allow_in_spec]
165            #[cfg(not(verus_verify_core))]
166            pub assume_specification[<$uN>::checked_rem](lhs: $uN, rhs: $uN) -> Option<$uN>
167                returns (
168                    if rhs == 0 {
169                        None
170                    }
171                    else {
172                        Some((lhs % rhs) as $uN)
173                    }
174                );
175
176            #[verifier::allow_in_spec]
177            #[cfg(not(verus_verify_core))]
178            pub assume_specification[<$uN>::checked_rem_euclid](lhs: $uN, rhs: $uN) -> Option<$uN>
179                returns (
180                    if rhs == 0 {
181                        None
182                    }
183                    else {
184                        Some((lhs % rhs) as $uN)
185                    }
186                );
187
188            #[verifier::allow_in_spec]
189            #[cfg(not(verus_verify_core))]
190            pub assume_specification[<$uN>::saturating_add](x: $uN, y: $uN) -> $uN
191                returns (
192                    if x + y > <$uN>::MAX {
193                        <$uN>::MAX
194                    } else {
195                        (x + y) as $uN
196                    }
197                );
198
199            #[verifier::allow_in_spec]
200            #[cfg(not(verus_verify_core))]
201            pub assume_specification[<$uN>::saturating_sub](x: $uN, y: $uN) -> $uN
202                returns (
203                    if x - y < <$uN>::MIN {
204                        <$uN>::MIN
205                    } else {
206                        (x - y) as $uN
207                    }
208                );
209
210            #[verifier::allow_in_spec]
211            #[cfg(not(verus_verify_core))]
212            pub assume_specification[<$uN>::is_multiple_of](x: $uN, y: $uN) -> bool
213                returns (
214                    if y == 0 { x == 0 } else { x % y == 0 }
215                );
216        }
217
218        // Signed ints (i8, i16, etc.)
219
220        mod $mod_i_tmp {
221            use super::*;
222
223            pub assume_specification[<$iN as Clone>::clone](x: &$iN) -> (res: $iN)
224                ensures res == x;
225
226            impl super::super::cmp::PartialEqSpecImpl for $iN {
227                open spec fn obeys_eq_spec() -> bool {
228                    true
229                }
230
231                open spec fn eq_spec(&self, other: &$iN) -> bool {
232                    *self == *other
233                }
234            }
235
236            impl super::super::cmp::PartialOrdSpecImpl for $iN {
237                open spec fn obeys_partial_cmp_spec() -> bool {
238                    true
239                }
240
241                open spec fn partial_cmp_spec(&self, other: &$iN) -> Option<Ordering> {
242                    if *self < *other {
243                        Some(Ordering::Less)
244                    } else if *self > *other {
245                        Some(Ordering::Greater)
246                    } else {
247                        Some(Ordering::Equal)
248                    }
249                }
250            }
251
252            impl super::super::cmp::OrdSpecImpl for $iN {
253                open spec fn obeys_cmp_spec() -> bool {
254                    true
255                }
256
257                open spec fn cmp_spec(&self, other: &$iN) -> Ordering {
258                    if *self < *other {
259                        Ordering::Less
260                    } else if *self > *other {
261                        Ordering::Greater
262                    } else {
263                        Ordering::Equal
264                    }
265                }
266            }
267
268            pub assume_specification[<$iN as PartialEq<$iN>>::eq](x: &$iN, y: &$iN) -> bool;
269
270            pub assume_specification[<$iN as PartialEq<$iN>>::ne](x: &$iN, y: &$iN) -> bool;
271
272            pub assume_specification[<$iN as Ord>::cmp](x: &$iN, y: &$iN) -> Ordering;
273
274            pub assume_specification[<$iN as PartialOrd<$iN>>::partial_cmp](x: &$iN, y: &$iN) -> Option<Ordering>;
275
276            pub assume_specification[<$iN as PartialOrd<$iN>>::lt](x: &$iN, y: &$iN) -> bool;
277
278            pub assume_specification[<$iN as PartialOrd<$iN>>::le](x: &$iN, y: &$iN) -> bool;
279
280            pub assume_specification[<$iN as PartialOrd<$iN>>::gt](x: &$iN, y: &$iN) -> bool;
281
282            pub assume_specification[<$iN as PartialOrd<$iN>>::ge](x: &$iN, y: &$iN) -> bool;
283
284            #[verifier::allow_in_spec]
285            #[cfg(not(verus_verify_core))]
286            pub assume_specification[<$iN>::wrapping_add](x: $iN, y: $iN) -> $iN
287                returns $mod_i::wrapping_add(x, y);
288
289            #[verifier::allow_in_spec]
290            #[cfg(not(verus_verify_core))]
291            pub assume_specification[<$iN>::wrapping_add_unsigned](x: $iN, y: $uN) -> $iN
292                returns $mod_i::wrapping_add_unsigned(x, y);
293
294            #[verifier::allow_in_spec]
295            #[cfg(not(verus_verify_core))]
296            pub assume_specification[<$iN>::wrapping_sub](x: $iN, y: $iN) -> (res: $iN)
297                returns $mod_i::wrapping_sub(x, y);
298
299            #[verifier::allow_in_spec]
300            #[cfg(not(verus_verify_core))]
301            pub assume_specification[<$iN>::wrapping_mul](x: $iN, y: $iN) -> $iN
302                returns $mod_i::wrapping_mul(x, y);
303
304            #[verifier::allow_in_spec]
305            #[cfg(not(verus_verify_core))]
306            pub assume_specification[<$iN>::checked_add](x: $iN, y: $iN) -> Option<$iN>
307                returns (
308                    if x + y > <$iN>::MAX || x + y < <$iN>::MIN {
309                        None
310                    } else {
311                        Some((x + y) as $iN)
312                    }
313                );
314
315            #[verifier::allow_in_spec]
316            #[cfg(not(verus_verify_core))]
317            pub assume_specification[<$iN>::checked_add_unsigned](x: $iN, y: $uN) -> Option<$iN>
318                returns (
319                    if x + y > <$iN>::MAX {
320                        None
321                    } else {
322                        Some((x + y) as $iN)
323                    }
324                );
325
326            #[verifier::allow_in_spec]
327            #[cfg(not(verus_verify_core))]
328            pub assume_specification[<$iN>::checked_sub](x: $iN, y: $iN) -> Option<$iN>
329                returns (
330                    if x - y > <$iN>::MAX || x - y < <$iN>::MIN {
331                        None
332                    } else {
333                        Some((x - y) as $iN)
334                    }
335                );
336
337            #[verifier::allow_in_spec]
338            #[cfg(not(verus_verify_core))]
339            pub assume_specification[<$iN>::checked_sub_unsigned](x: $iN, y: $uN) -> Option<$iN>
340                returns (
341                    if x - y < <$iN>::MIN {
342                        None
343                    } else {
344                        Some((x - y) as $iN)
345                    }
346                );
347
348            #[verifier::allow_in_spec]
349            #[cfg(not(verus_verify_core))]
350            pub assume_specification[<$iN>::checked_mul](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_div](lhs: $iN, rhs: $iN) -> Option<$iN>
362                returns (
363                    if rhs == 0 {
364                        None
365                    }
366                    else {
367                        let x = lhs as int;
368                        let d = rhs as int;
369                        let output = if x == 0 {
370                            0
371                        } else if x > 0 && d > 0 {
372                            x / d
373                        } else if x < 0 && d < 0 {
374                            ((x * -1) / (d * -1))
375                        } else if x < 0 {
376                            ((x * -1) / d) * -1
377                        } else {  // d < 0
378                            (x / (d * -1)) * -1
379                        };
380                        if output < <$iN>::MIN || output > <$iN>::MAX {
381                            None
382                        } else {
383                            Some(output as $iN)
384                        }
385                    }
386                );
387
388            #[verifier::allow_in_spec]
389            #[cfg(not(verus_verify_core))]
390            pub assume_specification[<$iN>::checked_div_euclid](lhs: $iN, rhs: $iN) -> Option<$iN>
391                returns (
392                    if rhs == 0 {
393                        None
394                    }
395                    else if <$iN>::MIN <= lhs / rhs <= <$iN>::MAX {
396                        Some((lhs / rhs) as $iN)
397                    }
398                    else {
399                        None
400                    }
401                );
402
403            #[verifier::allow_in_spec]
404            #[cfg(not(verus_verify_core))]
405            pub assume_specification[<$iN>::checked_rem](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)) * -1
419                        } else if x < 0 {
420                            ((x * -1) % d) * -1
421                        } else {  // d < 0
422                            x % (d * -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_rem_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
448        }
449    };
450}
451
452num_specs!(u8, i8, u8_specs_tmp, i8_specs_tmp, u8_specs, i8_specs, 0x100);
453num_specs!(u16, i16, u16_specs_tmp, i16_specs_tmp, u16_specs, i16_specs, 0x1_0000);
454num_specs!(u32, i32, u32_specs_tmp, i32_specs_tmp, u32_specs, i32_specs, 0x1_0000_0000);
455num_specs!(u64, i64, u64_specs_tmp, i64_specs_tmp, u64_specs, i64_specs, 0x1_0000_0000_0000_0000);
456num_specs!(
457    u128,
458    i128,
459    u128_specs_tmp,
460    i128_specs_tmp,
461    u128_specs,
462    i128_specs,
463    0x1_0000_0000_0000_0000_0000_0000_0000_0000
464);
465num_specs!(
466    usize,
467    isize,
468    usize_specs_tmp,
469    isize_specs_tmp,
470    usize_specs,
471    isize_specs,
472    (usize::MAX - usize::MIN + 1)
473);
vstd/std_specs/num.rs

vstd/std_specs/
num.rs
