# Liquid Types vs. Floyd-Hoare Logic

Several folks who are experts in the program verification literature have asked me some variant of the following question:

How are Liquid/Refinement types different from Floyd-Hoare logics?

This question always reminds me of Yannis Smaragdakis' clever limerick:

No idea is too obvious or dreary,

If appropriately expressed in type theory,

That no one understands,

But they are all too impressed to be leery.

That is, the above question can be rephrased as: why bother with the hassle of encoding properties in types when good old-fashioned assertions, pre- and post-conditions would do? Is it just a marketing gimmick to make readers too impressed to be leery?

## The Problem: Quantifiers¶

The main algorithmic problem with classical Floyd-Hoare logic is that to do useful things, you need to use universally quantified logical formulas inside invariants, pre- and post-conditions.

Verification then proceeds by asking SMT solvers to check verification conditions (VCs) over these quantified formulas. While SMT solvers are marvelous technological artifacts, and I bow to no one in my admiration of them, in reality, they work best on formulas from a narrowly defined set of decidable theories.

In particular, they are notoriously (and justifiably!) fickle when quizzed on VCs with quantifiers. Briefly, this is because even if the solver "knows" the universally quantified fact:

``````forall x. P(x)
``````

the solver doesn't know which particular terms `e1`, `e2` or `e3` to instantiate the fact at. That is, the solver doesn't know which `P(e1)` or `P(e2)` or `P(e3)` it should work with to prove some given goal. At best, it can make some educated guesses, or use hints from the user, but these heuristics can turn out to be quite brittle as the underlying logics are undecidable in general. To make verification predictable, we really want to ensure that the VCs remain decidable, and to do so, we must steer clear of the precipice of quantification.

## The Solution: Types¶

The great thing about types, as any devotee will tell you, is that the compose. Regrettably, that statement is only comprehensible to believers. I prefer to think of it differently: types decompose. To be precise:

Types decompose quantified assertions into quantifier-free refinements.

Let me make my point with some examples that show what verification looks like when using Refinement Types (as implemented in LiquidHaskell) vs Floyd-Hoare style contracts (as implemented in Dafny).

The goal of this exercise is to illustrate how types help with verification, not to compare the tools LH and Dafny. In particular, Dafny could profit from refinement types, and LH could benefit from the many clever ideas embodied within Dafny.

## Example 1: Properties of Data¶

Consider the following standard definition of a `List` datatype in Dafny (left) and LH (right).

(You can see the full definitions for Dafny and LiquidHaskell.)

### Accessing a list¶

The two descriptions are more or less the same except for some minor issues of concrete syntax. However, next consider the respective implementations of a function to access the `ith` element of a `List`. We also pass in a `def`ault value returned when the index `i` is invalid.

It is (usually) silly to access lists in this fashion. I use this example merely to illustrate the common case of defining a container structure (here, `List`) and then accessing its contents (here, `ith`). As such, we'd like to specify that the value returned by the `ith` element is indeed in the container or is the `def`ault.

Floyd-Hoare Logic

With classical Floyd-Hoare logic, as shown in the Dafny listing on the left, we must spell out the specification quite explicitly. The programmer must write an `elements` function that describes the set of values in the container, and then the post-condition of `ith` states that the `res` is either in that set or the default.

While this specification seems simple enough, we are already on dicey terrain: how are we to encode the semantics of the user-defined function `elements` to the SMT solver? In the classical Floyd-Hoare approach, we must use a quantified invariant of the form:

``````   elements(Nil) = empty
&& forall h t :: elements(Cons(h, t)) = {h} + elements(t)
``````

Thanks to the ingenuity of Greg Nelson who invented the notion of triggers and of Rustan Leino and many others, who devised ingenious heuristics for using them, Dafny handles the quantifier calmly to verify the above specification for `ith`. However, we are not always so fortunate: it frightfully easy to run into quantifier-related problems with user-defined functions, as we will see in due course.

Liquid/Refinement Types

In contrast, the liquid/refinement version is quite spare: there is no extra specification beyond the code. Surely there must be some mistake? Look again: the type signature says everything we need:

If you call `ith` with a list of `a` values and a default `a` value then you get an `a` value".

That is parametricity removes the overhead of using an explicit `elements` function.

### Building a list¶

Next, lets extend our example to illustrate the common situation where we want some invariant to be true for all the values in a container. To this end, let us write a function `mkList` that builds a container with values `k+1`,...,`k+n` and then test that when `k` is non-negative, any arbitrarily chosen value from the container is indeed strictly positive.

The code in Dafny and LH is more or less the same, except for one crucial difference.

Floyd-Hoare Logic

Recall that the specification for `ith(pos, i, 1)` states that the returned value is some element of the container (or `1`). Thus, to verify the `assert` in `testPosN` using classical Floyd-Hoare logic, we need a way to specify that every element in `pos` is indeed strictly positive. With classical program logics, the only way to do so is to use a universally quantified post-condition, highlighted in blue:

"for all `v` if `v` is in the elements of the `res`ult, then `v` is greater than `k`"

Liquid/Refinement Types

Regardless of my personal feelings about quantifiers, we can agree that the version on the right is simpler as types make it unnecessary to mention `elements` or `forall`. Instead, LH infers

``````mkList :: Int -> k:Int -> List {v:Int | k < v}
``````

That is, that the output type of `mkList` is a list of values `v` that are all greater than `k`. The scary forall has been replaced by the friendly type constructor `List`. In other words, types allow us to decompose the monolithic universally quantified invariant into:

1. a quantifier-free refinement `k < v`, and
2. a type constructor that implicitly "quantifies" over the container's elements.

### Lesson: Decomposition Enables Inference¶

Am I cheating? After all, what prevents Dafny from inferring the same post-condition as LH?

Once again, quantifiers are the villain.

There have been many decades worth of papers on the topic of inferring quantified invariants, but save some nicely circumscribed use-cases these methods turn out to be rather difficult to get working efficiently and predictably enough to be practical. In contrast, once the quantifiers are decomposed away, even an extremely basic approach called Monomial Predicate Abstraction, or more snappily, Houdini, suffices to infer the above liquid type.

## Example 2: Properties of Structures¶

Recall that when discussing the user-defined `elements` function above, I had issued some dark warnings about quantifier-related problems that arise from user-defined functions. Allow me to explain with another simple example, that continues with the `List` datatype defined above.

(You can see the full definitions for Dafny and LiquidHaskell.)

### Specifying a `size` Function¶

Lets write the usual recursive function that computes the `size` of a list. The definitions are mostly identical, except for the green `measure` highlight that we will discuss below.

Floyd-Hoare Logic

SMT solvers are restricted to a set of ground theories and hence, do not "natively" understand user-defined functions. Instead, the verifer must teach the SMT solver how to reason about formulas (VCs) containing uses of user-defined functions like `size`. In the classical Floyd-Hoare approach, this is done by converting the definition of `size` into a universally quantified axiom like:

``````size Nil == 0  && forall h, t :: size (Cons h t) = 1 + size t
``````

A quantifier! By the pricking of my thumbs, something wicked this way comes...

Liquid/Refinement Types

With a more type-centric view, we can think of the recursive function `size` as a way to decorate or refine the types of the data constructors. So, when you write the definition in the green box above, specifically when you add the `measure` annotation, the function is converted to strengthened versions for the types of the constructors `Nil` and `Cons`, so its as if we had defined the list type as two constructor functions

``````data List a where
Cons :: h:a -> t:List a -> {v:List a | size v == 1 + size t}
Nil  :: {v:List a | size v == 0}
``````

That is, the bodies of the measures get translated to refinements on the output types of the corresponding constructors. After this, the SMT solver "knows nothing" about the semantics of `size`, except that it is a function. In logic-speak, `size` is uninterpreted in the refinement, and there are no quantified axioms. That is, we choose to keep SMT solver blissfully ignorant about the semantics of `size`. How could this possibly be a good thing?

### Verifying the `size` of a List¶

Next, lets see what happens when we write a simple test that builds a small list with two elements and `assert`s that the lists `size` is indeed `2`:

Floyd-Hoare Logic

To get Dafny to verifier to sign off on the `assert (size(pos) == 2)` we have to add a mysterious extra assertion that checks the size of the intermediate value `Cons (1, Nil)`. (Without it, verification fails.)

Huh? Pesky quantifiers.

The SMT solver doesn't know where to instantiate the `size` axom. In this carefully chosen, but nevertheless simple situation, Dafny's instantiation heuristics come up short. I had to help them along by guessing this intermediate assertion, which effectively "adds" the fact that the size of the intermediate list is 1, thereby letting the SMT solver prove the second assertion.

Liquid/Refinement Types

In contrast, with types, the solver is able to verify the code without batting an eyelid. But how could it possibly do so even though we kept it ignorant of the semantics of `size`?

Because types decompose reasoning. In particular, here, the measure and constructor trick lets us factor reasoning about `size` into the type system.

In particular, LH internally views the code for `test` in A-Normal Form which is a fancy way of saying, by introducing temporary variables for all sub-expressions:

``````test x1 =
let tmp0 = Nil
tmp1 = Cons x1 tmp0
pos  = Cons  0 tmp1
in
assert (size pos == 2)
``````

And now, just by the rules of type checking, and applying the types of the constructors, it deduces that:

``````   tmp0 :: {size tmp0 == 0}
tmp1 :: {size tmp1 == 1 + size tmp0}
pos  :: {size pos  == 1 + size tmp1}
``````

which lets the SMT solver prove that `size pos == 2` without requiring any axiomatic description of `size`. This simple `measure` method goes a very long way in specifying and verifying lots of properties.

### Lesson: Decomposition Enables Type-Directed Instantiation¶

I'd like to emphasize again that this trick was enabled by the type-centric view: encode the function semantics in data constructors, and let the type checking (or VC generation) do the instantiation.

It could easily by incorporated inside and work together with axioms in Floyd-Hoare based systems like Dafny. Of course, this approach is limited to a restricted class of functions -- roughly, case-splits over a single data type's constructors -- but we can generalize the method quite a bit using the idea of logical evaluation.

## Summary¶

To sum up, we saw two examples where taking a type-centric view made verification more ergonomic, essentially by factoring reasoning about quantifiers into the type system.

• In the first case, when reasoning about data in containers, the polymorphic type constructor `List` provided an natural way to reason about the fact that all elements in a container satisfied some property.

• In the second case, when reasoning about the structure of the container via a recursive function, the types of the data constructors allowed us to factor the instantiation of properties of `size` at places where the list was constructed (and dually, not shown, destructed) without burdening the SMT solver with any axioms and the pressure of figuring out where to instantiate them.

To conclude I'd like to reiterate that the point is not that types and program logics are at odds with each other. Instead, the lesson is that while classical Floyd-Hoare logic associates invariants with program positions, Liquid/Refinement types are a generalization that additionally let you associate invariants with type positions, which lets us exploit

• types as a program logic, and
• syntax-directed typing rules as a decision procedure,

that, in many common situations, simplify verification by decomposing proof obligations (VCs) into simple, quantifier-free, SMT-friendly formulas. As you might imagine, the benefits are magnified when working with higher-order functions, e.g. `map`-ing or `fold`-ing over containers...

### Acknowledgments¶

Huge thanks to Rustan Leino, Nadia Polikarpova, Daniel Ricketts, Hillel Wayne, and Zizz Vonnegut for patiently answering my many questions about Dafny!

Ranjit Jhala
2019-10-21