Getting off the ground

False

The type False has no elements. Since there are no terms that satisfy e : False, the type False is the type of unprovable propositions.

Unit

The type unit has a single element denoted (), i.e., () : unit.

Booleans

The type bool has two elements, true and false. Note, the lowercase false is a boolean constant, distinct from the uppercase False type.

The following primitive boolean operators are available, in decreasing order of precedence.

• not: Boolean negation (unary, prefix)

• &&: Boolean conjunction (binary, infix)

• ||: Boolean disjunction (binary, infix)

if b then 1 else 0

if b1 && b2 || b3
then 17
else 42

Integers

The type int represents unbounded, primitive mathematical integers. Its elements are formed from the literals 0, 1, 2, ..., and the following primitive operators, in decreasing order of precedence.

• -: Unary negation (prefix)

• -: Subtraction (infix)

• +: Addition (infix)

• /: Euclidean division (infix)

• %: Euclidean modulus (infix)

• op_Multiply: Unfortunately, the traditional multiplication symbol * is reserved by default for the tuple type constructor. Use the module FStar.Mul to treat * as integer multiplication.

• < : Less than (infix)

• <=: Less than or equal (infix)

• > : Greater than (infix)

• >=: Greater than or equal (infix)

Refinement subtyping

We have seen so far how to define a new refinement type, like nat or even. However, to make use of refinement types we need rules that allow us to:

1. check that a program term has a given refinement type, e.g., to check that 0 has type nat. This is sometimes called introducing a refinement type.

2. make use of a term that has a refinement type, e.g., given x : even we would like to be able to write x + 1, treating x as an int to add 1 to it. This is sometimes called eliminating a refinement type.

The technical mechanism in F* that supports both these features is called refinement subtyping.

If you’re used to a language like Java, C# or some other object-oriented language, you’re familiar with the idea of subtyping. A type t is a subtype of s whenever a program term of type t can be safely treated as an s. For example, in Java, all object types are subtypes of the type Object, the base class of all objects.

For boolean refinement types, the subtyping rules are as follows:

• The type x:t { p } is a subtype of t. That is, given e : (x:t{p}), it is always safe to eliminate the refinement and consider e to also have type t.

• For a term e of type t (i.e., e : t), t is a subtype of the boolean refinement type x:t { p } whenever p[e / x] (p[e/x] is notation for the term p with the variable x replaced by e), is provably equal to true. In other words, to introduce e : t at the boolean refinement type x:t{ p }, it suffices to prove that the term p with e substituted for bound variable x, evaluates to true.

The elimination rule for refinement types (i.e., the first part above) is simple—with our intuition of types as sets, the refinement type x:t{ p } refines the set corresponding to t by the predicate p, i.e., the x:t{ p } denotes a subset of t, so, of course x:t{ p } is a subtype of t.

The other direction is a bit more subtle: x:t{ p } is only a subtype of p, for those terms e that validate p. You’re probably also wondering about how to prove that p[e/x] evaluates to true—we will look at this in detail later. But, the short version is that F*, by default, uses an SMT solver to prove such fact, though you can also use tactics and other techniques to do so.

An example

Given x:even, consider proving x + 1 : odd; it takes a few steps:

1. The operator + is defined in F*’s library. It expects both its arguments to have type int and returns an int.

2. To prove that the first argument x:even is a valid argument for +, we use refinement subtyping to eliminate the refinement and obtain x:int. The second argument 1:int already has the required type. Thus, x + 1 : int.

3. To conclude that x + 1 : odd, we need to introduce a refinement type, by proving that the refinement predicate of odd evaluates to true, i.e., x + 1 % 2 = 1. This is provable by SMT, since we started with the knowledge that x is even.

As such, F* applies subtyping repeatedly to introduce and eliminate refinement types, applying it multiple times even to check a simple term like x + 1 : odd.

Lambda terms

The term fun (x:int) -> x + 1 defines a function, a lambda term, which adds 1 to its integer-typed parameter x. You can also let F* infer the type of the parameter and write fun x -> x + 1 instead.

