1use 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} macro_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
91macro_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
118macro_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
235pub open spec fn low_bits_mask(n: nat) -> nat {
237 (pow2(n) - 1) as nat
238}
239
240pub 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
261pub 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
280pub 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
290pub 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} macro_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 $no_overflow(n);
387 lemma_pow2_pos(n);
388
389 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 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);