1use super::super::prelude::*;
2
3verus! {
4
5pub closed spec fn u8_trailing_zeros(i: u8) -> u32
12 decreases i,
13{
14 if i == 0 {
15 8
16 } else if (i & 1) != 0 {
17 0
18 } else {
19 (1 + u8_trailing_zeros(i / 2)) as u32
20 }
21}
22
23pub closed spec fn u8_leading_zeros(i: u8) -> u32
26 decreases i,
27{
28 if i == 0 {
29 8
30 } else {
31 (u8_leading_zeros(i / 2) - 1) as u32
32 }
33}
34
35pub open spec fn u8_trailing_ones(i: u8) -> u32 {
38 u8_trailing_zeros(!i)
39}
40
41pub open spec fn u8_leading_ones(i: u8) -> u32 {
44 u8_leading_zeros(!i)
45}
46
47#[verifier::when_used_as_spec(u8_trailing_zeros)]
48pub assume_specification[ u8::trailing_zeros ](i: u8) -> (r: u32)
49 ensures
50 r == u8_trailing_zeros(i),
51;
52
53#[verifier::when_used_as_spec(u8_trailing_ones)]
54pub assume_specification[ u8::trailing_ones ](i: u8) -> (r: u32)
55 ensures
56 r == u8_trailing_ones(i),
57;
58
59#[verifier::when_used_as_spec(u8_leading_zeros)]
60pub assume_specification[ u8::leading_zeros ](i: u8) -> (r: u32)
61 ensures
62 r == u8_leading_zeros(i),
63;
64
65#[verifier::when_used_as_spec(u8_leading_ones)]
66pub assume_specification[ u8::leading_ones ](i: u8) -> (r: u32)
67 ensures
68 r == u8_leading_ones(i),
69;
70
71pub broadcast proof fn axiom_u8_trailing_zeros(i: u8)
72 ensures
73 0 <= #[trigger] u8_trailing_zeros(i) <= 8,
74 i == 0 <==> u8_trailing_zeros(i) == 8,
75 0 <= u8_trailing_zeros(i) < 8 ==> (i >> u8_trailing_zeros(i) as u8) & 1u8 == 1u8,
77 i << sub(8, u8_trailing_zeros(i) as u8) == 0,
79 forall|j: u8| 0 <= j < u8_trailing_zeros(i) ==> #[trigger] (i >> j) & 1u8 == 0u8,
80 decreases i,
81{
82 assert(i >> 0 == i) by (bit_vector);
83 assert(i << 0 == i) by (bit_vector);
84 assert(i & 0 == 0) by (bit_vector);
85 assert(i / 2 == (i >> 1u8)) by (bit_vector);
86 assert((i & 1) == 0 ==> i != 1) by (bit_vector);
87 let x = u8_trailing_zeros(i / 2) as u8;
88 assert(x < 8 ==> (i >> 1) >> x == (i >> add(x, 1))) by (bit_vector);
89 assert(i << 8 == 0) by (bit_vector);
90 assert(i & 1 != 0 ==> i & 1 == 1) by (bit_vector);
91 assert((i & 1) == 0 ==> (i >> 1) << sub(8, x) == 0 ==> i << sub(8, add(x, 1)) == 0)
92 by (bit_vector);
93 if i != 0 {
94 axiom_u8_trailing_zeros(i / 2);
95 }
96 assert forall|j: u8| 0 <= j < u8_trailing_zeros(i) implies #[trigger] (i >> j) & 1u8 == 0u8 by {
97 let y = u8_trailing_zeros(i) as u8;
98 assert(y <= 8 ==> i << sub(8, y) == 0 && 0 <= j < y ==> (i >> j) & 1u8 == 0u8)
99 by (bit_vector);
100 }
101}
102
103pub broadcast proof fn axiom_u8_trailing_ones(i: u8)
104 ensures
105 0 <= #[trigger] u8_trailing_ones(i) <= 8,
106 i == 0xffu8 <==> u8_trailing_ones(i) == 8,
107 0 <= u8_trailing_ones(i) < 8 ==> (i >> u8_trailing_ones(i) as u8) & 1u8 == 0u8,
109 (!i) << sub(8, u8_trailing_ones(i) as u8) == 0,
111 forall|j: u8| 0 <= j < u8_trailing_ones(i) ==> #[trigger] (i >> j) & 1u8 == 1u8,
112{
113 axiom_u8_trailing_zeros(!i);
114 assert(!0xffu8 == 0) by (bit_vector);
115 assert(!i == 0 ==> i == 0xffu8) by (bit_vector);
116 let x = u8_trailing_ones(i) as u8;
117 assert(((!i) >> x) & 1u8 == 1u8 ==> (i >> x) & 1u8 == 0u8) by (bit_vector);
118 assert forall|j: u8| 0 <= j < u8_trailing_ones(i) implies #[trigger] (i >> j) & 1u8 == 1u8 by {
119 let y = u8_trailing_ones(i) as u8;
120 assert(y <= 8 ==> (!i) << sub(8, y) == 0 && 0 <= j < y ==> (i >> j) & 1u8 == 1u8)
121 by (bit_vector);
122 }
123}
124
125pub broadcast proof fn axiom_u8_leading_zeros(i: u8)
126 ensures
127 0 <= #[trigger] u8_leading_zeros(i) <= 8,
128 i == 0 <==> u8_leading_zeros(i) == 8,
129 0 <= u8_leading_zeros(i) < 8 ==> (i >> sub(7u8, u8_leading_zeros(i) as u8)) & 1u8 != 0u8,
131 i >> sub(8, u8_leading_zeros(i) as u8) == 0,
133 forall|j: u8| 8 - u8_leading_zeros(i) <= j < 8 ==> #[trigger] (i >> j) & 1u8 == 0u8,
134 decreases i,
135{
136 assert(i / 2 == (i >> 1u8)) by (bit_vector);
137 assert(((i >> 1) >> sub(7u8, 0)) & 1u8 == 0u8) by (bit_vector);
138 let x = u8_leading_zeros(i / 2) as u8;
139 assert(i >> 0 == i) by (bit_vector);
140 assert(1u8 & 1u8 == 1u8) by (bit_vector);
141 assert(0 < x < 8 ==> ((i >> 1) >> sub(7u8, x)) == (i >> sub(7u8, sub(x, 1)))) by (bit_vector);
142 assert(0 < x <= 8 ==> (i >> 1) >> sub(8, x) == 0 ==> i >> sub(8, sub(x, 1)) == 0)
143 by (bit_vector);
144 if i != 0 {
145 axiom_u8_leading_zeros(i / 2);
146 }
147 assert forall|j: u8| 8 - u8_leading_zeros(i) <= j < 8 implies #[trigger] (i >> j) & 1u8
148 == 0u8 by {
149 let y = u8_leading_zeros(i) as u8;
150 assert(y <= 8 ==> i >> sub(8, y) == 0 ==> sub(8, y) <= j < 8 ==> (i >> j) & 1u8 == 0u8)
151 by (bit_vector);
152 }
153}
154
155pub broadcast proof fn axiom_u8_leading_ones(i: u8)
156 ensures
157 0 <= #[trigger] u8_leading_ones(i) <= 8,
158 i == 0xffu8 <==> u8_leading_ones(i) == 8,
159 0 <= u8_leading_ones(i) < 8 ==> (i >> sub(7u8, u8_leading_ones(i) as u8)) & 1u8 == 0u8,
161 (!i) >> sub(8, u8_leading_ones(i) as u8) == 0,
162 forall|j: u8| 8 - u8_leading_ones(i) <= j < 8 ==> #[trigger] (i >> j) & 1u8 == 1u8,
163{
164 axiom_u8_leading_zeros(!i);
165 assert(!0xffu8 == 0) by (bit_vector);
166 assert(!i == 0 ==> i == 0xffu8) by (bit_vector);
167 let x = u8_leading_ones(i) as u8;
168 assert(((!i) >> sub(7u8, x)) & 1u8 != 0u8 ==> (i >> sub(7u8, x)) & 1u8 == 0u8) by (bit_vector);
169 assert forall|j: u8| 8 - u8_leading_ones(i) <= j < 8 implies #[trigger] (i >> j) & 1u8
170 == 1u8 by {
171 let y = u8_leading_ones(i) as u8;
172 assert(y <= 8 ==> (!i) >> sub(8, y) == 0 ==> sub(8, y) <= j < 8 ==> (i >> j) & 1u8 == 1u8)
173 by (bit_vector);
174 }
175}
176
177pub closed spec fn u16_trailing_zeros(i: u16) -> u32
182 decreases i,
183{
184 if i == 0 {
185 16
186 } else if (i & 1) != 0 {
187 0
188 } else {
189 (1 + u16_trailing_zeros(i / 2)) as u32
190 }
191}
192
193pub closed spec fn u16_leading_zeros(i: u16) -> u32
196 decreases i,
197{
198 if i == 0 {
199 16
200 } else {
201 (u16_leading_zeros(i / 2) - 1) as u32
202 }
203}
204
205pub open spec fn u16_trailing_ones(i: u16) -> u32 {
208 u16_trailing_zeros(!i)
209}
210
211pub open spec fn u16_leading_ones(i: u16) -> u32 {
214 u16_leading_zeros(!i)
215}
216
217#[verifier::when_used_as_spec(u16_trailing_zeros)]
218pub assume_specification[ u16::trailing_zeros ](i: u16) -> (r: u32)
219 ensures
220 r == u16_trailing_zeros(i),
221;
222
223#[verifier::when_used_as_spec(u16_trailing_ones)]
224pub assume_specification[ u16::trailing_ones ](i: u16) -> (r: u32)
225 ensures
226 r == u16_trailing_ones(i),
227;
228
229#[verifier::when_used_as_spec(u16_leading_zeros)]
230pub assume_specification[ u16::leading_zeros ](i: u16) -> (r: u32)
231 ensures
232 r == u16_leading_zeros(i),
233;
234
235#[verifier::when_used_as_spec(u16_leading_ones)]
236pub assume_specification[ u16::leading_ones ](i: u16) -> (r: u32)
237 ensures
238 r == u16_leading_ones(i),
239;
240
241pub broadcast proof fn axiom_u16_trailing_zeros(i: u16)
242 ensures
243 0 <= #[trigger] u16_trailing_zeros(i) <= 16,
244 i == 0 <==> u16_trailing_zeros(i) == 16,
245 0 <= u16_trailing_zeros(i) < 16 ==> (i >> u16_trailing_zeros(i) as u16) & 1u16 == 1u16,
247 i << sub(16, u16_trailing_zeros(i) as u16) == 0,
249 forall|j: u16| 0 <= j < u16_trailing_zeros(i) ==> #[trigger] (i >> j) & 1u16 == 0u16,
250 decreases i,
251{
252 assert(i >> 0 == i) by (bit_vector);
253 assert(i << 0 == i) by (bit_vector);
254 assert(i & 0 == 0) by (bit_vector);
255 assert(i / 2 == (i >> 1u16)) by (bit_vector);
256 assert((i & 1) == 0 ==> i != 1) by (bit_vector);
257 let x = u16_trailing_zeros(i / 2) as u16;
258 assert(x < 16 ==> (i >> 1) >> x == (i >> add(x, 1))) by (bit_vector);
259 assert(i << 16 == 0) by (bit_vector);
260 assert(i & 1 != 0 ==> i & 1 == 1) by (bit_vector);
261 assert((i & 1) == 0 ==> (i >> 1) << sub(16, x) == 0 ==> i << sub(16, add(x, 1)) == 0)
262 by (bit_vector);
263 if i != 0 {
264 axiom_u16_trailing_zeros(i / 2);
265 }
266 assert forall|j: u16| 0 <= j < u16_trailing_zeros(i) implies #[trigger] (i >> j) & 1u16
267 == 0u16 by {
268 let y = u16_trailing_zeros(i) as u16;
269 assert(y <= 16 ==> i << sub(16, y) == 0 && 0 <= j < y ==> (i >> j) & 1u16 == 0u16)
270 by (bit_vector);
271 }
272}
273
274pub broadcast proof fn axiom_u16_trailing_ones(i: u16)
275 ensures
276 0 <= #[trigger] u16_trailing_ones(i) <= 16,
277 i == 0xffffu16 <==> u16_trailing_ones(i) == 16,
278 0 <= u16_trailing_ones(i) < 16 ==> (i >> u16_trailing_ones(i) as u16) & 1u16 == 0u16,
280 (!i) << sub(16, u16_trailing_ones(i) as u16) == 0,
282 forall|j: u16| 0 <= j < u16_trailing_ones(i) ==> #[trigger] (i >> j) & 1u16 == 1u16,
283{
284 axiom_u16_trailing_zeros(!i);
285 assert(!0xffffu16 == 0) by (bit_vector);
286 assert(!i == 0 ==> i == 0xffffu16) by (bit_vector);
287 let x = u16_trailing_ones(i) as u16;
288 assert(((!i) >> x) & 1u16 == 1u16 ==> (i >> x) & 1u16 == 0u16) by (bit_vector);
289 assert forall|j: u16| 0 <= j < u16_trailing_ones(i) implies #[trigger] (i >> j) & 1u16
290 == 1u16 by {
291 let y = u16_trailing_ones(i) as u16;
292 assert(y <= 16 ==> (!i) << sub(16, y) == 0 && 0 <= j < y ==> (i >> j) & 1u16 == 1u16)
293 by (bit_vector);
294 }
295}
296
297pub broadcast proof fn axiom_u16_leading_zeros(i: u16)
298 ensures
299 0 <= #[trigger] u16_leading_zeros(i) <= 16,
300 i == 0 <==> u16_leading_zeros(i) == 16,
301 0 <= u16_leading_zeros(i) < 16 ==> (i >> sub(15u16, u16_leading_zeros(i) as u16)) & 1u16
303 != 0u16,
304 i >> sub(16, u16_leading_zeros(i) as u16) == 0,
306 forall|j: u16| 16 - u16_leading_zeros(i) <= j < 16 ==> #[trigger] (i >> j) & 1u16 == 0u16,
307 decreases i,
308{
309 assert(i / 2 == (i >> 1u16)) by (bit_vector);
310 assert(((i >> 1) >> sub(15u16, 0)) & 1u16 == 0u16) by (bit_vector);
311 let x = u16_leading_zeros(i / 2) as u16;
312 assert(i >> 0 == i) by (bit_vector);
313 assert(1u16 & 1u16 == 1u16) by (bit_vector);
314 assert(0 < x < 16 ==> ((i >> 1) >> sub(15u16, x)) == (i >> sub(15u16, sub(x, 1))))
315 by (bit_vector);
316 assert(0 < x <= 16 ==> (i >> 1) >> sub(16, x) == 0 ==> i >> sub(16, sub(x, 1)) == 0)
317 by (bit_vector);
318 if i != 0 {
319 axiom_u16_leading_zeros(i / 2);
320 }
321 assert forall|j: u16| 16 - u16_leading_zeros(i) <= j < 16 implies #[trigger] (i >> j) & 1u16
322 == 0u16 by {
323 let y = u16_leading_zeros(i) as u16;
324 assert(y <= 16 ==> i >> sub(16, y) == 0 ==> sub(16, y) <= j < 16 ==> (i >> j) & 1u16
325 == 0u16) by (bit_vector);
326 }
327}
328
329pub broadcast proof fn axiom_u16_leading_ones(i: u16)
330 ensures
331 0 <= #[trigger] u16_leading_ones(i) <= 16,
332 i == 0xffffu16 <==> u16_leading_ones(i) == 16,
333 0 <= u16_leading_ones(i) < 16 ==> (i >> sub(15u16, u16_leading_ones(i) as u16)) & 1u16
335 == 0u16,
336 (!i) >> sub(16, u16_leading_ones(i) as u16) == 0,
337 forall|j: u16| 16 - u16_leading_ones(i) <= j < 16 ==> #[trigger] (i >> j) & 1u16 == 1u16,
338{
339 axiom_u16_leading_zeros(!i);
340 assert(!0xffffu16 == 0) by (bit_vector);
341 assert(!i == 0 ==> i == 0xffffu16) by (bit_vector);
342 let x = u16_leading_ones(i) as u16;
343 assert(((!i) >> sub(15u16, x)) & 1u16 != 0u16 ==> (i >> sub(15u16, x)) & 1u16 == 0u16)
344 by (bit_vector);
345 assert forall|j: u16| 16 - u16_leading_ones(i) <= j < 16 implies #[trigger] (i >> j) & 1u16
346 == 1u16 by {
347 let y = u16_leading_ones(i) as u16;
348 assert(y <= 16 ==> (!i) >> sub(16, y) == 0 ==> sub(16, y) <= j < 16 ==> (i >> j) & 1u16
349 == 1u16) by (bit_vector);
350 }
351}
352
353pub closed spec fn u32_trailing_zeros(i: u32) -> u32
358 decreases i,
359{
360 if i == 0 {
361 32
362 } else if (i & 1) != 0 {
363 0
364 } else {
365 (1 + u32_trailing_zeros(i / 2)) as u32
366 }
367}
368
369pub closed spec fn u32_leading_zeros(i: u32) -> u32
372 decreases i,
373{
374 if i == 0 {
375 32
376 } else {
377 (u32_leading_zeros(i / 2) - 1) as u32
378 }
379}
380
381pub open spec fn u32_trailing_ones(i: u32) -> u32 {
384 u32_trailing_zeros(!i)
385}
386
387pub open spec fn u32_leading_ones(i: u32) -> u32 {
390 u32_leading_zeros(!i)
391}
392
393#[verifier::when_used_as_spec(u32_trailing_zeros)]
394pub assume_specification[ u32::trailing_zeros ](i: u32) -> (r: u32)
395 ensures
396 r == u32_trailing_zeros(i),
397;
398
399#[verifier::when_used_as_spec(u32_trailing_ones)]
400pub assume_specification[ u32::trailing_ones ](i: u32) -> (r: u32)
401 ensures
402 r == u32_trailing_ones(i),
403;
404
405#[verifier::when_used_as_spec(u32_leading_zeros)]
406pub assume_specification[ u32::leading_zeros ](i: u32) -> (r: u32)
407 ensures
408 r == u32_leading_zeros(i),
409;
410
411#[verifier::when_used_as_spec(u32_leading_ones)]
412pub assume_specification[ u32::leading_ones ](i: u32) -> (r: u32)
413 ensures
414 r == u32_leading_ones(i),
415;
416
417pub broadcast proof fn axiom_u32_trailing_zeros(i: u32)
418 ensures
419 0 <= #[trigger] u32_trailing_zeros(i) <= 32,
420 i == 0 <==> u32_trailing_zeros(i) == 32,
421 0 <= u32_trailing_zeros(i) < 32 ==> (i >> u32_trailing_zeros(i) as u32) & 1u32 == 1u32,
423 i << sub(32, u32_trailing_zeros(i) as u32) == 0,
425 forall|j: u32| 0 <= j < u32_trailing_zeros(i) ==> #[trigger] (i >> j) & 1u32 == 0u32,
426 decreases i,
427{
428 assert(i >> 0 == i) by (bit_vector);
429 assert(i << 0 == i) by (bit_vector);
430 assert(i & 0 == 0) by (bit_vector);
431 assert(i / 2 == (i >> 1u32)) by (bit_vector);
432 assert((i & 1) == 0 ==> i != 1) by (bit_vector);
433 let x = u32_trailing_zeros(i / 2) as u32;
434 assert(x < 32 ==> (i >> 1) >> x == (i >> add(x, 1))) by (bit_vector);
435 assert(i << 32 == 0) by (bit_vector);
436 assert(i & 1 != 0 ==> i & 1 == 1) by (bit_vector);
437 assert((i & 1) == 0 ==> (i >> 1) << sub(32, x) == 0 ==> i << sub(32, add(x, 1)) == 0)
438 by (bit_vector);
439 if i != 0 {
440 axiom_u32_trailing_zeros(i / 2);
441 }
442 assert forall|j: u32| 0 <= j < u32_trailing_zeros(i) implies #[trigger] (i >> j) & 1u32
443 == 0u32 by {
444 let y = u32_trailing_zeros(i) as u32;
445 assert(y <= 32 ==> i << sub(32, y) == 0 && 0 <= j < y ==> (i >> j) & 1u32 == 0u32)
446 by (bit_vector);
447 }
448}
449
450pub broadcast proof fn axiom_u32_trailing_ones(i: u32)
451 ensures
452 0 <= #[trigger] u32_trailing_ones(i) <= 32,
453 i == 0xffff_ffffu32 <==> u32_trailing_ones(i) == 32,
454 0 <= u32_trailing_ones(i) < 32 ==> (i >> u32_trailing_ones(i) as u32) & 1u32 == 0u32,
456 (!i) << sub(32, u32_trailing_ones(i) as u32) == 0,
458 forall|j: u32| 0 <= j < u32_trailing_ones(i) ==> #[trigger] (i >> j) & 1u32 == 1u32,
459{
460 axiom_u32_trailing_zeros(!i);
461 assert(!0xffff_ffffu32 == 0) by (bit_vector);
462 assert(!i == 0 ==> i == 0xffff_ffffu32) by (bit_vector);
463 let x = u32_trailing_ones(i) as u32;
464 assert(((!i) >> x) & 1u32 == 1u32 ==> (i >> x) & 1u32 == 0u32) by (bit_vector);
465 assert forall|j: u32| 0 <= j < u32_trailing_ones(i) implies #[trigger] (i >> j) & 1u32
466 == 1u32 by {
467 let y = u32_trailing_ones(i) as u32;
468 assert(y <= 32 ==> (!i) << sub(32, y) == 0 && 0 <= j < y ==> (i >> j) & 1u32 == 1u32)
469 by (bit_vector);
470 }
471}
472
473pub broadcast proof fn axiom_u32_leading_zeros(i: u32)
474 ensures
475 0 <= #[trigger] u32_leading_zeros(i) <= 32,
476 i == 0 <==> u32_leading_zeros(i) == 32,
477 0 <= u32_leading_zeros(i) < 32 ==> (i >> sub(31u32, u32_leading_zeros(i) as u32)) & 1u32
479 != 0u32,
480 i >> sub(32, u32_leading_zeros(i) as u32) == 0,
482 forall|j: u32| 32 - u32_leading_zeros(i) <= j < 32 ==> #[trigger] (i >> j) & 1u32 == 0u32,
483 decreases i,
484{
485 assert(i / 2 == (i >> 1u32)) by (bit_vector);
486 assert(((i >> 1) >> sub(31u32, 0)) & 1u32 == 0u32) by (bit_vector);
487 let x = u32_leading_zeros(i / 2) as u32;
488 assert(i >> 0 == i) by (bit_vector);
489 assert(1u32 & 1u32 == 1u32) by (bit_vector);
490 assert(0 < x < 32 ==> ((i >> 1) >> sub(31u32, x)) == (i >> sub(31u32, sub(x, 1))))
491 by (bit_vector);
492 assert(0 < x <= 32 ==> (i >> 1) >> sub(32, x) == 0 ==> i >> sub(32, sub(x, 1)) == 0)
493 by (bit_vector);
494 if i != 0 {
495 axiom_u32_leading_zeros(i / 2);
496 }
497 assert forall|j: u32| 32 - u32_leading_zeros(i) <= j < 32 implies #[trigger] (i >> j) & 1u32
498 == 0u32 by {
499 let y = u32_leading_zeros(i) as u32;
500 assert(y <= 32 ==> i >> sub(32, y) == 0 ==> sub(32, y) <= j < 32 ==> (i >> j) & 1u32
501 == 0u32) by (bit_vector);
502 }
503}
504
505pub broadcast proof fn axiom_u32_leading_ones(i: u32)
506 ensures
507 0 <= #[trigger] u32_leading_ones(i) <= 32,
508 i == 0xffff_ffffu32 <==> u32_leading_ones(i) == 32,
509 0 <= u32_leading_ones(i) < 32 ==> (i >> sub(31u32, u32_leading_ones(i) as u32)) & 1u32
511 == 0u32,
512 (!i) >> sub(32, u32_leading_ones(i) as u32) == 0,
513 forall|j: u32| 32 - u32_leading_ones(i) <= j < 32 ==> #[trigger] (i >> j) & 1u32 == 1u32,
514{
515 axiom_u32_leading_zeros(!i);
516 assert(!0xffff_ffffu32 == 0) by (bit_vector);
517 assert(!i == 0 ==> i == 0xffff_ffffu32) by (bit_vector);
518 let x = u32_leading_ones(i) as u32;
519 assert(((!i) >> sub(31u32, x)) & 1u32 != 0u32 ==> (i >> sub(31u32, x)) & 1u32 == 0u32)
520 by (bit_vector);
521 assert forall|j: u32| 32 - u32_leading_ones(i) <= j < 32 implies #[trigger] (i >> j) & 1u32
522 == 1u32 by {
523 let y = u32_leading_ones(i) as u32;
524 assert(y <= 32 ==> (!i) >> sub(32, y) == 0 ==> sub(32, y) <= j < 32 ==> (i >> j) & 1u32
525 == 1u32) by (bit_vector);
526 }
527}
528
529pub closed spec fn u64_trailing_zeros(i: u64) -> u32
534 decreases i,
535{
536 if i == 0 {
537 64
538 } else if (i & 1) != 0 {
539 0
540 } else {
541 (1 + u64_trailing_zeros(i / 2)) as u32
542 }
543}
544
545#[verifier::opaque]
548pub open spec fn u64_leading_zeros(i: u64) -> int
549 decreases i,
550{
551 if i == 0 {
552 64
553 } else {
554 u64_leading_zeros(i / 2) - 1
555 }
556}
557
558pub open spec fn u64_trailing_ones(i: u64) -> u32 {
561 u64_trailing_zeros(!i) as u32
562}
563
564pub open spec fn u64_leading_ones(i: u64) -> u32 {
567 u64_leading_zeros(!i) as u32
568}
569
570#[verifier::when_used_as_spec(u64_trailing_zeros)]
571pub assume_specification[ u64::trailing_zeros ](i: u64) -> (r: u32)
572 ensures
573 r == u64_trailing_zeros(i),
574;
575
576#[verifier::when_used_as_spec(u64_trailing_ones)]
577pub assume_specification[ u64::trailing_ones ](i: u64) -> (r: u32)
578 ensures
579 r == u64_trailing_ones(i),
580;
581
582pub assume_specification[ u64::leading_zeros ](i: u64) -> (r: u32)
584 ensures
585 r as int == u64_leading_zeros(i),
586;
587
588#[verifier::when_used_as_spec(u64_leading_ones)]
589pub assume_specification[ u64::leading_ones ](i: u64) -> (r: u32)
590 ensures
591 r == u64_leading_ones(i),
592;
593
594pub broadcast proof fn axiom_u64_trailing_zeros(i: u64)
595 ensures
596 0 <= #[trigger] u64_trailing_zeros(i) <= 64,
597 i == 0 <==> u64_trailing_zeros(i) == 64,
598 0 <= u64_trailing_zeros(i) < 64 ==> (i >> u64_trailing_zeros(i) as u64) & 1u64 == 1u64,
600 i << sub(64, u64_trailing_zeros(i) as u64) == 0,
602 forall|j: u64| 0 <= j < u64_trailing_zeros(i) ==> #[trigger] (i >> j) & 1u64 == 0u64,
603 decreases i,
604{
605 assert(i >> 0 == i) by (bit_vector);
606 assert(i << 0 == i) by (bit_vector);
607 assert(i & 0 == 0) by (bit_vector);
608 assert(i / 2 == (i >> 1u64)) by (bit_vector);
609 assert((i & 1) == 0 ==> i != 1) by (bit_vector);
610 let x = u64_trailing_zeros(i / 2) as u64;
611 assert(x < 64 ==> (i >> 1) >> x == (i >> add(x, 1))) by (bit_vector);
612 assert(i << 64 == 0) by (bit_vector);
613 assert(i & 1 != 0 ==> i & 1 == 1) by (bit_vector);
614 assert((i & 1) == 0 ==> (i >> 1) << sub(64, x) == 0 ==> i << sub(64, add(x, 1)) == 0)
615 by (bit_vector);
616 if i != 0 {
617 axiom_u64_trailing_zeros(i / 2);
618 }
619 assert forall|j: u64| 0 <= j < u64_trailing_zeros(i) implies #[trigger] (i >> j) & 1u64
620 == 0u64 by {
621 let y = u64_trailing_zeros(i) as u64;
622 assert(y <= 64 ==> i << sub(64, y) == 0 && 0 <= j < y ==> (i >> j) & 1u64 == 0u64)
623 by (bit_vector);
624 }
625}
626
627pub broadcast proof fn axiom_u64_trailing_ones(i: u64)
628 ensures
629 0 <= #[trigger] u64_trailing_ones(i) <= 64,
630 i == 0xffff_ffff_ffff_ffffu64 <==> u64_trailing_ones(i) == 64,
631 0 <= u64_trailing_ones(i) < 64 ==> (i >> u64_trailing_ones(i) as u64) & 1u64 == 0u64,
633 (!i) << sub(64, u64_trailing_ones(i) as u64) == 0,
635 forall|j: u64| 0 <= j < u64_trailing_ones(i) ==> #[trigger] (i >> j) & 1u64 == 1u64,
636{
637 axiom_u64_trailing_zeros(!i);
638 assert(!0xffff_ffff_ffff_ffffu64 == 0) by (bit_vector);
639 assert(!i == 0 ==> i == 0xffff_ffff_ffff_ffffu64) by (bit_vector);
640 let x = u64_trailing_ones(i) as u64;
641 assert(((!i) >> x) & 1u64 == 1u64 ==> (i >> x) & 1u64 == 0u64) by (bit_vector);
642 assert forall|j: u64| 0 <= j < u64_trailing_ones(i) implies #[trigger] (i >> j) & 1u64
643 == 1u64 by {
644 let y = u64_trailing_ones(i) as u64;
645 assert(y <= 64 ==> (!i) << sub(64, y) == 0 && 0 <= j < y ==> (i >> j) & 1u64 == 1u64)
646 by (bit_vector);
647 }
648}
649
650pub broadcast proof fn axiom_u64_leading_zeros(i: u64)
651 ensures
652 0 <= #[trigger] u64_leading_zeros(i) <= 64,
653 i == 0 <==> u64_leading_zeros(i) == 64,
654 0 <= u64_leading_zeros(i) < 64 ==> (i >> sub(63u64, u64_leading_zeros(i) as u64)) & 1u64
656 != 0u64,
657 i >> sub(64, u64_leading_zeros(i) as u64) == 0,
659 forall|j: u64| 64 - u64_leading_zeros(i) <= j < 64 ==> #[trigger] (i >> j) & 1u64 == 0u64,
660 decreases i,
661{
662 reveal(u64_leading_zeros);
663 assert(i / 2 == (i >> 1u64)) by (bit_vector);
664 assert(((i >> 1) >> sub(63u64, 0)) & 1u64 == 0u64) by (bit_vector);
665 let x = u64_leading_zeros(i / 2) as u64;
666 assert(i >> 0 == i) by (bit_vector);
667 assert(1u64 & 1u64 == 1u64) by (bit_vector);
668 assert(0 < x < 64 ==> ((i >> 1) >> sub(63u64, x)) == (i >> sub(63u64, sub(x, 1))))
669 by (bit_vector);
670 assert(0 < x <= 64 ==> (i >> 1) >> sub(64, x) == 0 ==> i >> sub(64, sub(x, 1)) == 0)
671 by (bit_vector);
672 if i != 0 {
673 axiom_u64_leading_zeros(i / 2);
674 }
675 assert forall|j: u64| 64 - u64_leading_zeros(i) <= j < 64 implies #[trigger] (i >> j) & 1u64
676 == 0u64 by {
677 let y = u64_leading_zeros(i) as u64;
678 assert(y <= 64 ==> i >> sub(64, y) == 0 ==> sub(64, y) <= j < 64 ==> (i >> j) & 1u64
679 == 0u64) by (bit_vector);
680 }
681}
682
683pub broadcast proof fn axiom_u64_leading_ones(i: u64)
684 ensures
685 0 <= #[trigger] u64_leading_ones(i) <= 64,
686 i == 0xffff_ffff_ffff_ffffu64 <==> u64_leading_ones(i) == 64,
687 0 <= u64_leading_ones(i) < 64 ==> (i >> sub(63u64, u64_leading_ones(i) as u64)) & 1u64
689 == 0u64,
690 (!i) >> sub(64, u64_leading_ones(i) as u64) == 0,
691 forall|j: u64| 64 - u64_leading_ones(i) <= j < 64 ==> #[trigger] (i >> j) & 1u64 == 1u64,
692{
693 axiom_u64_leading_zeros(!i);
694 assert(!0xffff_ffff_ffff_ffffu64 == 0) by (bit_vector);
695 assert(!i == 0 ==> i == 0xffff_ffff_ffff_ffffu64) by (bit_vector);
696 let x = u64_leading_ones(i) as u64;
697 assert(((!i) >> sub(63u64, x)) & 1u64 != 0u64 ==> (i >> sub(63u64, x)) & 1u64 == 0u64)
698 by (bit_vector);
699 assert forall|j: u64| 64 - u64_leading_ones(i) <= j < 64 implies #[trigger] (i >> j) & 1u64
700 == 1u64 by {
701 let y = u64_leading_ones(i) as u64;
702 assert(y <= 64 ==> (!i) >> sub(64, y) == 0 ==> sub(64, y) <= j < 64 ==> (i >> j) & 1u64
703 == 1u64) by (bit_vector);
704 }
705}
706
707pub broadcast group group_bits_axioms {
708 axiom_u8_trailing_zeros,
709 axiom_u8_trailing_ones,
710 axiom_u8_leading_zeros,
711 axiom_u8_leading_ones,
712 axiom_u16_trailing_zeros,
713 axiom_u16_trailing_ones,
714 axiom_u16_leading_zeros,
715 axiom_u16_leading_ones,
716 axiom_u32_trailing_zeros,
717 axiom_u32_trailing_ones,
718 axiom_u32_leading_zeros,
719 axiom_u32_leading_ones,
720 axiom_u64_trailing_zeros,
721 axiom_u64_trailing_ones,
722 axiom_u64_leading_zeros,
723 axiom_u64_leading_ones,
724}
725
726}