Abstract Refinements

7: module AbstractRefinements where

Abstract Refinements

17: maxInt     :: Int -> Int -> Int 
18: maxInt x y = if x <= y then y else x 

24: maxInt :: Nat -> Nat -> Nat
25: 
26: maxInt :: Even -> Even -> Even
27: 
28: maxInt :: Prime -> Prime -> Prime

But which is the right type?

Parametric Invariants

maxInt returns one of its two inputs x and y.

• If both inputs satisfy a property

• Then output must satisfy that property

This holds, regardless of what that property was!

• That is, we can abstract over refinements

• Or, parameterize a type over its refinements.

Parametric Invariants

53: {-@ maxInt :: forall <p :: Int -> Prop>. Int<p> -> Int<p> -> Int<p> @-}
54: maxInt     :: Int -> Int -> Int 
55: forall <p :: (GHC.Types.Int)-> Bool>.
{VV : (GHC.Types.Int)<p> | true}
-> {VV : (GHC.Types.Int)<p> | true}
-> {VV : (GHC.Types.Int)<p> | true}maxInt {VV : (GHC.Types.Int) | ((papp1 p VV))}x {VV : (GHC.Types.Int) | ((papp1 p VV))}y = if {VV : (GHC.Types.Int) | ((papp1 p VV)) && (VV == x)}x x:{VV : (GHC.Types.Int) | ((papp1 p VV))}
-> y:{VV : (GHC.Types.Int) | ((papp1 p VV))}
-> {VV : (GHC.Types.Bool) | (((Prop VV)) <=> (x <= y))}<= {VV : (GHC.Types.Int) | ((papp1 p VV)) && (VV == y)}y then {VV : (GHC.Types.Int) | ((papp1 p VV)) && (VV == y)}y else {VV : (GHC.Types.Int) | ((papp1 p VV)) && (VV == x)}x 

Where

• Int<p> is just an abbreviation for {v:Int | (p v)}

This type states explicitly:

• For any property p, that is a property of Int,

• maxInt takes two inputs of which satisfy p,

• maxInt returns an output that satisfies p.

Parametric Invariants via Abstract Refinements

78: maxInt :: forall <p :: Int -> Prop>. Int<p> -> Int<p> -> Int<p> 

We call p an an abstract refinement

In the refinement logic,

• abstract refinements are uninterpreted function symbols

• which (only) satisfy the congruence axiom: forall x, y. x = y => (p x) = (p y)

Using Abstract Refinements

• If we call maxInt with two Ints with the same concrete refinement,

• Then the p will be instantiated with that concrete refinement,

• The output of the call will also enjoy the concrete refinement.

For example, the refinement is instantiated with \v -> v >= 0

104: {-@ maxNat :: Nat @-}
105: maxNat     :: Int
106: {VV : (GHC.Types.Int) | (VV >= 0)}maxNat     = forall <p :: (GHC.Types.Int)-> Bool>.
{VV : (GHC.Types.Int)<p> | true}
-> {VV : (GHC.Types.Int)<p> | true}
-> {VV : (GHC.Types.Int)<p> | true}maxInt {VV : (GHC.Types.Int) | (VV == (2  :  int))}2 {VV : (GHC.Types.Int) | (VV == (5  :  int))}5

Using Abstract Refinements

• If we call maxInt with two Ints with the same concrete refinement,

• Then the p will be instantiated with that concrete refinement,

• The output of the call will also enjoy the concrete refinement.

Or any other property

121: {-@ type RGB = {v: Int | ((0 <= v) && (v < 256)) } @-}

to verify

127: {-@ maxRGB :: RGB @-}
128: maxRGB     :: Int
129: {VV : (GHC.Types.Int) | (VV < 256) && (0 <= VV)}maxRGB     = forall <p :: (GHC.Types.Int)-> Bool>.
{VV : (GHC.Types.Int)<p> | true}
-> {VV : (GHC.Types.Int)<p> | true}
-> {VV : (GHC.Types.Int)<p> | true}maxInt {VV : (GHC.Types.Int) | (VV == (56  :  int))}56 {VV : (GHC.Types.Int) | (VV == (8  :  int))}8