Decouple Invariants From Data

Recursive Structures

Lets see another example of decoupling...

14: {-# LANGUAGE NoMonomorphismRestriction #-}
15: 
16: module List (insertSort) where
17: 
18: {-@ LIQUID "--no-termination" @-}
19: 
20: mergeSort     :: Ord a => [a] -> [a]
21: insertSort :: (Ord a) => [a] -> L a 
22: slist :: L Int
23: slist' :: L Int
24: iGoUp, iGoDn, iDiff :: [Int]
25: infixr `C`

Decouple Invariants From Recursive Data

Recall: Lists

36: data L a = N 
37:          | C { forall a. (L a) -> ahd :: a, forall a. (L a) -> (L a)tl :: L a }

Recall: Refined Constructors

Define increasing Lists with strengthened constructors:

47: data L a where
48:   N :: L a
49:   C :: hd:a -> tl: L {v:a | hd <= v} -> L a

Problem: Decreasing Lists?

What if we need both increasing and decreasing lists?

Separate (indexed) types get quite complicated ...

Abstract That Refinement!

67: {-@ data L a <p :: a -> a -> Prop>
68:       = N 
69:       | C { hd :: a, tl :: L <p> a<p hd> } @-}

p is a binary relation between two a values

Definition relates hd with all the elements of tl

Recursive: p holds for every pair of elements!

Example

Consider a list with three or more elements

90: x1 `C` x2 `C` x3 `C` rest :: L <p> a

Example: Unfold Once

97: x1                 :: a
98: x2 `C` x3 `C` rest :: L <p> a<p x1>

Example: Unfold Twice

105: x1          :: a
106: x2          :: a<p x1>  
107: x3 `C` rest :: L <p> a<p x1 && p x2>

Example: Unfold Thrice

114: x1   :: a
115: x2   :: a<p x1>  
116: x3   :: a<p x1 && p x2>  
117: rest :: L <p> a<p x1 && p x2 && p x3>

Note how p holds between every pair of elements in the list.

A Concrete Example

That was a rather abstract!

How can we use fact that p holds between every pair?

Instantiate p with a concrete refinement

Example: Increasing Lists

Instantiate p with a concrete refinement

148: {-@ type IncL a = L <{\hd v -> hd <= v}> a @-}

Refinement says: hd less than every v in tail,

i.e., IncL denotes increasing lists.

Example: Increasing Lists

LiquidHaskell verifies that slist is indeed increasing...

165: {-@ slist :: IncL Int @-}
166: (L <\hd2 VV -> (hd2 <= VV)> Int)slist     = {x2 : Int | (x2 == (1  :  int))}1 forall <p :: GHC.Types.Int-> GHC.Types.Int-> Bool>.
x1:{x14 : Int | (x14 > 0)}
-> x2:(L <\x10 VV -> p x10> {x14 : Int<p x1> | (x14 > 0)})
-> {x3 : (L <\x5 VV -> p x5> {x14 : Int | (x14 > 0)}) | ((hd x3) == x1) && ((tl x3) == x2)}`C` {x2 : Int | (x2 == (6  :  int))}6 forall <p :: GHC.Types.Int-> GHC.Types.Int-> Bool>.
x1:{x14 : Int | (x14 > 0)}
-> x2:(L <\x10 VV -> p x10> {x14 : Int<p x1> | (x14 > 0)})
-> {x3 : (L <\x5 VV -> p x5> {x14 : Int | (x14 > 0)}) | ((hd x3) == x1) && ((tl x3) == x2)}`C` {x2 : Int | (x2 == (12  :  int))}12 forall <p :: GHC.Types.Int-> GHC.Types.Int-> Bool>.
x1:{x14 : Int | (x14 > 0)}
-> x2:(L <\x10 VV -> p x10> {x14 : Int<p x1> | (x14 > 0)})
-> {x3 : (L <\x5 VV -> p x5> {x14 : Int | (x14 > 0)}) | ((hd x3) == x1) && ((tl x3) == x2)}`C` (L <\_ VV -> false> {x3 : Int | false})N

... and protests that slist' is not:

176: {-@ slist' :: IncL Int @-}
177: (L <\hd2 VV -> (hd2 <= VV)> Int)slist' = {x2 : Int | (x2 == (6  :  int))}6 forall <p :: GHC.Types.Int-> GHC.Types.Int-> Bool>.
x1:{x14 : Int | (x14 > 0)}
-> x2:(L <\x10 VV -> p x10> {x14 : Int<p x1> | (x14 > 0)})
-> {x3 : (L <\x5 VV -> p x5> {x14 : Int | (x14 > 0)}) | ((hd x3) == x1) && ((tl x3) == x2)}`C` {x2 : Int | (x2 == (1  :  int))}1 forall <p :: GHC.Types.Int-> GHC.Types.Int-> Bool>.
x1:{x14 : Int | (x14 > 0)}
-> x2:(L <\x10 VV -> p x10> {x14 : Int<p x1> | (x14 > 0)})
-> {x3 : (L <\x5 VV -> p x5> {x14 : Int | (x14 > 0)}) | ((hd x3) == x1) && ((tl x3) == x2)}`C` {x2 : Int | (x2 == (12  :  int))}12 forall <p :: GHC.Types.Int-> GHC.Types.Int-> Bool>.
x1:{x14 : Int | (x14 > 0)}
-> x2:(L <\x10 VV -> p x10> {x14 : Int<p x1> | (x14 > 0)})
-> {x3 : (L <\x5 VV -> p x5> {x14 : Int | (x14 > 0)}) | ((hd x3) == x1) && ((tl x3) == x2)}`C` (L <\_ VV -> false> {x3 : Int | false})N

Insertion Sort

185: {-@ insertSort :: (Ord a) => [a] -> IncL a @-}
186: forall a. (Ord a) => [a] -> (L <\hd2 VV -> (hd2 <= VV)> a)insertSort     = (a -> (L <\x9 VV -> (VV >= x9)> a) -> (L <\x9 VV -> (VV >= x9)> a))
-> (L <\x9 VV -> (VV >= x9)> a)
-> [a]
-> (L <\x9 VV -> (VV >= x9)> a)foldr a -> (L <\x4 VV -> (VV >= x4)> a) -> (L <\x2 VV -> (VV >= x2)> a)insert (L <\_ VV -> false> {VV : a | false})N
187: 
188: forall a.
(Ord a) =>
a -> (L <\x2 VV -> (VV >= x2)> a) -> (L <\x1 VV -> (VV >= x1)> a)insert ay N          = {VV : a | (VV == y)}y forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV == y)}
-> x2:(L <\x6 VV -> p x6> {VV : a<p x1> | (VV == y)})
-> {x3 : (L <\x4 VV -> p x4> {VV : a | (VV == y)}) | ((hd x3) == x1) && ((tl x3) == x2)}`C` (L <\_ VV -> false> {VV : a | false})N
189: insert y (x `C` xs) 
190:   | {VV : a | (VV == y)}y x1:a -> x2:a -> {x2 : Bool | (((Prop x2)) <=> (x1 < x2))}< {VV : a | (VV == x)}x           = {VV : a | (VV == y)}y forall <p :: a-> a-> Bool>.
x1:{VV : a | (y <= VV)}
-> x2:(L <\x6 VV -> p x6> {VV : a<p x1> | (y <= VV)})
-> {x3 : (L <\x4 VV -> p x4> {VV : a | (y <= VV)}) | ((hd x3) == x1) && ((tl x3) == x2)}`C` ({VV : a | (VV == x)}x forall <p :: a-> a-> Bool>.
x1:{VV : a | (VV > y) && (x <= VV)}
-> x2:(L <\x6 VV -> p x6> {VV : a<p x1> | (VV > y) && (x <= VV)})
-> {x3 : (L <\x4 VV -> p x4> {VV : a | (VV > y) && (x <= VV)}) | ((hd x3) == x1) && ((tl x3) == x2)}`C` {x2 : (L <\x3 VV -> (VV >= x3)> {VV : a | (VV >= x)}) | (x2 == xs)}xs)
191:   | otherwise       = {VV : a | (VV == x)}x forall <p :: a-> a-> Bool>.
x1:{VV : a | (x <= VV)}
-> x2:(L <\x6 VV -> p x6> {VV : a<p x1> | (x <= VV)})
-> {x3 : (L <\x4 VV -> p x4> {VV : a | (x <= VV)}) | ((hd x3) == x1) && ((tl x3) == x2)}`C` forall a.
(Ord a) =>
a -> (L <\x2 VV -> (VV >= x2)> a) -> (L <\x1 VV -> (VV >= x1)> a)insert {VV : a | (VV == y)}y {x2 : (L <\x3 VV -> (VV >= x3)> {VV : a | (VV >= x)}) | (x2 == xs)}xs

