Simple Refinement Types


Refinement Types = Types + Predicates

Types


b := Int         -- base types
   | Bool
   | ...
   | a, b, c     -- type variables

t := {x:b | p}   -- refined base
   | x:t -> t    -- refined function

p := ...         -- predicate in decidable logic

Predicates


p := e           -- atom
   | e1 == e2    -- equality
   | e1 <  e2    -- ordering
   | (p && p)    -- and
   | (p || p)    -- or
   | (not p)     -- negation


Expressions

e := x, y, z,...    -- variable
   | 0, 1, 2,...    -- constant
   | (e + e)        -- addition
   | (e - e)        -- subtraction
   | (c * e)        -- linear multiplication
   | (f e1 ... en)  -- uninterpreted function

Refinement Logic: QF-UFLIA

Quantifier-Free Logic of Uninterpreted Functions and Linear Arithmetic

Example: Integers equal to 0


{-@ type Zero = {v:Int | v = 0} @-} {-@ zero :: Zero @-} zero = 0


Refinement types via special comments {-@ ... @-}

Example: Natural Numbers


{-@ type Nat = {v:Int | 0 <= v} @-} {-@ nats :: [Nat] @-} nats = [0, 1, 2, 3]


Exercise: Positive Integers


{-@ type Pos = {v:Int | 0 <= v} @-} {-@ poss :: [Pos] @-} poss = [0, 1, 2, 3]

Q: First, can you fix Pos so poss is rejected?

Q: Next, can you modify poss so it is accepted?

Refinement Type Checking


A Term Can Have Many Types


A Term Can Have Many Types


{-@ zeroA :: Zero @-} zeroA = 0 {-@ zeroB :: Nat @-} zeroB = 0


Predicate Subtyping [NUPRL, PVS]


In environment \(\Gamma\) the type \(t_1\) is a subtype of the type \(t_2\)

\[\boxed{\Gamma \vdash t_1 \preceq t_2}\]


Environment \(\Gamma\) is a sequence of binders

\[\Gamma \doteq \overline{\bindx{x_i}{P_i}}\]


Predicate Subtyping [NUPRL, PVS]


\[\boxed{\Gamma \vdash t_1 \preceq t_2}\]


\[ \begin{array}{rll} {\mathbf{If\ VC\ is\ Valid}} & \bigwedge_i P_i \Rightarrow Q \Rightarrow R & (\mbox{By SMT}) \\ & & \\ {\mathbf{Then}} & \overline{\bindx{x_i}{P_i}} \vdash \reft{v}{b}{Q} \preceq \reft{v}{b}{R} & \\ \end{array} \]


Example: Natural Numbers


\[ \begin{array}{rcrccll} \mathbf{VC\ is\ Valid:} & \True & \Rightarrow & v = 0 & \Rightarrow & 0 \leq v & \mbox{(by SMT)} \\ & & & & & & \\ \mathbf{So:} & \emptyset & \vdash & \Zero & \preceq & \Nat & \\ \end{array} \]

And so, we can type:

{-@ zero' :: Nat @-} zero' = zero -- zero :: Zero <: Nat


Example: Natural Numbers


\[ \begin{array}{rcrccll} \mathbf{VC\ is\ Valid:} & x = 3 & \Rightarrow & v = x + 1 & \Rightarrow & 0 \leq v & \mbox{(by SMT)} \\ & & & & & \\ \mathbf{So:} & x = 3 & \vdash & \Zero & \preceq & \Nat & \\ \end{array} \]

And so, we can type:

{-@ four :: Nat @-} four = x + 1 -- x = 3 |- {v = x + 1} <: Nat where x = 3

SMT Automates Subtyping


Eliminates boring proofs ... makes verification practical.



Contracts: Function Types


Pre-Conditions


{-@ impossible :: {v:_ | false} -> a @-} impossible msg = error msg


No value satisfies false \(\Rightarrow\) no valid inputs for impossible

Program type-checks \(\Rightarrow\) impossible never called at run-time


Exercise: Pre-Conditions


Let's write a safe division function

{-@ safeDiv :: Int -> Int -> Int @-} safeDiv _ 0 = impossible "divide-by-zero" safeDiv x n = x `div` n


Q: Yikes! Can you fix the type of safeDiv to banish the error?

Precondition Checked at Call-Site


avg2 x y = safeDiv (x + y) 2

Precondition

{-@ safeDiv :: n:Int -> d:NonZero -> Int @-}

Verifies As

\[\inferrule{}{(v = 2) \Rightarrow (v \not = 0)} {\bindx{x}{\Int}, \bindx{y}{\Int} \vdash \reftx{v}{v = 2} \preceq \reftx{v}{v \not = 0}} \]

Exercise: Check That Data


calc :: IO () calc = do putStrLn "Enter numerator" n <- readLn putStrLn "Enter denominator" d <- readLn putStrLn ("Result = " ++ show (safeDiv n d)) calc

Q: Can you fix calc so it typechecks?

Precondition Checked at Call-Site


avg :: [Int] -> Int avg xs = safeDiv total n where total = sum xs n = length xs -- returns a Nat

Rejected as n can be any Nat

\[0 \leq n \Rightarrow (v = n) \not \Rightarrow (v \not = 0)\]

size returns positive values


Specify post-condition as output type


{-@ size :: [a] -> Pos @-} size [_] = 1 size (_:xs) = 1 + size xs -- size _ = impossible "size"

Postconditions Checked at Return


{-@ size    :: [a] -> Pos @-}
size [_]    = 1                        -- (1)
size (_:xs) = 1 + n  where n = size xs -- (2)

Verified As

\[\begin{array}{rll} \True & \Rightarrow (v = 1) & \Rightarrow (0 < v) & \qquad \mbox{at (1)} \\ (0 < n) & \Rightarrow (v = 1 + n) & \Rightarrow (0 < v) & \qquad \mbox{at (2)} \\ \end{array}\]

Verifying avg


avg' xs = safeDiv total n where total = sum xs n = size xs -- returns a Pos

Verifies As

\[(0 < n) \Rightarrow (v = n) \Rightarrow (v \not = 0)\]


Recap


Refinements: Types + Predicates
Specification: Refined Input/Output Types
Verification: SMT-based Predicate Subtyping

Unfinished Business


How to prevent calling size with empty lists?

{-@ size' :: [a] -> Pos @-} size' [_] = 1 size' (_:xs) = 1 + size' xs size' _ = impossible "size"


Next: How to describe properties of structures [continue...]