crash: SMTLIB2 on ple

[mystaroll]

Hi guys, PLE fails on this for some reason:

{-@ LIQUID "--reflection"    @-}
{-@ LIQUID "--ple-local"    @-}

-- anyM is just Prelude's `any` but lifted to LH
{-@ reflect anyM @-}
anyM :: (a -> Bool) -> [a] -> Bool
anyM _ []        = False
anyM p (x:xs)    = p x || anyM p xs 

{-@ reflect asd @-}
asd :: Int -> [Int] -> Bool
asd a b = anyM (\x -> a == x) b

{-@ ple pr @-}
{-@ pr :: { asd 1 [1] } @-}
pr = ()

LH says:

:1:1-1:1: Error
  crash: SMTLIB2 respSat = Error "line 4415 column 23: unknown constant x$35$$35$auns"

[mystaroll]

Modifying asd to this:

{-@ reflect asd @-}
asd :: Int -> [Int] -> Bool
asd a b = anyM (a ==) b

takes away the crash, however it cannot prove this triviality:

{-@ ple pr @-}
{-@ pr :: { asd 1 [1] } @-}
pr = asd 1 [1]
  ===  anyM (1 ==) [1] --asd definition
    ***QED

Any help would be appreciated 🙏

[ranjitjhala]

Support for lambdas is super flaky; can you hoist out to a top level def and see if that helps?

[mystaroll]

It works for the example I posted above, however my real use case is something like this :disappointed: :

import Language.Haskell.Liquid.ProofCombinators

{-@ LIQUID "--ple-local" @-}
{-@ LIQUID "--reflection" @-}

data CList a = Empty
             | CList [a] a [a]

{-@ reflect singleton @-}
singleton :: a -> CList a
singleton e = CList [] e [] 

{-@ reflect toList @-}
toList :: CList a -> [a]
toList Empty = []
toList (CList l f r) = f : (r ++ (reverse l))

{-@ reflect eqToList @-}
eqToList ::  CList Int -> CList Int -> Bool
eqToList a b = toList a == toList b

{-@ reflect =*= @-}
{-@ infix 4 =*= @-}
(=*=) :: CList Int -> CList Int -> Bool
x =*= y = (any (eqToList x) (toList (singleton y)))

{-@ reflect lemma_refl @-}
lemma_refl :: Bool
lemma_refl = Empty =*= Empty

{-@ ple lemma_refl_proof @-}
{-@ lemma_refl_proof ::  { lemma_refl  } @-}
lemma_refl_proof :: Proof
lemma_refl_proof = lemma_refl
                *** QED

Which yields:

Fixpoint.Types.dummyLoc:0:0-0:0: Error
  elaborate makeKnowledge failed on:
      is$Main.Empty (Main.CList GHC.Types.[] Main.Empty GHC.Types.[])
  with error
      Unbound symbol is$Main.Empty --- perhaps you meant: Main.Empty ?
  in environment
      GHC.Types.[] := func(1 , [[@(0)]])
      Main.CList := func(1 , [[@(0)]; @(0); [@(0)]; (Main.CList @(0))])
      Main.Empty := func(1 , [(Main.CList @(0))])

Using --exactdc I get the original error.

:1:1-1:1: Error
  crash: SMTLIB2 respSat = Error "line 385 column 1622: unknown constant Main.CList  (Int (Main.CList Int) Int) (Main.CList Int) declared: (declare-fun Main.CList             (Int (Main.CList Int) Int)             (Main.CList (Main.CList Int))) declared: (declare-fun Main.CList (Int Int Int) (Main.CList Int)) "

Defining eqToList to = True, doesn't solve the issue, so it has something to do with (toList (singleton y))

[ranjitjhala]

Hmm, after some fiddling I think this is because the CList ADT is not something that SMTLIB is directly happy with (need to double check that...) Anyways, the workaround is to disable the native-smt adt encoding ... I really should make this automatic I think MOST of the last N issues have been about it. In short the following works:

https://liquid-demo.programming.systems/index.html#?demo=permalink%2F1590845831_9389.hs

import Language.Haskell.Liquid.ProofCombinators

