Concrete backend and reference evaluator have different `Integer` division semantics

[RyanGlScott]

The following Cryptol session computes the same expression involving integer division twice, once using the concrete backend and once again using the reference evaluator (:eval). I'd expect to get the same answer both times, but they instead return different answers:

Cryptol> (7 : Integer) / (-2 : Integer)
-4
Cryptol> :eval (7 : Integer) / (-2 : Integer)
-3

[RyanGlScott]

They also disagree on the semantics of (%) for Integers:

Cryptol> (7 : Integer) % (-2 : Integer)
-1
Cryptol> :eval (7 : Integer) % (-2 : Integer)
1

[RyanGlScott]

For prior art, see #662 and GaloisInc/saw-script#2415. Based on these discussions, I believe that the reference interpreter is computing things incorrectly.

[RyanGlScott]

The relevant code in the reference interpreter is:

cryptol/src/Cryptol/Eval/Reference.lhs

Line 726 in bccdc96

> , "/" ~> binary (integralBinary divWrap)

Where:

cryptol/src/Cryptol/Eval/Reference.lhs

Lines 1365 to 1372 in bccdc96

	> integralBinary ::
	> (Integer -> Integer -> E Integer) ->
	> TValue -> E Value -> E Value -> E Value
	> integralBinary op ty x y = case ty of
	> TVInteger ->
	> VInteger <$> appOp2 op (fromVInteger <$> x) (fromVInteger <$> y)
	> TVSeq w a | isTBit a ->
	> vWord w <$> appOp2 op (fromVWord =<< x) (fromVWord =<< y)

cryptol/src/Cryptol/Eval/Reference.lhs

Lines 1390 to 1392 in bccdc96

	> divWrap :: Integer -> Integer -> E Integer
	> divWrap _ 0 = cryError DivideByZero
	> divWrap x y = pure (x `quot` y)

Note that integralBinary is applying quot for Integers, which is wrong. We should be applying div on Integers, similarly to how the concrete backend does it:

cryptol/src/Cryptol/Eval/Generic.hs

Lines 510 to 515 in bccdc96

	{-# INLINE divV #-}
	divV :: Backend sym => sym -> Binary sym
	divV sym = integralBinary sym opw opi
	where
	opw _w x y = wordDiv sym x y
	opi x y = intDiv sym x y

cryptol/src/Cryptol/Backend/Concrete.hs

Lines 327 to 329 in bccdc96

	intDiv sym x y =
	do assertSideCondition sym (y /= 0) DivideByZero
	pure $! x `div` y

[RyanGlScott]

I originally opened #2061 with the intention of changing the reference evaluator to match what the concrete and symbolic backends do. But the discussion on that pull request revealed that the concrete/symbolic backends' implementation of (/)/(%) (i.e., div/mod semantics) is quite surprising anyway, and we really ought to change them to use quot/rem semantics instead. As it turns out, the reference evaluator is using quot/rem semantics, which means that we really need to do things the other way around. That is: keep the reference evaluator the same, but change the semantics of the concrete/symbolic backends (as well as SAW) to use quot/rem instead of div/mod.

Note that:

• For non-negative integers, this change in semantics would have no effect---this only affects what answers you get with negative integers. The change in semantics is a bit unfortunate, but we hope that for the most part, this is a corner case that won't affect too many peoples' workflows.
• We originally wondered if we should expose two division operators for Integers: one which uses quot/rem semantics, and another which uses div/mod semantics. After further discussion, however, we decided against this. Note that div/mod semantics can be defined in terms of quot/rem semantics, so it would be worth including a test case which does this for the sake of completeness.