# Laziness

```8: module Laziness where
```

# 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 @-}
```