Measures

7: module Measures where
8: import Prelude hiding ((!!), length)
9: import Language.Haskell.Liquid.Prelude

Measuring A List's length in logic

On List data type

18: infixr `C`
19: data L a = N | C a (L a)

We define a measure for the length of a List

25: {-@ measure llen :: (L a) -> Int
26:     llen(N)      = 0
27:     llen(C x xs) = 1 + (llen xs)
28:   @-}

34: data L a where 
35:   N :: {v : L a | (llen v) = 0}
36:   C :: x:a -> xs:(L a) -> {v:(L a) |(llen v) = 1 + (llen xs)}

Measuring A List's length in logic

Now we can verify

48: {-@ length :: xs:(L a) -> {v:Int | v = (llen xs)} @-}
49: length     :: L a -> Int
50: forall a.
x1:(Measures.L a) -> {VV : (GHC.Types.Int) | (VV == (llen x1))}length N        = x1:(GHC.Prim.Int#) -> {VV : (GHC.Types.Int) | (VV == (x1  :  int))}0
51: length (C _ ys) = {VV : (GHC.Types.Int) | (VV == (1  :  int))}1 x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ (forall a.
x1:(Measures.L a) -> {VV : (GHC.Types.Int) | (VV == (llen x1))}length {VV : (Measures.L a) | (VV == ys)}ys)

Measuring A List's length in logic

And we can type (!!) as

63: {-@ (!!) :: ls:(L a) -> {v:Nat | v < (llen ls)} -> a @-}
64: (!!)         :: L a -> Int -> a
65: (C x _) forall a.
x1:(Measures.L a)
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < (llen x1))} -> a!! 0 = {VV : a | (VV == x)}x
66: (C _ xs)!! n = (Measures.L {VV : a | (x <= VV)})xsforall a.
x1:(Measures.L a)
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < (llen x1))} -> a!!({VV : (GHC.Types.Int) | (VV >= 0)}nx1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}-{VV : (GHC.Types.Int) | (VV == (1  :  int))}1)
67: _       !! _ = {VV : [(GHC.Types.Char)] | false} -> {VV : a | false}liquidError {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"This should not happen!"

Demo: Lets see what happens if we change the precondition

Another measure for List

We define a new measure to check nullity of a List

82: {-@ measure isNull :: (L a) -> Prop
83:     isNull(N)      = true
84:     isNull(C x xs) = false
85:   @-}

91: data L a where 
92:   N :: {v : L a | isNull v}
93:   C :: x:a -> xs:(L a) -> {v:(L a) | not (isNull v)}

Multiple measures for List

The types of data constructors will be the conjuction of all the inferred types:

105: data L a where 
106:   N :: {v : L a | (llen v) = 0}
107:   C :: a -> xs: L a -> {v:L a |(llen v) = 1 + (llen xs)}

112: data L a where 
113:   N :: {v : L a | isNull v}
114:   C :: a -> xs: L a -> {v:L a | not (isNull v)}

120: data L a where 
121:   N :: {v : L a | (llen v) = 0 && (isNull v)}
122:   C :: a -> xs: L a -> {v:L a |(llen v) = 1 + (llen xs) && not (isNull v)}

Invariants in Data Constructors

We can refine the definition of data types setting invariants

131: {-@ data L a = N
132:              | C (x :: a) (xs :: L {v:a | x <= v})  @-}

138: data L a where
139:   N :: L a
140:   C :: x:a -> xs: L {v:a | x <= v} -> L a

Invariants in Data Constructors

We can refine the definition of data types setting invariants

149: {-@ data L a = N
150:              | C (x :: a) (xs :: L {v:a | x <= v})  @-}

156: data L a where
157:   N :: L a
158:   C :: x:a -> xs: L {v:a | x <= v} -> L a

LiquidHaskell

• Proves the property when C is called

• Assumes the property when C is opened

Increasing Lists

This invariant constrains all Lists to increasing

174: {-@ data L a = N
175:              | C (x :: a) (xs :: L {v:a | x <= v})  @-}

Insert sort

182: {-@ insert :: Ord a => a -> L a -> L a @-}
183: insert :: Ord a => a -> L a -> L a
184: forall a.
(GHC.Classes.Ord a) =>
a -> (Measures.L a) -> (Measures.L a)insert ay (x `C` xs) | {VV : a | (VV == x)}x x1:a
-> x2:a -> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 <= x2))}<= {VV : a | (VV == y)}y    = {VV : a | (VV == x)}x x1:{VV : a | (VV >= x)}
-> x2:(Measures.L {VV : a | (VV >= x) && (x1 <= VV)})
-> {VV : (Measures.L {VV : a | (VV >= x)}) | (((isNull VV)) <=> false) && ((llen VV) == (1 + (llen x2)))}`C` forall a.
(GHC.Classes.Ord a) =>
a -> (Measures.L a) -> (Measures.L a)insert {VV : a | (VV == y)}y {VV : (Measures.L {VV : a | (x <= VV)}) | (VV == xs)}xs
185:                     | otherwise = {VV : a | (VV == y)}y x1:{VV : a | (VV >= y)}
-> x2:(Measures.L {VV : a | (VV >= y) && (x1 <= VV)})
-> {VV : (Measures.L {VV : a | (VV >= y)}) | (((isNull VV)) <=> false) && ((llen VV) == (1 + (llen x2)))}`C` forall a.
(GHC.Classes.Ord a) =>
a -> (Measures.L a) -> (Measures.L a)insert {VV : a | (VV == x)}x {VV : (Measures.L {VV : a | (x <= VV)}) | (VV == xs)}xs
186: 
187: {-@ insertSort  :: Ord a => [a] -> L a @-}
188: insertSort  :: Ord a => [a] -> L a
189: forall a. (GHC.Classes.Ord a) => [a] -> (Measures.L a)insertSort = (a -> (Measures.L a) -> (Measures.L a))
-> (Measures.L a) -> [a] -> (Measures.L a)foldr a -> (Measures.L a) -> (Measures.L a)insert {VV : (Measures.L {VV : a | false}) | (((isNull VV)) <=> true) && ((llen VV) == 0)}N

What if increasing and decreasing lists should co-exist?

Invariants in ByteString

199: measure fplen :: ForeignPtr a -> Int
200: 
201: data ByteString = PS
202:   { pay :: ForeignPtr Word8
203:   , off :: {v:Nat | v <= (fplen pay)}
204:   , len :: {v:Nat | off + v <= (fplen pay)} }

Allow us to enforce low-level memory safety.