Shall the twain ever meet?

The two, mostly disjoint sides of program verification research

• In the left corner: Arbitrarily expressive logics, but only purely functional programming

• In the right: Only first-order logic, but rich, effectful programming

Bridging the gap: F*

• A general purpose, strict, higher-order effectful language

  • like ML, with a predictable CBV cost model
  • but with monadically encapsulated effects like Haskell

• An SMT-based, semi-automated program verification tool,

  • like Dafny, Why3 etc.

• On a foundation of dependent and inductive types

  • like Coq, Agda etc.

• Also in the gap: ATS, HTT, Idris, Trellys, …

  • But none give you all three

F* in action: Verified cryptographic security

• Everest: A verified, drop-in replacement for the HTTPS stack, built mainly using F*

  • TLS-1.2 and TLS-1.3:

    • https://​github.​com/​mitls/​mitls-​fstar

  • Verified elliptic curve cryptography:

    • https://​github.​com/​mitls/​hacl-​star

  • Compiled to OCaml by default, but a subset of F* compiled to C for efficiciency:

    • https://​github.​com/​FStarLang/​kremlin

• F* is programmed in F* and bootstraps in OCaml or F#.

F* in action: Other examples

• ReVer: Microsoft Quantum Computing's verified compiler to reversible circuits

• Wys*: A verified DSL for secure multi-party computations

• F*: A fragment of F* formalized in F*

• …

This talk: The design of F*

• Case studies --

• Language design ++

The core of F*

A mostly standard dependent type theory at the core:

• , , inductives, match, universe polymorphism

Plus, specific to F*

1. Extensional equality, works well with refinement types

2. Fixed points with termination based on well-founded orders

3. General recursion (non-termination)

4. Two classes of types (similar to call-by-push-value):

   • Value types
   • Computation types

5. Two forms of refinement types with proof irrelevance …

Refined value types

• x:t{} inhabited by e:t satisfying [e/x]

• Some examples:

   nat = x:int{x >= 0}
   vec n a = l:list a {length l = n}

• The proof of is never materialized

    squash  = _:unit{}

Refined computation types

• Unconditionally pure: Tot : Type -> CompType

    1 + 1       : Tot nat

• Conditionally pure:

  • Pure : a:Type -> wp:((a -> Type) -> Type) -> CompType

  • e: t wp terminates satisfying post e, if wp post is valid

    factorial x : Pure int (fun post -> x >=0 /\ forall y. y >= 0 ==> post y)

• Divergent terms with partial correctness specs:

  • Div : a:Type -> wp:((a -> Type) -> Type) -> CompType

  • e : Div t wp may diverge, but e r /\ wp post ==> post r

    let rec eval = function
      | App (Lam x e) e' -> eval (subst (x, e') e)
      | ... 
    : term -> Div term (fun post -> forall (x:term). post x)

Intrinsic proofs of pure programs

• Canonical, recursive implementation of quicksort

  let rec quicksort f = function 
    | [] -> []
    | pivot::tl -> let hi, lo = partition (f pivot) tl in 
                    quicksort f lo @ pivot::quicksort f hi
    

• Total correctness of quicksort, proven via a combination of F* type-checking and SMT solving

  val quicksort: f:total_order a
              -> l:list a
              -> Tot 
                  (m:list a{sorted f m /\ forall i. count i l = count i m})
                  (decreases (length l)) 

• Plus some quicksort-specific lemmas about partition and @

Termination based on well-founded orders

  val quicksort: f:total_order a
                -> l:list a
                -> Tot //Total function: semantic termination checking
                    (m:list a{sorted f m /\ forall i. count i l = count i m})
                    (decreases (length l)) //termination metric

• From library:

  let rec length = function [] -> 0 | _::tl -> 1 + length l

Full dependency and refinement types

val quicksort: f:total_order a
              -> l:list a
              -> Tot (m:list a{sorted f m /\ forall i. count i l = count i m})
                              (* ^^^^^^^^^^^refinement types^^^^^^^^^^^^^^^ *)

