vstd/
bits.rs

1//! Properties of bitwise operators.
2use super::prelude::*;
3
4verus! {
5
6#[cfg(verus_keep_ghost)]
7use super::arithmetic::power::pow;
8#[cfg(verus_keep_ghost)]
9use super::arithmetic::power2::{
10    pow2,
11    lemma_pow2_unfold,
12    lemma_pow2_adds,
13    lemma_pow2_pos,
14    lemma2_to64,
15    lemma2_to64_rest,
16    lemma_pow2_strictly_increases,
17};
18#[cfg(verus_keep_ghost)]
19use super::arithmetic::div_mod::{
20    lemma_div_by_multiple,
21    lemma_div_denominator,
22    lemma_div_is_ordered,
23    lemma_mod_breakdown,
24    lemma_mod_multiples_vanish,
25    lemma_remainder_lower,
26};
27#[cfg(verus_keep_ghost)]
28use super::arithmetic::mul::{
29    lemma_mul_inequality,
30    lemma_mul_is_commutative,
31    lemma_mul_is_associative,
32};
33#[cfg(verus_keep_ghost)]
34use super::calc_macro::*;
35
36} // verus!
37// Proofs that shift right is equivalent to division by power of 2.
38macro_rules! lemma_shr_is_div {
39    ($name:ident, $uN:ty) => {
40        #[cfg(verus_keep_ghost)]
41        verus! {
42        #[doc = "Proof that for x and n of type "]
43        #[doc = stringify!($uN)]
44        #[doc = ", shifting x right by n is equivalent to division of x by 2^n."]
45        pub broadcast proof fn $name(x: $uN, shift: $uN)
46            requires
47                0 <= shift < <$uN>::BITS,
48            ensures
49                #[trigger] (x >> shift) == x as nat / pow2(shift as nat),
50            decreases shift,
51        {
52            reveal(pow2);
53            if shift == 0 {
54                assert(x >> 0 == x) by (bit_vector);
55                reveal(pow);
56                assert(pow2(0) == 1) by (compute_only);
57            } else {
58                assert(x >> shift == (x >> ((sub(shift, 1)) as $uN)) / 2) by (bit_vector)
59                    requires
60                        0 < shift < <$uN>::BITS,
61                ;
62                calc!{ (==)
63                    (x >> shift) as nat;
64                        {}
65                    ((x >> ((sub(shift, 1)) as $uN)) / 2) as nat;
66                        { $name(x, (shift - 1) as $uN); }
67                    (x as nat / pow2((shift - 1) as nat)) / 2;
68                        {
69                            lemma_pow2_pos((shift - 1) as nat);
70                            lemma2_to64();
71                            lemma_div_denominator(x as int, pow2((shift - 1) as nat) as int, 2);
72                        }
73                    x as nat / (pow2((shift - 1) as nat) * pow2(1));
74                        {
75                            lemma_pow2_adds((shift - 1) as nat, 1);
76                        }
77                    x as nat / pow2(shift as nat);
78                }
79            }
80        }
81        }
82    };
83}
84
85lemma_shr_is_div!(lemma_u128_shr_is_div, u128);
86lemma_shr_is_div!(lemma_u64_shr_is_div, u64);
87lemma_shr_is_div!(lemma_u32_shr_is_div, u32);
88lemma_shr_is_div!(lemma_u16_shr_is_div, u16);
89lemma_shr_is_div!(lemma_u8_shr_is_div, u8);
90
91// Proofs of when a power of 2 fits in an unsigned type.
92macro_rules! lemma_pow2_no_overflow {
93    ($name:ident, $uN:ty) => {
94        #[cfg(verus_keep_ghost)]
95        verus! {
96        #[doc = "Proof that 2^n does not overflow "]
97        #[doc = stringify!($uN)]
98        #[doc = " for an exponent n."]
99        pub broadcast proof fn $name(n: nat)
100            requires
101                0 <= n < <$uN>::BITS,
102            ensures
103                0 < #[trigger] pow2(n) < <$uN>::MAX,
104        {
105            lemma_pow2_pos(n);
106            lemma2_to64();
107            lemma2_to64_rest();
108        }
109        }
110    };
111}
112
113lemma_pow2_no_overflow!(lemma_u64_pow2_no_overflow, u64);
114lemma_pow2_no_overflow!(lemma_u32_pow2_no_overflow, u32);
115lemma_pow2_no_overflow!(lemma_u16_pow2_no_overflow, u16);
116lemma_pow2_no_overflow!(lemma_u8_pow2_no_overflow, u8);
117
118// Proofs that shift left is equivalent to multiplication by power of 2.
119macro_rules! lemma_shl_is_mul {
120    ($name:ident, $no_overflow:ident, $uN:ty) => {
121        #[cfg(verus_keep_ghost)]
122        verus! {
123        #[doc = "Proof that for x and n of type "]
124        #[doc = stringify!($uN)]
125        #[doc = ", shifting x left by n is equivalent to multiplication of x by 2^n (provided no overflow)."]
126        pub broadcast proof fn $name(x: $uN, shift: $uN)
127            requires
128                0 <= shift < <$uN>::BITS,
129                x * pow2(shift as nat) <= <$uN>::MAX,
130            ensures
131                #[trigger] (x << shift) == x * pow2(shift as nat),
132            decreases shift,
133        {
134            $no_overflow(shift as nat);
135            if shift == 0 {
136                assert(x << 0 == x) by (bit_vector);
137                assert(pow2(0) == 1) by (compute_only);
138            } else {
139                assert(x << shift == mul(x << ((sub(shift, 1)) as $uN), 2)) by (bit_vector)
140                    requires
141                        0 < shift < <$uN>::BITS,
142                ;
143                assert((x << (sub(shift, 1) as $uN)) == x * pow2(sub(shift, 1) as nat)) by {
144                    lemma_pow2_strictly_increases((shift - 1) as nat, shift as nat);
145                    lemma_mul_inequality(
146                        pow2((shift - 1) as nat) as int,
147                        pow2(shift as nat) as int,
148                        x as int,
149                    );
150                    lemma_mul_is_commutative(x as int, pow2((shift - 1) as nat) as int);
151                    lemma_mul_is_commutative(x as int, pow2(shift as nat) as int);
152                    $name(x, (shift - 1) as $uN);
153                }
154                calc!{ (==)
155                    ((x << (sub(shift, 1) as $uN)) * 2);
156                        {}
157                    ((x * pow2(sub(shift, 1) as nat)) * 2);
158                        {
159                            lemma_mul_is_associative(x as int, pow2(sub(shift, 1) as nat) as int, 2);
160                        }
161                    x * ((pow2(sub(shift, 1) as nat)) * 2);
162                        {
163                            lemma_pow2_adds((shift - 1) as nat, 1);
164                            lemma2_to64();
165                        }
166                    x * pow2(shift as nat);
167                }
168            }
169        }
170        }
171    };
172}
173
174lemma_shl_is_mul!(lemma_u64_shl_is_mul, lemma_u64_pow2_no_overflow, u64);
175lemma_shl_is_mul!(lemma_u32_shl_is_mul, lemma_u32_pow2_no_overflow, u32);
176lemma_shl_is_mul!(lemma_u16_shl_is_mul, lemma_u16_pow2_no_overflow, u16);
177lemma_shl_is_mul!(lemma_u8_shl_is_mul, lemma_u8_pow2_no_overflow, u8);
178
179macro_rules! lemma_mul_pow2_le_max_iff_max_shr {
180    ($name:ident, $shr_is_div:ident, $uN:ty) => {
181        #[cfg(verus_keep_ghost)]
182        verus! {
183        #[doc = "Proof that for x, n and max of type "]
184        #[doc = stringify!($uN)]
185        #[doc = ", multiplication of x by 2^n is less than or equal to max if and only if x is less than or equal to shifting max right by n."]
186        pub proof fn $name(x: $uN, shift: $uN, max: $uN)
187        requires
188            0 <= shift < <$uN>::BITS,
189        ensures
190            x * pow2(shift as nat) <= max <==> x <= (max >> shift),
191    {
192        assert(max >> shift == max as nat / pow2(shift as nat)) by {
193            $shr_is_div(max, shift as $uN);
194        };
195
196        lemma_pow2_pos(shift as nat);
197
198        if x * pow2(shift as nat) <= max {
199            assert(x <= (max as nat) / pow2(shift as nat)) by {
200                lemma_div_is_ordered(x as int * pow2(shift as nat) as int, max as int, pow2(shift as nat) as int);
201                lemma_div_by_multiple(x as int, pow2(shift as nat) as int);
202            };
203        }
204        if x <= (max >> shift) {
205            assert(x * pow2(shift as nat) <= max as nat) by {
206                lemma_mul_inequality(x as int, max as int / pow2(shift as nat) as int,  pow2(shift as nat) as int);
207                lemma_remainder_lower(max as int, pow2(shift as nat) as int);
208                lemma_mul_is_commutative(max as int / pow2(shift as nat) as int,  pow2(shift as nat) as int);
209            };
210        }
211    }
212    }
213    };
214}
215
216lemma_mul_pow2_le_max_iff_max_shr!(
217    lemma_u64_mul_pow2_le_max_iff_max_shr,
218    lemma_u64_shr_is_div,
219    u64
220);
221lemma_mul_pow2_le_max_iff_max_shr!(
222    lemma_u32_mul_pow2_le_max_iff_max_shr,
223    lemma_u32_shr_is_div,
224    u32
225);
226lemma_mul_pow2_le_max_iff_max_shr!(
227    lemma_u16_mul_pow2_le_max_iff_max_shr,
228    lemma_u16_shr_is_div,
229    u16
230);
231lemma_mul_pow2_le_max_iff_max_shr!(lemma_u8_mul_pow2_le_max_iff_max_shr, lemma_u8_shr_is_div, u8);
232
233verus! {
234
235/// Mask with low n bits set.
236pub open spec fn low_bits_mask(n: nat) -> nat {
237    (pow2(n) - 1) as nat
238}
239
240/// Proof relating the n-bit mask to a function of the (n-1)-bit mask.
241pub broadcast proof fn lemma_low_bits_mask_unfold(n: nat)
242    requires
243        n > 0,
244    ensures
245        #[trigger] low_bits_mask(n) == 2 * low_bits_mask((n - 1) as nat) + 1,
246{
247    calc! {
248        (==)
249        low_bits_mask(n); {}
250        (pow2(n) - 1) as nat; {
251            lemma_pow2_unfold(n);
252        }
253        (2 * pow2((n - 1) as nat) - 1) as nat; {}
254        (2 * (pow2((n - 1) as nat) - 1) + 1) as nat; {
255            lemma_pow2_pos((n - 1) as nat);
256        }
257        (2 * low_bits_mask((n - 1) as nat) + 1) as nat;
258    }
259}
260
261/// Proof that low_bits_mask(n) is odd.
262pub broadcast proof fn lemma_low_bits_mask_is_odd(n: nat)
263    requires
264        n > 0,
265    ensures
266        #[trigger] (low_bits_mask(n) % 2) == 1,
267{
268    calc! {
269        (==)
270        low_bits_mask(n) % 2; {
271            lemma_low_bits_mask_unfold(n);
272        }
273        (2 * low_bits_mask((n - 1) as nat) + 1) % 2; {
274            lemma_mod_multiples_vanish(low_bits_mask((n - 1) as nat) as int, 1, 2);
275        }
276        1nat % 2;
277    }
278}
279
280/// Proof that dividing the low n bit mask by 2 gives the low n-1 bit mask.
281pub broadcast proof fn lemma_low_bits_mask_div2(n: nat)
282    requires
283        n > 0,
284    ensures
285        #[trigger] (low_bits_mask(n) / 2) == low_bits_mask((n - 1) as nat),
286{
287    lemma_low_bits_mask_unfold(n);
288}
289
290/// Proof establishing the concrete values of all masks of bit sizes from 0 to
291/// 32, and 64.
292pub proof fn lemma_low_bits_mask_values()
293    ensures
294        low_bits_mask(0) == 0x0,
295        low_bits_mask(1) == 0x1,
296        low_bits_mask(2) == 0x3,
297        low_bits_mask(3) == 0x7,
298        low_bits_mask(4) == 0xf,
299        low_bits_mask(5) == 0x1f,
300        low_bits_mask(6) == 0x3f,
301        low_bits_mask(7) == 0x7f,
302        low_bits_mask(8) == 0xff,
303        low_bits_mask(9) == 0x1ff,
304        low_bits_mask(10) == 0x3ff,
305        low_bits_mask(11) == 0x7ff,
306        low_bits_mask(12) == 0xfff,
307        low_bits_mask(13) == 0x1fff,
308        low_bits_mask(14) == 0x3fff,
309        low_bits_mask(15) == 0x7fff,
310        low_bits_mask(16) == 0xffff,
311        low_bits_mask(17) == 0x1ffff,
312        low_bits_mask(18) == 0x3ffff,
313        low_bits_mask(19) == 0x7ffff,
314        low_bits_mask(20) == 0xfffff,
315        low_bits_mask(21) == 0x1fffff,
316        low_bits_mask(22) == 0x3fffff,
317        low_bits_mask(23) == 0x7fffff,
318        low_bits_mask(24) == 0xffffff,
319        low_bits_mask(25) == 0x1ffffff,
320        low_bits_mask(26) == 0x3ffffff,
321        low_bits_mask(27) == 0x7ffffff,
322        low_bits_mask(28) == 0xfffffff,
323        low_bits_mask(29) == 0x1fffffff,
324        low_bits_mask(30) == 0x3fffffff,
325        low_bits_mask(31) == 0x7fffffff,
326        low_bits_mask(32) == 0xffffffff,
327        low_bits_mask(64) == 0xffffffffffffffff,
328{
329    reveal(pow2);
330    #[verusfmt::skip]
331    assert(
332        low_bits_mask(0) == 0x0 &&
333        low_bits_mask(1) == 0x1 &&
334        low_bits_mask(2) == 0x3 &&
335        low_bits_mask(3) == 0x7 &&
336        low_bits_mask(4) == 0xf &&
337        low_bits_mask(5) == 0x1f &&
338        low_bits_mask(6) == 0x3f &&
339        low_bits_mask(7) == 0x7f &&
340        low_bits_mask(8) == 0xff &&
341        low_bits_mask(9) == 0x1ff &&
342        low_bits_mask(10) == 0x3ff &&
343        low_bits_mask(11) == 0x7ff &&
344        low_bits_mask(12) == 0xfff &&
345        low_bits_mask(13) == 0x1fff &&
346        low_bits_mask(14) == 0x3fff &&
347        low_bits_mask(15) == 0x7fff &&
348        low_bits_mask(16) == 0xffff &&
349        low_bits_mask(17) == 0x1ffff &&
350        low_bits_mask(18) == 0x3ffff &&
351        low_bits_mask(19) == 0x7ffff &&
352        low_bits_mask(20) == 0xfffff &&
353        low_bits_mask(21) == 0x1fffff &&
354        low_bits_mask(22) == 0x3fffff &&
355        low_bits_mask(23) == 0x7fffff &&
356        low_bits_mask(24) == 0xffffff &&
357        low_bits_mask(25) == 0x1ffffff &&
358        low_bits_mask(26) == 0x3ffffff &&
359        low_bits_mask(27) == 0x7ffffff &&
360        low_bits_mask(28) == 0xfffffff &&
361        low_bits_mask(29) == 0x1fffffff &&
362        low_bits_mask(30) == 0x3fffffff &&
363        low_bits_mask(31) == 0x7fffffff &&
364        low_bits_mask(32) == 0xffffffff &&
365        low_bits_mask(64) == 0xffffffffffffffff
366    ) by (compute_only);
367}
368
369} // verus!
370// Proofs that and with mask is equivalent to modulo with power of two.
371macro_rules! lemma_low_bits_mask_is_mod {
372    ($name:ident, $and_split_low_bit:ident, $no_overflow:ident, $uN:ty) => {
373        #[cfg(verus_keep_ghost)]
374        verus! {
375        #[doc = "Proof that for natural n and x of type "]
376        #[doc = stringify!($uN)]
377        #[doc = ", and with the low n-bit mask is equivalent to modulo 2^n."]
378        pub broadcast proof fn $name(x: $uN, n: nat)
379            requires
380                n < <$uN>::BITS,
381            ensures
382                #[trigger] (x & (low_bits_mask(n) as $uN)) == x % (pow2(n) as $uN),
383            decreases n,
384        {
385            // Bounds.
386            $no_overflow(n);
387            lemma_pow2_pos(n);
388
389            // Inductive proof.
390            if n == 0 {
391                assert(low_bits_mask(0) == 0) by (compute_only);
392                assert(x & 0 == 0) by (bit_vector);
393                assert(pow2(0) == 1) by (compute_only);
394                assert(x % 1 == 0);
395            } else {
396                lemma_pow2_unfold(n);
397                assert((x % 2) == ((x % 2) & 1)) by (bit_vector);
398                calc!{ (==)
399                    x % (pow2(n) as $uN);
400                        {}
401                    x % ((2 * pow2((n-1) as nat)) as $uN);
402                        {
403                            lemma_pow2_pos((n-1) as nat);
404                            lemma_mod_breakdown(x as int, 2, pow2((n-1) as nat) as int);
405                        }
406                    add(mul(2, (x / 2) % (pow2((n-1) as nat) as $uN)), x % 2);
407                        {
408                            $name(x/2, (n-1) as nat);
409                        }
410                    add(mul(2, (x / 2) & (low_bits_mask((n-1) as nat) as $uN)), x % 2);
411                        {
412                            lemma_low_bits_mask_div2(n);
413                        }
414                    add(mul(2, (x / 2) & (low_bits_mask(n) as $uN / 2)), x % 2);
415                        {
416                            lemma_low_bits_mask_is_odd(n);
417                        }
418                    add(mul(2, (x / 2) & (low_bits_mask(n) as $uN / 2)), (x % 2) & ((low_bits_mask(n) as $uN) % 2));
419                        {
420                            $and_split_low_bit(x as $uN, low_bits_mask(n) as $uN);
421                        }
422                    x & (low_bits_mask(n) as $uN);
423                }
424            }
425        }
426
427        // Helper lemma breaking a bitwise-and operation into the low bit and the rest.
428        proof fn $and_split_low_bit(x: $uN, m: $uN)
429            by (bit_vector)
430            ensures
431                x & m == add(mul(((x / 2) & (m / 2)), 2), (x % 2) & (m % 2)),
432        {
433        }
434        }
435    };
436}
437
438lemma_low_bits_mask_is_mod!(
439    lemma_u64_low_bits_mask_is_mod,
440    lemma_u64_and_split_low_bit,
441    lemma_u64_pow2_no_overflow,
442    u64
443);
444lemma_low_bits_mask_is_mod!(
445    lemma_u32_low_bits_mask_is_mod,
446    lemma_u32_and_split_low_bit,
447    lemma_u32_pow2_no_overflow,
448    u32
449);
450lemma_low_bits_mask_is_mod!(
451    lemma_u16_low_bits_mask_is_mod,
452    lemma_u16_and_split_low_bit,
453    lemma_u16_pow2_no_overflow,
454    u16
455);
456lemma_low_bits_mask_is_mod!(
457    lemma_u8_low_bits_mask_is_mod,
458    lemma_u8_and_split_low_bit,
459    lemma_u8_pow2_no_overflow,
460    u8
461);