Introduction to Programming and Verification in F*

fstar-logo

Nik Swamy and Guido Martinez

ECI 2019

A first taste

  • Write ML-like code

    let rec factorial n = 
      if n = 0 then 1 
      else n * factorial (n - 1)
  • Give it a specification, claiming that factorial is a total function from non-negative to positive integers.

    val factorial: n:int{n >= 0} -> i:int{i >= 1}
  • Ask F* to check it

    fstar factorial.fst
    Verified module: Factorial
    All verification conditions discharged successfully
fstar factorial.fst
Verified module: Factorial
All verification conditions discharged successfully
F* builds a typing derivation of the form:

$\Gamma_{\mbox{prelude}} \vdash \mbox{\texttt{let factorial n = e}} : t \Leftarrow \phi$

  • In a context $\Gamma_{\mbox{prelude}}$ including definitions of F* primitives

  • The program $\mbox{\texttt{let factorial n = e}}$ has type $t$, given the validity of a logical formula $\phi$

  • $\phi$ is passed to Z3 (an automated theorem prover/SMT solver) to check for validity

  • If the check succeds, then, from the metatheory of F*, the program is safe at type $t$

Running F* Programs

fstar-lowstar-vale-compilation

The Functional Core of F*

Informally, like Coq or Agda, but with an extensional type theory (~Nuprl)

  • Refinement types

    let nat = x:int{x>=0}
    
  • Recursive functions

    let rec factorial (n:nat) : nat = if n = 0 then 1 else n * (factorial (n - 1))

Refinement types

type nat = x:int{x>=0}
  • Refinements introduced by type annotations (code unchanged)

    let rec factorial (n:nat) : nat = if n = 0 then 1 else n * (factorial (n - 1))
    
  • Logical obligations discharged by SMT (simplified)

    n >= 0, n <> 0 |= n - 1 >= 0
    n >= 0, n <> 0, factorial (n - 1) >= 0 |= n * (factorial (n - 1)) >= 0
  • Refinements eliminated by subtyping: nat<:int

    let i : int = factorial 42
    let f : x:nat{x>0} -> int = factorial

Dependent types

  • Dependent function types ($\Pi$), here together with refinements:

    val incr : x:int -> y:int{x < y}
    let incr x = x + 1
  • Can express pre- and post- conditions of pure functions

    val incr : x:int -> y:int{y = x + 1}
  • Exercise: Can you find other types for incr?

Inductive types and pattern matching

  • Inductive datatypes (immutable) and pattern matching

    type list a =
      | Nil  : list a
      | Cons : hd:a -> tl:list a -> list a
    
    let rec map (f:a -> b) (x:list a) : list b =
      match x with
      | [] -> []
      | h :: t -> f h :: map f t
  • Lambdas (unnamed, first-class functions)

    map (fun x -> x + 42) [1;2;3]

Inductive types and pattern matching

  • Recursive functions over inductive datatypes

    type vec a : nat -> Type =
      | Nil : vec a 0
      | Cons : #n:nat -> hd:a -> tl:vec a n -> vec a (n + 1)
    
    let rec append (v1:vec a n) (v2:vec a m) 
      : vec a (n + m) =
      match v1 with
      | Nil -> v2
      | Cons hd tl -> Cons hd (append tl v2)
  • Higher order

      let rec map (f:a -> b) (v:vec a n) 
        : vec b n 
        = match v with
          | Nil -> Nil
          | Cons hd tl -> Cons (f hd) (map f tl)
    
      map (fun x -> x + 42) (Cons 1 Nil)

Total functions in F*

  • The F* functions we saw so far were all total

  • Tot effect (default) = no side-effects, terminates on all inputs

    • a -> b is really shorthand for a -> Tot b
    val factorial : nat -> nat ~ nat -> Tot nat
    let rec factorial n = (if n = 0 then 1 else n * (factorial (n - 1)))
  • Quiz: How about giving this weak type to factorial?

    val factorial : int -> Tot int
  let rec factorial n = (if n = 0 then 1 else n * (factorial (n - 1)))
                                                              ^^^^^
  Subtyping check failed; expected type (x:int{(x << n)}); got type int

factorial (-1) loops! (int type in F* is unbounded)

