Proof backend and concrete evaluation disagree about signed shift

[brianhuffman]

Main> :prove \(x:[8]) -> x >>$ 0x00 == x
Q.E.D.
(Total Elapsed Time: 0.008s, using Z3)
Main> :check \(x:[8]) -> x >>$ 0x00 == x
Using exhaustive testing.
(\(x : [8]) -> x >>$ 0x00 == x) 0x80 = False
Main> 0x80 >>$ 0x00
0xff

Concrete evaluation is wrong here.

[brianhuffman]

Cryptol> :exhaust \(x:[8]) (y:[8]) -> x >= 0x80 ==> x >>$ y == 0xff
Using exhaustive testing.
Passed 65536 tests.
Q.E.D.

[brianhuffman]

The problem was introduced in revision 4d974fe, "Fix bugs in the signed right shift operation."

In particular, the local definition of negv is wrong, because it always evaluates to -1.

cryptol/src/Cryptol/Prims/Eval.hs

Lines 673 to 683 in c859570

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

[brianhuffman]

The SMTLib standard (http://smtlib.cs.uiowa.edu/logics-all.shtml) defines signed right shift in terms of logical (unsigned) right shift:

    (bvashr s t) abbreviates 
      (ite (= ((_ extract |m-1| |m-1|) s) #b0)
           (bvlshr s t)
           (bvnot (bvlshr (bvnot s) t)))

I propose that we define it the same way in the Cryptol prelude.

x >>$ y = if head x then ~ (~ x >> y) else x >> y

Then we don't have to worry about implementing it correctly as a primitive.

[brianhuffman]

Now that I think about it, it might be nice to keep >>$ as a primitive in Cryptol. The reason is that there is a signed-right-shift primitive in some of the Cryptol backends (e.g. what4 and saw-core), and it would be nice to be able to build expressions involving those primitives in those backends.

So maybe we should close #665 without merging, and just fix the broken implementations and add regression tests to ensure that they match the cryptol definition I suggested.