to ping or not to ping, that is the question

[sc...@ggr.com]

LH newb here. :) I thought I'd try out LH against my existing code base and see what bugs it tells me about, as a way for me to learn about LH and make my code better in the process. I've been able to fix a bunch of unsafe code, but I'm stumped on an error that I'm having trouble understanding.

The code being analysed by LH is this (https://github.com/bonds/winot/blob/master/src/Util.hs#L73-L80):

pingVia :: Int -> Int -> T.Text -> IO Bool
pingVia rt count host
    | count < 1 = M.return False
    | otherwise = do
        ec <- runEC $ T.concat ["ping -V ", T.pack (show rt), " -q -c 1 -w 1 ", host]
        if wasSuccess ec then M.return True else do
            D.delay $ (10::Integer)^(6::Integer) -- wait a second between ping attempts
            pingVia rt (count-1) host

LH has this to say about it:

 src/Util.hs:80:13-22: Error: Liquid Type Mismatch
 
 80 |             pingVia rt (count-1) host
                  ^^^^^^^^^^
 
   Inferred type
     VV : {VV : Int | VV == rt}
 
   not a subtype of Required type
     VV : {VV : Int | VV < rt
                      && VV >= 0}
 
   In Context
     rt := Int

pingVia is a function that takes a routing table number, a target ping count, and a host IP and pings the host until a ping succeeds or the count runs out, using the chosen routing table for routing the ping. The VV : Int makes sense. VV == rt makes sense. But where is the VV < rt coming from in the 'not a subtype of Required type'? That's not going to go so well...rt cannot be both == VV and > VV. Thus the error, I suppose. ;)

[Ranjit Jhala]

Hi Scott,

This error has to do with proving that `pingVia` terminates. 

To do so, by default LH uses the first parameter for which 

it has a "termination metric", and puts in a proof obligation 

that at the recursive call, the parameter passed in is:

(1) smaller than the current parameter,

(2) lower bounded by 0.

In this example, 

   pingVia :: Int -> Int -> T.Text -> IO Bool

it uses the first `Int` as such a parameter (namely `rt`) and hence,

tries to prove that at the recursive call, the (recursive) parameter is 

(1) v < rt "less than the current parameter"

(2) 0 <= v "lower bounded by 0" 

Of course, in this case, this is the WRONG thing to prove, because the 

"correct" termination metric is the *second* parameter, namely `count`.

To tell LH to use `count` (instead of the default), use the 

following type signature:

  {-@ pingVia :: Int -> count:Int -> T.Text -> IO Bool / [count] @-}

Or, alternately, if you prefer, disable termination checking with:

 {-@ LIQUID "--no-termination" @-}

Can you let us know if that works?

Thanks!

Ranjit.

@Niki : I thought you had changed things so this was marked as a "Termination Error"?)

--
You received this message because you are subscribed to the Google Groups "liquidhaskell" group.
To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskel...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[sc...@ggr.com]

That did the trick. I even got fancy and added a constraint on the routing table parameter:

{-@ pingVia :: {rt:Int | rt >= 0} -> count:Int -> T.Text -> IO Bool / [count] @-}

and I RTFM about the termination syntax, i.e. / [count]', in the README: https://github.com/ucsd-progsys/liquidhaskell

Thanks!

[Ranjit Jhala]

Great! 

Since its so common, I like to define: 

   {-@ type Nat = {v:Int | v >= 0} @-}

and then the above becomes:

   {-@ pingVia :: Nat -> count:Int -> T.Text -> IO Bool / [count] @-}

Best!

- Ranjit.

--

[Niki Vazou]

On Thu, May 26, 2016 at 10:01 AM, Ranjit Jhala <jh...@cs.ucsd.edu> wrote:

Great! 

Since its so common, I like to define: 

   {-@ type Nat = {v:Int | v >= 0} @-}

You do not have to define `Nat` it imported with LiquidHaskell.

@Scott, does your pingVia work?

pingVia :: {rt:Int | rt >= 0} -> count:Int -> T.Text -> IO Bool / [count]

I am surprised, as the termination metric should be >=0, i.e., it needs to be a Nat. 

@Ranjit, I haven't fixed the termination errors yet, they appear as type errors, unless you use the termination syntax.  

[Scott Bonds]

Yes, my pingVia works, LH does not complain about it. I tried the way
you suggested too, without defining Nat myself, and that works too:

{-@ pingVia :: Nat -> count:Int -> T.Text -> IO Bool / [count] @-}

On 05/26, Niki Vazou wrote:
> On Thu, May 26, 2016 at 10:01 AM, Ranjit Jhala <[1]jh...@cs.ucsd.edu>

> References
>
> 1. mailto:jh...@cs.ucsd.edu