1use vstd::arithmetic::logarithm::*;
2use vstd::arithmetic::power::*;
3use vstd::arithmetic::power2::*;
4use vstd::bits::*;
5use vstd::prelude::*;
6
7verus! {
8
9broadcast use is_pow2_equiv;
10
11pub broadcast proof fn lemma_pow2_log2(e: nat)
12 ensures
13 #[trigger] log(2, pow2(e) as int) == e,
14{
15 lemma_pow2(e);
16 lemma_log_pow(2, e);
17}
18
19pub broadcast proof fn lemma_pow2_increases(e1: nat, e2: nat)
20 requires
21 e1 <= e2,
22 ensures
23 #[trigger] pow2(e1) <= #[trigger] pow2(e2),
24{
25 if e1 < e2 {
26 lemma_pow2_strictly_increases(e1, e2);
27 } else if e1 == e2 {
28 assert(pow2(e1) == pow2(e2));
29 }
30}
31
32pub broadcast proof fn lemma_pow2_is_pow2(e: nat)
33 ensures
34 #[trigger] is_pow2(pow2(e) as int),
35 decreases e,
36{
37 lemma_pow2(e);
38 assert(is_pow2_exists(pow2(e) as int)) by {
39 assert(pow(2, e) == pow2(e) as int);
40 }
41}
42
43pub proof fn lemma2_to64_hi32()
44 ensures
45 pow2(33) == 0x200000000,
46 pow2(34) == 0x400000000,
47 pow2(35) == 0x800000000,
48 pow2(36) == 0x1000000000,
49 pow2(37) == 0x2000000000,
50 pow2(38) == 0x4000000000,
51 pow2(39) == 0x8000000000,
52 pow2(40) == 0x10000000000,
53 pow2(41) == 0x20000000000,
54 pow2(42) == 0x40000000000,
55 pow2(43) == 0x80000000000,
56 pow2(44) == 0x100000000000,
57 pow2(45) == 0x200000000000,
58 pow2(46) == 0x400000000000,
59 pow2(47) == 0x800000000000,
60 pow2(48) == 0x1000000000000,
61 pow2(49) == 0x2000000000000,
62 pow2(50) == 0x4000000000000,
63 pow2(51) == 0x8000000000000,
64 pow2(52) == 0x10000000000000,
65 pow2(53) == 0x20000000000000,
66 pow2(54) == 0x40000000000000,
67 pow2(55) == 0x80000000000000,
68 pow2(56) == 0x100000000000000,
69 pow2(57) == 0x200000000000000,
70 pow2(58) == 0x400000000000000,
71 pow2(59) == 0x800000000000000,
72 pow2(60) == 0x1000000000000000,
73 pow2(61) == 0x2000000000000000,
74 pow2(62) == 0x4000000000000000,
75 pow2(63) == 0x8000000000000000,
76 pow2(64) == 0x10000000000000000,
77{
78 lemma2_to64();
79 reveal(pow2);
80 reveal(pow);
81 #[verusfmt::skip]
82 assert(
83 pow2(33) == 0x200000000 &&
84 pow2(34) == 0x400000000 &&
85 pow2(35) == 0x800000000 &&
86 pow2(36) == 0x1000000000 &&
87 pow2(37) == 0x2000000000 &&
88 pow2(38) == 0x4000000000 &&
89 pow2(39) == 0x8000000000 &&
90 pow2(40) == 0x10000000000 &&
91 pow2(41) == 0x20000000000 &&
92 pow2(42) == 0x40000000000 &&
93 pow2(43) == 0x80000000000 &&
94 pow2(44) == 0x100000000000 &&
95 pow2(45) == 0x200000000000 &&
96 pow2(46) == 0x400000000000 &&
97 pow2(47) == 0x800000000000 &&
98 pow2(48) == 0x1000000000000 &&
99 pow2(49) == 0x2000000000000 &&
100 pow2(50) == 0x4000000000000 &&
101 pow2(51) == 0x8000000000000 &&
102 pow2(52) == 0x10000000000000 &&
103 pow2(53) == 0x20000000000000 &&
104 pow2(54) == 0x40000000000000 &&
105 pow2(55) == 0x80000000000000 &&
106 pow2(56) == 0x100000000000000 &&
107 pow2(57) == 0x200000000000000 &&
108 pow2(58) == 0x400000000000000 &&
109 pow2(59) == 0x800000000000000 &&
110 pow2(60) == 0x1000000000000000 &&
111 pow2(61) == 0x2000000000000000 &&
112 pow2(62) == 0x4000000000000000 &&
113 pow2(63) == 0x8000000000000000 &&
114 pow2(64) == 0x10000000000000000
115 ) by (compute_only);
116}
117
118pub proof fn lemma_pow2_is_pow2_to64()
119 ensures
120 is_pow2(0x1),
121 is_pow2(0x2),
122 is_pow2(0x4),
123 is_pow2(0x8),
124 is_pow2(0x10),
125 is_pow2(0x20),
126 is_pow2(0x40),
127 is_pow2(0x80),
128 is_pow2(0x100),
129 is_pow2(0x200),
130 is_pow2(0x400),
131 is_pow2(0x800),
132 is_pow2(0x1000),
133 is_pow2(0x2000),
134 is_pow2(0x4000),
135 is_pow2(0x8000),
136 is_pow2(0x10000),
137 is_pow2(0x20000),
138 is_pow2(0x40000),
139 is_pow2(0x80000),
140 is_pow2(0x100000),
141 is_pow2(0x200000),
142 is_pow2(0x400000),
143 is_pow2(0x800000),
144 is_pow2(0x1000000),
145 is_pow2(0x2000000),
146 is_pow2(0x4000000),
147 is_pow2(0x8000000),
148 is_pow2(0x10000000),
149 is_pow2(0x20000000),
150 is_pow2(0x40000000),
151 is_pow2(0x80000000),
152 is_pow2(0x100000000),
153 is_pow2(0x200000000),
154 is_pow2(0x400000000),
155 is_pow2(0x800000000),
156 is_pow2(0x1000000000),
157 is_pow2(0x2000000000),
158 is_pow2(0x4000000000),
159 is_pow2(0x8000000000),
160 is_pow2(0x10000000000),
161 is_pow2(0x20000000000),
162 is_pow2(0x40000000000),
163 is_pow2(0x80000000000),
164 is_pow2(0x100000000000),
165 is_pow2(0x200000000000),
166 is_pow2(0x400000000000),
167 is_pow2(0x800000000000),
168 is_pow2(0x1000000000000),
169 is_pow2(0x2000000000000),
170 is_pow2(0x4000000000000),
171 is_pow2(0x8000000000000),
172 is_pow2(0x10000000000000),
173 is_pow2(0x20000000000000),
174 is_pow2(0x40000000000000),
175 is_pow2(0x80000000000000),
176 is_pow2(0x100000000000000),
177 is_pow2(0x200000000000000),
178 is_pow2(0x400000000000000),
179 is_pow2(0x800000000000000),
180 is_pow2(0x1000000000000000),
181 is_pow2(0x2000000000000000),
182 is_pow2(0x4000000000000000),
183 is_pow2(0x8000000000000000),
184 is_pow2(0x10000000000000000),
185{
186 lemma2_to64();
187 lemma2_to64_hi32();
188 lemma_pow2_is_pow2(0);
189 lemma_pow2_is_pow2(1);
190 lemma_pow2_is_pow2(2);
191 lemma_pow2_is_pow2(3);
192 lemma_pow2_is_pow2(4);
193 lemma_pow2_is_pow2(5);
194 lemma_pow2_is_pow2(6);
195 lemma_pow2_is_pow2(7);
196 lemma_pow2_is_pow2(8);
197 lemma_pow2_is_pow2(9);
198 lemma_pow2_is_pow2(10);
199 lemma_pow2_is_pow2(11);
200 lemma_pow2_is_pow2(12);
201 lemma_pow2_is_pow2(13);
202 lemma_pow2_is_pow2(14);
203 lemma_pow2_is_pow2(15);
204 lemma_pow2_is_pow2(16);
205 lemma_pow2_is_pow2(17);
206 lemma_pow2_is_pow2(18);
207 lemma_pow2_is_pow2(19);
208 lemma_pow2_is_pow2(20);
209 lemma_pow2_is_pow2(21);
210 lemma_pow2_is_pow2(22);
211 lemma_pow2_is_pow2(23);
212 lemma_pow2_is_pow2(24);
213 lemma_pow2_is_pow2(25);
214 lemma_pow2_is_pow2(26);
215 lemma_pow2_is_pow2(27);
216 lemma_pow2_is_pow2(28);
217 lemma_pow2_is_pow2(29);
218 lemma_pow2_is_pow2(30);
219 lemma_pow2_is_pow2(31);
220 lemma_pow2_is_pow2(32);
221 lemma_pow2_is_pow2(33);
222 lemma_pow2_is_pow2(34);
223 lemma_pow2_is_pow2(35);
224 lemma_pow2_is_pow2(36);
225 lemma_pow2_is_pow2(37);
226 lemma_pow2_is_pow2(38);
227 lemma_pow2_is_pow2(39);
228 lemma_pow2_is_pow2(40);
229 lemma_pow2_is_pow2(41);
230 lemma_pow2_is_pow2(42);
231 lemma_pow2_is_pow2(43);
232 lemma_pow2_is_pow2(44);
233 lemma_pow2_is_pow2(45);
234 lemma_pow2_is_pow2(46);
235 lemma_pow2_is_pow2(47);
236 lemma_pow2_is_pow2(48);
237 lemma_pow2_is_pow2(49);
238 lemma_pow2_is_pow2(50);
239 lemma_pow2_is_pow2(51);
240 lemma_pow2_is_pow2(52);
241 lemma_pow2_is_pow2(53);
242 lemma_pow2_is_pow2(54);
243 lemma_pow2_is_pow2(55);
244 lemma_pow2_is_pow2(56);
245 lemma_pow2_is_pow2(57);
246 lemma_pow2_is_pow2(58);
247 lemma_pow2_is_pow2(59);
248 lemma_pow2_is_pow2(60);
249 lemma_pow2_is_pow2(61);
250 lemma_pow2_is_pow2(62);
251 lemma_pow2_is_pow2(63);
252 lemma_pow2_is_pow2(64);
253}
254
255pub proof fn lemma_log2_to64()
256 ensures
257 log(2, 0x1) == 0,
258 log(2, 0x2) == 1,
259 log(2, 0x4) == 2,
260 log(2, 0x8) == 3,
261 log(2, 0x10) == 4,
262 log(2, 0x20) == 5,
263 log(2, 0x40) == 6,
264 log(2, 0x80) == 7,
265 log(2, 0x100) == 8,
266 log(2, 0x200) == 9,
267 log(2, 0x400) == 10,
268 log(2, 0x800) == 11,
269 log(2, 0x1000) == 12,
270 log(2, 0x2000) == 13,
271 log(2, 0x4000) == 14,
272 log(2, 0x8000) == 15,
273 log(2, 0x10000) == 16,
274 log(2, 0x20000) == 17,
275 log(2, 0x40000) == 18,
276 log(2, 0x80000) == 19,
277 log(2, 0x100000) == 20,
278 log(2, 0x200000) == 21,
279 log(2, 0x400000) == 22,
280 log(2, 0x800000) == 23,
281 log(2, 0x1000000) == 24,
282 log(2, 0x2000000) == 25,
283 log(2, 0x4000000) == 26,
284 log(2, 0x8000000) == 27,
285 log(2, 0x10000000) == 28,
286 log(2, 0x20000000) == 29,
287 log(2, 0x40000000) == 30,
288 log(2, 0x80000000) == 31,
289 log(2, 0x100000000) == 32,
290 log(2, 0x200000000) == 33,
291 log(2, 0x400000000) == 34,
292 log(2, 0x800000000) == 35,
293 log(2, 0x1000000000) == 36,
294 log(2, 0x2000000000) == 37,
295 log(2, 0x4000000000) == 38,
296 log(2, 0x8000000000) == 39,
297 log(2, 0x10000000000) == 40,
298 log(2, 0x20000000000) == 41,
299 log(2, 0x40000000000) == 42,
300 log(2, 0x80000000000) == 43,
301 log(2, 0x100000000000) == 44,
302 log(2, 0x200000000000) == 45,
303 log(2, 0x400000000000) == 46,
304 log(2, 0x800000000000) == 47,
305 log(2, 0x1000000000000) == 48,
306 log(2, 0x2000000000000) == 49,
307 log(2, 0x4000000000000) == 50,
308 log(2, 0x8000000000000) == 51,
309 log(2, 0x10000000000000) == 52,
310 log(2, 0x20000000000000) == 53,
311 log(2, 0x40000000000000) == 54,
312 log(2, 0x80000000000000) == 55,
313 log(2, 0x100000000000000) == 56,
314 log(2, 0x200000000000000) == 57,
315 log(2, 0x400000000000000) == 58,
316 log(2, 0x800000000000000) == 59,
317 log(2, 0x1000000000000000) == 60,
318 log(2, 0x2000000000000000) == 61,
319 log(2, 0x4000000000000000) == 62,
320 log(2, 0x8000000000000000) == 63,
321 log(2, 0x10000000000000000) == 64,
322{
323 lemma2_to64();
324 lemma2_to64_hi32();
325 lemma_pow2_log2(0);
326 lemma_pow2_log2(1);
327 lemma_pow2_log2(2);
328 lemma_pow2_log2(3);
329 lemma_pow2_log2(4);
330 lemma_pow2_log2(5);
331 lemma_pow2_log2(6);
332 lemma_pow2_log2(7);
333 lemma_pow2_log2(8);
334 lemma_pow2_log2(9);
335 lemma_pow2_log2(10);
336 lemma_pow2_log2(11);
337 lemma_pow2_log2(12);
338 lemma_pow2_log2(13);
339 lemma_pow2_log2(14);
340 lemma_pow2_log2(15);
341 lemma_pow2_log2(16);
342 lemma_pow2_log2(17);
343 lemma_pow2_log2(18);
344 lemma_pow2_log2(19);
345 lemma_pow2_log2(20);
346 lemma_pow2_log2(21);
347 lemma_pow2_log2(22);
348 lemma_pow2_log2(23);
349 lemma_pow2_log2(24);
350 lemma_pow2_log2(25);
351 lemma_pow2_log2(26);
352 lemma_pow2_log2(27);
353 lemma_pow2_log2(28);
354 lemma_pow2_log2(29);
355 lemma_pow2_log2(30);
356 lemma_pow2_log2(31);
357 lemma_pow2_log2(32);
358 lemma_pow2_log2(33);
359 lemma_pow2_log2(34);
360 lemma_pow2_log2(35);
361 lemma_pow2_log2(36);
362 lemma_pow2_log2(37);
363 lemma_pow2_log2(38);
364 lemma_pow2_log2(39);
365 lemma_pow2_log2(40);
366 lemma_pow2_log2(41);
367 lemma_pow2_log2(42);
368 lemma_pow2_log2(43);
369 lemma_pow2_log2(44);
370 lemma_pow2_log2(45);
371 lemma_pow2_log2(46);
372 lemma_pow2_log2(47);
373 lemma_pow2_log2(48);
374 lemma_pow2_log2(49);
375 lemma_pow2_log2(50);
376 lemma_pow2_log2(51);
377 lemma_pow2_log2(52);
378 lemma_pow2_log2(53);
379 lemma_pow2_log2(54);
380 lemma_pow2_log2(55);
381 lemma_pow2_log2(56);
382 lemma_pow2_log2(57);
383 lemma_pow2_log2(58);
384 lemma_pow2_log2(59);
385 lemma_pow2_log2(60);
386 lemma_pow2_log2(61);
387 lemma_pow2_log2(62);
388 lemma_pow2_log2(63);
389 lemma_pow2_log2(64);
390}
391
392} macro_rules! impl_external_ilog2 {
394 ($uN: ty, $spec_name: ident,
395 $pow2_lemma: ident, $pow2_ilog2_lemma: ident,
396 $log2_bounds_lemma: ident, $ilog2_ordered_lemma: ident, $is_pow2_is_ilog2_pow2_lemma: ident $(,)?) => {
397 verus! {
398 #[verifier::inline]
399 pub open spec fn $spec_name(x: $uN) -> u32
400 {
401 log(2, x as int) as u32
402 }
403
404 #[verifier::when_used_as_spec($spec_name)]
405 pub assume_specification[$uN::ilog2](x:$uN) -> u32
406 requires
407 x > 0,
408 returns
409 log(2, x as int) as u32,
410 opens_invariants none
411 no_unwind;
412
413 pub broadcast proof fn $pow2_lemma(e: u32, x: $uN)
414 requires
415 #[trigger] pow2(e as nat) == x,
416 ensures
417 #[trigger] x.ilog2() == e,
418 {
419 lemma_pow2_log2(e as nat);
420 }
421
422 pub broadcast proof fn $pow2_ilog2_lemma(e: u32)
423 requires
424 pow2(e as nat) <= $uN::MAX,
425 ensures
426 #[trigger] (pow2(e as nat) as $uN).ilog2() == e,
427 {
428 $pow2_lemma(e, pow2(e as nat) as $uN);
429 }
430
431 pub proof fn $log2_bounds_lemma(x: $uN)
432 ensures
433 0 <= log(2, x as int) <= $uN::BITS,
434 0 <= x.ilog2() <= $uN::BITS,
435 {
436 lemma_log_nonnegative(2, x as int);
437 assert(x <= $uN::MAX);
438 assert(($uN::MAX as int) < (pow2($uN::BITS as nat) as int)) by {
439 lemma2_to64();
440 };
441 assert(log(2, x as int) <= log(2, pow2($uN::BITS as nat) as int)) by {
442 lemma_log_is_ordered(2, x as int, pow2($uN::BITS as nat) as int);
443 };
444 assert(log(2, pow2($uN::BITS as nat) as int) == $uN::BITS) by {
445 lemma_pow2_log2($uN::BITS as nat);
446 };
447 }
448
449 pub proof fn $ilog2_ordered_lemma(x: $uN, y: $uN)
450 requires
451 x <= y,
452 ensures
453 x.ilog2() <= y.ilog2(),
454 {
455 $log2_bounds_lemma(x);
456 $log2_bounds_lemma(y);
457 lemma_log_is_ordered(2, x as int, y as int);
458 }
459
460 pub broadcast proof fn $is_pow2_is_ilog2_pow2_lemma(x: $uN)
461 requires
462 #[trigger] is_pow2(x as int),
463 ensures
464 x as nat == pow2(x.ilog2() as nat),
465 {
466 let n = choose |n: nat| pow(2, n) == x as int;
467 assert(log(2, x as int) == n) by {
468 lemma_log_pow(2, n);
469 assert(pow(2, n) == x as int);
470 };
471 $log2_bounds_lemma(x);
472 assert(log(2, x as int) <= $uN::BITS);
473 assert(n <= $uN::BITS) by {
474 assert(log(2, x as int) == n);
475 };
476 assert(x.ilog2() == n);
477 lemma_pow2(n);
478 }
479 }
480 };
481}
482
483impl_external_ilog2!(
484 u8,
485 u8_ilog2_spec,
486 lemma_u8_pow2_ilog2_x,
487 lemma_u8_pow2_ilog2,
488 lemma_u8_log2_bounds,
489 lemma_u8_ilog2_ordered,
490 lemma_u8_is_pow2_is_ilog2_pow2,
491);
492
493impl_external_ilog2!(
494 u16,
495 u16_ilog2_spec,
496 lemma_u16_pow2_ilog2_x,
497 lemma_u16_pow2_ilog2,
498 lemma_u16_log2_bounds,
499 lemma_u16_ilog2_ordered,
500 lemma_u16_is_pow2_is_ilog2_pow2,
501);
502
503impl_external_ilog2!(
504 u32,
505 u32_ilog2_spec,
506 lemma_u32_pow2_ilog2_x,
507 lemma_u32_pow2_ilog2,
508 lemma_u32_log2_bounds,
509 lemma_u32_ilog2_ordered,
510 lemma_u32_is_pow2_is_ilog2_pow2,
511);
512
513impl_external_ilog2!(
514 usize,
515 usize_ilog2_spec,
516 lemma_usize_pow2_ilog2_x,
517 lemma_usize_pow2_ilog2,
518 lemma_usize_log2_bounds,
519 lemma_usize_ilog2_ordered,
520 lemma_usize_is_pow2_is_ilog2_pow2,
521);
522
523impl_external_ilog2!(
524 u64,
525 u64_ilog2_spec,
526 lemma_u64_pow2_ilog2_x,
527 lemma_u64_pow2_ilog2,
528 lemma_u64_log2_bounds,
529 lemma_u64_ilog2_ordered,
530 lemma_u64_is_pow2_is_ilog2_pow2,
531);
532
533verus! {
534
535pub proof fn lemma_u8_ilog2_to8()
536 ensures
537 (0x1 as u8).ilog2() == 0,
538 (0x2 as u8).ilog2() == 1,
539 (0x4 as u8).ilog2() == 2,
540 (0x8 as u8).ilog2() == 3,
541 (0x10 as u8).ilog2() == 4,
542 (0x20 as u8).ilog2() == 5,
543 (0x40 as u8).ilog2() == 6,
544 (0x80 as u8).ilog2() == 7,
545{
546 lemma_log2_to64();
547}
548
549pub proof fn lemma_u16_ilog2_to16()
550 ensures
551 (0x1 as u16).ilog2() == 0,
552 (0x2 as u16).ilog2() == 1,
553 (0x4 as u16).ilog2() == 2,
554 (0x8 as u16).ilog2() == 3,
555 (0x10 as u16).ilog2() == 4,
556 (0x20 as u16).ilog2() == 5,
557 (0x40 as u16).ilog2() == 6,
558 (0x80 as u16).ilog2() == 7,
559 (0x100 as u16).ilog2() == 8,
560 (0x200 as u16).ilog2() == 9,
561 (0x400 as u16).ilog2() == 10,
562 (0x800 as u16).ilog2() == 11,
563 (0x1000 as u16).ilog2() == 12,
564 (0x2000 as u16).ilog2() == 13,
565 (0x4000 as u16).ilog2() == 14,
566 (0x8000 as u16).ilog2() == 15,
567{
568 lemma_log2_to64();
569}
570
571pub proof fn lemma_u32_ilog2_to32()
572 ensures
573 (0x1 as u32).ilog2() == 0,
574 (0x2 as u32).ilog2() == 1,
575 (0x4 as u32).ilog2() == 2,
576 (0x8 as u32).ilog2() == 3,
577 (0x10 as u32).ilog2() == 4,
578 (0x20 as u32).ilog2() == 5,
579 (0x40 as u32).ilog2() == 6,
580 (0x80 as u32).ilog2() == 7,
581 (0x100 as u32).ilog2() == 8,
582 (0x200 as u32).ilog2() == 9,
583 (0x400 as u32).ilog2() == 10,
584 (0x800 as u32).ilog2() == 11,
585 (0x1000 as u32).ilog2() == 12,
586 (0x2000 as u32).ilog2() == 13,
587 (0x4000 as u32).ilog2() == 14,
588 (0x8000 as u32).ilog2() == 15,
589 (0x10000 as u32).ilog2() == 16,
590 (0x20000 as u32).ilog2() == 17,
591 (0x40000 as u32).ilog2() == 18,
592 (0x80000 as u32).ilog2() == 19,
593 (0x100000 as u32).ilog2() == 20,
594 (0x200000 as u32).ilog2() == 21,
595 (0x400000 as u32).ilog2() == 22,
596 (0x800000 as u32).ilog2() == 23,
597 (0x1000000 as u32).ilog2() == 24,
598 (0x2000000 as u32).ilog2() == 25,
599 (0x4000000 as u32).ilog2() == 26,
600 (0x8000000 as u32).ilog2() == 27,
601 (0x10000000 as u32).ilog2() == 28,
602 (0x20000000 as u32).ilog2() == 29,
603 (0x40000000 as u32).ilog2() == 30,
604 (0x80000000 as u32).ilog2() == 31,
605{
606 lemma_log2_to64();
607}
608
609pub proof fn lemma_usize_ilog2_to32()
610 ensures
611 (0x1 as usize).ilog2() == 0,
612 (0x2 as usize).ilog2() == 1,
613 (0x4 as usize).ilog2() == 2,
614 (0x8 as usize).ilog2() == 3,
615 (0x10 as usize).ilog2() == 4,
616 (0x20 as usize).ilog2() == 5,
617 (0x40 as usize).ilog2() == 6,
618 (0x80 as usize).ilog2() == 7,
619 (0x100 as usize).ilog2() == 8,
620 (0x200 as usize).ilog2() == 9,
621 (0x400 as usize).ilog2() == 10,
622 (0x800 as usize).ilog2() == 11,
623 (0x1000 as usize).ilog2() == 12,
624 (0x2000 as usize).ilog2() == 13,
625 (0x4000 as usize).ilog2() == 14,
626 (0x8000 as usize).ilog2() == 15,
627 (0x10000 as usize).ilog2() == 16,
628 (0x20000 as usize).ilog2() == 17,
629 (0x40000 as usize).ilog2() == 18,
630 (0x80000 as usize).ilog2() == 19,
631 (0x100000 as usize).ilog2() == 20,
632 (0x200000 as usize).ilog2() == 21,
633 (0x400000 as usize).ilog2() == 22,
634 (0x800000 as usize).ilog2() == 23,
635 (0x1000000 as usize).ilog2() == 24,
636 (0x2000000 as usize).ilog2() == 25,
637 (0x4000000 as usize).ilog2() == 26,
638 (0x8000000 as usize).ilog2() == 27,
639 (0x10000000 as usize).ilog2() == 28,
640 (0x20000000 as usize).ilog2() == 29,
641 (0x40000000 as usize).ilog2() == 30,
642 (0x80000000 as usize).ilog2() == 31,
643{
644 lemma_log2_to64();
645}
646
647pub proof fn lemma_u64_ilog2_to64()
648 ensures
649 (0x1 as u64).ilog2() == 0,
650 (0x2 as u64).ilog2() == 1,
651 (0x4 as u64).ilog2() == 2,
652 (0x8 as u64).ilog2() == 3,
653 (0x10 as u64).ilog2() == 4,
654 (0x20 as u64).ilog2() == 5,
655 (0x40 as u64).ilog2() == 6,
656 (0x80 as u64).ilog2() == 7,
657 (0x100 as u64).ilog2() == 8,
658 (0x200 as u64).ilog2() == 9,
659 (0x400 as u64).ilog2() == 10,
660 (0x800 as u64).ilog2() == 11,
661 (0x1000 as u64).ilog2() == 12,
662 (0x2000 as u64).ilog2() == 13,
663 (0x4000 as u64).ilog2() == 14,
664 (0x8000 as u64).ilog2() == 15,
665 (0x10000 as u64).ilog2() == 16,
666 (0x20000 as u64).ilog2() == 17,
667 (0x40000 as u64).ilog2() == 18,
668 (0x80000 as u64).ilog2() == 19,
669 (0x100000 as u64).ilog2() == 20,
670 (0x200000 as u64).ilog2() == 21,
671 (0x400000 as u64).ilog2() == 22,
672 (0x800000 as u64).ilog2() == 23,
673 (0x1000000 as u64).ilog2() == 24,
674 (0x2000000 as u64).ilog2() == 25,
675 (0x4000000 as u64).ilog2() == 26,
676 (0x8000000 as u64).ilog2() == 27,
677 (0x10000000 as u64).ilog2() == 28,
678 (0x20000000 as u64).ilog2() == 29,
679 (0x40000000 as u64).ilog2() == 30,
680 (0x80000000 as u64).ilog2() == 31,
681 (0x100000000 as u64).ilog2() == 32,
682 (0x200000000 as u64).ilog2() == 33,
683 (0x400000000 as u64).ilog2() == 34,
684 (0x800000000 as u64).ilog2() == 35,
685 (0x1000000000 as u64).ilog2() == 36,
686 (0x2000000000 as u64).ilog2() == 37,
687 (0x4000000000 as u64).ilog2() == 38,
688 (0x8000000000 as u64).ilog2() == 39,
689 (0x10000000000 as u64).ilog2() == 40,
690 (0x20000000000 as u64).ilog2() == 41,
691 (0x40000000000 as u64).ilog2() == 42,
692 (0x80000000000 as u64).ilog2() == 43,
693 (0x100000000000 as u64).ilog2() == 44,
694 (0x200000000000 as u64).ilog2() == 45,
695 (0x400000000000 as u64).ilog2() == 46,
696 (0x800000000000 as u64).ilog2() == 47,
697 (0x1000000000000 as u64).ilog2() == 48,
698 (0x2000000000000 as u64).ilog2() == 49,
699 (0x4000000000000 as u64).ilog2() == 50,
700 (0x8000000000000 as u64).ilog2() == 51,
701 (0x10000000000000 as u64).ilog2() == 52,
702 (0x20000000000000 as u64).ilog2() == 53,
703 (0x40000000000000 as u64).ilog2() == 54,
704 (0x80000000000000 as u64).ilog2() == 55,
705 (0x100000000000000 as u64).ilog2() == 56,
706 (0x200000000000000 as u64).ilog2() == 57,
707 (0x400000000000000 as u64).ilog2() == 58,
708 (0x800000000000000 as u64).ilog2() == 59,
709 (0x1000000000000000 as u64).ilog2() == 60,
710 (0x2000000000000000 as u64).ilog2() == 61,
711 (0x4000000000000000 as u64).ilog2() == 62,
712 (0x8000000000000000 as u64).ilog2() == 63,
713{
714 lemma_log2_to64();
715}
716
717pub broadcast proof fn lemma_usize_shl_is_mul(x: usize, shift: usize)
718 requires
719 0 <= shift < usize::BITS,
720 x * pow2(shift as nat) <= usize::MAX,
721 ensures
722 #[trigger] (x << shift) == x * pow2(shift as nat),
723{
724 if usize::BITS == 64 {
725 lemma_u64_shl_is_mul(x as u64, shift as u64);
726 } else if usize::BITS == 32 {
727 lemma_u32_shl_is_mul(x as u32, shift as u32);
728 } else {
729 assert(false);
730 }
731}
732
733pub broadcast proof fn lemma_usize_pow2_shl_is_pow2(x: usize, shift: usize)
734 requires
735 0 <= shift < usize::BITS,
736 is_pow2(x as int),
737 x * pow2(shift as nat) <= usize::MAX,
738 ensures
739 #[trigger] is_pow2((x << shift) as int),
740{
741 let n = choose|n: nat| pow(2, n) == x as int;
742 lemma_pow2(n);
743 assert(pow2(n) as int == x as int);
744 assert(x as nat == pow2(n));
745 lemma_usize_shl_is_mul(x, shift);
746 assert(x << shift == x * pow2(shift as nat));
747 lemma_pow2_adds(n, shift as nat);
748 assert(x * pow2(shift as nat) == pow2(n) * pow2(shift as nat));
749 assert(x * pow2(shift as nat) == pow2(n + shift as nat));
750 lemma_pow2_is_pow2(n + shift as nat);
751 assert(is_pow2((x << shift) as int));
752}
753
754}