Microsoft Research, Inria Paris, Rosario, MIT, …


Interactive proof assistants  Semiautomated verifiers of imperative programs  

Coq,  CompCert,  air  Dafny,  Verve, 
Isabelle,  4 colors,  FramaC,  IronClad,  
Agda,  seL4,  Why3  miTLS  
Lean,  gap  Vale 
In the left corner: Very expressive logics (higherorder and often dependentlytyped), but purely functional
In the right:
effectful programming, SMTbased automation,
but only firstorder logic
Functional programming language with effects
Program verifier based on WPs and SMT
Interactive proof assistant based on dependent types
Other tools in this space:
Functional programming language with effects
Program verifier based on WPs and SMT
Proof assistant based on dependent types
Verified library implementing modern cryptographic primitives
Written in Low* fragment of F*, extracted to efficient and readable C
Shipping in Mozilla Firefox (NSS), Wireguard (Linux), Tezos, RIOT OS, …
Developed by: Karthikeyan Bhargavan, Benjamin Beurdouche, Marina Polubelova, Jonathan Protzenko, Jean Karim Zinzindohoué, …
The functional core of F*
Verifying functional programs
Monadic effects in F*
Verifying effectful programs
Under the hood: Dijkstra monads (for free)
Using very simple examples throughout
Recursive functions
let rec factorial n = (if n = 0 then 1 else n * (factorial (n  1)))
Inductive datatypes
type list (a:Type) =
 Nil : list a
 Cons : hd:a > tl:list a > list a
val map : ('a > 'b) > list 'a > list 'b
let rec map f x = match x with
 [] > []
 h :: t > f h :: map f t
Lambdas
map (fun x > x + 42) [1;2;3]
type nat = x:int{x>=0}
Refinements introduced by type annotations (code unchanged)
val factorial : nat > nat
let rec factorial n = (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
Dependent function types (), 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}
The F* functions we saw so far were all total
Tot
effect (default) = no sideeffects, terminates on all inputs
val factorial : nat > Tot nat
let rec factorial n = (if n = 0 then 1 else n * (factorial (n  1)))
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)
<<
)
<
(negative integers unrelated)
%[a;b;c]
with lexicographic ordering
let rec ackermann (n m : nat) : Tot nat (decreases %[m;n]) =
if m=0 then n + 1
else if n = 0 then ackermann 1 (m  1)
else ackermann (ackermann (n  1) m) (m  1)
let rec ackermann (m n : nat) : Tot nat = ...
We might not want to prove all code terminating
val factorial : int > Dv int
Some useful code really is not always terminating
val eval : exp > Dv exp
let rec eval e =
match e with
 App (Lam x e1) e2 > eval (subst x e2 e1)
 App e1 e2 > eval (App (eval e1) e2)
 Lam x e1 > Lam x (eval e1)
 _ > e
let main = eval (App (Lam 0 (App (Var 0) (Var 0)))
(Lam 0 (App (Var 0) (Var 0))))
./Divergence.exe
Pure code cannot call potentially divergent code
Only pure code can appear in specifications
val factorial : int > Dv int
type tau = x:int{x = factorial (1)}
^^^^^^^^^^^^^^^^^^
Expected a pure expression; got an expression ... with effect "DIV"
Subeffecting: Tot t <: Dv t
(e.g. divergent code can include pure code)
incr 2 + factorial (1) : Dv int
val factorial : nat > Tot nat
val factorial : x:int > Pure int (requires (x >= 0))
(ensures (fun y > y >= 0))
Pure
, Div
), 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))
val factorial : nat > Dv nat
Div
computation type (pre and post conditions)
val eval_closed : e:exp > Div exp (requires (closed e))
(ensures (fun e' > Lam? e' /\ closed e'))
let rec eval_closed e =
match e with
 App e1 e2 > let Lam e1' = eval_closed e1 in
below_subst_beta 0 e1' e2;
eval_closed (subst (sub_beta e2) e1')
 Lam e1 > Lam e1
Dv
just an abbreviation
Dv t = Div t (requires True) (ensures (fun _ > True))
Two classes of types
t
): int
, list int
, …
C
): Tot t
and Dv t
Dependent function types of the form: x:t > C
Two forms of refinement types
x:t{p}
Pure t pre post
and Div t pre post
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 (#a:Type) (xs : list a) (ys : list a) :
Lemma (ensures (length (append xs ys) = length xs + length ys)) = ...
val preservation : #e:exp > #e':exp > #g:env > #t:typ >
ht:(typing g e t) > hs:step e e' > Tot (typing g e' t) (decreases ht)
let rec preservation #e #e' #g #t (TyApp h1 h2) hs =
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)
val progress : #e:exp > #t:typ > h:typing empty e t >
Pure (cexists (fun e' > step e e'))
(requires (~ (is_value e)))
(ensures (fun _ > True)) (decreases h)
let rec progress #e #t h =
match h with
 TyApp #g #e1 #e2 #t11 #t12 h1 h2 >
