Language-Integrated Verification

Specifications

Verification

Inference

Collections & HOFs

Refinements for Datatypes

Specifications

Verification

Inference

Collections & HOFs

Refinements for Datatypes

Specifications

Property: In-bounds Array Access

Specifications

Property: In-bounds Array Access

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

Specifications: Pre-Conditions

What does a function require for correct execution?

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

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} @-}
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Refinement on the function's output type

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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Oops! What gives?

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

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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

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

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

Synthesized Solution

$\kvar{}{v} = 0 \leq v$

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 = []
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

(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)
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

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

Types make refinement inference "just work" ...

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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Yikes! average requires non-empty lists!

Lift (some) functions into specification logic:

{-@ measure length @-}
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

which lets us define a type alias

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

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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Measures

Specify properties as functions over datatypes

Measures

Specify properties as functions over datatypes

Refined Constructors

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

Measures

Specify properties as functions over datatypes

Refined Constructors

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

Automate verification of data types

Specifications

Verification

Inference

Collections & HOFs

Refinements for Datatypes

Outline

Motivation

Refinements 101

Refinements by Example

Outline

Motivation

Refinements 101

Refinements by Example

How to Avoid Infinite Loops

Refinement Types by Example

Refinement Types by Example

Refinement Types by Example

Refinement Types by Example

Specifications: Pre-Conditions

Specifications: Post-Conditions

Refinement Types by Example

Verification: Vector Sum

Verification: Vector Sum

Verification: Vector Sum

Refinement Types by Example

Inference

Inference: Vector Sum

Inference: Vector Sum

Inference: Vector Sum

Inference: Vector Sum

Inference: Vector Sum

Inference: Vector Sum

Refinement Types by Example

Collections & Higher-Order Functions

Collections & Higher-Order Functions

Collections & Higher-Order Functions

Collections & Higher-Order Functions

Refinement Types by Example

Example: List `average`

Measures Yield Refined Constructors

Example: `map` over Lists

Refinement Types by Example

Outline

Outline

loading

Refinement Types by Example

Refinement Types by Example

Refinement Types by Example

Refinement Types by Example

Specifications: Pre-Conditions

Specifications: Post-Conditions

Refinement Types by Example

Verification: Vector Sum

Verification: Vector Sum

Verification: Vector Sum

Refinement Types by Example

Inference

Inference: Vector Sum

Inference: Vector Sum

Inference: Vector Sum

Inference: Vector Sum

Inference: Vector Sum

Inference: Vector Sum

Refinement Types by Example

Collections & Higher-Order Functions

Collections & Higher-Order Functions

Collections & Higher-Order Functions

Collections & Higher-Order Functions

Refinement Types by Example

Example: List average

Refinements for Datatypes

Measures Yield Refined Constructors

Example: map over Lists

Refinements for Datatypes

Refinements for Datatypes

Refinements for Datatypes

Refinement Types by Example

Outline

Outline

loading

Example: List `average`

Example: `map` over Lists