vstd_extra/external/
bits.rs

1//! Specifications for bit-related standard-library functions.
2use crate::bits::u64_bit_is_set;
3use vstd::prelude::*;
4
5verus! {
6
7/// The number of set bits among the lowest `n` bits of `w`.
8spec fn u64_set_bits_rec(w: u64, n: u64) -> int
9    decreases n,
10{
11    if n == 0 {
12        0
13    } else {
14        (if u64_bit_is_set(w, n - 1) {
15            1int
16        } else {
17            0int
18        }) + u64_set_bits_rec(w, (n - 1) as u64)
19    }
20}
21
22/// The number of set bits in a `u64` word.
23pub closed spec fn u64_set_bits(w: u64) -> int {
24    u64_set_bits_rec(w, 64)
25}
26
27/// `u64::count_ones`: "Returns the number of ones in the binary representation
28/// of `self`" (core/src/num/uint_macros.rs, `intrinsics::ctpop`).
29pub assume_specification[ u64::count_ones ](v: u64) -> (r: u32)
30    ensures
31        r == u64_set_bits(v),
32;
33
34/// A nonzero word has at least one set bit (and zero has none).
35pub broadcast proof fn lemma_u64_set_bits_nonzero(w: u64)
36    ensures
37        #![trigger u64_set_bits(w)]
38        (w != 0u64) == (1 <= u64_set_bits(w)),
39        0 <= u64_set_bits(w) <= 64,
40{
41    reveal(u64_set_bits);
42    lemma_u64_set_bits_rec_bounds(w, 64);
43    assert(w >> 64u64 == 0) by (bit_vector);
44}
45
46proof fn lemma_u64_set_bits_rec_bounds(w: u64, n: u64)
47    requires
48        n <= 64,
49    ensures
50        0 <= u64_set_bits_rec(w, n) <= n,
51        w >> n == 0 ==> ((w != 0) == (1 <= u64_set_bits_rec(w, n))),
52    decreases n,
53{
54    reveal_with_fuel(u64_set_bits_rec, 1);
55    if n != 0 {
56        let prev = (n - 1) as u64;
57        lemma_u64_set_bits_rec_bounds(w, prev);
58        if w >> n == 0 {
59            if w == 0 {
60                assert(u64_bit_is_set(w, prev as int) == false) by {
61                    assert((w & (1u64 << (prev as usize))) == 0u64) by (bit_vector)
62                        requires
63                            w == 0,
64                    ;
65                }
66                assert(w >> prev == 0) by (bit_vector)
67                    requires
68                        w == 0,
69                ;
70            } else {
71                if u64_bit_is_set(w, prev as int) {
72                    assert(1 <= u64_bit_is_set(w, prev as int) as int);
73                } else {
74                    assert((w & (1u64 << (prev as usize))) == 0u64);
75                    assert(w >> prev == 0) by (bit_vector)
76                        requires
77                            0 < n <= 64,
78                            prev == n - 1,
79                            w >> n == 0,
80                            (w & (1u64 << (prev as usize))) == 0u64,
81                    ;
82                }
83            }
84        }
85    } else {
86        assert(w >> n == w) by (bit_vector)
87            requires
88                n == 0,
89        ;
90    }
91}
92
93} // verus!
vstd_extra/external/bits.rs

vstd_extra/external/
bits.rs
