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.