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 -> 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