Operationally-based Program Equivalence Proofs using LCTRSs

We propose an operationally-based deductive proof method for program equivalence. It is based on encoding the language semantics as logically constrained term rewriting systems (LCTRSs) and the two programs as terms. The main feature of our method is its flexibility. We illustrate this flexibility in two applications, which are novel. For the first application, we show how to encode low-level details such as stack size in the language semantics and how to prove equivalence between two programs operating at different levels of abstraction. For our running example, we show how our method can prove equivalence between a recursive function operating with an unbounded stack and its tail-recursive optimized version operating with a bounded stack. This type of equivalence checking can be used to ensure that new, undesirable behavior is not introduced by a more concrete level of abstraction. For the second application, we show how to formalize read-sets and write-sets of symbolic expressions and statements by extending the operational semantics in a conservative way. This enables the relational verification of program schemas, which we exploit to prove correctness of compiler optimizations, some of which cannot be proven by existing tools. Our method requires an extension of standard LCTRSs with axiomatized symbols. We also present a prototype implementation that proves the feasibility of both applications that we propose.