Program verification with F*

Course at 2018 EUTypes Summer School on Types for Programming and Verification in Ohrid, Macedonia on 8-12 August, 2018

(Based on past courses by Cătălin Hriţcu and various other members of the F* team)

Schedule

Friday, 10 August, 2018:

• 10:30--11:30 A Gentle Introduction to F*: Verifying Purely Functional Programs (slides)
• Code:
• Ackermann.fst (Ackermann function and decreases metrics)
• Rev.fst (list reversal)
• Divergence.fst (potentially divergent evaluator)
• Exercise 1: Summing 1 + 2 + 3 + ... (Sum.fst; solution)
• Exercise 2: Simply typed stacks (Stack.fsti, Stack.fst, StackClient.fst; solution 1, solution 2, solution 3)
• Exercise 3: Refined stacks (RefinedStack.fsti; solution 1, solution 2, solution 3)

Saturday, 11 August, 2018:

• 16:30--17:30 Verifying Stateful Programs with F* (slides)
• 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
• Code:
• IncrST.fst, Incr2ST.fst (increment function)
• SwapRefsST.fst (reference swapping)
• CountST.fst (stateful counting)
• FibonacciST.fst (stateful fibonacci)
• BufferAlloc.fst, BufferAlloc.c (low-level code)
• Exercise 1: Sketch a hand proof of the correctness of integer reference swapping (SwapIntRefsST.fst)
• Exercise 2: Stateful summing 1 + 2 + 3 + ... (SumST.fst; solution)
• Exercise 3: Stateful factorial (FactorialST.fst; solution)
• Exercise 4: Experiment with the low-level memory model and extraction to C (see BufferAlloc.fst)
• 17:30--18:30 Exercise Class

Sunday, 12 August, 2018:

• 09:00--10:00 Monotonic State in F* (slides)
• 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
• Code:
• CounterMST.fst (monotonic counters)
• SimpleLogMST.fst (monotonic logs)
• InitFreezeMST.fst (initializable and freezable references)
• Snapshots.fst (escaping the preorder with snapshots)
• Exercise 1: Typing of initializable and freezable references read and freeze actions (InitFreezeMST.fst; solution)
• Exercise 2: Define a notion of initializable and freezable arrays (see the lecture slides for details; solution)
• 12:00--13:00 F*'s Extensible Effect System and Metaprogramming in F* (slides)
• F*'s extensible effect system; Dijkstra monads (for free) (paper1, paper2, examples)
• F*'s tactics and metaprogramming framework (paper, examples)
• Code:
• IncrReify.fst (verifying stateful increment function using monadic reification)
• NonInterference.fst (proving noninterference using monadic reification)
• Logic.fst (discharging verification conditions: simple tautology)
• CanonCommSemiring.fst (massaging verification conditions: canonicaliser for commutative semirings)
• Printers.fst (synthesising F* terms: printer for inductive types)
• Typeclasses.fst (metaprogramming typeclasses; needs a more recent version of F* than the v0.9.6.0 release)
• Exercise 1: Implement stateful summing (similarly to Lecture 2, but with a weak type) using a global state (similarly to IncrReify.fst) and use monadic reification (see Lecture 4) to prove that this stateful summing is equivalent to the purely functional code (SumReify.fst; solution)
• Exercise 2: Implement stateful Fibonacci (similarly to Lecture 2, but with a weak type) using a 2-location global state (as used in NonInterference.fst) and use monadic reification (see Lecture 4) to prove that this stateful Fibonacci is equivalent to the purely functional code (FibonacciReify.fst; solution)
• Exercise 3: Define the READER effect, show that it is a sub-effect of the STATE effect defined in SumReify.fst, and demonstrate that the READER effect you defined is correct wrt STATE (Reader.fst; solution)
• Exercise 4: Try out F*'s metaprogramming and tactics framework, starting with Logic.fst, and try to extend it to prove more interesting logical properties
• 15:00--16:00 Exercise Class

Setup instructions

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

We also have an even cooler online editor (experimental).

For people who want to get F* (v0.9.6.0, most recent release) installed on their machine there are 2 easy options:

1. Using the binary release (documentation on this)
2. or Using the OPAM package (especially for people already using OCaml; note that you still need to get Z3 separately)
   

In addition, if you're familiar with emacs, we recommend getting fstar-mode for it.

For people who are more motivated, there are even more ways including building F* from sources (see documentation on this).

^†Note: Recent versions of F* use the [@expect_failure] attribute to denote the expectation of failing typechecking, while the v0.9.6.0 release uses the [@fail] attribute for the same purpose. Change this according to the version you use, e.g., this concerns Ackermann.fst.