Hi everyone. I'm starting to use the bbv library for bitvectors/machine words, and I'm wondering what would be the most natural way to use it to define a function that checks whether the n last bits of a word are 0 (ie check pointer alignment)? I stared for a while at the definitions the lib provides and couldn't find an easy way, but maybe I missed something obvious..?

Not an expert, but a naive version could be `weqb (x ^% $(pow2 n)) $0`

, I've managed to prove

```
Lemma wordToNat_mod_pow2l sz (x : word sz) n :
0 < n < sz ->
#(x ^% $(pow2 n)) = #(x) mod (pow2 n).
Proof.
intros nLsz.
assert (H : #(($(pow2 n) : word sz)) = pow2 n).
rewrite wordToNat_natToWord_2; auto.
apply pow2_inc; lia.
rewrite wordToNat_mod, H; auto.
intros H1; destruct (pow2_ne_zero n).
now rewrite <-H, H1, roundTrip_0.
Qed.
```

thanks! that looks very good indeed

Last updated: Jun 15 2024 at 05:01 UTC