Abstract Refinements

Induction

Encoding induction with Abstract refinements

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

  1. Refinements: Types + Predicates
  2. Subtyping: SMT Implication
  3. Measures: Strengthened Constructors
  4. Abstract: Refinements over Type Signatures