SMT solvers complaining on tutorial examples

[ethanfrey]

First, I want to say that I am quite new to haskell and smt solvers, but heard of this project and it seems a very amazing way to do proofs on production code at minimal cost. I am going through the tutorial and it all makes sense, but I have spent quite a while debugging some issues.

First, the last release on hackage is 0.6.0.0 from almost a year ago, and the syntax is different from the tutorial, (like Prop v for Bool) so I checked out the develop branch and compiled from source with stack. No problem there. (Commit 72422e9 if that matters)

I get most code working, but now and then I am hitting my head, and I think there may be an issue with the setup. I took a minimal snippet from chapter 5 (datatypes) here. Unfortunately the issue with the

Here is a minimal snippet taken from the tutorial that is supposed to work.

module DataTypes
where

{-@ data IncList a =
        Emp
      | (:<) { hd :: a, tl :: IncList {v:a | hd <= v}}  @-}
data IncList a =
    Emp
  | (:<) { hd :: a, tl :: IncList a }

infixr 9 :<

okList  = 1 :< 2 :< 3 :< Emp      -- accepted by LH

insert             :: (Ord a) => a -> IncList a -> IncList a
insert y Emp       = y :< Emp
insert y (x :< xs)
  | y <= x         = y :< x :< xs
  | otherwise      = x :< insert y xs

When I run the solver with z3, I get the following error:

# liquid --smtsolver=z3 datatypes.hs
...
 /Users/ethan/haskell/liquid/src/datatypes.hs:16:1-6: Error: Termination Error

 16 | insert y Emp       = y :< Emp
      ^^^^^^
  DataTypes.insert
 No decreasing parameter

This is all on OSX Sierra (10.12.3)

# z3 --version
Z3 version 4.5.0 - 64 bit

Then I figured, it might be due to poor z3 support. Okay, I went ahead and installed the stable version of cvc4, and more problems. (devel versions even worse):

# cvc4 --version
This is CVC4 version 1.4
compiled with GCC version 4.2.1 Compatible Apple LLVM 5.1 (clang-503.0.40)
on Aug 30 2014 16:33:22

# liquid --smtsolver=cvc4 datatypes.hs
...
Working  14% [==========.......................................................]
liquid: fd:15: hGetLine: end of file

 # cvc4 .liquid/datatypes.hs.smt2
(error "Parse Error: .liquid/datatypes.hs.smt2:227.18: Symbol 'strLen' not declared as a variable

  (assert (= (strLen lit$36$tl) 2))
              ^
")

Then I went for the development version:

# cvc4 --version
This is CVC4 version 1.5-prerelease
compiled with GCC version 4.2.1 Compatible Apple LLVM 4.2 (clang-425.0.28)
on Jan  6 2017 04:07:55

# liquid --smtsolver=cvc4 datatypes.hs
...
Working  14% [==========.......................................................]
liquid:
**** ERROR *********************************************************************
**** ERROR *********************************************************************
**** ERROR *********************************************************************
SMTREAD:string
**** ERROR *********************************************************************
**** ERROR *********************************************************************
**** ERROR *********************************************************************

Callstack:
  error, called at src/Language/Fixpoint/Misc.hs:144:14 in liqui_HmdOaGuCAhX9FxqFDEV5dS:Language.Fixpoint.Misc
  errorstar, called at src/Language/Fixpoint/Smt/Interface.hs:180:21 in liqui_HmdOaGuCAhX9FxqFDEV5dS:Language.Fixpoint.Smt.Interface

# cvc4 .liquid/datatypes.hs.smt2
(error "Parse Error: .liquid/datatypes.hs.smt2:227.18: Symbol 'strLen' not declared as a variable

  (assert (= (strLen lit$36$tl) 2))
              ^
")

And mathsat didn't work either:

# mathsat -version
MathSAT5 version 5.4.0 (e760aff47185) (Mar 14 2017 16:32:22, gmp 5.1.3, clang/LLVM 6.0, 64-bit)

# liquid --smtsolver=mathsat datatypes.hs
...
Working  28% [===================..............................................]

**** DONE:  annotate ***********************************************************

**** RESULT: ERROR *************************************************************

:1:1-1:1: Error
  crash: SMTLIB2 respSat = Error "Undeclared type: Str"

Is there some trick to getting this all to work? Or is OSX just not supported? I hope I am just being stupid, but it would be great if there was a write up on how to do this all, since I think I did follow the instructions.

Thanks for the attention

[nikivazou]

It is not due to a z3 error. No decreasing parameter means it does not know how to prover termination of insert. Can you add the --no-termination flag?

Not sure about the cvc4 error.

[ethanfrey]

Okay, that seems to have solved it:

# liquid --smtsolver=z3 --notermination datatypes.hs
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.

**** DONE:  A-Normalization ****************************************************

**** DONE:  Extracted Core using GHC *******************************************

**** DONE:  Transformed Core ***************************************************

**** DONE:  Uniqify & Rename ***************************************************

Done solving.
RESULT: Safe

**** DONE:  annotate ***********************************************************

**** RESULT: SAFE **************************************************************

[ethanfrey]

Okay, then I guess I will just stick with z3 for now. Those other errors really scared me. If you have a chance to reproduce them, or prove it works for you, it would be great.

Looking forward to exploring more. Thanks for the quick response!

[ethanfrey]

As a note to anyone who sees this. Just add these lines to the top of the .hs file to be checked. At least this fixed my issues with z3. Not sure about the other smt libs...

{-@ LIQUID "--short-names"         @-}
{-@ LIQUID "--no-termination"      @-}
{-@ LIQUID "--scrape-used-imports" @-}

[ranjitjhala]

Hi @ethanfrey -- yes the broader problem is that there is some "boilerplate" code (like the pragmas above) that I omitted (is not visible in) the tutorial PDF but is in the Haskell source. Perhaps I can add a "NOTE" in the tutorial saying the above.

@nikivazou -- several folks have been puzzled by the 'termination error'. We can easily do the following: create a numeric code for each error 1,2,3,... etc. and then have a FAQ that folks can look up to get some initial help?

[nikivazou]

Sure, or we can just change the text "No decreasing parameter" to "Termination error: cannot prove termination, either give a termination hint or run liquid with "--no-termination"".

[ranjitjhala]

Yes that's an immediate fix ...!

On Sat, Apr 22, 2017 at 1:39 AM Niki Vazou notifications@github.com wrote:

Sure, or we can just change the text "No decreasing parameter" to "Termination error: cannot prove termination, either give a termination hint or run liquid with "--no-termination"".

— You are receiving this because you commented.

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