# Indexed-Dependent Refinements

7: module LiquidArray where
8:
10:
11: {-@ LIQUID "--no-termination" @-}

# Indexed-Dependent Refinements

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

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

# Abstract Over the Domain and Range

We parameterize the definition with two abstract refinements:

33: {-@ data Vec a <dom :: Int -> Prop, rng :: Int -> a -> Prop>
34:       = V {a :: i:Int<dom> -> a <rng i>}
35:   @-}
• dom: describes the domain

• rng: describes each value with respect to its index

# Describing Vectors

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

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

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

# Describing Vectors

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

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

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

# Describing Vectors

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

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

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

# Operations on Vectors

Demo:

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

• This means abstracting over the domain and range

# Empty

empty returns a Vector whose domain is always false

123: {-@ empty :: forall <p :: Int -> a -> Prop>. Vec < {v:Int | 0=1}, p> a @-}
124:
125: empty     :: Vec  a
126: 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) && ((sumLens 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

139: {-@ get :: forall a <r :: Int -> a -> Prop, d :: Int -> Prop>.
140:            i: Int<d>
141:         -> a: Vec<d, r> a
142:         -> a<r i> @-}
143:
144: get :: Int -> Vec a -> a
145: 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

159: {-@ set :: forall a <r :: Int -> a -> Prop, d :: Int -> Prop>.
160:            i: Int<d>
161:         -> x: a<r i>
162:         -> a: Vec < {v:Int<d> | v != i}, r> a
163:         -> Vec <d, r> a @-}
164:
165: set :: Int -> a -> Vec a -> Vec a
166: 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 ((x5:{VV : (GHC.Types.Int) | ((papp1 d VV))}
-> {VV : a | ((papp2 r VV x5))})
-> (LiquidArray.Vec <((papp1 d VV)), \x2 VV -> ((papp2 r VV x2))> a))
-> (x5:{VV : (GHC.Types.Int) | ((papp1 d VV))}
-> {VV : a | ((papp2 r VV x5))})
-> (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 x1:{VV : (GHC.Types.Int) | ((papp1 d VV))}
-> x2:{VV : (GHC.Types.Int) | ((papp1 d VV))}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 == x2))}== {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:
173: type FibV =
174:      Vec <{\v -> 0=0}, {\j v -> ((v != 0) => (v = (fib j)))}> Int

Where fib is an uninterprented function

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

We used fib to define the axiom_fib

187: {-@ predicate Fib I =
188:   (fib i) = (if (i <= 1) then 1 else ((fib (i-1)) + (fib (i-2))))
189:   @-}
190:
191: {-@ assume axiom_fib :: i:Int -> {v: Bool | ((Prop v) <=> (Fib i))} @-}
192:
193: axiom_fib :: Int -> Bool
194: 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

203: {-@ fastFib :: x:Int -> {v:Int | v = fib(x)} @-}
204: fastFib     :: Int -> Int
205: 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, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int))
-> i:(GHC.Types.Int)
-> ((LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (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 n))) && (VV == 0)})
-> (LiquidArray.Vec <dom, rng> {VV : (GHC.Types.Int) | ((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

212: {-@ fibMemo :: FibV -> i:Int -> (FibV, {v: Int | v = (fib i)}) @-}
213:
214: fibMemo :: Vec Int -> Int -> (Vec Int, Int)
215: (LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int))
-> i:(GHC.Types.Int)
-> ((LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib i))})fibMemo (LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int))t (GHC.Types.Int)i
216:   | {VV : (GHC.Types.Int) | (VV == i)}i x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int)
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x1 <= x2))}<= {VV : (GHC.Types.Int) | (VV == (1  :  int))}1
217:   = forall a b <p2 :: a-> b-> Bool>.
x1:a
-> x2:{VV : b<p2 x1> | true}
-> {VV : (a, b)<p2> | ((fst VV) == x1) && ((snd VV) == x2)}({VV : (LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int)) | (VV == t)}t, x1:(GHC.Types.Bool)
-> {VV : (GHC.Types.Int) | (VV == 1) && (VV > 0) && (VV >= i)}
-> {VV : (GHC.Types.Int) | ((Prop x1)) && (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))
218:
219:   | otherwise
220:   = 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, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int)) | (VV == t)}t of
221:       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, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int))
-> i:(GHC.Types.Int)
-> ((LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int)), {VV : (GHC.Types.Int) | (VV == (fib i))})fibMemo {VV : (LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int)) | (VV == t)}t  ({VV : (GHC.Types.Int) | (VV == i)}ix1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}-{VV : (GHC.Types.Int) | (VV == (1  :  int))}1)
222:                ({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, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int))
-> i:(GHC.Types.Int)
-> ((LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (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)}ix1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 - x2))}-{VV : (GHC.Types.Int) | (VV == (2  :  int))}2)
223:                (GHC.Types.Int)n        = x1:(GHC.Types.Bool)
-> (GHC.Types.Int) -> {VV : (GHC.Types.Int) | ((Prop x1))}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 x1:(GHC.Types.Int)
-> x2:(GHC.Types.Int) -> {VV : (GHC.Types.Int) | (VV == (x1 + x2))}+ {VV : (GHC.Types.Int) | (VV == n2) && (VV == n2)}n2)
224:             in forall a b <p2 :: a-> b-> Bool>.
x1:a
-> x2:{VV : b<p2 x1> | true}
-> {VV : (a, b)<p2> | ((fst VV) == x1) && ((snd VV) == x2)}(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)
225:       n -> {VV : ({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)> | ((fst VV) == t)}({VV : (LiquidArray.Vec <True, \j10 VV -> ((VV /= 0) => (VV == (fib j10)))> (GHC.Types.Int)) | (VV == t)}t, {VV : (GHC.Types.Int) | ((VV /= 0) => (VV == (fib i)))}n)