1. Introduction

F* is a verification-oriented programming language developed at Microsoft Research, MSR-Inria, and Inria. It follows in the tradition of the ML family of languages in that it is a typed, strict, functional programming language. However, its type system is significantly richer than ML's, allowing functional correctness specifications to be stated and checked semi-automatically. This tutorial provides a first taste of verified programming in F*. More information about F*, including papers and technical reports, can be found on the F* website.

It will help if you are already familiar with functional programming languages in the ML family (e.g., OCaml, F#, Standard ML), or with Haskell—we provide a quick review of some basic concepts if you're a little rusty, but if you feel you need more background, there are many useful resources freely available on the web, e.g., Learn F#, F# for fun and profit, Introduction to Caml, the Real World OCaml book, or the OCaml MOOC.

The easiest way to try F* and solve the verification exercises in this tutorial is directly in your browser by using the online F* editor. You can load the boilerplate code needed for each exercise into the online editor by clicking the “Load in editor” link in the body of each exercise. Your progress on each exercise will be stored in browser local storage, so you can return to your code later (e.g. if your browser crashes, etc).

You can also do this tutorial by installing F* locally on your machine. F* is open source and cross-platform, and you can get binary packages for Windows, Linux, and MacOS X or compile F* from the source code on github using these instructions.

You can edit F* code using your favorite text editor, but for Emacs the community maintains fstar-mode.el, a sophisticated extension that adds special support for F*, including syntax highlighting, completion, type hints, navigation, documentation queries, and interactive development (in the style of CoqIDE or ProofGeneral). You can find more details about editor support on the F* wiki.

The code for the exercises in this tutorial and their solutions are in the F* repository on Github. For some exercises, you have to include additional libraries, as done by the provided Makefiles. To include libraries for the Emacs interactive mode follow the instructions here.

By default F* only verifies the input code, it does not execute it. To execute F* code one needs to extract it to OCaml or F# and then compile it using the OCaml or F# compiler. More details on executing F* code on the F* wiki.

1.1. Your first F* program: a simple model of access control

Let's get started by diving into a simple model of access control on files. Along the way, we'll see some basic concepts from functional programming in general and a couple of F*-specific features.

Let's say we want to model a simple access control discipline on files—certain files are readable or writable, whereas others may be unauthorized. We'd like to write a policy to describe the privileges on each file, and we'd like to write programs whose file accesses are checked against this policy, guaranteeing statically that an unauthorized file is never accessed mistakenly.

Our model of this scenario (which we'll make more realistic in later sections) proceeds in three easy steps.

1. Define the policy using simple pure functions.

2. Identify the security-sensitive primitives in the program and protect them with the policy.

3. Write the rest of the program, resting assured that the F* type-checker will verify statically that the policy-protected primitives are never improperly accessed.

1.1.1. Defining a policy

The syntax of F* is based closely on the syntax of OCaml and the non-light syntax of F#. Our F* program is made up of one module per file, and the body of the module contains a number of definitions, and optionally includes a ‘main’ expression.

Here are the first three definitions from the program:

type filename = string

(** [canWrite] is a function specifying whether a file [f] can be written *)
let canWrite (f:filename) = 
  match f with 
    | "demo/tempfile" -> true
    | _ -> false

(** [canRead] is also a function ... *)
let canRead (f:filename) = 
  canWrite f               (* writeable files are also readable *)
  || f="demo/README"       (* and so is demo/README *)

The first definition defines a type synonym: we'll use strings to model filenames.

After that, we define two boolean functions: canWrite and canRead: The canWrite function inspects its argument f using a pattern matching expression: it returns the boolean true when f equals "demo/tempfile" and false otherwise. The function canRead is similar—a file is readable if it is writable, or if it is the "demo/README" file.

1.1.2. Tying the policy to the file-access primitives

To enforce the policy, we need to connect the policy to the primitives in our programs that actually implement the file reading and writing operations.

F* provides a facility to specify interfaces to external modules that are implemented elsewhere. For example, operations that perform file input/output are implemented by the operating system and made available to F* programs via the underlying framework, e.g., .NET or OCaml. We can describe a simple interface provided by the framework as follows:

val read  : f:filename{canRead f}  -> ML string
let read f  = FStar.IO.print_string ("Dummy read of file " ^ f ^ "\n"); f

val write : f:filename{canWrite f} -> string -> ML unit
let write f s = FStar.IO.print_string ("Dummy write of string " ^ s ^ " to file " ^ f ^ "\n")

This interface provides two functions, read and write, which in a real setup would implement the corresponding operations on files. In our simplified example they just print things on screen.

• The type of read says that it is a function expecting a filename argument f for which canRead f evaluates to true and returning a string-typed result. Thus the type-checker prevents any calls to read for which the canRead predicate can't be statically proved for the argument.

• The type of write says that it is a function of two arguments: the first is a filename f, such that canWrite f evaluates to true; the second is a string, the data to be written to the file f. The write function returns unit, roughly analogous to the void type in C. The type unit has only a single value, written ().

The crucial bits of these declarations are, of course, the use of the canRead and canWrite functions in the signature, which allow us to connect the types of these security-sensitive functions to our policy.

1.1.3. Writing programs and verifying their security

Trying to check that a piece of code conforms to an access-control policy is a tedious and error-prone process. Even if every access is guarded by a security check, how can we make sure that each check is adequate? We can use F*'s type-checker to automate this kind of code review.

Here's some simple, untrusted client code. It defines some common file names, and then a function called staticChecking, which tries to read and write a few files.

let passwd : filename = "demo/password"
let readme : filename = "demo/README"
let tmp    : filename = "demo/tempfile"

val staticChecking : unit -> ML unit
let staticChecking () =
  let v1 = read tmp in
  let v2 = read readme in
  (* let v3 = read passwd in // invalid read, fails type-checking *)
  write tmp "hello!"
  (* ; write passwd "junk" // invalid write , fails type-checking *)

The type-checker ensures statically that this untrusted code complies with the security policy. The reads to tmp and readme, and the write to tmp are allowed by the policy, so the program successfully type-checks. On the other hand, if we uncomment the lines that read or write "junk" to the password file, the F* type-checker complains that the passwd file does not have the type f:filename{canRead f}, respectively f:filename{canWrite f}. For instance, if we uncomment the write we get the following error message:

.\Ex01a.fst(40,10-40,16): Subtyping check failed; 
expected type (f:Ex01a.filename{(Prims.b2t (Ex01a.canWrite f))}); 
got type Ex01a.filename

You'll understand more about what that message means as you work through this tutorial, but, for now, take it to mean that F* expected canWrite passwd to evaluate to true, which isn't the case.

The staticChecking function above illustrates how F* can be used to specify a security policy, and statically enforce complete and correct mediation of that policy via type-checking. We will now illustrate that checking of the policy doesn't have to happen all statically, but that the dynamic checks added by the programmer are taken into account by the type system. In particular we implement a checkedRead function that consults the policy and only performs the read if the policy allows it, otherwise it raises an exception.

exception InvalidRead
val checkedRead : filename -> ML string
let checkedRead f =
  if canRead f then read f else raise InvalidRead

Note that the type of checkRead imposes no condition on the the input file f. When the canRead f check succeeds the type-checker knows that the read f call is safe.

assume val checkedWrite : filename -> string -> ML unit

exception InvalidWrite
let checkedWrite f s =
  if canWrite f then write f s else raise InvalidWrite

You can use checkedRead and your checkedWrite to replace read and write in staticChecking, so that now even the accesses to passwd are well-typed.

let dynamicChecking () =
  let v1 = checkedRead tmp in
  let v2 = checkedRead readme in
  let v3 = checkedRead passwd in (* this raises exception *)
  checkedWrite tmp "hello!";
  checkedWrite passwd "junk" (* this raises exception *)

This is secure because checkedRead and checkedWrite defer to runtime the same checks that were previously performed at compile time by F*, and perform the IO actions only if those checks succeed.

2. Basics: Types and effects

You may not have noticed them all, but our first example already covers several distinctive features of F*. Let's take a closer look.

2.1. Refinement types

One distinctive feature of F* is its use of refinement types. We have already seen two uses of this feature, e.g, the type f:filename{canRead f} is a refinement of the type filename. It's a refinement because only a subset of the filename values have this type, namely those that satisfy the canRead predicate. The refinement in the type of write is similar. In traditional ML-like languages, such types are inexpressible.

In general, a refinement type in F* has the form x:t{phi(x)}, a refinement of the type t to those elements x that satisfy the formula phi(x). For now, you can think of phi(x) as any pure boolean valued expression. The full story is more general (3.5).

2.2. Inferred types and effects for computations

Although we didn't write down any types for functions like canRead or canWrite, F* (like other languages in the ML family) infers types for your program (if F* believes it is indeed type correct). However, what is inferred by F* is more precise than what can be expressed in ML. For instance, in addition to inferring a type, F* also infers the side-effects of an expression (e.g., exceptions, state, etc).

For instance, in ML (canRead "foo.txt") is inferred to have type bool. However, in F*, we infer (canRead "foo.txt" : Tot bool). This indicates that canRead "foo.txt" is a pure total expression, which always evaluates to a boolean. For that matter, any expression that is inferred to have type-and-effect Tot t, is guaranteed (provided the computer has enough resources) to evaluate to a t-typed result, without entering an infinite loop; reading or writing the program's state; throwing exceptions; performing input or output; or, having any other effect whatsoever.

On the other hand, an expression like (read "foo.txt") is inferred to have type-and-effect ML string, meaning that this term may have arbitrary effects (it may loop, do IO, throw exceptions, mutate the heap, etc.), but if it returns, it always returns a string. The effect name ML is chosen to represent the default, implicit effect in all ML programs.

Tot and ML are just two of the possible effects. Some others include:

• Dv, the effect of a computation that may diverge;
• ST, the effect of a computation that may diverge, read, write or allocate new references in the heap;
• Exn, the effect of a computation that may diverge or raise an exception.

The primitive effects {Tot, Dv, ST, Exn, ML} are arranged in a lattice, with Tot at the bottom (less than all the others), ML at the top (greater than all the others), and with ST unrelated to Exn. This means that a computation with a particular effect can be treated as having any other effect that is greater than it in the effect ordering—we call this feature sub-effecting.

In fact, you can configure F* with your own family of effects and effect ordering and have F* infer those effects for your programs—but that's more advanced and beyond the scope of this tutorial. (If curious you can check out this paper.)

From now on, we'll just refer to a type-and-effect pair (e.g. Tot int where Tot is the effect and int is the result type), as a computation type.

2.3. Function types

F* is a functional language, so functions are first-class values that are assigned function types. For instance, in ML the function is_positive testing whether an integer is positive is given type int -> bool, i.e. it is a function taking an integer argument and producing a boolean result. Similarly, a maximum function on integers max is given type int -> int -> int, i.e. it is a function taking two integers and producing an integer. Function types in F* are more precise and capture not just the types of the arguments and the result, but also the effect of the function's body. As such, every function value has a type of the form t1 -> ... -> tn -> E t, where t1 .. tn are the types of each of the arguments; E is the effect of its body; and t is the type of its result. (Note to the experts: We will generalize this to dependent functions and indexed effects progressively.) The pure functions above are given a type using effect Tot in F*:

val is_positive : int -> Tot bool
let is_positive i = i > 0

val max : int -> int -> Tot int
let max i1 i2 = if i1 > i2 then i1 else i2

Impure functions, like reading the contents of a file, are given corresponding effects:

val read : filename -> ML string

F* is a call-by-value functional language (like OCaml and F#, and unlike Haskell), so function arguments are fully evaluated to values before being passed to the function. Values have no (immediate) effect, thus the types of a function's arguments have no effect annotation. On the other hand, the body of a function may perform some non-trivial computation and so the result is always given both a type and an effect, as explained above.

Like many functional languages, function application has higher precedence than almost any other operation. Remembering this can help you keep track of when you do (and do not) need parentheses. For example, if, using the definitions for is_positive and max above, you try to write:

let x = is_positive max 1 2

you will get a type resolution failure, since F* will try to apply is_positive to the max function itself, and it will complain that is_positive expects an int argument, whereas max is a function that maps two integers to another integer. In this case, you need one set of parentheses around max:

let x = is_positive (max 1 2)

(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module Ex02a
//can-read-write-types

type filename = string

//val canWrite : unit (* write a correct and precise type here *)
let canWrite (f:filename) =
  match f with 
    | "demo/tempfile" -> true
    | _ -> false

//val canRead : unit (* write correct and precise type here *)
let canRead (f:filename) =
  canWrite f               (* writeable files are also readable *)
  || f="demo/README"       (* and so is this file *)

val canRead: filename -> Tot bool
val canWrite: filename -> Tot bool

2.3.1. The default effect is Tot

Since total functions are very commonly used in verified programs, writing Tot is optional in F*'s syntax. As such, filename -> bool is a shorthand for filename -> Tot bool. Nevertheless, we consider it good practice to annotate functions with their result effect, even when it is Tot.

For more details on the syntax of function types and definitions, in particular the rules for default effects, see this wiki page.

2.3.2. Computing functions

Skip this section on a first read, if you are new to functional programming.

Sometimes it is useful to return a function after performing some computation. For example, here is a function that makes a new counter, initializing it to init.

val new_counter: int -> St (unit -> St int)
let new_counter init =
  let c = ST.alloc init in
  fun () -> c := !c + 1; !c

F* can show that new_counter has type int -> St (unit -> St int), the type of a function that given an integer, may read, write or allocate references, and then returns a unit -> St unit function. Using sub-effecting, we can also write the type below and F* will check that new_counter has that type as well.

val new_counter: int -> ML (unit -> ML int)

Note, the type above, is not the same as int -> unit -> ML int. The latter is a shorthand for int -> Tot (unit -> ML int).

3. First proofs about functions on integers

Our first example on access control lists illustrated how F*'s type system can be used to automatically check useful security properties for us. But, before we can do more interesting security-related programming and verification, we will need to understand more about the basics of F*. We'll shift back a gear now and look at programming and proving properties of simple functions on integers.

3.1. Statically checked assertions

One way to prove properties about your code in F* is to write assertions.

let _ = assert (max 0 1 = 1)

Our first assertion is an obvious property about max. You may have seen a construct called assert in other languages—typically, it is used to check a property of your code at runtime, raising an assertion-failed exception if the asserted condition is not true.

In F*, assertions have no runtime significance. Instead, F* checks statically (i.e. before compiling your program) that the asserted condition is always true, and hence could never fail.

In this case, the proof that max 0 1 = 1 is fairly easy. Under the covers, F* translates the definition of max and the asserted property to a theorem prover called Z3, which then proves the property automatically.

We can assert and automatically check more general properties about max. For example:

let _ = assert (forall x y. max x y >= x
                && max x y >= y
                && (max x y = x || max x y = y))

3.2. Factorial and Fibonacci functions

Let's take a look at the factorial function: open FStar.Mul let rec factorial n = if n = 0 then 1 else n * (factorial (n - 1))

For a recursive function, without further annotation, F* attempts to automatically prove that the recursion always terminates. In the case of factorial above, F* attempts to prove that it has type int -> Tot int, and fails to do so because, factorial is actually not a total function on arbitrary integers! Think about factorial -1.

The factorial function is, however, a total function on non-negative integers. We can ask F* to check that this is indeed the case by writing:

val factorial: x:int{x>=0} -> Tot int

The line above says several things:

• factorial is a value (that's the 'val factorial' part)

• It is a function (that's the arrow type '->')

• It can only be applied to integers x that are greater than or equal to 0 (that's the refinement type 'x:int{x>=0}')

• When applied to x it always terminates, has no effects (the 'Tot' part), and returns an integer (the result type 'int')

Once we write this down, F* automatically proves that factorial satisfies all these properties. The main interesting bit to prove, of course, is that factorial x actually does terminate when x is non-negative. We'll get into the details of how this is done in section 5, but, for now, it suffices to know that in this case F* is able to prove that every recursive call is on a non-negative number that is strictly smaller than the argument of the previous call. Since this cannot go on forever (we'll eventually hit the base case 0), F* agrees with our claim about the type of factorial.

The type of non-negative integers (or natural numbers) is common enough that you can define an abbreviation for it (in fact, F* already does this for you in its standard prelude).

type nat = x:int{x>=0}

val factorial: x:int{x>=0} -> Tot int
let rec factorial n = 
  if n = 0 then 1 else n * (factorial (n - 1))

val factorial: int -> Dv int                  (* factorial may loop forever, but may return an integer *)
val factorial: nat -> Tot int                 (* total function on nat inputs *)
val factorial: nat -> Tot nat                 (* stronger result type *)
val factorial: nat -> Tot (y:int{y>=1})       (* even stronger result type *)

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

(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module Ex03b
//fibonacci


(* val fibonacci : int -> int *)
(* val fibonacci : int -> ML int (same as above) *)
(* val fibonacci : int -> Tot nat *)
(* val fibonacci : int -> Tot (y:int{y>=1}) *)
(* val fibonacci : x:int -> Tot (y:int{y>=1 /\ y >= x}) *)
(* val fibonacci : x:int -> Tot *)
(*   (y:int{y >= 1 /\ y >= x /\ (x>=3 ==> y>=2)}) *)
val fibonacci : int -> Tot (x:nat{x>0})
let rec fibonacci n =
  if n <= 1 then 1 else fibonacci (n - 1) + fibonacci (n - 2)

3.3. Lemmas

Let's say you wrote the factorial function and gave it the type (nat -> Tot nat). Later, you care about some other property about factorial, e.g., that if x > 2 then factorial x > x. One option is to revise the type you wrote for factorial and get F* to reprove that it has this type. But this isn't always feasible. What if you also wanted to prove that if x > 3 then factorial x > 2 * x: clearly, polluting the type of factorial with all these properties that you may or may not care about is impractical.

However, F* will allow you to write other functions (we call them lemmas) to prove more properties about factorial, after you've defined factorial and given it some generally useful type like nat -> Tot nat.

A lemma is a ghost total function that always returns the single unit value (). As such, computationally, lemmas are useless—they have no effect and always return the same value, so what's the point? The point is that the type of the value returned by the lemma carries some useful properties about your program.

As a first lemma about factorial, let's prove that it always returns a positive number.

val factorial_is_positive: x:nat -> GTot (u:unit{factorial x > 0})
let rec factorial_is_positive x =
  match x with
  | 0 -> ()
  | _ -> factorial_is_positive (x - 1)

The statement of the lemma is the type given to factorial_is_positive, a ghost total function on x:nat which returns a unit, but with the refinement that factorial x > 0. The next three lines define factorial_is_positive and proves the lemma using a proof by induction on x. The basic concept here is that by programming total functions, we can write proofs about other pure expressions. We'll discuss such proofs in detail in the remainder of this section.

3.3.1. Dependent function types

Let's start by looking a little closer at the statement of the lemma.

val factorial_is_positive: x:nat -> GTot (u:unit{factorial x > 0})

This is a dependent function type in F*. Why dependent? Well, the type of the result depends on the value of the parameter x:nat. For example, factorial_is_positive 0 has the type GTot (u:unit{factorial 0 > 0)), which is different from the type of factorial_is_positive 1.

Now that we've seen dependent functions, we can elaborate a bit more on the general form of function types:

Each of a function's formal parameters are named xi and each of these names is in scope to the right of the first arrow that follows it. The notation t[x1 ... xm] indicates that the variables x1 ... xm may appear free in t.

3.3.2. Some syntactic sugar for refinement types and lemmas

How shall we specify that factorial is strictly greater than its argument when its argument is greater than 2? Here's a first cut:

val factorial_is_greater_than_arg1: x:(y:nat{y > 2}) -> GTot (u:unit{factorial x > x})

This does the job, but the type of the function's argument is a bit clumsy, since we needed two names: y to restrict the domain to natural numbers greater than 2 and x to speak about the argument in the result type. This pattern is common enough that F* provides some syntactic sugar for it—we have seen it already in passing in the first type we gave to factorial. Using it, we can write the following type, which is equivalent to, but more concise than, the type above.

val factorial_is_greater_than_arg2: x:nat{x > 2} -> GTot (u:unit{factorial x > x})

Another bit of clumsiness that you have no doubt noticed is the result type of the lemmas which include a refinement of the unit type. To make this lighter, F* provides the Lemma keyword which can be used in place of the GTot effect.

For example, the type of factorial_is_greater_than_arg2 is equivalent to the type of factorial_is_greater_than_arg3 (below), which is just a little easier to read and write.

val factorial_is_greater_than_arg3: x:nat{x > 2} -> Lemma (factorial x > x)

We can also write it in the following way, when that's more convenient:

val factorial_is_greater_than_arg4: x:nat -> Lemma (requires (x > 2))
                                              (ensures (factorial x > x))

The formula after requires is the pre-condition of the function/lemma, while the one after ensures is its post-condition.

3.3.3. A simple lemma proved by induction, in detail

Now, let's look at a proof of factorial_is_greater_than_arg in detail. Here it is:

let rec factorial_is_greater_than_arg x =
  match x with
  | 3 -> ()
  | _ -> factorial_is_greater_than_arg (x - 1)

The proof is a recursive function (as indicated by the let rec); the function is defined by cases on x.

In the first case, the argument is 3; so, we need to prove that factorial 3 > 3. F* generates a proof obligation corresponding to this property and asks Z3 to see if it can prove it, given the definition of factorial that we provided earlier—Z3 figures out that by factorial 3 = 6 and, of course, 6 > 3, and the proof for this case is done. This is the base case of the induction.

The cases are taken in order, so if we reach the second case, then we know that the first case is inapplicable, i.e., in the second case, we know from the type for factorial_is_greater_than_arg that x:nat{x > 2}, and from the inapplicability of the previous case that x <> 3. In other words, the second case is the induction step and handles the proof when x > 3.

Informally, the proof in this case works by using the induction hypothesis, which gives us that

forall n, 2 < n < x ==> factorial n > n

and our goal is to prove factorial x > x. Or, equivalently, that x * factorial (x - 1) > x, knowing that factorial (x - 1) > x - 1; or that x*x - x > x—which is true for x > 3. Let's see how this works formally in F*.

When defining a total recursive function, the function being defined (factorial_is_greater_than_arg in this case) is available for use in the body of the definition, but only at a type that ensures that the recursive call will terminate. In this case, the type of factorial_is_greater_than_arg in the body of the definition is:

n:nat{2 < n && n < x} -> Lemma (factorial n > n)

This is, of course, exactly our induction hypothesis. By calling factorial_is_greater_than_arg (x - 1) in the second case, we, in effect, make use of the induction hypothesis to prove that factorial (x - 1) > x - 1, provided we can prove that 2 < x - 1 && x - 1 < x—we give this to Z3 to prove, which it can, since in this case we know that x > 3. Finally, we have to prove the goal factorial x > x from the x > 3 and the property we obtained from our use of the induction hypothesis: again, Z3 proves this easily.

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

val fibonacci_greater_than_arg : n:nat{n >= 2} -> Lemma (fibonacci n >= n)

let rec fibonacci_greater_than_arg n =
  match n with
  | 2 -> ()
  | _ -> fibonacci_greater_than_arg (n-1)

(*     
 Z3 proves the base case.
  
 The proof uses the induction hypothesis:
   forall x, 2 <= x < n ==> fibonacci x >= x
   
 Our goal is to prove that:
  fibonacci n >= n or equivalently fibonacci (n-1) + fibonacci (n-2) > n
  
 We make use of induction hypothesis to prove that 
  fibonacci (n-1) >= n-1
  
 For fibonacci (n-1) we use the property 
   forall x, fibonacci x > 1 
   
 This can be seen by giving fibonacci the stronger type
   val fibonacci : nat -> Tot (r:nat{r>=1})
   
 From this Z3 can proves the post condition 
*)

3.4. Admit

When constructing proofs it is often useful to assume parts of proofs, and focus on other parts. For instance, when doing case analysis we often want to know which cases are trivial and are automatically solved by F*, and which ones need manual work. We can achieve this by admitting all but one case, if F* can prove the lemma automatically, then the case is trivial. For this F* provides an admit function, that can be used as follows:

    let rec factorial_is_greater_than_arg x =
      match x with
      | 3 -> ()
      | _ -> admit()

Since type-checking this succeeds we know that the base case of the induction is trivially proved and need to focus our effort on the inductive case.

3.5. Under the hood: bool versus Type

You can probably skip this section on a first reading, if the title sounds mysterious to you. However, as you start to use quantified formulas in refinement types, you should make sure you understand this section.

We mentioned earlier that a refinement type has the form x:t{phi(x)}. In its primitive form, phi is in fact a type, a predicate on the value x:t. We allow you to use a boolean function in place of a type: under the covers, we implicitly coerce the boolean to a type, by adding the coercion

b2t (b:bool) : Type = (b == true)

The type '==' is the type constructor for the homogeneous equality predicate; it is different from '=‘, which is a boolean function comparing a pair of values (F* also has a separate constructor for heterogeneous equality, ’===').

The propositional connectives, /\, \/, and ~, for conjunction, disjunction and negations are type constructors. We also include ==> and <==> for single and bidirectional implication. In contrast, &&, ||, and not are boolean functions.

Often, because of the implicit conversion from bool to Type, you can almost ignore the distinction between the two. However, when you start to write refinement formulas with quantifiers, the distinction between the two will become apparent.

Both the universal quantifier forall and the existential quantifier exists, are only available in Type. When you mix refinements that include boolean function and the quantifiers, you need to use the propositional connectives. For example, the following formula is well-formed:

canRead e /\ forall x. canWrite x ==> canRead x

It is a shorthand for the following, more elaborate form:

b2t(canRead e) /\ forall x. b2t(canWrite x) ==> b2t(canRead x)

On the other hand, the following formula is not well-formed; F* will reject it:

canRead e && forall x. canWrite x ==> canRead x

The reason is that the quantifier is a type, whereas the && operator expects a boolean. While a boolean can be coerced to a type, there is no coercion in the other direction.

4. Simple inductive types

Here's the standard definition of (immutable) lists in F*.

type list 'a =
  | Nil  : list 'a
  | Cons : hd:'a -> tl:list 'a -> list 'a

We note some important conventions for the constructors of a data type in F*.

• Constructor names must begin with a capital letter.

• When not writing effects in constructor types, the default effect on the result is Tot. So, when we write Cons: 'a -> list 'a -> list 'a, F* desugars it to Cons: 'a -> Tot (list 'a -> Tot (list 'a)).

• Constructors can be curried. So, we usually define our inductive types as above so that we write Cons hd tl (curried) rather than Cons(hd,tl) (uncurried).

• Constructors can be partially applied, so Cons hd is legal and has type list 'a -> Tot (list 'a) when hd:'a.

The list type is defined in F*'s standard prelude and is available implicitly in all F* programs. We provide special (but standard) syntax for the list constructors:

• [] is Nil
• [v1; ...; vn] is Cons v1 ... (Cons vn Nil)
• hd :: tl is Cons hd tl.

You can always just write out the constructors like Nil and Cons explicitly, if you find that useful (e.g., to partially apply Cons).

4.1. Proofs about basic functions on lists

The usual functions on lists are programmed in F* just as in any other ML dialect. Here is the length function:

val length: list 'a -> Tot nat
let rec length l = match l with
  | [] -> 0
  | _ :: tl -> 1 + length tl

The type of length proves it is a total function on lists of 'a-typed values, returning a non-negative integer.

let rec append l1 l2 = match l1 with
  | [] -> l2
  | hd :: tl -> hd :: append tl l2

    l1:list 'a -> l2:list 'a -> Tot (l:list 'a{length l = length l1 + length l2})

val append:list 'a -> list 'a -> Tot (list 'a)

val append_len: l1:list 'a -> l2:list 'a
             -> Lemma (requires True)
                      (ensures (length (append l1 l2) = length l1 + length l2)))
let rec append_len l1 l2 = match l1 with
    | [] -> ()
    | hd::tl -> append_len tl l2

We wrote the type of the function append above using an ML-like type variable 'a to stand for an arbitrary type. Under the hood F* expands this out to something like this:

val append : #a:Type -> list a -> list a -> Tot (list a)
let rec append #a l1 l2 = match l1 with
  | [] -> l2
  | hd :: tl -> hd :: append #a tl l2

This exposes the fact that a is really just an implicit argument of append. The implicit argument a is preceded by the # symbol both in the type of append, where we say that a has type Type, and in the definition of append, which takes an extra a argument. When calling append recursively we have a choice, we can either pass a explicitly by preceding it with the # sign, or we can leave it out and the F* type-checker will infer it automatically. (Implicit arguments are further discussed in 8.3.1.)

We would like to define a function mem: x:'a -> l:list 'a -> Tot bool that decides whether x is present in a list l or not. However, not all types in F* have decidable equality, so in order to write mem we cannot quantify over arbitrary types, but only over those with decidable equality. Thus the following definition of mem has to use #a:Type{hasEq a} instead of #a:Type (hasEq a holds if a has decidable equality—that is, if there exists a function eq_a: a -> a -> Tot bool such that eq_a a1 a2 iff. a1 == a2). For convenience, the standard library provides eqtype as an abbreviation of a: Type{hasEq a}.

val mem: #a:eqtype -> a -> list a -> Tot bool
let rec mem #a x xs =
  match xs with
  | [] -> false
  | hd :: tl -> hd = x || mem x tl

val append_mem:  #a:eqtype -> l1:list a -> l2:list a -> x:a
        -> Lemma (mem x (append l1 l2) <==> mem x l1 || mem x l2)

let rec append_mem #a l1 l2 x =
  match l1 with
  | [] -> ()
  | hd::tl -> append_mem tl l2 x

(*
 Z3 proves the base case: mem x (append [] l) <==> mem x l2.
  
 The proof uses the induction hypothesis:
   tl << l1 ==> mem x (append tl l2) <==> mem x tl || mem x l2.
   
 Our goal is to prove that:
  mem x (append l1 l2) <==> mem x l1 || mem x l2) or equivalently 
  let hd::tl = l1 in mem x (hd::(append tl l2)) <==> hd=x || mem x tl || mem x l2.

 From this Z3 can proves the post condition. 
*)

4.2. To type intrinsically, or to prove lemmas?

As the previous exercises illustrate, you can prove properties either by enriching the type of a function or by writing a separate lemma about it—we call these the ‘intrinsic’ and ‘extrinsic’ styles, respectively. Which style to prefer is a matter of taste and convenience: generally useful properties are often good candidates for intrinsic specification (e.g, that length returns a nat); more specific properties are better stated and proven as lemmas. However, in some cases, as in the following example, it may be impossible to prove a property of a function directly in its type—you must resort to a lemma.

val reverse: list 'a -> Tot (list 'a)
let rec reverse = function
  | [] -> []
  | hd :: tl -> append (reverse tl) [hd]

Let's try proving that reversing a list twice is the identity function. It's possible to specify this property in the type of reverse using a refinement type.

val reverse: #a:Type -> f:(list a -> Tot (list a)){forall l. l == f (f l)}

However, F* refuses to accept this as a valid type for reverse: proving this property requires two separate inductions, neither of which F* can perform automatically.

Instead, one can use two lemmas to prove the property we care about. Here it is:

let snoc l h = append l [h]

val snoc_cons: l:list 'a -> h:'a -> Lemma (reverse (snoc l h) == h :: reverse l)
let rec snoc_cons l h = match l with
  | [] -> ()
  | hd :: tl -> snoc_cons tl h

val rev_involutive: l:list 'a -> Lemma (reverse (reverse l) == l)
let rec rev_involutive l = match l with
  | [] -> ()
  | hd :: tl ->
    // (1) [reverse (reverse tl) == tl]
    rev_involutive tl;
    // (2) [reverse (append (reverse tl) [hd]) == h :: reverse (reverse tl)]
    snoc_cons (reverse tl) hd
    // These two facts are enough for Z3 to prove the lemma:
    //   reverse (reverse (hd :: tl))
    //   =def= reverse (append (reverse tl) [hd])
    //   =(2)= hd :: reverse (reverse tl)
    //   =(1)= hd :: tl
    //   =def= l

In the Cons case of rev_involutive we are explicitly applying not just the induction hypothesis but also the snoc_cons lemma we proved above.

val rev_injective : l1:list 'a -> l2:list 'a
                -> Lemma (requires (reverse l1 == reverse l2))
                         (ensures  (l1 == l2))

val snoc_injective: l1:list 'a -> h1:'a -> l2:list 'a -> h2:'a
                 -> Lemma (requires (snoc l1 h1 == snoc l2 h2))
                          (ensures (l1 == l2 /\ h1 == h2))
let rec snoc_injective l1 h1 l2 h2 = match l1, l2 with
  | _::tl1, _::tl2 -> snoc_injective tl1 h1 tl2 h2
  | _ -> ()

val rev_injective1: l1:list 'a -> l2:list 'a
                -> Lemma (requires (reverse l1 == reverse l2))
                         (ensures  (l1 == l2)) (decreases l1)
let rec rev_injective1 l1 l2 =
  match l1,l2 with
  | h1::t1, h2::t2 ->
      // assert(reverse (h1::t1) = reverse (h2::t2));
      // assert(snoc (reverse t1) h1  = snoc (reverse t2) h2);
      snoc_injective (reverse t1) h1 (reverse t2) h2;
      // assert(reverse t1 = reverse t2 /\ h1 = h2);
      rev_injective1 t1 t2
      // assert(t1 = t2 /\ h1::t1 = h2::t2)
  | _, _ -> ()

val rev_injective2: l1:list 'a -> l2:list 'a
                -> Lemma (requires (reverse l1 == reverse l2))
                         (ensures  (l1 == l2))
let rev_injective2 #t l1 l2 = rev_involutive l1; rev_involutive l2

4.3. Higher-order functions on lists

4.3.1. Mapping

We can write higher-order functions on lists, i.e., functions taking other functions as arguments. Here is the familiar map:

let rec map f l = match l with
  | [] -> []
  | hd::tl -> f hd :: map f tl

It takes a function f and a list l and it applies f to each element in l producing a new list. More precisely map f [a1; ...; an] produces the list [f a1; ...; f an]. For example:

map (fun x -> x + 1) [0; 1; 2] = [1; 2; 3]

As usual, without any specification, F* will infer for map type ('a -> 'b) -> list 'a -> list 'b. Written explicitly, the type of map is ('a -> Tot 'b) -> Tot (list 'a -> Tot (list 'b)). Notice that the type of f also defaults to a function with Tot effect.

By adding a type annotation we can give a different type to map:

val map: ('a -> ML 'b) -> list 'a -> ML (list 'b)

This type is neither a subtype nor a supertype of the type F* inferred on its own (for example, the manual annotation above allows you to write map (fun x -> FStar.IO.print_any x) l, whereas the automatically inferred type does not.

No parametric polymorphism on effects: You might hope to give map a very general type, one that accepts a function with any effect E and returns a function with that same effect. This would require a kind of effect polymorphism, which F* does not support. This may lead to some code duplication. We plan to address this by allowing you to write more than one type for a value, an ad hoc overloading mechanism.

4.3.2. Finding

    type option 'a =
       | None : option 'a
       | Some : v:'a -> option 'a

    let rec find f l = match l with
      | [] -> None
      | hd :: tl -> if f hd then Some hd else find f tl

(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module Ex04e
//find

type option 'a =  
   | None : option 'a
   | Some : v:'a -> option 'a

(* The intrinsic style is more convenient in this case *)
val find : f:('a -> Tot bool) -> list 'a -> Tot (option (x:'a{f x}))
let rec find f l = match l with
  | [] -> None
  | hd :: tl -> if f hd then Some hd else find f tl

(* Extrinsically things are more verbose, since we are basically duplicating
   the structure of find in find_some. It's still not too bad. *)

val find' : #t:Type -> f:(t -> Tot bool) -> list t -> Tot (option t)
let rec find' #t f l = match l with
  | [] -> None
  | hd :: tl -> if f hd then Some hd else find' f tl

val find_some : f:('a -> Tot bool) -> xs:(list 'a) ->
    Lemma (None? (find' f xs) || f (Some?.v (find' f xs)))
let rec find_some f xs =
    match xs with
    | [] -> ()
    | x :: xs' -> find_some f xs'

(* [Some?.v] and [None?] are convenient ways to manipulate options.  They are
   described later in the tutorial.  Here's a more verbose way to achieve the
   same thing: *)

val find_some' : f:('a -> Tot bool) -> xs:(list 'a) ->
    Lemma (match find f xs with
           | None -> true
           | Some v -> f v)
let rec find_some' f xs =
    match xs with
    | [] -> ()
    | x :: xs' -> find_some' f xs'

fold_left f [b1; ...; bn] a = f (bn, ... (f b2 (f b1 a)))

val fold_left_cons_is_reverse: l:list 'a -> l':list 'a ->
      Lemma (fold_left Cons l l' == append (reverse l) l')

val fold_left: f:('b -> 'a -> Tot 'a) -> l:list 'b -> 'a -> Tot 'a
let rec fold_left f l a = match l with
  | Nil -> a
  | Cons hd tl -> fold_left f tl (f hd a)

val append_assoc : #a:Type -> l1:list a -> l2:list a -> l3: list a ->
  Lemma (append l1 (append l2 l3) == append (append l1 l2) l3)
let rec append_assoc #a l1 l2 l3 =
  match l1 with
  | [] -> ()
  | h1 :: t1 -> append_assoc t1 l2 l3

let rec fold_left_Cons_is_rev #a (l1 l2: list a) :
  Lemma (fold_left Cons l1 l2 == append (reverse l1) l2) =
  match l1 with
  | [] -> ()
  | h1 :: t1 ->
    // (1) [append (append (reverse t1) [h1]) l2
    //      == append (reverse t1) (append [h1] l2)]
    append_assoc (reverse t1) [h1] l2;
    // (2) [fold_left Cons t1 (h1 :: l2) = append (reverse t1) (h1 :: l2)]
    fold_left_Cons_is_rev t1 (h1 :: l2)
    // append (reverse l1) l2
    // =def= append (append (reverse t1) [h1]) l2
    // =(1)= append (reverse t1) (append [h1] l2)
    // =def= append (reverse t1) (h1 :: l2)
    // =(2)= fold_left Cons t1 (h1 :: l2)
    // =def= fold_left Cons l1 l2

4.4. Implicitly defined functions on inductive types

For each definition of an inductive type, F* automatically introduces a number of utility functions: for each constructor, we have a discriminator; and for each argument of each constructor, we have a projector. We describe these next, using the list type (repeated below) as a running example.

type list 'a =
  | Nil  : list 'a
  | Cons : hd:'a -> tl:list 'a -> list 'a

4.4.1. Discriminators

A discriminator is a boolean-valued total function that tests whether a term is the application of a particular constructor. For the list type, we have two discriminators that are automatically generated.

val Nil?: list 'a -> Tot bool
let Nil? xs = match xs with | [] -> true | _ -> false

val Cons?: list 'a -> Tot bool
let Cons? xs = match xs with | _ :: _ -> true | _ -> false

Identifiers like Nil? and Cons? cannot be defined by the user directly. They are reserved to be automatically generated by the compiler. So, the above code will not typecheck as written—it's only for illustration purposes.

4.4.2. Projectors

From the type of the Cons constructor, F* generates the following signatures:

val Cons?.hd : l:list 'a{Cons? l} -> Tot 'a
val Cons?.tl : l:list 'a{Cons? l} -> Tot (list 'a)

This indicates why the names hd and tl in the types of Cons are significant: they correspond to the names of the auto-generated projectors. If you don't name the arguments of a data constructor, F* will generate names automatically (although these names are derived from the position of the arguments and their form is unspecified; so, it's good practice to name the arguments yourself).

Again, names like Cons?.hd are reserved for internal use.

(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module Ex04g
//hd-tl

val hd : l:list 'a{Cons? l} -> Tot 'a
val tl : l:list 'a{Cons? l} -> Tot (list 'a)

(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module Ex04g
//hd-tl

val hd : l:list 'a{Cons? l} -> Tot 'a
let hd l =
  match l with
  | h :: t -> h

val tl : l:list 'a{Cons? l} -> Tot (list 'a)
let tl l =
  match l with
  | h :: t -> t

(* Write your code here *)

val nth : l:list 'a -> n:nat{n < length l} -> 'a
let rec nth l n =
  match l with
  | h :: t -> if n = 0 then h else nth t (n - 1)

(* Note how the solution above omits the [] case: that's because whenever you
   pattern match a term (to analyze it by cases), F\* insists on proving that you
   have handled all the cases. We call this the 'exhaustiveness check', and unlike
   in F\# or OCaml, it is implemented semantically. *)

4.5. Tuples and records

F* provides syntactic sugar for tuples. Under the covers, tuples are just inductive types: tuples of size 2–8 are defined in the standard prelude. (You can add to this, if you like.) Here's the definition of pairs from the prelude:

type tuple2 'a 'b =
  | MkTuple2: _1:'a -> _2:'b -> tuple2 'a 'b

You can write (5, 7) instead of MkTuple2 5 7, and give it the type (int * int) as a shorthand for tuple2 int int.

This notation generalizes to tuples of arbitrary size, so long as the corresponding tupleN data type is defined in the prelude.

F* also provides syntax for records, although internally records (like tuples) boil down to data types with a single constructor. Here's an example:

type triple 'a 'b 'c = { fst:'a; snd:'b; third:'c }
let f x = x.fst + x.snd + x.third

F* accepts this program, giving f the type (triple int int int -> Tot int).

This is equivalent to the following, more verbose, source program:

type triple 'a 'b 'c =
  | MkTriple: fst:'a -> snd:'b -> third:'c -> triple 'a 'b 'c

let f x = MkTriple?.fst x + MkTriple?.snd x + MkTriple?.third x

5. Proving termination

In F* every pure function is proved to terminate. The termination check used by F* is based on a semantic criterion, not syntactic conditions. We quickly sketch the basic structure of the F* termination check—you'll need to understand a bit of this in order to write more interesting programs.

5.1. A well-founded partial order on values

In order to prove a function terminating in F* one provides a measure: a pure expression depending on the function's arguments. F* checks that this measure strictly decreases on each recursive call. The measure for the arguments of the call is compared to the measure for the previous call according to a well-founded partial order on F* values. We write v1 << v2 when v1 precedes v2 in this order.

A relation R is a well-founded partial order on a set S if, and only if, R is a partial order on S and there are no infinite descending chains in S related by R. For example, taking S to be nat, the set of natural numbers, the integer ordering < is a well-founded partial order (in fact, it is a total order).

Since the measure strictly decreases on each recursive call, and there are no infinite descending chains, this guarantees that the function eventually stops making recursive calls, i.e., it terminates.

5.1.1. The precedes relation

1. The ordering on integers: Given i, j : nat, we have i << j <==> i < j.

   Note: Negative integers are not related by the << relation, which is only a partial order.

2. The subterm ordering on inductive types: For any value v = D v1 ... vn of an inductive type (where D is a constructor applied to arguments v1 to vn) we include vi << v, for all i. That is, the sub-terms of a well-typed constructed term precede the constructed term. (The exception to this rule is lex_t below).

3. The lexicographic ordering on lex_t, as described below.

5.1.2. Lexically ordered pairs and lists

Take a look at the classic function, ackermann:

val ackermann: m:nat -> n:nat -> Tot nat
let rec ackermann m n =
  if m=0 then n + 1
  else if n = 0 then ackermann (m - 1) 1
  else ackermann (m - 1) (ackermann m (n - 1))

Why does it terminate? At each recursive call, it is not the case that all the arguments are strictly less than the arguments at the previous call, e.g, in the second branch, n increases from 0 to 1. However, this function does in fact terminate, and F* proves that it does.

The reason is that although each argument does not decrease in every recursive call, when taken together, the ordered pair of arguments (m,n) does decrease according to a lexical ordering on pairs.

In its standard prelude, F* defines the following inductive type:

type lex_t =
  | LexTop  : lex_t
  | LexCons : #a:Type -> a -> lex_t -> lex_t

(The # sign marks the first argument as implicit, see 8.3.1.) This is a list of heterogenously typed elements.

The lexicographic ordering on lex_t is the following:

• LexCons v1 v2 << LexCons v1' v2', if and only if, either v1 << v1'; or v1===v1' and v2 << v2'.

• If v:lex_t and v <> LexTop, then v << LexTop.

We include the following syntactic sugar:

%[v1;...;vn] is shorthand for (LexCons v1 ... (LexCons vn LexTop))

5.2. A termination proof in detail

Suppose we are defining a function by recursion, using the following form:

val f: y1:t1 -> .. -> yn:tn -> Tot t
let rec f x1 .. xn = e

Usually, in ML, when type-checking e, the recursively bound function f is available for use in e at the type y1:t1 -> .. -> yn:tn -> Tot t, exactly the type written by the programmer. This type is, however, not sufficient to guarantee that an invocation of f does not trigger an infinite chain of recursive calls.

To prove termination (i.e., to rule out infinitely deep recursive calls), F* uses a different rule for type-checking recursive functions. The recursively bound name f is available for use in e, but only at the more restrictive type shown below:

   y1:t1
-> ...
-> yn:tn{%[y1;...;yn] << %[x1;...;xn]}
-> Tot t

That is, by default, F* requires the function's parameters to decrease according to the lexical ordering of the parameters (in the order in which they appear, excluding all function-typed parameters). (There is a way to override this default—see Section 5.2.2.)

Let's see how this works on a couple of examples.

5.2.1. Ackermann

F* can show automatically that the ackermann function

(* 1 *) let rec ackermann m n =
(* 2 *)   if m=0 then n + 1
(* 3 *)   else if n = 0 then ackermann (m - 1) 1
(* 4 *)   else ackermann (m - 1)
(* 5 *)                  (ackermann m (n - 1))

is terminating and has type:

ackermann : nat -> nat -> Tot nat

F* gives this function a default termination metric, so this expands out to:

ackermann : m:nat -> n:nat -> Tot nat (decreases %[m;n])

The decreases clause will be discussed in the next section. In this example it leads to the F* type-checker using the following more restrictive type for the recursive calls in the body of ackermann:

ackermann: m':nat
        -> n':nat{%[m';n'] << %[m;n]}
        -> Tot nat

At each of three recursive calls to ackermann, we need to prove not only that the arguments are non-negative, but that they precede the previous arguments according to the refinement formula above.

• For the call at line 3, we have to show that %[(m - 1);1] << %[m;n]. This works out, since m - 1 << m according to the integer ordering, and we can disregard the rest of the terms.

• The call at line 4 verifies for the same reason—the first argument decreases.

• For the call at line 5, we have to show that %[m; (n-1)] << %[m; n]. Here, the first elements of each pair are equal, so we look at the second element, and there n - 1 << n, and we're done.

5.2.2. Decreases clauses

Of course, sometimes you will need to override the default measure for recursive functions. If we just swap the arguments of the ackermann function the default measure no longer works and we need to add a decreases clause explicitly choosing a lexicographic ordering that first compares m and then n:

val ackermann_swap: n:nat -> m:nat -> Tot nat (decreases %[m;n])
let rec ackermann_swap n m =
   if m=0 then n + 1
   else if n = 0 then ackermann_swap 1 (m - 1)
   else ackermann_swap (ackermann_swap (n - 1) m)
                       (m - 1)

The optional decreases clause is a second argument to the Tot effect. It is, in general, a total expression over the arguments of the function.

val rev : l1:list 'a -> l2:list 'a -> Tot (list 'a) (decreases l2)
let rec rev l1 l2 =
  match l2 with
  | []     -> l1
  | hd :: tl -> rev (hd :: l1) tl

val rev_is_ok : l:list 'a -> Lemma (rev [] l = reverse l)

val append_assoc : xs:list 'a -> ys:list 'a -> zs:list 'a -> Lemma
      (ensures (append (append xs ys) zs = append xs (append ys zs)))
let rec append_assoc xs ys zs =
  match xs with
  | [] -> ()
  | x :: xs' -> append_assoc xs' ys zs

val rev_is_ok_aux : l1:list 'a -> l2:list 'a -> Lemma
      (ensures (rev l1 l2 = append (reverse l2) l1)) (decreases l2)
let rec rev_is_ok_aux l1 l2 =
  match l2 with
  | [] -> ()
  | hd :: tl  -> rev_is_ok_aux (hd :: l1) tl; append_assoc (reverse tl) [hd] l1

val append_nil : xs:list 'a -> Lemma
      (ensures (append xs [] = xs))
let rec append_nil xs =
  match xs with
  | [] -> ()
  | _ :: tl  -> append_nil tl

val rev_is_ok : l:list 'a -> Lemma (rev [] l = reverse l)
let rev_is_ok l = rev_is_ok_aux [] l; append_nil (reverse l)

val fib : nat -> nat -> n:nat -> Tot nat (decreases n)
let rec fib a b n =
  match n with
  | 0 -> a
  | _ -> fib b (a+b) (n-1)

val fib_is_ok : n:nat -> Lemma (fib 1 1 n = fibonacci n)

val fib_is_ok_aux : (n: nat) -> (k: nat) ->
  Lemma (fib (fibonacci k) (fibonacci (k + 1)) n == fibonacci (k + n))
let rec fib_is_ok_aux n k =
  if n = 0 then () else fib_is_ok_aux (n - 1) (k + 1)

val fib_is_ok : n:nat -> Lemma (fib 1 1 n = fibonacci n)
let fib_is_ok n = fib_is_ok_aux n 0

5.3. Mutually recursive functions

The same strategy for proving termination also works for mutually recursive functions. In the case of mutually recursive functions, the F* termination checker requires that all directly or mutually recursive calls decrease the termination metric of the called function. This is a quite strong requirement. Consider for instance the following example:

val foo : l:list int -> Tot int
val bar : l:list int -> Tot int
let rec foo l = match l with
    | [] -> 0
    | x :: xs -> bar xs
and bar l = foo l

This function is terminating because foo is always called (via bar) on a sub-list. The call from bar to foo is not on a smaller list though, and with the default metrics this example is rejected.

We can use a custom metric to convince F* that the two functions are terminating:

val foo : l:list int -> Tot int (decreases %[l;0])
val bar : l:list int -> Tot int (decreases %[l;1])

The metrics of foo and bar are both lexicographic tuples with the argument l in the first position and 0 or 1 in the second. The call from foo to bar decreases l, while the call from bar to foo keeps l the same, but decreases the second component from 1 to 0.

6. Putting the pieces together

We now look at two complete programs that exercise the various features we have learned about so far. In each case, there are some exercises to modify or generalize the programs.

6.1. Quicksort on lists

A canonical example for program verification is proving various sorting algorithms correct.

We'll start with lists of integers and describe some properties that we'd like to hold true of a sorting algorithm, starting with a function sorted, which decides when a list of integers is sorted in increasing order.

  val sorted: list int -> Tot bool
  let rec sorted l = match l with
      | [] -> true
      | [x] -> true
      | x :: y :: xs -> x <= y && sorted (y :: xs)

Given a sorting algorithm sort, we would like to prove the following property, where mem is the list membership function from the earlier exercise on lists (Section 4.1).

sorted (sort l) /\ ( forall i. mem i l <==> mem i (sort l) )

We will see below that this specification can still be improved.

6.1.1. Implementing Quicksort

Here's a simple implementation of the quicksort algorithm. It always picks the first element of the list as the pivot; partitions the rest of the list into those elements greater than or equal to the pivot, and the rest; recursive sorts the partitions; and slots the pivot in the middle before returning.

let rec sort l = match l with
  | [] -> []
  | pivot :: tl ->
    let hi, lo  = partition (fun x -> pivot <= x) tl in
    append (sort lo) (pivot :: sort hi)

val partition: ('a -> Tot bool) -> list 'a -> Tot (list 'a * list 'a)

val partition: ('a -> Tot bool) -> list 'a -> Tot (list 'a * list 'a)
let rec partition f = function
  | [] -> [], []
  | hd::tl ->
     let l1, l2 = partition f tl in
     if f hd
     then hd::l1, l2
     else l1, hd::l2

6.1.2. Specifying sort

We'll verify sort intrinsically, although we'll have to use some additional lemmas. Here's a first-cut at a specification. Try asking F* to prove it.

val sort0: l:list int -> Tot (m:list int{sorted m /\ (forall i. mem i l <==> mem i m) })

Unsurprisingly, it fails, on several counts:

1. We fail to prove the function total. On what grounds can we claim that each recursive call to sort is on a smaller argument? Intuitively, at each recursive call, the length of the list passed as an argument is strictly smaller, since it is a partition of tl. To express this, we'll need to add a decreases clause.

2. We fail to prove both the sortedness property and the membership property—we need some lemmas about partition and also about the sorted function.

Let's try again:

val sort: l:list int -> Tot (m:list int{sorted m
                                     /\ (forall i. mem i l <==> mem i m)})
                            (decreases (length l))

And here are a couple of lemmas about partition and sorted:

 val partition_lemma: f:('a -> Tot bool)
    -> l:list 'a
    -> Lemma (requires True)
             (ensures (
                  let l1, l2 = partition f l in
                  length l1 + length l2 = length l /\
                  (forall x. mem x l1 ==> f x) /\
                  (forall x. mem x l2 ==> not (f x)) /\
                  (forall x. mem x l = (mem x l1 || mem x l2))))
 let rec partition_lemma f l = match l with
   | [] -> ()
   | hd :: tl -> partition_lemma f tl

 val sorted_concat_lemma: l1:list int{sorted l1}
                       -> l2:list int{sorted l2}
                       -> pivot:int
                       -> Lemma (requires ((forall y. mem y l1 ==> not (pivot <= y))
                                        /\ (forall y. mem y l2 ==> pivot <= y)))
                                (ensures (sorted (append l1 (pivot :: l2))))
 let rec sorted_concat_lemma l1 l2 pivot = match l1 with
  | [] -> ()
  | hd :: tl -> sorted_concat_lemma tl l2 pivot

Finally, we also need a lemma about append and mem:

 val append_mem:  l1:list 'a
               -> l2:list 'a
               -> Lemma (requires True)
                        (ensures (forall a. mem a (append l1 l2) = (mem a l1 || mem a l2)))
 let rec append_mem l1 l2 = match l1 with
   | [] -> ()
   | hd :: tl -> append_mem tl l2

Armed with these lemmas, let's return to our implementation of quicksort. Unfortunately, with the lemmas as they are, we still can't prove our original implementation of quicksort correct. As we saw with our proofs of rev_injective (Section 4.1), we need to explicitly invoke our lemmas in order to use their properties. We'll be able to do better in a minute, but let's see how to modify sort by calling the lemmas to make the proof go through.

let cmp i j = i <= j
val sort_tweaked: l:list int -> Tot (m:list int{sorted m /\ (forall i. mem i l = mem i m)})
                                    (decreases (length l))
let rec sort_tweaked l = match l with
  | [] -> []
  | pivot :: tl ->
    let hi', lo' = partition (cmp pivot) tl in
    partition_lemma (cmp pivot) tl;
    let hi = sort_tweaked hi' in
    let lo = sort_tweaked lo' in
    append_mem lo (pivot :: hi);
    sorted_concat_lemma lo hi pivot;
    append lo (pivot :: hi)

That works, but it's pretty ugly. Not only did we have to pollute our implementation with calls to the lemmas, in order to make those calls, we had to further rewrite our code so that we could bind names for the arguments to those lemmas. We can do much better.

6.1.3. SMT Lemmas: Bridging the gap between intrinsic and extrinsic proofs

If only we had given partition and sorted richer intrinsic types, types that captured the properties that we proved using lemmas, we wouldn't have had to pollute our implementation of quicksort. This is a significant advantage of using the intrinsic proof style—every call of a function like partition (fun x -> pivot <= x) tl immediately carries all the properties that were proven intrinsically about the function.

However, polluting the type of a general-purpose function with a very application-specific type would also be awful. Consider enriching the type of sorted with the property proven by sorted_concat_lemma. The lemma is highly specialized for the quicksort algorithm, whereas sorted is a nice, general specification of sortedness that would work for insertion sort or merge sort, just as well. Polluting its type is a non-starter. So, it seems we are caught in a bind.

Wouldn't it be nice if there were some way to retroactively associate a property proven about a function f by a lemma directly with f, so that every application f x immediately carries the lemma properties? F* provides exactly such a mechanism, which gives a way to bridge the gap between extrinsic and intrinsic proofs.

Let's say we wrote the type of partition_lemma as below—the only difference is in the very last line, the addition of [SMTPat (partition f l)]. That line instructs F* and the SMT solver to associate with every occurrence of the term partition f l the property proven by the lemma.

val partition_lemma: f:('a -> Tot bool)
  -> l:list 'a
  -> Lemma (requires True)
           (ensures (
               let l1, l2 = partition f l in
               length l1 + length l2 = length l /\
               (forall x. mem x l1 ==> f x) /\
               (forall x. mem x l2 ==> not (f x)) /\
               (forall x. mem x l = (mem x l1 || mem x l2))))
           [SMTPat (partition f l)]

Likewise, here's a revised type for sorted_concat_lemma. This time, we instruct F* and the SMT solver to associate the lemma property only with very specific terms: just those that have the shape

sorted (append l1 (pivot :: l2))

The more specific a pattern you can provide, the more discriminating the SMT solver will be in applying lemmas, keeping your verification times acceptable.

val sorted_concat_lemma: l1:list int{sorted l1}
                      -> l2:list int{sorted l2}
                      -> pivot:int
                      -> Lemma (requires ((forall y. mem y l1 ==> not (pivot <= y))
                                       /\ (forall y. mem y l2 ==> pivot <= y)))
                               (ensures (sorted (append l1 (pivot :: l2))))
                         [SMTPat (sorted (append l1 (pivot :: l2)))]

Finally, we also revise the type for append_mem in the same way:

val append_mem:  l1:list 'a
              -> l2:list 'a
              -> Lemma (requires True)
                       (ensures (forall a. mem a (append l1 l2) = (mem a l1 || mem a l2)))
                       [SMTPat (append l1 l2)]
let rec append_mem l1 l2 = match l1 with
  | [] -> ()
  | hd :: tl -> append_mem tl l2

With these revised signatures, we can write sort just as we originally did, and give it the type we want. The SMT solver implicitly derives the properties it needs from the lemmas that we have provided.

let cmp i j = i <= j
val sort: l:list int -> Tot (m:list int{sorted m /\ (forall i. mem i l = mem i m)})
                            (decreases (length l))
let rec sort l = match l with
  | [] -> []
  | pivot :: tl ->
    let hi, lo = partition (cmp pivot) tl in
    append (sort lo) (pivot :: sort hi)

6.1.4. Exercises

(* Start from the code in the "Load in editor" link *)

(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module Ex06b
//quick-sort-poly

val mem: #t:eqtype -> t -> list t -> Tot bool
let rec mem #t a l = match l with
  | [] -> false
  | hd::tl -> hd=a || mem a tl


val append : list 'a -> list 'a -> Tot (list 'a)
let rec append l1 l2 = match l1 with
  | [] -> l2
  | hd :: tl -> hd :: append tl l2


val append_mem: #t:eqtype 
          -> l1:list t
              -> l2:list t
              -> Lemma (requires True)
                       (ensures (forall a. mem a (append l1 l2) = (mem a l1 || mem a l2)))
                       [SMTPat (append l1 l2)]
let rec append_mem #t l1 l2 = match l1 with
  | [] -> ()
  | hd::tl -> append_mem tl l2


val length: list 'a -> Tot nat
let rec length l = match l with
  | [] -> 0
  | _ :: tl -> 1 + length tl


(* Specification of sortedness according to some comparison function f *)
val sorted: ('a -> 'a -> Tot bool) -> list 'a -> Tot bool
let rec sorted f l = match l with
    | [] -> true
    | [x] -> true
    | x::y::xs -> f x y && sorted f (y::xs)


val partition: ('a -> Tot bool) -> list 'a -> Tot (list 'a * list 'a)
let rec partition f = function
  | [] -> [], []
  | hd::tl ->
     let l1, l2 = partition f tl in
     if f hd
     then hd::l1, l2
     else l1, hd::l2

val partition_lemma: #t:eqtype -> f:(t -> Tot bool)
   -> l:list t
   -> Lemma (requires True)
           (ensures (
             let l1, l2 = partition f l in
              length l1 + length l2 = length l /\
              (forall x. mem x l1 ==> f x) /\
              (forall x. mem x l2 ==> not (f x)) /\
              (forall x. mem x l = (mem x l1 || mem x l2))))
            [SMTPat (partition f l)]
let rec partition_lemma #t f l = match l with
    | [] -> ()
    | hd::tl -> partition_lemma f tl


(* Defining a new predicate symbol *)
type total_order (a:eqtype) (f: (a -> a -> Tot bool)) =
    (forall a. f a a)                                           (* reflexivity   *)
    /\ (forall a1 a2. (f a1 a2 /\ a1<>a2)  <==> not (f a2 a1))  (* anti-symmetry *)
    /\ (forall a1 a2 a3. f a1 a2 /\ f a2 a3 ==> f a1 a3)        (* transitivity  *)


val sorted_concat_lemma: #t:eqtype 
              -> f:(t -> t -> Tot bool)
                      -> l1:list t{sorted f l1}
                      -> l2:list t{sorted f l2}
                      -> pivot:t
                      -> Lemma (requires (total_order t f
                                       /\ (forall y. mem y l1 ==> not (f pivot y))
                                       /\ (forall y. mem y l2 ==> f pivot y)))
                               (ensures (sorted f (append l1 (pivot::l2))))
                               [SMTPat (sorted f (append l1 (pivot::l2)))]
let rec sorted_concat_lemma #t f l1 l2 pivot = match l1 with
    | [] -> ()
    | hd::tl -> sorted_concat_lemma f tl l2 pivot


val sort: #t:eqtype -> f:(t -> t -> Tot bool){total_order t f}
       -> l:list t
       -> Tot (m:list t{sorted f m /\ (forall i. mem i l = mem i m)})
              (decreases (length l))

let rec sort #t f l = match l with
  | [] -> []
  | pivot::tl ->
    let hi, lo = partition (f pivot) tl in
    let m = append (sort f lo) (pivot::sort f hi) in
    assert (forall i. mem i (pivot :: sort f hi) = mem i (append [pivot] (sort f hi)));
    m