Verified programming in F*
A tutorial
The F* Team
MSR, MSR-Inria, Inria

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 Haskellwe provide a quick review of basic concepts if you're a little rusty. If you feel you need more background, there are many useful resources freely available on the web, e.g., TryF#, F# for fun and profit, Introduction to Caml, or the Real World OCaml book.

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 Emacs, Atom, and Vim have extensions that add special support for F*, including syntax highlighting and interactive development. More details on editor support on the F* wiki.

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 filescertain files are readable or writable, whereas others may be inaccessible. We'd like to write a policy to describe the privileges on each file, and we'd like to write programs whose file access patterns are checked against this policy, guaranteeing statically that an inaccessible 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.
  1. Identify the security-sensitive primitives in the program and protect them with the policy.
  1. 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 OCaml syntax 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 or not 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 this file *)

code/exercises/Ex01a.fstLoad in editor

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="demo/tempfile" and false otherwise. The function canRead is similara 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")

code/exercises/Ex01a.fstLoad in editor

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 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  = "demo/password"
let readme  = "demo/README"
let tmp     = "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 *)

code/exercises/Ex01a.fstLoad in editor

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 Prims.string

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

code/exercises/Ex01a.fstLoad in editor

Please note that the type of checkRead imposes no condition on the the input file f. When the ACLs.canRead f check succeeds the type-checker knows that the FileIO.read f is safe.

Exercise 1a:
Write a function called checkedWrite that takes a filename f and a string s as argument, checks the policy to make sure the file f is writable, and only if that is the case writes s to f. If the file is not writable your checkedWrite should raise an exception. As for checkedRead, your checkedRead should have no preconditions.

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

code/exercises/Ex01a.fstLoad in editor

exercise answer

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

code/solutions/Ex01a.fstLoad in editor

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 *)

code/exercises/Ex01a.fstLoad in editor

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:

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 orderingwe 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 programsbut 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 and Coq), 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.

Exercise 2a:
As you could see above, we use val to ask F* to check that a definition has a certain expected type. Write down the expected types for canRead and canWrite from 1.1.1 and ask F* to check it for you.

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 *)

code/exercises/Ex02a.fstLoad in editor

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

code/solutions/Ex02a.fstLoad in editor

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.

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

F* infers 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. You can write down this type and have F* check it; or, using sub-effecting, you can 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 -> int. The latter is a shorthand for int -> Tot (unit -> Tot 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 a = assert (max 0 1 = 1)

Our first assertion is an obvious property about max. You may have seen a construct called assert in other languagestypically, 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* tries to prove statically (i.e., before compiling your program) that the asserted condition is true, and hence, could never fail even if it were tested at runtime.

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 a more general property about max. For example:

let a = 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:

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.

Remark. F*'s int type represents unbounded mathematical integers.

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:

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}

Exercise 3a:
What are some other correct types you can give to factorial? Try writing them and see if F* agrees with you. Try describing in words what each of those types mean.

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

code/exercises/Ex03a.fstLoad in editor

exercise answer

There are many possible correct types for factorial. Here are a few:

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 *)

code/solutions/Ex03a.fstLoad in editor

Exercise 3b:
Give several types for the fibonacci function.

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

code/exercises/Ex03b.fstLoad in editor

exercise answer
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)

code/solutions/Ex03b.fstLoad in editor

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 uselessthey 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.

Remark. In F* an expression being ghost (computationally irrelevant) is an effect. The effect GTot in the type of factorial_is_positive indicates that it is a ghost, total function.

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:

x1:t1 -> ... -> xn:tn[x1 ... xn-1] -> E t[x1 ... xn]

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 itwe 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 earlierZ3 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 > xwhich 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 < xwe 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.

Exercise 3c:
Prove the following property for the fibonacci function:

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)

code/exercises/Ex03c.fstLoad in editor

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

code/solutions/Ex03c.fstLoad in editor

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 equality predicate; it is different from =, which is a boolean function comparing a pair of values. Additionally, == is heterogeneous: you can speak about equality between any pair of values, regardless of their type. In contrast, = is homogeneous.

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 && 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*.

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:

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.

Exercise 4a:
Here's the append function that concatenates two lists.

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

code/exercises/Ex04a.fstLoad in editor

Give append a type that proves it always returns a list whose length is the sum of the lengths of its arguments.

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

code/solutions/Ex04a.fstLoad in editor

Exercise 4b:
Give append the weak type below, then prove the same property as in the previous exercise using a lemma.

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

code/exercises/Ex04b.fstLoad in editor

exercise answer
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

code/solutions/Ex04b.fstLoad in editor

Exercise 4c:
Define a function mem: x:'a -> l:list 'a -> Tot bool that decides whether x is present in the l or not, then prove it satisfies the following property:

val append_mem:  l1:list 'a -> l2:list 'a -> a:'a
        -> Lemma (ensures (mem a (append l1 l2)  <==>  mem a l1 || mem a l2))

code/exercises/Ex04c.fstLoad in editor

exercise answer

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

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

code/solutions/Ex04c.fstLoad in editor

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 itwe 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 typeyou 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: 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 -> rev_involutive tl; snoc_cons (reverse tl) hd

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.

Exercise 4d:
Prove that reverse is injective, i.e.,

val snoc_injective: #t:eqtype -> l1:list t -> h1:t -> l2:list t -> h2:t
                 -> Lemma (requires (snoc l1 h1 = snoc l2 h2))
                          (ensures (l1 = l2 && h1 = h2))

code/exercises/Ex04d.fstLoad in editor

exercise answer

Perhaps you did it like this:

val snoc_injective: #t:eqtype -> l1:list t -> h1:t -> l2:list t -> h2:t
                 -> Lemma (requires (snoc l1 h1 = snoc l2 h2))
                          (ensures (l1 = l2 && h1 = h2))
let rec snoc_injective #t l1 h1 l2 h2 = match l1, l2 with
  | _::tl1, _::tl2 -> snoc_injective tl1 h1 tl2 h2
  | _ -> ()

val rev_injective1: #t:eqtype -> l1:list t -> l2:list t
                -> Lemma (requires (reverse l1 = reverse l2))
                         (ensures  (l1 = l2)) (decreases l1)
let rec rev_injective1 #t 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)
  | _, _ -> ()

code/solutions/Ex04d.fstLoad in editor

That's quite a tedious proof, isn't it. Here's a simpler proof.

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

code/solutions/Ex04d.fstLoad in editor

The rev_injective2 proof is based on the idea that every involutive function is injective. We've already proven that reverse is involutive. So, we invoke our lemma, once for l1 and once for l2. This gives to the SMT solver the information that reverse (reverse l1) = l1 and reverse (reverse l2) = l2, which suffices to complete the proof. As usual, when structuring proofs, lemmas are your friends!

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 -> ML 'b) -> Tot (list 'a -> ML (list 'b)). Notice that the type of f also defaults to a function with ML effect.

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

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

This type is neither a subtype nor a supertype of the type F* inferred on its own.

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

Exercise 4e:

We define a find function that given a boolean function f and a list l returns the first element in l for which f holds. If no element is found find returns None; for this we use the usual option type (shown below and available in F*'s standard prelude).

    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

code/exercises/Ex04e.fstLoad in editor

Prove that if find returns Some x then f x = true. Is it better to do this intrinsically or extrinsically? Do it both ways.

exercise answer
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'

code/solutions/Ex04e.fstLoad in editor

Exercise 4f:
Define the fold_left function on lists, so that

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

Prove that (fold_left Cons l [] = reverse l). (The proof is a level harder from what we've done so far)

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

code/exercises/Ex04f.fstLoad in editor

exercise answer
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_cons: #t:eqtype -> l:list t -> hd:t -> tl:list t ->
                 Lemma (append l (Cons hd tl) = append (append l (Cons hd Nil)) (tl))
let rec append_cons #t l hd tl = match l with
  | Nil -> ()
  | Cons hd' tl' ->
    append_cons tl' hd tl


val snoc_append: #t:eqtype -> l:list t -> h:t -> Lemma (snoc l h = append l (Cons h Nil))
let rec snoc_append #t l h = match l with
  | Nil -> ()
  | Cons hd tl ->
    snoc_append tl h

val reverse_append: #t:eqtype -> tl:list t -> hd:t ->
                  Lemma (reverse (Cons hd tl) = append (reverse tl) (Cons hd Nil))
let reverse_append #t tl hd = snoc_append (reverse tl) hd


val fold_left_cons_is_reverse: #t:eqtype -> l:list t -> l':list t ->
                             Lemma (fold_left Cons l l' = append (reverse l) l')
let rec fold_left_cons_is_reverse #t l l' = match l with
  | Nil -> ()
  | Cons hd tl ->
    fold_left_cons_is_reverse tl (Cons hd l');
    append_cons (reverse tl) hd l';
    reverse_append tl hd

code/solutions/Ex04f.fstLoad in editor

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:

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

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

4.4.2. Projectors

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

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

(here Cons.hd is a qualified name)

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).

Exercise 4g:
Write functions (call them hd and tl) whose types match those of Cons.hd and Cons.tl.

module Ex04g
//hd-tl

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

code/exercises/Ex04g.fstLoad in editor

exercise answer
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

code/solutions/Ex04g.fstLoad in editor

Exercise 4h:
Write a function that returns the nth element of a list. Give a type that ensures it is total.

(* Write your code here *)

code/exercises/Ex04h.fstLoad in editor

exercise answer
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)

code/solutions/Ex04h.fstLoad in editor

4.5. Tuples and records

F* provides syntactic sugar for tuples. Under the covers, tuples are just inductive types: tuples of size 28 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 checkyou'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 D v1 ... vn of an inductive type (where D is a constructor applied to arguments v1 to vn) we include v_i << 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

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.)

The lexicographic ordering on lex_t is the following:

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 defaultsee 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.

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.

Exercise 5a:
Here is a more efficient (tail-recursive) variant of the list reverse 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

code/exercises/Ex05a.fstLoad in editor

Prove the following lemma showing the correctness of this efficient implementation with respect to the previous simple implementation:

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

code/exercises/Ex05a.fstLoad in editor

exercise answer
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)

code/solutions/Ex05a.fstLoad in editor

Exercise 5b:
(Challenge!) Here is a more efficient (tail-recursive) variant of the Fibonacci function.

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)

code/exercises/Ex05b.fstLoad in editor

Prove the following lemma showing the correctness of this efficient implementation with respect to the previous simple implementation:

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

code/exercises/Ex05b.fstLoad in editor

exercise answer
val fib_is_ok_aux : i:nat -> n:nat{i<=n} ->
      Tot (u:unit{fib (fibonacci i) (fibonacci (i+1)) (n-i) = fibonacci n})
      (decreases (n-i))
let rec fib_is_ok_aux i n =
  if i=n then ()
  else fib_is_ok_aux (i+1) n

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

code/solutions/Ex05b.fstLoad in editor

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)

Exercise 6a:
Write the partition function and prove it total.

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

code/exercises/Ex06a.fstLoad in editor

exercise answer

The following definition is included in F*'s list library.

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

code/solutions/Ex06a.fstLoad in editor

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.
  1. We fail to prove both the sortedness property and the membership propertywe 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 ((length (fst (partition f l))
                      + length (snd (partition f l)) = length l
                  /\ (forall x. mem x (fst (partition f l)) ==> f x)
                  /\ (forall x. mem x (snd (partition f l)) ==> not (f x))
                  /\ (forall x. mem x l = (mem x (fst (partition f l))
                                        || mem x (snd (partition f l)))))))
 let rec partition_lemma f l = match l with
   | [] -> ()
   | hd::tl -> partition_lemma f tl

Remark. The repeated sub-terms like fst (partition f l) in specifications call for a let-binding construct in types. We will see how to do that in a later sectiononce we have introduced some additional machinery.

 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 universally quantified variant of the append_mem lemma presented in a previous exercise:

 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 lets 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 styleevery 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 provides a way to bridge the gap between extrinsic and intrinsic proofs.

Let's say we wrote the type of partition_lemma as belowthe 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 ((length (fst (partition f l))
                    + length (snd (partition f l)) = length l
                /\ (forall x. mem x (fst (partition f l)) ==> f x)
                /\ (forall x. mem x (snd (partition f l)) ==> not (f x))
                /\ (forall x. mem x l = (mem x (fst (partition f l))
                                      || mem x (snd (partition f l)))))))
                     [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 11 (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

Remark. Use SMTPat with care! If you specify a bad pattern, you will get very unpredictable performance from the verification engine. To understand the details behind SMTPat, you should read up a bit on patterns (aka triggers) for quantifiers in SMT solvers.

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

Exercise 6b:
Starting from this implementation (given below), generalize sort so that it works on lists with an arbitrary element type, instead of just lists of integers. Prove it correct.

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

code/exercises/Ex06b.fstLoad in editor

exercise answer
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 ((length (fst (partition f l))
                     + length (snd (partition f l)) = length l
                  /\ (forall x. mem x (fst (partition f l)) ==> f x)
                  /\ (forall x. mem x (snd (partition f l)) ==> not (f x))
                  /\ (forall x. mem x l = (mem x (fst (partition f l))
                                        || mem x (snd (partition f l)))))))
            [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
    append (sort f lo) (pivot::sort f hi)

code/solutions/Ex06b.fstLoad in editor

Exercise 6c:
Our specification for sort is incomplete. Why? Can you write a variation of sort that has the same specification as the one above, but discards some elements of the list?

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

code/exercises/Ex06b.fstLoad in editor

exercise answer

The specification does not ensure that the resulting list is a permutation of the initial list: it could discard or repeat some elements.

module Ex06c


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


(* append now duplicates the elements of the first list *)
val append : list 'a -> list 'a -> Tot (list 'a)
let rec append l1 l2 = match l1 with
  | [] -> l2
  | hd :: tl -> hd :: 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


val sorted: list int -> Tot bool
let rec sorted l = match l with
    | [] -> true
    | [x] -> true
    | x::y::xs -> x <= y && sorted (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 ((length (fst (partition f l)) + length (snd (partition f l)) = length l
                                  /\ (forall x. mem x (fst (partition f l)) ==> f x)
                                  /\ (forall x. mem x (snd (partition f l)) ==> not (f x))
                                  /\ (forall x. mem x l = (mem x (fst (partition f l)) || mem x (snd (partition f l)))))))
                            [SMTPat (partition f l)]
let rec partition_lemma #t 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))))
                               [SMTPat (sorted (append l1 (pivot::l2)))]
let rec sorted_concat_lemma l1 l2 pivot = match l1 with
    | [] -> ()
    | hd::tl -> sorted_concat_lemma tl l2 pivot


type match_head (l1:list int) (l2:list int) =
  (l1 = [] /\ l2 = []) \/
  (exists h t1 t2. l1 = h::t1 /\ l2 = h::t2)

val dedup: l:list int{sorted l} -> Tot (l2:list int{sorted l2 /\ (forall i. mem i l = mem i l2) /\ match_head l l2})
  let rec dedup l =
    match l with
    | [] -> []
    | [x] -> [x]
    | h::h2::t ->
      if h = h2 then dedup (h2::t)
      else  h::dedup (h2::t)


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))
//#set-options "--z3timeout 100"
let rec sort l = match l with
  | [] -> []
  | pivot::tl ->
    let hi, lo = partition (cmp pivot) tl in
    let l' = append (sort lo) (pivot::sort hi) in
    dedup l'

code/solutions/Ex06c.fstLoad in editor

Exercise 6d:
Fix the specification to ensure that sort cannot discard any elements in the list. Prove that sort meets the specification.

(* Start from either the problem or the solution of exercise 6b *)

code/exercises/Ex06b.fstLoad in editor

exercise answer
module Ex06d


(* Instead of a Boolean check that an element belongs to a list, count
the number of occurrences of an element in a list *)
val count : #t:eqtype -> t -> list t -> Tot nat
let rec count #t (x:t) (l:list t) = match l with
  | hd::tl -> if hd=x then 1 + count x tl else count x tl
  | [] -> 0


let mem #t x l = count #t x l > 0


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_count: #t:eqtype -> l:list t -> m:list t
               -> Lemma (requires True)
                        (ensures (forall x. count x (append l m) = (count x l + count x m)))
let rec append_count #t l m = match l with
  | [] -> ()
  | hd::tl -> append_count tl m


val append_mem: #t:eqtype -> l:list t -> m:list t
               -> Lemma (requires True)
                        (ensures (forall x. mem x (append l m) = (mem x l || mem x m)))
let append_mem #t l m = append_count l m


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 ((length (fst (partition f l)) + length (snd (partition f l)) = length l
                                  /\ (forall x. mem x (fst (partition f l)) ==> f x)
                                  /\ (forall x. mem x (snd (partition f l)) ==> not (f x))
                                  /\ (forall x. mem x l = (mem x (fst (partition f l)) || mem x (snd (partition f l))))
                                  /\ (forall x. count x l = (count x (fst (partition f l)) + count x (snd (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: #a:eqtype
                      -> f:(a -> a -> Tot bool)
                      -> l1:list a{sorted f l1}
                      -> l2:list a{sorted f l2}
                      -> pivot:a
                      -> Lemma (requires (total_order a 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))))

let rec sorted_concat_lemma #a 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) /\ (forall i. count i l = count i m)})
              (decreases (length l))
let rec sort #t f l = match l with
  | [] -> []
  | pivot::tl ->
    let hi, lo = partition (f pivot) tl in
    partition_lemma (f pivot) tl;
    let lo' = sort f lo in
    let hi' = sort f hi in
    append_count lo' (pivot::hi');
    append_mem lo' (pivot::hi');
    sorted_concat_lemma f lo' hi' pivot;
    append lo' (pivot::hi')

code/solutions/Ex06d.fstLoad in editor

Exercise 6e:
Implement insertion sort and prove the same properties.

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

code/exercises/Ex06e.fstLoad in editor

exercise answer
module Ex06e
//insertion-sort

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

(* Definition of the [mem] function *)
val mem: int -> list int -> Tot bool
let rec mem a l = match l with
  | [] -> false
  | hd::tl -> hd=a || mem a tl

(* A lemma to help Z3 *)
val sorted_smaller: x:int
                ->  y:int
                ->  l:list int
                ->  Lemma (requires (sorted (x::l) /\ mem y l))
                          (ensures (x <= y))
                          [SMTPat (sorted (x::l)); SMTPat (mem y l)]
let rec sorted_smaller x y l = match l with
    | [] -> ()
    | z::zs -> if z=y then () else sorted_smaller x y zs

(* Insertion function *)
val insert : i:int -> l:list int{sorted l} -> Tot (m:list int{sorted m /\ (forall x. mem x m <==> x==i \/ mem x l)})
let rec insert i l = match l with
  | [] -> [i]
  | hd::tl ->
     if i <= hd then
       i::l
     else
       (* Solver implicitly uses the lemma: sorted_smaller hd (Cons.hd i_tl) tl *)
       hd::(insert i tl)

(* Insertion sort *)
val sort : l:list int -> Tot (m:list int{sorted m /\ (forall x. mem x l == mem x m)})
let rec sort l = match l with
    | [] -> []
    | x::xs -> insert x (sort xs)

code/solutions/Ex06e.fstLoad in editor

7. Case study: simply-typed lambda-calculus

We now look at a larger case study: proving the soundness of a type-checker for the simply-typed $\lambda$-calculus (STLC). If you're not familiar with STLC, you can have a look at the Software Foundations book for a gentle introduction given by the textual explanations (you can ignore the Coq parts there). The formalization and proof here closely follows the one in Software Foundations. Our proofs are, however, shorter and much more readable than Coq proofs.

7.1. Syntax

We represent STLC types by the F* inductive datatype ty.

type ty =
  | TBool  : ty
  | TArrow : ty -> ty -> ty

We consider Booleans as the only base type (TBool). Function types are represented by the TArrow constructor taking two type arguments. For instance we write TArrow TBool TBool for the type of functions taking a Boolean argument and returning a Boolean result. This would be written as bool -> bool in F* syntax, and $\mathsf{bool} \to \mathsf{bool}$ in paper notation.

We represent the expressions of STLC by the datatype exp.

type exp =
  | EVar   : int -> exp
  | EApp   : exp -> exp -> exp
  | EAbs   : int -> ty -> exp -> exp
  | ETrue  : exp
  | EFalse : exp
  | EIf    : exp -> exp -> exp -> exp

Variables are represented as integer “names” decorated by the constructor EVar. Variables are “bound” by lambda abstractions (EAbs). For instance the identity function on Booleans is written EAbs 0 TBool (EVar 0). In paper notation one would write this function as $(\lambda x:\mathsf{bool}.~x)$. The type annotation on the argument (TBool) allows for very simple type-checking. We are not considering type inference here, to keep things simple. The expression that applies the identity function to the ETrue constant is written

EApp (EAbs 0 TBool (EVar 0)) ETrue

(in paper notation $(\lambda x:\mathsf{bool}.~x)~\mathsf{true}$).

The language also has a conditional construct (if-then-else). For instance, the Boolean “not” function can be written as

EAbs 0 TBool (EIf (EVar 0) EFalse ETrue)

(in paper notation $\lambda x:\mathsf{bool}.~\mathsf{if }~x~\mathsf{ then~false~else~true}$).

7.2. Operational semantics

We define a standard small-step call-by-value interpreter for STLC. The final result of successfully evaluating an expression is called a value. We postulate that functions and the Boolean constants are values by defining is_value, a boolean predicate on expressions (a total function):

val is_value : exp -> Tot bool
let is_value e =
  match e with
  | EAbs _ _ _
  | ETrue
  | EFalse     -> true
  | _          -> false

The EAbs, ETrue, and EFalse cases share the same right-hand-side (true), which is a way to prevent duplication in definitions.

In order to give a semantics to function applications we define a function subst x e e' that substitutes x with e in e':

val subst : int -> exp -> exp -> Tot exp
let rec subst x e e' =
  match e' with
  | EVar x' -> if x = x' then e else e'
  | EAbs x' t e1 ->
      EAbs x' t (if x = x' then e1 else (subst x e e1))
  | EApp e1 e2 -> EApp (subst x e e1) (subst x e e2)
  | ETrue -> ETrue
  | EFalse -> EFalse
  | EIf e1 e2 e3 -> EIf (subst x e e1) (subst x e e2) (subst x e e3)

We traverse the expression and when we reach a variable (EVar x') we check whether this is the variable x we want to substitute, and if it is we replace it by e. For lambda abstractions (EAbs x' t e1) we only substitute inside the body e1 if x and x' are different; if they are the same we leave the body unchanged. The reason for this is that the x in e1 is bound by the abstraction: it is a new, local name that just happens to be spelled the same as some global name x. The global x is no longer accessible in this scope, since it is shadowed by the local x. The other cases are straightforward.

Note for experts: Because we will only reduce closed expressions, where all variables are bound by previous lambdas, we will ever only substitute closed expressions (closed values in fact), and this naive definition of substitution is good enough. Substitution would become trickier to define or the representation of variables would have to change if we were considering the case where e, the expression replacing a variable in some other expression, may itself contain free variables.

Given the definition of values and of substitution we can now define a small-step interpreter, as a function step that takes an expression e and it either returns the expression to which e reduces in a single step, or it returns None in case of an error (all errors in this language are typing errors, and will be prevented statically by the type system).

val step : exp -> Tot (option exp)
  let rec step e =
  match e with
  | EApp e1 e2 ->
      if is_value e1 then
        if is_value e2 then
          match e1 with
          | EAbs x t e' -> Some (subst x e2 e')
          | _           -> None
        else
          match (step e2) with
          | Some e2' -> Some (EApp e1 e2')
          | None     -> None
      else
        (match (step e1) with
        | Some e1' -> Some (EApp e1' e2)
        | None     -> None)
  | EIf e1 e2 e3 ->
      if is_value e1 then
        match e1 with
        | ETrue   -> Some e2
        | EFalse  -> Some e3
        | _       -> None
      else
        (match (step e1) with
        | Some e1' -> Some (EIf e1' e2 e3)
        | None     -> None)
  | _ -> None

We execute an application expression EApp e1 e2 in multiple steps by first reducing e1 to a value, then reducing e2 to a value, and if additionally e1 is an abstraction EAbs x t e' we continue by substituting the formal argument x by the actual argument e2. If not we signal a dynamic typing error (a non-functional value is applied to arguments) by returning None. For EIf e1 e2 e3 we first reduce the guard e1: if the guard reduces to true then we continue with e2, if the guard reduces to false we continue with e3, and if the guard reduces to something else (e.g. a function) we report a dynamic typing error. The None -> None cases simply propagate errors to the top level.

assert (step (EApp (EAbs 0 TBool (EVar 0))) ETrue)) = Some ETrue)
assert (step (EApp ETrue ETrue) = None)

7.3. Type-checker

In order to assign a type to a term, we need to know what assumptions we should make about the types of its free variables. So typing happens with respect to a typing environmenta mapping from the variables in scope to their types. We represent such partial maps as functions taking an integer variable name and returning an optional type:

type env = int -> Tot (option ty)

We start type-checking closed terms in the empty environment, i.e. initially no variables are in scope.

val empty : env
let empty _ = None

When we move under a binder we extend the typing environment environment.

val extend : env -> int -> ty -> Tot env
let extend g x t x' = if x = x' then Some t else g x'

For instance we type-check EAbs x t e in typing environment g by first type-checking the body e in the environment extend g x t.

The type-checker is a total function taking an environment g and an expression e and producing either the type of e or None if e is not well-typed.

val typing : env -> exp -> Tot (option ty)
let rec typing g e =
  match e with
  | EVar x -> g x
  | EAbs x t e1 ->
      (match typing (extend g x t) e1 with
      | Some t' -> Some (TArrow t t')
      | None    -> None)
  | EApp e1 e2 ->
      (match typing g e1, typing g e2 with
      | Some (TArrow t11 t12), Some t2 -> if t11 = t2 then Some t12 else None
      | _                    , _       -> None)
  | ETrue  -> Some TBool
  | EFalse -> Some TBool
  | EIf e1 e2 e3 ->
      (match typing g e1, typing g e2, typing g e3 with
      | Some TBool, Some t2, Some t3 -> if t2 = t3 then Some t2 else None
      | _         , _      , _       -> None)

Variables are simply looked up in the environment. For abstractions EAbs x t e1 we type-check the body e1 under the environment extend g x t, as explained above. If that succeeds and produces a type t', then the whole abstraction is given type TArrow t t'. For applications EApp e1 e2 we type-check e1 and e2 separately, and if e1 has a function type TArrow t11 t12 and e2 has type t11, then the whole application has type t12. ETrue and EFalse have type TBool. For conditionals, we require that the guard has type TBool and the two branches have the same type, which is also the type of the conditional.

7.4. Soundness proof

We prove progress and preservation for STLC. The progress theorem tells us that closed, well-typed terms do not produce (immediate) dynamic typing errors: either a well-typed term is a value, or it can take an evaluation step. The proof is a relatively straightforward induction.

val progress : e:exp -> Lemma
      (requires (is_Some (typing empty e)))
      (ensures (is_value e \/ (is_Some (step e))))
let rec progress e =
  match e with
  | EApp e1 e2 -> progress e1; progress e2
  | EIf e1 e2 e3 -> progress e1; progress e2; progress e3
  | _ -> ()

Variables are not well-typed in the empty environment, so the theorem holds vacuously for variables. Boolean constants and abstractions are values, so the theorem holds trivially for these. All these simple cases are proved automatically by F*. For the remaining cases we need to use the induction hypothesis, but otherwise the proofs are fully automated. Under the hood F* and Z3 are doing quite a bit of work though.

In case e = (EApp e1 e2) F* and Z3 automate the following intuitive argument: We case split on the first instance of the induction hypothesis (is_value e1 \/ (is_Some (step e1))).

The intuitive proof of the EIf case is similar.

The preservation theorem (sometimes also called “subject reduction”) states that when a well-typed expression takes a step, the result is a well-typed expression of the same type. In order to show preservation we need to prove a couple of auxiliary results for reasoning about variables and substitution.

The case for function application has to reason about “beta reduction” steps, i.e. substituting the formal argument of a function with an actual value. To see that this step preserves typing, we need to know that the substitution itself does. So we prove a substitution lemma, stating that substituting a (closed) term v for a variable x in an expression e preserves the type of e. The tricky cases in the substitution proof are the ones for variables and for function abstractions. In both cases, we discover that we need to take an expression e that has been shown to be well-typed in some context g and consider the same expression e in a slightly different context g'. For this we prove a context invariance lemma, showing that typing is preserved under “inessential changes” to the context gin particular, changes that do not affect any of the free variables of the expression. For this, we need a definition of the free variables of an expressioni.e., the variables occurring in the expression that are not bound by an abstraction.

A variable x appears free in e if e contains some occurrence of x that is not under an abstraction labeled x:

val appears_free_in : x:int -> e:exp -> Tot bool
let rec appears_free_in x e =
  match e with
  | EVar y -> x = y
  | EApp e1 e2 -> appears_free_in x e1 || appears_free_in x e2
  | EAbs y _ e1 -> x <> y && appears_free_in x e1
  | EIf e1 e2 e3 ->
      appears_free_in x e1 || appears_free_in x e2 || appears_free_in x e3
  | ETrue
  | EFalse -> false

We also need a technical lemma connecting free variables and typing contexts. If a variable x appears free in an expression e, and if we know that e is well typed in context g, then it must be the case that g assigns some type to x.

val free_in_context : x:int -> e:exp -> g:env -> Lemma
      (requires (is_Some (typing g e)))
      (ensures (appears_free_in x e ==> is_Some (g x)))
let rec free_in_context x e g =
  match e with
  | EVar _
  | ETrue
  | EFalse -> ()
  | EAbs y t e1 -> free_in_context x e1 (extend g y t)
  | EApp e1 e2 -> free_in_context x e1 g; free_in_context x e2 g
  | EIf e1 e2 e3 -> free_in_context x e1 g;
                    free_in_context x e2 g; free_in_context x e3 g

The proof is a straightforward induction. As a corollary for g=empty we obtain that expressions typable in the empty environment have no free variables.

val typable_empty_closed : x:int -> e:exp -> Lemma
      (requires (is_Some (typing empty e)))
      (ensures (not(appears_free_in x e)))
      [SMTPat (appears_free_in x e)]
let typable_empty_closed x e = free_in_context x e empty

The quantifier pattern [SMTPat (appears_free_in x e)] signals F* that it should feed this lemma to the SMT solver using this pattern.

Sometimes, we know that typing g e = Some t, and we will need to replace g by an “equivalent” context g'. We still need to define formally when two environments are equivalent. A natural definition is extensional equivalence of functions:

opaque logic type Equal (g1:env) (g2:env) =
                 (forall (x:int). g1 x = g2 x)

According to this definition two environments are equivalent if have the same domain and they map all variables in the domain to the same type. We remark Equal in particular and logical formulas in general are “types” in F*, thus the different syntax for this definition.

The context invariance lemma uses in fact a weaker variant of this equivalence in which the two environments only need to agree on the variables that appear free in an expression e:

opaque logic type EqualE (e:exp) (g1:env) (g2:env) =
                 (forall (x:int). appears_free_in x e ==> g1 x = g2 x)

The context invariance lemma is then easily proved by induction:

val context_invariance : e:exp -> g:env -> g':env
                     -> Lemma
                          (requires (EqualE e g g'))
                          (ensures (typing g e == typing g' e))
let rec context_invariance e g g' =
  match e with
  | EAbs x t e1 ->
     context_invariance e1 (extend g x t) (extend g' x t)

  | EApp e1 e2 ->
     context_invariance e1 g g';
     context_invariance e2 g g'

  | EIf e1 e2 e3 ->
     context_invariance e1 g g';
     context_invariance e2 g g';
     context_invariance e3 g g'

  | _ -> ()

Because Equal is a stronger relation than EqualE we obtain the same property for Equal:

val typing_extensional : g:env -> g':env -> e:exp -> Lemma
                           (requires (Equal g g'))
                           (ensures (typing g e == typing g' e))
let typing_extensional g g' e = context_invariance e g g'

We can use these results to show the following substitution lemma:

val substitution_preserves_typing : x:int -> e:exp -> v:exp ->
      g:env -> Lemma
        (requires ( is_Some (typing empty v) /\
              is_Some (typing (extend g x (Some.v (typing empty v))) e)))
        (ensures (is_Some (typing empty v) /\
                  typing g (subst x v e) ==
                  typing (extend g x (Some.v (typing empty v))) e))
let rec substitution_preserves_typing x e v g =
  let Some t_x = typing empty v in
  let gx = extend g x t_x in
  match e with
  | ETrue -> ()
  | EFalse -> ()
  | EVar y ->
     if x=y
     then context_invariance v empty g (* uses lemma typable_empty_closed *)
     else context_invariance e gx g

  | EApp e1 e2 ->
     substitution_preserves_typing x e1 v g;
     substitution_preserves_typing x e2 v g

  | EIf e1 e2 e3 ->
     substitution_preserves_typing x e1 v g;
     substitution_preserves_typing x e2 v g;
     substitution_preserves_typing x e3 v g

  | EAbs y t_y e1 ->
     let gxy = extend gx y t_y in
     let gy = extend g y t_y in
     if x=y
     then typing_extensional gxy gy e1
     else
       (let gyx = extend gy x t_x in
        typing_extensional gxy gyx e1;
        substitution_preserves_typing x e1 v gy)

The proof proceeds by induction on the expression e; we give the intuition of the two most interesting cases:

We now have the tools we need to prove preservation: if a closed expression e has type t and takes an evaluation step to e', then e' is also a closed expression with type t. In other words, the small-step evaluation relation preserves types.

val preservation : e:exp -> Lemma
        (requires(is_Some (typing empty e) /\ is_Some (step e) ))
        (ensures(is_Some (step e) /\
                 typing empty (Some.v (step e)) == typing empty e))
let rec preservation e =
  match e with
  | EApp e1 e2 ->
     if is_value e1
     then (if is_value e2
           then let EAbs x _ ebody = e1 in
                substitution_preserves_typing x ebody e2 empty
           else preservation e2)
     else preservation e1

  | EIf e1 _ _ ->
      if not (is_value e1) then preservation e1

We only have two cases to consider, since only applications and conditionals can take successful execution steps. The case for e = EIf e1 e2 e3 is simple: either e1 is a value and thus the conditional reduces to e2 or e3 which by the typing hypothesis also have type t, or e1 takes a successful step and we can apply the induction hypothesis. We use the Some.v projector for options with the following type:

  Some.v : x:(option 'a){is_Some x} -> Tot 'a

which requires F* to prove that indeed e1 can take a step; this is immediate since we know that the whole conditional takes a step and we know that e1 is not a value.

The case for e = EApp e1 e2 is a bit more complex. If e1 steps or if e1 is a value and e2 steps then we just apply the induction hypothesis. If both e1 and e2 are values it needs to be the case that e1 is an abstraction EAbs x targ ebody and step e = subst x e2 ebody. From the typing assumption we have typing (extend empty x tags) ebody = Some t and typing empty e2 = Some targ, so we can use the substitution lemma to obtain that typing empty (subst x e2 ebody) = Some t, which concludes the proof.

7.5. Exercises for STLC

Exercise 7a:
Define a typed_step step function that takes a well-typed expression e that is not a value and produces the expression to which e steps. Give typed_step the following strong type (basically this type captures both progress and preservation):

  val typed_step : e:exp{is_Some (typing empty e) /\ not(is_value e)} ->
                   Tot (e':exp{typing empty e' = typing empty e})

code/exercises/Ex07a.fstLoad in editor

(Hint: the most direct solution to this exercise fits on one line)

exercise answer
    let typed_step e = progress e; preservation e; Some.v (step e)

code/solutions/Ex07a.fstLoad in editor

Exercise 7b:
To add pairs to this formal development we add the following to the definition of types, expressions, values, substitution, and step:

type ty =
  ...
  | TPair : ty -> ty -> ty

type exp =
  ...
  | EPair  : exp -> exp -> exp
  | EFst   : exp -> exp
  | ESnd   : exp -> exp

code/exercises/Ex07b.fstLoad in editor

(note the extra rec in is_value below!)

let rec is_value e =
  match e with
  ...
  | EPair e1 e2 -> is_value e1 && is_value e2

let rec subst x e e' =
  match e' with
  ...
  | EPair e1 e2 -> EPair (subst x e e1) (subst x e e2)
  | EFst e1 -> EFst (subst x e e1)
  | ESnd e1 -> ESnd (subst x e e1)

let rec step e =
  ...
  | EPair e1 e2 ->
      if is_value e1 then
        if is_value e2 then None
        else
          (match (step e2) with
          | Some e2' -> Some (EPair e1 e2')
          | None     -> None)
      else
        (match (step e1) with
        | Some e1' -> Some (EPair e1' e2)
        | None     -> None)
  | EFst e1 ->
      if is_value e1 then
        (match e1 with
        | EPair v1 v2 -> Some v1
        | _           -> None)
      else
        (match (step e1) with
        | Some e1' -> Some (EFst e1')
        | None     -> None)
  | ESnd e1 ->
      if is_value e1 then
        (match e1 with
        | EPair v1 v2 -> Some v2
        | _           -> None)
      else
        (match (step e1) with
        | Some e1' -> Some (ESnd e1')
        | None     -> None)

code/exercises/Ex07b.fstLoad in editor

Add cases to typing for the new constructs and fix all the proofs.

exercise answer

We extend the typing and appears_free_in functions with cases for EPair, EFst, and ESnd:

val typing : env -> exp -> Tot (option ty)
let rec typing g e =
...
  | EPair e1 e2 ->
      (match typing g e1, typing g e2 with
      | Some t1, Some t2 -> Some (TPair t1 t2)
      | _      , _       -> None)
  | EFst e1 ->
      (match typing g e1 with
      | Some (TPair t1 t2) -> Some t1
      | _                  -> None)
  | ESnd e1 ->
      (match typing g e1 with
      | Some (TPair t1 t2) -> Some t2
      | _                  -> None)

val appears_free_in : x:int -> e:exp -> Tot bool
...
  | EPair e1 e2 -> appears_free_in x e1 || appears_free_in x e2
  | EFst e1 -> appears_free_in x e1
  | ESnd e1 -> appears_free_in x e1

code/solutions/Ex07b.fstLoad in editor

The proofs of the lemmas are also easy to extend by just calling the induction hypothesis:

val free_in_context : x:int -> e:exp -> g:env -> Lemma
      (requires (is_Some (typing g e)))
      (ensures (appears_free_in x e ==> is_Some (g x)))
let rec free_in_context x e g =
...
  | EPair e1 e2 -> free_in_context x e1 g; free_in_context x e2 g
  | EFst e1
  | ESnd e1 -> free_in_context x e1 g

val context_invariance : e:exp -> g:env -> g':env
                     -> Lemma
                          (requires (EqualE e g g'))
                          (ensures (typing g e == typing g' e))
let rec context_invariance e g g' =
...
| EPair e1 e2 ->
     context_invariance e1 g g';
     context_invariance e2 g g'

  | EFst e1
  | ESnd e1 -> context_invariance e1 g g'

val substitution_preserves_typing : x:int -> e:exp -> v:exp ->
      g:env{is_Some (typing empty v) &&
            is_Some (typing (extend g x (Some.v (typing empty v))) e)} ->
      Tot (u:unit{typing g (subst x v e) ==
                  typing (extend g x (Some.v (typing empty v))) e})
let rec substitution_preserves_typing x e v g =
...
  | EPair e1 e2 ->
     (substitution_preserves_typing x e1 v g;
      substitution_preserves_typing x e2 v g)

  | EFst e1
  | ESnd e1 ->
      substitution_preserves_typing x e1 v g

code/solutions/Ex07b.fstLoad in editor

As for the other cases, the preservation proof when e = EPair e1 e2 follows the structure of the step function. If e1 is not a value then it further evaluates, so we apply the induction hypothesis to e1. If e1 is a value, then since we know that the pair evaluates, it must be the case that e2 is not a value and further evaluates, so we apply the induction hypothesis to it. The cases for EFst and ESnd are similar.

val preservation : e:exp{is_Some (typing empty e) /\ is_Some (step e)} ->
      Tot (u:unit{typing empty (Some.v (step e)) == typing empty e})
let rec preservation e =
...
  | EPair e1 e2 ->
      (match is_value e1, is_value e2 with
      | false, _     -> preservation e1
      | true , false -> preservation e2)

  | EFst e1
  | ESnd e1 ->
      if not (is_value e1) then preservation e1

code/solutions/Ex07b.fstLoad in editor

Exercise 7c:
We want to add a let construct to this formal development. We add the following to the definition of expressions:

type exp =
  ...
  | ELet  : int -> exp -> exp -> exp

code/exercises/Ex07c.fstLoad in editor

Add cases for ELet to all definitions and proofs.

Load answer in editor

Exercise 7d:
Define a big-step interpreter for STLC as a recursive function eval that given a well-typed expression e either produces the well-typed value v to which e evaluates or it diverges if the evaluation of e loops. Give eval the following strong type ensuring that v has the same type as e (basically this type captures both progress and preservation):

  val eval : e:exp{is_Some (typing empty e)} ->
             Dv (v:exp{is_value v && typing empty v = typing empty e})

code/exercises/Ex07d.fstLoad in editor

The Dv effect is that of potentially divergent computations. We cannot mark this as Tot since a priori STLC computations could loop, and it is hard to prove that well-typed ones don't, while defining an interpreter.

exercise answer

Here is a solution that only uses typed_step (suggested by Santiago Zanella):

val eval : e:exp{is_Some (typing empty e)} ->
           Dv (v:exp{is_value v && typing empty v = typing empty e})
let rec eval e =
  if is_value e then e
  else eval (typed_step e)

code/solutions/Ex07d.fstLoad in editor

or using the progress and preservation lemmas instead of typed_step (suggested by Guido Martinez):

val eval : e:exp{is_Some (typing empty e)} ->
  Dv (v:exp{is_value v && typing empty v = typing empty e})
let rec eval e = match step e with
  | None -> progress e; e
  | Some e' -> preservation e; eval e'

Here is another solution that only uses the substitution lemma:

val eval' : e:exp{is_Some (typing empty e)} ->
            Dv (v:exp{is_value v && typing empty v = typing empty e})
let rec eval' e =
  let Some t = typing empty e in
  match e with
  | EApp e1 e2 ->
     (let EAbs x _ e' = eval' e1 in
      let v = eval' e2 in
      substitution_preserves_typing x e' v empty;
      eval' (subst x v e'))
  | EAbs _ _ _
  | ETrue
  | EFalse     -> e
  | EIf e1 e2 e3 ->
     (match eval' e1 with
      | ETrue  -> eval' e2
      | EFalse -> eval' e3)
  | EPair e1 e2 -> EPair (eval' e1) (eval' e2)
  | EFst e1 ->
     let EPair v1 _ = eval' e1 in v1
  | ESnd e1 ->
     let EPair _ v2 = eval' e1 in v2
  | ELet x e1 e2 ->
     (let v = eval' e1 in
      substitution_preserves_typing x e2 v empty;
      eval' (subst x v e2))

code/solutions/Ex07d.fstLoad in editor

8. Higher kinds, indexed types, implicit arguments, and type-level functions

So far, we have mostly programmed total functions and give them specifications using rich types. Under the covers, F* has a second level of checking at work to ensure that the specifications that you write are also meaningfulthis is F*'s kind system. Before moving on to more advanced F* features, you'll have to understand the kind system a little. In short, just as types describe properties of programs, kinds describe properties of types.

8.1. Type: The type of types

The basic construct in the kind system is the constant Type, which is the basic type of a type. For example, just as we say that 0 : int (zero has type int), we also say int : Type (int has kind Type), bool : Type, nat : Type etc.

8.2. Arrow kinds

Beyond the base types, consider types like list int, list bool etc. These are also types, of course, and in F* list int : Type and list bool : Type. But, what about the unapplied type constructor listit's not a Type on its own; it only produces a Type when applied to a Type. In that sense, list is type constructor. To describe this, just as we use the -> type constructor to describe functions at the level of programs, we use the -> kind constructor to describe functions at the level of types. As such, we write list : Type -> Type, meaning that it produces a Type when applied to a Type.

8.3. Indexed types and implicit arguments

Beyond inductive types like list, F* also supports inductive type families, or GADTs. For example, here is one definition of a vector, a length-indexed list.

type vector (a:Type) : nat -> Type =
   | Nil :  vector a 0
   | Cons : hd:a -> n:nat -> tl:vector a n -> vector a (n + 1)

Here, we define a type constructor vector (a:Type) : nat -> Type, which takes two arguments: it produces a Type when applied first to a Type and then to a nat.

The point is to illustrate that just as functions at the level of programs may take either type- or term-arguments, types themselves can take either types or pure expressions as arguments.

8.3.1. Implicit arguments

When writing functions over terms with indexed types, it is convenient to mark some arguments as implicit, asking the type-checker to infer them rather than having to provide them manually.

For example, the type of a function that reverses a vector can be written as follows:

val reverse_vector: #a:Type -> #n:nat -> vector a n -> Tot (vector a n)

This indicates that reverse_vector expects three arguments, but the # sign mark the first two arguments as implicit. Given a term v : vector t m, simply writing reverse_vector v will type-check as vector t minternally, F* elaborates the function call to reverse_vector #t #m v, instantiating the two implicit arguments automatically. To view what F* inferred, you can provide the --print_implicits argument to the compiler, which will cause all implicitly inferred arguments to be shown in any message from the compiler. Alternatively, you can write reverse_vector #t #m v yourself to force the choice of implicit arguments manually. Applying this to the Cons constructor's n argument we get:

type vector (a:Type) : nat -> Type =
   | Nil :  vector a 0
   | Cons : hd:a -> #n:nat -> tl:vector a n -> vector a (n + 1)

With this, given v: vector int m, we can write Cons 0 v to build a vector int (m + 1).

When you write a type like 'a -> M t wp (note the “ticked” variable 'a), this is simply syntactic sugar for #a:Type -> a -> M t wp, with every occurrence of 'a replaced by a in M t wpin other words, the “ticked” type variable is an implicit type argument. So the signature below is equivalent to the previous one.

val reverse_vector' : #n:nat -> vector 'a n -> Tot (vector 'a n)

8.4. Dependent kind arrows and type function

Even some of the built-in type constructors can be given kinds. Consider the refinement type constructor: _:_{_}, whose instances include types we've seen before, like x:int{x >= 0}, which is the type nat, of course. With less syntactic sugar, you can view the type x:int{phi(x)} as the application of a type constructor refinement to two arguments int and a refinement formula fun x -> phi(x). As discussed in Section 3.5, the formula phi(x) is itself a Type. Thus, the kind of the refinement constructor is a:Type -> (a -> Type) -> Type, meaning it takes two arguments; first, a type a; then a second argument, a predicate on a (whose kind depends on a); and then builds a Type.

The type fun x -> phi(x) is type function, a lambda abstraction at the level of types, which when applied to a particular value, say, 0, reduces as usual to phi(0).

8.5. Kind abbreviations

F* allows top-level declarations to define abbreviations for kinds. For example, one can write:

kind Predicate (a:Type) = a -> Type

Now, the kind Predicate a is an abbreviation for a -> Type.

9. Specifying effects

F* provides a mechanism to define new effects. As mentioned earlier, the system is already configured with several basic effects, including non-termination, state and exceptions. In this section, we look briefly at how effects are defined, using the PURE and STATE effects for illustration.

On a first reading, you may wish to skip this section and proceed directly to the next chapter.

9.1. Background: Generating compact verification conditions

Type inference in F* is based on a weakest pre-condition calculus for higher order programs. For every term e, F* computes WP e, which captures the semantics of e as a predicate transformer. If you want to prove some property P about the result of e (i.e., a post-condition), it suffices to prove WP e P of the initial configuration in which e is executed (i.e., a pre-condition).

Let's start by considering a very simple, purely functional programming language with only the following forms:

b ::= x | true | false
e ::= b | let x = e1 in e2 | assert b | if b then e1 else e2

For this tiny language, the post-conditions P that you may want to prove are predicates on the boolean results of a computation, while the pre-conditions are just propositions. Defining WP e for this language is fairly straightforward:

WP b P                      = P b
WP (let x = e1 in e2) P     = WP e1 (fun x -> WP e2 P)
WP (assert b) P             = b /\ P b
WP (if b then e1 else e2) P = (b ==> WP e1 P) /\ ((not b) ==> WP e2 P)

This is nice and simple, but it has a significant drawback, particularly in the fourth rule: the post-condition formula P is duplicated across the branches. As several branching expressions are sequenced, this leads to an exponential blowup in the size of the verification condition.

This problem with WP computations is well knownFlanagan and Saxe and Leino both study this problem and provide equivalent solutions. In essence, they show that for a first-order, assignment-free guarded command language the weakest pre-condition can be computed in a size nearly linear in the size of the program. Then, they show that first-order imperative WHILE language can be converted into SSA form and then into a guarded command language.

In the context of F*, we generalize the results of Flanagan and Saxe, and Leino, to the setting of a higher-order language. The main technical idea is a new “Double Dijkstra Monad. Given a program, F* infers a monadic computation type indexed by (1) a WP, the weakest pre-condition predicate transformer; and (2) a WLP, the weakest liberal pre-condition predicate transformer. Intuitively, WLP e Q is sufficient to guarantee that if e contains no internal assertion failures, then its result satisfies P; in contrast, the WP e P is sufficient to guarantee both that e's internal assertions succeed and that its result satisfies P.

Here's the definition of WLP for our small example language.

WLP b P                      = P b
WLP (let x = e1 in e2) P     = WLP e1 (fun x -> WLP e2 P)
WLP (assert b) P             = b ==> P b
WLP (if b then e1 else e2) P = (b ==> WLP e1 P) /\ ((not b) ==> WLP e2 P)

The only difference with the WP is in the case of assertions. For a WLP, rather than requiring a proof of the assertion, we try to prove the post-condition assuming the assertion succeeds.

How does this help us? Let's see.

First, you can prove the following property about WLP.

(Identity 1)
           WLP e P
      <==> forall x. P x \/ WLP e (fun y -> y <> x)

Here's one way to read formula (1): Proving that P is true of the typed result of a computation (the LHS) is equivalent to proving that for every x, we either have P x or we can prove that the result of the computation is not x (the RHS).

Armed with identity (1) above, we can also prove the following identity:

(Identity 2)
          WP e P
     <==> WP e (fun x -> True) /\ WLP e P
     <==> WP e (fun x -> True) /\ (forall x. P x \/ WLP e (fun y -> y <> x)) (by (1))

That is, in order to prove that a computation e has no internal assertion failures and produces a result satisfying P, one can equivalently prove (a) that e has no internal assertion failures (i.e., WP e (fun x -> True)) and then prove (b) that e's result satisfies P (i.e, WLP e P).

Finally, we come back to our rule for conditional expressions, which we can restate as follows (using identities (1) and (2)):

WP (if b then e1 else e2) P
=    (b ==> WP e1 (fun x -> True))
  /\ ((not b) ==> WP e2 (fun x -> True))
  /\ (forall y. P y \/ ((b ==> WLP e1 (fun x -> x<>y)
                     /\ (not b) ==> WLP e2 (fun x -> x<>y)))

In this form, the post-condition P is no longer duplicated across the branches of the computation and we avoid the exponential blowup (at the cost of computing both the WP and the WLP).

WPs and WLPs are convenient for type inferencefor loop- and recursion-free code, we can simply compute the most precise verification condition for a program without further annotation. However, programmers are often more comfortable writing specification in terms of pre- and post-conditions, rather than predicate transformers. As we will see shortly, computing both the WP and the WLP allows F* to move between the two styles without a loss in precision (computing just the WP alone would not allow this).

9.2. Computation types

Expressions in F* are given computation types C. In its most primitive form, each effect in F* introduces a computation type of the form M t1..tn t wp wlp. The M t1..tn indicates the name of the effect M and several user-defined indexes t1..tn. The type t indicates the type of the result of the computation; wp is a predicate transformer that is not weaker than the weakest pre-condition of e; and wlp is a predicate transformer not weaker than the weakest liberal pre-condition of e. For the sake of brevity, we call wp the weakest pre-condition and wlp the weakest liberal pre-condition.

For the purposes of the presentation here, we start by discussing a simplified form of these C types, i.e, we will consider computation types of the form M t wp wlp, those that have a non-parameterized effect constructor M (and generalize to the full form towards the end of this chapter).

A computation e has type M t wp wlp if when run in an initial configuration satisfying wp post, it (either runs forever, if allowed, or) produces a result of type t in a final configuration f such that post f is true, all the while exhibiting no more effects than are allowed by M. In other words, M is an upper bound on the effects of e; t is its result type; and wp is a predicate transformer that for any post-condition of the final configuration of e, produces a sufficient condition on the initial configuration of e. The wlp is similar, except it is liberal with respect to the internal assertions of e in the sense described in the previous section.

These computation types (specifically their predicate transformers) form what is known as a Dijkstra monad. Some concrete examples should provide better intuition.

Remark. We follow an informal syntactic convention that the non-abbreviated all-caps names for computation types are the primitive formsother forms are derived from these.

For example, the computation type constructor PURE is a more primitive version of Pure, which we have used earlier in this tutorial. By the end of this chapter, you will see how Pure, Tot, etc. are expressed in terms of PURE. Likewise STATE is the primitive form of ST; EXN is the primitive form of Exn; etc.

9.3. The PURE effect

The PURE effect is primitive in F*. No user should ever have to (re-)define it. Its definition is provided once and for all in lib/prims.fst. It's instructive to look at its definition inasmuch as it provides some insight into how F* works under the covers. It also provides some guidance on how to define new effects. We discuss a fragment of it here.

The type of pure computations is PURE t wp wlp where wp, wlp : (t -> Type) -> Type. This means that pure computations produce t-typed results and are described by predicate transformers that transform result predicates (post-conditions of kind t -> Type) to pre-conditions, which are propositions of kind Type.

Seen another way, the signatures of the wp and wlp have the following formthey transform pure post-conditions to pure pre-conditions.

kind PurePost (a:Type) = a -> Type
kind PurePre = Type
kind PureWP (a:Type) = PurePost a -> PurePre

For example, one computation type for 0 is PURE int return_zero return_zero where

return_zero = fun (p:(int -> Type)) -> p 0

This means that in order to prove any property p about the result of the computation 0 is suffices to prove p 0which is of course what you would expect. The type return_zero is an instance of the more general form below:

type return_PURE (#a:Type) (x:a) = fun (post: PurePost a) -> post x

When sequentially composing two pure computations using let x = e1 in e2, if e1: PURE t1 wp1 wlp1 and e2: (x:t1 -> PURE t2 (wp2 x) (wlp2 x)), we type the composed computation as

PURE t2 (bind_PURE wp1 wp2) (bind_PURE wlp1 wlp2)

where:

type bind_PURE (#a:Type) (#b:Type)
               (wp1: PureWP a)
               (wp2: a -> PureWP b)
 = fun (post:PurePost b) -> wp1 (fun (x:a) -> wp2 x post)

One can show that return_PURE and bind_PURE together form a monad.

9.3.1. Pure and Tot

The Pure effect is an abbreviation for PURE that allows you to write specifications with pre- and post-conditions instead of predicate transformers. It is defined as follows:

effect Pure (a:Type) (pre:Type) (post: a -> Type) =
       PURE a (fun (p:PurePost a) -> pre /\ forall (x:a). post x ==> p x)
              (fun (p:PurePost a) -> forall (x:a). pre /\ post x ==> p x)

That is Pure a pre post is a computation which when pre is true produces a result v:a such that post v is true.

The Tot effect is defined below:

effect Tot (a:Type) =
       PURE a (fun (p:PurePost a) -> forall (x:a). p x)
              (fun (p:PurePost a) -> forall (x:a). p x)

This means that a computation type Tot a only reveals that the computation always terminates with an a-typed result.

9.3.2. From predicate transformers to pre- and post-conditions

We have just seen how the definition of Pure a pre post unfolds into the PURE effect. It is also possible to go in the other direction, turning a specification written in the PURE a wp wlp style into a Pure a pre post. However, whereas F* will always automatically unfold the definition of Pure in terms of PURE as needed, it will not automatically transform the more primitive PURE effect into the derived form Pure. Instead, one uses an explicit coercion for this purpose, with the signature shown below.

type as_requires (#a:Type) (wp:PureWP a)  = wp (fun x -> True)
type as_ensures  (#a:Type) (wlp:PureWP a) (x:a) = ~ (wlp (fun y -> ~(y=x)))
assume val as_Pure: #a:Type -> #b:(a -> Type)
          -> #wp:(x:a -> PureWP (b x))
          -> #wlp:(x:a -> PureWP (b x))
          -> =f:(x:a -> PURE (b x) (wp x) (wlp x))
          -> x:a -> Pure (b x) (as_requires (wp x))
                               (as_ensures (wlp x))

Remark. The second last argument to as_Pure is named f and is tagged with an equality constraint, written by preceding the bound variable name with the equality symbol, i.e., =f. Given an application as_Pure g, the equality constraint on the f argument of as_Pure instructs F*'s type inference engine to unify the type of g with the expected type of f. Without this constraint, by default, F* will try to prove that the type of g is a subtype of the expected type of f. In cases like this, where an argument mentions several implicit arguments that need to be inferred (a, b, wp, wlp, in this case), the equality constraint produces better inference results.

One way to understand this type is as follows: as_Pure f coerces the type of f which has a PURE (b x) wp wlp effect to an equivalent function type written in terms of Pure. The pre-condition of the resulting function type is easily computed from the wp, using as_requires wp, which is just the weakest pre-condition of the trivial post-condition.

Computing the post-condition is a bit more subtle, and is accomplished with the as_ensures wlp function. Perhaps the easiest way to understand it is by studying the roundtrip transformation of PURE to Pure and back to PURE. The key step below is in the transformation from (b) to (c), where we see that by ensuring ~wlp (fun y -> y <> x), we make use precisely of the Identity 1 from the previous section. Given only a wp without a wlp, we would be stuck not being able to construct as_ensures.

(a) Pure t (as_requires wp)
           (as_ensures wlp)

= (definition)

(b) PURE t (fun post -> wp (fun x -> True) /\ forall y. ~(wlp (fun y' -> y<>y')) ==> post y)
           (fun post -> forall y. wp (fun x -> True) /\  ~(wlp (fun y’ -> y<>y')) ==> post y)

= (unfolding ==> and double negation)

(c) PURE t (fun post -> wp (fun x -> True) /\ forall y.  wlp (fun y' -> y<>y’) \/ post y)
           (fun post -> forall y. not (wp (fun x -> True)) \/ wlp (fun y’ -> y<>y’) \/ post y)

= (folding ==>)

(d) PURE t (fun post -> wp (fun x -> True) /\ forall y.  wlp (fun y’ -> y<>y’) \/ post y)
           (fun post -> forall y. wp (fun x -> True) ==> (wlp (fun y’ -> y<>y’) \/ post y))

= (rearranging quantifier)

(e) PURE t (fun post -> wp (fun x -> True) /\ forall y.  wlp (fun y’ -> y<>y’) \/ post y)
           (fun post -> wp (fun x -> True) ==> forall y. (wlp (fun y’ -> y<>y’) \/ post y))

= (identity 1)

(f) PURE t (fun post -> wp (fun x -> True) /\ wlp (fun y’ -> post y’))
           (fun post -> wp (fun x -> True) ==> wlp (fun y’ -> post y’))

<: (strengthening wlp, eta reduction)

(g) PURE t (fun post -> wp (fun x -> True) /\ wlp post)
            wlp

= (identity 2, eta)

(h) PURE t wp wlp

Here are a few small examples using this coercion to move from PURE to Pure.

val f : x:int -> PURE int (fun 'p -> x > 0 /\ 'p (x + 1)) (fun 'p -> x > 0 ==> 'p (x + 1))
let f x = assert (x > 0); x + 1

val h : #req:(int -> Type)
     -> #ens:(int -> int -> Type)
     -> =f:(x:int -> Pure int (req x) (ens x))
     -> y:int -> Pure int (req y) (ens y)
let h f x = f x

val g : x:int -> Pure int (x > 0) (fun y -> y == x + 1)
let g = h (as_Pure f)

Exercise 9a:

Work out the roundtrip unfolding a Pure t pre post into a PURE effect and then back to a Pure using the as_Pure coercion. Prove that after this round trip, the resulting type is logically equivalent to the type you started with.

exercise answer
Pure t p q

= (definition)

PURE t wp wlp
  where wp  = fun post -> p /\ forall (y:t). q y ==> post y
    and wlp = fun post -> forall (y:t). p /\ q y ==> post y

<:  (definition)

  Pure t (p /\ forall (y:t). q y ==> True)
         (fun y -> not (forall (z:t). p /\ q z ==> (y<>z)))

=  (simplification/de Morgan)

Pure t (p)
       (fun y -> exists (z:t). p /\ q z /\ y=z)

= (replacing existential by equality)

   Pure t p
          (fun y -> p /\ q y)

<: (weakening post-condition, eta)

   Pure t p q

9.4. The STATE effect

Stateful programs operate on an input heap producing a result and an output heap. The computation type STATE t wp wlp describes such a computation, where wp, wlp : StateWP t has the signature below.

kind StatePost t = t -> heap -> Type
kind StatePre    = heap -> Type
kind StateWP t   = StatePost t -> StatePre

In other words, WPs and WLPs for stateful programs transform stateful post-conditions (relating the t-typed result of a computation to the final heap) into a pre-condition, a predicate on the input heap.

The type heap is axiomatized in lib/heap.fst and is one model of the primitive heap provided by the F* runtime system. Specifically, we have functions to select, update, and test the presence of a reference in a heap.

module Heap
assume type heap
assume val sel : #a:Type -> heap -> ref a -> Tot a
assume val upd : #a:Type -> heap -> ref a -> a -> Tot heap
assume val contains : #a:Type -> heap -> ref a -> a -> Tot bool

These functions are interpreted using standard axioms, which allows the SMT solver to reason about heaps, for instance:

assume SelUpd1:       forall (a:Type) (h:heap) (r:ref a) (v:a).
                      {:pattern (sel (upd h r v) r)}
                      sel (upd h r v) r = v

assume SelUpd2:       forall (a:Type) (b:Type) (h:heap) (k1:ref a) (k2:ref b) (v:b).
                      {:pattern (sel (upd h k2 v) k1)}
                      k2=!=k1 ==> sel (upd h k2 v) k1 = sel h k1

The Heap library axiomatizes several other functionsthe interested reader refer to lib/heap.fst for more details.

Remark. Note, although sel is marked as a total function, the axioms underspecify its behavior, e.g., sel h r has no further interpretation unless h can be proven to be an upd.

Also note the use of the {:pattern ...} form in the axioms above. This provides the SMT solver with a trigger for the quantifiers, in effect orienting the equalities in SelUpd1 and SelUpd2 as left-to-right rewritings.

The functions sel and upd provide a logical theory of heaps. At the programmatic level, we require stateful operations to allocate, read and write references in the current heap of the program. The signatures of these stateful primitives are provided in lib/st.fst, as illustrated (in slightly simplified form) below.

Let's start with the signature of read:

assume val read: #a:Type -> r:ref a -> STATE a (wp_read r) (wp_read r)
where wp_read r = fun (post:StatePost a) (h0:heap) ->  post (sel h0 r) h0

This says that read r returns a result v:a when r:ref a; and, to prove for any post-condition post:StatePost a relating the v to the resulting heap, it suffices to prove post (sel h0 r) h0 when read r is run in the initial heap h0.

Next, here's the signature of write:

assume val write: #a:Type -> r:ref a -> v:a -> STATE unit (wp_write r) (wp_write r)
where wp_write r = fun (post:StatePost a) (h0:heap) -> post () (upd h0 r v)

This says that write r v returns a a unit-typed result when r:ref a and v:a; and, to prove any post-condition post:StatePost a relating the () to the resulting heap, it suffices to prove post () (upd h0 r v) when write r v is run in the initial heap h0.

Remark. F* provides support for user-defined custom operators. To allow you to write !r for read r and r := v instead of ST.write r v, we define

let op_Bang x = ST.read x

and

let op_Colon_Equals x v = ST.write x v

As with the PureWP, the predicate transformers StateWP t form a monad, as shown by the combinators below.

type return_STATE (#a:Type) (v:a) = fun (post:StatePost a) (h0:heap) -> post v h0

type bind_STATE (#a:Type) (wp1:StateWP a) (wp2:a -> StateWP b)
     = fun (post:StatePost b) (h0:heap) -> wp1 (fun (x:a) -> wp2 x post) h0

9.4.1. The ST effect

ST is to STATE what Pure is to PURE: it provides a way to write stateful specifications using pre- and post-conditions instead of predicate transformers. It is defined as shown below (in lib/st.fst):

effect ST (a:Type) (pre:StatePre) (post: (heap -> StatePost a)) = STATE a
  (fun (p:StatePost a) (h:heap) ->
     pre h /\ (forall a h1. (pre h /\ post h a h1) ==> p a h1)) (* WP *)
  (fun (p:StatePost a) (h:heap) ->
     (forall a h1. (pre h /\ post h a h1) ==> p a h1))          (* WLP *)

As before, we can also define a coercion to move to ST from STATE.

type as_requires (#a:Type) (wp:STWP_h heap a)  = wp (fun x h -> True)
type as_ensures  (#a:Type) (wlp:STWP_h heap a) (h0:heap) (x:a) (h1:heap)
  = ~ (wlp (fun y h1' -> y<>x \/ h1<>h1') h0)
val as_ST: #a:Type -> #b:(a -> Type)
          -> #wp:(x:a -> STWP_h heap (b x))
          -> #wlp:(x:a -> STWP_h heap (b x))
          -> =f:(x:a -> STATE (b x) (wp x) (wlp x))
          -> x:a -> ST (b x) (as_requires (wp x))
                             (as_ensures (wlp x))

And here's a small program that uses this coercion.

let f x = !x * !x

val h : #req:(ref int -> heap -> Type)
     -> #ens:(ref int -> heap -> int -> heap -> Type)
     -> =f:(x:ref int -> ST int (req x) (ens x))
     -> y:ref int -> ST int (req y) (ens y)
let h f x = f x

val g : x:ref int -> ST int (fun h -> True) (fun h0 y h1 -> h0=h1 /\ y >= 0)
let g = h (as_ST f)

9.4.2. The St effect

We define another abbreviation on top of ST for stateful programs with trivial pre- and post-conditions.

  effect St (a:Type) = ST a (fun h -> True) (fun _ _ _ -> True)

9.5. Lifting effects

When programming with multiple effects, you can instruct F* to automatically infer a specification for your program with a predicate transformer that captures the semantics of all the effects you use. The way this works is that F* computes the least effect for each sub-term of your program, and then lifts the specification of each sub-term into some larger effect, as may be needed by the context.

For example, say you write:

let y = !x in y + 1

The sub-term !x has the STATE effect; whereas the sub-term y+1 is PURE. Since the whole term has at least STATE effect, we'd like to lift the pure sub-computation to STATE. To do this, you can specify that PURE is a sub-effect of STATE, as follows (adapted from lib/prims.fst):

sub_effect
  PURE   ~> STATE = fun (a:Type) (wp:PureWP a) (p:StatePost a) (h:heap) ->
                    wp (fun a -> p a h)

This says that in order to lift a PURE computation to STATE, we lift its wp:PureWP a (equivalently for its wlp) to a StateWP a that says that that pure computation leaves the state unmodified.

Note that the type of PURE ~> STATE is (a:Type) -> PureWP a -> StatePost a -> heap -> Type which corresponds to (a:Type) -> PureWP a -> StateWP a since:

kind StateWP a   = StatePost a -> StatePre
kind StatePre    = heap -> Type

9.6. Indexed computation types

Finally, as mentioned earlier, in its full form a computation type has the shape M t1..tn t wp wlp, where t1..tn are some user-chosen indices to the effect constructor M.

This is convenient in that it allows effects to be defined parametrically, and specific effects derived just by instantiation.

For example, the STATE effect is actually defined as an instance of a more general parameterized effect STATE_h (mem:Type), which is parametric in the type of the memory used by the state monad.

Specifically, we have in lib/prims.fst

new_effect STATE = STATE_h heap

However, as we will see in subsequent sections, it is often convenient to define other variants of the state monad using different memory structures.

10. Verifying Stateful Programs

In the previous chapter, we saw how F*'s ST monad was specified. We now look at several programs illustrating its use. If you skipped the previous chapter, you should be okwe'll explain what's needed about the ST monad as we go along, although, eventually, you'll probably want to refer to the previous chapter for more details.

10.1. Stateful access control

We'll start with a simple example, based on the access control example from 1.1. A restriction of that example was that the access control policy was fixed by the two functions canWrite and canRead. What if we want to administer access rights using an access control list (ACL)? Here's one simple way to model itof course, a full implementation of stateful access control would have to pay attention to many more details.

The main idea is to maintain a reference that holds the current access control list. In order to access a resource, we need to prove that the current state contains the appropriate permission.

Here's how it goes:

module Ex10a
open FStar.All
//acls-variant

open FStar.List.Tot
open FStar.Heap

type file = string

(* Each entry is an element in our access-control list *)
type entry =
  | Readable of string
  | Writable of string
type db = list entry

(* We define two pure functions that test whether
   the suitable permission exists in some db *)
let canWrite db file =
  Some? (tryFind (function Writable x -> x=file | _ -> false) db)


let canRead db file =
  Some? (tryFind (function Readable x | Writable x -> x=file) db)

(* The acls reference stores the current access-control list, initially empty *)
val acls: ref db
let acls = alloc []

(*
   Here are two stateful functions which alter the access control list.
   In reality, these functions may themselves be protected by some
   further authentication mechanism to ensure that an attacker cannot
   alter the access control list

   F* infers a fully precise predicate transformer semantics for them.
*)

let grant e = ST.write acls (e::ST.read acls)

let revoke e =
  let db = filter (fun e' -> e<>e') (ST.read acls) in
  ST.write acls db

(* Next, we model two primitives that provide access to files *)

(* We use two heap predicates, which will serve as stateful pre-conditions *)
type canRead_t f h  = canRead  (sel h acls) f  == true
type canWrite_t f h = canWrite (sel h acls) f == true

(* In order to call `read`, you need to prove
   the `canRead f` permission exists in the input heap *)
assume val read:   file:string -> ST string
                                     (requires (canRead_t file))
                                     (ensures (fun h s h' -> modifies_none h h'))

(* Likewise for `delete` *)
assume val delete: file:string -> ST unit
                                     (requires (canWrite_t file))
                                     (ensures (fun h s h' -> modifies_none h h'))

(* Then, we have a top-level API, which provides protected
   access to a file by first checking the access control list.

   If the check fails, it raises a fatal exception using `failwith`.
   As such, it is defined to have effect `All`, which combines
   both state and exceptions.

   Regardless, the specification proves that `checkedDelete`
   does not change the heap.
 *)
val safe_delete: file -> All unit 
                (requires (fun h -> True))
                (ensures (fun h x h' -> modifies_none h h'))


let safe_delete file =
  if canWrite !acls file
  then delete file
  else failwith "unwritable"

(* Finally, we have a top-level client program *)
val test_acls: file -> ML unit
let test_acls f =
  grant (Readable f);     (* ok *)
  let _ = read f in       (* ok --- it's in the acl *)
  //delete f;               (* not ok --- we're only allowed to read it *) 
  safe_delete f;          (* ok, but fails dynamically *)
  revoke (Readable f);
  //let _ = read f in       (* not ok any more *) 
  ()

Exercise 10a:
Write down some types for grant and revoke that are sufficiently precise to allow the program to continue to type-check.

val grant : e:entry -> ST unit (requires (fun h -> True))
                               (ensures (fun h x h' -> True))
let grant e = ST.write acls (e::ST.read acls)

val revoke: e:entry -> ST unit (requires (fun h -> True))
                               (ensures (fun h x h' -> True))
let revoke e =
  let db = List.filterT (fun e' -> e<>e') (ST.read acls) in
  ST.write acls db

code/exercises/Ex10a.fstLoad in editor

exercise answer
val grant : e:entry -> ST unit (requires (fun h -> True))
                               (ensures (fun h x h' -> sel h' acls = e::sel h acls))
let grant e = ST.write acls (e::ST.read acls)

val revoke: e:entry -> ST unit (requires (fun h -> True))
                               (ensures (fun h x h' -> not(List.mem e (sel h' acls))))
let revoke e =
  let db = List.filter (fun e' -> e<>e') (ST.read acls) in
  ST.write acls db

code/solutions/Ex10a.fstLoad in editor

10.2. Reasoning about (anti-)aliased heap structures

A central problem in reasoning about heap-manipulating programs has to do with reasoning about updates to references in the presence of aliasing. In general, any two references (with compatible types) can alias each other (i.e, they may refer to the same piece of memory), so updating one can also change the contents of the other. In this section, we'll look at two small but representative samples that illustrate how this form of reasoning can be done in F*.

10.2.1. Dynamic frames

For our first example, we define the type of a 2-dimensional mutable point. The refinement on y ensures that the references used to store each coordinate are distinct.

type point =
  | Point : x:ref int -> y:ref int{y<>x} -> point

Allocating a new point is straightforward:

let new_point x y =
  let x = ST.alloc x in
  let y = ST.alloc y in
  Point x y

As is moving a point by a unit along the x-axis.

let shift_x p = Point.x p := !(Point.x p) + 1

Now, things get a bit more interesting. Let's say we have a pair of points, p1 and p2, we want to shift p1, and reason that p2 is unchanged. For example, we'd like to identify some conditions that are sufficient to prove that the assertion in the program below always succeeds.

let shift_x_p1 p1 p2 =
    let p2_0 = !(Point?.x p2), !(Point?.y p2)  in //p2 is initially p2_0
    shift_x p1;
    let p2_1 = !(Point?.x p2), !(Point?.y p2) in
    assert (p2_0 = p2_1)                        //p2 is unchanged

If you give this program (reproduced in its entirety below) to F*, it will report no errors. This may surprise you: after all, if you call shift_x_p1 p p the assertion will indeed fail. What's going on here is that for functions in the ST effect, F* infers a most precise type for it, and if the programmer did not write down any other specification, this precise inferred type is what F* will use. This means that without an annotation on shift_x_p1, F* does not check that the assertion will succeed on every invocation of shift_x_p1; instead, using the inferred type it will aim to prove that the assertion will succeed whenever the function is called. Let's try:

val test0: unit -> St unit
let test0 () =
  let p1 = new_point 0 0 in
  shift_x_p1 p1 p1

Here, we wrote a specification for test0, asking it to have trivial pre-condition. When we ask F* to check this, it complains at the call to shift_x_p1 x x, saying that the assertion failed.

If we try calling shift_x_p1 with two distinct points, as below, then we can prove that the assertion succeeds.

val test1: unit -> St unit
let test1 () =
  let p1 = new_point 0 0 in
  let p2 = new_point 0 0 in
  shift_x_p1 p1 p2

In simple code like our example above, it is a reasonable trade-off to let F* infer the most precise type of a function, and to have it check later, at each call site, that those calls are safe.

As you write larger programs, it's a good idea to write down the types you expect, at least for tricky top-level functions. To see what these types look like for stateful programs, let's decorate each of the top-level functions in our example with the typesfor these tiny functions, the types can often be larger than the code itself; but this is just an exercise. Typically, one wouldn't write down the types of such simple functions.

10.2.2. A type for shift_x and the Heap.modifies predicate

Let's start with shift_x, since it is the simplest:

Here's one very precise type for it:

val shift_x : p:point -> ST unit
  (requires (fun h -> True))
  (ensures (fun h0 _ h1 -> h1=upd h0 (Point.x p) (sel h0 (Point.x p) + 1)))

Another, less precise but more idiomatic type for it is:

val shift_x: p:point -> ST unit
  (requires (fun h -> True))
  (ensures (fun h0 x h1 -> modifies (only (Point?.x p)) h0 h1))

Informally, ensures-clause above says that the heap after calling this function (h1) differs from the initial heap h0 only at Point.x (and possibly some newly allocated locations). Let's look at it in more detail.

The predicate modifies is defined in the module Heap (lib/heap.fst). First, let's look at its signature, which says that it relates a set aref to a pair of heaps. The type aref is the type of a reference, but with the type of referent abstracted. As such, the first argument to modifies is a set of heterogenously typed references.

  type aref =
    | Ref : #a:Type -> ref a -> aref
  let only x = Set.singleton (Ref x)
  type modifies : set aref -> heap -> heap -> Type

The definition of modifies follows:

type modifies mods h0 h1 =
  Heap.equal h1 (Heap.concat h1 (Heap.restrict (Set.complement mods) h0))

Heap.equal: Heap.equal is an equivalence relation on heap capturing the notion of extensional equality; i.e., two heaps are extensionally equal if they map each reference to the same value.

Heap.concat: Each reference r in the heap concat h h' contains a value that is the same as in h, except if the r is in h', in which case it's value is whatever value h' contains at r. More formally:

   sel r (concat h h')
   = if contains h' r then sel h' r else sel h r

Heap.restrict The function restrict s h provides a way to shrink the domain of the heap h to be at most s. Specifically:

  contains (restrict s h) r = Set.mem (Ref r) s && contains h r

Altogether, the definition of modifies says that for every reference r, if r is not in the set mods and r if the heap h0 contains r, then sel h1 r = sel h0 r, i.e., it hasn't changed. Otherwise, sel h1 r = sel h1 rmeaning we know nothing else about it.

Remark. We define the following infix operators to build sets of heterogenous references.

let op_Hat_Plus_Plus (#a:Type) (r:ref a) (s:set aref) = // ^++
    Set.union (Set.singleton (Ref r)) s

let op_Plus_Plus_Hat (#a:Type) (s:set aref) (r:ref a) = // ++^
    Set.union s (Set.singleton (Ref r))

let op_Hat_Plus_Hat (#a:Type) (#b:Type) (r1:ref a) (r2:ref b) = // ^+^
    Set.union (Set.singleton (Ref r1)) (Set.singleton (Ref r2))

10.2.3. A type for new_point and freshness of references

Here's a precise type for new_point, with its definition reproduced for convenience.

val new_point: x:int -> y:int -> ST point
  (requires (fun h -> True))
  (ensures (fun h0 p h1 ->
                modifies TSet.empty h0 h1
                /\ Heap.fresh (Point?.x p ^+^ Point?.y p) h0 h1
                /\ Heap.sel h1 (Point?.x p) = x
                /\ Heap.sel h1 (Point?.y p) = y
                /\ Heap.contains h1 (Point?.x p) //these two lines should be captures by fresh
                /\ Heap.contains h1 (Point?.y p)))

let new_point x y =
  let x = ST.alloc x in
  let y = ST.alloc y in
  Point x y

The modifies clause says the function modifies no existing referencethat's easy to see, it only allocates new references.

In the body of the definition, we build Point x y and the type of Point requires us to prove that x <> y. The only way to prove that is if we know that ref returns a distinct reference each time, i.e., we need freshness.

The type of ST.alloc gives us the freshness we need to prove that x <> y. The type below says that the returned reference does not exists in the initial heap and does exist in the final heap (initialized appropriately).

val alloc:  #a:Type -> init:a -> ST (ref a)
    (requires (fun h -> True))
    (ensures (fun h0 r h1 -> fresh (only r) h0 h1 /\ h1==upd h0 r init))

type fresh (refs:set aref) (h0:heap) (h1:heap) =
  (forall (a:Type) (r:ref a). mem (Ref r) refs
                         ==> not(contains h0 r) /\ contains h1 r)

Coming back to the type of new_point: By stating that the new heap contains both Point.x and Point.y, we provide the caller with enough information to prove that any references that it might allocate subsequently will be different from the references in the newly allocated point. For example, the assertion in the code below succeeds, only because new_point guarantees that the heap prior to the allocation of z contains Point.x p; and ST.alloc guarantees that z is different from any reference that exists in the prior heap. Carrying Heap.contains predicates in specifications is important for this reason.

val test2: unit -> St unit
let test2 () =
  let p = new_point 0 0 in
  let z = ST.alloc 0 in
  assert (Point?.x p <> z)

On the other hand, since the ST library we are working with provides no ability to deallocate a reference (other versions of it do; see, for example, lib/stperm.fst), we know that if we have a value v:ref t, that the current heap must contain it. Capturing this invariant, the ST library also provides the following primitive (whose implementation is a noop).

val recall: #a:Type -> r:ref a -> ST unit
  (requires (fun h -> True))
  (ensures (fun h0 _ h1 -> h0=h1 /\ Heap.contains h1 r))

Using this, we can write the following code.

val f : ref int -> St unit
let f (x:ref int) =
  recall x;         //gives us that the initial heap contains x, for free
  let y = ST.alloc 0 in
  assert (y <> x)

As a matter of style, we prefer to keep the use of recall to a minimum, and instead carry Heap.contains predicates in our specifications, as much as possible.

10.2.4. A type for shift_x_p1

Now, we have all the machinery we need to give shift_x_p1 a sufficiently strong type to prove that its assertion will never fail (if its pre-condition is met).

val shift_x_p1: p1:point
           -> p2:point{   Point?.x p2 <> Point?.x p1
                       /\ Point?.y p2 <> Point?.x p1 }
           -> ST unit
    (requires (fun h -> Heap.contains h (Point?.x p2)
                    /\  Heap.contains h (Point?.y p2)))
    (ensures (fun h0 _ h1 -> modifies (only (Point?.x p1)) h0 h1))

In order to prove that the assignment to Point.x p1 did not change p2, we need to know that Point.x p1 does not alias either component of p2. In general, if p1 can change arbitrarily, we also need the other two conjuncts, i.e., we will need that the references of p1 and p2 are pairwise distinct.

Remark. A note on style: we could have placed the refinement on p2 within the requires clause. However, since the refinement is independent of the state, we prefer to write it in a manner that makes its state independence explicit.

Exercise 10b:
Change shift_x to the function shift below that moves both the x and y components of its argument by some amount. Prove that calling this function in a function like shift_p1 does not change p2.

let shift p = Point.x p := ...; Point.y p := ...

code/exercises/Ex10b.fstLoad in editor

exercise answer
let shift p =
  Point?.x p := !(Point?.x p) + 1;
  Point?.y p := !(Point?.y p) + 1


val shift_p1: p1:point
           -> p2:point{   Point?.x p2 <> Point?.x p1
                       /\ Point?.y p2 <> Point?.x p1
                       /\ Point?.x p2 <> Point?.y p1
                       /\ Point?.y p2 <> Point?.y p1 }
           -> ST unit
    (requires (fun h -> Heap.contains h (Point?.x p2)
                    /\  Heap.contains h (Point?.y p2)))
    (ensures (fun h0 _ h1 -> modifies (Point?.x p1 ^+^ Point?.y p1) h0 h1))

let shift_p1 p1 p2 =
    let p2_0 = !(Point?.x p2), !(Point?.y p2)  in //p2 is initially p2_0
    shift p1;
    let p2_1 = !(Point?.x p2), !(Point?.y p2) in
    assert (p2_0 = p2_1)                        //p2 is unchanged

code/solutions/Ex10b.fstLoad in editor

11. Lightweight framing with hyper-heaps

The style of the previous section is quite general. But, as programs scale up, specifying and reasoning about anti-aliasing can get to be quite tedious. In this chapter, we look at an alternative way of proving stateful programs correct by making use of a more structured representation of memory that we call a “HyperHeap”. First, we illustrate the problem of scaling up the approach of the previous chapter to even slightly larger examples

11.1. Flying robots