Abstract Refinements

Induction

Encoding induction with Abstract refinements

12: module Loop where
13: import Prelude hiding ((!!), foldr, length, (++))
14: -- import Measures
15: import Language.Haskell.Liquid.Prelude
16: {-@ LIQUID "--no-termination" @-}
17: 
18: {-@ measure llen  :: (L a) -> Int
19:     llen (N)      = 0
20:     llen (C x xs) = 1 + (llen xs)  @-}
21: 
22: size  :: L a -> Int
23: add   :: Int -> Int -> Int
24: loop  :: Int -> Int -> α -> (Int -> α -> α) -> α
25: foldr :: (L a -> a -> b -> b) -> b -> L a -> b

Induction

Example: `loop` redux

Recall the higher-order loop

40: forall a <p :: GHC.Types.Int-> a-> Bool>.
x1:Int
-> x2:{hi : Int | (x1 <= hi)}
-> {VV : a<p x1> | true}
-> (x5:Int
    -> {VV : a<p x5> | true}
    -> forall [ex:{VV : Int | (VV == (x5 + 1))}].{VV : a<p ex> | true})
-> {VV : a<p x2> | true}loop Intlo {hi : Int | (lo <= hi)}hi {VV : a | ((papp2 p VV lo))}base x1:Int
-> {VV : a | ((papp2 p VV x1))}
-> forall [ex:{VV : Int | (VV == (x1 + 1))}].{VV : a | ((papp2 p VV ex))}f = x1:{x4 : Int | (x4 >= lo) && (lo <= x4) && (x4 <= hi)}
-> {VV : a | ((papp2 p VV x1))} -> {VV : a | ((papp2 p VV hi))}go {x2 : Int | (x2 == lo)}lo {VV : a | ((papp2 p VV lo)) && (VV == base)}base
41:   where 
42:     x1:{VV : Int | (VV >= lo) && (VV <= hi) && (lo <= VV)}
-> {VV : a | ((papp2 p VV x1))} -> {VV : a | ((papp2 p VV hi))}go {VV : Int | (VV >= lo) && (VV <= hi) && (lo <= VV)}i {VV : a | ((papp2 p VV i))}acc 
43:       | {x5 : Int | (x5 == i) && (x5 >= lo) && (lo <= x5) && (x5 <= hi)}i x1:Int -> x2:Int -> {x2 : Bool | (((Prop x2)) <=> (x1 < x2))}< {x3 : Int | (x3 == hi) && (lo <= x3)}hi    = x1:{VV : Int | (VV >= lo) && (VV <= hi) && (lo <= VV)}
-> {VV : a | ((papp2 p VV x1))} -> {VV : a | ((papp2 p VV hi))}go ({x5 : Int | (x5 == i) && (x5 >= lo) && (lo <= x5) && (x5 <= hi)}ix1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 + x2))}+{x2 : Int | (x2 == (1  :  int))}1) (x1:Int
-> {VV : a | ((papp2 p VV x1))}
-> forall [ex:{VV : Int | (VV == (x1 + 1))}].{VV : a | ((papp2 p VV ex))}f {x5 : Int | (x5 == i) && (x5 >= lo) && (lo <= x5) && (x5 <= hi)}i {VV : a | ((papp2 p VV i)) && (VV == acc)}acc)
44:       | otherwise = {VV : a | ((papp2 p VV i)) && (VV == acc)}acc

Iteration Dependence

We used loop to write

53: {-@ add :: n:Nat -> m:Nat -> {v:Nat|v=m+n} @-}
54: add n m = loop 0 m n (\_ i -> i + 1)

Problem

As property only holds after last loop iteration...
... cannot instantiate α with {v:Int | v = n + m}

Iteration Dependence

We used loop to write

75: {-@ add :: n:Nat -> m:Nat -> {v:Nat|v=m+n} @-}
76: add n m = loop 0 m n (\_ i -> i + 1)

Problem

Need invariant relating iteration i with accumulator acc

Iteration Dependence

