Laziness

8: module Laziness where
9: import Language.Haskell.Liquid.Prelude

Infinite Computations can lead to Unsoundness

Infinite Computations can be refined with false

18: {-@ foo :: n:Nat -> {v:Nat | v < n} @-}
19: foo     :: Int -> Int
20: n:{VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}foo {VV : (GHC.Types.Int) | (VV >= 0)}n   | {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0)}n x1:{VV : (GHC.Types.Int) | (VV >= 0) && (VV <= n)}
-> x2:{VV : (GHC.Types.Int) | (VV >= 0) && (VV <= n)}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 > x2))}> {VV : (GHC.Types.Int) | (VV == (0  :  int))}0     = {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0)}n x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}- {VV : (GHC.Types.Int) | (VV == (1  :  int))}1
21:         | otherwise = n:{VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}foo {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0)}n

Under false anything can be proven

28: forall a. a -> aprop = {VV : (GHC.Types.Bool) | ((Prop VV))} -> a -> aliquidAssert ({VV : (GHC.Types.Bool) | (not (((Prop VV)))) && ((Prop VV)) && (VV == GHC.Types.False) && (VV == GHC.Types.True) && (VV > GHC.Types.False) && (VV > GHC.Types.True) && (VV < GHC.Types.False) && (VV < GHC.Types.True)}(\{VV : (GHC.Types.Int) | (VV == 0) && (VV == 1) && (VV > 0) && (VV < 0)}x -> {VV : (GHC.Integer.Type.Integer) | (VV == 1)}0x1:{VV : (GHC.Integer.Type.Integer) | (VV == 0) && (VV == 1) && (VV == x) && (VV > 0) && (VV > x) && (VV < 0) && (VV < x)}
-> x2:{VV : (GHC.Integer.Type.Integer) | (VV == 0) && (VV == 1) && (VV == x) && (VV > 0) && (VV > x) && (VV < 0) && (VV < x)}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 == x2))}==1) (n:{VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}foo {VV : (GHC.Types.Int) | (VV == (0  :  int))}0))

Demo: Check a real property here!

Our solution (Current Work)

• Use termination analysis to track infinite computations

• Use true refinements for infinite computations

Size-based Termination Analysis

• Use refinement types to force the recursive argument to decrease

47: {-@ unsafeFoo :: n:Nat -> {v:Nat | v < n} @-}
48: unsafeFoo     :: Int -> Int
49:   -- unsafeFoo :: n'{v:Nat | v < n} -> {v:Nat | v < n'}
50: x1:{VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < x1)}unsafeFoo {VV : (GHC.Types.Int) | (VV >= 0)}n   | {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0)}n x1:{VV : (GHC.Types.Int) | (VV >= 0) && (VV <= n)}
-> x2:{VV : (GHC.Types.Int) | (VV >= 0) && (VV <= n)}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 > x2))}> {VV : (GHC.Types.Int) | (VV == (0  :  int))}0     = {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0)}n x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}- {VV : (GHC.Types.Int) | (VV == (1  :  int))}1
51:               | otherwise = x1:{VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < x1)}unsafeFoo {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0)}n

• prop is safe, but the program is decided unsafe

58: forall a. a -> aprop1 = {VV : (GHC.Types.Bool) | ((Prop VV))} -> a -> aliquidAssert ({VV : (GHC.Types.Bool) | (not (((Prop VV)))) && ((Prop VV)) && (VV == GHC.Types.False) && (VV == GHC.Types.True) && (VV > GHC.Types.False) && (VV > GHC.Types.True) && (VV < GHC.Types.False) && (VV < GHC.Types.True)}(\{VV : (GHC.Types.Int) | (VV == 0) && (VV == 1) && (VV == inf) && (VV > 0) && (VV > inf) && (VV < 0) && (VV < inf)}x -> {VV : (GHC.Integer.Type.Integer) | (VV == 1)}0x1:{VV : (GHC.Integer.Type.Integer) | (VV == 0) && (VV == 1) && (VV == inf) && (VV == x) && (VV > 0) && (VV > inf) && (VV > x) && (VV < 0) && (VV < inf) && (VV < x)}
-> x2:{VV : (GHC.Integer.Type.Integer) | (VV == 0) && (VV == 1) && (VV == inf) && (VV == x) && (VV > 0) && (VV > inf) && (VV > x) && (VV < 0) && (VV < inf) && (VV < x)}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 == x2))}==1) {VV : (GHC.Types.Int) | (VV == inf) && (VV >= 0)}inf)
59:   where {VV : (GHC.Types.Int) | (VV >= 0)}inf = x1:{VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < x1)}unsafeFoo {VV : (GHC.Types.Int) | (VV == (0  :  int))}0

Refinements of infinite Computations

If you need a non-terminating function, use Lazy to declare

• We know that foo may not terminate

• Its return type is refined with true

71: {-@ Lazy safeFoo @-}
72: {-@ safeFoo :: n:Nat -> {v:Int | true} @-}
73: safeFoo    :: Int   -> Int
74: {VV : (GHC.Types.Int) | (VV >= 0)} -> (GHC.Types.Int)safeFoo {VV : (GHC.Types.Int) | (VV >= 0)}n   | {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0)}n x1:{VV : (GHC.Types.Int) | (VV >= 0) && (VV <= n)}
-> x2:{VV : (GHC.Types.Int) | (VV >= 0) && (VV <= n)}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 > x2))}> {VV : (GHC.Types.Int) | (VV == (0  :  int))}0     = {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0)}n x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}- {VV : (GHC.Types.Int) | (VV == (1  :  int))}1
75:             | otherwise = {VV : (GHC.Types.Int) | (VV >= 0)} -> (GHC.Types.Int)safeFoo {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0)}n

Now, prop is unsafe

83: forall a. a -> aprop2 = {VV : (GHC.Types.Bool) | ((Prop VV))} -> a -> aliquidAssert ({VV : (GHC.Types.Bool) | (not (((Prop VV)))) && (VV /= GHC.Types.True)}(\{VV : (GHC.Types.Int) | (VV == inf)}x -> {VV : (GHC.Integer.Type.Integer) | (VV == 1)}0x1:{VV : (GHC.Integer.Type.Integer) | (VV >= 0)}
-> x2:{VV : (GHC.Integer.Type.Integer) | (VV >= 0)}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 == x2))}==1) {VV : (GHC.Types.Int) | (VV == inf)}inf)
84:   where (GHC.Types.Int)inf = {VV : (GHC.Types.Int) | (VV >= 0)} -> (GHC.Types.Int)safeFoo {VV : (GHC.Types.Int) | (VV == (0  :  int))}0

Restore Soundness

• Use termination analysis to track infinite objects

• Use true refinements for infinite objects

Foo was declared Lazy

97: {-@ Lazy foo @-}