Refactoring and Equivalence in Rust: Expanding the REM Toolchain with a Novel Approach to Automated Equivalence Proofs

TL;DR

This work presents REM2.0, a Rust extract-method toolchain built on rust-analyzer that delivers fast, semantics-aware refactorings and optional machine-checked verification. The system combines an RA-backed extraction engine, a lifetime/ownership repairer, and a verification pipeline that translates code to LLBC via CHARON and to Coq via AENEAS to prove behavioural equivalence. It extends REM to cover modern Rust features (async/await, generics, const fn, and non-local control flow) and integrates with a VSCode front-end through a persistent daemon, achieving latency in the low milliseconds for extraction and sub-second, end-to-end verification for the supported subset. The results demonstrate substantial performance gains over the original REM and illustrate the practicality of combining fast, RA-based refactoring with optional formal verification in real development workflows.

Abstract

Refactoring tools are central to modern development, with extract-function refactorings used heavily in day-to-day work. For Rust, however, ownership, borrowing, and advanced type features make automated extract-function refactoring challenging. Existing tools either rely on slow compiler-based analysis, support only restricted language fragments, or provide little assurance beyond "it still compiles." This paper presents REM2.0, a new extract-function and verification toolchain for Rust. REM2.0 works atop rust-analyzer as a persistent daemon, providing low-latency refactorings with a VSCode front-end. It adds a repairer that automatically adjusts lifetimes and signatures when extraction exposes borrow-checker issues, and an optional verification pipeline connecting to CHARON and AENEAS to generate Coq equivalence proofs for a supported Rust subset. The architecture is evaluated on three benchmark suites. On the original REM artefact, REM2.0 achieves 100% compatibility while reducing latency from ~1000ms to single-digit milliseconds in the daemon. On 40 feature-focused extractions from 20 highly starred GitHub repositories, REM2.0 handles most examples involving async/await, const fn, non-local control flow, generics, and higher-ranked trait bounds. On twenty verification benchmarks, the CHARON/AENEAS pipeline constructs end-to-end equivalence proofs for cases within its current subset. Overall, results show that a rust-analyzer-based design can provide fast, feature-rich extract-function refactoring for real Rust programs, while opt-in verification delivers machine-checked behaviour preservation.

Figures (19)

• Figure 1: Borrowing in Rust
• Figure 2: Overview of the REM extract-method pipeline (after Costea et al. AdventureOfALifetime)
• Figure 3: High-level overview of the expanded REM architecture: VS Code communicates bidirectionally with the REM Server, which dispatches to the Extraction Engine, the REM Repairer, and the REM Verification pipeline.
• Figure 4: Comparison of an extraction prior to the std and core fixes and after. Before we return a '_' as a placeholder, as Rust-Analyzer is unable to infer the type without the semantic information provided by std.
• Figure 5: Options presented to the user when they have selected a region to extract.