reflection of quot and rem

[ninioArtillero]

This PR aims to fix #1447

I start by adding a negative test showing the offending behavior.
It is on /test/reflect/neg/, but welcome suggestions if there is a more appropriate place.

A lead: both quot and rem functions are opaque-reflected, while div and mod are not.

[ninioArtillero]

I implemented quot and rem in the refinement logic and added define abs x = if x >= 0 then x else -x to src/GHC/Num_LHAssumptions.hs.
I think the implementation of both are correct, but still need to verify it. how should I go about it? Should I implement some unit tests? If so, where?

Also, I'm still to run all tests to look for regressions (or does ci/circleci does this already?).

[facundominguez]

Thanks @ninioArtillero. CI might catch some regressions indeed. For tests, you could add a module under "tests/" with concrete examples like

{-@ exQuot1 :: { -2 = quot -5 2 } @-}
exQuot1 :: ()
exQuot1 = ()

and/or create a testsuite in the liquidhaskell package for property based tests.

[ninioArtillero]

For the second option, you mean something like what I just pushed? I would add all the properties as post-conditions of that same function.

[facundominguez]

For the second option, you mean something like what I just pushed? I would add all the properties as post-conditions of that same function.

Not really. It would have to be a test suite using QuickCheck, to test for the equivalence of quot and rem in Haskell and in the logic. But we can skip this and just stick with a module under tests/.

[ninioArtillero]

Not really. It would have to be a test suite using QuickCheck, to test for the equivalence of quot and rem in Haskell and in the logic. But we can skip this and just stick with a module under tests/.

I have played around with QuickCheck and think I can implement the tests. As there are no custom data types involved, guess it should not be much of a problem.

[ninioArtillero]

I implemented quotRem in terms of divMod in the test-suite to test the implementation of quot and rem at src/GHC/Real_LHAssumptions.hs (kind of a inverse-reflect experiment). QuickCheck tests suggest implementation is correct.

Nevertheless, I found some specific cases that prevented verification of my original reflect-pos test, and I think I have found a bug: logic / and mod don´t behave as Haskell's div and mod when both arguments are negative as implied by the existing defines at said module.

[facundominguez]

Bravo @ninioArtillero! Here go some comments.

[facundominguez]

This is a good observation. In Haskell QuickCheck is used with tasty and tasty-quickcheck or similar scaffolding for tests.

I've found these tests can be integrated in tests:test:tasty. It is a testsuite inside the tests package. If you want, you can look into that. Otherwise I could do it too.

[ninioArtillero]

I could look into that after having my test pass LH verification.

[ninioArtillero]

Used an alternative implementation proposed by @facundominguez that uses an explicit termination metric to make verification pass. Now both the property tests and LH verification pass, so we can be confident that the logic implementation of quot and rem is fine.

But the lemmaQuotRem at the reflect-pos test is complaining, even though the test examples work ok 😣

[ninioArtillero]

The regression was introduced at 7b648be9e where the definition of quot and rem at src/GHC/Real_LHAssumptions.hs was changed to the match the implementation proved correct at the test/QuotRem.

[facundominguez]

I'm setting up to merge. We need an issue to investigate the negative test.

Thanks @ninioArtillero!

[facundominguez]

hm, the neg test started failing after 280c0e1. I thought I had tested that before.