content: Abstract Refinements {#data}
  ============================
  
  Recap
  -----
  
  **So far**
  
  Decouple invariants from *functions*
  
  <br>
  
  <div class="fragment">
  
  **Next**
  
  Decouple invariants from *data structures*
  </div>
  
  Decouple Invariants From Data {#vector}
  =======================================
  
  Example: Vectors
  ----------------
  
  <div class="hidden">
  \begin{code}
  module LiquidArray where
  
  import Language.Haskell.Liquid.Prelude (liquidAssume, liquidError)
  
  {-@ LIQUID "--no-termination" @-}
  
  fibMemo   :: Vec Int -> Int -> (Vec Int, Int)
  fastFib   :: Int -> Int
  idv       :: Int -> Vec Int
  axiom_fib :: Int -> Bool
  axiom_fib = undefined
  
  {-@ predicate AxFib I = (fib I) == (if I <= 1 then 1 else fib(I-1) + fib(I-2)) @-}
  \end{code}
  </div>
  
  <div class="fragment">
  
  Implemented as maps from `Int` to `a`
  
  <br>
  
  \begin{code}
  data Vec a = V (Int -> a)
  \end{code}
  
  </div>
  
  
  Abstract *Domain* and *Range*
  -----------------------------
  
  Parameterize type with *two* abstract refinements:
  
  <br>
  
  \begin{code}
  {-@ data Vec a < dom :: Int -> Prop,
                   rng :: Int -> a -> Prop >
        = V {a :: i:Int<dom> -> a <rng i>}  @-}
  \end{code}
  
  <br>
  
  - `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`
  
  <br>
  
  <div class="fragment">
  
  A quick alias for *segments* between `I` and `J`
  
  <br>
  
  \begin{code}
  {-@ predicate Seg V I J = (I <= V && V < J) @-}
  \end{code}
  
  </div>
  
  Ex: Identity Vectors
  --------------------
  
  Defined between `[0..N)` mapping each key to itself:
  
  <br>
  
  <div class="fragment">
  
  \begin{code}
  {-@ type IdVec N = Vec <{\v -> (Seg v 0 N)},
                          {\k v -> v=k}>
                         Int                  @-}
  \end{code}
  
  </div>
  
  Ex: Identity Vectors
  --------------------
  
  Defined between `[0..N)` mapping each key to itself:
  
  <br>
  
  \begin{code}
  {-@ idv :: n:Nat -> (IdVec n) @-}
  idv n   = V (\k -> if 0 < k && k < n
                       then k
                       else liquidError "eeks")
  \end{code}
  
  <br>
  
  <div class="fragment">
  <a href="https://liquidhaskell.goto.ucsd.edu/index.html#?demo=Array.hs" target="_blank">Demo:</a>Whats the problem? How can we fix it?
  </div>
  
  Ex: Zero-Terminated Vectors
  ---------------------------
  
  Defined between `[0..N)`, with *last* element equal to `0`:
  
  <br>
  
  <div class="fragment">
  
  \begin{code}
  {-@ type ZeroTerm N =
       Vec <{\v -> (Seg v 0 N)},
            {\k v -> (k = N-1 => v = 0)}>
            Int                             @-}
  \end{code}
  
  </div>
  
  
  Ex: Fibonacci Table
  -------------------
  
  A vector whose value at index `k` is either
  
  - `0` (undefined), or,
  
  - `k`th fibonacci number
  
  \begin{code}
  {-@ type FibV =
       Vec <{\v -> true},
            {\k v -> (v = 0 || v = (fib k))}>
            Int                               @-}
  \end{code}
  
  
  Accessing Vectors
  -----------------
  
  Next: lets *abstractly* type `Vec`tor operations, *e.g.*
  
  <br>
  
  - `empty`
  
  - `set`
  
  - `get`
  
  
  Ex: Empty Vectors
  -----------------
  
  `empty` returns Vector whose domain is `false`
  
  <br>
  
  \begin{code}
  {-@ empty :: forall <p :: Int -> a -> Prop>.
                 Vec <{v:Int|false}, p> a     @-}
  
  empty     = V $ \_ -> error "empty vector!"
  \end{code}
  
  <br>
  
  <div class="fragment">
  <a href="https://liquidhaskell.goto.ucsd.edu/index.html#?demo=Array.hs" target="_blank">Demo:</a>
  What would happen if we changed `false` to `true`?
  </div>
  
  Ex: `get` Key's Value
  ---------------------
  
  - *Input* `key` in *domain*
  
  - *Output* value in *range* related with `k`
  
  \begin{code}
  {-@ get :: forall a <d :: Int -> Prop,
                       r :: Int -> a -> Prop>.
             key:Int <d>
          -> vec:Vec <d, r> a
          -> a<r key>                        @-}
  
  get k (V f) = f k
  \end{code}
  
  
  Ex: `set` Key's Value
  ---------------------
  
  - <div class="fragment">Input `key` in *domain*</div>
  
  - <div class="fragment">Input `val` in *range* related with `key`</div>
  
  - <div class="fragment">Input `vec` defined at *domain except at* `key`</div>
  
  - <div class="fragment">Output domain *includes* `key`</div>
  
  Ex: `set` Key's Value
  ---------------------
  
  \begin{code}
  {-@ set :: forall a <d :: Int -> Prop,
                       r :: Int -> a -> Prop>.
             key: Int<d> -> val: a<r key>
          -> vec: Vec<{v:Int<d>| v /= key},r> a
          -> Vec <d, r> a                     @-}
  set key val (V f) = V $ \k -> if k == key
                                  then val
                                  else f key
  \end{code}
  
  <br>
  
  <div class="fragment">
  <a href="https://liquidhaskell.goto.ucsd.edu/index.html#?demo=Array.hs" target="_blank">Demo:</a>
  Help! Can you spot and fix the errors?
  </div>
  
  <!-- INSERT tests/pos/vecloop.lhs here AFTER FIXED -->
  
  Using the Vector API
  --------------------
  
  Memoized Fibonacci
  ------------------
  
  Use `Vec` API to write a *memoized* fibonacci function
  
  <br>
  
  <div class="fragment">
  \begin{code} Using the fibonacci table:
  type FibV =
       Vec <{\v -> true},
            {\k v -> (v = 0 || v = (fib k))}>
            Int
  \end{code}
  </div>
  
  <br>
  
  <div class="fragment">
  But wait, what is `fib` ?
  </div>
  
  
  Specifying Fibonacci
  --------------------
  
  `fib` is *uninterpreted* in the refinement logic
  
  <br>
  
  \begin{code}
  {-@ measure fib :: Int -> Int @-}
  \end{code}
  
  <br>
  
  Specifying Fibonacci
  --------------------
  
  We *axiomatize* the definition of `fib` in SMT ...
  
  \begin{code}<br>
  predicate AxFib I =
    (fib I) == if I <= 1
                 then 1
                 else fib(I-1) + fib(I-2)
  \end{code}
  
  Specifying Fibonacci
  --------------------
  
  Finally, lift axiom into LiquidHaskell as *ghost function*
  
  <br>
  
  \begin{code}
  {-@ axiom_fib ::
        i:_ -> {v:_|((Prop v) <=> (AxFib i))} @-}
  \end{code}
  
  <br>
  
  <div class="fragment">
  **Note:** Recipe for *escaping* SMT limitations
  
  1. *Prove* fact externally
  2. *Use* as ghost function call
  </div>
  
  
  Fast Fibonacci
  --------------
  
  An efficient fibonacci function
  
  <br>
  
  \begin{code}
  {-@ fastFib :: n:Int -> {v:_ | v = (fib n)} @-}
  fastFib n   = snd $ fibMemo (V (\_ -> 0)) n
  \end{code}
  
  <br>
  
  <div class="fragment">
  - `fibMemo` *takes* a table initialized with `0`
  
  - `fibMemo` *returns* a table with `fib` values upto `n`.
  </div>
  
  
  Memoized Fibonacci
  ------------------
  
  \begin{code}
  fibMemo t i
    | i <= 1
    = (t, liquidAssume (axiom_fib i) 1)
    | otherwise
    = case get i t of
       0 -> let (t1,n1) = fibMemo t  (i-1)
                (t2,n2) = fibMemo t1 (i-2)
                n       = liquidAssume
                          (axiom_fib i) (n1+n2)
            in (set i n t2,  n)
       n -> (t, n)
  \end{code}
  
  Memoized Fibonacci
  ------------------
  
  - `fibMemo` *takes* a table initialized with `0`
  - `fibMemo` *returns* a table with `fib` values upto `n`.
  
  <br>
  
  \begin{code}
  {-@ fibMemo :: FibV
              -> i:Int
              -> (FibV,{v:Int | v = (fib i)}) @-}
  \end{code}
  
  
  Recap
  -----
  
  Created a `Vec` container
  
  Decoupled *domain* and *range* invariants from *data*
  
  <br>
  
  <div class="fragment">
  
  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!
  </div>
  