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!

Bad: Modification of run-time code.


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


{-@ (.) :: 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 Abstract Refinements