(Mouseover insert to see inferred type.)

Checking GHC Lists

Demo: Above applies to GHC's List definition:

205: data [a] <p :: a -> a -> Prop>
206:   = [] 
207:   | (:) { h :: a, tl :: [a<p h>]<p> }

Checking GHC Lists

Increasing Lists

218: {-@ type Incs a = [a]<{\h v -> h <= v}> @-}
219: 
220: {-@ iGoUp :: Incs Int @-}
221: [Int]<\h6 VV -> (h6 <= VV)>iGoUp     = {x3 : [{x13 : Int | (x13 > 0)}]<\x10 VV -> (x10 /= x11) && (x11 > 0) && (x11 > x10) && (x10 <= x11)> | (((null x3)) <=> false) && ((len x3) >= 0)}[{x2 : Int | (x2 == (1  :  int))}1,{x2 : Int | (x2 == (2  :  int))}2,{x2 : Int | (x2 == (3  :  int))}3]

Checking GHC Lists

Decreasing Lists

232: {-@ type Decs a = [a]<{\h v -> h >= v}> @-}
233: 
234: {-@ iGoDn :: Decs Int @-}
235: [Int]<\h8 VV -> (h8 >= VV)>iGoDn     = {x3 : [{x14 : Int | (x14 > 0)}]<\x12 VV -> (x11 == 1) && (x12 /= x11) && (x11 > 0) && (x12 >= x11) && (x11 < x12)> | (((null x3)) <=> false) && ((len x3) >= 0)}[{x2 : Int | (x2 == (3  :  int))}3,{x2 : Int | (x2 == (2  :  int))}2,{x2 : Int | (x2 == (1  :  int))}1]

