Program verification with F*
Guest lecture and accompanying lab sessions for the Advanced Programming Course (ITT8060) at the Tallinn University of Technology.
Lecture slides (9.12.2020)
Lab exercises (9-10.12.2020)
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
Homework
Useful code snippets
- Ackermann function, interfaces, and decreases metrics: Ackermann.fsti, Ackermann.fst
- List reversal: Rev.fst
- Potential divergence:Divergence.fst
- F*'s ML-style garbage-collected memory model: FStar.Heap.fst, FStar.ST.fst
- F*'s low-level memory model: FStar.HyperStack.fst, FStar.HyperStack.ST.fst
- Stateful increment function: IncrST.fst, Incr2ST.fst
- Reference swapping: SwapRefsST.fst
- Stateful counting: CountST.fst
- Low-level code example: BufferAlloc.fst, BufferAlloc.c
- F*'s witnessed modality: FStar.Monotonic.Witnessed.fsti, FStar.Monotonic.Witnessed.fst
- F*'s monotonic ML-style memory model: FStar.Monotonic.Heap.fst, FStar.ST.fst, FStar.Ref.fst
- F*'s monotonic low-level 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 4 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 SMT-solver, 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 a Docker container (especially for people who already have Docker on their computer):
-
Get the F* Docker container:
$ docker pull fstarlang/fstar-emacs
-
NOTE: This gets you the most recent F* build, the supported version of Z3, and also the Emacs fstar-mode (to use Emacs with GUI, follow these instructions).
-
In order to persist your work between subsequent docker and container runs, create a volume to keep your exercises and code:
$ docker volume create fstar-vol
-
Run the container and log into it:
$ docker run -i -t --mount source=fstar-vol,target=/fstar-vol fstarlang/fstar-emacs
-
When logged into the container, change the owner of the /fstar-vol volume to build:build:
$ sudo chown -R build:build /fstar-vol
-
And you should be all set to start writing and veirfying programs in F*:
$ cd /fstar-vol ; cp ~/FStar/examples/hello/Hello.fst . ; emacs Hello.fst
-
If needed for the exercises, you can find the F* standard library in ~/FStar/ulib and various examples in ~/FStar/examples.
-
After you exit the container, you can restart it by looking up its ID using
$ docker ps -a
and running $ docker start -i CONTAINER_ID
.
-
People who are more motivated and more adventurous can of course also build F* directly from its sources, see the documentation.
Using F* interactively
-
If you are familiar with the Emacs text editor, it is recommended getting
fstar-mode for it to make the most of F*'s interactive features.
More references
Acknowledgements
The lecturer has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie
grant agreement No 834146.