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