Overview

We illustrate Liquid Haskell as a theorem prover. It is a formed version of § 2 of "Towards Complete Specification and Verification with SMT".

Prelude

Overview is a Haskell module with Liquid Haskell annotations. We enable the Liquid Haskell flags that allow higher order reasoning (which is increasing the precision of verification and is by default off for efficiency). By default Liquid Haskell checks that all your functions are total.

2.1 Refinement Types

Propositions with SMT-automated proofs

Note: In the paper we defined plus_2_2 to take zero arguments, while here we give it a unit argument. The reason is to keep verification local. If we define a zero argument proof term, the property it is proving will be checked but then will enter in the assumption environment that proves the rest of the module. For example, the following property (commented out) will get verified as unsafe

but then verification of the rest of the module will assume false. This is sound, but inconvenient. Thus, we follow the convention not to have proof terms without arguments.

2.2 Refinement Reflection

We define the function fib on natural numbers and reflect it into logic.

Unlike the paper, we return the results t0, t1, and t2. If we do not return these calls, ghc will optimize them away, to Liquid Haskell will not see these calls. Thus the pf_fib2 version presented in the paper:

In unsafe, since Liquid Haskell just sees

Alternative, we could write

2.3 Equational Proofs

We structure proofs using proof combinators from the imported ProofCombinators library, that comes with Liquid Haskell.

• “Equation” Combinators Using the (==.) equational operator, the proof fib2_1 is formatted as below.

Note: the operator ==. takes two terms to be proved equal and one optional proof argument. You can check its definition at the library
ProofCombinators

Also, the intermediate steps of the proofs are not checked. For example, the following proof is verified, even if the intermediate equality steps are not correct

• “Because” Combinators To prove fib 3 = 2 we call the proof fib2_1 as a lemma using the (?) combinator.

• Arithmetic and Ordering Similarly, we use arithmetic proof combinators for arithmetic proofs.

• Induction & Higher Order Reasoning Our technique reasons about higher order properties too, that is, we can prove theorems over any function f. For example, we prove that every function f that increases locally (i.e. f z ≤ f (z+1) for all z) also increases globally (i.e. f x ≤ f y for all x < y)

We prove the theorem by induction on y as specified by the annotation / [y] which states that y is a well-founded termination metric that decreases at each recursive call.

We can apply the general fMono theorem to prove that fib increases monotonically:

2.4 Complete Verification: Automating Equational Reasoning

Next, we use PLE to automate our proofs. The local automatic-instances flag activates PLE on functions that are marked with automatic-instances

With these flags (as thus PLE) activated, the proof terms as simplified to only use recursive calls and helper lemmata.