[saw-core-coq] Check bitvector lemmas for < 4 bits

[m-yac]

Inspired by @robdockins' comment in #1236, this PR adds the axiom:

Axiom holds_up_to_4 : forall (P : nat -> Prop),
                      P 0 -> P 1 -> P 2 -> P 3 -> P 4 ->
                      forall n, P n.

and uses it instead of Admitted to ensure that the bitvector propositions in SAWCoreBitvectors.v at least work for inputs with less than four bits. In the process, this PR fixes a few incorrect bitvector propositions (namely, Preorder_isBvslt, Preorder_isBvult, isBvsle_suc_r, and bvNeg_msb).

This is quick way to gain some confidence in the existing lemmas, not a long-term solution. To reinforce that, the tactic holds_for_bits_up_to_4, which tries to prove a lemma using the above axiom, prints out a warning each time it is used.

This PR also fixes the definition of shiftR, as noticed in #1236.

This is a draft because I still need to either fix or remove bvslt_bvSub_r and bvslt_bvSub_l, and have yet to update the heapster example proofs.

[robdockins]

Yeah, that's more or less what I had in mind. It's a touch disappointing it starts to slow down too much beyond 4 bits, but that is probably enough to catch most of the problematic corner cases and such.

[jpaykin]

Looks good! I think size-3 or 4 bitvectors should be fine for the types of lemmas you have here. If you really did want to scale to larger dimensions, I could suggest 2 things... (1) instead of dependent destruction, just enumerate all the n-digit bitvectors. I'm not sure if this would be faster but it's a possibility; (2) use something like quickchick (https://github.com/QuickChick/QuickChick) to randomly test inputs at larger dimensions, instead of enumerating all of them.

[m-yac]

Thanks Rob and Jen. I got the Heapster examples working again with these new lemmas, so this should be ready to merge now.

Note that I updated all the checks to only go up to 3 bits, for the sake of performance (checking SAWCoreBitvectors.v now takes 35s instead of 72s on my machine). I did this after realizing that every time either the saw-core prelude or the proof automation changes, this file would need to be recompiled – so it would be nice if it didn't take over a minute to check every time.

If this idea ends up being more permanent, we should definitely look into implementing your suggestions @jpaykin.