Deriving and extending the effectful semantics of F*
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
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
A general purpose, strict, higher-order effectful language
An SMT-based, semi-automated program verification tool,
On a foundation of dependent and inductive types
Also in the gap: ATS, HTT, Idris, Trellys, …
Everest: A verified, drop-in replacement for the HTTPS stack, built mainly using F*
TLS-1.2 and TLS-1.3:
Verified elliptic curve cryptography:
Compiled to OCaml by default, but a subset of F* compiled to C for efficiciency:
F* is programmed in F* and bootstraps in OCaml or F#.
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*
…
Case studies --
Language design ++
A mostly standard dependent type theory at the core:
match
, universe polymorphism
Plus, specific to F*
Extensional equality, works well with refinement types
Fixed points with termination based on well-founded orders
General recursion (non-termination)
Two classes of types (similar to call-by-push-value):
Two forms of refinement types with proof irrelevance …
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{}
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)
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 @
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
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
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 *)
}
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 = ...
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
Configuring F* with user-defined effects
Intrinsic proofs of effectful programs using Dijkstra monads
Extrinsic proofs of effectful programs using monadic reflection
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:
F* aims to achieve something similar … let's see how this works
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
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)))))
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
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)
-transformation really produces WPsThe -transformation produces monotone predicate transformers
st a
:
The -transformation produces conjunctive predicate transformers
The -transformation of a monad is 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
M, bind, return
form a monad
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)
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
An elaborated term is logically related to its WP
Others have looked at WPs and CPS at first-order
Dijkstra monads for free: the first characterization of WPs via CPS for monadic effects at arbitrary order
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)
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)
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))
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))
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
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
Effect inclusion witnessed by monad morphisms
lift (e:ST a wp) : ST_EXN a (lift wp)
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)
//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
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
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
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
Effect inclusion witnessed by monad morphisms
lift (e:ST a wp) : ST_EXN a (lift wp)
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 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
We prove that monads like ST
, Exn
, StExn
etc. can be implemented
primitively
reify
and reflect
to “Ghost” contexts
Open questions
Extrinsic reasoning for divergent programs?
Type inference with effect polymorphism?
Formalizing F* and its encoding to SMT
A tactic language for F*
F* + Lean
Low*, a subset of F* compiled to C
F* to C++
Relational F*: Proving relations among effectful programs
Stateful invariants for F*
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