7: module LiquidArray where 8: 9: import Language.Haskell.Liquid.Prelude (liquidAssume)
We define a Vector of a
s implemented as a function from Int
to a
s
20: data Vec a = V (Int -> a)
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: @-}
dom
: describes the domain
rng
: describes each value with respect to its index
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: @-}
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: @-}
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 j
th fibonacci:
97: {-@ type FibV = 98: Vec <{\v -> 0=0}, {\j v -> ((v != 0) => (v = (fib j)))}> Int 99: @-}
We give appropriate types to vector operations (empty, set, get...)
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!")
If i
satisfies the domain then if we get
the i
th 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
If i
satisfies the domain then if we set
the i
th 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
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
Now we can efficiently compute the i
th 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
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)