vstd/std_specs/
bits.rs

1use super::super::prelude::*;
2
3verus! {
4
5// TODO mark the lemmas as not external_body when it's supported
6// along with broadcast_forall
7///////////////////////////
8/////////////////////////// For u8
9/// Equivalent to `i.trailing_zeros()`.
10/// See [`axiom_u8_trailing_zeros`] for useful properties.
11pub 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
23/// Equivalent to `i.leading_zeros()`.
24/// See [`axiom_u8_leading_zeros`] for useful properties.
25pub 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
35/// Equivalent to `i.trailing_ones()`.
36/// See [`axiom_u8_trailing_ones`] for useful properties.
37pub open spec fn u8_trailing_ones(i: u8) -> u32 {
38    u8_trailing_zeros(!i)
39}
40
41/// Equivalent to `i.leading_ones()`.
42/// See [`axiom_u8_leading_ones`] for useful properties.
43pub 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        // i^th bit is 1
76        0 <= u8_trailing_zeros(i) < 8 ==> (i >> u8_trailing_zeros(i) as u8) & 1u8 == 1u8,
77        // trailing bits are 0
78        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        // i^th bit is 0
108        0 <= u8_trailing_ones(i) < 8 ==> (i >> u8_trailing_ones(i) as u8) & 1u8 == 0u8,
109        // trailing bits are 1
110        (!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        // i^th bit from the left is 1
130        0 <= u8_leading_zeros(i) < 8 ==> (i >> sub(7u8, u8_leading_zeros(i) as u8)) & 1u8 != 0u8,
131        // leading bits are 0
132        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        // i^th bit from the left is 0
160        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
177///////////////////////////
178/////////////////////////// For u16
179/// Equivalent to `i.trailing_zeros()`.
180/// See [`axiom_u16_trailing_zeros`] for useful properties.
181pub 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
193/// Equivalent to `i.leading_zeros()`.
194/// See [`axiom_u16_leading_zeros`] for useful properties.
195pub 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
205/// Equivalent to `i.trailing_ones()`.
206/// See [`axiom_u16_trailing_ones`] for useful properties.
207pub open spec fn u16_trailing_ones(i: u16) -> u32 {
208    u16_trailing_zeros(!i)
209}
210
211/// Equivalent to `i.leading_ones()`.
212/// See [`axiom_u16_leading_ones`] for useful properties.
213pub 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        // i^th bit is 1
246        0 <= u16_trailing_zeros(i) < 16 ==> (i >> u16_trailing_zeros(i) as u16) & 1u16 == 1u16,
247        // trailing bits are 0
248        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        // i^th bit is 0
279        0 <= u16_trailing_ones(i) < 16 ==> (i >> u16_trailing_ones(i) as u16) & 1u16 == 0u16,
280        // trailing bits are 1
281        (!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        // i^th bit from the left is 1
302        0 <= u16_leading_zeros(i) < 16 ==> (i >> sub(15u16, u16_leading_zeros(i) as u16)) & 1u16
303            != 0u16,
304        // leading bits are 0
305        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        // i^th bit from the left is 0
334        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
353///////////////////////////
354/////////////////////////// For u32
355/// Equivalent to `i.trailing_zeros()`.
356/// See [`axiom_u32_trailing_zeros`] for useful properties.
357pub 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
369/// Equivalent to `i.leading_zeros()`.
370/// See [`axiom_u32_leading_zeros`] for useful properties.
371pub 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
381/// Equivalent to `i.trailing_ones()`.
382/// See [`axiom_u32_trailing_ones`] for useful properties.
383pub open spec fn u32_trailing_ones(i: u32) -> u32 {
384    u32_trailing_zeros(!i)
385}
386
387/// Equivalent to `i.leading_ones()`.
388/// See [`axiom_u32_leading_ones`] for useful properties.
389pub 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        // i^th bit is 1
422        0 <= u32_trailing_zeros(i) < 32 ==> (i >> u32_trailing_zeros(i) as u32) & 1u32 == 1u32,
423        // trailing bits are 0
424        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        // i^th bit is 0
455        0 <= u32_trailing_ones(i) < 32 ==> (i >> u32_trailing_ones(i) as u32) & 1u32 == 0u32,
456        // trailing bits are 1
457        (!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        // i^th bit from the left is 1
478        0 <= u32_leading_zeros(i) < 32 ==> (i >> sub(31u32, u32_leading_zeros(i) as u32)) & 1u32
479            != 0u32,
480        // leading bits are 0
481        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        // i^th bit from the left is 0
510        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
529///////////////////////////
530/////////////////////////// For u64
531/// Equivalent to `i.trailing_zeros()`.
532/// See [`axiom_u64_trailing_zeros`] for useful properties.
533pub 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/// Equivalent to `i.leading_zeros()`.
546/// See [`axiom_u64_leading_zeros`] for useful properties.
547#[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
558/// Equivalent to `i.trailing_ones()`.
559/// See [`axiom_u64_trailing_ones`] for useful properties.
560pub open spec fn u64_trailing_ones(i: u64) -> u32 {
561    u64_trailing_zeros(!i) as u32
562}
563
564/// Equivalent to `i.leading_ones()`.
565/// See [`axiom_u64_leading_ones`] for useful properties.
566pub 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
582//#[verifier::when_used_as_spec(u64_leading_zeros)]
583pub 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        // i^th bit is 1
599        0 <= u64_trailing_zeros(i) < 64 ==> (i >> u64_trailing_zeros(i) as u64) & 1u64 == 1u64,
600        // trailing bits are 0
601        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        // i^th bit is 0
632        0 <= u64_trailing_ones(i) < 64 ==> (i >> u64_trailing_ones(i) as u64) & 1u64 == 0u64,
633        // trailing bits are 1
634        (!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        // i^th bit from the left is 1
655        0 <= u64_leading_zeros(i) < 64 ==> (i >> sub(63u64, u64_leading_zeros(i) as u64)) & 1u64
656            != 0u64,
657        // leading bits are 0
658        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        // i^th bit from the left is 0
688        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} // verus!