Program verification with F*
Guest lecture and accompanying lab sessions for the Advanced Programming Course (ITT8060) at the Tallinn University of Technology.
Lecture slides (12.12.2018)
Lab exercises (1214.12.2018)
These exercises are mostly independent of each other, so you do not need to do them in the given order, but the earlier ones are generally more basic.
Out of all of them, Exercise 7 is probably the most involved. It lets you simultaneously practice the verification of both pure and stateful programs.
Verifying purely functional programs
 Exercise 1: Summing 1 + 2 + 3 + ...
 Exercise 2: Simply typed stacks
 Exercise 3: Refined stacks
Verifying stateful programs
 Exercise 4: Stateful summing 1 + 2 + 3 + ...
 Exercise 5: Stateful factorial 1 * 2 * 3 * ...
 Exercise 6: Stateful Fibonacci 1 , 1 , 2 , 3 , 5 , 8 , ...
Verifying purely functional and stateful programs
 Exercise 7: Functional and mutable binary search trees
Verifying monotonic stateful programs
 Exercise 8: Initializable and freezable references
Useful code snippets
 Ackermann function, interfaces, and decreases metrics: Ackermann.fsti, Ackermann.fst
 List reversal: Rev.fst
 Potential divergence:Divergence.fst
 F*'s MLstyle garbagecollected memory model: FStar.Heap.fst, FStar.ST.fst
 F*'s lowlevel memory model: FStar.HyperStack.fst, FStar.HyperStack.ST.fst
 Stateful increment function: IncrST.fst, Incr2ST.fst
 Reference swapping: SwapRefsST.fst
 Stateful counting: CountST.fst
 Lowlevel code example: BufferAlloc.fst, BufferAlloc.c
 F*'s witnessed modality: FStar.Monotonic.Witnessed.fsti, FStar.Monotonic.Witnessed.fst
 F*'s monotonic MLstyle memory model: FStar.Monotonic.Heap.fst, FStar.ST.fst, FStar.Ref.fst
 F*'s monotonic lowlevel memory model: FStar.Monotonic.HyperStack.fst, FStar.HyperStack.ST.fst
 Classical logic in F*: FStar.Classical.fsti, FStar.Classical.fst, FStar.StrongExcludedMiddle.fst
 Monotonic counters: CounterMST.fst
 Monotonic logs: SimpleLogMST.fst
 Temporarily violating monotonicity with snapshots: Snapshots.fst
Sample solutions
Setup instructions
Using F* in your browser
Deploying F* on your computer

For people who want to get F* installed on their computer with little fuzz there are 3 easy options:
 Using the binary releases
(documentation on this)
 WARNING: The most recent (development) version of F* and its libraries are often not compatible with these binary releases^{†}.
 In order to get more recent, but also more experimental binary builds please look at the automatically generated weekly builds (Linux and Windows only).
 Using the OPAM package
(especially for people already using OCaml)
 WARNING: As with the binary releases, the stable version of F* on OPAM is often not compatible with with the most recent (develoment) version of F* and its libraries^{†}.
 In order to install the recent (development) version of F* through OPAM, please follow the instructions.
 IMPORTANT: You need to additionally download and add to your PATH a supported version of the Z3 SMTsolver, see the instructions.

Using the Homebrew formula (if you are a macOS user)
 WARNING: As with the binary releases, the stable version of F* on Homebrew is often not compatible with with the most recent (develoment) version of F* and its libraries^{†}.
 In order to install the recent (development) version of F* through Homebrew, please follow the instructions.

Using the Docker container (especially for people who already have Docker on their computer)

Get the F* Docker container:
docker pull fstarlang/fstaremacs

NOTE: This gets you both the most recent F* build, the supported version of Z3, and also the Emacs fstarmode.

To persist your work between subsequent container runs, create a volume:
docker volume create fstarvol

Run the container and log into it:
docker run i t mount source=fstarvol,target=/fstarvol fstarlang/fstaremacs:latest /bin/bash

When IN the container (for the first time), change the owner of the /fstarvol volume to FStar:
sudo chown R FStar:FStar /fstarvol

And you are ready to work on the exercises in /fstarvol:
cd /fstarvol ; cp ~/FStar/examples/hello/hello.fst . ; emacs hello.fst

If needed for exercises, you can find the F* standard library in /home/FStar/FStar/ulib and various examples in /home/FStar/FStar/examples

People who are more motivated and more adventurous can of course also build F* directly from its sources, see the documentation.
^{†}Note: E.g., recent versions of F* use the [@expect_failure] attribute to denote the expectation of failing typechecking, while the v0.9.6.0 binary release uses the [@fail] attribute for the same purpose.
Using F* interactively

If you are familiar with the Emacs text editor, it is recommended getting
fstarmode for it to make the most of F*'s interactive features.
More references