Proving Functional Program Equivalence via Directed Lemma Synthesis

TL;DR

This paper introduces directed lemma synthesis, a systematic method for automating program equivalence proofs by automatically generating critical lemmas, significantly improving efficiency over heuristic approaches.

Contribution

The paper presents a novel approach to automate lemma discovery for program equivalence proofs using directed synthesis techniques, enhancing proof automation and efficiency.

Findings

Reduces proof runtime by 95.47% on average

Solves 38 more tasks than heuristic methods

Transforms lemma synthesis into efficient program synthesis problems

Abstract

Proving equivalence between functional programs is a fundamental problem in program verification, which often amounts to reasoning about algebraic data types (ADTs) and compositions of structural recursions. Modern theorem provers address this problem by applying structural induction, which is insufficient for proving many equivalence theorems. In such cases, one has to invent a set of lemmas, prove these lemmas by additional induction, and use these lemmas to prove the original theorem. There is, however, a lack of systematic understanding of what lemmas are needed for inductive proofs and how these lemmas can be synthesized automatically. This paper presents directed lemma synthesis, an effective approach to automating equivalence proofs by discovering critical lemmas using program synthesis techniques. We first identify two induction-friendly forms of propositions that give formal guarantees to the progress of the proof. We then propose two tactics that synthesize and apply lemmas, thereby transforming the proof goal into induction-friendly forms. Both tactics reduce lemma synthesis to a specialized class of program synthesis problems with efficient algorithms. Experimental results demonstrate the effectiveness of our approach: Compared to state-of-the-art equivalence checkers employing heuristic-based lemma enumeration, directed lemma synthesis saves 95.47% runtime on average and solves 38 more tasks over an extended version of the standard benchmark set.