Nothing

Dependent types and Effects in F*

Short talk & demo

Nik Swamy & Catalin Hritcu

Aseem Rastogi, Chantal Keller, Simon Forest, Karthik Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Jean-Karim Zinzindohoue, Markulf Kohlweiss, Pierre-Yves Strub

Microsoft Research, MSR-INRIA, INRIA, UMD

 https://fstar-lang.org

fstar-logo

A framework for verifying ML-like programs

  • Higher order, effectful, call-by-value

  • F$\omega$ + dependent types + effects

  • Highly customizable

    • Very little is baked in; most semantics governed by libraries
    • Easily experiment with memory representations, effects etc.

A brief history of an evolving line of languages

timeline

F* Situated

  • Many semi-automated verifiers for first-order languages

    • Relatively simple logics, effectful, good SMT automation
  • Many interactive proof assistants

    • Good control, but automation lacking; effects via encoding
  • F* tries to span the divide

    • Higher order with primitive effects
    • SMT for large boring proofs
    • Dependently typed programs as proofs, when SMT fails
    • Highly flexible, customizable with user-defined effects
    • Open source, bootstraps, binaries for all platforms

Indexed monadic effects and dependent types

Every expression is classified with a indexed, monadic effect

  • Unconditionally pure: $\Tot$

    1 + 1       : Tot int  
  • Conditionally pure: $\kw{Pure}$

    factorial x : Pure int (requires (x >= 0)) (ensures (fun y -> y >= 0)) 
  • By refinement subtyping:

    type nat = x:int{x >= 0}
    factorial 1 : Tot nat
  • Stateful: $\kw{ST}$

    x := 17     : ST unit (requires (fun h -> h contains x)) 
    (ensures (fun h0 _ h1 -> h1 = upd h0 x 17))

F*: Parameterized by a user-defined

lattice of primitive effects

For example:

lattice-1

  • Can also pick other effects (e.g., Ghost, IO, NonDet, )

  • Each effect is a monad equipped with its own WP calculus

  • Lifting from one effect to another is a monad morphism, embedding one WP calculus in another

Call-by-value semantics

Functions have monadic co-domains

  x:t -> M s phi_1 ... phi_n
  • Shorthand for ML-ish arrows
    x1:t1 -> ... -> xn:tn -> t
    =
    x1:t1 -> Tot ( ... -> Tot (xn:tn -> ML t))
fstar factorial.fst
Verified module: Factorial
All verification conditions discharged successfully

F* builds a typing derivation of the form:

$\Gamma \vdash \mbox{\texttt{(let factorial n = e)}} : \mathbb{N} \rightarrow~\mathtt{Tot}~\mathbb{N} \mid \phi$

  • The program $\mbox{\texttt{let factorial n = e}}$ has type $\mathbb{N} \rightarrow~\mathtt{Tot}~\mathbb{N}$, given the validity of a logical formula $\phi$

  • $\phi$ is passed to Z3 to check for validity in context $\Gamma$

  • If the check succeeds, then, from the metatheory of F*, the program is safe at type $t$

    • If the check fails, can still provide a dependently typed program as a proof term
  • Compile to Ocaml or F# for execution

F* Reloaded: What we've used it for, so far

About 45,000 lines of verified code in our test suite.

  • F* as a proof assistant

    • Metatheory of $\mu$F* in F*
  • F* as a host for several verification-oriented embedded DSLs

    • Region-based memory management (using a new native region library in OCaml)
    • A DSL and interpreter for secure multi-party computations
  • F* for verifying cryptographic protocols

    • A new, verified implementation of TLS-1.2/1.3, in the works

Learn more about F*

  • Several courses taught on this material so far
  • + On Friday, an F* tutorial at CUFP
    • Sign up!
  • Snag a t-shirt : )

Plan

  • How to use F* with F# and OCaml

  • Demo: Several small verified programs

Gradually verifying an ML program

interop1

Gradually verifying an ML program

interop2

Migration

interop3

  • No objects

  • No functors; but, F* is like F$\omega$, so encode if you must

  • list int (or list<int> for F# users)

Verification

interop4

  1. Just check effects (Pure, Div, ST, Exn, etc. )

  2. Add simple data refinements to check basic invariants

    • array indexing, exhaustiveness of patterns, etc.
  3. Specify more invariants, towards functional correctness

  4. Relational proofs for optimizations and security properties

Extraction to OCaml

interop5

  • Erasure of ghost code and proof terms; erasure of fancy types

  • Insertion of Obj.magic as little as possible

    • Dependent types, inductive families
    • Higher-rank polymorphism, value restriction, polymorphic recursion

Safety of interop with OCaml

interop6

  • At the interface, the type erasure should be the identity
  • User can insert verified wrappers, if needed
  • But, this is not always possible, e.g.,
      val sort_with: a:Type -> f:total_order a -> l:list a 
    -> Tot (m:list a{sorted f m /\ permutation l m})

Extraction to and interop with F#

interop6

  • No Obj.t; only System.Object

    • But, can't cast list<t> to list<Object>
  • No Obj.magic; only checked casts

Demo