Indexed-Dependent Refinements

Indexed-Dependent Refinements

7: module LiquidArray where
8: 
9: import Language.Haskell.Liquid.Prelude (liquidAssume)

Indexed-Dependent Refinements

We define a Vector of as implemented as a function from Int to as

20: data Vec a = V (Int -> a)

Abstract Over the Domain and Range

We parameterize the definition with two abstract refinements:

31: {-@ data Vec a <dom :: Int -> Prop, rng :: Int -> a -> Prop>
32:       = V {a :: i:Int<dom> -> a <rng i>}
33:   @-}

Describing Vectors

By instantiating these two predicates, we describe Vector's domain and range
45: {-@ data Vec a <dom :: Int -> Prop, rng :: Int -> a -> Prop>
46:       = V {a :: i:Int<dom> -> a <rng i>}
47:   @-}


A vector of Int defined on values less than 42 containing values equal to their index:

57: {-@ type IdVec = 
58:       Vec <{\v -> (v < 42)}, {\j v -> (v = j)}> Int
59:   @-}

Describing Vectors

By instantiating these two predicates, we describe Vector's domain and range
65: {-@ data Vec a <dom :: Int -> Prop, rng :: Int -> a -> Prop>
66:       = V {a :: i:Int<dom> -> a <rng i>}
67:   @-}


A vector defined on the range [0..n) with its last element equal to 0:

76: {-@ type ZeroTerm N = 
77:      Vec <{\v -> (0 <= v && v < N)}, {\j v -> (j = N - 1 => v = 0)}> Int
78:   @-}

Describing Vectors

By instantiating these two predicates, we describe Vector's domain and range
84: {-@ data Vec a <dom :: Int -> Prop, rng :: Int -> a -> Prop>
85:       = V {a :: i:Int<dom> -> a <rng i>}
86:   @-}


A vector defined on integers whose value at index j is either 0 or the jth fibonacci:

97: {-@ type FibV =  
98:      Vec <{\v -> 0=0}, {\j v -> ((v != 0) => (v = (fib j)))}> Int 
99:   @-}

Operations on Vectors

Demo

We give appropriate types to vector operations (empty, set, get...)

Empty

empty returns a Vector whose domain is always false

121: {-@ empty :: forall <p :: Int -> a -> Prop>. Vec < {v:Int | 0=1}, p> a @-}
122: empty     :: Vec  a
123: forall a <p :: (GHC.Types.Int)-> a-> Bool>.
(LiquidArray.Vec <false, \_ VV -> p> a)empty     = ({VV : (GHC.Types.Int) | false} -> {VV : a | false})
-> (LiquidArray.Vec <false, \_ VV -> false> {VV : a | false})V (({VV : (GHC.Types.Int) | false} -> {VV : a | false})
 -> (LiquidArray.Vec <false, \_ VV -> false> {VV : a | false}))
-> ({VV : (GHC.Types.Int) | false} -> {VV : a | false})
-> (LiquidArray.Vec <false, \_ VV -> false> {VV : a | false})$ {VV : (GHC.Types.Int) | false} -> {VV : a | false}\_ -> ([(GHC.Types.Char)] -> {VV : a | false}error {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Empty array!")

Typing Get

If i satisfies the domain then if we get the ith element of an array, the result should satisfy the range at i

136: {-@ get :: forall a <r :: Int -> a -> Prop, d :: Int -> Prop>.
137:            i: Int<d>
138:         -> a: Vec<d, r> a
139:         -> a<r i> @-}
140: get :: Int -> Vec a -> a
141: forall a <r :: (GHC.Types.Int)-> a-> Bool, d :: (GHC.Types.Int)-> Bool>.
i:{VV : (GHC.Types.Int)<d> | true}
-> (LiquidArray.Vec <d, \_ VV -> r> a) -> {VV : a<r i> | true}get {VV : (GHC.Types.Int) | ((papp1 d VV))}i (V f) = i:{VV : (GHC.Types.Int) | ((papp1 d VV))}
-> {VV : a | ((papp2 r VV i))}f {VV : (GHC.Types.Int) | ((papp1 d VV)) && (VV == i)}i

Typing Set

If i satisfies the domain then if we set the ith element of a Vector to a value that satisfies range at i, then Vector's domain will be extended with i

155: {-@ set :: forall a <r :: Int -> a -> Prop, d :: Int -> Prop>.
156:            i: Int<d>
157:         -> x: a<r i>
158:         -> a: Vec < {v:Int<d> | v != i}, r> a
159:         -> Vec <d, r> a @-}
160: set :: Int -> a -> Vec a -> Vec a
161: forall a <r :: (GHC.Types.Int)-> a-> Bool, d :: (GHC.Types.Int)-> Bool>.
i:{VV : (GHC.Types.Int)<d> | true}
-> {VV : a<r i> | true}
-> (LiquidArray.Vec <d & (VV /= i), \_ VV -> r> a)
-> (LiquidArray.Vec <d, \_ VV -> r> a)set {VV : (GHC.Types.Int) | ((papp1 d VV))}i {VV : a | ((papp2 r VV i))}v (V f) = (i:{VV : (GHC.Types.Int) | ((papp1 d VV))}
 -> {VV : a | ((papp2 r VV i))})
-> (LiquidArray.Vec <((papp1 d VV)), \x1 VV -> ((papp2 r VV x1))> a)V ((x4:{VV : (GHC.Types.Int) | ((papp1 d VV))}
  -> {VV : a | ((papp2 r VV x4))})
 -> (LiquidArray.Vec <((papp1 d VV)), \x2 VV -> ((papp2 r VV x2))> a))
-> (x4:{VV : (GHC.Types.Int) | ((papp1 d VV))}
    -> {VV : a | ((papp2 r VV x4))})
-> (LiquidArray.Vec <((papp1 d VV)), \x2 VV -> ((papp2 r VV x2))> a)$ k:{VV : (GHC.Types.Int) | ((papp1 d VV))}
-> {VV : a | ((papp2 r VV k))}\{VV : (GHC.Types.Int) | ((papp1 d VV))}k -> if {VV : (GHC.Types.Int) | ((papp1 d VV)) && (VV == k)}k x:{VV : (GHC.Types.Int) | ((papp1 d VV))}
-> y:{VV : (GHC.Types.Int) | ((papp1 d VV))}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x == y))}== {VV : (GHC.Types.Int) | ((papp1 d VV)) && (VV == i)}i then {VV : a | ((papp2 r VV i)) && (VV == v)}v else i:{VV : (GHC.Types.Int) | ((papp1 d VV)) && (VV /= i)}
-> {VV : a | ((papp2 r VV i))}f {VV : (GHC.Types.Int) | ((papp1 d VV)) && (VV == k)}k

