Specification of div seems to be incorrect

[facundominguez]

The following example doesn't go well

iterateTo0 :: Int -> Int
iterateTo0 0 = 0
iterateTo0 n = iterateTo0 (div n 2)

main :: IO ()
main = print $ iterateTo0 (-1)

It passes verification, but then fails to terminate.

I think the problem might be that the specification of div uses real division where integer division is expected.

[nikivazou]

This specification was written for div on Reals this is why the filename has Real. If I recall correctly, there was a different one for the integer division.

[facundominguez]

div comes from GHC.Real.

ghci> :i div
type Integral :: * -> Constraint
class (Real a, Enum a) => Integral a where
  ...
  div :: a -> a -> a
  ...
  	-- Defined in ‘GHC.Real’
infixl 7 `div`

but it seems to be instantiated only with types that need integer division.

ghci> :i GHC.Real.Integral
type Integral :: * -> Constraint
class (Real a, Enum a) => Integral a where
  ...
  div :: a -> a -> a
  ...
  {-# MINIMAL quotRem, toInteger #-}
  	-- Defined in ‘GHC.Real’
instance Integral Int -- Defined in ‘GHC.Real’
instance Integral Integer -- Defined in ‘GHC.Real’
instance Integral Word -- Defined in ‘GHC.Real’

[ranjitjhala]

Good catch @facundominguez !!! Specifically the clause on line 27

liquidhaskell/src/GHC/Real_LHAssumptions.hs

Line 27 in 5fbff05

((1 < y) => v < x ) &&

Is wrong: the output is only < x if 0 < x

We should have quickchecked these specs!