• From library:

  let rec sorted f = function
    | [] | [_] -> true
    | x::y::tl -> f x y && sorted f (y::tl)
  
  let rec count i = function
   | [] -> 0
   | hd::tl when i=hd -> 1 + count tl
   | _::tl -> count tl

Refinements at higher order

val quicksort: f:total_order a //refinements at higher order
              -> l:list a
              -> Tot (m:list a{sorted f m /\ forall i. count i l = count i m})

• From library:

  type total_order a = f:(a -> a -> Tot bool){
    (forall a. f a a)                                           (* reflexivity   *)
    /\ (forall a1 a2. f a1 a2 /\ f a2 a1  ==> a1 = a2)          (* anti-symmetry *)
    /\ (forall a1 a2 a3. f a1 a2 /\ f a2 a3 ==> f a1 a3)        (* transitivity  *)
    /\ (forall a1 a2. f a1 a2 \/ f a2 a1)                       (* totality  *)
   }

Extrinsic proofs of pure programs

For example, a simply-typed implementation of first-order unification - with lexicographic orders for termination

val unify : e:eqns -> list subst -> Tot (option (list subst))
            (decreases %[n_evars e; efuns e; n_flex_rhs e])
let rec unify e s = match e with
  | [] -> Some s
  | (V x, t)::tl ->
    if is_V t && V.i t = x then unify tl s //t is a flex-rhs
    else if occurs x t then None
    else (vars_decrease_eqns x t tl;
          unify (lsubst_eqns [x,t] tl) ((x,t)::s))
 | (t, V x)::tl -> //flex-rhs
   evars_permute_hd t (V x) tl;
   unify ((V x, t)::tl) s
 | (F t1 t2, F t1' t2')::tl -> //efuns reduces
   evars_unfun t1 t2 t1' t2' tl;
   unify ((t1, t1')::(t2, t2')::tl) s

• A separate lemma proving total correctess of unify

  val unify_eqns_correct: e:eqns -> Tot
      (squash (match unify_eqns e with
               | None -> not_solveable_eqns e
               | Some subst -> solved (subst_eqns subst e)))
  let unify_eqns_correct e = ...

Beyond purity

A fragment of the top-level theorem we prove of TLS:

val write : c:connection
         -> i:id
         -> rg:frange i
         -> data:DataStream.fragment i rg
         -> IO_ST_EX ioresult_w
  (requires (fun h -> 
                 current_writer_pre c i h /\
                 writeHandshake_requires h c false h))
  (ensures (fun h0 r h1 -> 
       match current_writer_T c i h1, r with 
       | Some w, Success Written -> 
         authId i 
           ==> stream_deltas w h1 == snoc (stream_deltas w h0) (DataStream.Data d)
       | ...))

This is a specification for a function that makes use of three kinds of effects: state, exceptions and IO

Rest of the talk

• Configuring F* with user-defined effects

• Intrinsic proofs of effectful programs using Dijkstra monads

• Extrinsic proofs of effectful programs using monadic reflection

A simple stateful program

let incr () =
    let x = get() in
    put (x + 1);
    let y = get() in
    assert (y > x)

To prove that the assertion at the last line always succeeds:

• A tool like Dafny or Why3, computes a weakest pre-condition for this program with respect to the post-condition, obtaining a logical formula, which is checked for validity.

F* aims to achieve something similar … let's see how this works

How does this work?

Monads, of course, in several steps

A library defines a standard state monad using DM, a simply-typed sub-language of F* for defining monadic effects

   let st a     = nat -> Tot (a * nat) //state specialized to nat for this talk
   let return x = fun s0 -> x, s0
   let bind f g = fun s0 -> let x, s1 = f s0 in g x s1
   let get ()   = fun s -> s, s
   let put s    = fun _ -> (), s

From implicit to explicitly monadic

via type and effect inference

• In F*, the programmer writes:

  let incr () =
      let x = get() in
      put (x + 1);
      let y = get() in
      assert (y > x)