Using Vectors

Remember the fibonacci memoization Vector:
168: type FibV = 
169:      Vec <{\v -> 0=0}, {\j v -> ((v != 0) => (v = (fib j)))}> Int


Where fib is an uninterprented function

175: {-@ measure fib :: Int -> Int @-}


We used fib to define the axiom_fib

182: {-@ predicate Fib I = 
183:   (fib i) = ((i <= 1)?1:((fib (i-1)) + fib (i-2)))
184:   @-}
185: 
186: {-@ assume axiom_fib :: i:Int -> {v: Bool | ((Prop v) <=> (Fib i))} @-}
187: axiom_fib :: Int -> Bool
188: i:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> ((fib i) == (if (i <= 1) then 1 else ((fib (i - 1)) + (fib (i - 2))))))}axiom_fib (GHC.Types.Int)i = forall a. aundefined

Fast Fibonacci

Now we can efficiently compute the ith fibonacci number

197: {-@ fastFib :: x:Int -> {v:Int | v = fib(x)} @-}
198: fastFib     :: Int -> Int
199: x:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (fib x))}fastFib (GHC.Types.Int)n   = ((LiquidArray.Vec <false, \x1 VV -> ((VV /= 0) => (VV == (fib x1)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib n))})
-> {VV : (GHC.Types.Int) | (VV == (fib n))}snd (((LiquidArray.Vec <false, \x2 VV -> ((VV /= 0) => (VV == (fib x2)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib n))})
 -> {VV : (GHC.Types.Int) | (VV == (fib n))})
-> ((LiquidArray.Vec <false, \x2 VV -> ((VV /= 0) => (VV == (fib x2)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib n))})
-> {VV : (GHC.Types.Int) | (VV == (fib n))}$ (LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int))
-> i:(GHC.Types.Int)
-> ((LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib i))})fibMemo (forall <rng :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool, dom :: (GHC.Types.Int)-> Bool>.
(i:{VV : (GHC.Types.Int)<dom> | true}
 -> {VV : (GHC.Types.Int)<rng i> | ((VV /= 0) => (VV == (fib $$"Empty array!"))) && ((VV /= 0) => (VV == (fib n))) && (VV == 0)})
-> (LiquidArray.Vec <dom, rng> {VV : (GHC.Types.Int) | ((VV /= 0) => (VV == (fib $$"Empty array!"))) && ((VV /= 0) => (VV == (fib n))) && (VV == 0)})V ((GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (0  :  int))}\_ -> {VV : (GHC.Types.Int) | (VV == (0  :  int))}0)) {VV : (GHC.Types.Int) | (VV == n)}n

Fibonacci Memo

