Interfacing with an SMT solver

As mentioned at the start of this section, a type t represents a proposition and a term e : t is a proof of t. In many other dependently typed languages, exhibiting a term e : t is the only way to prove that t is valid. In F*, while one can do such proofs, it is not the only way to prove a theorem.

By way of illustration, let’s think about Boolean refinement types. As we’ve seen already, it is easy to prove 17 : x:int{x >= 0} in F*. Under the covers, F* proves that (x >= 0) [17/x] reduces to true, yet no explicit term is given to prove this fact. Instead, F* encodes facts about a program (including things like the semantics of arithmetic operators like >=) in the classical logic of an SMT solver and asks it (Z3 typically) to prove whether the formula 17 >= 0 is valid in a context including all encoded facts about a program. If Z3 is able to prove it valid, F* accepts the formula as true, without ever constructing a term representing a proof of 17 >= 0.

This design has many important consequences, including, briefly:

  • Trust: F* implicitly trusts its encoding to SMT logic and the correctness of the Z3 solver.

  • Proof irrelevance: Since no proof term is constructed for proofs done by SMT, a program cannot distinguish between different proofs of a fact proven by SMT.

  • Subtyping: Since no proof term is constructed, a term like 17 can have many types, int, nat, x:int{x = 17}, etc. As mentioned earlier, F* leverages this to support refinement subtyping.

  • Undecidability: Since Z3 can check the validity of formulas in the entirety of its logic, including things like quantifying universally and existentially over infinite ranges, F* does not restrict the the formulas checked for validity by Z3 to be boolean, or even decidable. Yes, typechecking in F* is undecidable.

In this chapter, we’ll learn about the the classical logic parts of F*, i.e., the parts that allow it to interface with an SMT solver.

Note

The beginning of this chapter is a little technical, even though we’re not telling the full story behind F*’s classical logic yet. If parts of it are hard to understand right now, here’s what you need to know to before you jump ahead.

F* let’s you write quantified formulas, called propositions, like so

forall (x1:t1) ... (xn:tn). p
exists (x1:t1) ... (xn:tn). p

You can build propositions from booleans and conjunctions, disjunctions, negations, implications, and bi-implications:

p /\ q   //conjunction
p \/ q   //disjunction
~p       //negation
p ==> q  //implication
p <==> q //bi-implication

For example, one can say (as shown below) that for all natural numbers x and y, if the modulus x % y is 0, then there exists a natural number z such that x is z * y.

forall (x:nat) (y:nat). x % y = 0 ==> (exists (z:nat). x = z * y)

F* also has a notion of propositional equality, written ==, that can be used to state that two terms of any type are equal. In contrast, the boolean equality = can only be used on types that support decidable equality. For instance, for f1, f2 : int -> int, you can write f1 == f2 but you cannot write f1 = f2, since two functions cannot be decidably compared for equality.

Propositions

The type prop defined in Prims is F*’s type of proof-irrelevant propositions. More informally, prop is the type given to facts that are provable using the SMT solver’s classical logic.

Propositions defined in prop need not be decidable. For example, for a Turing machine tm, the fact halts tm can be defined as a prop, although it is impossible to decide for an arbitrary tm whether tm halts on all inputs. This is contrast with bool, the type of booleans {true, false}. Clearly, one could not define halts tm as a bool, since one would be claiming that for halts is function that for any tm can decide (by returning true or false) whether or not tm halts on all inputs.

F* will implicitly convert a bool to a prop when needed, since a decidable fact can be turned into a fact that may be undecidable. But, when using propositions, one can define things that cannot be defined in bool, including quantified formulae, as we’ll see next.

Propositional connectives

Consider stating that factorial n always returns a positive number, when n:nat. In the previous section we learned that one way to do this is to give factorial a type like so.

val factorial (n:nat) : x:nat{x > 0}

Here’s another way to state it:

forall (n:nat). factorial n > 0

What about stating that factorial n can sometimes return a value that’s greater than n * n?

exists (n:nat). factorial n > n * n

We’ve just seen our first use of universal and existential quantifiers.

Quantifiers

A universal quantifier is constructed using the forall keyword. Its syntax has the following shape.

forall (x1:t1) ... (xn:tn) . p

The x1 ... xn are bound variables and signify the domain over which one the proposition p is quantified. That is, forall (x:t). p is valid when for all v : t the proposition p[v/x] is valid.

And existential quantifier has similar syntax, using the exists keyword.

exists (x1:t1) ... (xn:tn) . p

In this case, exists (x:t). p is valid when for some v : t the proposition p[v/x] is valid.

The scope of a quantifier extends as far to the right as possible.

As usual in F*, the types on the bound variables can be omitted and F* will infer them. However, in the case of quantified formulas, it’s a good idea to write down the types, since the meaning of the quantifier can change significantly depending on the type of the variable. Consider the two propositions below.

exists (x:int). x < 0
exists (x:nat). x < 0

The first formula is valid by considering x = -1, while the second one is not—there is not natural number less than zero.

It is possible to quantify over any F* type. This makes the quantifiers higher order and dependent. For example, one can write

forall (n:nat) (p: (x:nat{x >= n} -> prop)). p n

Note

