liquidhaskell-0.7.0.0: docs/slides/IHP14/lhs/01_SimpleRefinements.lhs
{#simplerefinements}
=======================
Simple Refinement Types
-----------------------
<div class="hidden">
\begin{code}
{-@ LIQUID "--no-termination" @-}
module SimpleRefinements where
import Language.Haskell.Liquid.Prelude
import Prelude hiding (abs, max)
-- boring haskell type sigs
zero :: Int
zero' :: Int
safeDiv :: Int -> Int -> Int
abs :: Int -> Int
nats :: L Int
evens :: L Int
odds :: L Int
range :: Int -> Int -> L Int
\end{code}
</div>
Simple Refinement Types
=======================
Types + Predicates
------------------
Example: Integers equal to `0`
------------------------------
<br>
\begin{code}
{-@ type Zero = {v:Int | v = 0} @-}
{-@ zero :: Zero @-}
zero = 0
\end{code}
<br>
<div class="fragment">
Refinement types via special comments `{-@ ... @-}`
<br>
<a href="http://goto.ucsd.edu:8090/index.html#?demo=HaskellSimpleRefinements.hs" target= "_blank">Demo</a>
</div>
Refinements Are Predicates
==========================
From A Decidable Logic
----------------------
<br>
1. Expressions
2. Predicates
<br>
<div class="fragment">
**Refinement Logic: QF-UFLIA**
Quant.-Free. Uninterpreted Functions and Linear Arithmetic
</div>
Expressions
-----------
<br>
\begin{code} <div/>
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
----------
<br>
\begin{code} <div/>
p := e -- atom
| e1 == e2 -- equality
| e1 < e2 -- ordering
| (p && p) -- and
| (p || p) -- or
| (not p) -- negation
\end{code}
<br>
Refinement Types
----------------
<br>
\begin{code}<div/>
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
------------------
<br>
$$\boxed{\Gamma \vdash t_1 \preceq t_2}$$
<div class="fragment">
<br>
Where **environment** $\Gamma$ is a sequence of binders
<br>
$$\Gamma \defeq \overline{\bindx{x_i}{t_i}}$$
</div>
Subtyping is Implication
------------------------
[PVS' Predicate Subtyping](http://pvs.csl.sri.com/papers/subtypes98/tse98.pdf)
<br>
(For **Base** Types ...)
Subtyping is Implication
------------------------
<br>
$$
\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
------------------------
<br>
\begin{code} <div/>
type Nat = {v:Int | 0 <= v}
\end{code}
<br>
<div class="fragment">
$$
\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}
$$
</div>
<br>
<div class="fragment">
Hence, we can type:
\begin{code}
{-@ zero' :: Nat @-}
zero' = zero -- zero :: Zero <: Nat
\end{code}
</div>
Contracts: Function Types
=========================
{#as}
------
Pre-Conditions
--------------
<br>
\begin{code}
safeDiv n d = n `div` d -- crashes if d==0
\end{code}
<br>
<div class="fragment">
**Requires** non-zero input divisor `d`
\begin{code}
{-@ type NonZero = {v:Int | v /= 0} @-}
\end{code}
</div>
<br>
<div class="fragment">
Specify pre-condition as **input type**
\begin{code}
{-@ safeDiv :: n:Int -> d:NonZero -> Int @-}
\end{code}
</div>
Precondition: `safeDiv`
-----------------------
Specify pre-condition as **input type**
\begin{code} <div/>
{-@ safeDiv :: n:Int -> d:NonZero -> Int @-}
\end{code}
<br>
Precondition is checked at **call-site**
\begin{code}
{-@ bad :: Nat -> Int @-}
bad n = 10 `safeDiv` n
\end{code}
<br>
<div class="fragment">
**Rejected As**
$$\bindx{n}{\Nat} \vdash \reftx{v}{v = n} \not \subty \reftx{v}{v \not = 0}$$
</div>
Precondition: `safeDiv`
-----------------------
Specify pre-condition as **input type**
\begin{code} <div/>
{-@ safeDiv :: n:Int -> d:NonZero -> Int @-}
\end{code}
<br>
Precondition is checked at **call-site**
\begin{code}
{-@ ok :: Nat -> Int @-}
ok n = 10 `safeDiv` (n+1)
\end{code}
<br>
<div class="fragment">
**Verifies As**
$\bindx{n}{\Nat} \vdash \reftx{v}{v = n+1} \subty \reftx{v}{v \not = 0}$
</div>
Precondition: `safeDiv`
-----------------------
Specify pre-condition as **input type**
\begin{code} <div/>
{-@ safeDiv :: n:Int -> d:NonZero -> Int @-}
\end{code}
<br>
Precondition is checked at **call-site**
\begin{code} <div/>
{-@ ok :: Nat -> Int @-}
ok n = 10 `safeDiv` (n+1)
\end{code}
<br>
**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}
<br>
<div class="fragment">
Specify post-condition as **output type**
\begin{code}
{-@ abs :: x:Int -> {v:Nat | x <= v} @-}
\end{code}
</div>
<br>
<div class="fragment">
**Dependent Function Types**
Outputs *refer to* inputs
</div>
Postcondition: `abs`
--------------------
Specify post-condition as **output type**
\begin{code} <div/>
{-@ abs :: x:Int -> {v:Nat | x <= v} @-}
abs x | 0 <= x = x
| otherwise = 0 - x
\end{code}
<br>
Postcondition is checked at **return-site**
<br>
Postcondition: `abs`
--------------------
Specify post-condition as **output type**
\begin{code} <div/>
{-@ abs :: x:Int -> {v:Nat | x <= v} @-}
abs x | 0 <= x = x
| otherwise = 0 - x
\end{code}
<br>
**Verified As**
<br>
$$\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} <div/>
{-@ abs :: x:Int -> {v:Nat | x <= v} @-}
abs x | 0 <= x = x
| otherwise = 0 - x
\end{code}
<br>
**Verified As**
<br>
$$\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
<br>
<div class="fragment">
**Next**
How to **synthesize** signatures from code
</div>
<br>
<div class="fragment">
**2-Phase Process**
1. H-M to synthesize *types*
2. A-I to synthesize *refinements*
</div>
<br>
<div class="fragment">Lets quickly look at 2. </div>
From Checking To Inference
==========================
Recipe
------
<br>
<div class="fragment">
**Step 1. Templates**
Types with variables $\kvar{}$ for *unknown* refinements
</div>
<br>
<div class="fragment">
**Step 2. Constraints**
Typecheck templates: VCs $\rightarrow$ Horn constraints over $\kvar{}$
</div>
<br>
<div class="fragment">
**Step 3. Solve**
Via least-fixpoint over suitable abstract domain
</div>
Step 1. Templates (`abs`)
-------------------------
<br>
<div class="fragment">
**Type**
$$\bindx{x}{\Int} \rightarrow \Int$$
</div>
<br>
<div class="fragment">
**Template**
$$\ereft{x}{\Int}{\kvar{1}} \rightarrow \reft{v}{\Int}{\kvar{2}}$$
</div>
Step 2. Constraints (`abs`)
-------------------------
<br>
Step 2. Constraints (`abs`)
-------------------------
<br>
**Subtyping Queries**
<br>
$$
\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`)
-------------------------
<br>
**Verification Conditions**
<br>
$$\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`)
-------------------------
<br>
**Horn Constraints** over $\kvar{}$
<br>
$$\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}$$
<br>
<br>
**Note:** $\kvar{}$ occur positively, hence constraints are monotone.
Step 3. Solve (`abs`)
---------------------
Least-fixpoint over abstract domain
<br>
<div class="fragment">
**Predicate Abstraction**
Conjunction of predicates from (finite) ground set $\quals$
</div>
<br>
<div class="fragment">
$$\mbox{e.g.}\ \quals \defeq \{ c \sim X \}$$
<br>
$$\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}$$
</div>
Step 3. Solve (`abs`)
---------------------
Least-fixpoint over abstract domain
<br>
**Predicate Abstraction**
Conjunction of predicates from (finite) ground set $\quals$
<br>
+ Obtain $\quals$ via CEGAR
+ Or use other domains
<br>
[[Rybalchenko et al., CAV 2011]](http://goto.ucsd.edu/~rjhala/papers/hmc.html)
Recipe Scales Up
----------------
<br>
**1. Templates** $\rightarrow$ **2. Horn Constraints** $\rightarrow$ **3. Fixpoint**
<br>
<div class="fragment">
+ Define type checker, get inference for free
+ Scales to Data types, HO functions, Polymorphism
</div>
<br>
<div class="fragment">
**Key Requirement**
Refinements belong in abstract domain, e.g. QF-UFLIA
</div>
{#universalinvariants}
=======================
Types = Universal Invariants
----------------------------
(Notoriously hard with *pure* SMT)
Types Yield Universal Invariants
================================
Example: Lists
--------------
<div class="hidden">
\begin{code}
infixr `C`
\end{code}
</div>
<br>
<br>
<br>
\begin{code}
data L a = N -- Empty
| C a (L a) -- Cons
\end{code}
<br>
<div class="fragment">
How to **specify** every element in `nats` is non-negative?
\begin{code}
nats = 0 `C` 1 `C` 3 `C` N
\end{code}
</div>
Example: Lists
--------------
How to **specify** every element in `nats` is non-negative?
\begin{code} <div/>
nats = 0 `C` 1 `C` 2 `C` N
\end{code}
<br>
**Logic**
$$\forall x \in \mathtt{nats}. 0 \leq x$$
<br>
<div class="fragment">
VCs over **quantified formulas** ... *terrible* for SMT
</div>
Example: Lists
--------------
How to **specify** every element in `nats` is non-negative?
\begin{code} <div/>
nats = 0 `C` 1 `C` 2 `C` N
\end{code}
<br>
**Refinement Types**
\begin{code}
{-@ nats :: L Nat @-}
\end{code}
<br>
+ <div class="fragment">Type *implicitly* has quantification</div>
+ <div class="fragment">Sub-typing *eliminates* quantifiers</div>
+ <div class="fragment">Robust verification via *quantifier-free* VCs</div>
Example: Lists
--------------
How to **verify** ?
\begin{code} <div/>
{-@ 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}
<br>
<div class="fragment">
<a href="http://goto.ucsd.edu:8090/index.html#?demo=HaskellSimpleRefinements.hs" target= "_blank">Demo:</a>
What if `nats` contained `-2`?
</div>
<!--
Example: Even/Odd Lists
-----------------------
\begin{code}
{-@ type Even = {v:Int | v mod 2 = 0} @-}
{-@ type Odd = {v:Int | v mod 2 /= 0} @-}
\end{code}
<br>
<div class="fragment">
\begin{code}
{-@ evens :: L Even @-}
evens = 0 `C` 2 `C` 4 `C` N
{-@ odds :: L Odd @-}
odds = 1 `C` 3 `C` 5 `C` N
\end{code}
</div>
<br>
<div class="fragment">
<a href="http://goto.ucsd.edu:8090/index.html#?demo=HaskellSimpleRefinements.hs" target= "_blank">Demo:</a>
What if `evens` contained `1`?
</div>
-->
Example: `range`
----------------
`(range i j)` returns `Int`s **between** `i` and `j`
Example: `range`
----------------
`(range i j)` returns `Int`s **between** `i` and `j`
<br>
\begin{code}
{-@ type Btwn I J = {v:_ | (I<=v && v<J)} @-}
\end{code}
Example: `range`
----------------
`(range i j)` returns `Int`s between `i` and `j`
<br>
\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}
<br>
<div class="fragment">
**Note:** Type of `go` is automatically inferred
</div>
Example: Indexing Into List
---------------------------
\begin{code}
(!) :: L a -> Int -> a
(C x _) ! 0 = x
(C _ xs) ! i = xs ! (i - 1)
_ ! _ = liquidError "Oops!"
\end{code}
<br>
<div class="fragment">(Mouseover to view type of `liquidError`)</div>
<br>
<div class="fragment">To ensure safety, *require* `i` between `0` and list **length**</div>
<br>
<div class="fragment">Need way to **measure** the length of a list [[continue...]](02_Measures.lhs.slides.html)</div>