Named functions

Any term in F* can be given a name using a let binding. We’ll want this to define a function once and to call it many times. For example, all of the following are synonyms and bind the lambda term fun x -> x + 1 to the name incr

let incr = fun (x:int) -> x + 1
let incr (x:int) = x + 1
let incr x = x + 1

Functions can take several arguments and the result type of a function can also be annotated, if desired

let incr (x:int) : int = x + 1
let more_than_twice (x:int) (y:int) : bool = x > y + y

It’s considered good practice to annotate all the parameters and result type of a named function definition.

let incr = fun (x:int) -> (x + 1 <: int)

Recursive functions

Recursive functions in F* are always named. To define them, one uses the let rec syntax, as shown below.

open FStar.Mul
let rec factorial (n:nat)
  : nat
  = if n = 0
    then 1
    else n * factorial (n - 1)

This syntax defines a function names factorial with a single parameter n:nat, returning a nat. The definition of factorial is allowed to use the factorial recursively—as we’ll see in a later chapter, ensuring that the recursion is well-founded (i.e., all recursive calls terminate) is key to F*’s soundness. However, in this case, the proof of termination is automatic.

F* also supports mutual recursion. We’ll see that later.

Some examples and common notation

1. Functions are curried. Functions that take multiple arguments are written as functions that take the first argument and return a function that takes the next argument and so on. For instance, the type of integer addition is:

   val (+) : x:int -> y:int -> int
   

2. Not all functions are dependent and the name of the argument can be omitted when it is not needed. For example, here’s a more concise way to write the type of (+):

   val (+) : int -> int -> int
   

3. Function types can be mixed with refinement types. For instance, here’s the type of integer division—the refinement on the divisor forbids division-by-zero errors:

   val (/) : int -> (divisor:int { divisor <> 0 }) -> int
   

4. Dependence between the arguments and the result type can be used to state relationships among them. For instance, there are several types for the function let incr = (fun (x:int) -> x + 1):

   val incr : int -> int
   val incr : x:int -> y:int{y > x}
   val incr : x:int -> y:int{y = x + 1}
   

   The first type int -> int is its traditional type in languages like OCaml.

   The second type x:int -> y:int{y > x} states that the returned value y is greater than the argument x.

   The third type is the most precise: x:int -> y:int{y = x + 1} states that the result y is exactly the increment of the argument x.

5. It’s often convenient to add refinements on arguments in a dependent function type. For instance:

   val f : x:(x:int{ x >= 1 }) -> y:(y:int{ y > x }) -> z:int{ z > x + y }
   

   Since this style is so common, and it is inconvenient to have to bind two names for the parameters x and y, F* allows (and encourages) you to write:

   val f : x:int{ x >= 1 } -> y:int{ y > x } -> z:int{ z > x + y }
   

6. To emphasize that functions in F*’s core are total functions (i.e., they always return a result), we sometimes annotate the result type with the effect label “Tot”. This label is optional, but especially as we learn about effects, emphasizing that some functions have no effects via the Tot label is useful. For example, one might sometimes write:

   val f : x:int{ x >= 1 } -> y:int{ y > x } -> Tot (z:int{ z > x + y })
   

   adding a Tot annotation on the last arrow, to indicate that the function has no side effects. One could also write:

   val f : x:int{ x >= 1 } -> Tot (y:int{ y > x } -> Tot (z:int{ z > x + y }))
   

   adding an annotation on the intermediate arrow, though this is not customary.

Many types for incr

Here are some types for incr, including some types that are valid and some others that are not.

This type claims that incr result is greater than its argument and F* agrees—remember, the int type is unbounded, so there’s no danger of the addition overflowing.

let incr1 (x:int) : y:int{y > x} = x + 1

This type claims that incr always returns a natural number, but it isn’t true, since incrementing a negative number doesn’t always produce a non-negative number.

let incr2 (x:int) : nat = x + 1

