# Simple Refinement Types

{-@ LIQUID "--no-termination" @-} module SimpleRefinements where import Prelude hiding (abs, max)

# Simple Refinement Types

Refinement Types = Types + Predicates

# Example: Integers equal to 0

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

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

# Example: Natural Numbers

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

# Exercise: Positive Integers

{-@ type Pos = {v:Int | 0 <= v} @-} {-@ poss :: [Pos] @-} poss :: [Int] 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?

# Type Checking

{-@ type Pos = {v:Int | 0 < v} @-}

{-@ poss :: [Pos]               @-}
poss     =  [1, 2, 3]


Type Checking Via Implication Checking.

v = 1 => 0 < v
v = 2 => 0 < v
v = 3 => 0 < v


# SMTs to Automate Type Checking

{-@ type Pos = {v:Int | 0 < v} @-}


Refinements Drawn from Decidable logics.

For automatic, decidable (and thus predictable) SMT type checking.

# A Term Can Have Many Types

What is the type of 0 ?

{-@ zero  :: Zero @-}
zero      = 0

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


# 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' :: Int 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 & \{v:Int\ |\ v = x + 1\} & \preceq & \Nat & \\ \end{array}$

And so, we can type:

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

# SMT Automates Implication Checking

Eliminates boring proofs ... makes verification practical.

# Pre-Conditions

{-@ impossible :: {v:_ | false} -> a @-} impossible :: String -> 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

{-@ type NonZero = {v:Int | v /= 0} @-} {-@ safeDiv :: Int -> Int -> Int @-} safeDiv :: Int -> Int -> Int safeDiv _ 0 = undefined -- 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 :: Int -> Int -> Int avg2 x y = safeDiv (x + y) 2

Precondition

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


Verifies As

${(v = 2) \Rightarrow (v \not = 0)}$

# 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)$

How to talk about list length in logic?

# Recap

Refinement Types Types + Predicates

Specify Properties

Via Refined Input- and Output- Types

Verify Properties

Via SMT based Implication Checking

{-@ avg :: {v:[a]| 0 < length v } -> Pos @-}