Higher Order Specifications

8: module Loop where
9: import Prelude hiding ((!!), length)
10: import SimpleRefinements

Higher Order Specifications

Consider a loop function:

20: loop :: Int -> Int -> a -> (Int -> a -> a) -> a
21: forall a.
lo:{VV : (GHC.Types.Int) | (VV == 0) && ((VV mod 2) == 0) && (VV >= 0)}
-> hi:(GHC.Types.Int)
-> a
-> ({VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV < hi)}
    -> a -> a)
-> aloop {VV : (GHC.Types.Int) | (VV == 0) && ((VV mod 2) == 0) && (VV >= 0)}lo (GHC.Types.Int)hi abase {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV < hi)}
-> a -> af        = {VV : (GHC.Types.Int) | (VV == 0) && (VV == lo) && (VV == (lo + lo)) && ((VV mod 2) == 0) && (VV >= 0)}
-> {VV : a | (VV == base)} -> ago {VV : (GHC.Types.Int) | (VV == 0) && (VV == lo) && ((VV mod 2) == 0) && (VV >= 0)}lo {VV : a | (VV == base)}base
22:   where 
23:     forall a.
lo:{VV : (GHC.Types.Int) | (VV == 0) && (VV == lo) && (VV == (lo + lo)) && ((VV mod 2) == 0) && (VV >= 0)}
-> hi:{VV : (GHC.Types.Int) | (VV == hi) && (VV == (hi + lo)) && (VV == (hi + lo)) && (VV == (lo + hi)) && (VV == (lo + hi))}
-> {VV : a | (VV == base)}
-> ({VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV >= lo) && (VV < hi) && (VV < hi)}
    -> a -> a)
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV >= lo)}
-> a
-> ago {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV >= lo)}i aacc | {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV >= lo) && (VV >= lo)}i x:(GHC.Types.Int)
-> y:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x < y))}< {VV : (GHC.Types.Int) | (VV == hi) && (VV == hi) && (VV == (hi + lo)) && (VV == (hi + lo)) && (VV == (lo + hi)) && (VV == (lo + hi))}hi    = forall a.
lo:{VV : (GHC.Types.Int) | (VV == 0) && (VV == lo) && (VV == (lo + lo)) && ((VV mod 2) == 0) && (VV >= 0)}
-> hi:{VV : (GHC.Types.Int) | (VV == hi) && (VV == (hi + lo)) && (VV == (hi + lo)) && (VV == (lo + hi)) && (VV == (lo + hi))}
-> {VV : a | (VV == base)}
-> ({VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV >= lo) && (VV < hi) && (VV < hi)}
    -> a -> a)
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV >= lo)}
-> a
-> ago ({VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV >= lo) && (VV >= lo)}ix:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+{VV : (GHC.Types.Int) | (VV == (1  :  int))}1) ({VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV >= lo) && (VV < hi) && (VV < hi)}
-> a -> af {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV >= lo) && (VV >= lo)}i {VV : a | (VV == acc)}acc)
24:              | otherwise = {VV : a | (VV == acc)}acc

LiquidHaskell infers

if lo <= hi then f called with lo <= i < hi

Higher Order Specifications

Lets use (!!) to write a function that sums an Int list

40: {-@ listSum :: L Int -> Int @-}
41: listSum     :: L Int -> Int
42: (SimpleRefinements.L (GHC.Types.Int)) -> (GHC.Types.Int)listSum (SimpleRefinements.L (GHC.Types.Int))xs  = lo:{VV : (GHC.Types.Int) | (VV == 0) && ((VV mod 2) == 0) && (VV >= 0)}
-> hi:(GHC.Types.Int)
-> (GHC.Types.Int)
-> ({VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV < hi)}
    -> (GHC.Types.Int) -> (GHC.Types.Int))
-> (GHC.Types.Int)loop {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV == n) && (VV == (llen xs))}n {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}
-> (GHC.Types.Int) -> (GHC.Types.Int)body 
43:   where 
44:     {VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}
-> (GHC.Types.Int) -> (GHC.Types.Int)body    = \{VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}i (GHC.Types.Int)acc -> {VV : (GHC.Types.Int) | (VV == acc)}acc x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+ ({VV : (SimpleRefinements.L (GHC.Types.Int)) | (VV == xs)}xs ls:(SimpleRefinements.L (GHC.Types.Int))
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < (llen ls))}
-> (GHC.Types.Int)!! {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV < n)}i)
45:     {VV : (GHC.Types.Int) | (VV == (llen xs))}n       = xs:(SimpleRefinements.L (GHC.Types.Int))
-> {VV : (GHC.Types.Int) | (VV == (llen xs))}length {VV : (SimpleRefinements.L (GHC.Types.Int)) | (VV == xs)}xs

By function subtyping LiquidHaskell infers

body called with 0 <= i < llen xs
hence, indexing safe.

