Higher-Order Specifications

Types scale to Higher-Order Specifications


  • map
  • fold
  • visitors
  • callbacks
  • ...


Very difficult with first-order program logics

Higher Order Specifications

Example: Higher Order Loop


50: loop :: Int -> Int -> α -> (Int -> α -> α) -> α
51: forall a.
lo:{VV : Int | (VV == 0) && (VV >= 0)}
-> hi:{VV : Int | (VV >= 0) && (VV >= lo)}
-> a
-> ({VV : Int | (VV >= 0) && (VV >= lo) && (VV < hi)} -> a -> a)
-> aloop {VV : Int | (VV == 0) && (VV >= 0)}lo {VV : Int | (VV >= 0) && (VV >= lo)}hi abase {VV : Int | (VV >= 0) && (VV >= lo) && (VV < hi)} -> a -> af = {x4 : Int | (x4 >= 0) && (x4 >= lo) && (x4 <= hi)} -> a -> ago {x4 : Int | (x4 == 0) && (x4 == lo) && (x4 >= 0)}lo {VV : a | (VV == base)}base
52:   where 
53:     {VV : Int | (VV >= 0) && (VV >= lo) && (VV <= hi)} -> a -> ago {VV : Int | (VV >= 0) && (VV >= lo) && (VV <= hi)}i aacc 
54:       | {x5 : Int | (x5 == i) && (x5 >= 0) && (x5 >= lo) && (x5 <= hi)}i x1:Int -> x2:Int -> {x2 : Bool | (((Prop x2)) <=> (x1 < x2))}< {x4 : Int | (x4 == hi) && (x4 >= 0) && (x4 >= lo)}hi    = {VV : Int | (VV >= 0) && (VV >= lo) && (VV <= hi)} -> a -> ago ({x5 : Int | (x5 == i) && (x5 >= 0) && (x5 >= lo) && (x5 <= hi)}ix1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 + x2))}+{x2 : Int | (x2 == (1  :  int))}1) ({x4 : Int | (x4 >= 0) && (x4 >= lo) && (x4 < hi)} -> a -> af {x5 : Int | (x5 == i) && (x5 >= 0) && (x5 >= lo) && (x5 <= hi)}i {VV : a | (VV == acc)}acc)
55:       | otherwise = {VV : a | (VV == acc)}acc


LiquidHaskell infers f called with values (Btwn lo hi)

Example: Summing Lists

67: listSum     :: [Int] -> Int
68: [Int] -> IntlistSum [Int]xs  = x1:{x14 : Int | (x14 == 0) && (x14 >= 0)}
-> x2:{x11 : Int | (x11 >= 0) && (x11 >= x1)}
-> Int
-> ({x7 : Int | (x7 >= 0) && (x7 >= x1) && (x7 < x2)}
    -> Int -> Int)
-> Intloop {x2 : Int | (x2 == (0  :  int))}0 {x3 : Int | (x3 == n) && (x3 == (len xs))}n {x2 : Int | (x2 == (0  :  int))}0 {x5 : Int | (x5 >= 0) && (x5 < n)} -> Int -> Intbody 
69:   where 
70:     {VV : Int | (VV >= 0) && (VV < n)} -> Int -> Intbody    = \{VV : Int | (VV >= 0) && (VV < n)}i Intacc -> {x2 : Int | (x2 == acc)}acc x1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 + x2))}+ ({x3 : [Int] | (x3 == xs) && ((len x3) >= 0)}xs x1:[Int] -> {x4 : Int | (x4 < (len x1)) && (0 <= x4)} -> Int!! {x4 : Int | (x4 == i) && (x4 >= 0) && (x4 < n)}i)
71:     {x2 : Int | (x2 == (len xs))}n       = x1:[Int] -> {x2 : Int | (x2 == (len x1))}length {x3 : [Int] | (x3 == xs) && ((len x3) >= 0)}xs


Function Subtyping

  • body called with i :: Btwn 0 (llen xs)

  • Hence, indexing with !! is safe.