We used loop to write

92: {-@ add :: n:Nat -> m:Nat -> {v:Nat|v=m+n} @-}
93: add n m = loop 0 m n (\_ i -> i + 1)

Solution

Abstract Refinement p :: Int -> a -> Prop
(p i acc) relates iteration i with accumulator acc

Induction in `loop` (by hand)

110: loop lo hi base f = go lo base
111:   where 
112:     go i acc 
113:       | i < hi    = go (i+1) (f i acc)
114:       | otherwise = acc

Assume	:	`out = loop lo hi base f`
Prove	:	`(p hi out)`

Induction in `loop` (by hand)

136: loop lo hi base f = go lo base
137:   where 
138:     go i acc 
139:       | i < hi    = go (i+1) (f i acc)
140:       | otherwise = acc

Base Case: Initial accumulator base satisfies invariant

(p lo base)

Induction in `loop` (by hand)

155: loop lo hi base f = go lo base
156:   where 
157:     go i acc 
158:       | i < hi    = go (i+1) (f i acc)
159:       | otherwise = acc

Inductive Step: f preserves invariant at i

(p i acc) => (p (i+1) (f i acc))

Induction in `loop` (by hand)

173: loop lo hi base f = go lo base
174:   where 
175:     go i acc 
176:       | i < hi    = go (i+1) (f i acc)
177:       | otherwise = acc

"By Induction" out satisfies invariant at hi

(p hi out)

Induction in `loop` (by type)

Induction is an abstract refinement type for loop

195: {-@ loop :: forall a <p :: Int -> a -> Prop>.
196:         lo:Int
197:      -> hi:{Int | lo <= hi}
198:      -> base:a<p lo>                      
199:      -> f:(i:Int -> a<p i> -> a<p (i+1)>) 
200:      -> a<p hi>                           @-}

Induction in `loop` (by type)

p is the index dependent invariant!

212: p    :: Int -> a -> Prop             -- invt 
213: base :: a<p lo>                      -- base 
214: f    :: i:Int -> a<p i> -> a<p(i+1)> -- step
215: out  :: a<p hi>                      -- goal

Using Induction

224: {-@ add :: n:Nat -> m:Nat -> {v:Nat| v=m+n} @-}
225: 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 = forall <p :: GHC.Types.Int-> GHC.Types.Int-> Bool>.
x1:Int
-> x2:{x19 : Int | (x1 <= x19)}
-> {x17 : Int<p x1> | (x17 >= 0) && (x17 >= n) && (n <= x17)}
-> (x5:Int
    -> {x17 : Int<p x5> | (x17 >= 0) && (x17 >= n) && (n <= x17)}
    -> forall [ex:{VV : Int | (VV == (x5 + 1))}].{x17 : Int<p ex> | (x17 >= 0) && (x17 >= n) && (n <= x17)})
-> {x17 : Int<p x2> | (x17 >= 0) && (x17 >= n) && (n <= x17)}loop {x2 : Int | (x2 == (0  :  int))}0 {x3 : Int | (x3 == m) && (x3 >= 0)}m {x3 : Int | (x3 == n) && (x3 >= 0)}n (x1:Int
-> x2:{x17 : Int | (x17 == (x1 + n)) && (x17 == (n + x1)) && (x17 >= 0) && (x17 >= x1) && (x17 >= n) && (x1 <= x17) && (n <= x17)}
-> {x9 : Int | (x9 == (x2 + 1)) && (x9 > 0) && (x9 > x1) && (x9 > x2) && (x9 > n) && (x9 >= 0) && (x1 <= x9) && (n <= x9)}\_ {VV : Int | (VV >= 0) && (VV >= n) && (n <= VV)}z -> {x5 : Int | (x5 == z) && (x5 >= 0) && (x5 >= n) && (n <= x5)}z x1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 + x2))}+ {x2 : Int | (x2 == (1  :  int))}1)

Verified by instantiating the abstract refinement of loop

p := \i acc -> acc = i + n