Demo: Let's change the 0 to -1 and see what happens!

Higher Order Specifications

We can give this function a better type:

62: {-@ listNatSum :: L Nat -> Nat @-}
63: listNatSum     :: L Int -> Int
64: (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0)})
-> {VV : (GHC.Types.Int) | (VV >= 0)}listNatSum (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0)})xs  = lo:{VV : (GHC.Types.Int) | (VV == 0) && ((VV mod 2) == 0) && (VV >= 0)}
-> hi:(GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (VV >= 0)}
-> ({VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV < hi)}
    -> {VV : (GHC.Types.Int) | (VV >= 0)}
    -> {VV : (GHC.Types.Int) | (VV >= 0)})
-> {VV : (GHC.Types.Int) | (VV >= 0)}loop {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV == n) && (VV == (llen xs))}n {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}
-> acc:{VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= acc)}body 
65:   where 
66:     {VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}
-> acc:{VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= acc)}body       = \{VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}i {VV : (GHC.Types.Int) | (VV >= 0)}acc -> {VV : (GHC.Types.Int) | (VV == acc) && (VV >= 0)}acc x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+ ({VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0)}) | (VV == xs)}xs ls:(SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0)})
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < (llen ls))}
-> {VV : (GHC.Types.Int) | (VV >= 0)}!! {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV < n)}i)
67:     {VV : (GHC.Types.Int) | (VV == (llen xs))}n          = xs:(SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0)})
-> {VV : (GHC.Types.Int) | (VV == (llen xs))}length {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | (VV >= 0)}) | (VV == xs)}xs

To verify this type, note: (+) :: Nat -> Nat -> Nat

LiquidHaskell instantiates a in loop with Nat

loop :: Int -> Int -> Nat -> (Int -> Nat -> Nat) -> Nat

Yielding the output.

Higher Order Specifications

By the same analysis, LiquidHaskell verifies that

84: {-@ listEvenSum :: L Even -> Even @-}
85: listEvenSum     :: L Int -> Int
86: (SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0)})
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}listEvenSum (SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0)})xs  = lo:{VV : (GHC.Types.Int) | (VV == 0) && ((VV mod 2) == 0) && (VV >= 0)}
-> hi:(GHC.Types.Int)
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}
-> ({VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV < hi)}
    -> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}
    -> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)})
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}loop {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV == n) && (VV == (llen xs))}n {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}body 
87:   where {VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}body   = \{VV : (GHC.Types.Int) | (VV >= 0) && (VV < n)}i {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}acc -> {VV : (GHC.Types.Int) | (VV == acc) && ((VV mod 2) == 0)}acc x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+ ({VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}) | (VV == xs)}xs ls:(SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0)})
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV < (llen ls))}
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}!! {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV < n)}i)
88:         {VV : (GHC.Types.Int) | (VV == (llen xs))}n      = xs:(SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0)})
-> {VV : (GHC.Types.Int) | (VV == (llen xs))}length {VV : (SimpleRefinements.L {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}) | (VV == xs)}xs

Here, the system deduces that (+) has type

x:Int-> y:Int -> {v:Int| v=x+y} <: Even -> Even -> Even

Hence, verification proceeds by instantiating a with Even

loop :: Int -> Int -> Even -> (Int -> Even -> Even) -> Even

Another Example

Consider a simpler example:

107: {-@ add :: n:Nat -> m:Nat -> {v:Int| v = m + n} @-}
108: add     :: Int -> Int -> Int
109: n:{VV : (GHC.Types.Int) | (VV >= 0)}
-> m:{VV : (GHC.Types.Int) | (VV >= 0)}
-> {VV : (GHC.Types.Int) | (VV == (m + n))}add {VV : (GHC.Types.Int) | (VV >= 0)}n {VV : (GHC.Types.Int) | (VV >= 0)}m = lo:{VV : (GHC.Types.Int) | (VV == 0) && ((VV mod 2) == 0) && (VV >= 0)}
-> hi:(GHC.Types.Int)
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= n)}
-> ({VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV < hi)}
    -> {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= n)}
    -> {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= n)})
-> {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= n)}loop {VV : (GHC.Types.Int) | (VV == (0  :  int))}0 {VV : (GHC.Types.Int) | (VV == m) && (VV >= 0)}m {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0)}n ({VV : (GHC.Types.Int) | (VV >= 0) && (VV < m)}
-> i:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= n)}
-> {VV : (GHC.Types.Int) | (VV > 0) && (VV > i) && (VV > n) && (VV >= 0)}\_ {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= n)}i -> {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV >= n)}i x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+ {VV : (GHC.Types.Int) | (VV == (1  :  int))}1)

Cannot use parametric polymorphism as before!

Cannot instantiate a with {v:Int|v = n + m} ...
... as this only holds after last iteration of loop!

Require Higher Order Invariants

On values computed in intermediate iterations...
... i.e. invariants that depend on the iteration index.