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


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


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.