Generalizes To Structures

Same idea applies for induction over structures ...

Structural Induction

Example: Lists

272: data L a = N 
273:          | C a (L a)

Lets write a generic loop over such lists ...

Example: `foldr`

286: foldr f b N        = b
287: foldr f b (C x xs) = f xs x (foldr f b xs)

Lets brace ourselves for the type...

Example: `foldr`

300: {-@ foldr :: 
301:     forall a b <p :: L a -> b -> Prop>. 
302:       (xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)>) 
303:     -> b<p N> 
304:     -> ys:L a
305:     -> b<p ys>                            @-}
306: forall a b <p :: (Loop.L a)-> b-> Bool>.
(x2:(L a)
 -> x3:a
 -> {VV : b<p x2> | true}
 -> forall [ex:{VV : (L a) | (VV == (Loop.C x3 x2))}].{VV : b<p ex> | true})
-> forall [ex:{VV : (L a) | (VV == (Loop.N))}].{VV : b<p ex> | true}
-> x6:(L a)
-> {VV : b<p x6> | true}foldr x1:(L a)
-> x2:a
-> {VV : b | ((papp2 p VV x1))}
-> forall [ex:{VV : (L a) | (VV == (Loop.C x2 x1))}].{VV : b | ((papp2 p VV ex))}f forall [ex:{VV : (L a) | (VV == (Loop.N))}].{VV : a | ((papp2 p VV ex))}b N        = forall [ex:{VV : (L a) | (VV == (Loop.N))}].{VV : a | ((papp2 p VV ex))}b
307: foldr f b (C x xs) = x1:(L a)
-> x2:a
-> {VV : b | ((papp2 p VV x1))}
-> forall [ex:{VV : (L a) | (VV == (Loop.C x2 x1))}].{VV : b | ((papp2 p VV ex))}f {x2 : (L a) | (x2 == xs)}xs {VV : a | (VV == x)}x (forall a b <p :: (Loop.L a)-> b-> Bool>.
(x2:(L a)
 -> x3:a
 -> {VV : b<p x2> | true}
 -> forall [ex:{VV : (L a) | (VV == (Loop.C x3 x2))}].{VV : b<p ex> | true})
-> forall [ex:{VV : (L a) | (VV == (Loop.N))}].{VV : b<p ex> | true}
-> x6:(L a)
-> {VV : b<p x6> | true}foldr x1:(L a)
-> x2:a
-> {VV : b | ((papp2 p VV x1))}
-> forall [ex:{VV : (L a) | (VV == (Loop.C x2 x1))}].{VV : b | ((papp2 p VV ex))}f forall [ex:{VV : (L a) | (VV == (Loop.N))}].{VV : a | ((papp2 p VV ex))}b {x2 : (L a) | (x2 == xs)}xs)

Lets step through the type...

`foldr`: Abstract Refinement

321: p    :: L a -> b -> Prop   
322: step :: xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)> 
323: base :: b<p N> 
324: ys   :: L a
325: out  ::  b<p ys>

(p xs b) relates b with folded xs

p :: L a -> b -> Prop

`foldr`: Base Case

339: p    :: L a -> b -> Prop   
340: step :: xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)> 
341: base :: b<p N> 
342: ys   :: L a
343: out  :: b<p ys>

base is related to empty list N

base :: b<p N>

`foldr`: Ind. Step

358: p    :: L a -> b -> Prop   
359: step :: xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)> 
360: base :: b<p N> 
361: ys   :: L a
362: out  :: b<p ys>

step extends relation from xs to C x xs

step :: xs:_ -> x:_ -> b<p xs> -> b<p (C x xs)>

`foldr`: Output

376: p    :: L a -> b -> Prop   
377: step :: xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)> 
378: base :: b<p N> 
379: ys   :: L a
380: out  :: b<p ys>

Hence, relation holds between out and entire input list ys

out :: b<p ys>

Using `foldr`: Size

We can now verify

