What's new in F*?

fstar-logo

Cătălin Hriţcu, Inria Paris

Everest Workshop

Inria Paris, 2 October 2017

3-en-1

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é

fstar-v0.9.5

fstar-v0.9.4

Functional core of F*

  • Variant of dependent type theory

    • $\lambda$, $\Pi$, 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

Monadic effects in F*

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

    • relies on a monad on predicate transformers (Dijkstra monad)

    • 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)

  • Monadic reification

      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

Tactics can discharge SMT obligations

tactics-assert_by_tactic

Tactics can massage SMT obligations

tactics-canon

Tactics can synthesize F* terms (metaprogramming)

tactics-synth_by_tactic

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

  • Better treatment of effects: Dijkstra monads for free v2

  • 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

It will be a long journey, but we've already done 2/3 of the way

66-percent-there