Refinement Reflection



Allow terminating Haskell functions in refinements!

Theorems about Haskell functions


e.g. Parallelized Function Equivalent to Original


forall xs. sum xs == parallelSum xs

Theorems about Haskell functions




Can we express the above theorems in Liquid Haskell?

Express & Prove Theorems in Haskell ...

... for Haskell functions.

Types As Theorems

Refined Types are theorems

and

Haskell Functions are proofs.

{-@ onePlusOne :: () -> {v:() | 1 + 1 == 2 } @-} onePlusOne _ = ()

Make the theorems pretty!


ProofCombinators comes with Liquid Haskell and allows for pretty proofs!


-- import Language.Haskell.Liquid.ProofCombinators {-@ propOnePlusOne :: () -> {v: Proof | 1 + 1 == 2} @-} propOnePlusOne _ = trivial

Make the theorems even prettier!


ProofCombinators comes with Liquid Haskell and allows for pretty proofs!


{-@ propOnePlusOne' :: _ -> { 1 + 1 == 2 } @-} propOnePlusOne' _ = trivial *** QED

Use more SMT knowledge


ProofCombinators comes with Liquid Haskell and allows for pretty proofs!


{-@ propPlusAccum :: x:Int -> y:Int -> { x + y == y + x } @-} propPlusAccum _ _ = trivial *** QED

Theorems about Haskell functions




Can we express the above theorems in Liquid Haskell?

Express & Prove Theorems in Haskell ...

... for Haskell functions.

Refinement Reflection

Reflect fib in the logic.

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


(Need to prove fib terminates...)

fib is an uninterpreted function


For which logic only knows the congruence axiom...

{-@ fibCongr :: i:Nat -> j:Nat -> {i == j => fib i == fib j} @-} fibCongr _ _ = trivial


... and nothing else


{-@ fibOne :: () -> {fib 1 == 1 } @-} fibOne _ = trivial

Reflect Function into Output Type


The type of fib connects logic & Haskell implementation 

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


Calling fib i reveals its implementation in the logic!

Reflection at Result Type


{-@ fibEq :: () -> {fib 1 == 1 } @-} fibEq _ = let f1 = fib 1 -- f1:: {f1 == fib 1 && f1 == 1} in [f1] *** QED


Exercise: Lets prove that fib 2 == 1.

Structuring Proofs



Using combinators from ProofCombinators!



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

Reusing Proofs: The "because" operator



Using combinators from ProofCombinators!



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

Paper & Pencil style Proofs


fib is increasing

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

Another "Paper & Pencil" Proof


Exercise: Lets fix the proof that fib is monotonic?

{-@ fibMonotonic :: x:Nat -> y:{Nat | x < y } -> {fib x <= fib y} @-} fibMonotonic x y | y == x + 1 = fib x <=. fib (x+1) ? fibUp x <=. fib y *** QED | x < y - 1 = fib x <=. fib (y-1) ? trivial {- Inductive Hypothesis call goes here -} <=. fib y ? fibUp (y-1) *** QED

Exercise: Can you replace trivial to fix the monotonicity proof?

Note: Totality checker should be on for valid proofs

{-@ LIQUID "--totality" @-}

Generalizing monotonicity proof


Exercise: Generalize the implementation of fMono proof below to any increasing function f.

{-@ fMono :: f:(Nat -> Int) -> fUp:(z:Nat -> {f z <= f (z+1)}) -> x:Nat -> y:{Nat|x < y} -> {f x <= f y} / [y] @-} fMono f fUp x y | y == x + 1 = fib x <=. fib (x+1) ? fibUp x <=. fib y *** QED | x < y - 1 = fib x <=. fib (y-1) ? fibMonotonic x (y-1) <=. fib y ? fibUp (y-1) *** QED

Reusing Theorems by Application


fib is monotonic!


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

Recap


Refinements: Types + Predicates
Specification: Refined Input/Output Types
Verification: SMT-based Predicate Subtyping
Measures: Specify Properties of Data
Termination: Well-founded Metrics
Reflection: Haskell functions in Logic


Next: Structural Induction: Program Properties about data types!