\( \require{color} \definecolor{kvcol}{RGB}{203,23,206} \definecolor{tycol}{RGB}{5,177,93} \definecolor{refcol}{RGB}{18,110,213} \newcommand{\quals}{\mathbb{Q}} \newcommand{\defeq}{\ \doteq\ } \newcommand{\subty}{\preceq} \newcommand{\True}{\mathit{True}} \newcommand{\Int}{\mathtt{Int}} \newcommand{\Nat}{\mathtt{Nat}} \newcommand{\Zero}{\mathtt{Zero}} \newcommand{\foo}[4]{{#1}^{#4} + {#2}^{#4} = {#3}^{#4}} \newcommand{\reft}[3]{\{\bindx{#1}{#2} \mid {#3}\}} \newcommand{\ereft}[3]{\bindx{#1}{\{#2 \mid #3\}}} \newcommand{\bindx}[2]{{#1}\!:\!{#2}} \newcommand{\reftx}[2]{\{{#1}\mid{#2}\}} \newcommand{\inferrule}[3][]{\frac{#2}{#3}\;{#1}} \newcommand{\kvar}[1]{\color{kvcol}{\mathbf{\kappa_{#1}}}} \newcommand{\llen}[1]{\mathtt{llen}(#1)} \)

Abstract Refinements

Decoupling Invariants & Code

  • Abstract refinements deoouple invariants from code

  • Yield precise, reusable summaries of HOFs

Recall: Tricky Problem


Problem

Require context-dependent invariants & summaries for HOFs.



A Solution

Decoupled invariants yield precise & reusable summaries

Induction

Example: loop redux

Recall the higher-order loop


71: forall a <p :: GHC.Types.Int a -> Prop>.
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:{v : Int | v >= lo && v <= hi && lo <= v}
-> {VV : a | papp2 p VV x1} -> {VV : a | papp2 p VV hi}go {v : Int | v == lo}lo {VV : a | papp2 p VV lo && VV == base}base
72:   where 
73:     x1:{v : Int | v >= lo && lo <= v && v <= hi}
-> {VV : a | papp2 p VV x1} -> {VV : a | papp2 p VV hi}go {VV : Int | VV >= lo && lo <= VV && VV <= hi}i {VV : a | papp2 p VV i}acc 
74:       | {v : Int | v == i && v >= lo && lo <= v && v <= hi}i x1:Int -> x2:Int -> {v : Bool | Prop v <=> x1 < v}< {v : Int | v == hi && lo <= v}hi    = x1:{VV : Int | VV >= lo && lo <= VV && VV <= hi}
-> {VV : a | papp2 p VV x1} -> {VV : a | papp2 p VV hi}go ({v : Int | v == i && v >= lo && lo <= v && v <= hi}ix1:Int -> x2:Int -> {v : Int | v == x1 + x2}+{v : Int | v == (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 {v : Int | v == i && v >= lo && v <= hi && lo <= v}i {VV : a | papp2 p VV i && VV == acc}acc)
75:       | otherwise = {VV : a | papp2 p VV i && VV == acc}acc

Iteration Dependence

We used loop to write


84: {-@ add :: n:Nat -> m:Nat -> {v:Nat|v=m+n} @-}
85: 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


106: {-@ add :: n:Nat -> m:Nat -> {v:Nat|v=m+n} @-}
107: 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


123: {-@ add :: n:Nat -> m:Nat -> {v:Nat|v=m+n} @-}
124: 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)


141: loop lo hi base f = go lo base
142:   where 
143:     go i acc 
144:       | i < hi    = go (i+1) (f i acc)
145:       | otherwise = acc


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

Induction in loop (by hand)


167: loop lo hi base f = go lo base
168:   where 
169:     go i acc 
170:       | i < hi    = go (i+1) (f i acc)
171:       | otherwise = acc


Base Case:   Initial accumulator base satisfies invariant

(p lo base)

Induction in loop (by hand)


186: loop lo hi base f = go lo base
187:   where 
188:     go i acc 
189:       | i < hi    = go (i+1) (f i acc)
190:       | otherwise = acc


Inductive Step:   f preserves invariant at i

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

Induction in loop (by hand)


204: loop lo hi base f = go lo base
205:   where 
206:     go i acc 
207:       | i < hi    = go (i+1) (f i acc)
208:       | 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


226: {-@ loop :: forall a <p :: Int -> a -> Prop>.
227:         lo:Int
228:      -> hi:{Int | lo <= hi}
229:      -> base:a<p lo>                      
230:      -> f:(i:Int -> a<p i> -> a<p (i+1)>) 
231:      -> a<p hi>                           @-}


Induction in loop (by type)

p is the index dependent invariant!


243: p    :: Int -> a -> Prop             -- invt 
244: base :: a<p lo>                      -- base 
245: f    :: i:Int -> a<p i> -> a<p(i+1)> -- step
246: out  :: a<p hi>                      -- goal

Using Induction

255: {-@ add :: n:Nat -> m:Nat -> {v:Nat| v=m+n} @-}
256: 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:Int
-> x2:{v : Int | x1 <= v}
-> {v : Int | v == x1 + n && v == n + x1 && v >= 0 && v >= x1 && v >= n}
-> (x5:Int
    -> {v : Int | v == x5 + n && v == n + x5 && v >= 0 && v >= x5 && v >= n}
    -> forall [ex:{VV : Int | VV == x5 + 1}].{v : Int | v == ex + n && v == n + ex && v >= 0 && v >= ex && v >= n})
-> {v : Int | v == n + x2 && v == x2 + n && v >= 0 && v >= n && v >= x2}loop {v : Int | v == (0  :  int)}0 {v : Int | v == m && v >= 0}m {v : Int | v == n && v >= 0}n (x1:Int
-> x2:{v : Int | v == x1 + n && v == n + x1 && v >= 0 && v >= x1 && v >= n}
-> {v : Int | v == x2 + 1 && v > 0 && v > x1 && v > n && v > x2 && v >= 0}\_ {VV : Int | VV >= 0 && VV >= n}z -> {v : Int | v == z && v >= 0 && v >= n}z x1:Int -> x2:Int -> {v : Int | v == x1 + x2}+ {v : Int | v == (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


303: data L a = N 
304:          | C a (L a)


Lets write a generic loop over such lists ...

Example: foldr


317: foldr f b N        = b
318: foldr f b (C x xs) = f xs x (foldr f b xs)


Lets brace ourselves for the type...

Example: foldr

331: {-@ foldr :: 
332:     forall a b <p :: L a -> b -> Prop>. 
333:       (xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)>) 
334:     -> b<p N> 
335:     -> ys:L a
336:     -> b<p ys>                            @-}
337: forall a b <p :: (Loop.L a) b -> Prop>.
(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
338: 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 {v : (L a) | v == xs}xs {VV : a | VV == x}x (forall a b <p :: (Loop.L a) b -> Prop>.
(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 {v : (L a) | v == xs}xs)


Lets step through the type...

foldr: Abstract Refinement

352: p    :: L a -> b -> Prop   
353: step :: xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)> 
354: base :: b<p N> 
355: ys   :: L a
356: out  ::  b<p ys>                            


(p xs b) relates b with folded xs

p :: L a -> b -> Prop

foldr: Base Case

370: p    :: L a -> b -> Prop   
371: step :: xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)> 
372: base :: b<p N> 
373: ys   :: L a
374: out  :: b<p ys>                            


base is related to empty list N

base :: b<p N>

foldr: Ind. Step

389: p    :: L a -> b -> Prop   
390: step :: xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)> 
391: base :: b<p N> 
392: ys   :: L a
393: 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

407: p    :: L a -> b -> Prop   
408: step :: xs:_ -> x:_ -> b<p xs> -> b<p(C x xs)> 
409: base :: b<p N> 
410: ys   :: L a
411: 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

426: {-@ size :: xs:_ -> {v:Int| v = llen xs} @-}
427: forall a. x1:(L a) -> {v : Int | v == llen x1}size     = forall a b <p :: (Loop.L a) b -> Prop>.
(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:{v : Int | v == llen x1 && v >= 0}
-> {v : Int | v == x3 + 1 && v > 0 && v > x3 && v >= 0}\_ _ {VV : Int | VV >= 0}n -> {v : Int | v == n && v >= 0}n x1:Int -> x2:Int -> {v : Int | v == x1 + x2}+ {v : Int | v == (1  :  int)}1) {v : Int | v == (0  :  int)}0


by automatically instantiating

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

Using foldr: Append

We can now verify

444: {-@ (++) :: xs:_ -> ys:_ -> Cat a xs ys @-} 
445: (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 -> Prop>.
(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) -> {v : (L a) | llen v == 1 + llen x3}\_ -> a -> x2:(L a) -> {v : (L a) | llen v == 1 + llen v}C) {v : (L a) | v == ys}ys {v : (L a) | v == xs}xs 


where

454: {-@ type Cat a X Y = 
455:     {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 iteration


Reusable summaries 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