# 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 `>=`) to 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 defined `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 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.