Standard Refinement Types

























Division by Zero


module Refinements where
div0 :: () -> Int 
div0 _ = 42 `div` 0
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

To run Liquid Haskell on your Refinements.lhs file

  • Here: Press Play

  • Locally:

cabal install liquidhaskell
liquid Foo.lhs













Division by a variable.


The input x might be 0.

divx :: Int -> Int 
divx x = 42 `div` x
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Fixes:

  • Divide with a provably non-zero value (e.g., x*x+1)

  • Make divx only accept non-zero arguments.













Constrain Propagation

Now you can only call divx on non-zero inputs!

readDivx :: IO Int 
readDivx = do 
  i <- getLine
  let x = read i :: Int 
  return $ divx x 
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


Q: Change the code to only call divx on non-zero.

Q: What if the call to div in divx changes?













Refinement Types


Refinements of Haskell types with logical predicates!

{-@ divx :: x:{Int | x /= 0} -> Int @-}

The special comments {-@ ... @-} are

  • interpreted by Liquid Haskell, but

  • ignored by ghc.












Head of lists


Another check: head on only non-empty lists.


headEmp :: () -> a 
headEmp _ = head [] 
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX


Q: Can you fix the error?












Head on variables

headxs :: [a] -> a 
headxs xs = head xs  
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Fixes:

  • Make the list (provably) nonempty

  • Better, refine the type to only accept nonempty lists!












List Appending

{-@ headxsys :: [a] -> xs:{[a] | 0 < len xs } -> a @-}
headxsys :: [a] -> [a] -> a 
headxsys ys xs = head (xs ++ ys)  
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

The type is good, but too restrictive.

Q: Can you make the below pass?

foo :: () -> Int
foo _ = headxsys [1, 2, 3] []
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX












Example: Avegerage on Lists


{-@ avg :: [Int] -> Int @-}
avg :: [Int] -> Int 
avg xs = sum xs `div` length xs 
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Q: Can you fix the type error?











We saw verification under two constraints


{-@ div  :: Int -> x:{Int | 0 /= x } -> Int @-}

{-@ head :: xs:{[a] | 0 < len xs } -> a @-}

Where do these constraints come from?











What takes to verify take?

{-@ safeTake :: i:Int -> xs:[a] -> [a] @-}
safeTake :: Int -> [a] -> [a]
safeTake 0 []     = [] 
safeTake i (x:xs) = if i == 0 then [] else x:safeTake (i-1) xs
safeTake i []     = error "Out of bounds indexing!"
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Q: Can you fix the error?











In-bounds indexing to prevent Heartbleed

Reminder of Haskell Heartbleed.

λ> :m +Data.Text Data.Text.Unsafe
λ>  takeWord16 10 (pack "zurihac")
"zurihac\NUL\26984\1930"

Detect Heartbleed with Liquid Haskell.

{-@ takeWord16 :: i:Nat -> xs:{Text | i < tlen xs } -> Text @-}
heartbleed :: Text 
heartbleed = takeWord16 10  (pack "zurihac")
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX











Length of a Text

{-@ takeWord16 :: i:Nat -> xs:{Text | i < tlen xs } -> Text @-}

Define logical functions as measures.

{-@ measure tlen :: Text -> Int @-}
{-@ pack :: s:String -> {t:Text | len s == tlen t} @-}
safe   :: Text 
safe   = takeWord16 4  (pack "zurihac") 
unsafe :: Text 
unsafe = takeWord16 10 (pack "zurihac")
{-@ depends :: i:{Nat |  i < 7 } -> Text @-}
depends :: Int -> Text 
depends i = takeWord16 i (pack "zurihac")
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX











Recap

  • Refinement Types: Haskell Types + Predicates

  • Used to:

    • Catch runtime crashing.

    • Propagate & discharge constraints.

    • Remove runtime checks (make unsafe functions safe!).

  • Other checked properties: Totality & Termination





















Appendix

{-@ LIQUID "--no-termination" @-}
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
data Text = Text 
pack :: String -> Text 
pack _ = undefined  
takeWord16 :: Int -> Text -> Text
takeWord16 _ _ = Text 
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX