F* is a verification-oriented programming language developed at Microsoft Research, MSR-Inria, and Inria. It follows in the tradition of the ML family of languages in that it is a typed, strict, functional programming language. However, its type system is significantly richer than ML's, allowing functional correctness specifications to be stated and checked semi-automatically. This tutorial provides a first taste of verified programming in F*. More information about F*, including papers and technical reports, can be found on the F* website.
It will help if you are already familiar with functional programming languages in the ML family (e.g., OCaml, F#, Standard ML), or with Haskell—we provide a quick review of some basic concepts if you're a little rusty, but if you feel you need more background, there are many useful resources freely available on the web, e.g., Learn F#, F# for fun and profit, Introduction to Caml, the Real World OCaml book, or the OCaml MOOC.
The easiest way to try F* and solve the verification exercises in this tutorial is directly in your browser by using the online F* editor. You can load the boilerplate code needed for each exercise into the online editor by clicking the “Load in editor” link in the body of each exercise. Your progress on each exercise will be stored in browser local storage, so you can return to your code later (e.g. if your browser crashes, etc).
You can also do this tutorial by installing F* locally on your machine. F* is open source and cross-platform, and you can get binary packages for Windows, Linux, and MacOS X or compile F* from the source code on github using these instructions.
You can edit F* code using your favorite text editor, but for Emacs the community maintains fstar-mode.el, a sophisticated extension that adds special support for F*, including syntax highlighting, completion, type hints, navigation, documentation queries, and interactive development (in the style of CoqIDE or ProofGeneral). You can find more details about editor support on the F* wiki.
The code for the exercises in this tutorial and their solutions are in the F* repository on Github. For some exercises, you have to include additional libraries, as done by the provided Makefiles. To include libraries for the Emacs interactive mode follow the instructions here.
By default F* only verifies the input code, it does not execute it. To execute F* code one needs to extract it to OCaml or F# and then compile it using the OCaml or F# compiler. More details on executing F* code on the F* wiki.
Let's get started by diving into a simple model of access control on files. Along the way, we'll see some basic concepts from functional programming in general and a couple of F*-specific features.
Let's say we want to model a simple access control discipline on files—certain files are readable or writable, whereas others may be unauthorized. We'd like to write a policy to describe the privileges on each file, and we'd like to write programs whose file accesses are checked against this policy, guaranteeing statically that an unauthorized file is never accessed mistakenly.
Our model of this scenario (which we'll make more realistic in later sections) proceeds in three easy steps.
The syntax of F* is based closely on the syntax of OCaml and the non-light syntax of F#. Our F* program is made up of one module per file, and the body of the module contains a number of definitions, and optionally includes a ‘main’ expression.
Here are the first three definitions from the program:
type filename = string
(** [canWrite] is a function specifying whether a file [f] can be written *)
let canWrite (f:filename) =
match f with
| "demo/tempfile" -> true
| _ -> false
(** [canRead] is also a function ... *)
let canRead (f:filename) =
canWrite f (* writeable files are also readable *)
|| f="demo/README" (* and so is demo/README *)
code/exercises/Ex01a.fstLoad in editor
The first definition defines a type synonym: we'll use string
s to
model filename
s.
After that, we define two boolean functions:
canWrite
and canRead
:
The canWrite
function inspects its argument f
using a pattern matching expression: it returns the boolean true
when f
equals "demo/tempfile"
and false
otherwise. The function
canRead
is similar—a file is readable if it is writable, or if it
is the "demo/README"
file.
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 type of read
says that it is a function expecting a filename
argument f
for which canRead f
evaluates to true
and returning a
string
-typed result. Thus the type-checker prevents any calls to
read
for which the canRead
predicate can't be statically proved
for the argument.
The type of write
says that it is a function of two arguments: the
first is a filename
f
, such that canWrite f
evaluates to true
;
the second is a string
, the data to be written to the file f
. The write
function returns unit
, roughly analogous to the void
type in
C. The type unit
has only a single value, written ()
.
The crucial bits of these declarations are, of course, the use of the
canRead
and canWrite
functions in the signature, which allow us to
connect the types of these security-sensitive functions to our policy.
Trying to check that a piece of code conforms to an access-control policy is a tedious and error-prone process. Even if every access is guarded by a security check, how can we make sure that each check is adequate? We can use F*'s type-checker to automate this kind of code review.
Here's some simple, untrusted client code. It defines some common file names,
and then a function called staticChecking
,
which tries to read and write a few files.
let passwd : filename = "demo/password"
let readme : filename = "demo/README"
let tmp : filename = "demo/tempfile"
val staticChecking : unit -> ML unit
let staticChecking () =
let v_{1} = read tmp in
let v_{2} = read readme in
(* let v_{3} = 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 Ex01a.filename
You'll understand more about what that message means as you work
through this tutorial, but, for now, take it to mean that F* expected
canWrite passwd
to evaluate to true
, which isn't the case.
The staticChecking
function above illustrates how F* can be used to
specify a security policy, and statically enforce complete and correct
mediation of that policy via type-checking. We will now illustrate
that checking of the policy doesn't have to happen all statically, but
that the dynamic checks added by the programmer are taken into account
by the type system. In particular we implement a checkedRead
function
that consults the policy and only performs the read
if the policy
allows it, otherwise it raises an exception.
exception InvalidRead
val checkedRead : filename -> ML string
let checkedRead f =
if canRead f then read f else raise InvalidRead
code/exercises/Ex01a.fstLoad in editor
Note that the type of checkRead
imposes no condition on the
the input file f
. When the canRead f
check succeeds the
type-checker knows that the read f
call is safe.
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 with
checkedRead
, your checkedWrite
should have no preconditions.
assume val checkedWrite : filename -> string -> ML unit
code/exercises/Ex01a.fstLoad in editor
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 v_{1} = checkedRead tmp in
let v_{2} = checkedRead readme in
let v_{3} = 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.
You may not have noticed them all, but our first example already covers several distinctive features of F*. Let's take a closer look.
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).
Although we didn't write down any types for functions like canRead
or canWrite
, F* (like other languages in the ML family) infers
types for your program (if F* believes it is indeed type
correct). However, what is inferred by F* is more precise than what
can be expressed in ML. For instance, in addition to inferring a type,
F* also infers the side-effects of an expression (e.g., exceptions,
state, etc).
For instance, in ML (canRead "foo.txt")
is inferred to have type bool
.
However, in F*, we infer (canRead "foo.txt" : Tot bool)
. This
indicates that canRead "foo.txt"
is a pure total expression, which always
evaluates to a boolean. For that matter, any expression that is
inferred to have type-and-effect Tot t
, is guaranteed (provided the
computer has enough resources) to evaluate to a t
-typed result,
without entering an infinite loop; reading or writing the program's
state; throwing exceptions; performing input or output; or, having any
other effect whatsoever.
On the other hand, an expression like (read "foo.txt")
is
inferred to have type-and-effect ML string
, meaning that this term
may have arbitrary effects (it may loop, do IO, throw exceptions,
mutate the heap, etc.), but if it returns, it always returns a
string. The effect name ML
is chosen to represent the default,
implicit effect in all ML programs.
Tot
and ML
are just two of the possible effects. Some others
include:
Dv
, the effect of a computation that may diverge;
ST
, the effect of a computation that may diverge, read,
write or allocate new references in the heap;
Exn
, the effect of a computation that may diverge
or raise an exception.
The primitive effects {Tot, Dv, ST, Exn, ML}
are arranged in a
lattice, with Tot
at the
bottom (less than all the others), ML
at the top (greater than all
the others), and with ST
unrelated to Exn
. This means that a
computation with a particular effect can be treated as having any
other effect that is greater than it in the effect ordering—we call
this feature sub-effecting.
In fact, you can configure F* with your own family of effects and effect ordering and have F* infer those effects for your programs—but that's more advanced and beyond the scope of this tutorial. (If curious you can check out this paper.)
From now on, we'll just refer to a type-and-effect pair (e.g. Tot
int
where Tot
is the effect and int
is the result type), as a
computation type.
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 t_{1} -> ... -> t_{n} -> E t
, where t_{1} .. t_{n}
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 i_{1} i_{2} = if i_{1} > i_{2} then i_{1} else i_{2}
Impure functions, like reading the contents of a file, are given corresponding effects:
val read : filename -> ML string
F* is a call-by-value functional language (like OCaml and F#, and unlike Haskell), so function arguments are fully evaluated to values before being passed to the function. Values have no (immediate) effect, thus the types of a function's arguments have no effect annotation. On the other hand, the body of a function may perform some non-trivial computation and so the result is always given both a type and an effect, as explained above.
Like many functional languages, function application has higher precedence
than almost any other operation. Remembering this can help you keep track
of when you do (and do not) need parentheses. For example, if, using the
definitions for is_positive
and max
above, you try to write:
let x = is_positive max 1 2
you will get a type resolution failure, since F* will try to apply
is_positive
to the max
function itself, and it will complain that
is_positive
expects an int
argument, whereas max
is a function
that maps two integers to another integer. In this case, you need one
set of parentheses around max
:
let x = is_positive (max 1 2)
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.
(*
Copyright 2008-2018 Microsoft Research
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
module Ex02a
//can-read-write-types
type filename = string
//val canWrite : unit (* write a correct and precise type here *)
let canWrite (f:filename) =
match f with
| "demo/tempfile" -> true
| _ -> false
//val canRead : unit (* write correct and precise type here *)
let canRead (f:filename) =
canWrite f (* writeable files are also readable *)
|| f="demo/README" (* and so is this file *)
code/exercises/Ex02a.fstLoad in editor
val canRead: filename -> Tot bool
val canWrite: filename -> Tot bool
code/solutions/Ex02a.fstLoad in editor
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.
Skip this section on a first read, if you are new to functional programming.
Sometimes it is useful to return a function after performing some
computation. For example, here is a function that makes a new counter,
initializing it to init
.
val new_counter: int -> St (unit -> St int)
let new_counter init =
let c = ST.alloc init in
fun () -> c := !c + 1; !c
F* can show that new_counter
has type int -> St (unit -> St int)
,
the type of a function that given an integer, may read, write or
allocate references, and then returns a unit -> St unit
function. Using sub-effecting, we can also write the type below
and F* will check that new_counter
has that type as well.
val new_counter: int -> ML (unit -> ML int)
Note, the type above, is not the same as int -> unit -> ML int
.
The latter is a shorthand for int -> Tot (unit -> ML int)
.
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.
One way to prove properties about your code in F* is to write assertions.
let _ = assert (max 0 1 = 1)
Our first assertion is an obvious property about max
. You may have seen
a construct called assert
in other languages—typically, it is used to
check a property of your code at runtime, raising an assertion-failed
exception if the asserted condition is not true
.
In F*, assertions have no runtime significance. Instead, F* checks statically (i.e. before compiling your program) that the asserted condition is always true, and hence could never fail.
In this case, the proof that max 0 1 = 1
is fairly easy. Under the
covers, F* translates the definition of max
and the asserted property
to a theorem prover called Z3, which then proves the property
automatically.
We can assert and automatically check more general properties about max
. For example:
let _ = assert (forall x y. max x y >= x
&& max x y >= y
&& (max x y = x || max x y = y))
Let's take a look at the factorial function:
let rec factorial n =
if n = 0 then 1 else n * (factorial (n - 1))
By default the .
op_Star
operator of F* (the *
above) is the type constructor of product types also known as tuples. If, as in the example above, we are not doing anything with tuples, it is convenient to open the module FStar.Mul
to let *
be multiplication. Otherwise, one has to write op_Multiply a b
instead of a * b
.
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
.
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:
factorial
is a value (that's the 'val factorial
' part)
It is a function (that's the arrow type '->
')
It can only be applied to integers x
that are greater than or
equal to 0
(that's the refinement type 'x:int{x>=0}
')
When applied to x
it always terminates, has no effects (the
'Tot
' part), and returns an integer (the result type 'int
')
Once we write this down, F* automatically proves that factorial
satisfies all these properties. The main interesting bit to prove, of
course, is that factorial x
actually does terminate when x
is
non-negative. We'll get into the details of how this is done in
section 5, but, for now, it suffices to know that in
this case F* is able to prove that every recursive call is
on a non-negative number that is strictly smaller than the argument of
the previous call. Since this cannot go on forever (we'll eventually hit
the base case 0
), F* agrees with our claim about the type of
factorial
.
The type of non-negative integers (or natural numbers) is common enough that you can define an abbreviation for it (in fact, F* already does this for you in its standard prelude).
type nat = x:int{x>=0}
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
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
(*
Copyright 2008-2018 Microsoft Research
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
module Ex03b
//fibonacci
(* val fibonacci : int -> int *)
(* val fibonacci : int -> ML int (same as above) *)
(* val fibonacci : int -> Tot nat *)
(* val fibonacci : int -> Tot (y:int{y>=1}) *)
(* val fibonacci : x:int -> Tot (y:int{y>=1 /\ y >= x}) *)
(* val fibonacci : x:int -> Tot *)
(* (y:int{y >= 1 /\ y >= x /\ (x>=3 ==> y>=2)}) *)
val fibonacci : int -> Tot (x:nat{x>0})
let rec fibonacci n =
if n <= 1 then 1 else fibonacci (n - 1) + fibonacci (n - 2)
code/solutions/Ex03b.fstLoad in editor
Let's say you wrote the factorial
function and gave it the type
(nat -> Tot nat)
. Later, you care about some other property about
factorial
, e.g., that if x > 2
then factorial x > x
. One option is
to revise the type you wrote for factorial
and get F* to reprove that
it has this type. But this isn't always feasible. What if you also wanted
to prove that if x > 3
then factorial x > 2 * x
: clearly, polluting
the type of factorial
with all these properties that you may or may not
care about is impractical.
However, F* will allow you to write other functions (we call them
lemmas) to prove more properties about factorial
, after you've defined
factorial
and given it some generally useful type like
nat -> Tot nat
.
A lemma is a ghost total function that always returns the single unit
value
()
. As such, computationally, lemmas are useless—they have no effect
and always return the same value, so what's the point? The point is that
the type of the value returned by the lemma carries some useful
properties about your program.
As a first lemma about factorial
, let's prove that it always
returns a positive number.
val factorial_is_positive: x:nat -> GTot (u:unit{factorial x > 0})
let rec factorial_is_positive x =
match x with
| 0 -> ()
| _ -> factorial_is_positive (x - 1)
The statement of the lemma is the type given to factorial_is_positive
,
a ghost total function on x:nat
which returns a unit, but with the refinement
that factorial x > 0
. The next three lines define
factorial_is_positive
and proves the lemma using a proof by induction
on x
. The basic concept here is that by programming total functions, we
can write proofs about other pure expressions. We'll discuss such proofs
in detail in the remainder of this section.
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.
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:
x_{1}:t_{1} -> ... -> E_{n} x_{n}:t_{n}[x_{1} ... x_{n-1}] -> E t[x_{1} ... x_{n}]
Each of a function's formal parameters are named
x_{i}
and each of these names is in scope to the right of the first
arrow that follows it. The notation t[x_{1} ... x_{m}]
indicates that
the variables x_{1} ... x_{m}
may appear free in t
.
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_arg_{1}: x:(y:nat{y > 2}) -> GTot (u:unit{factorial x > x})
This does the job, but the type of the function's argument is a bit
clumsy, since we needed two names: y
to restrict the domain to natural
numbers greater than 2
and x
to speak about the argument in the
result type. This pattern is common enough that F* provides some
syntactic sugar for it—we have seen it already in passing in the first
type we gave to factorial
. Using it, we can write the following type,
which is equivalent to, but more concise than, the type above.
val factorial_is_greater_than_arg_{2}: 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_arg_{2}
is equivalent to the
type of factorial_is_greater_than_arg_{3}
(below), which is just a little
easier to read and write.
val factorial_is_greater_than_arg_{3}: 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_arg_{4}: 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.
Now, let's look at a proof of factorial_is_greater_than_arg
in detail. Here it is:
let rec factorial_is_greater_than_arg x =
match x with
| 3 -> ()
| _ -> factorial_is_greater_than_arg (x - 1)
The proof is a recursive function (as indicated by the let rec
); the
function is defined by cases on x
.
In the first case, the argument is 3
; so, we need to prove that
factorial 3 > 3
. F* generates a proof obligation corresponding to this
property and asks Z3 to see if it can prove it, given the definition of
factorial
that we provided earlier—Z3 figures out that by
factorial 3 = 6
and, of course, 6 > 3
, and the proof for this case is
done. This is the base case of the induction.
The cases are taken in order, so if we reach the second case, then we
know that the first case is inapplicable, i.e., in the second case, we
know from the type for factorial_is_greater_than_arg
that x:nat{x > 2}
, and
from the inapplicability of the previous case that x <> 3
. In other
words, the second case is the induction step and handles the proof when
x > 3
.
Informally, the proof in this case works by using the induction hypothesis, which gives us that
forall n, 2 < n < x ==> factorial n > n
and our goal is to prove factorial x > x
. Or, equivalently, that
x * factorial (x - 1) > x
, knowing that factorial (x - 1) > x - 1
; or
that x*x - x > x
—which is true for x > 3
.
Let's see how this works formally in F*.
When defining a total recursive function, the function being defined
(factorial_is_greater_than_arg
in this case) is available for use in the body
of the definition, but only at a type that ensures that the recursive
call will terminate. In this case, the type of factorial_is_greater_than_arg
in
the body of the definition is:
n:nat{2 < n && n < x} -> Lemma (factorial n > n)
This is, of course, exactly our induction hypothesis. By calling
factorial_is_greater_than_arg (x - 1)
in the second case, we, in effect, make
use of the induction hypothesis to prove that
factorial (x - 1) > x - 1
, provided we can prove that
2 < x - 1 && x - 1 < x
—we give this to Z3 to prove, which it can,
since in this case we know that x > 3
. Finally, we have to prove the
goal factorial x > x
from the x > 3
and the property we obtained
from our use of the induction hypothesis: again, Z3 proves this easily.
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
let rec fibonacci_greater_than_arg n =
match n with
| 2 -> ()
| _ -> fibonacci_greater_than_arg (n-1)
(*
Z_{3} proves the base case.
The proof uses the induction hypothesis:
forall x, 2 <= x < n ==> fibonacci x >= x
Our goal is to prove that:
fibonacci n >= n or equivalently fibonacci (n-1) + fibonacci (n-2) > n
We make use of induction hypothesis to prove that
fibonacci (n-1) >= n-1
For fibonacci (n-1) we use the property
forall x, fibonacci x > 1
This can be seen by giving fibonacci the stronger type
val fibonacci : nat -> Tot (r:nat{r>=1})
From this Z_{3} can proves the post condition
*)
code/solutions/Ex03c.fstLoad in editor
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.
bool
versus Type
You can probably skip this section on a first reading, if the title sounds mysterious to you. However, as you start to use quantified formulas in refinement types, you should make sure you understand this section.
We mentioned earlier that a refinement type has the form x:t{phi(x)}
.
In its primitive form, phi
is in fact a type, a predicate on the value
x:t
. We allow you to use a boolean function in place of a type: under
the covers, we implicitly coerce the boolean to a type, by adding the
coercion
b2t (b:bool) : Type = (b == true)
The type '==
' is the type constructor for the homogeneous equality
predicate; it is different from '=
‘, which is a boolean function
comparing a pair of values (F* also has a separate constructor for
heterogeneous equality, ’===
').
Equality is more complex than it looks! See also . equality on F* wiki.
The propositional connectives, /\
, \/
, and ~
, for conjunction,
disjunction and negations are type constructors. We also include ==>
and <==>
for single and bidirectional implication. In contrast,
&&
, ||
, and not
are boolean functions.
Often, because of the implicit conversion from bool
to Type
, you
can almost ignore the distinction between the two. However, when you
start to write refinement formulas with quantifiers, the distinction
between the two will become apparent.
Both the universal quantifier forall
and the existential quantifier
exists
, are only available in Type
. When you mix refinements that
include boolean function and the quantifiers, you need to use the
propositional connectives. For example, the following formula
is well-formed:
canRead e /\ forall x. canWrite x ==> canRead x
It is a shorthand for the following, more elaborate form:
b2t(canRead e) /\ forall x. b2t(canWrite x) ==> b2t(canRead x)
On the other hand, the following formula is not well-formed; F* will reject it:
canRead e && forall x. canWrite x ==> canRead x
The reason is that the quantifier is a type, whereas the &&
operator
expects a boolean. While a boolean can be coerced to a type, there is no
coercion in the other direction.
Here's the standard definition of (immutable) lists in F*.
type list 'a =
| Nil : list 'a
| Cons : hd:'a -> tl:list 'a -> list 'a
We note some important conventions for the constructors of a data type in F*.
Constructor names must begin with a capital letter.
When not writing effects in constructor types,
the default effect on the result is Tot
.
So, when we write Cons: 'a -> list 'a -> list 'a
, F* desugars it to
Cons: 'a -> Tot (list 'a -> Tot (list 'a))
.
Constructors can be curried. So, we usually define our inductive
types as above so that we write Cons hd tl
(curried)
rather than Cons(hd,tl)
(uncurried).
Constructors can be partially applied, so Cons hd
is legal and has
type list 'a -> Tot (list 'a)
when hd:'a
.
The list
type is defined in F*'s standard prelude and is available
implicitly in all F* programs. We provide special (but standard) syntax
for the list constructors:
[]
is Nil
[v_{1}; ...; vn]
is Cons v_{1} ... (Cons vn Nil)
hd :: tl
is Cons hd tl
.
You can always just write out the constructors like Nil
and Cons
explicitly, if you find that useful (e.g., to partially apply Cons
).
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 l_{1} l_{2} = match l_{1} with
| [] -> l_{2}
| hd :: tl -> hd :: append tl l_{2}
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.
l_{1}:list 'a -> l_{2}:list 'a -> Tot (l:list 'a{length l = length l_{1} + length l_{2}})
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
val append_len: l_{1}:list 'a -> l_{2}:list 'a
-> Lemma (requires True)
(ensures (length (append l_{1} l_{2}) = length l_{1} + length l_{2})))
let rec append_len l_{1} l_{2} = match l_{1} with
| [] -> ()
| hd::tl -> append_len tl l_{2}
code/solutions/Ex04b.fstLoad in editor
We wrote the type of the function append
above using an ML-like type
variable 'a
to stand for an arbitrary type. Under the hood F*
expands this out to something like this:
val append : #a:Type -> list a -> list a -> Tot (list a)
let rec append #a l_{1} l_{2} = match l_{1} with
| [] -> l_{2}
| hd :: tl -> hd :: append #a tl l_{2}
This exposes the fact that a
is really just an implicit argument of
append
. The implicit argument a
is preceded by the #
symbol
both in the type of append, where we say that a
has type Type
,
and in the definition of append, which takes an extra a
argument.
When calling append
recursively we have a choice, we can either
pass a
explicitly by preceding it with the #
sign, or we can
leave it out and the F* type-checker will infer it automatically.
(Implicit arguments are further discussed in 8.3.1.)
We would like to define a function mem: x:'a -> l:list 'a -> Tot bool
that decides whether x
is present in a list l
or
not. However, not all types in F* have decidable equality, so in
order to write mem
we cannot quantify over arbitrary types, but only
over those with decidable equality. Thus the following definition of
mem
has to use #a:Type{hasEq a}
instead of #a:Type
(hasEq a
holds if a
has decidable equality—that is, if there exists a
function eq_a: a -> a -> Tot bool
such that eq_a a_{1} a_{2}
iff.
a_{1} == a_{2}
). For convenience, the standard library provides eqtype
as an abbreviation of a: Type{hasEq a}
.
val mem: #a:eqtype -> a -> list a -> Tot bool
let rec mem #a x xs =
match xs with
| [] -> false
| hd :: tl -> hd = x || mem x tl
Exercise 4c:
Prove that mem
satisfies the
following property:
val append_mem: #a:eqtype -> l_{1}:list a -> l_{2}:list a -> x:a
-> Lemma (mem x (append l_{1} l_{2}) <==> mem x l_{1} || mem x l_{2})
code/exercises/Ex04c.fstLoad in editor
let rec append_mem #a l_{1} l_{2} x =
match l_{1} with
| [] -> ()
| hd::tl -> append_mem tl l_{2} x
(*
Z_{3} proves the base case: mem x (append [] l) <==> mem x l_{2}.
The proof uses the induction hypothesis:
tl << l_{1} ==> mem x (append tl l_{2}) <==> mem x tl || mem x l_{2}.
Our goal is to prove that:
mem x (append l_{1} l_{2}) <==> mem x l_{1} || mem x l_{2}) or equivalently
let hd::tl = l_{1} in mem x (hd::(append tl l_{2})) <==> hd=x || mem x tl || mem x l_{2}.
From this Z_{3} can proves the post condition.
*)
code/solutions/Ex04c.fstLoad in editor
As the previous exercises illustrate, you can prove properties either
by enriching the type of a function or by writing a separate lemma
about it—we call these the ‘intrinsic’ and ‘extrinsic’ styles,
respectively. Which style to prefer is a matter of taste and
convenience: generally useful properties are often good candidates for
intrinsic specification (e.g, that length
returns a nat
); more
specific properties are better stated and proven as lemmas. However,
in some cases, as in the following example, it may be impossible to
prove a property of a function directly in its type—you must resort
to a lemma.
val reverse: list 'a -> Tot (list 'a)
let rec reverse = function
| [] -> []
| hd :: tl -> append (reverse tl) [hd]
Let's try proving that reversing a list twice is the identity function.
It's possible to
specify this property in the type of reverse
using a refinement type.
val reverse: #a:Type -> f:(list a -> Tot (list a)){forall l. l == f (f l)}
However, F* refuses to accept this as a valid type for reverse
:
proving this property requires two separate inductions, neither of
which F* can perform automatically.
Instead, one can use two lemmas to prove the property we care about. Here it is:
let snoc l h = append l [h]
val snoc_cons: l:list 'a -> h:'a -> Lemma (reverse (snoc l h) == h :: reverse l)
let rec snoc_cons l h = match l with
| [] -> ()
| hd :: tl -> snoc_cons tl h
val rev_involutive: l:list 'a -> Lemma (reverse (reverse l) == l)
let rec rev_involutive l = match l with
| [] -> ()
| hd :: tl ->
// (1) [reverse (reverse tl) == tl]
rev_involutive tl;
// (2) [reverse (append (reverse tl) [hd]) == h :: reverse (reverse tl)]
snoc_cons (reverse tl) hd
// These two facts are enough for Z_{3} to prove the lemma:
// reverse (reverse (hd :: tl))
// =def= reverse (append (reverse tl) [hd])
// =(2)= hd :: reverse (reverse tl)
// =(1)= hd :: tl
// =def= l
In the Cons
case of rev_involutive
we are explicitly applying not just
the induction hypothesis but also the snoc_cons
lemma we proved above.
Exercise 4d:
Prove that reverse is injective, i.e.,
val rev_injective : l_{1}:list 'a -> l_{2}:list 'a
-> Lemma (requires (reverse l_{1} == reverse l_{2}))
(ensures (l_{1} == l_{2}))
code/exercises/Ex04d.fstLoad in editor
Perhaps you did it like this:
val snoc_injective: l_{1}:list 'a -> h_{1}:'a -> l_{2}:list 'a -> h_{2}:'a
-> Lemma (requires (snoc l_{1} h_{1} == snoc l_{2} h_{2}))
(ensures (l_{1} == l_{2} /\ h_{1} == h_{2}))
let rec snoc_injective l_{1} h_{1} l_{2} h_{2} = match l_{1}, l_{2} with
| _::tl_{1}, _::tl_{2} -> snoc_injective tl_{1} h_{1} tl_{2} h_{2}
| _ -> ()
val rev_injective_{1}: l_{1}:list 'a -> l_{2}:list 'a
-> Lemma (requires (reverse l_{1} == reverse l_{2}))
(ensures (l_{1} == l_{2})) (decreases l_{1})
let rec rev_injective_{1} l_{1} l_{2} =
match l_{1},l_{2} with
| h_{1}::t_{1}, h_{2}::t_{2} ->
// assert(reverse (h_{1}::t_{1}) = reverse (h_{2}::t_{2}));
// assert(snoc (reverse t_{1}) h_{1} = snoc (reverse t_{2}) h_{2});
snoc_injective (reverse t_{1}) h_{1} (reverse t_{2}) h_{2};
// assert(reverse t_{1} = reverse t_{2} /\ h_{1} = h_{2});
rev_injective_{1} t_{1} t_{2}
// assert(t_{1} = t_{2} /\ h_{1}::t_{1} = h_{2}::t_{2})
| _, _ -> ()
code/solutions/Ex04d.fstLoad in editor
That's quite a tedious proof, isn't it. Here's a simpler proof.
val rev_injective_{2}: l_{1}:list 'a -> l_{2}:list 'a
-> Lemma (requires (reverse l_{1} == reverse l_{2}))
(ensures (l_{1} == l_{2}))
let rev_injective_{2} #t l_{1} l_{2} = rev_involutive l_{1}; rev_involutive l_{2}
code/solutions/Ex04d.fstLoad in editor
The rev_injective_{2}
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 l_{1}
and once for l_{2}
.
This gives to the SMT solver the information that reverse (reverse
l_{1}) = l_{1}
and reverse (reverse l_{2}) = l_{2}
, which suffices to complete
the proof. As usual, when structuring proofs, lemmas are your friends!
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 [a_{1}; ...; a_{n}]
produces the list
[f a_{1}; ...; f a_{n}]
. For example:
map (fun x -> x + 1) [0; 1; 2] = [1; 2; 3]
As usual, without any specification, F* will infer for map
type
('a -> 'b) -> list 'a -> list 'b
. Written explicitly, the type of
map
is ('a -> Tot 'b) -> Tot (list 'a -> Tot (list 'b))
. Notice
that the type of f
also defaults to a function with Tot
effect.
By adding a type annotation we can give a different type to map
:
val map: ('a -> ML 'b) -> list 'a -> ML (list 'b)
This type is neither a subtype nor a supertype of the type F* inferred
on its own (for example, the manual annotation above allows you to write
map (fun x -> FStar.IO.print_any x) l
, whereas the automatically inferred
type does not.
No parametric polymorphism on effects: You might hope to give
map
a very general type, one that accepts a function with any effectE
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.
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.
(*
Copyright 2008-2018 Microsoft Research
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
module Ex04e
//find
type option 'a =
| None : option 'a
| Some : v:'a -> option 'a
(* The intrinsic style is more convenient in this case *)
val find : f:('a -> Tot bool) -> list 'a -> Tot (option (x:'a{f x}))
let rec find f l = match l with
| [] -> None
| hd :: tl -> if f hd then Some hd else find f tl
(* Extrinsically things are more verbose, since we are basically duplicating
the structure of find in find_some. It's still not too bad. *)
val find' : #t:Type -> f:(t -> Tot bool) -> list t -> Tot (option t)
let rec find' #t f l = match l with
| [] -> None
| hd :: tl -> if f hd then Some hd else find' f tl
val find_some : f:('a -> Tot bool) -> xs:(list 'a) ->
Lemma (None? (find' f xs) || f (Some?.v (find' f xs)))
let rec find_some f xs =
match xs with
| [] -> ()
| x :: xs' -> find_some f xs'
(* [Some?.v] and [None?] are convenient ways to manipulate options. They are
described later in the tutorial. Here's a more verbose way to achieve the
same thing: *)
val find_some' : f:('a -> Tot bool) -> xs:(list 'a) ->
Lemma (match find f xs with
| None -> true
| Some v -> f v)
let rec find_some' f xs =
match xs with
| [] -> ()
| x :: xs' -> find_some' f xs'
code/solutions/Ex04e.fstLoad in editor
Exercise 4f:
Define the fold_left
function on lists, so that
fold_left f [b_{1}; ...; bn] a = f (bn, ... (f b_{2} (f b_{1} a)))
Prove that (fold_left Cons l [] == reverse l)
.
(The proof is a level harder from what we've done so far. You will need to
strengthen the induction hypothesis, and possibly to prove that append
is
associative)
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
val fold_left: f:('b -> 'a -> Tot 'a) -> l:list 'b -> 'a -> Tot 'a
let rec fold_left f l a = match l with
| Nil -> a
| Cons hd tl -> fold_left f tl (f hd a)
val append_assoc : #a:Type -> l_{1}:list a -> l_{2}:list a -> l_{3}: list a ->
Lemma (append l_{1} (append l_{2} l_{3}) == append (append l_{1} l_{2}) l_{3})
let rec append_assoc #a l_{1} l_{2} l_{3} =
match l_{1} with
| [] -> ()
| h_{1} :: t_{1} -> append_assoc t_{1} l_{2} l_{3}
let rec fold_left_Cons_is_rev #a (l_{1} l_{2}: list a) :
Lemma (fold_left Cons l_{1} l_{2} == append (reverse l_{1}) l_{2}) =
match l_{1} with
| [] -> ()
| h_{1} :: t_{1} ->
// (1) [append (append (reverse t_{1}) [h_{1}]) l_{2}
// == append (reverse t_{1}) (append [h_{1}] l_{2})]
append_assoc (reverse t_{1}) [h_{1}] l_{2};
// (2) [fold_left Cons t_{1} (h_{1} :: l_{2}) = append (reverse t_{1}) (h_{1} :: l_{2})]
fold_left_Cons_is_rev t_{1} (h_{1} :: l_{2})
// append (reverse l_{1}) l_{2}
// =def= append (append (reverse t_{1}) [h_{1}]) l_{2}
// =(1)= append (reverse t_{1}) (append [h_{1}] l_{2})
// =def= append (reverse t_{1}) (h_{1} :: l_{2})
// =(2)= fold_left Cons t_{1} (h_{1} :: l_{2})
// =def= fold_left Cons l_{1} l_{2}
code/solutions/Ex04f.fstLoad in editor
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
A discriminator is a boolean-valued total function that tests whether a
term is the application of a particular constructor. For the list
type,
we have two discriminators that are automatically generated.
val Nil?: list 'a -> Tot bool
let Nil? xs = match xs with | [] -> true | _ -> false
val Cons?: list 'a -> Tot bool
let Cons? xs = match xs with | _ :: _ -> true | _ -> false
Identifiers like Nil?
and Cons?
cannot be defined by the user
directly. They are reserved to be automatically generated by the
compiler. So, the above code will not typecheck as written—it's only
for illustration purposes.
From the type of the Cons
constructor, F* generates the following
signatures:
val Cons?.hd : l:list 'a{Cons? l} -> Tot 'a
val Cons?.tl : l:list 'a{Cons? l} -> Tot (list 'a)
This indicates why the names hd
and tl
in the types of Cons
are
significant: they correspond to the names of the auto-generated
projectors. If you don't name the arguments of a data constructor, F*
will generate names automatically (although these names are derived from
the position of the arguments and their form is unspecified; so, it's
good practice to name the arguments yourself).
Again, names like Cons?.hd
are reserved for internal use.
Exercise 4g:
Write functions (call them hd
and tl
) whose types match
those of Cons?.hd
and Cons?.tl
.
(*
Copyright 2008-2018 Microsoft Research
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
module 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
(*
Copyright 2008-2018 Microsoft Research
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
module Ex04g
//hd-tl
val hd : l:list 'a{Cons? l} -> Tot 'a
let hd l =
match l with
| h :: t -> h
val tl : l:list 'a{Cons? l} -> Tot (list 'a)
let tl l =
match l with
| h :: t -> t
code/solutions/Ex04g.fstLoad in editor
Exercise 4h:
Write a function that returns the n
th element of a list. Give a
type that ensures it is total.
(* Write your code here *)
code/exercises/Ex04h.fstLoad in editor
val nth : l:list 'a -> n:nat{n < length l} -> 'a
let rec nth l n =
match l with
| h :: t -> if n = 0 then h else nth t (n - 1)
(* Note how the solution above omits the [] case: that's because whenever you
pattern match a term (to analyze it by cases), F\* insists on proving that you
have handled all the cases. We call this the 'exhaustiveness check', and unlike
in F\# or OCaml, it is implemented semantically. *)
code/solutions/Ex04h.fstLoad in editor
F* provides syntactic sugar for tuples. Under the covers, tuples are just inductive types: tuples of size 2–8 are defined in the standard prelude. (You can add to this, if you like.) Here's the definition of pairs from the prelude:
type tuple_{2} 'a 'b =
| MkTuple_{2}: _1:'a -> _2:'b -> tuple_{2} 'a 'b
You can write (5, 7)
instead of MkTuple_{2} 5 7
, and give it the type
(int * int)
as a shorthand for tuple_{2} 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
In F* every pure function is proved to terminate. The termination check used by F* is based on a semantic criterion, not syntactic conditions. We quickly sketch the basic structure of the F* termination check—you'll need to understand a bit of this in order to write more interesting programs.
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 v_{1} << v_{2}
when v_{1}
precedes v_{2}
in this order.
A relation
R
is a well-founded partial order on a setS
if, and only if,R
is a partial order onS
and there are no infinite descending chains inS
related byR
. For example, takingS
to benat
, 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.
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.
The subterm ordering on inductive types: For any value
v = D v_{1} ... vn
of an inductive type (where D
is a constructor applied
to arguments v_{1}
to vn
) we include vi << v
, for all i
.
That is, the sub-terms of a well-typed constructed term
precede the constructed term. (The exception to this rule is lex_t
below).
The lexicographic ordering on lex_t, as described below.
Take a look at the classic function, ackermann
:
val ackermann: m:nat -> n:nat -> Tot nat
let rec ackermann m n =
if m=0 then n + 1
else if n = 0 then ackermann (m - 1) 1
else ackermann (m - 1) (ackermann m (n - 1))
Why does it terminate? At each recursive call, it is not the case that
all the arguments are strictly less than the arguments at the previous
call, e.g, in the second branch, n
increases from 0
to 1
. However,
this function does in fact terminate, and F* proves that it does.
The reason is that although each argument does not decrease in every
recursive call, when taken together, the ordered pair of arguments (m,n)
does decrease according to a lexical ordering on pairs.
In its standard prelude, F* defines the following inductive type:
type lex_t =
| LexTop : lex_t
| LexCons : #a:Type -> a -> lex_t -> lex_t
(The #
sign marks the first argument as implicit, see 8.3.1.)
This is a list of heterogenously typed elements.
The lexicographic ordering on lex_t
is the following:
LexCons v_{1} v_{2} << LexCons v_{1}' v_{2}'
, if and only if, either
v_{1} << v_{1}'
; or v_{1}===v_{1}'
and v_{2} << v_{2}'
.
If v:lex_t
and v <> LexTop
, then v << LexTop
.
We include the following syntactic sugar:
%[v_{1};...;v_{n}]
is shorthand for(LexCons v_{1} ... (LexCons v_{n} LexTop))
Suppose we are defining a function by recursion, using the following form:
val f: y_{1}:t_{1} -> .. -> yn:t_{n} -> Tot t
let rec f x_{1} .. xn = e
Usually, in ML, when type-checking e
, the recursively bound function
f
is available for use in e
at the type
y_{1}:t_{1} -> .. -> yn:t_{n} -> 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:
y_{1}:t_{1}
-> ...
-> yn:t_{n}{%[y_{1};...;y_{n}] << %[x_{1};...;x_{n}]}
-> Tot t
That is, by default, F* requires the function's parameters to decrease according to the lexical ordering of the parameters (in the order in which they appear, excluding all function-typed parameters). (There is a way to override this default—see Section 5.2.2.)
Let's see how this works on a couple of examples.
F* can show automatically that the ackermann
function
(* 1 *) let rec ackermann m n =
(* 2 *) if m=0 then n + 1
(* 3 *) else if n = 0 then ackermann (m - 1) 1
(* 4 *) else ackermann (m - 1)
(* 5 *) (ackermann m (n - 1))
is terminating and has type:
ackermann : nat -> nat -> Tot nat
F* gives this function a default termination metric, so this expands out to:
ackermann : m:nat -> n:nat -> Tot nat (decreases %[m;n])
The decreases
clause will be discussed in the next section. In this
example it leads to the F* type-checker using the following more
restrictive type for the recursive calls in the body of ackermann
:
ackermann: m':nat
-> n':nat{%[m';n'] << %[m;n]}
-> Tot nat
At each of three recursive calls to ackermann
, we need to prove not
only that the arguments are non-negative, but that they precede the
previous arguments according to the refinement formula above.
For the call at line 3, we have to show that %[(m - 1);1] << %[m;n]
.
This works out, since m - 1 << m
according to the integer ordering, and
we can disregard the rest of the terms.
The call at line 4 verifies for the same reason—the first argument decreases.
For the call at line 5, we have to show that %[m; (n-1)] << %[m; n]
.
Here, the first elements of each pair are equal, so we look at the second
element, and there n - 1 << n
, and we're done.
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 : l_{1}:list 'a -> l_{2}:list 'a -> Tot (list 'a) (decreases l_{2})
let rec rev l_{1} l_{2} =
match l_{2} with
| [] -> l_{1}
| hd :: tl -> rev (hd :: l_{1}) 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
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 : l_{1}:list 'a -> l_{2}:list 'a -> Lemma
(ensures (rev l_{1} l_{2} = append (reverse l_{2}) l_{1})) (decreases l_{2})
let rec rev_is_ok_aux l_{1} l_{2} =
match l_{2} with
| [] -> ()
| hd :: tl -> rev_is_ok_aux (hd :: l_{1}) tl; append_assoc (reverse tl) [hd] l_{1}
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 (linear-time)
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
val fib_is_ok_aux : (n: nat) -> (k: nat) ->
Lemma (fib (fibonacci k) (fibonacci (k + 1)) n == fibonacci (k + n))
let rec fib_is_ok_aux n k =
if n = 0 then () else fib_is_ok_aux (n - 1) (k + 1)
val fib_is_ok : n:nat -> Lemma (fib 1 1 n = fibonacci n)
let fib_is_ok n = fib_is_ok_aux n 0
code/solutions/Ex05b.fstLoad in editor
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
.
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.
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.
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
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 l_{1}, l_{2} = partition f tl in
if f hd
then hd::l_{1}, l_{2}
else l_{1}, hd::l_{2}
code/solutions/Ex06a.fstLoad in editor
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 sort_{0}: l:list int -> Tot (m:list int{sorted m /\ (forall i. mem i l <==> mem i m) })
Unsurprisingly, it fails, on several counts:
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.
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
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 section—once we have introduced some additional
machinery.
val sorted_concat_lemma: l_{1}:list int{sorted l_{1}}
-> l_{2}:list int{sorted l_{2}}
-> pivot:int
-> Lemma (requires ((forall y. mem y l_{1} ==> not (pivot <= y))
/\ (forall y. mem y l_{2} ==> pivot <= y)))
(ensures (sorted (append l_{1} (pivot :: l_{2}))))
let rec sorted_concat_lemma l_{1} l_{2} pivot = match l_{1} with
| [] -> ()
| hd :: tl -> sorted_concat_lemma tl l_{2} pivot
Finally, we also need a lemma about append
and mem
:
val append_mem: l_{1}:list 'a
-> l_{2}:list 'a
-> Lemma (requires True)
(ensures (forall a. mem a (append l_{1} l_{2}) = (mem a l_{1} || mem a l_{2})))
let rec append_mem l_{1} l_{2} = match l_{1} with
| [] -> ()
| hd :: tl -> append_mem tl l_{2}
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.
If only we had given partition
and sorted
richer intrinsic types,
types that captured the properties that we proved using lemmas, we
wouldn't have had to pollute our implementation of quicksort. This is
a significant advantage of using the intrinsic proof style—every
call of a function like partition (fun x -> pivot <= x) tl
immediately carries all the properties that were proven intrinsically
about the function.
However, polluting the type of a general-purpose function with a very
application-specific type would also be awful. Consider enriching the
type of sorted
with the property proven by
sorted_concat_lemma
. The lemma is highly specialized for the
quicksort algorithm, whereas sorted
is a nice, general specification
of sortedness that would work for insertion sort or merge sort, just
as well. Polluting its type is a non-starter. So, it seems we are
caught in a bind.
Wouldn't it be nice if there were some way to retroactively associate
a property proven about a function f
by a lemma directly with f
,
so that every application f x
immediately carries the lemma
properties? F* provides exactly such a mechanism, which gives a
way to bridge the gap between extrinsic and intrinsic proofs.
Let's say we wrote the type of partition_lemma
as below—the only
difference is in the very last line, the addition of [SMTPat
(partition f l)]
. That line instructs F* and the SMT solver to
associate with every occurrence of the term partition f l
the
property proven by the lemma.
val partition_lemma: f:('a -> Tot bool)
-> l:list 'a
-> Lemma (requires True)
(ensures ((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 :: l_{2}))
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: l_{1}:list int{sorted l_{1}}
-> l_{2}:list int{sorted l_{2}}
-> pivot:int
-> Lemma (requires ((forall y. mem y l_{1} ==> not (pivot <= y))
/\ (forall y. mem y l_{2} ==> pivot <= y)))
(ensures (sorted (append l_{1} (pivot :: l_{2}))))
[SMTPat (sorted (append l_{1} (pivot :: l_{2})))]
Finally, we also revise the type for append_mem
in the same way:
val append_mem: l_{1}:list 'a
-> l_{2}:list 'a
-> Lemma (requires True)
(ensures (forall a. mem a (append l_{1} l_{2}) = (mem a l_{1} || mem a l_{2})))
[SMTPat (append l_{1} l_{2})]
let rec append_mem l_{1} l_{2} = match l_{1} with
| [] -> ()
| hd :: tl -> append_mem tl l_{2}
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)
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
(*
Copyright 2008-2018 Microsoft Research
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
module Ex06b
//quick-sort-poly
val mem: #t:eqtype -> t -> list t -> Tot bool
let rec mem #t a l = match l with
| [] -> false
| hd::tl -> hd=a || mem a tl
val append : list 'a -> list 'a -> Tot (list 'a)
let rec append l_{1} l_{2} = match l_{1} with
| [] -> l_{2}
| hd :: tl -> hd :: append tl l_{2}
val append_mem: #t:eqtype
-> l_{1}:list t
-> l_{2}:list t
-> Lemma (requires True)
(ensures (forall a. mem a (append l_{1} l_{2}) = (mem a l_{1} || mem a l_{2})))
[SMTPat (append l_{1} l_{2})]
let rec append_mem #t l_{1} l_{2} = match l_{1} with
| [] -> ()
| hd::tl -> append_mem tl l_{2}
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 l_{1}, l_{2} = partition f tl in
if f hd
then hd::l_{1}, l_{2}
else l_{1}, hd::l_{2}
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 a_{1} a_{2}. (f a_{1} a_{2} /\ a_{1}<>a_{2}) <==> not (f a_{2} a_{1})) (* anti-symmetry *)
/\ (forall a_{1} a_{2} a_{3}. f a_{1} a_{2} /\ f a_{2} a_{3} ==> f a_{1} a_{3}) (* transitivity *)
val sorted_concat_lemma: #t:eqtype
-> f:(t -> t -> Tot bool)
-> l_{1}:list t{sorted f l_{1}}
-> l_{2}:list t{sorted f l_{2}}
-> pivot:t
-> Lemma (requires (total_order t f
/\ (forall y. mem y l_{1} ==> not (f pivot y))
/\ (forall y. mem y l_{2} ==> f pivot y)))
(ensures (sorted f (append l_{1} (pivot::l_{2}))))
[SMTPat (sorted f (append l_{1} (pivot::l_{2})))]
let rec sorted_concat_lemma #t f l_{1} l_{2} pivot = match l_{1} with
| [] -> ()
| hd::tl -> sorted_concat_lemma f tl l_{2} pivot
val sort: #t:eqtype -> f:(t -> t -> Tot bool){total_order t f}
-> l:list t
-> Tot (m:list t{sorted f m /\ (forall i. mem i l = mem i m)})
(decreases (length l))
let rec sort #t f l = match l with
| [] -> []
| pivot::tl ->
let hi, lo = partition (f pivot) tl in
let m = append (sort f lo) (pivot::sort f hi) in
assert (forall i. mem i (pivot :: sort f hi) = mem i (append [pivot] (sort f hi)));
m
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
The specification does not ensure that the resulting list is a permutation of the initial list: it could discard or repeat some elements.
(*
Copyright 2008-2018 Microsoft Research
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
module 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 l_{1} l_{2} = match l_{1} with
| [] -> l_{2}
| hd :: tl -> hd :: hd :: append tl l_{2}
val append_mem: #t:eqtype -> l_{1}:list t
-> l_{2}:list t
-> Lemma (requires True)
(ensures (forall a. mem a (append l_{1} l_{2}) = (mem a l_{1} || mem a l_{2})))
[SMTPat (append l_{1} l_{2})]
let rec append_mem #t l_{1} l_{2} = match l_{1} with
| [] -> ()
| hd::tl -> append_mem tl l_{2}
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 l_{1}, l_{2} = partition f tl in
if f hd
then hd::l_{1}, l_{2}
else l_{1}, hd::l_{2}
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: l_{1}:list int{sorted l_{1}}
-> l_{2}:list int{sorted l_{2}}
-> pivot:int
-> Lemma (requires ((forall y. mem y l_{1} ==> not (pivot <= y))
/\ (forall y. mem y l_{2} ==> pivot <= y)))
(ensures (sorted (append l_{1} (pivot::l_{2}))))
[SMTPat (sorted (append l_{1} (pivot::l_{2})))]
let rec sorted_concat_lemma l_{1} l_{2} pivot = match l_{1} with
| [] -> ()
| hd::tl -> sorted_concat_lemma tl l_{2} pivot
type match_head (l_{1}:list int) (l_{2}:list int) =
(l_{1} = [] /\ l_{2} = []) \/
(exists h t_{1} t_{2}. l_{1} = h::t_{1} /\ l_{2} = h::t_{2})
val dedup: l:list int{sorted l} -> Tot (l_{2}:list int{sorted l_{2} /\ (forall i. mem i l = mem i l_{2}) /\ match_head l l_{2}})
let rec dedup l =
match l with
| [] -> []
| [x] -> [x]
| h::h_{2}::t ->
if h = h_{2} then dedup (h_{2}::t)
else h::dedup (h_{2}::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))
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
assert (forall i. mem i (pivot::sort hi) = mem i (append [pivot] (sort hi)));
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
(*
Copyright 2008-2018 Microsoft Research
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
module Ex06d
#set-options "--z3rlimit_factor 2"
(* 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 l_{1} l_{2} = match l_{1} with
| [] -> l_{2}
| hd :: tl -> hd :: append tl l_{2}
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 l_{1}, l_{2} = partition f tl in
if f hd
then hd::l_{1}, l_{2}
else l_{1}, hd::l_{2}
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 a_{1} a_{2}. (f a_{1} a_{2} /\ a_{1}<>a_{2}) <==> not (f a_{2} a_{1})) (* anti-symmetry *)
/\ (forall a_{1} a_{2} a_{3}. f a_{1} a_{2} /\ f a_{2} a_{3} ==> f a_{1} a_{3}) (* transitivity *)
val sorted_concat_lemma: #a:eqtype
-> f:(a -> a -> Tot bool)
-> l_{1}:list a{sorted f l_{1}}
-> l_{2}:list a{sorted f l_{2}}
-> pivot:a
-> Lemma (requires (total_order a f
/\ (forall y. mem y l_{1} ==> not (f pivot y))
/\ (forall y. mem y l_{2} ==> f pivot y)))
(ensures (sorted f (append l_{1} (pivot::l_{2}))))
let rec sorted_concat_lemma #a f l_{1} l_{2} pivot =
match l_{1} with
| [] -> ()
| hd::tl -> sorted_concat_lemma f tl l_{2} 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
(*
Copyright 2008-2018 Microsoft Research
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
module 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 Z_{3} *)
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
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.
We represent STLC types by the F* inductive datatype ty
.
type ty =
| TBool : ty
| TArrow : tin:ty -> tout: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 : v:var -> exp
| EApp : fn:exp -> arg:exp -> exp
| EAbs : v:var -> vty:ty -> body:exp -> exp
| ETrue : exp
| EFalse : exp
| EIf : test:exp -> btrue:exp -> bfalse: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
let stlc_app_id_to_true = 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
let stlc_not = EAbs 0 TBool (EIf (EVar 0) EFalse ETrue)
(in paper notation $\lambda x:\mathsf{bool}.~\mathsf{if }~x~\mathsf{ then~false~else~true}$).
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 e_{1} ->
EAbs x' t (if x = x' then e_{1} else (subst x e e_{1}))
| EApp e_{1} e_{2} -> EApp (subst x e e_{1}) (subst x e e_{2})
| ETrue -> ETrue
| EFalse -> EFalse
| EIf e_{1} e_{2} e_{3} -> EIf (subst x e e_{1}) (subst x e e_{2}) (subst x e e_{3})
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 e_{1})
we only substitute inside the body
e_{1}
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 e_{1}
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 only ever substitute closed expressions
e
, 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 wheree
, 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 e_{1} e_{2} ->
if is_value e_{1} then
if is_value e_{2} then
match e_{1} with
| EAbs x t e' -> Some (subst x e_{2} e')
| _ -> None
else
match (step e_{2}) with
| Some e_{2}' -> Some (EApp e_{1} e_{2}')
| None -> None
else
(match (step e_{1}) with
| Some e_{1}' -> Some (EApp e_{1}' e_{2})
| None -> None)
| EIf e_{1} e_{2} e_{3} ->
if is_value e_{1} then
match e_{1} with
| ETrue -> Some e_{2}
| EFalse -> Some e_{3}
| _ -> None
else
(match (step e_{1}) with
| Some e_{1}' -> Some (EIf e_{1}' e_{2} e_{3})
| None -> None)
| _ -> None
We execute an application expression EApp e_{1} e_{2}
in multiple steps by first reducing
e_{1}
to a value, then reducing e_{2}
to a value (following a call-by-value
evaluation order), and if additionally e_{1}
is an abstraction EAbs x t e'
we continue by substituting the formal
argument x
by the actual argument e_{2}
. If not we signal a dynamic typing error
(a non-functional value is applied to arguments) by returning None
.
For EIf e_{1} e_{2} e_{3}
we first reduce the guard e_{1}
: if the guard reduces to true
then we continue with e_{2}
, if the guard reduces to false
we continue with e_{3}
,
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.
let _ = assert (step (EApp (EAbs 0 TBool (EVar 0)) ETrue) = Some ETrue)
let _ = assert (step (EApp ETrue ETrue) = None)
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 environment—a 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 = fun _ -> None
When we move under a binder we extend the typing environment.
val extend : env -> int -> ty -> Tot env
let extend g x t = fun 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 e_{1} ->
(match typing (extend g x t) e_{1} with
| Some t' -> Some (TArrow t t')
| None -> None)
| EApp e_{1} e_{2} ->
(match typing g e_{1}, typing g e_{2} with
| Some (TArrow t11 t12), Some t_{2} -> if t11 = t_{2} then Some t12 else None
| _ , _ -> None)
| ETrue -> Some TBool
| EFalse -> Some TBool
| EIf e_{1} e_{2} e_{3} ->
(match typing g e_{1}, typing g e_{2}, typing g e_{3} with
| Some TBool, Some t_{2}, Some t_{3} -> if t_{2} = t_{3} then Some t_{2} else None
| _ , _ , _ -> None)
Variables are simply looked up in the environment.
For abstractions EAbs x t e_{1}
we type-check the body e_{1}
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 e_{1} e_{2}
we type-check e_{1}
and e_{2}
separately, and
if e_{1}
has a function type TArrow t11 t12
and
e_{2}
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.
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 (Some? (typing empty e)))
(ensures (is_value e \/ (Some? (step e))))
let rec progress e =
match e with
| EApp e_{1} e_{2} -> progress e_{1}; progress e_{2}
| EIf e_{1} e_{2} e_{3} -> progress e_{1}; progress e_{2}; progress e_{3}
| _ -> ()
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 e_{1} e_{2})
F* and Z3 automate the following intuitive argument:
We case split on the first instance of the induction
hypothesis (is_value e_{1} \/ (Some? (step e_{1})))
.
e_{1}
steps to e_{1}'
then, by the definition of step
,
(EApp e_{1} e_{2})
steps to (EApp e_{1}' e_{2})
.
e_{1}
is a value, we case split on the second induction hypothesis instance,
(is_value e_{2} \/ (Some? (step e_{2})))
.
e_{2}
steps to e_{2}'
then (EApp e_{1} e_{2})
steps to (EApp e_{1} e_{2}')
,
since e_{1}
is a value.
e_{2}
is also a value, then we need to obtain that e_{1}
has
a function type and from this that it is an abstraction.
Expression e_{1}
has a function type because, by the definition of typing
,
an application is well-typed only when the first expression is a function.
The remaining step is usually done as a separate “canonical forms” lemma, stating
that any value that has a function type is actually an abstraction.
Z3 can prove this fact automatically from the definitions of typing
and is_value
.
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 g
—in
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 expression—i.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 e_{1} e_{2} -> appears_free_in x e_{1} || appears_free_in x e_{2}
| EAbs y _ e_{1} -> x <> y && appears_free_in x e_{1}
| EIf e_{1} e_{2} e_{3} ->
appears_free_in x e_{1} || appears_free_in x e_{2} || appears_free_in x e_{3}
| 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 (Some? (typing g e)))
(ensures (appears_free_in x e ==> Some? (g x)))
let rec free_in_context x e g =
match e with
| EVar _
| ETrue
| EFalse -> ()
| EAbs y t e_{1} -> free_in_context x e_{1} (extend g y t)
| EApp e_{1} e_{2} -> free_in_context x e_{1} g; free_in_context x e_{2} g
| EIf e_{1} e_{2} e_{3} -> free_in_context x e_{1} g;
free_in_context x e_{2} g; free_in_context x e_{3} 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 (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 to Z3
that it should consider applying this lemma when its context contains a
term of the form appears_free_in
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:
logic type equal (g_{1}:env) (g_{2}:env) = forall (x:int). g_{1} x = g_{2} 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
:
logic type equalE (e:exp) (g_{1}:env) (g_{2}:env) =
forall (x:int). appears_free_in x e ==> g_{1} x = g_{2} 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 e_{1} ->
context_invariance e_{1} (extend g x t) (extend g' x t)
| EApp e_{1} e_{2} ->
context_invariance e_{1} g g';
context_invariance e_{2} g g'
| EIf e_{1} e_{2} e_{3} ->
context_invariance e_{1} g g';
context_invariance e_{2} g g';
context_invariance e_{3} 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 (Some? (typing empty v) /\
Some? (typing (extend g x (Some?.v (typing empty v))) e)))
(ensures (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 e_{1} e_{2} ->
substitution_preserves_typing x e_{1} v g;
substitution_preserves_typing x e_{2} v g
| EIf e_{1} e_{2} e_{3} ->
substitution_preserves_typing x e_{1} v g;
substitution_preserves_typing x e_{2} v g;
substitution_preserves_typing x e_{3} v g
| EAbs y t_y e_{1} ->
let gxy = extend gx y t_y in
let gy = extend g y t_y in
if x=y
then typing_extensional gxy gy e_{1}
else
(let gyx = extend gy x t_x in
typing_extensional gxy gyx e_{1};
substitution_preserves_typing x e_{1} v gy)
The proof proceeds by induction on the expression e
;
we give the intuition of the two most interesting cases:
e = EVar y
x = y
: We have subst x v e = v
and we already know that
typing empty v == Some t_x
. However, what we need to show is
typing g v == Some t_x
for some arbitrary environment g
.
From the typable_empty_closed
lemma we obtain that v
contains
no free variables, so we have equalE v empty g
. This allows us
to apply the context_invariance
lemma to obtain that
typing empty v = typing g v
and complete the proof of this case.
x <> y
: We have subst x v e = e
and
typing gx e = Some t_e
and need to show that
typing g e == Some t_e
We have that EquivE (EVar y) gx g
since x <> y
so we can apply
the context_invariance
lemma to conclude.
e = EAbs y t_y e_{1}
:
We have that typing gxy e_{1} = Some t_e_{1}
,
and need to show that
typing gy e_{1} == Some t_e_{1}
x = y
: We have subst x v e = EAbs y t_y e_{1}
.
Since x = y
the x
binder in gxy
is spurious (we have equal gy gxy
)
and can apply the typing_extensional
lemma.
x <> y
: We have subst x v e = EAbs y t_y (subst x v e_{1})
.
Since x <> y
(and since we are in a simply typed calculus, not
a dependently typed one) we can swap the x
and y
binding to show
that equal gxy xyx
. By the typing_extensional
lemma we obtain that
typing gxy e_{1} == typing gyx e_{1}
. By the induction hypothesis we thus
obtain that
typing gy (subst x v e_{1}) == Some t_e_{1}
and by the definition
of typing
we conclude that typing g (EAbs y t_y (subst x v e)) = t_e
.
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 (Some? (typing empty e) /\ Some? (step e) ))
(ensures (Some? (step e) /\
typing empty (Some?.v (step e)) == typing empty e))
let rec preservation e =
match e with
| EApp e_{1} e_{2} ->
if is_value e_{1}
then (if is_value e_{2}
then let EAbs x _ ebody = e_{1} in
substitution_preserves_typing x ebody e_{2} empty
else preservation e_{2})
else preservation e_{1}
| EIf e_{1} _ _ ->
if not (is_value e_{1}) then preservation e_{1}
We only have two cases to consider, since only applications and conditionals
can take successful execution steps. The case for e = EIf e_{1} e_{2} e_{3}
is simple:
either e_{1}
is a value and thus the conditional reduces to e_{2}
or e_{3}
which
by the typing hypothesis also have type t
, or e_{1}
takes a successful step and
we can apply the induction hypothesis. We use the Some?.v
projector,
which requires F* to prove that indeed e_{1}
can take a step;
this is immediate since we know that the whole conditional takes a step
and we know that e_{1}
is not a value.
The case for e = EApp e_{1} e_{2}
is a bit more complex. If e_{1}
steps or if e_{1}
is
a value and e_{2}
steps then we just apply the induction hypothesis.
If both e_{1}
and e_{2}
are values it needs to be the case that e_{1}
is
an abstraction EAbs x targ ebody
and step e = subst x e_{2} ebody
.
From the typing assumption we have typing (extend empty x tags) ebody = Some t
and typing empty e_{2} = Some targ
, so we can use the substitution lemma
to obtain that typing empty (subst x e_{2} ebody) = Some t
, which concludes the proof.
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{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)
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 e_{1} e_{2} -> is_value e_{1} && is_value e_{2}
let rec subst x e e' =
match e' with
...
| EPair e_{1} e_{2} -> EPair (subst x e e_{1}) (subst x e e_{2})
| EFst e_{1} -> EFst (subst x e e_{1})
| ESnd e_{1} -> ESnd (subst x e e_{1})
let rec step e =
...
| EPair e_{1} e_{2} ->
if is_value e_{1} then
if is_value e_{2} then None
else
(match (step e_{2}) with
| Some e_{2}' -> Some (EPair e_{1} e_{2}')
| None -> None)
else
(match (step e_{1}) with
| Some e_{1}' -> Some (EPair e_{1}' e_{2})
| None -> None)
| EFst e_{1} ->
if is_value e_{1} then
(match e_{1} with
| EPair v_{1} v_{2} -> Some v_{1}
| _ -> None)
else
(match (step e_{1}) with
| Some e_{1}' -> Some (EFst e_{1}')
| None -> None)
| ESnd e_{1} ->
if is_value e_{1} then
(match e_{1} with
| EPair v_{1} v_{2} -> Some v_{2}
| _ -> None)
else
(match (step e_{1}) with
| Some e_{1}' -> Some (ESnd e_{1}')
| None -> None)
code/exercises/Ex07b.fstLoad in editor
Add cases to typing
for the new constructs and fix all the proofs.
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 e_{1} e_{2} ->
(match typing g e_{1}, typing g e_{2} with
| Some t_{1}, Some t_{2} -> Some (TPair t_{1} t_{2})
| _ , _ -> None)
| EFst e_{1} ->
(match typing g e_{1} with
| Some (TPair t_{1} t_{2}) -> Some t_{1}
| _ -> None)
| ESnd e_{1} ->
(match typing g e_{1} with
| Some (TPair t_{1} t_{2}) -> Some t_{2}
| _ -> None)
val appears_free_in : x:int -> e:exp -> Tot bool
...
| EPair e_{1} e_{2} -> appears_free_in x e_{1} || appears_free_in x e_{2}
| EFst e_{1} -> appears_free_in x e_{1}
| ESnd e_{1} -> appears_free_in x e_{1}
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 (Some? (typing g e)))
(ensures (appears_free_in x e ==> Some? (g x)))
let rec free_in_context x e g =
...
| EPair e_{1} e_{2} -> free_in_context x e_{1} g; free_in_context x e_{2} g
| EFst e_{1}
| ESnd e_{1} -> free_in_context x e_{1} 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 e_{1} e_{2} ->
context_invariance e_{1} g g';
context_invariance e_{2} g g'
| EFst e_{1}
| ESnd e_{1} -> context_invariance e_{1} g g'
val substitution_preserves_typing : x:int -> e:exp -> v:exp ->
g:env{Some? (typing empty v) &&
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 e_{1} e_{2} ->
(substitution_preserves_typing x e_{1} v g;
substitution_preserves_typing x e_{2} v g)
| EFst e_{1}
| ESnd e_{1} ->
substitution_preserves_typing x e_{1} v g
code/solutions/Ex07b.fstLoad in editor
As for the other cases, the preservation proof when e = EPair e_{1} e_{2}
follows the structure of the step
function. If e_{1}
is not a value
then it further evaluates, so we apply the induction hypothesis to
e_{1}
. If e_{1}
is a value, then since we know that the pair evaluates,
it must be the case that e_{2}
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{Some? (typing empty e) /\ Some? (step e)} ->
Tot (u:unit{typing empty (Some?.v (step e)) == typing empty e})
let rec preservation e =
...
| EPair e_{1} e_{2} ->
(match is_value e_{1}, is_value e_{2} with
| false, _ -> preservation e_{1}
| true , false -> preservation e_{2})
| EFst e_{1}
| ESnd e_{1} ->
if not (is_value e_{1}) then preservation e_{1}
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.
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{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.
Here is a solution that only uses typed_step
(suggested by Santiago Zanella):
val eval : e:exp{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{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{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 e_{1} e_{2} ->
(let EAbs x _ e' = eval' e_{1} in
let v = eval' e_{2} in
substitution_preserves_typing x e' v empty;
eval' (subst x v e'))
| EAbs _ _ _
| ETrue
| EFalse -> e
| EIf e_{1} e_{2} e_{3} ->
(match eval' e_{1} with
| ETrue -> eval' e_{2}
| EFalse -> eval' e_{3})
| EPair e_{1} e_{2} -> EPair (eval' e_{1}) (eval' e_{2})
| EFst e_{1} ->
let EPair v_{1} _ = eval' e_{1} in v_{1}
| ESnd e_{1} ->
let EPair _ v_{2} = eval' e_{1} in v_{2}
| ELet x e_{1} e_{2} ->
(let v = eval' e_{1} in
substitution_preserves_typing x e_{2} v empty;
eval' (subst x v e_{2}))
code/solutions/Ex07d.fstLoad in editor
So far, we have mostly programmed total functions and given 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 meaningful—this 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.
Type
: The type of typesThe 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.
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 list
—it'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
.
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.
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 m
—internally, 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 wp
—in 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)
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)
.
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.
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 = e_{1} in e_{2} | assert b | if b then e_{1} else e_{2}
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 = e_{1} in e_{2}) P = WP e_{1} (fun x -> WP e_{2} P)
WP (assert b) P = b /\ P b
WP (if b then e_{1} else e_{2}) P = (b ==> WP e_{1} P) /\ ((not b) ==> WP e_{2} 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 known—Flanagan 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 the 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 = e_{1} in e_{2}) P = WLP e_{1} (fun x -> WLP e_{2} P)
WLP (assert b) P = b ==> P b
WLP (if b then e_{1} else e_{2}) P = (b ==> WLP e_{1} P) /\ ((not b) ==> WLP e_{2} 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 e_{1} else e_{2}) P
= (b ==> WP e_{1} (fun x -> True))
/\ ((not b) ==> WP e_{2} (fun x -> True))
/\ (forall y. P y \/ ((b ==> WLP e_{1} (fun x -> x<>y)
/\ (not b) ==> WLP e_{2} (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 inference—for 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).
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 t_{1}..t_{n} t wp wlp
. The M t_{1}..t_{n}
indicates the name of the
effect M
and several user-defined indexes t_{1}..t_{n}
. 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.
We follow an informal syntactic convention that the non-abbreviated all-caps names for computation types are the primitive forms—other 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.
PURE
effectThe 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 form—they transform pure post-conditions to pure
pre-conditions.
let pure_post (a:Type) = a -> Type
let pure_pre = Type
let pure_wp (a:Type) = pure_post a -> pure_pre
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 0
—which 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: pure_post a) -> post x
When sequentially composing two pure computations using
let x = e_{1} in e_{2}
, if
e_{1}: PURE t_{1} wp_{1} wlp_{1}
and
e_{2}: (x:t_{1} -> PURE t_{2} (wp_{2} x) (wlp_{2} x))
,
we type the composed computation as
PURE t_{2} (bind_PURE wp_{1} wp_{2}) (bind_PURE wlp_{1} wlp_{2})
where:
type bind_PURE (#a:Type) (#b:Type)
(wp_{1}: pure_wp a)
(wp_{2}: a -> pure_wp b)
= fun (post:pure_post b) -> wp_{1} (fun (x:a) -> wp_{2} x post)
One can show that return_PURE
and bind_PURE
together form a monad over
PureWP
.
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:pure_post a) -> pre /\ forall (x:a). post x ==> p x)
(fun (p:pure_post 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:pure_post a) -> forall (x:a). p x)
(fun (p:pure_post 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.
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:pure_wp a) = wp (fun x -> True)
type as_ensures (#a:Type) (wlp:pure_wp a) (x:a) = ~ (wlp (fun y -> ~(y==x)))
assume val as_Pure: #a:Type -> #b:(a -> Type)
-> #wp:(x:a -> pure_wp (b x))
-> #wlp:(x:a -> pure_wp (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))
The second-to-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 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.
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
STATE
effectStateful 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 : state_wp t
has the signature below.
let state_post t = t -> heap -> Type
let state_pre = heap -> Type
let state_wp t = state_post t -> state_pre
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 -> Tot bool
These functions are interpreted using standard axioms, which allows the SMT solver to reason about heaps, for instance:
assume SelUpd_{1}: 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 SelUpd_{2}: forall (a:Type) (b:Type) (h:heap) (k_{1}:ref a) (k_{2}:ref b) (v:b).
{:pattern (sel (upd h k_{2} v) k_{1})}
k_{2}=!=k_{1} ==> sel (upd h k_{2} v) k_{1} = sel h k_{1}
The Heap
library axiomatizes several other functions—the
interested reader refer to lib/heap.fst
for more details.
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 SelUpd_{1}
and SelUpd_{2}
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
:
let wp_read r = fun (post:state_post a) (h_{0}:heap) -> post (sel h_{0} r) h_{0}
assume val read: #a:Type -> r:ref a -> STATE a (wp_read r) (wp_read r)
This says that read r
returns a result v:a
when r:ref a
;
and, to prove for any post-condition post:state_post a
relating the
v
to the resulting heap, it suffices to prove post (sel h_{0} r) h_{0}
when read r
is run in the initial heap h_{0}
.
Next, here's the signature of write
:
let wp_write r = fun (post:state_post a) (h_{0}:heap) -> post () (upd h_{0} r v)
assume val write: #a:Type -> r:ref a -> v:a -> STATE unit (wp_write r) (wp_write r)
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:state_post a
relating the ()
to the resulting heap, it suffices to prove
post () (upd h_{0} r v)
when write r v
is run in the initial heap h_{0}
.
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 pure_wp
, the predicate transformers state_wp t
form a
monad, as shown by the combinators below.
type return_STATE (#a:Type) (v:a) = fun (post:state_post a) (h_{0}:heap) -> post v h_{0}
type bind_STATE (#a:Type) (wp_{1}:state_wp a) (wp_{2}:a -> state_wp b)
= fun (post:state_post b) (h_{0}:heap) -> wp_{1} (fun (x:a) -> wp_{2} x post) h_{0}
ST
effectST
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:state_pre) (post: (heap -> state_post a)) = STATE a
(fun (p:state_post a) (h:heap) ->
pre h /\ (forall a h_{1}. (pre h /\ post h a h_{1}) ==> p a h_{1})) (* WP *)
(fun (p:state_post a) (h:heap) ->
(forall a h_{1}. (pre h /\ post h a h_{1}) ==> p a h_{1})) (* 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) (h_{0}:heap) (x:a) (h_{1}:heap)
= ~ (wlp (fun y h_{1}' -> y<>x \/ h_{1}<>h_{1}') h_{0})
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 h_{0} y h_{1} -> h_{0}=h_{1} /\ y >= 0)
let g = h (as_ST f)
St
effectWe 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)
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:pure_wp a) (p:state_post 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:pure_wp a
(equivalently for its wlp
) to a state_wp a
that says that that pure computation leaves the state unmodified.
Note that the type of PURE ~> STATE
is
(a:Type) -> pure_wp a -> state_post a -> heap -> Type
which corresponds
to (a:Type) -> pure_wp a -> state_wp a
since:
let state_wp a = state_post a -> state_pre
let state_pre = heap -> Type
Finally, as mentioned earlier, in its full form a computation type has
the shape M t_{1}..t_{n} t wp wlp
, where t_{1}..t_{n}
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.
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 ok—we'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.
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 it—of 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:
(*
Copyright 2008-2018 Microsoft Research
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
module Ex10a
open FStar.All
open FStar.List.Tot
open FStar.Ref
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 = ST.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.
*)
(*
// Uncomment these types and make them precise enough to pass the test
// BEGIN: Ex10aExercise
val grant : e:entry -> ST unit (requires (fun h -> True))
(ensures (fun h x h' -> True))
val revoke: e:entry -> ST unit (requires (fun h -> True))
(ensures (fun h x h' -> True))
// END: Ex10aExercise
*)
let grant e = acls := e::!acls
let revoke e =
let db = filter (fun e' -> e<>e') !acls in
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 `safe_Delete`
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))
val revoke: e:entry -> ST unit (requires (fun h -> True))
(ensures (fun h x h' -> True))
code/exercises/Ex10a.fstLoad in editor
val grant : e:entry -> ST unit (requires (fun h -> True))
(ensures (fun h _ h' -> sel h' acls == e::sel h acls))
val revoke: e:entry -> ST unit (requires (fun h -> True))
(ensures (fun h x h' -> not(mem e (sel h' acls))))
code/solutions/Ex10a.fstLoad in editor
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*.
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, p_{1}
and p_{2}
, we want to shift p_{1}
, and
reason that p_{2}
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_p_{1} p_{1} p_{2} =
let p2_0 = !(Point?.x p_{2}), !(Point?.y p_{2}) in //p_{2} is initially p2_0
shift_x p_{1};
let p2_1 = !(Point?.x p_{2}), !(Point?.y p_{2}) in
assert (p2_0 = p2_1) //p_{2} 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_p_{1} 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_p_{1}
, F* does not check that the assertion will succeed
on every invocation of shift_x_p_{1}
; instead, using the inferred type it will
aim to prove that the assertion will succeed whenever the function is
called. Let's try:
val test_{0}: unit -> St unit
let test_{0} () =
let p_{1} = new_point 0 0 in
shift_x_p_{1} p_{1} p_{1}
Here, we wrote a specification for test_{0}
, asking it to have trivial
pre-condition. When we ask F* to check this, it complains at the call to
shift_x_p_{1} x x
, saying that the assertion failed.
If we try calling shift_x_p_{1}
with two distinct points, as below, then we
can prove that the assertion succeeds.
val test_{1}: unit -> St unit
let test_{1} () =
let p_{1} = new_point 0 0 in
let p_{2} = new_point 0 0 in
shift_x_p_{1} p_{1} p_{2}
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 types—for 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.
shift_x
and the Heap.modifies
predicateLet'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 h_{0} _ h_{1} -> h_{1}=upd h_{0} (Point?.x p) (sel h_{0} (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 h_{0} x h_{1} -> modifies (only (Point?.x p)) h_{0} h_{1}))
Informally, ensures
-clause above says that the heap after calling this
function (h_{1}
) differs from the initial heap h_{0}
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 h_{0} h_{1} =
Heap.equal h_{1} (Heap.concat h_{1} (Heap.restrict (Set.complement mods) h_{0}))
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 h_{0}
contains r
,
then sel h_{1} r = sel h_{0} r
, i.e., it hasn't changed. Otherwise,
sel h_{1} r = sel h_{1} r
—meaning we know nothing else about it.
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) (r_{1}:ref a) (r_{2}:ref b) = // ^+^
Set.union (Set.singleton (Ref r_{1})) (Set.singleton (Ref r_{2}))
new_point
and freshness of referencesHere'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 h_{0} p h_{1} ->
modifies Set.empty h_{0} h_{1}
/\ Heap.fresh (Point?.x p) h_{0} h_{1}
/\ Heap.fresh (Point?.y p) h_{0} h_{1}
/\ Heap.sel h_{1} (Point?.x p) = x
/\ Heap.sel h_{1} (Point?.y p) = y
/\ Heap.contains h_{1} (Point?.x p) //these two lines should be captures by fresh
/\ Heap.contains h_{1} (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
reference—that'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 h_{0} r h_{1} -> fresh (only r) h_{0} h_{1} /\ h_{1}==upd h_{0} r init))
type fresh (refs:set aref) (h_{0}:heap) (h_{1}:heap) =
(forall (a:Type) (r:ref a). mem (Ref r) refs
==> not(contains h_{0} r) /\ contains h_{1} 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 test_{2}: unit -> St unit
let test_{2} () =
let p = new_point 0 0 in
let z :ref nat = ST.alloc 0 in
assert (addr_of (Point?.x p) <> addr_of 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 h_{0} _ h_{1} -> h_{0}=h_{1} /\ Heap.contains h_{1} 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.
shift_x_p_{1}
Now, we have all the machinery we need to give shift_x_p_{1}
a sufficiently
strong type to prove that its assertion will never fail (if its pre-condition is met).
val shift_x_p_{1}: p_{1}:point
-> p_{2}:point{ addr_of (Point?.x p_{2}) <> addr_of (Point?.x p_{1})
/\ addr_of (Point?.y p_{2}) <> addr_of (Point?.x p_{1}) }
-> ST unit
(requires (fun h -> Heap.contains h (Point?.x p_{2})
/\ Heap.contains h (Point?.y p_{2})))
(ensures (fun h_{0} _ h_{1} -> modifies (only (Point?.x p_{1})) h_{0} h_{1}))
In order to prove that the assignment to Point?.x p_{1}
did not change
p_{2}
, we need to know that Point?.x p_{1}
does not alias either component
of p_{2}
. In general, if p_{1}
can change arbitrarily, we also need the
other two conjuncts, i.e., we will need that the references of p_{1}
and p_{2}
are pairwise distinct.
A note on style: we could have placed the refinement on .
p_{2}
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_p_{1}
does not change p_{2}
.
let shift p = Point?.x p := ...; Point?.y p := ...
code/exercises/Ex10b.fstLoad in editor
let shift p =
Point?.x p := !(Point?.x p) + 1;
Point?.y p := !(Point?.y p) + 1
val shift_p_{1}: p_{1}:point
-> p_{2}:point{ addr_of (Point?.x p_{2}) <> addr_of (Point?.x p_{1})
/\ addr_of (Point?.y p_{2}) <> addr_of (Point?.x p_{1})
/\ addr_of (Point?.x p_{2}) <> addr_of (Point?.y p_{1})
/\ addr_of (Point?.y p_{2}) <> addr_of (Point?.y p_{1}) }
-> ST unit
(requires (fun h -> Heap.contains h (Point?.x p_{2})
/\ Heap.contains h (Point?.y p_{2})))
(ensures (fun h_{0} _ h_{1} -> modifies (Point?.x p_{1} ^+^ Point?.y p_{1}) h_{0} h_{1}))
let shift_p_{1} p_{1} p_{2} =
let p2_0 = !(Point?.x p_{2}), !(Point?.y p_{2}) in //p_{2} is initially p2_0
shift p_{1};
let p2_1 = !(Point?.x p_{2}), !(Point?.y p_{2}) in
assert (p2_0 = p2_1) //p_{2} is unchanged
code/solutions/Ex10b.fstLoad in editor
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