Abstract Refinements {#data} ============================ Recap ----- **So far** Decouple invariants from *functions*

**Next** Decouple invariants from *data structures*

Decouple Invariants From Data {#vector} ======================================= Example: Vectors ----------------

28: module LiquidArray where
29: 
30: import Language.Haskell.Liquid.Prelude (liquidAssume, liquidError)
31: 
32: {-@ LIQUID "--no-termination" @-}
33: 
34: fibMemo   :: Vec Int -> Int -> (Vec Int, Int)
35: fastFib   :: Int -> Int
36: idv       :: Int -> Vec Int
37: axiom_fib :: Int -> Bool
38: i:(Int)
-> {v : (Bool) | (((Prop v)) <=> ((fib i) == (if (i <= 1) then 1 else ((fib (i - 1)) + (fib (i - 2))))))}axiom_fib = forall a. aundefined
39: 
40: {-@ predicate AxFib I = (fib I) == (if I <= 1 then 1 else fib(I-1) + fib(I-2)) @-}

Implemented as maps from `Int` to `a`

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

Abstract *Domain* and *Range* ----------------------------- Parameterize type with *two* abstract refinements:

65: {-@ data Vec a < dom :: Int -> Prop,
66:                  rng :: Int -> a -> Prop >
67:       = V {a :: i:Int<dom> -> a <rng i>}  @-}

- `dom`: *domain* on which `Vec` is *defined* - `rng`: *range* and relationship with *index* Abstract *Domain* and *Range* ----------------------------- Diverse `Vec`tors by *instantiating* `dom` and `rng`

A quick alias for *segments* between `I` and `J`

90: {-@ predicate Seg V I J = (I <= V && V < J) @-}

Ex: Identity Vectors -------------------- Defined between `[0..N)` mapping each key to itself:

105: {-@ type IdVec N = Vec <{\v -> (Seg v 0 N)}, 
106:                         {\k v -> v=k}> 
107:                        Int                  @-}

Ex: Identity Vectors -------------------- Defined between `[0..N)` mapping each key to itself:

120: {-@ idv :: n:Nat -> (IdVec n) @-}
121: n:{VV : (Int) | (VV >= 0)}
-> (Vec <(VV < n) && (0 <= VV), \k4 VV -> (VV == k4)> (Int))idv {VV : (Int) | (VV >= 0)}n   = forall <rng :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool, dom :: (GHC.Types.Int)-> Bool>.
(i:{x13 : (Int)<dom> | true}
 -> {x12 : (Int)<rng i> | (x12 > 0) && (x12 >= 0) && (x12 < n)})
-> (Vec <dom, rng> {x12 : (Int) | (x12 > 0) && (x12 >= 0) && (x12 < n)})V (\{VV : (Int) | (VV >= 0) && (VV < n)}k -> if {x2 : (Int) | (x2 == (0  :  int))}0 x1:{x12 : (Int) | (x12 >= 0) && (x12 < n) && (0 <= x12) && (x12 <= k)}
-> x2:{x12 : (Int) | (x12 >= 0) && (x12 < n) && (0 <= x12) && (x12 <= k)}
-> {x2 : (Bool) | (((Prop x2)) <=> (x1 < x2))}< {x4 : (Int) | (x4 == k) && (x4 >= 0) && (x4 < n)}k x1:(Bool)
-> x2:(Bool)
-> {x2 : (Bool) | (((Prop x2)) <=> (((Prop x1)) && ((Prop x2))))}&& {x4 : (Int) | (x4 == k) && (x4 >= 0) && (x4 < n)}k x1:{x12 : (Int) | (x12 >= 0) && (x12 >= k) && (0 <= x12) && (x12 <= n)}
-> x2:{x12 : (Int) | (x12 >= 0) && (x12 >= k) && (0 <= x12) && (x12 <= n)}
-> {x2 : (Bool) | (((Prop x2)) <=> (x1 < x2))}< {x3 : (Int) | (x3 == n) && (x3 >= 0)}n 
122:                      then {x4 : (Int) | (x4 == k) && (x4 >= 0) && (x4 < n)}k 
123:                      else {x2 : [(Char)] | false} -> {x1 : (Int) | false}liquidError {x3 : [(Char)] | ((len x3) >= 0) && ((sumLens x3) >= 0)}"eeks")

Demo:Whats the problem? How can we fix it?

Ex: Zero-Terminated Vectors --------------------------- Defined between `[0..N)`, with *last* element equal to `0`:

142: {-@ type ZeroTerm N = 
143:      Vec <{\v -> (Seg v 0 N)}, 
144:           {\k v -> (k = N-1 => v = 0)}> 
145:           Int                             @-}

Ex: Fibonacci Table ------------------- A vector whose value at index `k` is either - `0` (undefined), or, - `k`th fibonacci number

161: {-@ type FibV =  
162:      Vec <{\v -> true}, 
163:           {\k v -> (v = 0 || v = (fib k))}> 
164:           Int                               @-}

Accessing Vectors ----------------- Next: lets *abstractly* type `Vec`tor operations, *e.g.*
- `empty` - `set` - `get` Ex: Empty Vectors ----------------- `empty` returns Vector whose domain is `false`

190: {-@ empty :: forall <p :: Int -> a -> Prop>. 
191:                Vec <{v:Int|false}, p> a     @-}
192: 
193: forall a <p :: (GHC.Types.Int)-> a-> Bool>.
(Vec <false, \_ VV -> p> a)empty     = ({x4 : (Int) | false} -> {VV : a | false})
-> (Vec <false, \_ VV -> false> {VV : a | false})V (({x9 : (Int) | false} -> {VV : a | false})
 -> (Vec <false, \_ VV -> false> {VV : a | false}))
-> ({x9 : (Int) | false} -> {VV : a | false})
-> (Vec <false, \_ VV -> false> {VV : a | false})$ {x1 : (Int) | false} -> {VV : a | false}\_ -> [(Char)] -> {VV : a | false}error {x3 : [(Char)] | ((len x3) >= 0) && ((sumLens x3) >= 0)}"empty vector!"

Demo: What would happen if we changed `false` to `true`?

Ex: `get` Key's Value --------------------- - *Input* `key` in *domain* - *Output* value in *range* related with `k`

211: {-@ get :: forall a <d :: Int -> Prop,  
212:                      r :: Int -> a -> Prop>.
213:            key:Int <d>
214:         -> vec:Vec <d, r> a
215:         -> a<r key>                        @-}
216: 
217: forall a <d :: (GHC.Types.Int)-> Bool, r :: (GHC.Types.Int)-> a-> Bool>.
key:{VV : (Int)<d> | true}
-> (Vec <d, \_ VV -> r> a) -> {VV : a<r key> | true}get {VV : (Int) | ((papp1 d VV))}k (V f) = x1:{x2 : (Int) | ((papp1 d x2))} -> {VV : a | ((papp2 r VV x1))}f {x3 : (Int) | ((papp1 d x3)) && (x3 == k)}k

Ex: `set` Key's Value --------------------- -

Input `key` in *domain*

Input `val` in *range* related with `key`

Input `vec` defined at *domain except at* `key`

Output domain *includes* `key`

Ex: `set` Key's Value ---------------------

236: {-@ set :: forall a <d :: Int -> Prop,
237:                      r :: Int -> a -> Prop>.
238:            key: Int<d> -> val: a<r key>
239:         -> vec: Vec<{v:Int<d>| v /= key},r> a
240:         -> Vec <d, r> a                     @-}
241: forall a <d :: (GHC.Types.Int)-> Bool, r :: (GHC.Types.Int)-> a-> Bool>.
key:{VV : (Int)<d> | true}
-> {VV : a<r key> | true}
-> (Vec <d & (VV /= key), \_ VV -> r> a)
-> (Vec <d, \_ VV -> r> a)set {VV : (Int) | ((papp1 d VV))}key {VV : a | ((papp2 r VV key))}val (V f) = ({x6 : (Int) | ((papp1 d x6))} -> {VV : a | ((papp2 r VV key))})
-> (Vec <((papp1 d x3)), \_ VV -> ((papp2 r VV key))> {VV : a | ((papp2 r VV key))})V (({x13 : (Int) | ((papp1 d x13))} -> {VV : a | ((papp2 r VV key))})
 -> (Vec <((papp1 d x10)), \_ VV -> ((papp2 r VV key))> {VV : a | ((papp2 r VV key))}))
-> ({x13 : (Int) | ((papp1 d x13))}
    -> {VV : a | ((papp2 r VV key))})
-> (Vec <((papp1 d x10)), \_ VV -> ((papp2 r VV key))> {VV : a | ((papp2 r VV key))})$ \{VV : (Int) | ((papp1 d VV))}k -> if {x3 : (Int) | ((papp1 d x3)) && (x3 == k)}k x1:{x6 : (Int) | ((papp1 d x6))}
-> x2:{x6 : (Int) | ((papp1 d x6))}
-> {x2 : (Bool) | (((Prop x2)) <=> (x1 == x2))}== {x3 : (Int) | ((papp1 d x3)) && (x3 == key)}key 
242:                                 then {VV : a | ((papp2 r VV key)) && (VV == val)}val 
243:                                 else x1:{x3 : (Int) | ((papp1 d x3)) && (x3 /= key)}
-> {VV : a | ((papp2 r VV x1))}f {x3 : (Int) | ((papp1 d x3)) && (x3 == key)}key

Demo: Help! Can you spot and fix the errors?

Using the Vector API -------------------- Memoized Fibonacci ------------------ Use `Vec` API to write a *memoized* fibonacci function

Using the fibonacci table:

267: type FibV =  
268:      Vec <{\v -> true}, 
269:           {\k v -> (v = 0 || v = (fib k))}> 
270:           Int

But wait, what is `fib` ?

Specifying Fibonacci -------------------- `fib` is *uninterpreted* in the refinement logic

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

Specifying Fibonacci -------------------- We *axiomatize* the definition of `fib` in SMT ...

300: predicate AxFib I = 
301:   (fib I) == if I <= 1 
302:                then 1 
303:                else fib(I-1) + fib(I-2)

Specifying Fibonacci -------------------- Finally, lift axiom into LiquidHaskell as *ghost function*

314: {-@ axiom_fib :: 
315:       i:_ -> {v:_|((Prop v) <=> (AxFib i))} @-}

**Note:** Recipe for *escaping* SMT limitations 1. *Prove* fact externally 2. *Use* as ghost function call

Fast Fibonacci -------------- An efficient fibonacci function

336: {-@ fastFib :: n:Int -> {v:_ | v = (fib n)} @-}
337: n:(Int) -> {v : (Int) | (v == (fib n))}fastFib (Int)n   = ((Vec <false, \x10 VV -> ((x9 == 0) || (x9 == (fib x10)))> (Int)), {x13 : (Int) | (x13 == (fib n))})
-> {x2 : (Int) | (x2 == (fib n))}snd (((Vec <false, \x24 VV -> ((x23 == 0) || (x23 == (fib x24)))> (Int)), {x27 : (Int) | (x27 == (fib n))})
 -> {x16 : (Int) | (x16 == (fib n))})
-> ((Vec <false, \x24 VV -> ((x23 == 0) || (x23 == (fib x24)))> (Int)), {x27 : (Int) | (x27 == (fib n))})
-> {x16 : (Int) | (x16 == (fib n))}$ (Vec <True, \x18 VV -> ((x17 == 0) || (x17 == (fib x18)))> (Int))
-> x2:(Int)
-> ((Vec <True, \x8 VV -> ((x7 == 0) || (x7 == (fib x8)))> (Int)), {x11 : (Int) | (x11 == (fib x2))})fibMemo (forall <rng :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool, dom :: (GHC.Types.Int)-> Bool>.
(i:{x15 : (Int)<dom> | true}
 -> {x14 : (Int)<rng i> | ((x14 == 0) || (x14 == (fib n))) && (x14 == 0) && (x14 >= 0)})
-> (Vec <dom, rng> {x14 : (Int) | ((x14 == 0) || (x14 == (fib n))) && (x14 == 0) && (x14 >= 0)})V ((Int) -> {x2 : (Int) | (x2 == (0  :  int))}\_ -> {x2 : (Int) | (x2 == (0  :  int))}0)) {x2 : (Int) | (x2 == n)}n

- `fibMemo` *takes* a table initialized with `0` - `fibMemo` *returns* a table with `fib` values upto `n`.

Memoized Fibonacci ------------------

353: (Vec <True, \k10 VV -> ((VV == 0) || (VV == (fib k10)))> (Int))
-> i:(Int)
-> ((Vec <True, \k10 VV -> ((VV == 0) || (VV == (fib k10)))> (Int)), {VV : (Int) | (VV == (fib i))})fibMemo (Vec <True, \k10 VV -> ((VV == 0) || (VV == (fib k10)))> (Int))t (Int)i 
354:   | {x2 : (Int) | (x2 == i)}i x1:(Int)
-> x2:(Int) -> {x2 : (Bool) | (((Prop x2)) <=> (x1 <= x2))}<= {x2 : (Int) | (x2 == (1  :  int))}1    
355:   = forall a b <p2 :: a-> b-> Bool>.
x1:a
-> x2:{VV : b<p2 x1> | true}
-> {x3 : (a, b)<p2> | ((fst x3) == x1) && ((snd x3) == x2)}({x2 : (Vec <True, \x7 VV -> ((x6 == 0) || (x6 == (fib x7)))> (Int)) | (x2 == t)}t, x1:(Bool)
-> {x8 : (Int) | (x8 == 1) && (x8 > 0) && (x8 >= i)}
-> {x8 : (Int) | ((Prop x1)) && (x8 == 1) && (x8 > 0) && (x8 >= i)}liquidAssume (x1:(Int)
-> {x2 : (Bool) | (((Prop x2)) <=> ((fib x1) == (if (x1 <= 1) then 1 else ((fib (x1 - 1)) + (fib (x1 - 2))))))}axiom_fib {x2 : (Int) | (x2 == i)}i) {x2 : (Int) | (x2 == (1  :  int))}1)
356:   | otherwise 
357:   = case forall <r :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool, d :: (GHC.Types.Int)-> Bool>.
x1:{x7 : (Int)<d> | true}
-> (Vec <d, \x5 VV -> r x5> (Int)) -> {x6 : (Int)<r x1> | true}get {x2 : (Int) | (x2 == i)}i {x2 : (Vec <True, \x7 VV -> ((x6 == 0) || (x6 == (fib x7)))> (Int)) | (x2 == t)}t of   
358:      0 -> let ({VV : (Vec <True, \x1 VV -> ((VV == 0) || (VV == (fib x1)))> (Int)) | (VV == t1)}t1,{VV : (Int) | (VV == n1)}n1) = (Vec <True, \x18 VV -> ((x17 == 0) || (x17 == (fib x18)))> (Int))
-> x2:(Int)
-> ((Vec <True, \x8 VV -> ((x7 == 0) || (x7 == (fib x8)))> (Int)), {x11 : (Int) | (x11 == (fib x2))})fibMemo {x2 : (Vec <True, \x7 VV -> ((x6 == 0) || (x6 == (fib x7)))> (Int)) | (x2 == t)}t  ({x2 : (Int) | (x2 == i)}ix1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}-{x2 : (Int) | (x2 == (1  :  int))}1)
359:               ({VV : (Vec <(VV /= i), \x1 VV -> ((VV == 0) || (VV == (fib x1)))> (Int)) | (VV == t2)}t2,{VV : (Int) | (VV == n2)}n2) = (Vec <True, \x18 VV -> ((x17 == 0) || (x17 == (fib x18)))> (Int))
-> x2:(Int)
-> ((Vec <True, \x8 VV -> ((x7 == 0) || (x7 == (fib x8)))> (Int)), {x11 : (Int) | (x11 == (fib x2))})fibMemo {x3 : (Vec <True, \x8 VV -> ((x7 == 0) || (x7 == (fib x8)))> (Int)) | (x3 == t1) && (x3 == t1)}t1 ({x2 : (Int) | (x2 == i)}ix1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 - x2))}-{x2 : (Int) | (x2 == (2  :  int))}2)
360:               (Int)n       = x1:(Bool) -> (Int) -> {x2 : (Int) | ((Prop x1))}liquidAssume 
361:                         (x1:(Int)
-> {x2 : (Bool) | (((Prop x2)) <=> ((fib x1) == (if (x1 <= 1) then 1 else ((fib (x1 - 1)) + (fib (x1 - 2))))))}axiom_fib {x2 : (Int) | (x2 == i)}i) ({x3 : (Int) | (x3 == n1) && (x3 == n1)}n1x1:(Int) -> x2:(Int) -> {x4 : (Int) | (x4 == (x1 + x2))}+{x3 : (Int) | (x3 == n2) && (x3 == n2)}n2)
362:           in forall a b <p2 :: a-> b-> Bool>.
x1:a
-> x2:{VV : b<p2 x1> | true}
-> {x3 : (a, b)<p2> | ((fst x3) == x1) && ((snd x3) == x2)}(forall <r :: (GHC.Types.Int)-> (GHC.Types.Int)-> Bool, d :: (GHC.Types.Int)-> Bool>.
x1:{x13 : (Int)<d> | true}
-> {x12 : (Int)<r x1> | true}
-> (Vec <d & (x8 /= x1), \x10 VV -> r x10> (Int))
-> (Vec <d, \x4 VV -> r x4> (Int))set {x2 : (Int) | (x2 == i)}i {x2 : (Int) | (x2 == n)}n {x3 : (Vec <(x5 /= i), \x9 VV -> ((x8 == 0) || (x8 == (fib x9)))> (Int)) | (x3 == t2) && (x3 == t2)}t2,  {x2 : (Int) | (x2 == n)}n)
363:      n -> {x2 : ({x7 : (Vec <True, \x12 VV -> ((x11 == 0) || (x11 == (fib x12)))> (Int)) | (x7 == t)}, {x16 : (Int) | (x16 == (fib i)) && (x16 /= 0)})<\_ VV -> (x16 == (fib i)) && (x16 /= 0)> | ((fst x2) == t)}({x2 : (Vec <True, \x7 VV -> ((x6 == 0) || (x6 == (fib x7)))> (Int)) | (x2 == t)}t, {x3 : (Int) | ((x3 == 0) || (x3 == (fib i)))}n)

Memoized Fibonacci ------------------ - `fibMemo` *takes* a table initialized with `0` - `fibMemo` *returns* a table with `fib` values upto `n`.

375: {-@ fibMemo :: FibV 
376:             -> i:Int 
377:             -> (FibV,{v:Int | v = (fib i)}) @-}

Recap ----- Created a `Vec` container Decoupled *domain* and *range* invariants from *data*

Previous, special purpose program analyses - [Gopan-Reps-Sagiv, POPL 05](link) - [J.-McMillan, CAV 07](link) - [Logozzo-Cousot-Cousot, POPL 11](link) - [Dillig-Dillig, POPL 12](link) - ... Encoded as instance of abstract refinement types!