match e1 with
 ELam t e1' > ExIntro (subst (sub_beta e2) e1') (SBeta t e1' e2)
 _ > let ExIntro e1' h1' = progress h1 in
ExIntro (EApp e1' e2) (SApp1 e2 h1')
Note: match exhaustiveness check also semantic (via SMT)
Dependent type theory variant
Recursion and semantic termination check
Refined value and computation types
Subtyping and subeffecting
Extensional equality
Effects defined using monads
type st (mem:Type) (a:Type) = mem > Tot (a * mem)
total new_effect {
STATE_m (mem:Type) : a:Type > Effect
with repr = st mem;
return = fun (a:Type) (x:a) (m:mem) > x, m;
bind = fun (a b:Type) (f:st mem a) (g:a > st mem b) (m:mem) >
let z, m' = f m in g z m';
get = fun () (m:mem) > m, m;
put = fun (m:mem) _ > (), m }
total new_effect STATE = STATE_m nat // keeping it simple
STATE
is not)
State and exception monad
let stexn a = nat > Tot ((either a string) * nat))
new_effect {
STEXN: a:Type > Effect with
repr = stexn;
return = fun (a:Type) (x:a) s > Inl x, s;
bind = fun (a b:Type) (f:stexn a) (g:a > stexn b) s0 >
let (r,s1) = f s0 in
match r with
 Inl ret > Inl (g ret s1), s1
 Inr m > Inr m, s1
raise = fun (a:Type) (msg:string) s > Inr msg, s
}
sub_effect STATE ~> STEXN {
lift = fun (a:Type) (e:st nat a) > (fun s > let (x,s') = e s in Inl x, s')
}
In F*, the programmer writes:
let incr () =
let x = STATE.get() in
STATE.put (x + 1);
let y = STATE.get() in
assert (y > x)
Made explicitly monadic via type and effect inference
let incr () =
STATE.bind (STATE.get ()) (fun x >
STATE.bind (STATE.put (x + 1)) (fun _ >
STATE.bind (STATE.get ()) (fun y >
STATE.return (assert (y > x)))))
Programmer writes:
( / ) : int > x:int{x<>0} > Tot int
let divide_by (x:int) : STEXN unit ...
= if x <> 0 then put (get () / x) else raise "Divide by zero"
Elaborated to:
let divide_by x =
if x <> 0 then STATE_STEXN.lift (STATE.bind (STATE.get())
(fun n > STATE.put (n / x)))
else STEXN.raise "Divide by zero"
F* infers the least effect of each subterm
Hoare (type theory) style pre and postconditions
val incr : unit > ST unit (requires (fun n0 > True))
(ensures (fun n0 _ n1 > n1 = n0 + 1))
let incr () =
let x = STATE.get() in
STATE.put (x + 1)
Beyond what can be expressed with value refinements
Now precondition is relation on initial states; postcondition is relation on initial states, result values, and final states
Revealing pure effect representation
STATE.reify (e : ST a pre post)
: n0:nat > Pure (a * nat) (requires (pre n0))
(ensures (fun r > post n0 (fst r) (snd r))
Allows us to give weak specification to an effectful function
let incr () : ST a (requires (fun _ > True)) (ensures (fun _ _ _ > True))
= let n = STATE.get() in STATE.put (n + 1)
… then prove lemmas about reification of effectful computation
let incr_increases (s0:s) : Lemma (snd (ST.reify (incr()) s0) = s0 + 1) = ()
only works for code proved terminating
reify/reflect only when the abstraction permits (e.g. ghost code)
Reducing effectful verification to pure verification
Recent experiments using this for “relational reasoning”
F* tactics written as effectful F* code (inspired by Lean, Idris)
have access to F*'s proof state (and can efficiently roll it back)
can introspect on F* terms (deep embedding, simply typed)
can be interpreted by F*'s normalizer or compiled to OCaml
userdefined, nonprimitive effect: proof state + exceptions
noeq type __result a =
 Success of a * proofstate
 Failed of string //error message
* proofstate //the proofstate at time of failure
let __tac (a:Type) = proofstate > Tot (__result a)
reifiable reflectable new_effect {
TAC : a:Type > Effect
with repr = __tac ... }
let tactic (a:Type) = unit > Tac a
Nonlinear arithmetic (proof automation, reflective)
Bitvectors in Vale (proof automation)
Separation logic (proof automation)
Pattern matcher (metaprogramming)
Efficient lowlevel parsers and printers (metaprogramming)
Type classes (metaprogramming)
Pre and post conditions are just syntactic sugar:
Pure t (pre : Type0) (post : t>Type0)
= PURE t (fun k > pre /\ forall y. post y ==> k y)
val factorial : x:int > Pure int (requires (x >= 0)) (ensures (fun y > y >= 0))
val factorial : x:int > PURE int (fun k > x >= 0 /\ forall y. y >= 0 ==> k y)
Same for userdefined effects, like state:
ST t (pre : nat > Type0) (post : nat > t > nat > Type0)
= STATE t (fun n0 k > pre n0 /\ forall x n1. post n0 x n1 ==> k x n1)
val incr : unit > ST unit (requires (fun n0 > True))
(ensures (fun n0 _ n1 > n1 = n0 + 1))
val incr : unit > STATE unit (fun n0 k > k () (n0 + 1))
let incr () = STATE.bind (STATE.get()) (fun x > STATE.put (x + 1))
By inferring type for incr
against following interface:
STATE.get : unit > STATE nat (STATE.get_wp())
STATE.put : n:nat > STATE unit (STATE.put_wp n)
STATE.bind : STATE 'a 'wa >
(x:'a > STATE 'b ('wb x)) >
STATE 'b (STATE.bind_wp 'wa 'wb)
… we compute the weakest precondition for incr
val incr : unit > STATE unit
(STATE.bind_wp (STATE.get_wp()) (fun x > STATE.put_wp (x + 1)))
= (fun n0 k > k () (n0 + 1))
Generic way of computing weakestpreconditions for all effects, provided we have a monad on predicate transformers
let STATE.wp t = (t > nat > Type0) > (nat > Type0)
val STATE.return_wp : 'a > Tot (STATE.wp 'a)
val STATE.bind_wp : (STATE.wp 'a) >
('a > Tot (STATE.wp 'b)) >
Tot (STATE.wp 'b)
val STATE.get_wp : unit > Tot (STATE.wp nat)
val STATE.put_wp : nat > Tot (STATE.wp unit)
we need to implement this Dijkstra monad:
let STATE.return_wp v = fun p > p v
let STATE.bind_wp wp f = fun p > wp (fun v > f v p)
let STATE.get_wp () = fun p n0 > p n0 n0
let STATE.put_wp n = fun p _ > p () n
and for a while we wrote such things by hand;
but this is quite tricky and comes with strong proof obligations
(correctness with respect to effect definition, monad laws, …)
The state predicate transformer:
STATE.wp t = (t > nat > Type0) > (nat > Type0)
~= nat > (t * nat > Type0) > Type0
… can be automatically derived,
StT M t = nat > M (t * nat)
Type0
(i.e. transformer for PURE
)
Cont t = (t > Type0) > Type0
This works well for large class of monadic effects:
state, exceptions, continuations, etc.
From monadic effect definition we can derive a correctbyconstruction weakestprecondition calculus for this effect.
Improve tactics, balance automation and control
Dijkstra monads for free, semantically
Studying more effects: probabilities, concurrency, …
Effect masking: hiding exceptions, state, divergence(!?), …
Further work out metatheory, selfcertify core typechecker
Functional programming language with effects
Program verifier based on WPs and SMT
Interactive proof assistant based on dependent types
Open source, code on GitHub
Tutorial, papers, slides at fstarlang.org