Reducing Partial Equivalence to Partial Correctness

Two programs P and Q are partially equivalent if, when both terminate on the same input, they end up with equivalent outputs. Establishing partial equivalence is useful in, e.g., Compiler verification, when P is the source program and Q is the target program, or in compiler optimisation, when P is the initial program and Q is the optimised program. A program R is partially correct if, when it terminates, it ends up in a "good" state. We show that, somewhat surprisingly, the problem of establishing partial equivalence can be reduced to the problem of showing partial correctness in an aggregated language, where programs R consist of pairs of programs 〈P, Q〉. Our method is crucially based on the recently-introduced matching logic, which allows to faithfully define the operational semantics of any language. We show that we can construct the aggregated language mechanically, from the semantics of the initial languages. Furthermore, matching logic gives us for free a proof system for partial correctness for the resulting language. This proof system can then be used to prove partial equivalence.