Refinement Types by Example


Specifications

Verification

Inference

Collections & HOFs

Refinements for Datatypes

Refinement Types by Example


Specifications

Verification

Inference

Collections & HOFs

Refinements for Datatypes

Refinement Types by Example


Specifications


Property: In-bounds Array Access

Refinement Types by Example


Specifications


Property: In-bounds Array Access

{-@ measure vlen :: Vector a -> Int @-}

Specifications: Pre-Conditions


What does a function require for correct execution?


{-@ at :: vec:Vector a -> {i:Nat| i < vlen vec} -> a @-}

Refinement on the function's input type

Specifications: Post-Conditions


What does a function ensure about its result?


{-@ size :: v:Vector a -> {n:Int | n == vlen v} @-}

Refinement on the function's output type

Refinement Types by Example


Specifications

Verification

Inference

Collections & HOFs

Refinements for Datatypes

Verification: Vector Sum


sum :: Vector Int -> Int sum v = loop 0 where {-@ loop :: Nat -> Int @-} loop i | i <= size v = at v i + loop (i + 1) | otherwise = 0

Oops! What gives?

Verification: Vector Sum

Verification: Vector Sum

Verification Conditions

\[\begin{array}{lll} \True & \Rightarrow v = 0 & \Rightarrow 0 \leq v & \mbox{(A)} \\ 0 \leq i \wedge n = \mathit{vlen}\ v \wedge i < n & \Rightarrow v = i + 1 & \Rightarrow 0 \leq v & \mbox{(B)} \\ 0 \leq i \wedge n = \mathit{vlen}\ v \wedge i < n & \Rightarrow v = i & \Rightarrow 0 \leq v < \mathit{vlen}\ v & \mbox{(C)} \\ \end{array}\]

Refinement Types by Example


Specifications

Verification

Inference

Collections & HOFs

Refinements for Datatypes

Inference


The more interesting your types get,
the less fun it is to write them down.

                   -- Benjamin Pierce

Inference: Vector Sum


sum' :: Vector Int -> Int sum' v = loop 0 where {-@ loop :: _ -> _ @-} loop i | i < size v = at v i + loop (i + 1) | otherwise = 0

Inference: Vector Sum


Not magic, just Abstract Interpretation

Inference: Vector Sum


Not magic, just Abstract Interpretation

Represent unknown refinements with \(\kvar{}{\cdot}\) variables ...

... Solve resulting Horn Constraints


[PLDI 2008]

Inference: Vector Sum

Inference: Vector Sum

Horn Constraints

\[\begin{array}{lll} \True & \Rightarrow v = 0 & \Rightarrow \kvar{}{v} & \mbox{(A)} \\ \kvar{}{i} \wedge n = \mathit{vlen}\ v \wedge i < n & \Rightarrow v = i + 1 & \Rightarrow \kvar{}{v} & \mbox{(B)} \\ \kvar{}{i} \wedge n = \mathit{vlen}\ v \wedge i < n & \Rightarrow v = i & \Rightarrow 0 \leq v < \mathit{vlen}\ v & \mbox{(C)} \\ \end{array}\]

Inference: Vector Sum


Horn Constraints

\[\begin{array}{lll} \True & \Rightarrow v = 0 & \Rightarrow \kvar{}{v} & \mbox{(A)} \\ \kvar{}{i} \wedge n = \mathit{vlen}\ v \wedge i < n & \Rightarrow v = i + 1 & \Rightarrow \kvar{}{v} & \mbox{(B)} \\ \kvar{}{i} \wedge n = \mathit{vlen}\ v \wedge i < n & \Rightarrow v = i & \Rightarrow 0 \leq v < \mathit{vlen}\ v & \mbox{(C)} \\ \end{array}\]


Synthesized Solution

\[\kvar{}{v} = 0 \leq v\]

Refinement Types by Example


Specifications

Verification

Inference

Collections & HOFs

Refinements for Datatypes

Collections & Higher-Order Functions


Composition >> Recursion!

Collections & Higher-Order Functions


Generic Sequences

range lo hi | lo < hi = lo : range (lo + 1) hi | otherwise = []

(What's a good type for range?)

Collections & Higher-Order Functions


Fold over Sequences

foldr :: (a -> b -> b) -> b -> [a] -> b foldr f b [] = b foldr f b (x:xs) = f x (foldr f b xs)

Collections & Higher-Order Functions


"Wholemeal" Vector Sum

sum'' :: Vector Int -> Int sum'' v = foldr add 0 is where add = \i n -> n + at v i is = range 0 (size v)

Types make refinement inference "just work" ...

Refinement Types by Example


Specifications

Verification

Inference

Collections & HOFs

Refinements for Datatypes

Example: List average

{-@ average :: [Int] -> Int @-} average xs = total `div` n where total = foldr (+) 0 xs n = length xs length :: [a] -> Int length [] = 0 length (_:xs) = 1 + length xs

Yikes! average requires non-empty lists!

Refinements for Datatypes

Lift (some) functions into specification logic:

{-@ measure length @-}

which lets us define a type alias

{-@ type ListNE a = {v:[a] | 0 < length v} @-}

Now lets go back and fix average ...

Measures Yield Refined Constructors

Lift (some) functions into specification logic:

data [a] where
  []  :: {v:[a] | length v = 0}
  (:) :: a
      -> t:[a]
      -> {v:[a] | length v = 1 + length t}

Where length is uninterpreted in refinement Logic

Example: map over Lists

What's the problem here? (Lets fix it!)

{-@ hwAverage :: ListNE (a, Int) -> Int @-} hwAverage nxs = average (map snd nxs) {-@ map :: (a -> b) -> [a] -> [b] @-} map f [] = [] map f (x:xs) = f x : map f xs

Refinements for Datatypes


Measures

Specify properties as functions over datatypes

Refinements for Datatypes


Measures

Specify properties as functions over datatypes


Refined Constructors

Instantiate constraints at fold (C ...) & unfold (case-of)

Refinements for Datatypes


Measures

Specify properties as functions over datatypes


Refined Constructors

Instantiate constraints at fold (C ...) & unfold (case-of)


Automate verification of data types

Refinement Types by Example


Specifications

Verification

Inference

Collections & HOFs

Refinements for Datatypes