# 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 -> Prop , tlprop :: a -> Prop , p :: a -> a -> Prop>. (RecProp a hdprop tlprop p) => [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


## Verification of compose

You should know compose:

(.) f g x = f (g x)

What type of compose can verify the following?

{-@ incr2 :: n:Int -> {v:Int| v = n + 2} @-} incr2 = incr . incr {-@ incr :: n:Int -> {v:Int| v = n + 1} @-} incr x = x + 1

## Specification of Compose

Abstract over refinements of input functions:

{-@ (.) :: forall < p :: b -> c -> Prop, q :: a -> b -> Prop, r :: a -> c -> Prop>. (Chain b c a p q r) => (y:b -> c< p y >) -> (z:a -> b< q z >) -> x:a -> c< r x > @-}

## Specification of Compose

Relate refinements of input functions:

{-@ bound chain @-} chain p q r = \ x y z -> q x y ==> p y z ==> r x z

## Call compose

Discharge compose bound at call site:

{-@ incr2 :: n:Int -> {v:Int| v = n + 2} @-}
incr2     =  incr . incr

{-@ incr  :: n:Int -> {v:Int| v = n + 1} @-}
incr x    = x + 1


Abstract Refinement Instantiation:
p, q := \n v -> v = n + 1
r := \n v -> v = n + 2


Bound Instantiation:
Chain =
\ x y z -> y = x + 1 ==> z = y + 1 ==> z = x + 2


## 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 Absract Refinements