Abstract Refinements

Abstract Refinements

Two Problems



Problem 1:

How do we specify both increasing and decreasing lists?


Problem 2:

How do we specify iteration-dependence in higher-order functions?

Problem Is Pervasive

Lets distill it to a simple example...


(First, a few aliases)


67: {-@ type Odd  = {v:Int | (v mod 2) = 1} @-}
68: {-@ type Even = {v:Int | (v mod 2) = 0} @-}

Example: maxInt

Compute the larger of two Ints:


80: maxInt     :: Int -> Int -> Int 
81: maxInt x y = if y <= x then x else y

Example: maxInt

Has many incomparable refinement types


92: maxInt :: Nat  -> Nat  -> Nat
93: maxInt :: Even -> Even -> Even
94: maxInt :: Odd  -> Odd  -> Odd


Oh no! Which one should we use?

Refinement Polymorphism

maxInt returns one of its two inputs x and y


If : the inputs satisfy a property
Then : the output satisfies that property


Above holds for all properties!


Need to abstract properties over types

Parametric Refinements

Enable quantification over refinements ...


222: {-@ maxInt :: forall <p :: Int -> Prop>. 
223:                 Int<p> -> Int<p> -> Int<p>  @-}
224: 
225: forall <p :: GHC.Types.Int-> Bool>.
{VV : Int<p> | true}
-> {VV : Int<p> | true} -> {VV : Int<p> | true}maxInt {VV : Int | ((papp1 p VV))}x {VV : Int | ((papp1 p VV))}y = if {x3 : Int | ((papp1 p x3)) && (x3 == x)}x x1:Int -> x2:Int -> {x2 : Bool | (((Prop x2)) <=> (x1 <= x2))}<= {x3 : Int | ((papp1 p x3)) && (x3 == y)}y then {x3 : Int | ((papp1 p x3)) && (x3 == y)}y else {x3 : Int | ((papp1 p x3)) && (x3 == x)}x


Type says: for any p that is a property of Int,
  • max takes two Ints that satisfy p,
  • max returns an Int that satisfies p.

Parametric Refinements

Enable quantification over refinements ...


245: {-@ maxInt :: forall <p :: Int -> Prop>. 
246:                 Int<p> -> Int<p> -> Int<p>  @-}
247: 
248: maxInt x y = if x <= y then y else x


Key idea:   Int<p>   is just   {v:Int | (p v)}


i.e., Abstract Refinement is an uninterpreted function in SMT logic

Parametric Refinements


263: {-@ maxInt :: forall <p :: Int -> Prop>. 
264:                 Int<p> -> Int<p> -> Int<p>  @-}
265: 
266: maxInt x y = if x <= y then y else x


Check and Instantiate

Using SMT and Abstract Interpretation.

Using Abstract Refinements

  • When we call maxInt with args with some refinement,
  • Then p instantiated with same refinement,
  • Result of call will also have same concrete refinement. 
288: {-@ o' :: Odd  @-}
289: {v : Int | ((v mod 2) == 1)}o' = forall <p :: GHC.Types.Int-> Bool>.
{x3 : Int<p> | true}
-> {x2 : Int<p> | true} -> {x1 : Int<p> | true}maxInt {x2 : Int | (x2 == (3  :  int))}3 {x2 : Int | (x2 == (7  :  int))}7     -- p := \v -> Odd v 
290: 
291: {-@ e' :: Even @-}
292: {v : Int | ((v mod 2) == 0)}e' = forall <p :: GHC.Types.Int-> Bool>.
{x3 : Int<p> | true}
-> {x2 : Int<p> | true} -> {x1 : Int<p> | true}maxInt {x2 : Int | (x2 == (2  :  int))}2 {x2 : Int | (x2 == (8  :  int))}8     -- p := \v -> Even v

Using Abstract Refinements

Or any other property ...


307: {-@ type RGB = {v:_ | (0 <= v && v < 256)} @-}
308: 
309: {-@ rgb :: RGB @-}
310: {v : Int | (v < 256) && (0 <= v)}rgb = forall <p :: GHC.Types.Int-> Bool>.
{x3 : Int<p> | true}
-> {x2 : Int<p> | true} -> {x1 : Int<p> | true}maxInt {x2 : Int | (x2 == (56  :  int))}56 {x2 : Int | (x2 == (8  :  int))}8   -- p := \v -> 0 <= v < 256

Recap

  1. Refinements: Types + Predicates
  2. Subtyping: SMT Implication
  3. Measures: Strengthened Constructors
  4. Abstract Refinements over Types



Abstract Refinements are very expressive ... [continue]