Refinement logic pretends Int is infinite

[rrnewton]

I understand that this is a known limitation; nevertheless I thought there should be a place to discuss/comment on it and share any solutions you all might have planned.

Here's a concrete example. Liquid haskell (as of 4a489c9f3798), marks this as safe:

{-@ LIQUID "--higherorder"     @-}
{-@ LIQUID "--totality"        @-}
{-@ LIQUID "--prune-unsorted"  @-}
module OverflowTest where

{-@ incr :: x:Int -> { y:Int | y == x+1 && y > x } @-}
incr :: Int -> Int
incr = (+1)

But, naturally this is false, as incr maxBound is -9223372036854775808.

I don't know much about this, but this document seems to indicate there has been some previous work with Z3 and modular arithmetic ("bit vectors"?).

[nikivazou]

One clear disadvantage of bounding Ints is that you would need to guard all integer operations with overflow checks. For example, Haskell's (+) will not be mapped directly to the logical (+) but you will have to check for overflows.

Now we have

(+) :: x:Int -> y:Int -> {v:Int | v == x + y}

With overflow reasoning, the type of (+) will look like

(+) :: x:Int -> y:Int -> {v:Int | if v < maxBound then v == x + y else ...}

This gets quickly "imprecise" as to extract the result of n + m in the logic you should first prove that the "guard" (n + m < maxBound) is satisfied.

Not sure how this reasoning can lead to practical verification...

From a quick look at your Z3 link I quote Sec 11.4 "It is possible, but expensive, to integrate the theory of integers with bit-vectors. It is therefore turned off by default in Z3."

[TomMD]

What if we simply forbid any overflow? The user would still need to prove overflow doesn't occur but at least we wouldn't have to reason about the overflow case:

(+) :: x:Int -> y:Int -> {v:Int | v == x+y && v <= maxBound }

Or alternatively a precondition:

(+) :: x:Int -> {y:Int | y<= maxBound - x} -> {v:Int | v==x+y}

Has anyone gone through the exercise of using this type (taking care to reflect some maxBound value) and trying to push through the numerous case studies? It seems like a worthy exercise... though I don't think the case studies are synced up with liquidhaskell master branch at the moment.

[nikivazou]

Oh, actually, we had some nice progress on this issue...

Since numeric operators are basically haskell's instances of Num, you can have two instances:

• one that provably does not overflow (VerifiedNum)
• one that may overflow (Num to reduce proof obligations)

This idea is defined here

https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/todo/VerifiedNum.hs

and used in this example https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/pos/BinarySearchOverflow.hs

(No numeric studies are done, though definitely interesting)

[ranjitjhala]

Am preparing a proper writeup explanation of the above...

On Tue, Mar 7, 2017 at 3:05 AM, Niki Vazou notifications@github.com wrote:

Oh, actually, we had some nice progress on this issue...

Since numeric operators are basically haskell's instances of Num, you can have two instances:

• one that provably does not overflow (VerifiedNum)
• one that may overflow (Num to reduce proof obligations)

This idea is defined here

https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/todo/ VerifiedNum.hs

and used in this example https://github.com/ucsd- progsys/liquidhaskell/blob/develop/tests/pos/BinarySearchOverflow.hs

(No numeric studies are done, though definitely interesting)

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/827#issuecomment-284540436, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOBcx98dJmNTUbK81n2KmAFDt6LXAks5rjHwTgaJpZM4JzEwq .

[spacekitteh]

Isn't this the entire point of the distinction between Int and Integer, though? The efficiency increase of (usually, modulo boxing) using machine words comes at the expense of having to deal with overflow/underflow.

At the very least, there should be an option to treat Ints, etc as actual bitvectors (and IMO should be the default, but probably not straight away)

[nikivazou]

You are correct. In LH we just made the choice few years back to ignore overflows/underflows so that you have more precise functional correctness.

There is an option to use type classes to encode machine ints (https://ucsd-progsys.github.io/liquidhaskell-blog/2017/03/20/arithmetic-overflows.lhs/). Using bitvectors to encode machine ints is an interesting idea that we have not yet explored.

[ranjitjhala]

It would be nice to allow users to easily “override” the default specs in the LH prelude with different ones. We could then easily switch in overflow checking for example.

This is possible with the “assume” mechanism but would be nice to have it streamlined somehow...

On Mon, Dec 17, 2018 at 12:47 AM Niki Vazou notifications@github.com wrote:

You are correct. In LH we just made the choice few years back to ignore overflows/underflows so that you have more precise functional correctness.

There is an option to use type classes to encode machine ints ( https://ucsd-progsys.github.io/liquidhaskell-blog/2017/03/20/arithmetic-overflows.lhs/). Using bitvectors to encode machine ints is an interesting idea that we have not yet explored.

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/827#issuecomment-447765656, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOGqpsz_NJ3hcZjSueXSeQSrSe5kHks5u51oYgaJpZM4JzEwq .