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

### A framework for verifying ML-like programs

• Higher order, effectful, call-by-value

• F + dependent types + effects

• Highly customizable

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

### 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:

1 + 1       : Tot int  
• Conditionally 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:

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

### lattice of primitive effects

For example:

• 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

  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:

• The program has type , given the validity of a logical formula

• is passed to Z3 to check for validity in context

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

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

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

### Plan

• How to use F* with F# and OCaml

• Demo: Several small verified programs

### Migration

• No objects

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

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

### Verification

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

• 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

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

• No Obj.t; only System.Object

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