Stream: Coq users

Topic: bbv library: defining an alignment check

Armaël Guéneau (May 10 2021 at 16:32):

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..?

Laurent Théry (May 11 2021 at 15:18):

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.

Armaël Guéneau (May 12 2021 at 08:35):

thanks! that looks very good indeed

Last updated: Oct 13 2024 at 01:02 UTC