 6: module Loop (
 7:     listSum
 8:   , sumNats
 9:   ) where
10: 
11: import Prelude
12: 
13: {-@ LIQUID "--no-termination"@-}
14: sumNats  :: [Int] -> Int
15: add         :: Int -> Int -> Int

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

By subtyping, we infer 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 `Nat`s

100: {-@ sumNats :: [Nat] -> Nat @-}
101: [{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

108: foldl :: (α -> β -> α) -> α -> [β] -> α

How to instantiate α and β ?

Function Subtyping

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

Because,

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

Because,

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

Example: Summing `Nat`s

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

Where:

158: foldl :: (α -> β -> α) -> α -> [β] -> α
159: (+)   :: Nat -> Nat -> Nat

Hence, sumNats verified by instantiating α,β := Nat

α is loop invariant, instantiation is invariant synthesis

Instantiation And Inference

Polymorphism ubiquitous, so inference is critical!

Step 1. Templates Instantiate with unknown refinements

\[ \begin{array}{rcl} \alpha & \defeq & \reft{v}{\Int}{\kvar{\alpha}}\\ \beta & \defeq & \reft{v}{\Int}{\kvar{\beta}}\\ \end{array} \]

Step 2. Horn-Constraints By type checking the templates

Step 3. Fixpoint Abstract interpretatn. to get solution for \(\kvar{}\)

Iteration Dependence

Problem: Cannot use parametric polymorphism to verify

214: {-@ add :: n:Nat -> m:Nat -> {v:Nat|v=m+n} @-}
215: 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 \(\alpha \defeq \reft{v}{\Int}{v = n + m}\)

Problem: Iteration-dependent invariants...? [Continue]