Computer Science > Programming Languages
[Submitted on 17 Mar 2018 (v1), revised 12 Jul 2018 (this version, v2), latest version 7 Mar 2019 (v4)]
Title:Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
View PDFAbstract:Scripting proofs with tactics has been a tradition in interactive theorem proving for decades. For nearly as long, semi-automated program verifiers have used tools like SMT solvers to improve proof automation. Despite their strengths, for verification in the large, both approaches also have shortcomings: (1) building application-specific tactics requires great effort and automated provers are not easily exploitable; (2) SMT solvers only efficiently automate a limited class of logics and theories. On the theories that are not efficiently SMT-automatable users must provide ad-hoc hints, resulting in brittleness and a waste of human effort.
Meta-F* is a new metaprogramming framework for F* which permits to profit from the state-of-the-art automation in SMT solvers, while using tactics to stay clear of their weaknesses, increasing overall proof robustness. Dually, this new style of proof reduces the effort of the tactic writer, as tactics need to automate only those parts of a proof that are difficult for an SMT solver. Beyond tactics, Meta-F* programs can construct and reflect on the syntax of F* programs, while safely manipulating the internal state of its typechecker. This allows scripting the construction of effectful programs along with their proofs of correctness, significantly reducing the need for user interaction in some proofs.
Meta-F* is not a new language: it is embedded into F* simply as a new, custom effect, which readily enables safe interactions between programs and metaprograms on equal footing. In support of executing them efficiently, we design and implement a new mechanism for extending the F* compiler with binary plugins compiled from verified source (meta)programs. Our experimental evaluation shows that with metaprogram plugins, performance and stability of hybrid SMT/metaprogramming proofs exceeds that of SMT-only proofs.
Submission history
From: Catalin Hritcu [view email][v1] Sat, 17 Mar 2018 18:08:13 UTC (110 KB)
[v2] Thu, 12 Jul 2018 15:04:19 UTC (151 KB)
[v3] Sat, 17 Nov 2018 20:50:50 UTC (142 KB)
[v4] Thu, 7 Mar 2019 13:25:38 UTC (142 KB)
Bibliographic and Citation Tools
Bibliographic Explorer (What is the Explorer?)
Litmaps (What is Litmaps?)
scite Smart Citations (What are Smart Citations?)
Code, Data and Media Associated with this Article
CatalyzeX Code Finder for Papers (What is CatalyzeX?)
DagsHub (What is DagsHub?)
Gotit.pub (What is GotitPub?)
Papers with Code (What is Papers with Code?)
ScienceCast (What is ScienceCast?)
Demos
Recommenders and Search Tools
Influence Flower (What are Influence Flowers?)
Connected Papers (What is Connected Papers?)
CORE Recommender (What is CORE?)
arXivLabs: experimental projects with community collaborators
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.