{#simplerefinements} ======================= Simple Refinement Types ----------------------- Simple Refinement Types ======================= Types + Predicates ------------------ Example: Integers equal to `0` ------------------------------
\begin{code} {-@ type Zero = {v:Int | v = 0} @-} {-@ zero :: Zero @-} zero = 0 \end{code}
Refinement types via special comments `{-@ ... @-}`
Demo
Refinements Are Predicates ========================== From A Decidable Logic ----------------------
1. Expressions 2. Predicates
**Refinement Logic: QF-UFLIA** Quant.-Free. Uninterpreted Functions and Linear Arithmetic
Expressions -----------
\begin{code}
e := x, y, z,... -- variable | 0, 1, 2,... -- constant | (e + e) -- addition | (e - e) -- subtraction | (c * e) -- linear multiplication | (f e1 ... en) -- uninterpreted function \end{code} Predicates ----------
\begin{code}
p := e -- atom | e1 == e2 -- equality | e1 < e2 -- ordering | (p && p) -- and | (p || p) -- or | (not p) -- negation \end{code}
Refinement Types ----------------
\begin{code}
b := Int | Bool | ... -- base types | a, b, c -- type variables t := {x:b | p} -- refined base | x:t -> t -- refined function \end{code} Subtyping Judgment ------------------
$$\boxed{\Gamma \vdash t_1 \preceq t_2}$$

Where **environment** $\Gamma$ is a sequence of binders
$$\Gamma \defeq \overline{\bindx{x_i}{t_i}}$$
Subtyping is Implication ------------------------ [PVS' Predicate Subtyping](http://pvs.csl.sri.com/papers/subtypes98/tse98.pdf)
(For **Base** Types ...) Subtyping is Implication ------------------------
$$ \begin{array}{rl} {\mathbf{If\ VC\ is\ Valid}} & \bigwedge_i P_i \Rightarrow Q \Rightarrow R \\ & \\ {\mathbf{Then}} & \overline{\bindx{x_i}{P_i}} \vdash \reft{v}{b}{Q} \subty \reft{v}{v}{R} \\ \end{array} $$ Example: Natural Numbers ------------------------
\begin{code}
type Nat = {v:Int | 0 <= v} \end{code}
$$ \begin{array}{rcrccll} \mathbf{VC\ is\ Valid:} & \True & \Rightarrow & v = 0 & \Rightarrow & 0 \leq v & \mbox{(by SMT)} \\ % & & & & & \\ \mathbf{So:} & \emptyset & \vdash & \Zero & \subty & \Nat & \\ \end{array} $$

Hence, we can type: \begin{code} {-@ zero' :: Nat @-} zero' = zero -- zero :: Zero <: Nat \end{code}
Contracts: Function Types ========================= {#as} ------ Pre-Conditions --------------
\begin{code} safeDiv n d = n `div` d -- crashes if d==0 \end{code}
**Requires** non-zero input divisor `d` \begin{code} {-@ type NonZero = {v:Int | v /= 0} @-} \end{code}

Specify pre-condition as **input type** \begin{code} {-@ safeDiv :: n:Int -> d:NonZero -> Int @-} \end{code}
Precondition: `safeDiv` ----------------------- Specify pre-condition as **input type** \begin{code}
{-@ safeDiv :: n:Int -> d:NonZero -> Int @-} \end{code}
Precondition is checked at **call-site** \begin{code} {-@ bad :: Nat -> Int @-} bad n = 10 `safeDiv` n \end{code}
**Rejected As** $$\bindx{n}{\Nat} \vdash \reftx{v}{v = n} \not \subty \reftx{v}{v \not = 0}$$
Precondition: `safeDiv` ----------------------- Specify pre-condition as **input type** \begin{code}
{-@ safeDiv :: n:Int -> d:NonZero -> Int @-} \end{code}
Precondition is checked at **call-site** \begin{code} {-@ ok :: Nat -> Int @-} ok n = 10 `safeDiv` (n+1) \end{code}
**Verifies As** $\bindx{n}{\Nat} \vdash \reftx{v}{v = n+1} \subty \reftx{v}{v \not = 0}$
Precondition: `safeDiv` ----------------------- Specify pre-condition as **input type** \begin{code}
{-@ safeDiv :: n:Int -> d:NonZero -> Int @-} \end{code}
Precondition is checked at **call-site** \begin{code}
{-@ ok :: Nat -> Int @-} ok n = 10 `safeDiv` (n+1) \end{code}
**Verifies As** $$(0 \leq n) \Rightarrow (v = n+1) \Rightarrow (v \not = 0)$$ Post-Conditions --------------- **Ensures** output is a `Nat` greater than input `x`. \begin{code} abs x | 0 <= x = x | otherwise = 0 - x \end{code}
Specify post-condition as **output type** \begin{code} {-@ abs :: x:Int -> {v:Nat | x <= v} @-} \end{code}

**Dependent Function Types** Outputs *refer to* inputs
Postcondition: `abs` -------------------- Specify post-condition as **output type** \begin{code}
{-@ abs :: x:Int -> {v:Nat | x <= v} @-} abs x | 0 <= x = x | otherwise = 0 - x \end{code}
Postcondition is checked at **return-site**
Postcondition: `abs` -------------------- Specify post-condition as **output type** \begin{code}
{-@ abs :: x:Int -> {v:Nat | x <= v} @-} abs x | 0 <= x = x | otherwise = 0 - x \end{code}
**Verified As**
$$\begin{array}{rll} \bindx{x}{\Int},\bindx{\_}{0 \leq x} & \vdash \reftx{v}{v = x} & \subty \reftx{v}{0 \leq v \wedge x \leq v} \\ \bindx{x}{\Int},\bindx{\_}{0 \not \leq x} & \vdash \reftx{v}{v = 0 - x} & \subty \reftx{v}{0 \leq v \wedge x \leq v} \\ \end{array}$$ Postcondition: `abs` -------------------- Specify post-condition as **output type** \begin{code}
{-@ abs :: x:Int -> {v:Nat | x <= v} @-} abs x | 0 <= x = x | otherwise = 0 - x \end{code}
**Verified As**
$$\begin{array}{rll} (0 \leq x) & \Rightarrow (v = x) & \Rightarrow (0 \leq v \wedge x \leq v) \\ (0 \not \leq x) & \Rightarrow (v = 0 - x) & \Rightarrow (0 \leq v \wedge x \leq v) \\ \end{array}$$ {#inference} ============= From Checking To Inference -------------------------- **So far** How to **check** code against given signature
**Next** How to **synthesize** signatures from code

**2-Phase Process** 1. H-M to synthesize *types* 2. A-I to synthesize *refinements*

Lets quickly look at 2.
From Checking To Inference ========================== Recipe ------
**Step 1. Templates** Types with variables $\kvar{}$ for *unknown* refinements

**Step 2. Constraints** Typecheck templates: VCs $\rightarrow$ Horn constraints over $\kvar{}$

**Step 3. Solve** Via least-fixpoint over suitable abstract domain
Step 1. Templates (`abs`) -------------------------
**Type** $$\bindx{x}{\Int} \rightarrow \Int$$

**Template** $$\ereft{x}{\Int}{\kvar{1}} \rightarrow \reft{v}{\Int}{\kvar{2}}$$
Step 2. Constraints (`abs`) -------------------------
Step 2. Constraints (`abs`) -------------------------
**Subtyping Queries**
$$ \begin{array}{rll} \bindx{x}{\kvar{1}},\bindx{\_}{0 \leq x} & \vdash \reftx{v}{v = x} & \subty \reftx{v}{\kvar{2}} \\ \bindx{x}{\kvar{1}},\bindx{\_}{0 \not \leq x} & \vdash \reftx{v}{v = 0 - x} & \subty \reftx{v}{\kvar{2}} \\ \end{array} $$ Step 2. Constraints (`abs`) -------------------------
**Verification Conditions**
$$\begin{array}{rll} {\kvar{1}} \wedge (0 \leq x) & \Rightarrow (v = x) & \Rightarrow \kvar{2} \\ {\kvar{1}} \wedge (0 \not \leq x) & \Rightarrow (v = 0 - x) & \Rightarrow \kvar{2} \\ \end{array}$$ Step 2. Constraints (`abs`) -------------------------
**Horn Constraints** over $\kvar{}$
$$\begin{array}{rll} {\kvar{1}} \wedge (0 \leq x) & \Rightarrow (v = x) & \Rightarrow \kvar{2} \\ {\kvar{1}} \wedge (0 \not \leq x) & \Rightarrow (v = 0 - x) & \Rightarrow \kvar{2} \\ \end{array}$$

**Note:** $\kvar{}$ occur positively, hence constraints are monotone. Step 3. Solve (`abs`) --------------------- Least-fixpoint over abstract domain
**Predicate Abstraction** Conjunction of predicates from (finite) ground set $\quals$

$$\mbox{e.g.}\ \quals \defeq \{ c \sim X \}$$
$$\begin{array}{ccll} c & \in & \{0,1,\ldots \} & \mbox{program constants} \\ X & \in & \{n,x,v,\ldots \} & \mbox{program variables} \\ \sim & \in & \{<, \leq, >, \geq, =, \not =\} & \mbox{comparisons} \\ \end{array}$$
Step 3. Solve (`abs`) --------------------- Least-fixpoint over abstract domain
**Predicate Abstraction** Conjunction of predicates from (finite) ground set $\quals$
+ Obtain $\quals$ via CEGAR + Or use other domains
[[Rybalchenko et al., CAV 2011]](http://goto.ucsd.edu/~rjhala/papers/hmc.html) Recipe Scales Up ----------------
**1. Templates** $\rightarrow$ **2. Horn Constraints** $\rightarrow$ **3. Fixpoint**
+ Define type checker, get inference for free + Scales to Data types, HO functions, Polymorphism

**Key Requirement** Refinements belong in abstract domain, e.g. QF-UFLIA
{#universalinvariants} ======================= Types = Universal Invariants ---------------------------- (Notoriously hard with *pure* SMT) Types Yield Universal Invariants ================================ Example: Lists --------------


\begin{code} data L a = N -- Empty | C a (L a) -- Cons \end{code}
How to **specify** every element in `nats` is non-negative? \begin{code} nats = 0 `C` 1 `C` 3 `C` N \end{code}
Example: Lists -------------- How to **specify** every element in `nats` is non-negative? \begin{code}
nats = 0 `C` 1 `C` 2 `C` N \end{code}
**Logic** $$\forall x \in \mathtt{nats}. 0 \leq x$$
VCs over **quantified formulas** ... *terrible* for SMT
Example: Lists -------------- How to **specify** every element in `nats` is non-negative? \begin{code}
nats = 0 `C` 1 `C` 2 `C` N \end{code}
**Refinement Types** \begin{code} {-@ nats :: L Nat @-} \end{code}
+
Type *implicitly* has quantification
+
Sub-typing *eliminates* quantifiers
+
Robust verification via *quantifier-free* VCs
Example: Lists -------------- How to **verify** ? \begin{code}
{-@ nats :: L Nat @-} nats = l0 where l0 = 0 `C` l1 -- Nat `C` L Nat >>> L Nat l1 = 1 `C` l2 -- Nat `C` L Nat >>> L Nat l2 = 2 `C` l3 -- Nat `C` L Nat >>> L Nat l3 = N -- L Nat \end{code}
Demo: What if `nats` contained `-2`?
Example: `range` ---------------- `(range i j)` returns `Int`s **between** `i` and `j` Example: `range` ---------------- `(range i j)` returns `Int`s **between** `i` and `j`
\begin{code} {-@ type Btwn I J = {v:_ | (I<=v && v \begin{code} {-@ range :: i:Int -> j:Int -> L (Btwn i j) @-} range i j = go i where go n | n < j = n `C` go (n + 1) | otherwise = N \end{code}
**Note:** Type of `go` is automatically inferred
Example: Indexing Into List --------------------------- \begin{code} (!) :: L a -> Int -> a (C x _) ! 0 = x (C _ xs) ! i = xs ! (i - 1) _ ! _ = liquidError "Oops!" \end{code}
(Mouseover to view type of `liquidError`)

To ensure safety, *require* `i` between `0` and list **length**

Need way to **measure** the length of a list [[continue...]](02_Measures.lhs.slides.html)