KestRel: Relational Verification Using E-Graphs for Program Alignment

TL;DR

The paper tackles the challenge of verifying relational properties by constructing an aligned intermediate program for two target programs. It introduces KestRel, which embeds program pairs into a relational calculus, saturates an e-graph with algebraic realignment rules, and uses data-driven extraction based on execution traces to select a semantically well-aligned intermediate program that can be handed to standard non-relational verifiers. Core theoretical foundations are provided by the CoreRel calculus and its embedding/reification framework, while the implementation (in Rust using Egg) demonstrates practical verification on benchmarks with backends such as Dafny and SeaHorn. Empirical results show that KestRel discovers alignments enabling verification where naive concatenation fails, and ablation studies illustrate the value of combining syntactic and semantic extraction, albeit with limitations related to data-dependent alignments and back-end invariants. The work advances relational verification by marrying algebraic realignment with trace-informed search, offering a verifier-agnostic approach that scales to a broad set of relational properties and program features.

Abstract

Many interesting program properties involve the execution of multiple programs, including observational equivalence, noninterference, co-termination, monotonicity, and idempotency. One strategy for verifying such relational properties is to construct and reason about an intermediate program whose correctness implies that the individual programs exhibit those properties. A key challenge in building an intermediate program is finding a good alignment of the original programs. An alignment puts subparts of the original programs into correspondence so that their similarities can be exploited in order to simplify verification. We propose an approach to intermediate program construction that uses e-graphs, equality saturation, and algebraic realignment rules to efficiently represent and build programs amenable to automated verification. A key ingredient of our solution is a novel data-driven extraction technique that uses execution traces of candidate intermediate programs to identify solutions that are semantically well-aligned. We have implemented a relational verification engine based on our proposed approach, called KestRel, and use it to evaluate our approach over a suite of benchmarks taken from the relational verification literature.

Figures (21)

• Figure 1: Two programs for calculating employee bonuses.
• Figure 2: A program that combines $_1$ and $_2$ from \ref{['fig:example']}
• Figure 3: A good alignment matches every iteration of the loop in with two iterations of the loop in .
• Figure 4: The function optimizes by collapsing its inner loop into a single addition operation.
• Figure 5: High-level overview of KestRel.

Theorems & Definitions (6)

• definition 1: E-Graph
• definition 2: Relational Safety
• theorem 1: Embedding is Sound
• definition 3: Alignment Equivalence
• theorem 2: Reification preserves Equivalence
• corollary 1