bulky representation of concrete words

[aa755]

Because of indices (which nest), every concrete 64 bit word has 2080 S constructors, even though it has only 64 WS constructors. Should we opt for a less intrinisically dependently typed variant like Word s := {n:N | log n< s}?

Fixpoint sumFirstN (n : nat) : nat :=
match n with
| O => O
| S n => (S n) + (sumFirstN n)
end.

Eval compute in (sumFirstN 64)

[gmalecha]

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

[samuelgruetter]

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 :wink: