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)
- Final version (on the publisher's website)
- Paper preprint
- Submission versions on arXiV
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.