REST: Integrating Term Rewriting with Program Verification (Extended Version)

TL;DR

REST is a new term rewriting technique for theorem proving that dynamically selects orderings and integrates external oracles to improve flexibility and termination, and it can be incorporated into existing program verifiers.

Contribution

It introduces REST, a flexible, dynamically adaptive term rewriting method with external oracle integration, designed for seamless integration into existing verification tools.

Findings

REST outperforms existing rewriting techniques in proofs.

REST can replace manual lemma application in Liquid Haskell.

The implementation demonstrates practical integration and effectiveness.

Abstract

We introduce REST, a novel term rewriting technique for theorem proving that uses online termination checking and can be integrated with existing program verifiers. REST enables flexible but terminating term rewriting for theorem proving by: (1) exploiting newly-introduced term orderings that are more permissive than standard rewrite simplification orderings; (2) dynamically and iteratively selecting orderings based on the path of rewrites taken so far; and (3) integrating external oracles that allow steps that cannot be justified with rewrite rules. Our REST approach is designed around an easily implementable core algorithm, parameterizable by choices of term orderings and their implementations; in this way our approach can be easily integrated into existing tools. We implemented REST as a Haskell library and incorporated it into Liquid Haskell's evaluation strategy, extending Liquid Haskell with rewriting rules. We evaluated our REST implementation by comparing it against both existing rewriting techniques and E-matching and by showing that it can be used to supplant manual lemma application in many existing Liquid Haskell proofs.