206: {-@ fibMemo :: FibV -> i:Int -> (FibV, {v: Int | v = fib(i)}) @-}
207: fibMemo :: Vec Int -> Int -> (Vec Int, Int)
208: (LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int))
-> i:(GHC.Types.Int)
-> ((LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib i))})fibMemo (LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int))t (GHC.Types.Int)i 
209:   | {VV : (GHC.Types.Int) | (VV == i)}i x:(GHC.Types.Int)
-> y:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x <= y))}<= {VV : (GHC.Types.Int) | (VV == (1  :  int))}1    
210:   = forall a b <p2 :: a-> b-> Bool>.
x1_(,):a -> {VV : b<p2 x1_(,)> | true} -> (a, b)<p2>({VV : (LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int)) | (VV == t)}t, b:(GHC.Types.Bool)
-> {VV : (GHC.Types.Int) | (VV == 1) && (VV > 0) && (VV >= i)}
-> {VV : (GHC.Types.Int) | ((Prop b)) && (VV == 1) && (VV > 0) && (VV >= i)}liquidAssume (i:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> ((fib i) == (if (i <= 1) then 1 else ((fib (i - 1)) + (fib (i - 2))))))}axiom_fib {VV : (GHC.Types.Int) | (VV == i)}i) ({VV : (GHC.Types.Int) | (VV == (1  :  int))}1 :: Int))
211:   
212:   | otherwise 
213:   = case forall <d :: (GHC.Types.Int)-> Bool, r :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
i:{VV : (GHC.Types.Int)<d> | true}
-> (LiquidArray.Vec <d, \_ VV -> r> (GHC.Types.Int))
-> {VV : (GHC.Types.Int)<r i> | true}get {VV : (GHC.Types.Int) | (VV == i)}i {VV : (LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int)) | (VV == t)}t of   
214:       0 -> let ({VV : (LiquidArray.Vec <True, \x1 VV -> ((VV /= 0) => (VV == (fib x1)))> (GHC.Types.Int)) | (VV == t1)}t1, {VV : (GHC.Types.Int) | (VV == n1)}n1) = (LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int))
-> i:(GHC.Types.Int)
-> ((LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib i))})fibMemo {VV : (LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int)) | (VV == t)}t  ({VV : (GHC.Types.Int) | (VV == i)}ix:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x - y))}-{VV : (GHC.Types.Int) | (VV == (1  :  int))}1)
215:                ({VV : (LiquidArray.Vec <(VV /= i), \x1 VV -> ((VV /= 0) => (VV == (fib x1)))> (GHC.Types.Int)) | (VV == t2)}t2, {VV : (GHC.Types.Int) | (VV == n2)}n2) = (LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int))
-> i:(GHC.Types.Int)
-> ((LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib i))})fibMemo {VV : (LiquidArray.Vec <True, \x1 VV -> ((VV /= 0) => (VV == (fib x1)))> (GHC.Types.Int)) | (VV == t1) && (VV == t1)}t1 ({VV : (GHC.Types.Int) | (VV == i)}ix:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x - y))}-{VV : (GHC.Types.Int) | (VV == (2  :  int))}2)
216:                (GHC.Types.Int)n        = b:(GHC.Types.Bool)
-> (GHC.Types.Int) -> {VV : (GHC.Types.Int) | ((Prop b))}liquidAssume (i:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> ((fib i) == (if (i <= 1) then 1 else ((fib (i - 1)) + (fib (i - 2))))))}axiom_fib {VV : (GHC.Types.Int) | (VV == i)}i) ({VV : (GHC.Types.Int) | (VV == n1) && (VV == n1)}n1 x:(GHC.Types.Int)
-> y:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x + y))}+ {VV : (GHC.Types.Int) | (VV == n2) && (VV == n2)}n2)
217:            in  forall a b <p2 :: a-> b-> Bool>.
x1_(,):a -> {VV : b<p2 x1_(,)> | true} -> (a, b)<p2>(forall <d :: (GHC.Types.Int)-> Bool, r :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool>.
i:{VV : (GHC.Types.Int)<d> | true}
-> {VV : (GHC.Types.Int)<r i> | true}
-> (LiquidArray.Vec <d & (VV /= i), \_ VV -> r> (GHC.Types.Int))
-> (LiquidArray.Vec <d, \_ VV -> r> (GHC.Types.Int))set {VV : (GHC.Types.Int) | (VV == i)}i {VV : (GHC.Types.Int) | (VV == n)}n {VV : (LiquidArray.Vec <(VV /= i), \x1 VV -> ((VV /= 0) => (VV == (fib x1)))> (GHC.Types.Int)) | (VV == t2) && (VV == t2)}t2,  {VV : (GHC.Types.Int) | (VV == n)}n)
218:       n -> ({VV : (LiquidArray.Vec <True, \x1 VV -> ((VV /= 0) => (VV == (fib x1)))> (GHC.Types.Int)) | (VV == t)}, {VV : (GHC.Types.Int) | (VV == (fib i)) && (VV /= 0)})<\_ VV -> (VV == (fib i)) && (VV /= 0)>({VV : (LiquidArray.Vec <True, \j VV -> ((VV /= 0) => (VV == (fib j)))> (GHC.Types.Int)) | (VV == t)}t, {VV : (GHC.Types.Int) | ((VV /= 0) => (VV == (fib i)))}n)