Document behavior of `shiftR a n` when `n > BitSize a` or negative

[martijnbastiaan]

shiftR's documentation:

Shift the first argument right by the specified number of bits. The result is undefined for negative shift amounts and shift amounts greater or equal to the bitSize. Some instances may throw an Overflow exception if given a negative input.

We have picked specific behavior:

• Undefined / errorX on negative shifts
• shiftR a n == shiftR a (BitSize a), for all n > BitSize a

Given that we can't really go back (at least according to my strong belief that API conserving behavioral changes are not-done), we should document this.

Edit: this should be done per-instance. I only looked at Unsigned :-).

[DigitalBrains1]

I think we should just explicitly say

• Unsigned, BitVector and Index: a `shiftR` n == 0, for all n >= BitSize a
• Signed:
  • a `shiftR` n == 0, for all a >= 0 and n >= BitSize a
  • a `shiftR` n == -1, for all a < 0 and n >= BitSize a

to take the guesswork (or experimentation) out. Per-instance, as you say, otherwise they could all be covered with just the statements for Signed, since a < 0 simply drops out for the other Num types we have.

PS: We could be more technically correct for Signed:

• a `shiftR` n == 0, for all a >= 0 and n >= BitSize a - 1
• a `shiftR` n == -1, for all a < 0 and n >= BitSize a - 1

since we already specify the MSB so the rule triggers even sooner, but I don't think this would actually improve the text.