Posted by Niki Vazou Sep 18, 2016

Tags: reflection

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. 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 fibrestricted to natural numbers, always terminates returning a natural number.

70: {-@ fib :: i:Nat -> Nat / [i] @-}
71: {v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0}fib {v : GHC.Types.Int | v >= 0}i | GHC.Types.Booli x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x1 == x2}== 0    = 0
72:       | GHC.Types.Booli x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x1 == x2}== 1    = 1
73:       | otherwise = {v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1) x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-2)

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 with, we import ProofCombinators, a (Liquid) Haskell library that defines and manipulates logical proofs.

A Proof is a data type that carries no run time information

95: type Proof = ()

but can be refined with desired logical propositions. For example, the following type states that 1 + 1 == 2

102: {-@ type OnePlusOne = {v: Proof | 1 + 1 == 2} @-}

Since the v and Proof are irrelevant, we may as well abbreviate the above to

109: {-@ type OnePlusOne' = { 1 + 1 == 2 } @-}

As another example, the following function type declares that for each x and y the plus operator commutes.

117: {-@ type PlusComm = x:Int -> y:Int -> {x + y == y + x} @-}

Trivial Proofs

We prove the above theorems using Haskell programs. The ProofCombinators module defines the trivial proof

129: trivial :: Proof
130: trivial = ()

and the “casting” operator (***) that makes proof terms look nice:

137: data QED = QED
138:
139: (***) :: a -> QED -> Proof
140: _ *** _ = ()

Using the underlying SMT’s knowledge on linear arithmetic, we can trivially prove the above propositions.

147: {-@ propOnePlueOne :: _ -> OnePlusOne @-}
148: () -> {VV : () | 1 + 1 == 2}propOnePlueOne _ = {v : Language.Haskell.Liquid.ProofCombinators.QED | v == Language.Haskell.Liquid.ProofCombinators.QED}trivial *** QED
149:
150: {-@ propPlusComm :: PlusComm @-}
151: x1:GHC.Types.Int -> x2:GHC.Types.Int -> {VV : () | x1 + x2 == x2 + x1}propPlusComm _ _ = {v : Language.Haskell.Liquid.ProofCombinators.QED | v == Language.Haskell.Liquid.ProofCombinators.QED}trivial *** QED

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

171: {-@ reflect fib @-}

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.

185: fib :: Int -> Int

SMT only knows that fib satisfies the congruence axiom.

191: {-@ fibCongruence :: i:Nat -> j:Nat -> {i == j => fib i == fib j} @-}
192: x1:{v : GHC.Types.Int | v >= 0} -> x2:{v : GHC.Types.Int | v >= 0} -> {VV : () | x1 == x2 => fib x1 == fib x2}fibCongruence _ _ = {v : Language.Haskell.Liquid.ProofCombinators.QED | v == Language.Haskell.Liquid.ProofCombinators.QED}trivial *** QED

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.

210: 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.

217: fibP i = if i == 0 then 0 else
218:          if i == 1 then 1 else
219:          fin (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:

231: {-@ fibTwo :: _ -> { fib 2 == 1 } @-}
232: () -> {VV : () | fib 2 == 1}fibTwo _ = {v : [GHC.Types.Int] | null v <=> false}[{v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 0, {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 1, {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 2] *** QED

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

252: (==.) :: x:a -> y:{a| x==y} -> {v:a| v==x}
253: x ==. _ = x
254:
255: (<=.) :: x:a -> y:{a| x<=y} -> {v:a| v==x}
256: x <=. _ = x

Using these predefined operators, we construct paper and pencil-like proofs for the fib function.

263: {-@ fibTwoPretty :: { fib 2 == 1 } @-}
264: {VV : () | fib 2 == 1}fibTwoPretty
265:   =   {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 2
266:   GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int==. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 1 x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 0
267:   *** QED

Because operator

To allow the reuse of existing proofs, ProofCombinators defines the because operator (∵)

279: () :: (Proof -> a) -> Proof -> a
280: f  y = f y

For example, fib 3 == 2 holds because fib 2 == 1:

286: {-@ fibThree :: _ -> { fib 3 == 2 } @-}
287: () -> {VV : () | fib 3 == 2}fibThree _
288:   =   {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 3
289:   GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int==. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 2 x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 1
290:   GHC.Types.Int -> GHC.Types.Int -> () -> GHC.Types.Int==. GHC.Types.Int1     x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ 1       fibTwoPretty
291:   GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int==. 2
292:   *** QED

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 fubUp and use Haskell code to persuade Liquid Haskell that the theorem holds.

309: {-@ fibUp :: i:Nat -> {fib i <= fib (i+1)} @-}
310: x1:{v : GHC.Types.Int | v >= 0} -> {VV : () | fib x1 <= fib (x1 + 1)}fibUp {v : GHC.Types.Int | v >= 0}i
311:   | GHC.Types.Booli x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x1 == x2}== 0
312:   =   {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 0 GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int<. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 1
313:   *** QED
314:
315:   | GHC.Types.Booli x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x1 == x2}== 1
316:   =   {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 1 GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int<=. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 1 x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 0 GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int<=. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib 2
317:   *** QED
318:
319:   | otherwise
320:   =   {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib i
321:   GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int==. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1) x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-2)
322:   GHC.Types.Int -> GHC.Types.Int -> () -> GHC.Types.Int<=. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib i     x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-2)  x1:{v : GHC.Types.Int | v >= 0} -> {VV : () | fib x1 <= fib (x1 + 1)}fibUp (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1)
323:   GHC.Types.Int -> GHC.Types.Int -> () -> GHC.Types.Int<=. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib i     x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1)  x1:{v : GHC.Types.Int | v >= 0} -> {VV : () | fib x1 <= fib (x1 + 1)}fibUp (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-2)
324:   GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int<=. {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib (GHC.Types.Intix1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+1)
325:   *** QED

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!

345: {-@ fMono :: f:(Nat -> Int)
346:           -> fUp:(z:Nat -> {f z <= f (z+1)})
347:           -> x:Nat
348:           -> y:{Nat|x < y}
349:           -> {f x <= f y} / [y]
350:   @-}
351: x1:({v : GHC.Types.Int | v >= 0} -> GHC.Types.Int) -> (x4:{v : GHC.Types.Int | v >= 0} -> {VV : () | x1 x4 <= x1 (x4 + 1)}) -> x5:{v : GHC.Types.Int | v >= 0} -> x6:{v : GHC.Types.Int | v >= 0
&& x5 < v} -> {VV : () | x1 x5 <= x1 x6}fMono {v : GHC.Types.Int | v >= 0} -> GHC.Types.Intf x1:{v : GHC.Types.Int | v >= 0} -> {VV : () | f x1 <= f (x1 + 1)}thm {v : GHC.Types.Int | v >= 0}x {v : GHC.Types.Int | v >= 0
&& x < v}y
352:   | GHC.Types.Intx x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ 1 x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x1 == x2}== y
353:   = {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f y GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int==. {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f (GHC.Types.Intx x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ 1)
354:          GHC.Types.Int -> GHC.Types.Int -> () -> GHC.Types.Int>. {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f x        {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : () | f x1 <= f (x1 + 1)} | v == thm}thm x
355:         *** QED
356:
357:   | GHC.Types.Intx x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}+ 1 x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x1 < x2}< y
358:   = {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f x
359:   GHC.Types.Int -> GHC.Types.Int -> () -> GHC.Types.Int<.  {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f (GHC.Types.Intyx1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1)          x1:({v : GHC.Types.Int | v >= 0} -> GHC.Types.Int) -> (x4:{v : GHC.Types.Int | v >= 0} -> {VV : () | x1 x4 <= x1 (x4 + 1)}) -> x5:{v : GHC.Types.Int | v >= 0} -> x6:{v : GHC.Types.Int | v >= 0
&& x5 < v} -> {VV : () | x1 x5 <= x1 x6}fMono {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : () | f x1 <= f (x1 + 1)} | v == thm}thm x (GHC.Types.Intyx1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1)
360:   GHC.Types.Int -> GHC.Types.Int -> () -> GHC.Types.Int<.  {v : {v : GHC.Types.Int | v >= 0} -> GHC.Types.Int | v == f}f y              {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : () | f x1 <= f (x1 + 1)} | v == thm}thm (GHC.Types.Intyx1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 - x2}-1)
361:   *** QED

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.

371: {-@ fibMono :: n:Nat -> m:{Nat | n < m }  -> {fib n <= fib m} @-}
372: x1:{v : GHC.Types.Int | v >= 0} -> x2:{v : GHC.Types.Int | v >= 0
&& x1 < v} -> {VV : () | fib x1 <= fib x2}fibMono = {v : x1:({v : GHC.Types.Int | v >= 0} -> GHC.Types.Int) -> (x4:{v : GHC.Types.Int | v >= 0} -> {v : () | x1 x4 <= x1 (x4 + 1)}) -> x5:{v : GHC.Types.Int | v >= 0} -> x6:{v : GHC.Types.Int | v >= 0
&& x5 < v} -> {v : () | x1 x5 <= x1 x6} | v == RefinementReflection.fMono}fMono {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : GHC.Types.Int | v >= 0
&& v == fib x1
&& v == (if x1 == 0 then 0 else (if x1 == 1 then 1 else fib (x1 - 1) + fib (x1 - 2)))} | v == fib}fib {v : x1:{v : GHC.Types.Int | v >= 0} -> {v : () | fib x1 <= fib (x1 + 1)} | v == RefinementReflection.fibUp}fibUp

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 for more!