# Simple Refinement Types

## Ex: `Int`egers equal to `0`

```43: {-@ type EqZero = {v:Int | v = 0} @-}
44:
45: {-@ zero :: EqZero @-}
46: {v : Int | (v == 0)}zero     =  x1:Int# -> {x2 : Int | (x2 == (x1  :  int))}0
```

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

Demo

# Refinements Are Predicates

1. Expressions

2. Predicates

## Expressions

```78: e := x, y, z,...      -- variable
79:    | 0, 1, 2,...      -- constant
80:    | (e + e)          -- addition
81:    | (e - e)          -- subtraction
82:    | (c * e)          -- linear multiplication
83:    | (v e1 e2 ... en) -- uninterpreted function
```

## Predicates

```92: p := e           -- atom
93:    | e1 == e2    -- equality
94:    | e1 <  e2    -- ordering
95:    | (p && p)    -- and
96:    | (p || p)    -- or
97:    | (not p)     -- negation
```

## Subtyping is Implication

PVS' Predicate Subtyping

## Subtyping is Implication

 If: `P` `=> Q` Then: `{v:t | P}` `<: {v:t | Q}`

## Example: Natural Numbers

```143:         type Nat = {v:Int | 0 <= v}
```

 By SMT: `v = 0` `=>` `0 <= v` So: `EqZero` `<:` `Nat`

Hence, we can type:

```165: {-@ zero' :: Nat @-}
166: {v : Int | (v >= 0)}zero'     =  {x3 : Int | (x3 == 0) && (x3 == SimpleRefinements.zero)}zero   -- zero :: EqZero <: Nat
```

## Types = Universal Invariants

(Notoriously hard with pure SMT)

# Types Yield Universal Invariants

## Example: Lists

```191: data L a = N | C a (L a)
```

Every element in `nats` is non-negative:

```202: {-@ nats :: L Nat @-}
203: (L {v : Int | (v >= 0)})nats     =  {x2 : Int | (x2 == (0  :  int))}0 {x8 : Int | (x8 >= 0)}
-> (L {x8 : Int | (x8 >= 0)}) -> (L {x8 : Int | (x8 >= 0)})`C` {x2 : Int | (x2 == (1  :  int))}1 {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)}
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})`C` {x2 : Int | (x2 == (3  :  int))}3 {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)}
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})`C` (L {x2 : Int | false})N
```

Demo: What if `nats` contained `-2`?

## Example: Even/Odd Lists

```220: {-@ type Even = {v:Int | v mod 2 =  0} @-}
221: {-@ type Odd  = {v:Int | v mod 2 /= 0} @-}
```

```228: {-@ evens :: L Even @-}
229: (L {v : Int | ((v mod 2) == 0)})evens     =  {x2 : Int | (x2 == (0  :  int))}0 {x11 : Int | ((x11 mod 2) == 0) && (x11 >= 0)}
-> (L {x11 : Int | ((x11 mod 2) == 0) && (x11 >= 0)})
-> (L {x11 : Int | ((x11 mod 2) == 0) && (x11 >= 0)})`C` {x2 : Int | (x2 == (2  :  int))}2 {x17 : Int | ((x17 mod 2) == 0) && (x17 /= 0) && (x17 > 0) && (x17 >= 0)}
-> (L {x17 : Int | ((x17 mod 2) == 0) && (x17 /= 0) && (x17 > 0) && (x17 >= 0)})
-> (L {x17 : Int | ((x17 mod 2) == 0) && (x17 /= 0) && (x17 > 0) && (x17 >= 0)})`C` {x2 : Int | (x2 == (4  :  int))}4 {x17 : Int | ((x17 mod 2) == 0) && (x17 /= 0) && (x17 > 0) && (x17 >= 0)}
-> (L {x17 : Int | ((x17 mod 2) == 0) && (x17 /= 0) && (x17 > 0) && (x17 >= 0)})
-> (L {x17 : Int | ((x17 mod 2) == 0) && (x17 /= 0) && (x17 > 0) && (x17 >= 0)})`C` (L {x2 : Int | false})N
230:
231: {-@ odds  :: L Odd  @-}
232: (L {v : Int | ((v mod 2) == 1)})odds      =  {x2 : Int | (x2 == (1  :  int))}1 {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)}
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})`C` {x2 : Int | (x2 == (3  :  int))}3 {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)}
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})`C` {x2 : Int | (x2 == (5  :  int))}5 {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)}
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})
-> (L {x14 : Int | ((x14 mod 2) == 1) && (x14 > 0) && (x14 >= 0)})`C` (L {x2 : Int | false})N
```

