Basic 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 SMT 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

Congruence Axiom for 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 \ldots \Rightarrow p_n\]

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

Example: "Singletons"

The alias Zero describes a type inhabited by a single Int value 0

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

Exercise: What happens if you modify the code or type?

Example: Natural Numbers

Exercise: What happens if you modify the code or type?

A Term Can Have Many Types

What is the type of 0 ?

Is it {v:Int|v=0} or is it {v:Int|0<=v} ?

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 \(\Gamma\) is variable-and-type bindings that are in-scope

\[\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 function-applications.

2. Typing Applications (Function Calls)

Terms built up by function-applications.

Built-in Functions

                  plus  :: x:Int -> y:Int -> {v:Int|v = x + y} 
                  minus :: x:Int -> y:Int -> {v:Int|v = x - y} 

Output Type is a Post-Condition

Specifies the output value equals the sum/difference of the inputs

2. Typing Applications (Function Calls)

Terms built up by function-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 \mathit{plus} :: \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 \mathit{plus}\ x\ 1 :: \reft{v}{\Int}{v = x + 1} \end{array} \]

2. Typing Applications (Function Calls)

And so, we can type:

Exercise: What happens if you replace plus with minus?

2. Typing Applications (Function Calls)

Similarly, we can type:

Exercise: Now, what happens if you replace plus with minus?

Recap: Basic Refinement Types

Refinement Types

Types + Predicates

Recap: Basic Refinement Types

Refinement Types

Types + Predicates

Refinement Checking

Dependent Application + Predicate Subtyping

Recap: Refinement Types 101

Refinement Types

Types + Predicates

Refinement Checking

Dependent Application + Predicate Subtyping

Plan

Part I: Refinements 101

Case Study: Vector Bounds

Part II: Properties of Structures

Case Study: Sorting, Interpreter

Part III: Invariants of Data Structures

Case Study: Sorting actually Sorts Lists

Part IV: Termination and Correctness Proofs

Case Study: Optimizing Arithmetic Expressions