Lazy Evaluation?












[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

LiquidHaskell Lies!

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!



[continue...]