Demo: Tweak loop exit condition?

Polymorphic Instantiation

Example: Summing Nats

98: {-@ sumNats :: [Nat] -> Nat @-}
99: [{v : Int | (v >= 0)}] -> {v : Int | (v >= 0)}sumNats [{v : Int | (v >= 0)}]xs  = ({x14 : Int | (x14 >= 0)}
 -> {x12 : Int | (x12 >= 0)} -> {x14 : Int | (x14 >= 0)})
-> {x14 : Int | (x14 >= 0)}
-> [{x12 : Int | (x12 >= 0)}]
-> {x14 : Int | (x14 >= 0)}foldl x1:Int -> x2:Int -> {x2 : Int | (x2 == (x1 + x2))}(+) {x2 : Int | (x2 == (0  :  int))}0 {x3 : [{x6 : Int | (x6 >= 0)}] | (x3 == xs) && ((len x3) >= 0)}xs


Recall 
106: foldl :: (α -> β -> α) -> α -> [β] -> α


How to instantiate α and β ?

Function Subtyping

120: (+) ::  x:Int -> y:Int -> {v:Int|v=x+y} 
121:     <:  Nat   -> Nat   -> Nat


Because,

130:                |- Nat       <: Int  -- Contra
131:   x:Nat, y:Nat |- {v = x+y} <: Nat  -- Co


Because,

141:   0<=x && 0<=y && v = x+y   => 0 <= v

Example: Summing Nats

149: {-@ sumNats :: [Nat] -> Nat @-}
150: sumNats xs  = foldl (+) 0 xs


Where: 
156: foldl :: (α -> β -> α) -> α -> [β] -> α
157: (+)   :: Nat -> Nat -> Nat


sumNats verified by instantiating α,β := Nat


α is loop invariant, instantiation is invariant synthesis

Instantiation And Inference

Polymorphic instantiation happens everywhere...


... so automatic inference is crucial


Cannot use unification (unlike indexed approaches)


LiquidHaskell uses SMT and Abstract Interpretation.

Iteration Dependence

Problem: Cannot use parametric polymorphism to verify


198: {-@ add :: n:Nat -> m:Nat -> {v:Nat|v=m+n} @-}
199: x1:{v : Int | (v >= 0)}
-> x2:{v : Int | (v >= 0)}
-> {v : Int | (v == (x2 + x1)) && (v >= 0)}add {v : Int | (v >= 0)}n {v : Int | (v >= 0)}m = x1:{x22 : Int | (x22 == 0) && (x22 >= 0)}
-> x2:{x19 : Int | (x19 >= 0) && (x19 >= x1)}
-> {x16 : Int | (x16 >= 0) && (x16 >= n)}
-> ({x13 : Int | (x13 >= 0) && (x13 >= x1) && (x13 < x2)}
    -> {x16 : Int | (x16 >= 0) && (x16 >= n)}
    -> {x16 : Int | (x16 >= 0) && (x16 >= n)})
-> {x16 : Int | (x16 >= 0) && (x16 >= n)}loop {x2 : Int | (x2 == (0  :  int))}0 {x3 : Int | (x3 == m) && (x3 >= 0)}m {x3 : Int | (x3 == n) && (x3 >= 0)}n ({x11 : Int | (x11 >= 0) && (x11 < m)}
-> x2:{x8 : Int | (x8 >= 0) && (x8 >= n)}
-> {x5 : Int | (x5 > 0) && (x5 > x2) && (x5 > n) && (x5 >= 0)}\_ {VV : Int | (VV >= 0) && (VV >= n)}i -> {x4 : Int | (x4 == i) && (x4 >= 0) && (x4 >= n)}i x1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 + x2))}+ {x2 : Int | (x2 == (1  :  int))}1)


As property only holds after last iteration ...

... cannot instantiate α := {v:Int | v = n + m}


Problem: Need iteration-dependent invariants...    [Continue]