The Eurydice project, initiated in 2023, aims to convert Rust code into clean C code, addressing the needs of high-assurance software that relies on existing verification tools designed for C. This project is part of the Aeneas initiative, which focuses on developing tools for applying formal verification to Rust code. Eurydice operates by taking a Rust program, converting it into an intermediate representation (IR), modifying the IR, and then outputting it as C code. Jonathan Protzenko, a key contributor, emphasizes that Eurydice seeks to maintain the structure of the original Rust code while adapting it for C compatibility.
Eurydice has been successfully used to compile post-quantum cryptography routines from Rust to C. However, it faces challenges, such as the inability to represent all Rust constructs in C, particularly with iterator-based for loops and the absence of generics in C. The project also addresses dynamically sized types, ensuring that the conversion preserves important semantic details necessary for formal verification.
The tool utilizes Charon, another Aeneas project, to extract parsed Rust code from the rustc compiler. While Eurydice currently works best for small, self-contained Rust programs, it effectively maintains the original structure of the code, making it a useful tool for developers looking to transition Rust codebases to C environments. Despite its limitations, Eurydice represents a significant step in diversifying Rust's compiler implementations.