Simple Refinement Types

Refinement Types = Types + Predicates

Types

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

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

p is a predicate from a decidable logic

Predicates

Quantifier-Free Logic of Uninterpreted Functions & Linear Arithmetic

Predicates

Quantifier-Free Logic of Uninterpreted Functions & Linear Arithmetic

e := x, y, z, ...         -- variables
   | 0, 1, 2, ...         -- constants
   | e + e | c * e | ...  -- arithmetic
   | f e1 ... en          -- uninterpreted function

Predicates

Quantifier-Free Logic of Uninterpreted Functions & Linear Arithmetic

e := x, y, z, ...         -- variables
   | 0, 1, 2, ...         -- constants
   | e + e | c * e | ...  -- arithmetic
   | f e1 ... en          -- uninterpreted function

Uninterpreted Functions

\[\forall \overline{x}, \overline{y}.\ \overline{x} = \overline{y}\ \Rightarrow\ f(x) = f(y)\]

Predicates

Quantifier-Free Logic of Uninterpreted Functions & Linear Arithmetic

e := x, y, z, ...         -- variables
   | 0, 1, 2, ...         -- constants
   | e + e | c * e | ...  -- arithmetic
   | f e1 ... en          -- uninterpreted function

p := e <= e | ...         -- atoms
   | p && p | p || p | !p -- boolean combinations

Predicates

Quantifier-Free Logic of Uninterpreted Functions & Linear Arithmetic

Given a Verification Condition (VC)

\[p_1 \Rightarrow p_2\]

SMT solvers can decide if VC is Valid ("always true")

Example: Singletons

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

Example: Natural Numbers

A Term Can Have Many Types

What is the type of 0 ?

1. Predicate Subtyping [NUPRL, PVS]

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

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

1. Predicate Subtyping [NUPRL, PVS]

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

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

Where environment \(\Gamma\) is a sequence of in-scope binders

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

1. Predicate Subtyping [NUPRL, PVS]

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

\[\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} \]

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:

2. Typing Applications (Function Calls)

Terms built up by applications.

How to prove four :: Nat ?

2. Typing Applications (Function Calls)

Dependent Application

\[\begin{array}{rl} {\mathbf{If}} & \Gamma \vdash f :: \bindx{x}{s} \rightarrow t \\ & \Gamma \vdash y :: s \\ {\mathbf{Then}} & \Gamma \vdash f\ y :: t[x \mapsto y] \\ \end{array}\]

i.e. Output type with formals substituted by actuals

2. Typing Applications (Function Calls)

Dependent Application: Example

\[ \begin{array}{rl} {\mathbf{If}} & \Gamma \vdash (+) :: \bindx{a}{\Int} \rightarrow \bindx{b}{\Int} \rightarrow \reft{v}{\Int}{v = a + b} \\ & \Gamma \vdash x :: \Int \\ & \Gamma \vdash 1 :: \Int \\ & \\ {\mathbf{Then}} & \Gamma \vdash x + 1 :: \reft{v}{\Int}{v = x + 1} \end{array} \]

2. Typing Applications (Function Calls)

And so, we can type:

Recap: Refinement Types 101

Refinement Types

Types + Predicates

Recap: Refinement Types 101

Refinement Types

Types + Predicates

Refinement Checking

Dependent Application + Predicate Subtyping

Recap: Refinement Types 101

Refinement Types

Types + Predicates

Refinement Checking

Dependent Application + Predicate Subtyping

[Eliminates boring proofs & Makes Verification Practical]

Outline

Motivation

Refinements 101

Outline

Motivation

Refinements 101

Refinements by Example