Using Liquid Haskell to Check for Valid Tokens

Question

I am doing some experimentation using liquid-haskell to see what kinds of neat things I can do with it and I have hit a bit of a wall. The basic idea is that I have some functions that require an access token that expires after a certain amount of time has passed. I am trying to see how I might use liquid-haskell to ensure that the token is checked for validity before passing it into one of my functions. I have created a minimal working version below that demonstrates my problem. When I run liquid on this file I get the following error:

/tmp/liquidTest.hs:18:17-42: Error: Liquid Type Mismatch

 18 | isExpired tok = currTime >= expiration tok
                      ^^^^^^^^^^^^^^^^^^^^^^^^^^

   Inferred type
     VV : {VV : GHC.Types.Bool | Prop VV <=> Main.currTime >= ?a}

   not a subtype of Required type
     VV : {VV : GHC.Types.Bool | Prop VV <=> currTime >= expiration tok}

   In Context
     Main.currTime := Data.Time.Clock.UTC.UTCTime

     tok := Main.Token

     ?a := {?a : Data.Time.Clock.UTC.UTCTime | ?a == expiration tok}

I cannot seem to figure out why this error is showing up and everything I have tried has failed. Could someone please help me?

Also, I would like to have the currTime function replaced with the getCurrentTime function in the time package. That way I can compare the timestamp on the token with the current time. That would mean that my isExpired function would be of type Token -> IO Bool. Would that even be possible using liquid haskell?

import Data.Time
import Language.Haskell.Liquid.Prelude

{-@ data Token = Token
         (expiration :: UTCTime)
@-}

data Token = Token
    { expiration :: UTCTime
    } deriving Show

{-@ measure currTime :: UTCTime @-}
currTime :: UTCTime
currTime = UTCTime (ModifiedJulianDay 57614) 83924.978297

{-@ isExpired :: t:Token -> {v:Bool | ((Prop v) <=> (currTime >= expiration t))} @-}
isExpired :: Token -> Bool
isExpired tok = currTime >= expiration tok

{-@ type ValidToken = {t:Token | currTime < expiration t} @-}

{-@ showToken :: ValidToken -> String @-}
showToken :: Token -> String
showToken tok = show tok

main :: IO ()
main = do
  ct <- getCurrentTime
  let tok = Token ct

  print currTime

  case isExpired tok of
    True -> putStrLn "The token has expired!"
    False -> putStrLn $ showToken tok

Thanks!

Answer 1

There are a couple problems here.

1. You're trying to define currTime as a measure but measures are supposed to be functions. This should be flagged as an error by LiquidHaskell.

2. You may have noticed this before you made currTime a measure, but you can't currently refer to top-level definitions in a type signature. We can fix your example by passing currTime as a parameter to isExpired, and by adding a parameter to the ValidToken type (which is probably what you want to do anyway since the validity of the token is with respect to some timestamp). Here's a link to the working version on our demo page.

Finally, you certainly can rewrite the code to use getCurrentTime inside isValid, though you'll probably need to change the definition of ValidToken since the current time never escapes isValid. Here's how I would do it.

I define an "uninterpreted" measure (no body) called valid and change isExpired's type to return IO {v:Bool | ((Prop v) <=> (not (valid t)))}. Unfortunately, LiquidHaskell can't verify the definition of isExpired because we haven't told it what valid means. So we have to assume the type for isExpired, making it part of our trusted computing base. I'm ok with this because it's a small function, and it's the only thing that needs to be assumed.