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

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!