Meta-F⭑

Proof Automation with SMT, Tactics, and Metaprograms

Guido Martínez^1,2    Danel Ahman³    Victor Dumitrescu⁴    Nick Giannarakis⁵
Chris Hawblitzel⁶    Cătălin Hriţcu²    Monal Narasimhamurthy⁷
Zoe Paraskevopoulou⁵    Clément Pit-Claudel⁸    Jonathan Protzenko⁶
Tahina Ramananandro⁶    Aseem Rastogi⁶    Nikhil Swamy⁶

¹CIFASIS-CONICET    ²Inria Paris    ³University of Ljubljana
⁴MSR-Inria Joint Centre    ⁵Princeton University    ⁶Microsoft Research
⁷University of Colorado Boulder    ⁸MIT-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.