Building theories/Word.vo is slow about bbv HOT 9 OPEN

I think splitting would be an excellent thing to do! How about this:

File WordDefs.v:

Module Word.
   (* all word definitions *)
End Word.

File WordLib.v:

Module Word.
   (* all word lemmas *)
End Word.

File Word.v:

Require Export bbv.WordDef.
Require Export bbv.WordLib.

This (or a similar thing) should be very straightforward, and we should do it now. @JasonGross would you mind submitting a PR for this which works with your fiat-crypto requirements?

After that, we should also talk about how to make the proofs faster, which might also require some redesign, maybe like what I did in riscv-coq's Word.v

from bbv.

Would it be desirable to define a module type that defines the type, the operations, and the properties as axioms and then make different instantiations? If there is a small set of axioms that can be used to derive other theorems, then things should be able to be proved generically.

All that said, I'm not sure if there would be a huge benefit to having multiple implementations.

from bbv.

I don't think there's much value in having multiple implementations at the same time, but there is value in having small interfaces between the "data representation" of word and the lemmas about words, because it simplifies proofs.

The interface I'd propose to use is the following:

Module Type WORD.

  Parameter word: Z -> Set.

  Parameter ZToWord: forall (sz: Z) (x: Z), word sz.

  Parameter uwordToZ: forall {sz: Z} (w: word sz), Z.

  Axiom uwordToZ_ZToWord: forall sz n,
    uwordToZ (ZToWord sz n) = n mod 2 ^ sz.

  Axiom ZToWord_uwordToZ: forall {sz: Z} (a : word sz),
    ZToWord sz (uwordToZ a) = a.

End WORD.

As you can see here, even though this interface is very small, it allows us to define all operations on words we want, and prove all lemmas we want in a much more principled way.

This abstraction allowed me to replace the data representation { x: Z | x mod 2 ^ sz = x } by bbv.Word.word very easily.

However, I would not want to use opaque module type ascription, because then cbv on words would not work any more.

from bbv.

from bbv.

from bbv.

@samuelgruetter My other question is about the use of Z as the model rather than N (this is independent of my above question about the index being Z rather than N or nat). From what I can see, all the definitions on Z seem to make pretty arbitrary definitions for negative numbers, e.g. if z is negative than forall n, testbit z n = false. In addition, it also seems like it would be nice to have both a signed and an unsigned models, where the signed model maps as_signed : word n -> Z and forall w, -(2^(n-1)) <= as_signed w < 2^(n-1).

What about operations such as rotate? Would you want to define those operations in the same way? I.e. by implementing them on Z (or N)?

I'm not sure how expediant it would be, but given that it is a bitvector library, perhaps it makes sense to expose the bits in the interface (in a primitive way) and provide numeric interpretations as derived concepts (or as primitive ones if it makes the proofs easier). This wouldn't prevent us from using N as an implementation or a specification.

Concretely, I guess I'm proposing the following interface (which is morally similar to your, though larger).

Parameter word : nat -> Set.

(* the bitvector interface (accessing bits, useful for defining concat, slice, etc.) *)
Parameter bit : forall sz, word sz -> fin sz -> bool. (* could also use nat or N instead of `fin sz` *)

(* the unsigned model (your interface with Z replaced with N) *)
Parameter of_N : forall {sz}, N -> word sz.
Parameter to_N : forall {sz}, word sz -> N.
Axiom of_N_to_N : forall sz (w : word sz), of_N (to_N w) = w.
Axiom to_N_of_N : forall sz (n : N), to_N (of_N n) = n mod 2^sz.

(* the signed interface (for 2s-complement) *)
Definition representableZ (sz : nat) (z : Z) : Prop := -(2^(sz-1)) <= z < 2^(sz-1).
Parameter of_Z : forall {sz}, Z -> word sz.
Parameter to_Z : forall {sz}, word sz -> Z.
Axiom of_Z_to_Z : forall sz (w : word sz), of_Z (to_Z w) = w.
Axiom to_Z_of_Z : forall sz (z : Z), representableZ sz z -> to_Z (of_Z z) = z. (* maybe you need something stronger than this? *)

from bbv.

From what I can see, all the definitions on Z seem to make pretty arbitrary definitions for negative numbers,

The arithmetic operations are sensibly defined (with the caveat that Z.pow takes the floor rather than giving Q), and the bitwise operations use an infinite twos-complement representation. The only arbitrary choices I'm aware of are things like Z.log2 (I can't recall if it gives 0 or -1) and things where a Z is used as an index, if there are such, in which case negative indices are treated as invalid, whatever that means for the given operation (I think this is where your testbit behavior comes from). Oh, and having a negative number as a modulus is also sort-of strange, and I think there's an arbitrary choice made there.

from bbv.

Thanks for the insights, @JasonGross. I assume the choices for Z were made so that everything fits together during typing, e.g. z^i^-i is well typed (even though it isn't always equal to z). I think switching to N gives us all the properties we want without needing to worry about the side-conditions.

from bbv.

I think the main reason for using Z is that there are much more lemmas and tactics for Z than there are for N.

from bbv.