Measuring Data Types

11: 
12: {-# LIQUID "--no-termination" #-}
13: {-# LIQUID "--full" #-}
14: 
15: module Measures where
16: import Prelude hiding ((!!), length)
17: import Language.Haskell.Liquid.Prelude
18: 
19: 
20: length      :: L a -> Int
21: (!)         :: L a -> Int -> a
22: insert      :: Ord a => a -> L a -> L a
23: insertSort  :: Ord a => [a] -> L a
24: 
25: infixr `C`

Measuring Data Types

Recap

Refinements: Types + Predicates
Subtyping: SMT Implication

Example: Length of a List

Given a type for lists:

49: data L a = N | C a (L a)

We can define the length as:

60: {-@ measure llen  :: (L a) -> Int
61:     llen (N)      = 0
62:     llen (C x xs) = 1 + (llen xs)  @-}

68: {-@ data L [llen] a = N | C {hd :: a, tl :: L a } @-}
69: {-@ invariant {v: L a | 0 <= llen v}              @-}

Example: Length of a List

78: {-@ measure llen  :: (L a) -> Int
79:     llen (N)      = 0
80:     llen (C x xs) = 1 + llen xs  @-}

We strengthen data constructor types

90: data L a where 
91:   N :: {v: L a | (llen v) = 0}
92:   C :: a -> t:_ -> {v:_| llen v = 1 + llen t}

Measures Are Uninterpreted

99: data L a where 
100:   N :: {v: L a | (llen v) = 0}
101:   C :: a -> t:_ -> {v:_| llen v = 1 + llen t}

llen is an uninterpreted function in SMT logic

Measures Are Uninterpreted

In SMT, uninterpreted function \(f\) obeys congruence axiom:

\[\forall \overline{x}, \overline{y}. \overline{x} = \overline{y} \Rightarrow f(\overline{x}) = f(\overline{y})\]

Other properties of llen asserted when typing fold & unfold

Crucial for efficient, decidable and predictable verification.

Measures Are Uninterpreted

Other properties of llen asserted when typing fold & unfold

Fold

141: z = C x y     -- z :: {v | llen v = 1 + llen y}

Unfold

149: case z of 
150:   N     -> e1 -- z :: {v | llen v = 0}
151:   C x y -> e2 -- z :: {v | llen v = 1 + llen y}

Measured Refinements

Now, we can verify:

164: {-@ length      :: xs:L a -> EqLen xs @-}
165: forall a. x1:(L a) -> {v : Int | v == llen x1 && v >= 0}length N        = x1:Int# -> {v : Int | v == (x1  :  int)}0
166: length (C _ xs) = {v : Int | v == (1  :  int)}1 x1:Int -> x2:Int -> {v : Int | v == x1 + x2}+ forall a. x1:(L a) -> {v : Int | v == llen x1 && v >= 0}length {v : (L a) | v == xs && 0 <= llen v}xs

Where EqLen is a type alias:

176: {-@ type EqLen Xs = {v:Nat | v = llen Xs} @-}

List Indexing Redux

We can type list lookup:

187: {-@ (!)      :: xs:L a -> LtLen xs -> a @-}
188: (C x _)  forall a. x1:(L a) -> {v : Int | v >= 0 && v < llen x1} -> a! 0 = {VV : a | VV == x}x
189: (C _ xs) ! i = {v : (L {VV : a | x <= VV}) | 0 <= llen v}xs forall a. x1:(L a) -> {v : Int | v >= 0 && v < llen x1} -> a! ({v : Int | v >= 0}i x1:Int -> x2:Int -> {v : Int | v == x1 - x2}- {v : Int | v == (1  :  int)}1)
190: _        ! _ = {v : [Char] | false} -> aliquidError {v : [Char] | len v >= 0}"never happens!"

Where LtLen is a type alias:

199: {-@ type LtLen Xs = {v:Nat | v < llen Xs} @-}

Demo: What if we remove the precondition?

Multiple Measures

Multiple measures by conjoining refinements.

e.g. Red Black Tree

Height
Color
Nodes, etc.

Refined Data Constructors

Can encode other invariants inside constructors

241: {-@ data L a = N
242:              | C { x  :: a 
243:                  , xs :: L {v:a| x <= v} } @-}

Head x is less than every element of tail xs

i.e. specifies increasing Lists

Increasing Lists

262: data L a where
263:   N :: L a
264:   C :: x:a -> xs: L {v:a | x <= v} -> L a

We check property when folding C
We assume property when unfolding C

Increasing Lists

Demo: Insertion Sort (hover for inferred types)

280: forall a. (Ord a) => [a] -> (L a)insertSort [a]xs = (a -> (L a) -> (L a)) -> (L a) -> [a] -> (L a)foldr a -> (L a) -> (L a)insert {v : (L a) | llen v == 0 && 0 <= llen v}N {v : [a] | v == xs && len v >= 0}xs
281: 
282: forall a. (Ord a) => a -> (L a) -> (L a)insert ay (x `C` xs) 
283:   | {VV : a | VV == y}y x1:a -> x2:a -> {v : Bool | Prop v <=> x1 <= v}<= {VV : a | VV == x}x    = {VV : a | VV == y}y x1:a
-> x2:(L {VV : a | x1 <= VV})
-> {v : (L a) | llen v == 1 + llen x2 && x2 v == x2 && hd v == x1 && tl v == x2 && x1 v == x1}`C` ({VV : a | VV == x}x x1:{VV : a | VV >= x && VV >= y}
-> x2:(L {VV : a | VV >= x && VV >= y && x1 <= VV})
-> {v : (L {VV : a | VV >= x && VV >= y}) | x2 v == x2 && llen v == 1 + llen x2 && x1 v == x1 && hd v == x1 && tl v == x2}`C` {v : (L {VV : a | x <= VV}) | v == xs && 0 <= llen v}xs)
284:   | otherwise = {VV : a | VV == x}x x1:a
-> x2:(L {VV : a | x1 <= VV})
-> {v : (L a) | llen v == 1 + llen x2 && x1 v == x1 && hd v == x1 && tl v == x2 && x2 v == x2}`C` forall a. (Ord a) => a -> (L a) -> (L a)insert {VV : a | VV == y}y {v : (L {VV : a | x <= VV}) | v == xs && 0 <= llen v}xs
285: insert y N    = {VV : a | VV == y}y x1:a
-> x2:(L {VV : a | x1 <= VV})
-> {v : (L a) | llen v == 1 + llen x2 && x2 v == x2 && hd v == x1 && tl v == x2 && x1 v == x1}`C` {v : (L {VV : a | false}) | llen v == 0 && 0 <= llen v}N

Recap

Refinements: Types + Predicates
Subtyping: SMT Implication
Measures: Strengthened Constructors

Logic + Analysis for Collections

[continue]