{-@ LIQUID "--ple-local" @-}
{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--no-adt" @-}

data CList a = Empty
             | CList [a] a [a]

{-@ reflect singleton @-}
singleton :: a -> CList a
singleton e = CList [] e []

{-@ reflect toList @-}
toList :: CList a -> [a]
toList Empty = []
toList (CList l f r) = f : (r `append` (rev l))

{-@ reflect rev @-}
rev :: [a] -> [a]
rev [] = []
rev (x:xs) = (rev xs) `append` [x]

{-@ reflect append @-}
append :: [a] -> [a] -> [a]
append [] ys = ys
append (x:xs) ys = x: (append xs ys)

{-@ reflect eqToList @-}
eqToList ::  CList Int -> CList Int -> Bool
eqToList a b = toList a == toList b

{-@ reflect =*= @-}
{-@ infix 4 =*= @-}
(=*=) :: CList Int -> CList Int -> Bool
x =*= y = (any' (eqToList x) (toList (singleton y)))

{-@ reflect any' @-}
any' :: (a -> Bool) -> [a] -> Bool
any' p [] = False
any' p (x:xs) = p x || any' p xs

{-@ reflect lemma_refl @-}
lemma_refl :: Bool
lemma_refl = Empty =*= Empty

{-@ ple lemma_refl_proof @-}
{-@ lemma_refl_proof ::  { lemma_refl  } @-}
lemma_refl_proof :: Proof
lemma_refl_proof = lemma_refl
                *** QED

[mystaroll]

Thank you for taking a look a this. I feel like the ADT thing was necessary to me: Originally CList is actually imported from another module where other functions are reflected, using --no-adt breaks all the reflections with something like this Unbound symbol Lib.CL.CircularList.CList##lqdc##$select##Lib.CL.CircularList.CList##2

What's the right way to go with this? I guess in the worst case I will need to have a single huge module so that CList is defined in the same place where the reflections happen?

[ranjitjhala]

I think adding no-adt to those modules also should work?

On Sat, May 30, 2020 at 11:08 AM Mustafa Hafidi notifications@github.com wrote:

Thank you for taking a look a this. I feel like --no-adt was necessary to me: Originally CList is actually imported from another module where other functions are reflected, using --no-adt breaks all the reflections with something like this Unbound symbol Lib.CL.CircularList.CList##lqdc##$select##Lib.CL.CircularList.CList##2

What's the right way to go with this? I guess in the worst case I will need to have a single huge module so that CList is defined in the same place where the reflections happen?

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1682*issuecomment-636365200__;Iw!!Mih3wA!QndNSQTcACRni0B2mh9EXPWDGQrRwvRjpw3rLriVkMAOm9uficvoMzVQK7UkmCNL$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OASEQUYKFZZDHAERLLRUFDRBANCNFSM4NONTRMQ__;!!Mih3wA!QndNSQTcACRni0B2mh9EXPWDGQrRwvRjpw3rLriVkMAOm9uficvoMzVQK4n3IVAz$ .

[ranjitjhala]

Ie , just Use no-adt “globally” for your project?

On Sat, May 30, 2020 at 11:42 AM Ranjit Jhala jhala@cs.ucsd.edu wrote:

I think adding no-adt to those modules also should work?

On Sat, May 30, 2020 at 11:08 AM Mustafa Hafidi notifications@github.com wrote:

Thank you for taking a look a this. I feel like --no-adt was necessary to me: Originally CList is actually imported from another module where other functions are reflected, using --no-adt breaks all the reflections with something like this Unbound symbol Lib.CL.CircularList.CList##lqdc##$select##Lib.CL.CircularList.CList##2

What's the right way to go with this? I guess in the worst case I will need to have a single huge module so that CList is defined in the same place where the reflections happen?

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1682*issuecomment-636365200__;Iw!!Mih3wA!QndNSQTcACRni0B2mh9EXPWDGQrRwvRjpw3rLriVkMAOm9uficvoMzVQK7UkmCNL$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OASEQUYKFZZDHAERLLRUFDRBANCNFSM4NONTRMQ__;!!Mih3wA!QndNSQTcACRni0B2mh9EXPWDGQrRwvRjpw3rLriVkMAOm9uficvoMzVQK4n3IVAz$ .

[mystaroll]

Oh, that works! Thank you very much! should I close this issue?

[ranjitjhala]

Let’s keep it open for now till I can figure out why the CList crashes no adt?

Thanks!

On Sat, May 30, 2020 at 11:51 AM Mustafa Hafidi notifications@github.com wrote:

Oh, that works! Thank you very much! should I close this issue?

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1682*issuecomment-636370052__;Iw!!Mih3wA!UeDl9VGl_NGvcU_kLiGXSBKTm2ehaysE5_Jhn8FePi-ZgiwBjoAQ1i3aMzmsC2jM$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OBWLYQKXQYXZ364EIDRUFISZANCNFSM4NONTRMQ__;!!Mih3wA!UeDl9VGl_NGvcU_kLiGXSBKTm2ehaysE5_Jhn8FePi-ZgiwBjoAQ1i3aM48HM4dd$ .