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)*

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

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:

- Using the binary release (documentation on this)
- 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.