Program verification with F*

Guest lecture and accompanying lab session for the Advanced Programming Course (ITT8060) at the Tallinn University of Technology.

Lecture slides (6.12.2023)

• PDF Slides

Lab exercises (6-7.12.2023)

• ZIP archive with all the exercises

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

• FileSystem.fst and FileSystemClient.fst

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

• ZIP archive with solutions to all exercises

Setup instructions

Using F* in your browser

• The easiest way to try out F* quickly is directly in your browser using the online editor that's part of the F* tutorial.

Deploying F* on your computer

• For people who want to get F* installed on their computer with little fuzz there are 2 easy options:
  1. 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.
  2. 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.
• 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.
• There is now also a new(ish) F* plugin for VS Code editor, which supports both full and lax typechecking of F* code.

More references

• F* website
• F* tutorial
• F* book
• F* source code and libraries on GitHub
• KaRaMeL C compiler for Low*
• Steel and Pulse separation logic libraries
• Project Everest

Acknowledgements

The lecturer has received funding from the Air Force Office of Scientific Research under awards number FA9550-21-1-0024.