Higher Order Specifications

8: module Loop where
9: 
10: {-@ LIQUID "--no-termination"@-}

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:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo)}
-> 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 {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo)}hi abase {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV < hi)}
-> a -> af        = {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV <= hi)}
-> a -> 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) && (VV <= hi)}
-> hi:{VV : (GHC.Types.Int) | (VV == hi) && (VV == (hi + lo)) && (VV == (hi + lo)) && (VV == (lo + hi)) && (VV == (lo + hi)) && (VV >= 0) && (VV >= lo) && (VV >= lo)}
-> {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) && (VV <= hi) && (VV <= hi)}
-> a
-> ago {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi)}i aacc | {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi)}i x1:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= i) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi)}
-> x2:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= i) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi)}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 < x2))}< {VV : (GHC.Types.Int) | (VV == hi) && (VV == hi) && (VV == (hi + lo)) && (VV == (hi + lo)) && (VV == (lo + hi)) && (VV == (lo + hi)) && (VV >= 0) && (VV >= lo) && (VV >= lo)}hi    = forall a.
lo:{VV : (GHC.Types.Int) | (VV == 0) && (VV == lo) && (VV == (lo + lo)) && ((VV mod 2) == 0) && (VV >= 0) && (VV <= hi)}
-> hi:{VV : (GHC.Types.Int) | (VV == hi) && (VV == (hi + lo)) && (VV == (hi + lo)) && (VV == (lo + hi)) && (VV == (lo + hi)) && (VV >= 0) && (VV >= lo) && (VV >= lo)}
-> {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) && (VV <= hi) && (VV <= hi)}
-> a
-> ago ({VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi)}ix1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+{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) && (VV <= hi) && (VV <= hi)}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 :: [Int] -> Int @-}
41: listSum     :: [Int] -> Int
42: [(GHC.Types.Int)] -> (GHC.Types.Int)listSum [(GHC.Types.Int)]xs  = lo:{VV : (GHC.Types.Int) | (VV == 0) && ((VV mod 2) == 0) && (VV >= 0)}
-> hi:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo)}
-> (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 == (len 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 x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ ({VV : [(GHC.Types.Int)] | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}xs x1:[(GHC.Types.Int)]
-> {VV : (GHC.Types.Int) | (VV < (len x1)) && (0 <= VV)}
-> (GHC.Types.Int)!! {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV < n)}i)
45:     {VV : (GHC.Types.Int) | (VV == (len xs))}n       = x1:[(GHC.Types.Int)] -> {VV : (GHC.Types.Int) | (VV == (len x1))}length {VV : [(GHC.Types.Int)] | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}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 :: [Nat] -> Nat @-}
63: listNatSum     :: [Int] -> Int
64: [{VV : (GHC.Types.Int) | (VV >= 0)}]
-> {VV : (GHC.Types.Int) | (VV >= 0)}listNatSum [{VV : (GHC.Types.Int) | (VV >= 0)}]xs  = lo:{VV : (GHC.Types.Int) | (VV == 0) && ((VV mod 2) == 0) && (VV >= 0)}
-> hi:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo)}
-> {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 == (len 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 x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ ({VV : [{VV : (GHC.Types.Int) | (VV >= 0)}] | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}xs x1:[{VV : (GHC.Types.Int) | (VV >= 0)}]
-> {VV : (GHC.Types.Int) | (VV < (len x1)) && (0 <= VV)}
-> {VV : (GHC.Types.Int) | (VV >= 0)}!! {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV < n)}i)
67:     {VV : (GHC.Types.Int) | (VV == (len xs))}n          = x1:[{VV : (GHC.Types.Int) | (VV >= 0)}]
-> {VV : (GHC.Types.Int) | (VV == (len x1))}length {VV : [{VV : (GHC.Types.Int) | (VV >= 0)}] | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}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 :: [Even] -> Even @-}
85: listEvenSum     :: [Int] -> Int
86: [{VV : (GHC.Types.Int) | ((VV mod 2) == 0)}]
-> {VV : (GHC.Types.Int) | ((VV mod 2) == 0)}listEvenSum [{VV : (GHC.Types.Int) | ((VV mod 2) == 0)}]xs  = lo:{VV : (GHC.Types.Int) | (VV == 0) && ((VV mod 2) == 0) && (VV >= 0)}
-> hi:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo)}
-> {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 == (len 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 x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ ({VV : [{VV : (GHC.Types.Int) | ((VV mod 2) == 0)}] | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}xs x1:[{VV : (GHC.Types.Int) | ((VV mod 2) == 0)}]
-> {VV : (GHC.Types.Int) | (VV < (len x1)) && (0 <= VV)}
-> {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 == (len xs))}n      = x1:[{VV : (GHC.Types.Int) | ((VV mod 2) == 0)}]
-> {VV : (GHC.Types.Int) | (VV == (len x1))}length {VV : [{VV : (GHC.Types.Int) | ((VV mod 2) == 0)}] | (VV == xs) && ((len VV) >= 0) && ((sumLens VV) >= 0)}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:{VV : (GHC.Types.Int) | (VV >= 0) && (VV >= lo)}
-> {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 x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ {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.