Abstract Refinements

Recap

So far

Decouple invariants from functions


Next

Decouple invariants from data structures

Decouple Invariants From Data

Example: Vectors

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 Vectors 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: x1:{v : Int | (v >= 0)}
-> (Vec <(VV < x1) && (0 <= VV), \k4 VV -> (VV == k4)> Int)idv {v : Int | (v >= 0)}n   = forall <rng :: GHC.Types.Int-> GHC.Types.Int-> Bool, dom :: GHC.Types.Int-> Bool>.
x1:(x2:{x13 : Int<dom> | true}
    -> {x12 : Int<rng x2> | (x12 > 0) && (x12 >= 0) && (x12 < n)})
-> {x2 : (Vec <dom, rng> {x12 : Int | (x12 > 0) && (x12 >= 0) && (x12 < n)}) | ((a x2) == x1)}V (\{VV : Int | (VV >= 0) && (VV < n)}k -> if {x2 : Int | (x2 == (0  :  int))}0 x1:Int -> x2:Int -> {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:Int -> x2:Int -> {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 {x2 : [Char] | ((len x2) >= 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,

  • kth 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 Vector 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     = x1:({x4 : Int | false} -> {VV : a | false})
-> {x2 : (Vec <false, \_ VV -> false> {VV : a | false}) | ((a x2) == x1)}V (({x8 : Int | false} -> {VV : a | false})
 -> (Vec <false, \_ VV -> false> a))
-> ({x8 : Int | false} -> {VV : a | false})
-> (Vec <false, \_ VV -> false> a)$ {x1 : Int | false} -> {VV : a | false}\_ -> [Char] -> {VV : a | false}error {x2 : [Char] | ((len x2) >= 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>.
x1:{VV : Int<d> | true}
-> (Vec <d, \_ VV -> r> a) -> {VV : a<r x1> | 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>.
x1:{VV : Int<d> | true}
-> {VV : a<r x1> | true}
-> (Vec <d & (VV /= x1), \_ VV -> r> a)
-> (Vec <d, \_ VV -> r> a)set {VV : Int | ((papp1 d VV))}key {VV : a | ((papp2 r VV key))}val (V f) = x1:({x6 : Int | ((papp1 d x6))} -> {VV : a | ((papp2 r VV key))})
-> {x2 : (Vec <((papp1 d x4)), \_ VV -> ((papp2 r VV key))> {VV : a | ((papp2 r VV key))}) | ((a x2) == x1)}V (({x12 : Int | ((papp1 d x12))} -> {VV : a | ((papp2 r VV key))})
 -> (Vec <((papp1 d x9)), \_ VV -> ((papp2 r VV key))> a))
-> ({x12 : Int | ((papp1 d x12))} -> {VV : a | ((papp2 r VV key))})
-> (Vec <((papp1 d x9)), \_ VV -> ((papp2 r VV key))> a)$ \{VV : Int | ((papp1 d VV))}k -> if {x3 : Int | ((papp1 d x3)) && (x3 == k)}k x1:Int -> x2:Int -> {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: x1:Int -> {v : Int | (v == (fib x1))}fastFib Intn   = ((Vec Int), {x10 : Int | (x10 == (fib n))})
-> {x2 : Int | (x2 == (fib n))}snd (((Vec Int), {x20 : Int | (x20 == (fib n))})
 -> {x12 : Int | (x12 == (fib n))})
-> ((Vec Int), {x20 : Int | (x20 == (fib n))})
-> {x12 : Int | (x12 == (fib n))}$ (Vec <True, \k10 VV -> ((VV == 0) || (VV == (fib k10)))> Int)
-> x2:Int
-> ((Vec <True, \k10 VV -> ((VV == 0) || (VV == (fib k10)))> Int), {v : Int | (v == (fib x2))})fibMemo (forall <rng :: GHC.Types.Int-> GHC.Types.Int-> Bool, dom :: GHC.Types.Int-> Bool>.
x1:(x2:{x15 : Int<dom> | true}
    -> {x14 : Int<rng x2> | ((x14 == 0) || (x14 == (fib n))) && (x14 == 0) && (x14 >= 0)})
-> {x2 : (Vec <dom, rng> {x14 : Int | ((x14 == 0) || (x14 == (fib n))) && (x14 == 0) && (x14 >= 0)}) | ((a x2) == x1)}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)
-> x2:Int
-> ((Vec <True, \k10 VV -> ((VV == 0) || (VV == (fib k10)))> Int), {v : Int | (v == (fib x2))})fibMemo (Vec <True, \k10 VV -> ((VV == 0) || (VV == (fib k10)))> Int)t Inti 
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, \k10 VV -> ((VV == 0) || (VV == (fib k10)))> Int)
-> x2:Int
-> ((Vec <True, \k10 VV -> ((VV == 0) || (VV == (fib k10)))> Int), {v : Int | (v == (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 <True, \x1 VV -> ((VV == 0) || (VV == (fib x1)))> Int) | (VV == t2)}t2,{VV : Int | (VV == n2)}n2) = (Vec <True, \k10 VV -> ((VV == 0) || (VV == (fib k10)))> Int)
-> x2:Int
-> ((Vec <True, \k10 VV -> ((VV == 0) || (VV == (fib k10)))> Int), {v : Int | (v == (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:               Intn       = 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:{x19 : Int<d> | true}
-> {x18 : Int<r x1> | (x18 == n) && (x18 == (fib i))}
-> (Vec <d & (x10 /= x1), \x12 VV -> r x12> {x18 : Int | (x18 == n) && (x18 == (fib i))})
-> (Vec <d, \x4 VV -> r x4> {x18 : Int | (x18 == n) && (x18 == (fib i))})set {x2 : Int | (x2 == i)}i {x2 : Int | (x2 == n)}n {x3 : (Vec <True, \x8 VV -> ((x7 == 0) || (x7 == (fib x8)))> 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

Encoded as instance of abstract refinement types!