Abstract Refinements

A Tricky Problem

Problem Is Pervasive

Lets distill it to a simple example...

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

Example: maxInt

Compute the larger of two Ints:

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

Example: maxInt

Has many incomparable refinement types/summaries

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

Refinement Polymorphism

maxInt returns one of its two inputs x and y

Parametric Refinements

Enable quantification over refinements ...

144: {-@ maxInt :: forall <p :: Int -> Prop>. 
145:                 Int<p> -> Int<p> -> Int<p>  @-}
146: 
147: forall <p :: GHC.Types.Int -> Prop>.
{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 {v : Int | papp1 p v && v == x}x x1:Int -> x2:Int -> {v : Bool | Prop v <=> x1 <= v}<= {v : Int | papp1 p v && v == y}y then {v : Int | papp1 p v && v == y}y else {v : Int | papp1 p v && v == x}x 

• max takes two Ints that satisfy p,
• max returns an Int that satisfies p.

Parametric Refinements

Enable quantification over refinements ...

167: {-@ maxInt :: forall <p :: Int -> Prop>. 
168:                 Int<p> -> Int<p> -> Int<p>  @-}
169: 
170: maxInt x y = if x <= y then y else x 

Parametric Refinements

186: {-@ maxInt :: forall <p :: Int -> Prop>. 
187:                 Int<p> -> Int<p> -> Int<p>  @-}
188: 
189: maxInt x y = if x <= y then y else x 

Check Implementation via SMT

Parametric Refinements

200: {-@ maxInt :: forall <p :: Int -> Prop>. 
201:                 Int<p> -> Int<p> -> Int<p>  @-}
202: 
203: maxInt x y = if x <= y then y else x 

Check Implementation via SMT

\[\begin{array}{rll} \ereft{x}{\Int}{p(x)},\ereft{y}{\Int}{p(y)} & \vdash \reftx{v}{v = y} & \subty \reftx{v}{p(v)} \\ \ereft{x}{\Int}{p(x)},\ereft{y}{\Int}{p(y)} & \vdash \reftx{v}{v = x} & \subty \reftx{v}{p(v)} \\ \end{array}\]

Parametric Refinements

221: {-@ maxInt :: forall <p :: Int -> Prop>. 
222:                 Int<p> -> Int<p> -> Int<p>  @-}
223: 
224: maxInt x y = if x <= y then y else x 

Check Implementation via SMT

\[\begin{array}{rll} {p(x)} \wedge {p(y)} & \Rightarrow {v = y} & \Rightarrow {p(v)} \\ {p(x)} \wedge {p(y)} & \Rightarrow {v = x} & \Rightarrow {p(v)} \\ \end{array}\]

Using Abstract Refinements

• If we call maxInt with args satisfying common property,
• Then p instantiated property, result gets same property.

250: {-@ xo :: Odd  @-}
251: {v : Int | v mod 2 == 1}xo = {v : Int | v mod 2 == 1 && v > 0}
-> {v : Int | v mod 2 == 1 && v > 0}
-> {v : Int | v mod 2 == 1 && v > 0}maxInt {v : Int | v == (3  :  int)}3 {v : Int | v == (7  :  int)}7     -- p := \v -> Odd v 
252: 
253: {-@ xe :: Even @-}
254: {v : Int | v mod 2 == 0}xe = {v : Int | v mod 2 == 0 && v /= AbstractRefinements.xo && v > 0}
-> {v : Int | v mod 2 == 0 && v /= AbstractRefinements.xo && v > 0}
-> {v : Int | v mod 2 == 0 && v /= AbstractRefinements.xo && v > 0}maxInt {v : Int | v == (2  :  int)}2 {v : Int | v == (8  :  int)}8     -- p := \v -> Even v 

Recap

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