Checking GHC Lists

Duplicate-free Lists

247: {-@ type Difs a = [a]<{\h v -> h /= v}> @-}
248: 
249: {-@ iDiff :: Difs Int @-}
250: [Int]<\h10 VV -> (h10 /= VV)>iDiff     = {x3 : [{x13 : Int | (x13 > 0)}]<\x11 VV -> (x11 /= x10) && (x10 > 0) && (x11 >= x10) && (x10 < x11)> | (((null x3)) <=> false) && ((len x3) >= 0)}[{x2 : Int | (x2 == (1  :  int))}1,{x2 : Int | (x2 == (3  :  int))}3,{x2 : Int | (x2 == (2  :  int))}2]

Checking GHC Lists

Now we can check all the usual list sorting algorithms

Demo: List Sorting

Phew!

Lets see one last example...

[Skip]

Example: Binary Trees

... Map from keys of type k to values of type a

Implemented, in Data.Map as a binary tree:

418: data Map k a = Tip
419:              | Bin Size k a (Map k a) (Map k a)
420: 
421: type Size    = Int

Two Abstract Refinements

l : relates root key with left-subtree keys
r : relates root key with right-subtree keys

434: {-@ data Map k a < l :: k -> k -> Prop
435:                  , r :: k -> k -> Prop >
436:     = Tip
437:     | Bin (sz :: Size) (key :: k) (val :: a)
438:           (left  :: Map <l,r> (k<l key>) a)
439:           (right :: Map <l,r> (k<r key>) a) @-}

Ex: Binary Search Trees

Keys are Binary-Search Ordered

451: {-@ type BST k a = 
452:       Map <{\r v -> v < r }, 
453:            {\r v -> v > r }> 
454:           k a                   @-}

Ex: Minimum Heaps

Root contains minimum value

465: {-@ type MinHeap k a = 
466:       Map <{\r v -> r <= v}, 
467:            {\r v -> r <= v}> 
468:            k a               @-}

Ex: Maximum Heaps

Root contains maximum value

479: {-@ type MaxHeap k a = 
480:       Map <{\r v -> r >= v}, 
481:            {\r v -> r >= v}> 
482:            k a               @-}

Example: Data.Map

Standard Key-Value container

1300+ non-comment lines
insert, split, merge,...
Rotation, Rebalance,...

SMT & inference crucial for verification

Demo: Binary Search Maps

Recap

Refinements: Types + Predicates
Subtyping: SMT Implication
Measures: Strengthened Constructors
Abstract: Refinements over functions and data
Er, what about Haskell's lazy evaluation?

[continue...]

Decouple Invariants From Data

Recursive Structures

Decouple Invariants From Recursive Data

Recall: Lists

Recall: Refined Constructors

Problem: Decreasing Lists?

Abstract That Refinement!

Example

Example: Unfold Once

Example: Unfold Twice

Example: Unfold Thrice

A Concrete Example

Example: Increasing Lists

Example: Increasing Lists

Insertion Sort

Checking GHC Lists

Checking GHC Lists

Checking GHC Lists

Checking GHC Lists

Checking GHC Lists

Phew!

Example: Binary Trees

Two Abstract Refinements

Ex: Binary Search Trees

Ex: Minimum Heaps

Ex: Maximum Heaps

Example: Data.Map

Recap: Abstract Refinements

Recap