F* produces the following error message:

Sample.fst(11,26-11,31): (Error 19) Subtyping check failed; expected type
Prims.nat; got type Prims.int; The SMT solver could not prove the query, try to
spell your proof in more detail or increase fuel/ifuel (see also prims.fst(626,
18-626,24))
Verified module: Sample
1 error was reported (see above)

Source location

The error message points to Sample.fst(11,26-11,31), a source range mentioned the file name, a starting position (line, column), and an ending position (line, column). In this case, it highlights the x + 1 term.

Severity and error code

The (Error 19) mentions a severity (i.e., Error, as opposed to, say, Warning), and an error code (19).

Error message

The first part of the message stated what you might expect:

Subtyping check failed; expected type Prims.nat; got type Prims.int

The rest of the message provides more details, which we’ll ignore for now, until we’ve had a chance to explain more about how F* interacts with the SMT solver. However, one part of the error message is worth pointing out now:

(see also prims.fst(626,18-626,24))

Error messages sometimes mention an auxiliary source location in a “see also” parenthetical. This source location can provide some more information about why F* rejected a program—in this case, it points to the constraint x>=0 in the definition of nat in prims.fst, i.e., this is the particular constraint that F* was not able to prove.

So, let’s try again. Here’s another type for incr, claiming that if its argument is a natural number then so is its result. This time F* is happy.

let incr3 (x:nat) : nat = x + 1

Sometimes, it is convenient to provide a type signature independently of a definition. Below, the val incr4 provides only the signature and the subsequent let incr4 provides the definition—F* checks that the definition is compatible with the signature.

val incr4 (x:int) : int
let incr4 x = x + 1

Try writing some more types for incr. (Load exercise.)

let incr5 (x:int) : y:int{y = x + 1} = x + 1
let incr6 (x:int) : y:int{x = y - 1} = x + 1
let incr7 (x:int) : y:int{if x%2 = 0 then y%2 = 1 else y%2 = 0} = x + 1

Computing the maximum of two integers

Provide an implementation of the following signature:

val max (x:int) (y:int) : int

There are many possible implementations that satisfy this signature, including trivial ones like:

let max x y = 0

Provide an implementation of max coupled with a type that is precise enough to rule out definitions that do not correctly return the maximum of x and y.

val max (x:int) (y:int) : int
let max x y = if x >= y then x else y

val max1 (x:int) (y:int)
  : z:int{ z >= x && z >= y && (z = x || z = y)}
let max1 x y = if x >= y then x else y

let max2 (x:int) (y:int)
  : z:int{ z = max x y }
  = if x > y
    then x
    else y

More types for factorial

Recall the definition of factorial from earlier.

open FStar.Mul
let rec factorial (n:nat)
  : nat
  = if n = 0
    then 1
    else n * factorial (n - 1)

Can you write down some more types for factorial?

let rec factorial1 (n:nat)
  : int
  = if n = 0
    then 1
    else n * factorial1 (n - 1)

let rec factorial2 (n:nat)
  : y:int{y>=1}
  = if n = 0
    then 1
    else n * factorial2 (n - 1)

Fibonacci

Here’s a doubly recursive function:

let rec fibonacci (n:nat)
  : nat
  = if n <= 1
    then 1
    else fibonacci (n - 1) + fibonacci (n - 2)

What other types can you give to it?

val fibonacci_1 : x:int -> y:int{y >= 1 /\ y >= x /\ (if x>=3 then y >= 2 else true)}
let rec fibonacci_1 n =
  if n <= 1 then 1 else fibonacci_1 (n - 1) + fibonacci_1 (n - 2)

(* Try these other types too *)
(* val fibonacci_1 : int -> int *)
(* val fibonacci_1 : int -> nat *)
(* val fibonacci_1 : int -> y:int{y>=1} *)
(* val fibonacci_1 : x:int -> y:int{y>=1 /\ y >= x} *)
(* val fibonacci_1 : int -> Tot (x:nat{x>0}) *)