{#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>