improv_verified/
bits.rs

1//! The 48-bit operations of `BITAND`, `BITOR`, `BITXOR`, `BITLSHIFT` and
2//! `BITRSHIFT`. Operands are below 2⁴⁸ (the engine checks that) and shifts
3//! are at most 53 places.
4
5#[allow(unused_imports)]
6use vstd::arithmetic::power2::*;
7#[allow(unused_imports)]
8use vstd::bits::*;
9#[allow(unused_imports)]
10use vstd::prelude::*;
11
12verus! {
13
14/// 2⁴⁸, the bit functions' exclusive operand bound.
15pub const LIMIT: u64 = 0x1_0000_0000_0000;
16
17/// `a & b`: below 2⁴⁸ and at most either operand.
18pub fn and(a: u64, b: u64) -> (r: u64)
19    requires
20        a < LIMIT,
21        b < LIMIT,
22    ensures
23        r == a & b,
24        r < LIMIT,
25        r <= a,
26        r <= b,
27{
28    assert(a & b <= a && a & b <= b) by (bit_vector);
29    a & b
30}
31
32/// `a | b`: below 2⁴⁸ and at least either operand.
33pub fn or(a: u64, b: u64) -> (r: u64)
34    requires
35        a < LIMIT,
36        b < LIMIT,
37    ensures
38        r == a | b,
39        r < LIMIT,
40        r >= a,
41        r >= b,
42{
43    assert(a | b < 0x1_0000_0000_0000 && a | b >= a && a | b >= b) by (bit_vector)
44        requires
45            a < 0x1_0000_0000_0000,
46            b < 0x1_0000_0000_0000,
47    ;
48    a | b
49}
50
51/// `a ^ b`: below 2⁴⁸.
52pub fn xor(a: u64, b: u64) -> (r: u64)
53    requires
54        a < LIMIT,
55        b < LIMIT,
56    ensures
57        r == a ^ b,
58        r < LIMIT,
59{
60    assert(a ^ b < 0x1_0000_0000_0000) by (bit_vector)
61        requires
62            a < 0x1_0000_0000_0000,
63            b < 0x1_0000_0000_0000,
64    ;
65    a ^ b
66}
67
68/// `x · 2ⁿ`, exactly: below 2¹⁰¹, so it never overflows the `u128`.
69pub fn shl(x: u64, n: u32) -> (r: u128)
70    requires
71        x < LIMIT,
72        n <= 53,
73    ensures
74        r == x * pow2(n as nat),
75        r < 0x20_0000_0000_0000_0000_0000_0000,
76{
77    proof {
78        lemma2_to64_rest();
79        if n < 53 {
80            lemma_pow2_strictly_increases(n as nat, 53);
81        }
82        let p = pow2(n as nat);
83        assert(x * p < 0x20_0000_0000_0000_0000_0000_0000) by (nonlinear_arith)
84            requires
85                x < 0x1_0000_0000_0000,
86                p <= 0x20_0000_0000_0000,
87        ;
88        lemma_u64_pow2_no_overflow(n as nat);
89        lemma_u64_shl_is_mul(1, n as u64);
90    }
91    let p = 1u64 << (n as u64);
92    (x as u128) * (p as u128)
93}
94
95/// `x / 2ⁿ` (rounded down): at most `x`.
96pub fn shr(x: u64, n: u32) -> (r: u64)
97    requires
98        n <= 53,
99    ensures
100        r as nat == x as nat / pow2(n as nat),
101        r <= x,
102{
103    proof {
104        lemma_u64_shr_is_div(x, n as u64);
105    }
106    let s = n as u64;
107    assert(x >> s <= x) by (bit_vector);
108    x >> s
109}
110
111} // verus!
112
113#[cfg(test)]
114#[cfg_attr(coverage_nightly, coverage(off))]
115mod tests {
116    use super::*;
117
118    #[test]
119    fn bit_ops() {
120        assert_eq!(and(0b1100, 0b1010), 0b1000);
121        assert_eq!(or(0b1100, 0b1010), 0b1110);
122        assert_eq!(xor(0b1100, 0b1010), 0b0110);
123        assert_eq!(shl(LIMIT - 1, 53), u128::from(LIMIT - 1) << 53);
124        assert_eq!(shr(LIMIT - 1, 47), 1);
125        assert_eq!(shr(5, 53), 0);
126    }
127}
improv_verified/bits.rs

improv_verified/
bits.rs