Semantic termination checking

  • Based on well-founded ordering on expressions (<<)
    • naturals related by < (negative integers unrelated)
    • inductives related by subterm ordering
    • lex tuples %[a;b;c] with lexicographic ordering
    • result of a total function smaller than the function itself (f x << f)
  • order constraints discharged by the SMT solver
  • arbitrary total expression as decreases metric
    let rec ackermann (m n:nat) : Tot nat (decreases %[m;n]) =
      if m=0 then n + 1
      else if n = 0 then ackermann (m - 1) 1
      else ackermann (m - 1) (ackermann m (n - 1))
  • default metric is lex ordering of all (non-function) args
    val ackermann: m:nat -> n:nat -> Tot nat

Values and Computations

  • “Values” aka unconditionally total terms

  • Two classes of types

    • Value types (t): int, list int,
    • Computation types (C): conditionally pure, divergent, stateful,
  • F* effect system encapsulates effectful code

    • Pure code cannot call effectful code
    • But, via sub-effecting, pure code can be used in effectful contexts
  • Dependent function types of the form: x:t -> C

    • F* is call-by-value
    • argument can't have side-effects, so value type
  • Two forms of refinement types

    • Refined value types: x:t{p}
    • Refined computation types

Refined Computation Types

Refined Computation Types

  • Saw this already:

    val factorial : nat -> Tot nat
  • Can equivalently use pre- and post- conditions for this

    val factorial : x:int -> Pure int (requires (x >= 0))
                                      (ensures (fun y -> y >= 0))
  • Each computation type contains

    • effect (Pure), result type (int), spec (e.g. pre and post)
  • Tot can be seen as just an abbreviation

    Tot t = Pure t (requires True) (ensures (fun _ -> True))

Intrinsic vs Extrinsic Proofs

  • Intrinsic proof: The type of a term at the “definition site” expresses properties of interest

    let rec factorial (n:nat) : Tot nat = if n = 0 then 1 else n * factorial (n - 1)
  • Extrinsic proof: The type of a term is relatively simple; properties are proven separately from the definition

Lemma: Pure Computations as Extrinsic Proofs

let rec append (#a:Type) (xs ys : list a) : Tot (list a) =
  match xs with
  | [] -> ys
  | x :: xs' -> x :: append xs' ys
let rec append_length (#a:Type) (xs ys : list a) :
    Pure unit
      (requires True)
      (ensures (fun _ -> length (append xs ys) = length xs + length ys))
= match xs with
  | [] -> ()
  | x :: xs' -> append_length xs' ys
  • Syntax sugar (Lemma)
    let rec append_length_lemma (#a:Type) (xs ys : list a) :
      Lemma (ensures (length (append xs ys) = length xs + length ys))
    = match xs with
    | [] -> ()
    | x :: xs' -> append_length_lemma xs' ys

Often lemmas are unavoidable

let snoc l h = l @ [h]

let rec reverse (#a:Type) (l:list a) : Tot (list a) =
  match l with
  | [] -> []
  | hd::tl -> snoc (reverse tl) hd
let rec rev_snoc #a (l:list a) (h:a)
    : Lemma (reverse (snoc l h) == h::reverse l) =
    match l with
    | [] -> ()
    | hd::tl -> rev_snoc tl h
let rec rev_involutive #a (l:list a)
    : Lemma (reverse (reverse l) == l) =
    match l with
    | [] -> ()
    | hd::tl -> rev_involutive tl; rev_snoc (reverse tl) hd

Verifying pure programs

Variant #3: extrinsically using proof terms

let rec preservation (#e #e':exp) (#g:env) (#t:typ)
                     (ht:typing g e t)
                     (hs:step e e')
    : Tot (typing g e' t) (decreases ht) =
    match hs with
    | SBeta tx e1' e2' -> substitution_beta h2 (TyLam?.hbody h1)
    | SApp1 e2' hs1   -> TyApp (preservation h1 hs1) h2
    | SApp2 e1' hs2   -> TyApp h1 (preservation h2 hs2)
let rec progress (#e:exp) (#t:typ) 
                 (h:typing empty e t)
    : Pure (e':exp & step e e')
           (requires (~ (is_value e)))
           (ensures (fun _ -> True)) (decreases h) =
    match h with
    | TyApp #g #e1 #e2 #t11 #t12 h1 h2 ->
       match e1 with
       | ELam t e1' -> (| subst (sub_beta e2) e1', SBeta t e1' e2 |)
       | _          -> let ExIntro e1' h1' = progress h1 in
                       (| EApp e1' e2, SApp1 e2 h1' |)a
  • Note: match exhaustiveness check also semantic (via SMT)