Refinement Reflection


Reflect function definition into its result refined type.


module RefinementRelfection where {-@ LIQUID "--higherorder" @-} import Language.Haskell.Liquid.ProofCombinators


Refinement Types

Types + Logical Predicates

{-@ type Nat = {v : Int | 0 <= v} @-}

Used for Specification

{-@ nats :: [Nat] @-} nats = [0, 1, 2]

Specification & Termination & Verification

We user refinement types for specification & termination

{-@ fib :: Nat -> Nat @-} fib i | i <= 1 = i fib i = fib (i-1) + fib (i-2)

Propositions

Propositions are refined unit types

  type Proof = ()

with SMT-automated proofs

{-@ plus_2_2 :: () -> {v:Proof | 2 + 2 = 4 } @-} plus_2_2 _ = ()

Universal & Existential Propositions

Function arguments for universals
{-@ plusComm :: x:Int -> y:Int -> {v:Proof | x + y = y + x } @-} plusComm _ _ = ()


Dependent Pairs for existentials
{-@ intUp :: n:Int -> (m::Int, {v:Proof | n < m}) @-} intUp n = (n+1, ())

Refinement Reflection


How do we talk about user defined functions e.g., fib?


{-@ reflect fib @-}

Step 1: Definition

In the logic, fib is an uninterpreted function

{-@ fibCongr :: x:Nat -> y:Nat -> {x == y => fib x == fib y} @-} fibCongr _ _ = ()

Step 2: Reflection

The Haskell definition of fib is reflected into the type

  fib :: i:Nat -> { v:Nat | v = fib i && fibP i }
where 
  fibP i = if i <= 1 then fib i = i 
           else fib i = fib (i-1) + fib (i-2)

Step 3: Application


To prove that fib 2 == 1 we call fib on 0, 1, and 2.

{-@ pf_fib2 :: { v:_ | fib 2 = 1 } @-} pf_fib2 = let { t0 = fib 0; t1 = fib 1; t2 = fib 2 } in (t0,t1,t2)


This does not look good ...

Proof structure is not important ...

... as long as it has proper applications.

{-@ pf_fib2' :: () -> {v:[Nat] | fib 2 = 1 } @-} pf_fib2' _ = [ fib 0 , fib 1 , fib 2 ]


Still does not look good ...

Equational Proofs

ProofCombinators library to structure proof terms.

data QED = QED 

(***) :: a -> QED -> Proof 
_ *** QED = () 

(==.) :: x:a -> a -> {v:a | v == x }

Equational Proofs in Practice

We rewrite the fib2 proof using ProofCombinators.

{-@ fib2_1 :: () -> { fib 2 = 1 } @-} fib2_1 _ = fib 2 ==. fib 1 + fib 0 ==. 1 *** QED


Finally, looks like a proof!

“Because” Combinators

We extend (==.) to take an optional proof argument and ...

... define a dollar like (?) combinator.

{-@ fib3_2 :: () -> { fib 3 = 2 } @-} fib3_2 _ = fib 3 ==. fib 2 + fib 1 ==. 2 ? fib2_1 () *** QED

Arithmetic and Ordering

Similarly, we use arithmetic proof combinators for arithmetic proofs.

{-@ fibUp :: n:Nat -> {fib n <= fib (n + 1)} @-} fibUp 0 = fib 0 <. fib 1 *** QED fibUp 1 = fib 1 <=. fib 1 + fib 0 ==. fib 2 *** QED fibUp n = fib n <=. fib n + fib (n-1) ==. fib (n+1) *** QED

Induction

Since fib increases locally, it is also monotonic.
{-@ fibMono :: x:Nat -> y:{Nat | x < y} -> {fib x <= fib y} / [y] @-} fibMono x y | x+1 == y = fib x <=. fib (x+1) ? fibUp x <=. fib y *** QED | x+1 < y = fib x <=. fib (y-1) ? fibMono x (y-1) <=. fib y ? fibUp (y-1) *** QED

Higher Order Reasoning

Every function that increases locally, is also monotonic.
{-@ fMono :: f:(Nat -> Int) -> (n:Nat -> {f n <= f (n + 1)}) -> x:Nat -> y:{Nat | x < y} -> {f x <= f y} / [y] @-} fMono f up x y | x+1 == y = f x <=. f (x+1) ? up x <=. f y *** QED | x+1 < y = f x <=. f (y-1) ? fMono f up x (y-1) <=. f y ? up (y-1) *** QED

Instantiation of Higher Order Theorems

We get back monotonicity of fib ...

... by application of the general fMono theorem.

{-@ fibMono' :: n:Nat -> m:{Nat | n < m } -> { fib n <= fib m } @-} fibMono' = fMono fib fibUp

What about automation?


Observation: Since all reflected functions are terminating, ...

... their unfoldings are also termining,

... so unfolding can be predictably automated.

Proof by Logical Evaluation (PLE)

  • In theory: Repeatedly unfold each function that statically unfolds.

  • In practise:

{-@ LIQUID "--automatic-instances=liquidinstanceslocal" @-} {- automatic-instances fib3_2_PLE @-} {- fib3_2_PLE :: () -> { fib 3 = 2 } @-} fib3_2_PLE _ = ()

Summary:


  • Refinement Reflection and Proof by Logical Evaluation combined ...

  • ... allow for complete verification with SMT-automation!


Haskell Sigs

fib3_2_PLE :: () -> Proof nats :: [Int] fib :: Int -> Int fibCongr :: Int -> Int -> Proof plus_2_2 :: () -> Proof pf_fib2 :: (Int,Int,Int) pf_fib2' :: () -> [Int] fib2_1 :: () -> Proof intUp :: Int -> (Int, Proof) plusComm :: Int -> Int -> Proof fib3_2 :: () -> Proof fibUp :: Int -> Proof fMono :: (Int -> Int) -> (Int -> Proof) -> Int -> Int -> Proof fibMono' :: Int -> Int -> Proof fibMono :: Int -> Int -> Proof