Signed-right-shift with large shift amounts gives wrong result

[brianhuffman]

The signed right shift operator (>>$) produces the wrong result when given a shift amount too large to fit in a Haskell Int (2^63 or higher).

Cryptol> 0x55 >>$ 0x8000000000000000
0x55

Both the concrete and symbolic evaluation backends have this problem:

Cryptol> :prove \(x:[8]) -> x >>$ 0x8000000000000000 == x
Q.E.D.
(Total Elapsed Time: 0.008s, using "Z3")
Cryptol> :exhaust \(x:[8]) -> x >>$ 0x8000000000000000 == x
Using exhaustive testing.
Passed 256 tests.
Q.E.D.

Here is the offending function from the concrete backend. It includes an unsafe use of fromInteger (#637).

cryptol/src/Cryptol/Eval/Concrete.hs

Lines 279 to 288 in 7e841e9

	sshrV :: Value
	sshrV =
	nlam $ \_n ->
	nlam $ \_k ->
	wlam Concrete $ \(BV i x) -> return $
	wlam Concrete $ \y ->
	let signx = testBit x (fromInteger (i-1))
	amt = fromInteger (bvVal y)
	x' = if signx then x - bit (fromInteger i) else x
	in return . VWord i . ready . WordVal . mkBv i $! x' `shiftR` amt

[brianhuffman]

The situation is a bit complicated in the symbolic backend. It appears that the bug only shows up when the shift amount is concrete.

Cryptol> :prove \(i:[64]) -> (0x55 >>$ i == 0x55) == (i == 0)
Q.E.D.
(Total Elapsed Time: 0.010s, using "Z3")

[robdockins]

Fixed via #724.