395: {-@ size :: xs:_ -> {v:Int| v = (llen xs)} @-}
396: forall a. x1:(L a) -> {v : Int | (v == (llen x1))}size     = forall a b <p :: (Loop.L a)-> b-> Bool>.
(x2:(L a)
 -> x3:a
 -> {VV : b<p x2> | true}
 -> forall [ex:{VV : (L a) | (VV == (Loop.C x3 x2))}].{VV : b<p ex> | true})
-> forall [ex:{VV : (L a) | (VV == (Loop.N))}].{VV : b<p ex> | true}
-> x6:(L a)
-> {VV : b<p x6> | true}foldr (x1:(L a)
-> a
-> x3:{x8 : Int | (x8 == (llen x1)) && (x8 >= 0)}
-> {x5 : Int | (x5 == (x3 + 1)) && (x5 > 0) && (x5 > x3) && (x5 >= 0)}\_ _ {VV : Int | (VV >= 0)}n -> {x3 : Int | (x3 == n) && (x3 >= 0)}n x1:Int -> x2:Int -> {x4 : Int | (x4 == (x1 + x2))}+ {x2 : Int | (x2 == (1  :  int))}1) {x2 : Int | (x2 == (0  :  int))}0

by automatically instantiating

p := \xs acc -> acc = (llen xs)

Using `foldr`: Append

We can now verify

413: {-@ (++) :: xs:_ -> ys:_ -> (Cat a xs ys) @-} 
414: (L a)xs forall a.
x1:(L a)
-> x2:(L a) -> {v : (L a) | ((llen v) == ((llen x1) + (llen x2)))}++ (L a)ys = forall a b <p :: (Loop.L a)-> b-> Bool>.
(x2:(L a)
 -> x3:a
 -> {VV : b<p x2> | true}
 -> forall [ex:{VV : (L a) | (VV == (Loop.C x3 x2))}].{VV : b<p ex> | true})
-> forall [ex:{VV : (L a) | (VV == (Loop.N))}].{VV : b<p ex> | true}
-> x6:(L a)
-> {VV : b<p x6> | true}foldr ((L a)
-> a -> x3:(L a) -> {x2 : (L a) | ((llen x2) == (1 + (llen x3)))}\_ -> a -> x2:(L a) -> {x2 : (L a) | ((llen x2) == (1 + (llen x2)))}C) {x2 : (L a) | (x2 == ys)}ys {x2 : (L a) | (x2 == xs)}xs

where

421: {-@ type Cat a X Y = 
422:     {v:_|(llen v) = (llen X) + (llen Y)} @-}

By automatically instantiating

p := \xs acc -> llen acc = llen xs + llen ys

Recap

Abstract refinements decouple invariant from traversal

Reusable specifications for higher-order functions.

Automatic checking and instantiation by SMT.

Recap

Refinements: Types + Predicates
Subtyping: SMT Implication
Measures: Strengthened Constructors
Abstract: Refinements over Type Signatures
- Functions
- Data [continue]

Abstract Refinements

Induction

Induction

Example: loop redux

Iteration Dependence

Iteration Dependence

Iteration Dependence

Induction in loop (by hand)

Induction in loop (by hand)

Induction in loop (by hand)

Induction in loop (by hand)

Induction in loop (by type)

Induction in loop (by type)

Using Induction

Generalizes To Structures

Structural Induction

Example: Lists

Example: foldr

Example: foldr

foldr: Abstract Refinement

foldr: Base Case

foldr: Ind. Step

foldr: Output

Using foldr: Size

Using foldr: Append

Recap

Recap

Example: `loop` redux

Induction in `loop` (by hand)

Induction in `loop` (by hand)

Induction in `loop` (by hand)

Induction in `loop` (by hand)

Induction in `loop` (by type)

Induction in `loop` (by type)

Example: `foldr`

Example: `foldr`

`foldr`: Abstract Refinement

`foldr`: Base Case

`foldr`: Ind. Step

`foldr`: Output

Using `foldr`: Size

Using `foldr`: Append