Chapter 2 Issues

[hafizhmakmur]

There are some examples in Chapter 2 that is supposed to be safe but turns out it isn't. First I thought that it was only on my machine but it turns out it's deemed unsafe in the online demo too.

First, examples that really shouldn't be safe because of writer's logic error : {-@ ex7 :: Bool -> Bool -> TRUE @-} ex7 a b = a ==> (a ==> b) ==> b

{-@ ax3 :: Int -> Int -> TRUE @-} ax3 x y = (0 <= x) ==> (0 <= y) ==> (0 <= x + y)

{-@ ax5 :: Int -> Int -> Int -> TRUE @-} ax5 x y z = (x <= 0 && x >= 0) ==> (y == x + z) ==> (y == z)

They only work if one replace the first ==> with && because all of them are False if all parameters are False.

Second, almost all uninterpreted function example is somehow deemed unsafe by SMT Solver except fx0. It's very perplexing because it means somehow the entire section is wrong for some reason.

[ranjitjhala]

Hi! are you trying the online version or from the PDF or starter code? There are some “hidden” definitions that I think i should just expose for clarity. Still, can you let me know? Thanks!

On Mon, Feb 17, 2020 at 12:01 PM Hafizh Afkar Makmur < notifications@github.com> wrote:

There are some examples in Chapter 2 that is supposed to be safe but turns out it isn't. First I thought that it was only on my machine but it turns out it's deemed unsafe in the online demo too.

First, examples that really shouldn't be safe because of writer's logic error : {-@ ex7 :: Bool -> Bool -> TRUE @-} ex7 a b = a ==> (a ==> b) ==> b

{-@ ax3 :: Int -> Int -> TRUE @-} ax3 x y = (0 <= x) ==> (0 <= y) ==> (0 <= x + y)

{-@ ax5 :: Int -> Int -> Int -> TRUE @-} ax5 x y z = (x <= 0 && x >= 0) ==> (y == x + z) ==> (y == z)

They only work if one replace the first ==> with && because all of them are False if all parameters are False.

Second, almost all uninterpreted function example is somehow deemed unsafe by SMT Solver except fx0. It's very perplexing because it means somehow the entire section is wrong for some reason.

— 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-tutorial/issues/90?email_source=notifications&email_token=AAMS4OAMB4ALXCEFFXWOAYTRDLUJNA5CNFSM4KWXWBBKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4IOEAHWA, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAMS4OCUWK5WNIYM2ZWBGN3RDLUJNANCNFSM4KWXWBBA .

[hafizhmakmur]

First, thank you very much for answering. I very appreciate it.

Second, I mostly follow this tutorial . I've learnt to include some definitions to make the program work, if that's what you meant by "hidden" definitions, and it worked well so far. Except in examples I have mentioned of course.

logic.txt Here is my code so far. Tell me if I'm doing something wrong. Mostly, it's just copy pasting the code for testing if SMT Solver really works.

[ranjitjhala]

Hi @hafizhmakmur -- sorry for the delay just took a look. See this:

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1581980818_5067.hs

The main problem was that you missed the (hidden) GHC annotation

infixr 9 ==>

which is needed so that an expression e1 => e2 => e3 is parsed as e1 => (e2 => e3) (and not (e1 => e2) => e3). With this change, ex7, ax3, and ax5 work as written.

The issue with the uninterpreted examples is that we made a change in the defaults, so we really need to add the line {-@ LIQUID "--reflection" @-} to the preamble. My apologies for this, but I hope this gets you unstuck!

[hafizhmakmur]

Thank you very much ! It really works! Yeah, you should really add all of these somewhere in the tutorial lol :D . Once again thank you very much for your quick assistance!

[ranjitjhala]

Yes, I updated it in the source -- thanks for pointing it out, and apologies again!

https://github.com/ucsd-progsys/liquidhaskell-tutorial/blob/master/src/02-logic.lhs

On Mon, Feb 17, 2020 at 3:18 PM Hafizh Afkar Makmur < notifications@github.com> wrote:

Thank you very much ! It really works! Yeah, you should really add all of these somewhere in the tutorial lol :D . Once again thank you very much for your quick assistance!

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/90?email_source=notifications&email_token=AAMS4OHKLYHZ7DVYQRZBEGLRDMLMNA5CNFSM4KWXWBBKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEL74MBA#issuecomment-587187716, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAMS4OEXS4XDMTDX5FX5QB3RDMLMNANCNFSM4KWXWBBA .

[hafizhmakmur]

Eh, by the way, @ranjitjhala, for some reason fx2 is still unsafe despite all other functions are now working. Is there anything else I missed so far? It looks like it should've worked but it doesn't.

[hafizhmakmur]

Nevermind, there's this cheeky {-@ size :: [a] -> Nat @-} right after {-@ measure size @-} that fixes it lol. I really missed something :D .

[ranjitjhala]

Yes the Nat says that “size” is nonnegative which is needed for those examples :-)

On Mon, Feb 17, 2020 at 3:41 PM Hafizh Afkar Makmur < notifications@github.com> wrote:

Nevermind, there's this cheeky {-@ size :: [a] -> Nat @-} right after {-@ measure size @-} that fixes it lol. I really missed something :D .

— You are receiving this because you were mentioned.

Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/90?email_source=notifications&email_token=AAMS4OD6RUFZUS5H2REPLYLRDMODJA5CNFSM4KWXWBBKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEMAAYNQ#issuecomment-587205686, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAMS4ODMRTZDQUDDJJVPRGTRDMODJANCNFSM4KWXWBBA .