Bounded Refinement Types

Relating Abstract Refinements

Verification of QuickSort (I)

{-@ qsort1 :: xs:[a] -> IList a @-} qsort1 [] = [] qsort1 (x:xs) = append1 listLess (x:listGEq) where listLess = qsort1 [y | y <- xs, y < x] -- :: IList {y:a | y < x} listGEq = qsort1 [z | z <- xs, z >= x] -- :: IList {y:a | y < x}

append1 :: [a] -> [a] -> [a] append1 [] ys = ys append1 (x:xs) ys = x:append1 xs ys

Ghost Variables

Good: Bring info in scope for verification!

Ugly: Pollute the code.

Verification of append

{-@ append :: x:a -> IList {hd:a | hd < x} -> IList {tl:a | x <= tl} -> IList a @-} append _ [] ws = ws append x (y:ys) ws = y:append x ys ws

Verification requirement:

hdProp  = \hd -> hd < x      -- property of head elements
tlProp  = \tl -> x <= tl     -- property of tail elements
----------------------------------------------------------
recProp = \hd tl -> hd <= tl -- recursive (sorted) list

Abstracting over Properties:

forall hd tl. hdProp hd => tlProp tl => recProp hd tl

Note: Abstract requirement is independent of x!

Bounds on Abstract Refinements

Turn Requirement:

forall hd tl. hdProp hd => tlProp tl => recProp hd tl

Into a Bound: Haskell function that relates abstract refinements

{- bound recProp @-} recProp hdProp tlProp recProp = \hd tl -> hdProp hd ==> tlProp tl ==> recProp hd tl

Bound Abstraction

{-@ (++) :: forall < hdprop :: a -> Bool , tlprop :: a -> Bool , p :: a -> a -> Bool>. {hd :: a < hdprop >|- a< tlprop > <: a < p hd >} [a< hdprop >]< p > -> [a< tlprop >]< p > -> [a]< p > @-} (++) [] ys = ys (++) (x:xs) ys = x:(xs ++ ys)

Bound RecProp combines

• the recursive property p
• the property of each head hdprop
• the property of tail elements tlprop

Bound Instantiations

{-@ qsort :: xs:[a] -> IList a @-} qsort [] = [] qsort (x:xs) = listLess ++ (x:listGEq) -- :: IList a == [a]<{\hd tl -> hd <= tl}> where listLess = qsort [y | y <- xs, y < x ] -- :: IList {y:a | y < x} listGEq = qsort [z | z <- xs, z >= x] -- :: IList {z:a | x <= z}

Abstract Refinement Instantiation:
recProp = \hd tl -> hd <= tl -- recursive (sort) property
hdProp  = \hd -> hd < x      -- property of head elements
tlProp  = \tl -> x <= tl     -- property of tail elements

Bound Instantiation:

recProp
= \hd tl -> hd < x  ==> x <= tl ==>  hd <= tl

Recap

1. Refinements: Types + Predicates
2. Subtyping: SMT Implication
3. Measures: Specify Properties of Data
4. Abstract Refinements: Decouple properties from code
5. Bounded Refinements: Relating Abstract Refinements