Meta-F*: Proof Automation with SMT, Tactics and Metaprograms

Guido Martínez (CIFASIS-CONICET, Rosario, Argentina)
Danel Ahman (University of Ljubljana, Slovenia)
Victor Dumitrescu (Prosecco, INRIA, Paris, France)
Nick Giannarakis (Department of Computer Science, Princeton University, Princeton, NJ, USA)
Chris Hawblitzel (Systems Research Group, Microsoft Research, Redmond, WA, USA
Catalin Hritcu (Prosecco)
Monal Narasimhamurthy (Programming Languages and Verification, University of Colorado, Boulder, CO, USA)
Zoe Paraskevopoulou (Department of Computer Science, Princeton University, Princeton, NJ, USA)
Clément Pit-Claudel (Programming Languages and Verification, Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, MA, USA)
Jonathan Protzenko (RiSE: Research in Software Engineering, Microsoft Research, Redmond, WA, USA)
Tahina Ramananandro (RiSE)
Aseem Rastogi (Microsoft Research, Bengaluru, Karnataka, India)
Nikhil Swamy (RiSE)

ESOP 2019 (accepted for publication, to appear)

We introduce Meta-F*, a tactics and metaprogramming framework for the F* program verifier. The main novelty of Meta-F* is allowing to use tactics and metaprogramming to discharge assertions not solvable by SMT, or to just simplify them into well-behaved SMT fragments. Plus, Meta-F* can be used to generate verified code automatically.
Meta-F* is implemented as an F* effect, which, given the powerful effect system of F*, heavily increases code reuse and even enables the lightweight verification of metaprograms. Metaprograms can be either interpreted, or compiled to efficient native code that can be dynamically loaded into the F* type-checker and can interoperate with interpreted code. Evaluation on realistic case studies shows that Meta-F* provides substantial gains in proof development, efficiency, and robustness.