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

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

Guido Martínez1,2    Danel Ahman3    Victor Dumitrescu4    Nick Giannarakis5   
Chris Hawblitzel6    Cătălin Hriţcu2    Monal Narasimhamurthy7   
Zoe Paraskevopoulou5    Clément Pit-Claudel8    Jonathan Protzenko6   
Tahina Ramananandro6    Aseem Rastogi6    Nikhil Swamy6

1CIFASIS-CONICET    2Inria Paris    3University of Ljubljana   
4MSR-Inria Joint Centre    5Princeton University    6Microsoft Research   
7University of Colorado Boulder    8MIT-CSAIL

28th European Symposium on Programming, ESOP 2019

Abstract

We introduce Meta-F*, a tactics and metaprogramming framework for the F* program verifier. The main novelty of Meta-F* is allowing the use of 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.