Demo: What if `evens` contained `1`?

# Contracts: Function Types

## Example: `safeDiv`

Precondition divisor is non-zero.

```263: {-@ type NonZero = {v:Int | v /= 0} @-}
```

## Example: `safeDiv`

• Pre-condition divisor is non-zero.
• Input type specifies pre-condition

```280: {-@ safeDiv :: Int -> NonZero -> Int @-}
281: Int -> {v : Int | (v /= 0)} -> IntsafeDiv Intx {v : Int | (v /= 0)}y = {x2 : Int | (x2 == x)}x x1:Int
-> x2:Int
-> {x6 : Int | (((x1 >= 0) && (x2 >= 0)) => (x6 >= 0)) && (((x1 >= 0) && (x2 >= 1)) => (x6 <= x1)) && (x6 == (x1 / x2))}`div` {x3 : Int | (x3 == y) && (x3 /= 0)}y
```

Demo: What if precondition does not hold?

## Example: `abs`

• Postcondition result is non-negative
• Output type specifies post-condition

```304: {-@ abs       :: x:Int -> Nat @-}
305: Int -> {v : Int | (v >= 0)}abs Intx
306:   | {x2 : Int | (x2 == (0  :  int))}0 x1:Int -> x2:Int -> {x2 : Bool | (((Prop x2)) <=> (x1 <= x2))}<= {x2 : Int | (x2 == x)}x    = {x2 : Int | (x2 == x)}x
307:   | otherwise = {x2 : Int | (x2 == (0  :  int))}0 x1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 - x2))}- {x2 : Int | (x2 == x)}x
```

## Dependent Function Types

Outputs refer to inputs

Relational invariants

# Dependent Function Types

## Example: `range`

`(range i j)` returns `Int`s between `i` and `j`

## Example: `range`

`(range i j)` returns `Int`s between `i` and `j`

```343: {-@ type Btwn I J = {v:_ | (I<=v && v<J)} @-}
```

## Example: `range`

`(range i j)` returns `Int`s between `i` and `j`

```355: {-@ range :: i:Int -> j:Int -> L (Btwn i j) @-}
356: x1:Int -> x2:Int -> (L {v : Int | (v < x2) && (x1 <= v)})range Inti Intj            = x1:{x10 : Int | (x10 >= i) && (i <= x10)}
-> (L {x7 : Int | (x7 >= i) && (x7 >= x1) && (x7 < j) && (i <= x7) && (x1 <= x7)})go {x2 : Int | (x2 == i)}i
357:   where
358:     x1:{VV : Int | (VV >= i) && (i <= VV)}
-> (L {VV : Int | (VV >= i) && (VV >= x1) && (VV < j) && (i <= VV) && (x1 <= VV)})go {VV : Int | (VV >= i) && (i <= VV)}n | {x4 : Int | (x4 == n) && (x4 >= i) && (i <= x4)}n x1:Int -> x2:Int -> {x2 : Bool | (((Prop x2)) <=> (x1 < x2))}< {x2 : Int | (x2 == j)}j     = {x4 : Int | (x4 == n) && (x4 >= i) && (i <= x4)}n {x20 : Int | (x20 >= i) && (x20 >= n) && (x20 < j) && (i <= x20) && (n <= x20)}
-> (L {x20 : Int | (x20 >= i) && (x20 >= n) && (x20 < j) && (i <= x20) && (n <= x20)})
-> (L {x20 : Int | (x20 >= i) && (x20 >= n) && (x20 < j) && (i <= x20) && (n <= x20)})`C` x1:{VV : Int | (VV >= i) && (i <= VV)}
-> (L {VV : Int | (VV >= i) && (VV >= x1) && (VV < j) && (i <= VV) && (x1 <= VV)})go ({x4 : Int | (x4 == n) && (x4 >= i) && (i <= x4)}n x1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 + x2))}+ {x2 : Int | (x2 == (1  :  int))}1)
359:          | otherwise =  (L {x2 : Int | false})N
```

Note: Type of `go` is automatically inferred

## Example: Indexing Into List

```373: (!)          :: L a -> Int -> a
374: (C x _)  forall a. (L a) -> Int -> a! 0 = {VV : a | (VV == x)}x
375: (C _ xs) ! i = (L a)xs forall a. (L a) -> Int -> a! (Inti x1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 - x2))}- {x2 : Int | (x2 == (1  :  int))}1)
376: _        ! _ = {x1 : [Char] | false} -> aliquidError {x2 : [Char] | ((len x2) >= 0)}"Oops!"
```

(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...]