Extending F* in F*: Proof automation and Metaprogramming for Typeclasses

Опубликовано 27 сентября 2018, 17:01

Abstract for Talk Title 1: Extending F* in F*: Proof automation and Metaprogramming for Typeclasses, Concurrency, Optimizations and More

In this talk we will provide an overview of the road we've been following for the past year with Meta-F*, the tactics and metaprogramming engine for F*. While F* itself is a highly-automated theorem prover and program verifier, there are unavoidable limitations to its automation. Meta-F* aims to put the programmer in near full control of F*'s behaviour, allowing to nudge, tweak, twist and compose its internal components in a safe fashion.

We introduce the "meta" into F* via a custom effect, making Meta-F* a part of F*, and not something above it. We provide several "hooks" into Meta-F*, allowing to preprocess or solve proof obligations, generate terms and top-level definitions, implement custom strategies for solving implicit arguments (birthing F*'s typeclasses), and transforming programs before extracting (to OCaml, F#, or C). We ensure the safety of these transformations by designing Meta-F* to closely follow F*'s static semantics. Further, metaprograms can be compiled and linked into the compiler, obtaining fast-and-safe extension capabilities for F*, and blurring the line between the compiler's source code and Meta-F* metaprograms.

We will describe some interesting use cases for Meta-F*, including arithmetic expression canonicalization, automated provably-memory-safe parser and printer generation, and some ongoing work in reasoning about concurrent programs in F*.

Abstract for Talk Title 2: Layered DSLs for Verified Stateful Programming

Cryptographic code is security- and performance-critical and hence it calls for high-assurance, efficient implementations. However, optimized low-level code is not a good target for formal verification. To mitigate this, a two-layered verification approach is often employed: the efficient low-level code is shown to adhere to a high-level implementation, which is more amenable to formal verification. Low* is a subset of C, shallowly embedded in F*, that was build to assist this process. It gives access to the full memory model of C while supporting F*-style formal verification, allowing efficient crypto programs to be verified against their purely functional specs.

This work aims to further reduce the gap between high-level code written with verification in mind and low-level code optimized for efficiency. In particular, following ideas from bidirectional programing, we allow the user to express their algorithms as pure programs that operate on some high-level, purely functional state that provides a view of C’s memory. High-level programs written in this style enjoy a straight-forward interpretation as low-level programs. To further optimize these low-level programs we provide a set of rewrite rules whose soundness has been verified in F* and can be applied using F*’s tactic engine, in order to obtain an efficient and correct by construction Low* program.

See more at microsoft.com/en-us/research/v...