• After type inference and elaboration, is made explicitly monadic (no do-notation)

  let incr () =
    bind (get ()) (fun x -> 
    bind (put (x + 1)) (fun _ ->
    bind (get ()) (fun y ->  
    return (assert (y > x)))))

  • ICFP 2011; Lightweight monadic programming in ML; Swamy, Leijen, Guts, Hicks

Deriving a WP calculus for a monadic effect

From Dijkstra: the WP of an st a computation is a predicate transformer:

  Given    st a  = nat -> Tot (a * nat)
  derive   WP_ST : st_post a -> st_pre    //signature of stateful predicate transformers
  
  where   st_post a = (a * nat) -> Type  //post-conditions
  and        st_pre = nat -> Type        //pre-conditions

Deriving a WP calculus for a monadic effect

Using a selective CPS transformation with result Type

• CPS translation of types

      (st a) = (nat -> Tot (a * nat))
              = nat -> ((a * nat) -> Type) -> Type
               ((a * nat) -> Type) -> nat -> Type
              = WP_ST a

• CPS translate terms, accordingly

      return : x:a -> (st a)
      return = fun x s0 k -> k (x, s0)
  
      bind : f:(st a) -> g:(a -> (st b)) -> (st b)
      bind = fun f g s0 k -> f s0 (fun (x, s1) -> g x s1 k)
  
      get  : unit -> (st nat)
      get  = fun () s0 k -> k (s0, s0)
  
      put  : nat -> (st unit)
      put  = fun s _ k -> k ((), s)

The -transformation really produces WPs

1. The -transformation produces monotone predicate transformers

   • E.g, for st a:

2. The -transformation produces conjunctive predicate transformers

3. The -transformation of a monad is a monad

   • Prove the monad laws in F* for a monad M

     bind (return x) f = f x
     bind f return     = f
     bind f (fun x -> bind (g x) h) = bind (bind f g) h   

   • Get for free: M, bind, return form a monad

Extending F* with the derived WP calculus

• Introduce a new computation type constructor, an abstract computation type defined in terms of Pure

  ST a wp is the type of stateful computations indexed by their predicate transformers

  ST (a:Type) (wp:(st a)) = n0:nat -> Pure (a * nat) (wp n0)

• For partial correctness, also introduce an abstract computation type defined in terms of Div

  STDiv a wp is the type of stateful, potentially divergent computations indexed by their predicate transformers

  STDiv (a:Type) (wp:(st a)) = n0:nat -> Div (a * nat) (wp n0)

Extending F* with the derived WP calculus

• Elaborate DM terms in st a to computations in ST a wp

• Identity elaboration for first-order terms:

    return : x:a -> ST a (return x)
    return x n0 = (x, n0)
    
    get    : unit -> ST nat (get ())
    get () n0 = (n0, n0)
    
    put    : n:nat -> ST unit (put ())
    put n _ = ((), n)

• A bit more involved at higher order

    bind : wp_f:(st a) -> f:ST a wp_f
          -> wp_g:(a -> (st b))) -> g:(x:a -> ST b (wp_g x))
          -> ST b (bind wp_f wp_g)
    bind wp_f f wp_g g n0 = let x, n1 = f n0 in g x n1

• An elaborated term is logically related to its WP

  • implies

Logical relation between CPS and WPs

at arbitrary order

An elaborated term is logically related to its WP

• implies

• Others have looked at WPs and CPS at first-order

  • Jensen (1978)
  • Audebaud and Zucca (1999)

• Dijkstra monads for free: the first characterization of WPs via CPS for monadic effects at arbitrary order

Adding arbitrary user-defined effects

CPS'ing the Continuation monad

• The and -elaboration work even for effects like the continuation monad itself

  let cont a = (a -> Tot ans) -> Tot ans
  let return x = fun k -> k x
  let bind f g k = f (fun x -> g x k)

• After elaboration:

    kwp a      = a -> (ans -> Type) -> Type
    KT a wp    = x:a -> Pure ans (wp x)
    return     : x:a -> wpk:kwp a -> k:kt a wpk -> Pure ans (return x wpk)
               = fun x wpk k -> k x
    bind       : wpf:(cont a)
               -> f:(wpk:kwp a -> k:kt a wpk -> Pure ans (wpf wpk))
               -> wpg:(a -> (cont b))
               -> g:(x:a -> wpk:kwp b -> k:kt b wpk -> Pure ans (wpg x wpk))
               -> wpk:kwp b
               -> k:kt b wpk
               -> Pure ans (bind wpf wpg wpk)
               = fun wpf f wpg g wpk k -> f (fun x -> wpg x wpk) (fun x -> g x wpk k)

Adding arbitrary user-defined effects

CPS'ing the Continuation monad

• The and -elaboration work even for effects like the continuation monad itself

  let cont a = (a -> Tot ans) -> Tot ans
  let return x = fun k -> k x
  let bind f g k = f (fun x -> g x k)

• After elaboration:

    kwp a      = a -> (ans -> Type) -> Type
    KT a wp    = x:a -> Pure ans (wp x)
    return     : x:a -> KT a (return x)
               = fun x wpk k -> k x
    bind       : wpf:(cont a)
               -> f:KT a wpf
               -> wpg:(a -> (cont b))
               -> g:(x:a -> KT b (wpg x))
               -> KT b (bind wpf wpg)
               = fun wpf f wpg g wpk k -> f (fun x -> wpg x wpk) (fun x -> g x wpk k)

Inferring a precise WP for a user's program

• The programmer writes:

  let incr () =
      let x = get() in
      put (x + 1);
      let y = get() in
      assert (y > x)

• After type inference and elaboration:

  let incr () =
    bind #wp_get (get ()) #wp_rest (fun x -> 
    bind #wp_put (put (x + 1)) #wp_rest1 (fun _ ->
    bind #wp_get (get ()) #wp_rest2 (fun y ->  
    return (assert (y > x)))))

• incr : ST unit (bind #(get ()) (fun x -> 
                  bind #(put (x + 1)) (fun _ -> 
                  bind #(get ()) (fun y n k -> 
                  y > x /\ k ((), n))))
       = ST unit (fun n0 post -> n0 + 1 > n /\ post ((), n0 + 1))

Checking user-provided spec against inferred WP

• Hoare triples instead of WPs

  St a (pre: nat -> Type) (post: nat -> a -> nat -> Type) 
  = ST a (fun n0 k -> pre n0 /\ forall x n1. post n0 x n1 ==> k (x, n1))

• The programmer writes:

  val incr : unit -> St unit 
    (requires (fun n -> True))
    (ensures (fun n _ n' -> True))

• F* infers

  incr : ST unit (fun n0 post -> n0 + 1 > n0 /\ post ((), n0 + 1))

• Then checks that the user-spec implies the inferred, weakest pre-condition, i.e.,

  ST unit (fun n0 post -> n0 + 1 > n0 /\ post ((), n0 + 1))
  <: St unit (fun n -> True) (fun _ _ _ -> True)
  =  ST unit (fun n0 post -> forall n1. post ((), n1)) 

Relating computation types

1. Subsumption

    ST a wp1 <: ST b wp2
     
    n0:nat -> Pure a (wp1 n0) <: n0:nat -> Pure b (wp2 n0)
     
    a <: b /\ forall n0 post. wp2 n0 post  wp1 n0 post

2. Monadic reflection (inspired by Filinski)

    //revealing representation using reify
    ST.reify (e: ST a wp) : n0:nat -> Pure (a * nat) (wp n0)
    
    //packaging representations using reflect
    ST.reflect (e: (n0:nat -> Pure (a * nat) (wp n0))) : ST a wp

3. Effect inclusion witnessed by monad morphisms

    lift (e:ST a wp) : ST_EXN a (lift wp) 

Intrinsic reasoning for effectful programs via WPs

• Intrinsic reasoning of stateful code: uses Hoare-style reasoning and decorating definitions with pre- and post-conditions

• Requires anticipating what properties might be needed of a definition in as-yet-unknown contexts

      let incr_intrinsic : St unit (requires (fun n -> True)
                                   (ensures (fun n0 _ n1 -> n1 = n0 + 1))
          = put (get() + 1)

Reifying effectful programs for extrinsic reasoning

    //revealing representation using reify
    ST.reify (e: ST a wp) : n0:nat -> Pure (a * nat) (wp n0)
    
    //packaging representations using reflect
    ST.reflect (e: (n0:nat -> Pure (a * nat) (wp n0))) : ST a wp

• Instead, reason extrinsically by

  • writing simple specifications for a definition
  • proving lemmas about effectful defs reified as pure terms

    let StNull a = ST a (λ s0 post → ∀x. post x)
    let incr : StNull unit = let n = get() in put (n + 1)
    let incr_increases (s0:s) = assert (snd (ST.reify (incr()) s0) = s0 + 1)

• Only for Pure effects, not Div

• Reify/Reflect only when the abstraction permits

Relating computation types (revisited)

1. Subsumption

    ST a wp1 <: ST b wp2
     
    n0:nat -> Pure a (wp1 n0) <: n0:nat -> Pure b (wp2 n0)
     
    a <: b /\ forall n0 post. wp2 n0 post  wp1 n0 post

2. Monadic reflection

    //revealing representation using reify
    ST.reify (e: ST a wp) : n0:nat -> Pure (a * nat) (wp n0)
    
    //packaging representations using reflect
    ST.reflect (e: (n0:nat -> Pure (a * nat) (wp n0))) : ST a wp

3. Effect inclusion witnessed by monad morphisms

    lift (e:ST a wp) : ST_EXN a (lift wp) 

Multiple monadic effects

• Define another monad in DM

    stexn a = nat -> Tot (either a string * nat)
    return_stexn, bind_stexn = ...
    raise msg = fun n0 -> Inr msg, n0

• Relate it to existing monads by providing morphisms

    lift_st_stexn : st a -> Tot (stexn a) = fun f n0 -> let x, n1 = f n0 in Inl x, n1

• -transform and -elaborate the definitions to F* obtaining another computation type

    ST_EXN : a:Type -> (stexn a) -> CompType
    ST_EXN a wp = n0:nat -> Pure (either a string * nat) (wp n0)
    
    ST_EXN_DIV : a:Type -> (stexn a) -> CompType
    ST_EXN_DIV a wp = n0:nat -> Div (either a string * nat) (wp n0)

Program implicitly with multiple monadic effects

Program with a mixture of state and exceptions and F* automatically lifts computations to use the suitable effect

• Programmer writes:

  ( / ) : int -> x:int{x<>0} -> Tot int
  let divide_by x = if x <> 0 then put (get () / x) else raise "Divide by zero"

• Elaborated to:

  let divide_by x = 
    if x <> 0 
    then lift_st_st_exn (bind_st (get()) (fun n -> put (n / x))
    else raise "Divide by zero"

• Infer the least effect for each sub-term, ensuring that reasoning and specification aren't needlessly polluted by unused effects

Loose ends

• We prove that monads like ST, Exn, StExn etc. can be implemented primitively

  • Need to restrict the use of reify and reflect to “Ghost” contexts
  • Compiler implements this by translation to OCaml's primitive effects

• Open questions

  • Extrinsic reasoning for divergent programs?

  • Type inference with effect polymorphism?

    • seems to require higher-rank universe polymorphism?

Other F* threads in the works

• Formalizing F* and its encoding to SMT

• A tactic language for F*

• F* + Lean

• Low*, a subset of F* compiled to C

  • with proofs of correctness and security

• F* to C++

  • An unverified, but high-performance extraction path

• Relational F*: Proving relations among effectful programs

  • By relating their reifications

• Stateful invariants for F*

  • Via a new pre-order indexed state monad

F*, in summary

• Open source on github, OCaml-based binaries for all platforms

• Full dependent types with inductive families, refinements, and universe polymorphism

• General recursion and the Div effect

• Termination checking with well-founded orders

• Support for user-defined monadic effects, automatically deriving a pre-order of predicate-transformer monads

• Type and effect inference

• SMT for large boring proofs

• Dependently typed programs as proofs, when SMT fails