content: ---
  layout: post
  title: "Refinement Reflection: Haskell as a theorem prover"
  date: 2016-09-18
  comments: true
  external-url:
  author: Niki Vazou
  published: true
  categories: reflection
  demo: RefinementReflection.hs
  ---
  
  We've taught LiquidHaskell a new trick that we call ``Refinement Reflection''
  which lets us turn Haskell into a theorem prover capable of proving arbitrary
  properties of code. The key idea is to **reflect** the code of the function into
  its **output type**, which lets us then reason about the function at the
  (refinement) type level. Lets see how to use refinement types to express a
  theorem, for example that fibonacci is a monotonically increasing function, 
  then write plain Haskell code to reify a paper-and-pencil-style proof 
  for that theorem, that can be machine checked by LiquidHaskell.
  
  <!-- more -->
  
  <br>
  <br>
  <br>
  
  <div class="row-fluid">
    <div class="span12 pagination-centered">
    <img src="https://eyesofodysseus.files.wordpress.com/2013/06/full-moon-over-ocean-reflection.jpg"
         alt="Reflection" width="300">
         <br>
         <br>
         <br>
         The beauty of Liquid Reflection.
         <br>
         <br>
         <br>
    </div>
  </div>
  
  
  <div class="hidden">
  \begin{code}
  {-@ LIQUID "--higherorder"     @-}
  {-@ LIQUID "--totality"        @-}
  module RefinementReflection where
  import Language.Haskell.Liquid.ProofCombinators
  
  fib :: Int -> Int
  propPlusComm :: Int -> Int -> Proof 
  propOnePlueOne :: () -> Proof 
  fibTwo :: () -> Proof 
  fibCongruence :: Int -> Int -> Proof
  fibUp :: Int -> Proof 
  fibTwoPretty :: Proof 
  fibThree :: () -> Proof 
  fMono :: (Int -> Int)
        -> (Int -> Proof)
        -> Int
        -> Int 
        -> Proof 
  fibMono :: Int -> Int -> Proof 
  
  \end{code}
  </div>
  
  Shallow vs. Deep Specifications
  -------------------------------
  
  Up to now, we have been using Liquid Haskell to specify and verify "shallow"
  specifications that abstractly describe the behavior of functions.  For example,
  below, we specify and verify that `fib`restricted to natural numbers, always
  terminates returning a natural number.
  
  \begin{code}
  {-@ fib :: i:Nat -> Nat / [i] @-}
  fib i | i == 0    = 0 
        | i == 1    = 1 
        | otherwise = fib (i-1) + fib (i-2)
  \end{code}
  
  In this post we present how refinement reflection is used to verify 
  "deep" specifications that use the exact definition of Haskell functions. 
  For example, we will prove that the Haskell `fib` function is increasing.
  
  
  
  Propositions
  ------------
  
  To begin, we import [ProofCombinators][proofcomb], a (Liquid) Haskell 
  library that defines and manipulates logical proofs. 
  
  ```haskell
  import Language.Haskell.Liquid.ProofCombinators
  ```
  
  A `Proof` is a data type that carries no run time information
  
  ```haskell
  type Proof = ()
  ```
  
  but can be refined with desired logical propositions.
  For example, the following type states that `1 + 1 == 2`
  
  \begin{code}
  {-@ type OnePlusOne = {v: Proof | 1 + 1 == 2} @-}
  \end{code}
  
  Since the `v` and `Proof` are irrelevant, we may as well abbreviate 
  the above to 
  
  \begin{code}
  {-@ type OnePlusOne' = { 1 + 1 == 2 } @-}
  \end{code}
  
  
  As another example, the following function type declares 
  that _for each_ `x` and `y` the plus operator commutes. 
  
  \begin{code}
  {-@ type PlusComm = x:Int -> y:Int -> {x + y == y + x} @-} 
  \end{code}
  
  
  
  Trivial Proofs
  --------------
  
  We prove the above theorems using Haskell programs. 
  The `ProofCombinators` module defines the `trivial` proof
  
  ```haskell
  trivial :: Proof 
  trivial = ()
  ```
  
  and the "casting" operator `(***)` that makes proof terms look 
  nice:
  
  ```haskell
  data QED = QED
  
  (***) :: a -> QED -> Proof
  _ *** _ = ()
  ```
  
  Using the underlying SMT's knowledge on linear arithmetic, 
  we can trivially prove the above propositions.
  
  \begin{code}
  {-@ propOnePlusOne :: _ -> OnePlusOne @-} 
  propOnePlusOne _ = trivial *** QED 
  
  {-@ propPlusComm :: PlusComm @-} 
  propPlusComm _ _ = trivial *** QED 
  \end{code}
  
  
  We saw how we use SMT's knowledge on linear arithmetic 
  to trivially prove arithmetic properties. But how can 
  we prove ``deep'' properties on Haskell's functions?
  
  
  Refinement Reflection 
  ---------------------
  
  Refinement Reflection allows deep specification and 
  verification by reflecting the code implementing a Haskell
  function into the function’s output refinement type.
  
  Refinement Reflection proceeds in 3 steps: definition, reflection, and application.
  Consider reflecting the definition of `fib` into the logic
  
  \begin{code}
  {-@ reflect fib @-}
  \end{code}
  
  then the following three reflection steps will occur. 
  
  Step 1: Definition 
  ------------------
  
  Reflection of the Haskell function `fib` defines in logic 
  an _uninterpreted_ function `fib` that satisfies the congruence axiom.
  
  In the logic the function `fib` is defined.
  
  ```haskell
  fib :: Int -> Int 
  ```
  
  SMT only knows that `fib` satisfies the congruence axiom.
  
  \begin{code}
  {-@ fibCongruence :: i:Nat -> j:Nat -> {i == j => fib i == fib j} @-}
  fibCongruence _ _ = trivial *** QED 
  \end{code}
  
  Other than congruence, SMT knowns nothing for the function `fib`,
  until reflection happens!
  
  
  Step 2: Reflection
  ------------------
  
  As a second step, Liquid Haskell connects the Haskell function `fib`
  with the homonymous logical function, 
  by reflecting the implementation of `fib` in its result type. 
  
  
  The result type of `fib` is automatically strengthened to the following.
  
  ```haskell
  fib :: i:Nat -> {v:Nat | v == fib i && v = fibP i }
  ```
  
  That is, the result satisfies the `fibP` predicate
  exactly reflecting the implementation of `fib`.
  
  ```haskell
  fibP i = if i == 0 then 0 else
           if i == 1 then 1 else
           fib (i-1) + fib (i-2)
  ```
  
  Step 3: Application 
  -------------------
  
  With the reflected refinement type,
  each application of `fib` automatically unfolds the definition of `fib` 
  once. 
  As an example, applying `fib` to `0`, `1`, and `2` allows us to prove that `fib 2 == 1`:
  
  \begin{code}
  {-@ fibTwo :: _ -> { fib 2 == 1 } @-}
  fibTwo _ = [fib 0, fib 1, fib 2] *** QED
  \end{code}
  
  Though valid, the above `fibTwo` proof is not pretty! 
  
  
  Structuring Proofs 
  ------------------
  
  To make our proofs look nice, we use combinators from 
  the `ProofCombinators` library, which exports a family 
  of operators `(*.)` where `*` comes from the theory of 
  linear arithmetic and the refinement type of `x *. y` 
  
  + **requires** that `x *. y` holds and 
  + **ensures** that the returned value is equal to `x`.
  
  For example, `(==.)` and `(<=.)` are predefined in `ProofCombinators` as
  
  ```haskell
  (==.) :: x:a -> y:{a| x==y} -> {v:a| v==x}
  x ==. _ = x
  
  (<=.) :: x:a -> y:{a| x<=y} -> {v:a| v==x}
  x <=. _ = x
  ```
  
  Using these predefined operators, we construct paper and pencil-like proofs 
  for the `fib` function.
  
  \begin{code}
  {-@ fibTwoPretty :: { fib 2 == 1 } @-}
  fibTwoPretty 
    =   fib 2 
    ==. fib 1 + fib 0 
    *** QED
  \end{code}
  
  
  
  Because operator 
  -----------------
  
  To allow the reuse of existing proofs, `ProofCombinators` defines the because 
  operator `(∵)`
  
  ```haskell
  (∵) :: (Proof -> a) -> Proof -> a
  f ∵ y = f y
  ```
  
  For example, `fib 3 == 2` holds because `fib 2 == 1`:
  
  \begin{code}
  {-@ fibThree :: _ -> { fib 3 == 2 } @-}
  fibThree _ 
    =   fib 3 
    ==. fib 2 + fib 1
    ==. 1     + 1      ∵ fibTwoPretty
    ==. 2 
    *** QED
  \end{code}
  
  
  
  Proofs by Induction (i.e. Recursion) 
  ------------------------------------
  
  Next, combining the above operators we specify and prove that 
  `fib` is increasing, that is for each natural number `i`, 
  `fib i <= fib (i+1)`. 
  
  We specify the theorem as a refinement type for `fibUp`
  and use Haskell code to persuade Liquid Haskell that 
  the theorem holds. 
  
  \begin{code}
  {-@ 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
  \end{code}
  
  The proof proceeds _by induction on_ `i`. 
  
  + The base cases `i == 0` and `i == 1` are represented 
    as Haskell's case splitting. 
  
  + The inductive hypothesis is represented by recursive calls 
    on smaller inputs. 
  
  Finally, the SMT solves arithmetic reasoning to conclude the proof.  
  
  Higher Order Theorems
  ----------------------
  
  Refinement Reflection can be used to express and verify higher order theorems!
  For example, `fMono` specifies that each locally increasing function is monotonic! 
  
  \begin{code}
  {-@ 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 thm x y  
    | x + 1 == y
    = f y ==. f (x + 1)
           >. f x       ∵ thm x
          *** QED
  
    | x + 1 < y
    = f x
    <.  f (y-1)         ∵ fMono f thm x (y-1)
    <.  f y             ∵ thm (y-1)
    *** QED
  \end{code}
  
  Again, the recursive implementation of `fMono` depicts the paper and pencil 
  proof of `fMono` by induction on the decreasing argument `/ [y]`. 
  
  Since `fib` is proven to be locally increasing by `fUp`, we use `fMono` 
  to prove that `fib` is monotonic. 
  
  \begin{code}
  {-@ fibMono :: n:Nat -> m:{Nat | n < m }  -> {fib n <= fib m} @-}
  fibMono = fMono fib fibUp
  \end{code}
  
  
  Conclusion
  ----------
  
  We saw how refinement reflection turns Haskell
  into a theorem prover by reflecting the code 
  implementing a Haskell function into the 
  function’s output refinement type.
  
  Refinement Types are used to express theorems, 
  Haskell code is used to prove such theorems
  expressing paper pencil proofs, and Liquid Haskell 
  verifies the validity of the proofs!
  
  Proving `fib` monotonic is great, but this is Haskell!
  Wouldn’t it be nice to prove theorems about inductive data types 
  and higher order functions? Like fusions and folds? 
  Or program equivalence on run-time optimizations like map-reduce?
  
  Stay tuned!
  
  Even better, if you happen you be in Nara for ICFP'16, 
  come to my [CUFP tutorial][cufp16] for more!
  
  
  [cufp16]: http://cufp.org/2016/t6-niki-vazou-liquid-haskell-intro.html
  [proofcomb]:https://github.com/ucsd-progsys/liquidhaskell/blob/develop/include/Language/Haskell/Liquid/ProofCombinators.hs
  