What's new in F*?

Everest Workshop

Inria Paris, 2 October 2017

F*: produit 3 en 1

1. Functional programming language with effects

2. Semi-automated verification system using SMT

3. Interactive proof assistant based on dependent types

The current F* team

Microsoft Research, Inria Paris, MIT, Rosario, …

 Danel Ahman Benjamin Beurdouche Karthikeyan Bhargavan Tej Chajed Antoine Delignat-Lavaud Victor Dumitrescu Cédric Fournet Armaël Guéneau Cătălin Hriţcu Samin Ishtiaq Markulf Kohlweiss Qunyan Mangus Kenji Maillard Guido Martínez Clément Pit-Claudel Jonathan Protzenko Tahina Ramananandro Aseem Rastogi Nikhil Swamy (benevolent dictator) Christoph M. Wintersteiger Santiago Zanella-Béguelin Jean-Karim Zinzindohoué

Functional core of F*

• Variant of dependent type theory

• , , inductives, matches, universe polymorphism
• Recursion and semantic termination check

• potential non-termination is an effect
• Refinements

• Refined value types: x:t{p}
• Refined computation types: Pure t pre post
• computationally and proof irrelevant, discharged by SMT
• Subtyping and sub-effecting, Extensional equality

type st (mem:Type) (a:Type) = mem -> Tot (a * mem)
total reifiable 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 reifiable new_effect STATE = STATE_m heap
• this monadic definition is the model F* uses to verify stateful code
• state can be primitively implemented under the hood or not
• for instance by ML heap or C stack+heap

Verifying effectful programs

Usual way: intrinsically (using refinements at definition time)

• Hoare logic style pre- and post-conditions

let incr () : ST unit (requires (fun n0 -> True))
(ensures (fun n0 _ n1 -> n1 = n0 + 1))
= let n = STATE.get() in STATE.put (n + 1)
• Pre- and post- conditions are just syntactic sugar for WPs

• WPs computed generically for all effects

• we now obtain this for free by selective CPS-ing effect definition

STATE.repr t = mem -> t * mem
STATE.wp t  ~= mem -> (t * mem -> Type0) -> Type0

Verifying effectful programs

New way: extrinsically (by exposing pure monadic representation)

  STATE.reify : (St a) -> Ghost (nat -> Tot (a * nat))
• Allows us to give weak specification to an effectful function

  let incr () : St unit = let n = STATE.get() in STATE.put (n + 1)
• and prove lemmas about reification of effectful computation

  let incr_works (n:nat) : Lemma (snd (STATE.reify (incr()) n) = n + 1) = ()
• Reduces “relational” effectful verification to pure verification

Tactics (New, Experimental)

• 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

• user-defined, non-primitive effect: proof state + exceptions monad

  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

Early uses of tactics (proof automation)

• Arithmetic expression canonizer (Guido)

• Bitvectors in Vale (Nick G, Nik S, and Chris H)

• Separation logic (Monal and Aseem, ongoing)

• Pattern matcher (Clément, ongoing)

• upcoming case studies will probably include:

• turn F* sequence code to Low* buffer code (metaprogramming)
• generate code for inductives: pretty printers, (metaprogramming)
• metatheory of subsets of F* (interactive proofs)

Some dreams and ongoing work on F*

• Improve tactics, balance automation and control

• Studying more effects: probabilities, concurrency,

• Effect masking: hiding exceptions, state, divergence(!?),

• Verified interoperability: F* (OCaml) + Low* (C) + Vale (ASM)

• Further work out metatheory and self-certify core type-checker

• monadic reification + monotonic state and relation to modal logic
• soundly allowing depth subtyping for datatypes
• Join the team at Inria Paris and Microsoft Research