# F* Basics

#### Cătălin Hriţcu (Inria Paris)

Type Systems for Security Verification Lecture

Saarland University

Tuesday, 17 March 2015

## Some organization

• 1st Homework

• 2 optional exercises, for bonus points (4d and 4f)
• all exercises 1p (6p without, 8p with bonus points)
• Extending project period to Monday, 30 March

## Small correction for Lemma

Lemma t (requires r) (ensures e) = Pure unit (requires r) (ensures (fun _ -> e))Tot t = Pure (requires True) (ensures True)

## Today

• Semantic termination checking

• Simple effects: non-termination, exceptions

• Examples

• Binary search trees
• While language interpreter
• Tutorial

• solving 4d and 4f, maybe more

## Semantic termination checking

• Pure expressions proved terminating in F*
• Well-founded measure on F* expressions
• e1 << e2 (e1 precedes e2)
• (<<) : #a:Type -> #b:Type -> a -> b -> Type
• no infinite descending chains (e1 >> e2 >> ...)
• Decreases metric on recursive functions
• pure function/expression on the argument(s)
• at each recursive call check that metric applied to the argument(s) of the recursive call decreases
• default: lex ordering of the non-function arguments (left-to-right)
• default can be overridden with (decreases ...) clause

## The precedes relation

• if i, j : nat then i << j <==> i < j.
• negative integers are not related by <<
• sub-term ordering for inductive types
• hd::tl << hd and hd::tl << tl
• elements of type lex_t are ordered lexicographically
type lex_t = LexTop : lex_t | LexCons: #a:Type -> a -> lex_t -> lex_t%[v1;...;vn]@ = LexCons v1 ... (LexCons vn LexTop)
• LexCons v1 v2 << LexCons v1' v2' if and only if
either v1 << v1' or (v1=v1' and v2 << v2')
• if v:lex_t and v \neq LexTop, then v << LexTop
• Well-founded (since we require that negative occurrences in an inductive type definition are under at least one DIV arrow)

## Non-termination

• Same as pure, just no termination check

• DIV ~ PURE, Div ~ Pure, Dv ~ Tot

• no equivalent for Lemma, of course
val loop : u:unit -> Div unit (requires True) (ensures (fun _ -> False))let rec loop () = loop ()
• We'll see examples soon (While interpreter)

## Exceptions

• For code that can raise exceptions
• Exceptions can be caught with
try e1 with| pattern1 -> expression2| pattern2 -> expression3...
• This cannot make one pure (DIV actually),
although one can get close to that (see ICFP)
• EXN ~~ PURE, Exn ~~ Pure, Ex ~~ Tot
• EXN includes DIV (DIV <: EXN)

## Looking at examples

• Binary search trees
• While language interpreter

## Homework

• Binary search trees (extrinsic proofs) - 3 x 1p
• While language interpreter
(adding if-then-else removing while) - 2 x 1p
• Two optional problems (5a and 5b, tail recursion) - 2 x 1p

## Tutorial

• solving some of the prev homework together
• 4a, 4b, 4c, 4g, 4h easy
• 4e a bit more interesting
• 4d, 4f slightly challenging, optional