Decouple Invariants From Data

Recursive Structures

Lets see another example of decoupling...

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:{x12 : Int | (x12 > 0)}
-> x2:(L <p> {x12 : Int<p x1> | (x12 > 0)})
-> {x3 : (L <p> {x12 : Int | (x12 > 0)}) | ((hd x3) == x1) && ((tl x3) == x2)}`C` {x2 : Int | (x2 == (6  :  int))}6 forall <p :: GHC.Types.Int-> GHC.Types.Int-> Bool>.
x1:{x12 : Int | (x12 > 0)}
-> x2:(L <p> {x12 : Int<p x1> | (x12 > 0)})
-> {x3 : (L <p> {x12 : Int | (x12 > 0)}) | ((hd x3) == x1) && ((tl x3) == x2)}`C` {x2 : Int | (x2 == (12  :  int))}12 forall <p :: GHC.Types.Int-> GHC.Types.Int-> Bool>.
x1:{x12 : Int | (x12 > 0)}
-> x2:(L <p> {x12 : Int<p x1> | (x12 > 0)})
-> {x3 : (L <p> {x12 : Int | (x12 > 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 <p> {VV : a<p x1> | (VV == y)})
-> {x3 : (L <p> {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 <p> {VV : a<p x1> | (y <= VV)})
-> {x3 : (L <p> {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 <p> {VV : a<p x1> | (VV > y) && (x <= VV)})
-> {x3 : (L <p> {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 <p> {VV : a<p x1> | (x <= VV)})
-> {x3 : (L <p> {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
432: {-@ data Map k a < l :: k -> k -> Prop
433:                  , r :: k -> k -> Prop >
434:     = Tip
435:     | Bin (sz :: Size) (key :: k) (val :: a)
436:           (left  :: Map <l,r> (k<l key>) a)
437:           (right :: Map <l,r> (k<r key>) a) @-}

Ex: Binary Search Trees

Keys are Binary-Search Ordered


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

Ex: Minimum Heaps

Root contains minimum value


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

Ex: Maximum Heaps

Root contains maximum value


477: {-@ type MaxHeap k a = 
478:       Map <{\r v -> r >= v}, 
479:            {\r v -> r >= v}> 
480:            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: Abstract Refinements

Decouple invariants from functions

  • max
  • loop
  • foldr

Decouple invariants from data

  • Vector
  • List
  • Tree

Recap

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