bulky representation of concrete words about bbv HOT 2 OPEN

I'm in favor of this. See the discussion in #21

from bbv.

I already did this for riscv-coq, see here.

I use the following representation:

  Record word_record{sz: Z} := Build_word {
    word_val: Z;
    word_mod: word_val mod 2 ^ sz = word_val
  }.

It seems to work well in the sense that I use it everywhere in riscv-coq and in bedrock2, without any problems.

If you want to use that too, we should incorporate this into bbv, PRs welcome 😉

from bbv.