7: module Loop where 8: import Prelude hiding ((!!), foldr, length, (++)) 9: import SimpleRefinements
loop
RevisitedRecall the higher-order loop
function
19: loop :: Int -> Int -> a -> (Int -> a -> a) -> a 20: forall a <p :: (GHC.Types.Int)-> a-> Bool>. lo:(GHC.Types.Int) -> hi:{VV : (GHC.Types.Int) | (lo <= VV)} -> {VV : a<p lo> | true} -> (i:(GHC.Types.Int) -> {VV : a<p i> | true} -> forall [ex:{VV : (GHC.Types.Int) | (VV == (i + 1))}].{VV : a<p ex> | true}) -> {VV : a<p hi> | true}loop (GHC.Types.Int)lo {VV : (GHC.Types.Int) | (lo <= VV)}hi {VV : a | ((papp2 p VV lo))}base i:(GHC.Types.Int) -> {VV : a | ((papp2 p VV i))} -> forall [ex:{VV : (GHC.Types.Int) | (VV == (i + 1))}].{VV : a | ((papp2 p VV ex))}f = x1:{VV : (GHC.Types.Int) | (VV == lo) && (VV <= hi)} -> {VV : a | ((papp2 p VV lo)) && ((papp2 p VV x1)) && (VV == base)} -> {VV : a | ((papp2 p VV hi))}go {VV : (GHC.Types.Int) | (VV == lo)}lo {VV : a | ((papp2 p VV lo)) && (VV == base)}base 21: where forall a. lo:{VV : (GHC.Types.Int) | (VV == lo) && (VV <= hi)} -> hi:{VV : (GHC.Types.Int) | (VV == hi) && (VV >= lo) && (VV >= lo) && (lo <= VV) && (lo <= VV)} -> {VV : a | ((papp2 p VV lo)) && ((papp2 p VV lo)) && (VV == base)} -> (x1:{VV : (GHC.Types.Int) | (VV >= lo) && (VV >= lo) && (VV < hi) && (VV < hi) && (lo <= VV) && (lo <= VV)} -> {VV : a | ((papp2 p VV x1))} -> {VV : a | ((papp2 p VV (x1 + 1)))}) -> i:{VV : (GHC.Types.Int) | (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi) && (lo <= VV) && (lo <= VV)} -> {VV : a | ((papp2 p VV i))} -> {VV : a | ((papp2 p VV hi)) && ((papp2 p VV hi))}go {VV : (GHC.Types.Int) | (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi) && (lo <= VV) && (lo <= VV)}i {VV : a | ((papp2 p VV i))}acc | {VV : (GHC.Types.Int) | (VV == i) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi) && (lo <= VV) && (lo <= VV)}i x:{VV : (GHC.Types.Int) | (VV >= i) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi) && (i <= VV) && (lo <= VV) && (lo <= VV)} -> y:{VV : (GHC.Types.Int) | (VV >= i) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi) && (i <= VV) && (lo <= VV) && (lo <= VV)} -> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x < y))}< {VV : (GHC.Types.Int) | (VV == hi) && (VV == hi) && (VV >= lo) && (VV >= lo) && (lo <= VV) && (lo <= VV)}hi = forall a. lo:{VV : (GHC.Types.Int) | (VV == lo) && (VV <= hi)} -> hi:{VV : (GHC.Types.Int) | (VV == hi) && (VV >= lo) && (VV >= lo) && (lo <= VV) && (lo <= VV)} -> {VV : a | ((papp2 p VV lo)) && ((papp2 p VV lo)) && (VV == base)} -> (x1:{VV : (GHC.Types.Int) | (VV >= lo) && (VV >= lo) && (VV < hi) && (VV < hi) && (lo <= VV) && (lo <= VV)} -> {VV : a | ((papp2 p VV x1))} -> {VV : a | ((papp2 p VV (x1 + 1)))}) -> i:{VV : (GHC.Types.Int) | (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi) && (lo <= VV) && (lo <= VV)} -> {VV : a | ((papp2 p VV i))} -> {VV : a | ((papp2 p VV hi)) && ((papp2 p VV hi))}go ({VV : (GHC.Types.Int) | (VV == i) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi) && (lo <= VV) && (lo <= VV)}ix:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+{VV : (GHC.Types.Int) | (VV == (1 : int))}1) (x1:{VV : (GHC.Types.Int) | (VV >= lo) && (VV >= lo) && (VV < hi) && (VV < hi) && (lo <= VV) && (lo <= VV)} -> {VV : a | ((papp2 p VV x1))} -> {VV : a | ((papp2 p VV (x1 + 1)))}f {VV : (GHC.Types.Int) | (VV == i) && (VV >= lo) && (VV >= lo) && (VV <= hi) && (VV <= hi) && (lo <= VV) && (lo <= VV)}i {VV : a | ((papp2 p VV i)) && (VV == acc)}acc) 22: | otherwise = {VV : a | ((papp2 p VV i)) && (VV == acc)}acc
We used loop
to write
28: {-@ add :: n:Nat -> m:Nat -> {v:Int| v = m + n} @-} 29: add :: Int -> Int -> Int 30: n:{VV : (GHC.Types.Int) | (VV >= 0)} -> m:{VV : (GHC.Types.Int) | (VV >= 0)} -> {VV : (GHC.Types.Int) | (VV == (m + n))}add {VV : (GHC.Types.Int) | (VV >= 0)}n {VV : (GHC.Types.Int) | (VV >= 0)}m = forall <p :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>. lo:(GHC.Types.Int) -> hi:{VV : (GHC.Types.Int) | (lo <= VV)} -> {VV : (GHC.Types.Int)<p lo> | (VV >= 0) && (VV >= n) && (n <= VV)} -> (i:(GHC.Types.Int) -> {VV : (GHC.Types.Int)<p i> | (VV >= 0) && (VV >= n) && (n <= VV)} -> forall [ex:{VV : (GHC.Types.Int) | (VV == (i + 1))}].{VV : (GHC.Types.Int)<p ex> | (VV >= 0) && (VV >= n) && (n <= VV)}) -> {VV : (GHC.Types.Int)<p hi> | (VV >= 0) && (VV >= n) && (n <= VV)}loop {VV : (GHC.Types.Int) | (VV == (0 : int))}0 {VV : (GHC.Types.Int) | (VV == m) && (VV >= 0)}m {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0)}n (x1:(GHC.Types.Int) -> i:{VV : (GHC.Types.Int) | (VV == (x1 + n)) && (VV == (n + x1)) && (VV >= 0) && (VV >= x1) && (VV >= n) && (x1 <= VV) && (n <= VV)} -> {VV : (GHC.Types.Int) | (VV == (i + 1)) && (VV > 0) && (VV > x1) && (VV > i) && (VV > n) && (VV >= 0) && (x1 <= VV) && (n <= VV)}\_ {VV : (GHC.Types.Int) | (VV >= 0) && (VV >= n) && (n <= VV)}i -> {VV : (GHC.Types.Int) | (VV == i) && (VV >= 0) && (VV >= n) && (n <= VV)}i x:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+ {VV : (GHC.Types.Int) | (VV == (1 : int))}1)
Problem: Verification requires an index dependent loop invariant p
i
with accumulator acc
: formally (p acc i)
loop
function
40: loop :: Int -> Int -> a -> (Int -> a -> a) -> a 41: loop lo hi base f = go lo base 42: where go i acc | i < hi = go (i+1) (f i acc) 43: | otherwise = acc
To verify output satisfies relation at hi
we prove that if
base
satisfies invariant at lo
(p base lo)
f
preserves the invariant at i
(p acc i)
then (p (f i acc) (i+1))
hi
(p (loop lo hi base f) hi)
We capture induction with an abstract refinement type for loop
64: {-@ loop :: forall a <p :: Int -> a -> Prop>. 65: lo:Int 66: -> hi:{v:Int|lo <= v} 67: -> base:a<p lo> 68: -> f:(i:Int -> a<p i> -> a<p (i+1)>) 69: -> a<p hi> 70: @-}
p
is the index dependent invariant!
76: p :: Int -> a -> Prop> -- ind hyp 77: base :: a<p lo> -- base case 78: f :: (i:Int -> a<p i> -> a <p (i+1)>) -- ind. step 79: out :: a<p hi> -- output holds at hi
87: add n m = loop 0 m n (\_ z -> z + 1)
The invariant is: p
instantiated with \i acc -> acc = i + n
base case: (p 0 n)
holds as n = 0 + n
ind. step \_ z -> z + 1
preserves invariant
acc = i + n
implies acc + 1 = (i + 1) + n
output hence, loop 0 m n (\_ z -> z + 1) = m + n
Which lets us verify that
.103: add :: n:Nat -> m:Nat -> {v:Int| v = m + n}
Same idea applies for induction over structures
We define a foldr
function that resembles loop.
114: {-@ foldr :: forall a b <p :: L a -> b -> Prop>. 115: (xs:L a -> x:a -> b <p xs> -> b <p (C x xs)>) 116: -> b <p N> 117: -> ys: L a 118: -> b <p ys> 119: @-} 120: foldr :: (L a -> a -> b -> b) -> b -> L a -> b 121: forall a b <p :: (SimpleRefinements.L a)-> b-> Bool>. (xs:(SimpleRefinements.L a) -> x:a -> {VV : b<p xs> | true} -> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (C x xs))}].{VV : b<p ex> | true}) -> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (N))}].{VV : b<p ex> | true} -> ys:(SimpleRefinements.L a) -> {VV : b<p ys> | true}foldr xs:(SimpleRefinements.L a) -> x:a -> {VV : b | ((papp2 p VV xs))} -> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (C x xs))}].{VV : b | ((papp2 p VV ex))}f forall [ex:{VV : (SimpleRefinements.L a) | (VV == (N))}].{VV : a | ((papp2 p VV ex))}b N = forall [ex:{VV : (SimpleRefinements.L a) | (VV == (N))}].{VV : a | ((papp2 p VV ex))}b 122: foldr f b (C x xs) = xs:(SimpleRefinements.L a) -> x:a -> {VV : b | ((papp2 p VV xs))} -> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (C x xs))}].{VV : b | ((papp2 p VV ex))}f {VV : (SimpleRefinements.L a) | (VV == xs)}xs {VV : a | (VV == x)}x (forall <p :: (SimpleRefinements.L a)-> b-> Bool>. (xs:(SimpleRefinements.L a) -> x:a -> {VV : b<p xs> | true} -> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (C x xs))}].{VV : b<p ex> | true}) -> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (N))}].{VV : b<p ex> | true} -> ys:(SimpleRefinements.L a) -> {VV : b<p ys> | true}foldr xs:(SimpleRefinements.L a) -> x:a -> {VV : b | ((papp2 p VV xs))} -> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (C x xs))}].{VV : b | ((papp2 p VV ex))}f forall [ex:{VV : (SimpleRefinements.L a) | (VV == (N))}].{VV : a | ((papp2 p VV ex))}b {VV : (SimpleRefinements.L a) | (VV == xs)}xs)
b
is related to nil N
f
extends relation over cons C
ys
We can now verify
139: {-@ size :: xs:L a -> {v: Int | v = (llen xs)} @-} 140: size :: L a -> Int 141: forall a. xs:(SimpleRefinements.L a) -> {VV : (GHC.Types.Int) | (VV == (llen xs))}size = forall <p :: (SimpleRefinements.L a)-> (GHC.Types.Int)-> Bool>. (xs:(SimpleRefinements.L a) -> x:a -> {VV : (GHC.Types.Int)<p xs> | (VV >= 0)} -> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (C x xs))}].{VV : (GHC.Types.Int)<p ex> | (VV >= 0)}) -> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (N))}].{VV : (GHC.Types.Int)<p ex> | (VV >= 0)} -> ys:(SimpleRefinements.L a) -> {VV : (GHC.Types.Int)<p ys> | (VV >= 0)}foldr (x1:(SimpleRefinements.L a) -> a -> n:{VV : (GHC.Types.Int) | (VV == (llen x1)) && (VV >= 0)} -> {VV : (GHC.Types.Int) | (VV == (n + 1)) && (VV > 0) && (VV > n) && (VV >= 0)}\_ _ {VV : (GHC.Types.Int) | (VV >= 0)}n -> {VV : (GHC.Types.Int) | (VV == n) && (VV >= 0)}n x:(GHC.Types.Int) -> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+ {VV : (GHC.Types.Int) | (VV == (1 : int))}1) {VV : (GHC.Types.Int) | (VV == (0 : int))}0
Here, the relation
(p xs acc)
is automatically instantiated with
acc = (llen xs)
Similarly we can now verify
160: {-@ ++ :: xs:L a -> ys:L a -> {v:L a | (llen v) = (llen xs) + (llen ys)} @-} 161: (SimpleRefinements.L a)xs forall a. xs:(SimpleRefinements.L a) -> ys:(SimpleRefinements.L a) -> {VV : (SimpleRefinements.L a) | ((llen VV) == ((llen xs) + (llen ys)))}++ (SimpleRefinements.L a)ys = forall <p :: (SimpleRefinements.L a)-> (SimpleRefinements.L a)-> Bool>. (xs:(SimpleRefinements.L a) -> x:a -> {VV : (SimpleRefinements.L a)<p xs> | true} -> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (C x xs))}].{VV : (SimpleRefinements.L a)<p ex> | true}) -> forall [ex:{VV : (SimpleRefinements.L a) | (VV == (N))}].{VV : (SimpleRefinements.L a)<p ex> | true} -> ys:(SimpleRefinements.L a) -> {VV : (SimpleRefinements.L a)<p ys> | true}foldr (x1:(SimpleRefinements.L a) -> a -> zs:{VV : (SimpleRefinements.L a) | ((llen VV) == ((llen x1) + (llen ys))) && ((llen VV) == ((llen ys) + (llen x1)))} -> {VV : (SimpleRefinements.L a) | ((llen VV) == (1 + (llen zs)))}\_ az (SimpleRefinements.L a)zs -> a -> xs:(SimpleRefinements.L a) -> {VV : (SimpleRefinements.L a) | ((llen VV) == (1 + (llen xs)))}C {VV : a | (VV == z)}z {VV : (SimpleRefinements.L a) | (VV == zs)}zs) {VV : (SimpleRefinements.L a) | (VV == ys)}ys {VV : (SimpleRefinements.L a) | (VV == xs)}xs
Here, the relation
(p xs acc)
is automatically instantiated with
(llen acc) = (llen xs) + (llen ys)