Exploring Proof-Oriented Programming in F*
Learn how to customize F* to tailor to your program logic with insights from Aseem Rastogi from Microsoft Research. Delve into the world of F* programming, a functional language akin to OCaml and Haskell, featuring advanced type systems and interactive proof capabilities. Discover examples, details on indexed effects, and the landscape of F* in verified assembly code, domain-specific languages, and more.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Proof-oriented Programming in F* How to customize F* to your own program logic Aseem Rastogi Microsoft Research (Joint work with my collaborators: https://project-everest.github.io/people/)
Talk outline F* overview Introduction to F* by examples Indexed effects in F* (a.k.a. customize F* for your own program logic)
What is F* https://www.fstar-lang.org A functional programming language Like OCaml, F#, Haskell F* programs can be compiled to OCaml and F# by-default* Expressive type system based on dependent type theory (like proof assistants Coq, Lean, Agda, Idris, ) Meta-programming and tactics for interactive proofs (like Coq, Lean, Isabelle, ) SMT-based semi-automation (like program verifiers Dafny, Why3, )
A first example type list (a:Type) = let rec length (l:list a) = | Nil : list a match l with | Cons : a -> list a -> list a | [] -> 0 | _::tl -> 1 + length tl //[1; 2] Cons 1 (Cons 2 Nil) //append [1] [2] = [1; 2] let rec append (l1 l2:list a) = let rec length_append (l1 l2:list a) : Lemma (ensures length (append l1 l2) = length l1 + length l2) = match l1 with | [] -> () | _::tl -> length_append tl l2
Behind the scenes ? ? Typing derivation
F* Landscape Verified assembly code Verified C programs Vale Low* Embedded domain- specific languages Concurrency and distribution with separation logic Steel Verified parser generator Logical foundations of programs and proofs Interfacing with existing toolchains X86 C OCaml, F#, Rust? WebAssembly Assembly
F* and friends EverParse HACL* Vale EverCrypt QUIC Veritas mitls More than 600,000 lines of F* Under Continuous Integration Built several times a day
Proofs for Billions of Unsuspecting Users Automated parsing untrusted data with proofs in Hyper-V/VMSwitch DICE Verita s Wysteria An upcoming TCG standard for boot firmware (e.g. in IoT) Cloud infrastructure Verified cryptography in the Linux kernel Verified Merkle trees for Enterprise blockchains Secure communications MSQuic in Windows, Verified crypto in Firefox, mbedTLS, Signal in Wasm, Wireguard, Quic transport, High-value domains: Fintech, verifiable computing,
Basic types, functions as first-class values, lambdas type empty = type unit = () type bool = true | false let incr (x:int) : int = x + 1 let apply_twice (f:a -> a) (x:a) = f (f x) let add_2 (x:int) : int = apply_twice incr x let add_4 (x:int) : int = apply_twice (fun x -> x + 2) x //lambdas
Inductive types, pattern matching, recursion type list (a:Type) = | Nil : list a | Cons : a -> list a -> list a //[1; 2] Cons 1 (Cons 2 Nil) let rec map (f:a -> b) (l:list a) : list b = match l with | [] -> [] | hd::tl -> f hd :: map f tl
Semantic termination checking Semantic termination checking Based on well-founded ordering ( << ) let rec map (f:a -> b) (l:list a) : list b - a:nat << b:nat if a < b = match l with | [] -> [] - Inductive subterm ordering - hd << Cons hd tl and tl << Cons hd tl | hd::tl -> f hd :: map f tl - User-defined well-founded relations - Primitive support for lexicographic ordering let rec ackermann (m n : nat) : nat (decreases %[m;n]) = if m=0 then n+1 else if n=0 then ackermann (m-1) 1 else ackermann (m-1) (ackermann m (n-1))
Refinement types type nat = x:int{x >= 0} x:t{phi} type pos = x:int{x > 0} where x may occur free in phi type monotonic = f:int -> int{ Intuition: values of type t that satisfy phi forall x y. (x <= y) => (f x <= f y) } //coercive let f (x:int) : nat = if x >= 0 then x else 0
Dependent function types let incr (x:int) : y:int{y > x} = x + 1 let rec sum (x:nat) : y:nat{y >= x} = if x = 0 then 0 else x + sum (x-1) //writing specifications using dependent types let rec length_append (l1 l2:list a) : Lemma (ensures length (append l1 l2) = length l1 + length l2) = match l1 with | [] -> () | _::tl -> length_append tl l2
Proofs by Induction //writing specifications using dependent types let rec length_append (l1 l2:list a) : Lemma (ensures length (append l1 l2) = length l1 + length l2) = match l1 with | [] -> () | _::tl -> length_append tl l2 //invoke Induction Hypothesis Proof by induction on list l1: Base case, l1 = [] L.H.S. = length (append [] l2) = length l2 R.H.S. = length [] + length l2 = length l2 Inductive case: l1 = hd::tl Induction Hypothesis: length (append tl l2) = length tl + length l2 L.H.S. = length (append hd::tl l2) = length (hd::append tl l2) = 1+length (append tl l2) //apply I.H. at this step = 1+length tl+length l2 = length l1+length l2 = R.H.S.
Effectful programming and proving So far, we have seen side-effects free, terminating functions of type a -> b What about programming and proving with effects? State, exception, I/O, non-determinism, Indexed effects: a user-extensible effect system in F* Based on modeling effects using monads (Wadler, Moggi, )
Computation types In general functions have types: x:a -> M b is Type (M b is) is called a computation type M is an effect label, upper-bound on the effect of the function Effects are arranged in an ordering is are the effect indices, may encode effect-specific program logic
Primitive effects Pure and Div Pure a pre post where pre : prop and post : a -> prop A side-effect free computation that if called when pre holds, terminates, and returns a result of type a s.t. post a holds Div a pre post Similar, but the computation may diverge Tot a =def= Pure a True (fun _ -> True) a -> b =def= a -> Tot b a -> Lemma pre post =def= a -> Pure unit pre (fun _ -> post)
Modeling effects using monads Choose a representation for effectful functions Define two combinators that obey monadic laws: return : turn a pure value into an effectful computation bind : compose two effectful computations Define basic actions type st (a:Type) = int -> a * int let return (x:a) = fun s -> s, x let bind (f:st a) (g:a -> st b) : st b = fun s0 -> let s1, x = f s0 in (g x) s1 let get () : st int = fun s -> s, s let put (s:int) : st unit = fun _ -> (), s
Programming with monads type st (a:Type) = int -> a * int let return (x:a) = fun s -> s, x let bind (f:st a) (g:a -> st b) : st b = fun s0 -> let s1, x = f s0 in (g x) s1 let get () : st int = fun s -> s, s let put (s:int) : st unit = fun _ -> (), s let incr () : st int = bind (get ()) (fun s -> bind (put (s+1)) (fun _ -> return s))) //with shorthand let incr () : st int = s <- get (); put (s+1);; return s
Proving with monads type st (a:Type) is = ... Indexed monads : indices encode reasoning principles Several of them in the literature (graded monads, parameterized monads, ) Indexed effects in F* : A unifying framework for programming and proving with indexed monads and combinations thereof Example: Reasoning for stateful computations
Examples FStar/Sec1.GST.fst at master FStarLang/FStar (github.com) FStar/HoareST.fst at master FStarLang/FStar (github.com) FStar/examples/layeredeffects at master FStarLang/FStar (github.com)
Indexed effects Indexed effects in F* : A unifying framework for programming and proving with indexed monads and combinations thereof Abstraction Composition (via lifts and layering) Primitive syntax (let in) Seamless integration with rest of F* Inductive types, recursion, termination checking, refinement types, for free! Customize F* to your own program logic!
Indexed effects in action https://www.fstar-lang.org/papers/indexedeffects/ Steel, embedding of Concurrent Separation Logic in F*, based on indexed effects The indices are separation logic pre- and post assertions A variant has two additional indices for Hoare-style pre- and post Described in our ICFP 20 and ICFP 21 papers Meta-programming and tactics framework in F* Meta-programs are F* programs in the TAC indexed effect See ulib/FStar.Tactics.Effect.fsti DY*: Bhargavan et al., Euro S&P 21, based on a state and exception indexed effect https://github.com/reprosec/dolev-yao-star