The SMT solver uses a number of heuristics to determine if a quantified proposition is valid. As you start writing more substantial F* programs and proofs, it will become important to learn a bit about these heuristics. We’ll cover this in a later chapter. If you’re impatient, you can also read about in on the F* wiki.

Conjunction, Disjunction, Negation, Implication

In addition to the quantifiers, you can build propositions by combining them with other propositions, using the operators below, in decreasing order of precedence.

Negation

The proposition ~p is valid if the negation of p is valid. This is similar to the boolean operator not, but applies to propositions rather than just booleans.

Conjunction

The proposition p /\ q is valid if both p and q are valid. This is similar to the boolean operator &&, but applies to propositions rather than just booleans.

Disjunction

The proposition p \/ q is valid if at least one of p and q are valid. This is similar to the boolean operator ||, but applies to propositions rather than just booleans.

Implication

The proposition p ==> q is valid if whenever p is valid, q is also valid.

Double Implication

The proposition p <==> q is valid if p and q are equivalent.

Note

This may come as a surprise, but these precedence rules mean that p /\ q ==> r is parsed as (p /\ q) ==> r rather than p /\ (q ==> r). When in doubt, use parentheses.

Atomic propositions

We’ve shown you how to form new propositions by building them from existing propositions using the connectives. But, what about the basic propositions themselves?

Falsehood

The proposition False is always invalid.

Truth

The proposition True is always valid.

Propositional equality

We learned in the previous chapter about the two different forms of equality. The type of propositional equality is

val ( == ) (#a:Type) (x:a) (y:a) : prop

Unlike decidable equality (=), propositional equality is defined for all types. The result type of (==) is prop, the type of propositions, meaning that x == y is a proof-irrelevant proposition.

Turning a Boolean into a proposition

Propositional equality provides a convenient way to turn a boolean into a proposition. For any boolean b, then term b == true is a prop. One seldom needs to do write this manually (although it does come up occasionally), since F* will automatically insert a b==true if you’re using a b:bool in a context where a prop was expected.

Type vs. prop

This next bit is quite technical. Don’t worry if you didn’t understand it at first. It’s enough to know at this stage that, just like automatically converting a boolean to prop, F* automatically converts any type to prop, when needed. So, you can form new atomic propositions out of types.

Every well-typed term in F* has a type. Even types have types, e.g., the type of int is Type, i.e., int : Type, bool : Type, and even prop : Type. We’ll have to leave a full description of this to a later section, but, for now, we’ll just remark that another way to form an atomic proposition is to convert a type to a proposition.

For any type t : Type, the type _:unit { t } : prop. We call this “squashing” a type. This is so common, that F* provides two mechanisms to support this:

  1. All the propositional connectives, like p /\ q are designed so that both p and q can be types (i.e., p,q : Type), rather than propositions, and they implicitly squash their types.

  2. The standard library, FStar.Squash, provides several utilities for manipulating squashed types.

Assertions

Now that we have a way to write down propositions, how can we ask F* to check if those propositions are valid? There are several ways, the most common of which is an assertion. Here’s an example:

let sqr_is_nat (x:int) : unit = assert (x * x >= 0)

This defines a function sqr_is_nat : int -> unit—meaning it takes a nat and always returns (). So, it’s not very interesting as a function.

However, it’s body contains an assertion that x * x >= 0. Now, many programming languages support runtime assertions—code to check some property of program when it executes. But, assertions in F* are different—they are checked by the F* compiler before your program is executed.

In this case, the assert instructs F* to encode the program to SMT and to ask Z3 if x * x >= 0 is valid for an arbitrary integer x:int. If Z3 can confirm this fact (which it can), then F* accepts the program and no trace of the assertion is left in your program when it executes. Otherwise the program is rejected at compile time. For example, if we were to write

let sqr_is_pos (x:int) : unit = assert (x * x > 0)

Then, F* complains with the following message:

Ch2.fst(5,39-5,50): (Error 19) assertion failed; The SMT solver could not prove the query, try to spell your proof in more detail or increase fuel/ifuel

You can use an assertion with any proposition, as shown below.

let max x y = if x > y then x else y
let _ = assert (max 0 1 = 1)
let _ = assert (forall x y. max x y >= x /\
                            max x y >= y /\
                            (max x y = x \/ max x y = y))

Assumptions

The dual of an assertion is an assumption. Rather than asking F* and Z3 to prove a fact, an assumption allows one to tell F* and Z3 to accept that some proposition is valid. You should use assumptions with care—it’s easy to make a mistake and assume a fact that isn’t actually true.

The syntax of an assumption is similar to an assertion. Here, below, we write assume (x <> 0) to tell F* to assume x is non-zero in the rest of the function. That allows F* to prove that the assertion that follows is valid.

let sqr_is_pos (x:int) = assume (x <> 0); assert (x * x > 0)

Of course, the assertion is not valid for all x—it’s only valid for those x that also validate the preceding assumption.

Just like an assert, the type of assume p is unit.

There’s a more powerful form of assumption, called an admit. The term admit() can given any type you like. For example,

let sqr_is_pos (x:int) : y:nat{y > 0} = admit()

Both assume and admit can be helpful when you’re working through a proof, but a proof isn’t done until it’s free of them.