vstd_extra/external/
int_specs.rs

1//! Specs for stdlib methods on integer types that aren't covered by vstd.
2use vstd::arithmetic::power2::is_pow2;
3use vstd::prelude::*;
4
5verus! {
6
7/// Spec for `<int_type>::is_power_of_two`. Returns true iff `self` is a positive
8/// power of two, i.e., there exists `e: nat` with `pow2(e) == self`.
9pub assume_specification[ u8::is_power_of_two ](self_: u8) -> (r: bool)
10    returns
11        is_pow2(self_ as int),
12    opens_invariants none
13    no_unwind
14;
15
16pub assume_specification[ u16::is_power_of_two ](self_: u16) -> (r: bool)
17    returns
18        is_pow2(self_ as int),
19    opens_invariants none
20    no_unwind
21;
22
23pub assume_specification[ u32::is_power_of_two ](self_: u32) -> (r: bool)
24    returns
25        is_pow2(self_ as int),
26    opens_invariants none
27    no_unwind
28;
29
30pub assume_specification[ u64::is_power_of_two ](self_: u64) -> (r: bool)
31    returns
32        is_pow2(self_ as int),
33    opens_invariants none
34    no_unwind
35;
36
37pub assume_specification[ usize::is_power_of_two ](self_: usize) -> (r: bool)
38    returns
39        is_pow2(self_ as int),
40    opens_invariants none
41    no_unwind
42;
43
44} // verus!
vstd_extra/external/int_specs.rs

vstd_extra/external/
int_specs.rs
