Effective Interactive Proofs for Higher-Order Imperative Programs
We present a new approach for constructing and verifying higher-order, imperative programs using the Coq proof assistant. We build on the past work on the Ynot system, which is based on Hoare Type Theory. That original system was a proof of concept, where every program veriﬁcation was accomplished via laborious manual proofs, with much code devoted to uninteresting low-level details. In this paper, we present a re-implementation of Ynot which makes it possible to implement fully-veriﬁed, higher-order imperative programs with reasonable proof burden. At the same time, our new system is implemented entirely in Coq source ﬁles, showcasing the versatility of that proof assistant as a platform for research on language design and veriﬁcation.
Both versions of the system have been evaluated with case studies in the veriﬁcation of imperative data structures, such as hash tables with higher-order iterators. The veriﬁcation burden in our new system is reduced by at least an order of magnitude compared to the old system, by replacing manual proof with automation. The core of the automation is a simpliﬁcation procedure for implications in higher-order separation logic, with hooks that allow programmers to add domain-speciﬁc simpliﬁcation rules.
We argue for the effectiveness of our infrastructure by verifying a number of data structures and a packrat parser, and we compare to similar efforts within other projects. Compared to competing approaches to data structure veriﬁcation, our system includes much less code that must be trusted; namely, about a hundred lines of Coq code deﬁning a program logic. All of our theorems and decision procedures have or build machine-checkable correctness proofs from ﬁrst principles, removing opportunities for tool bugs to create faulty veriﬁcations.
Adam Chlipala has been telling us how underutilized Coq's Ltac tactic programming language for proof automation is for years. Here is the... er... proof.