[Skip]

# Lazy Evaluation

## SMT based Verification

Techniques developed for strict languages

 Floyd-Hoare : `ESCJava`, `SpecSharp` ... Model Checkers : `Slam`, `Blast` ... Refinement Types : `DML`, `Stardust`, `Sage`, `F7`, `F*`, ...

Surely soundness carries over to Haskell, right?

## Back To the Beginning

```71: {-@ safeDiv :: Int -> {v:Int|v /= 0} -> Int @-}
72: Int -> {v : Int | (v /= 0)} -> IntsafeDiv Intn 0 = {x2 : [Char] | false} -> IntliquidError {x2 : [Char] | ((len x2) >= 0)}"div-by-zero!"
73: safeDiv n d = {x2 : Int | (x2 == n)}n x1:Int
-> x2:Int
-> {x6 : Int | (((x1 >= 0) && (x2 >= 0)) => (x6 >= 0)) && (((x1 >= 0) && (x2 >= 1)) => (x6 <= x1)) && (x6 == (x1 / x2))}`div` {x2 : Int | (x2 /= 0)}d
```

Should only call `safeDiv` with non-zero values

## An Innocent Function

`foo` returns a value strictly less than input.

```90: {-@ foo       :: n:Nat -> {v:Nat | v < n} @-}
91: foo n
92:   | n > 0     = n - 1
93:   | otherwise = foo n
```

```100: {-@ foo       :: n:Nat -> {v:Nat | v < n} @-}
101: x1:{v : Int | (v >= 0)} -> {v : Int | (v >= 0) && (v < x1)}foo {v : Int | (v >= 0)}n
102:   | {x3 : Int | (x3 == n) && (x3 >= 0)}n x1:Int -> x2:Int -> {x2 : Bool | (((Prop x2)) <=> (x1 > x2))}> {x2 : Int | (x2 == (0  :  int))}0     = {x3 : Int | (x3 == n) && (x3 >= 0)}n x1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 - x2))}- {x2 : Int | (x2 == (1  :  int))}1
103:   | otherwise = x1:{v : Int | (v >= 0)} -> {v : Int | (v >= 0) && (v < x1)}foo {x3 : Int | (x3 == n) && (x3 >= 0)}n
104:
105: Intexplode = let {x2 : Int | (x2 == (0  :  int))}z = {x2 : Int | (x2 == (0  :  int))}0
106:               {x3 : Int | (x3 >= 0) && (x3 < z)}a = x1:{v : Int | (v >= 0)} -> {v : Int | (v >= 0) && (v < x1)}foo {x3 : Int | (x3 == z) && (x3 == (0  :  int))}z
107:           in
108:               ({VV : Int | (VV == 0) && (VV == 1) && (VV == a) && (VV == z) && (VV > 0) && (VV > a) && (VV > z) && (VV < 0) && (VV < a) && (VV < z)}
-> Int\{VV : Int | (VV == 0) && (VV == 1) && (VV == a) && (VV == z) && (VV > 0) && (VV > a) && (VV > z) && (VV < 0) && (VV < a) && (VV < z)}x -> {x2 : Int | (x2 == (2013  :  int))}2013 Int -> {x3 : Int | (x3 /= 0)} -> Int`safeDiv` {x3 : Int | (x3 == z) && (x3 == (0  :  int))}z) {x4 : Int | (x4 == a) && (x4 >= 0) && (x4 < z)}a
```

Why is this program deemed safe?!

## Safe With Eager Eval

```122: {-@ foo       :: n:Nat -> {v:Nat | v < n} @-}
123: foo n
124:   | n > 0     = n - 1
125:   | otherwise = foo n
126:
127: explode = let z = 0     -- :: {v:Int| v = 0}
128:               a = foo z -- :: {v:Nat| v < z}
129:           in
130:               (\x -> 2013 `safeDiv` z) a
```

Safe in Java, ML: program spins away, never hits divide-by-zero

## Unsafe With Lazy Eval

```143: {-@ foo       :: n:Nat -> {v:Nat | v < n} @-}
144: foo n
145:   | n > 0     = n - 1
146:   | otherwise = foo n
147:
148: explode = let z = 0     -- :: {v:Int| v = 0}
149:               a = foo z -- :: {v:Nat| v < z}
150:           in
151:               (\x -> 2013 `safeDiv` z) a
```

Unsafe in Haskell: program skips `foo z` and hits divide-by-zero!

## Problem: Divergence

What is denoted by:

`e :: {v:Int | P}`

`e` evaluates to `Int` satisfying `P`

or

diverges!

Classical Floyd-Hoare notion of partial correctness

## Problem: Divergence

Consider
```191:         {-@ e :: {v : Int | P} @-}
192:
193:         let x = e in body
```

Eager Evaluation

Can assume `P(x)` when checking `body`

Lazy Evaluation

Cannot assume `P(x)` when checking `body`

## Eager vs. Lazy Binders

```216: {-@ foo       :: n:Nat -> {v:Nat | v < n} @-}
217: foo n
218:   | n > 0     = n - 1
219:   | otherwise = foo n
220:
221: explode = let z = 0     -- :: {v:Int| v = 0}
222:               a = foo z -- :: {v:Nat| v < z}
223:           in
224:               (\x -> 2013 `safeDiv` z) a
```

Inconsistent refinement for `a` is sound for eager, unsound for lazy

## Panic! Now what?

Solution

Assign non-trivial refinements to non-diverging terms!

Require A Termination Analysis

Don't worry, its easy...

Demo:   Disable `"--no-termination"` and see what happens!

## Recap

1. Refinements: Types + Predicates
2. Subtyping: SMT Implication
3. Measures: Strengthened Constructors
4. Abstract: Refinements over functions and data
5. Lazy Evaluation: Requires Termination
6. Termination: via Refinements!