Abstract refinements deoouple invariants from code
Yield precise, reusable summaries of HOFs
Problem
Require context-dependent invariants & summaries for HOFs.
A Solution
Decoupled invariants yield precise & reusable summaries
43: module Loop where 44: import Prelude hiding ((!!), foldr, length, (++)) 45: -- import Measures 46: import Language.Haskell.Liquid.Prelude 47: {-@ LIQUID "--no-termination" @-} 48: 49: {-@ measure llen :: (L a) -> Int 50: llen (N) = 0 51: llen (C x xs) = 1 + (llen xs) @-} 52: 53: size :: L a -> Int 54: add :: Int -> Int -> Int 55: loop :: Int -> Int -> α -> (Int -> α -> α) -> α 56: foldr :: (L a -> a -> b -> b) -> b -> L a -> b
loop
reduxRecall 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
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}
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
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
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) |
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)
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))
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)
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> @-}
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
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
Same idea applies for induction over structures ...
303: data L a = N 304: | C a (L a)
foldr
317: foldr f b N = b 318: foldr f b (C x xs) = f xs x (foldr f b xs)
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)
foldr
: Abstract Refinement352: 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 Case370: 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. Step389: 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
: Output407: 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>
foldr
: SizeWe 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
foldr
: AppendWe 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
Abstract refinements decouple invariant from iteration