Dijkstra monads for free

Deriving and extending the effectful semantics of F*

Nikhil Swamy

Microsoft Research

  • And invaluable collaborators:

    Catalin Hritcu, Danel Ahman, Guido Martinez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, Chantal Keller, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, Santiago Zanella-Béguelin, Daan Leijen, Nataliya Guts, Michael Hicks, Gavin Bierman, Clement Pit-Claudel, Perry Wang

Shall the twain ever meet?

The two, mostly disjoint sides of program verification research

Interactive proof assistants Semi-automated verifiers of imperative programs
Coq, CompCert,   air Dafny, Verve,
Isabelle, seL4, FramaC, IronClad,
Agda, Bedrock, Vcc, miTLS
Lean, Feit-Thompson   gap Verifast,

  • 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

F* in action: Other examples

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

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

  • $\mu$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:

  • $\lambda$, $\Pi$, 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 $t$
    • Computation types $C$

  5. Two forms of refinement types with proof irrelevance …

Refined value types

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

  • Some examples: 

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

  • The proof of $\phi$ is never materialized 

      squash $\phi$ = _:unit{$\phi$}

Refined computation types

  • Unconditionally pure: Tot : Type -> CompType 

      1 + 1       : Tot nat

  • Conditionally pure:

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

    • e:$\kw{Pure}$ 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$_0$) -> Type$_0$) -> CompType

    • e : Div t wp may diverge, but e $\Downarrow$ 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 $\top$ 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$\cps$, 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$_0$  //post-conditions
  and        st_pre = nat -> Type$_0$        //pre-conditions

Deriving a WP calculus for a monadic effect

Using a selective CPS transformation with result Type$_0$

  • CPS translation of types $(\cdot)\cps$ 

        (st a)$\cps$ = (nat -> Tot (a * nat))$\cps$
            = nat -> ((a * nat) -> Type$_0$) -> Type$_0$
            $\sim$ ((a * nat) -> Type$_0$) -> nat -> Type$_0$
            = WP_ST a

  • CPS translate terms, accordingly 

        return$\cps$ : x:a -> (st a)$\cps$
    return$\cps$ = fun x s0 k -> k (x, s0)

    bind$\cps$ : f:(st a)$\cps$ -> g:(a -> (st b)$\cps$) -> (st b)$\cps$
    bind$\cps$ = fun f g s0 k -> f s0 (fun (x, s1) -> g x s1 k)

    get$\cps$  : unit -> (st nat)$\cps$
    get$\cps$  = fun () s0 k -> k (s0, s0)

    put$\cps$  : nat -> (st unit)$\cps$
    put$\cps$  = fun s _ k -> k ((), s)

The $\cps$-transformation really produces WPs

  1. The $\cps$-transformation produces monotone predicate transformers

    • E.g, for st a: $(\psi_1 x ==> \psi_2 x) ==> w~n_0~\psi_1 ==> w~n_0~\psi_2$

  2. The $\cps$-transformation produces conjunctive predicate transformers

    • $w~\psi_1~\wedge~w~\psi_2 \iff w~(\lambda x. \psi_1~x~\wedge~\psi_2~x)$

  3. The $\cps$-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$\cps$, bind$\cps$, return$\cps$ 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)$\cps$) = 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)$\cps$) = n0:nat -> Div (a * nat) (wp n0)

Extending F* with the derived WP calculus

  • Elaborate DM$\cps$ terms in st a to computations in ST a wp

  • Identity elaboration for first-order terms: 

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

  • A bit more involved at higher order 

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

  • An elaborated term $\ul{e}$ is logically related to its WP $e\cps$

    • $\Delta \mid \cdot \vdash e : C$ implies $\ul\Delta \vdash \ul{e} : F_C~e\cps$

Logical relation between CPS and WPs

at arbitrary order

An elaborated term $\ul{e}$ is logically related to its WP $e\cps$

  • $\Delta \mid \cdot \vdash e : C$ implies $\ul\Delta \vdash \ul{e} : F_C~e\cps$

  • 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 $\cps$ and $\ul{\ }$-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$_0$) -> Type$_0$
  KT a wp    = x:a -> Pure ans (wp x)
  return     : x:a -> wpk:kwp a -> k:kt a wpk -> Pure ans (return$\cps$ x wpk)
             = fun x wpk k -> k x
  bind       : wpf:(cont a)$\cps$
             -> f:(wpk:kwp a -> k:kt a wpk -> Pure ans (wpf wpk))
             -> wpg:(a -> (cont b)$\cps$)
             -> 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$\cps$ 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 $\cps$ and $\ul{\ }$-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$_0$) -> Type$_0$
  KT a wp    = x:a -> Pure ans (wp x)
  return     : x:a -> KT a (return$\cps$ x)
             = fun x wpk k -> k x
  bind       : wpf:(cont a)$\cps$
             -> f:KT a wpf
             -> wpg:(a -> (cont b)$\cps$)
             -> g:(x:a -> KT b (wpg x))
             -> KT b (bind$\cps$ 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$\cps$ #(get$\cps$ ()) (fun x -> 
                bind$\cps$ #(put$\cps$ (x + 1)) (fun _ -> 
                bind$\cps$ #(get$\cps$ ()) (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$_0$) (post: nat -> a -> nat -> Type$_0$) 
= 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
 $\iff$ 
 n0:nat -> Pure a (wp1 n0) <: n0:nat -> Pure b (wp2 n0)
 $\iff$ 
 a <: b /\ forall n0 post. wp2 n0 post $\Longrightarrow$ 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$\cps$ 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
 $\iff$ 
 n0:nat -> Pure a (wp1 n0) <: n0:nat -> Pure b (wp2 n0)
 $\iff$ 
 a <: b /\ forall n0 post. wp2 n0 post $\Longrightarrow$ 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$\cps$ wp)

Multiple monadic effects

  • Define another monad in DM$\cps$ 

      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

  • $\cps$-transform and $\ul{\ }$-elaborate the definitions to F* obtaining another computation type 

      ST_EXN : a:Type -> (stexn a)$\cps$ -> CompType
  ST_EXN a wp = n0:nat -> Pure (either a string * nat) (wp n0)
  
  ST_EXN_DIV : a:Type -> (stexn a)$\cps$ -> 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

https://​fstar-​lang.​org