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