Eurydice Project Compiles Rust to Readable C Code for High-Assurance Software

New Rust-to-C Compiler

Eurydice is a new project that compiles Rust code into readable C code. This expands the compilation options for Rust, which traditionally relied on the rustc compiler with LLVM. Other projects like mrustc, gccrs, rust_codegen_gcc, and Cranelift have also diversified Rust's compiler implementations.

Addressing High-Assurance Needs

The primary goal of Eurydice is to facilitate the use of Rust in high-assurance software. These environments often depend on existing verification and compliance tools designed for C. By generating C code, Eurydice offers a transitional path for projects to adopt Rust without immediately updating their C-centric toolchains. It also enables Rust deployment in environments that have a C compiler but no functional Rust compiler. For example, Eurydice has been used to compile post-quantum cryptography routines from Rust to C.

Project Origins and Structure

Eurydice began in 2023 and is part of the broader Aeneas project, which focuses on applying formal verification tools to Rust code. The project includes code under both the MIT and Apache-2.0 licenses. It is maintained by personnel from Inria (France's national computer-science research institution) and Microsoft, and accepts external contributions.

Eurydice operates like a standard compiler, converting Rust into an intermediate representation, applying passes, and then outputting C code. A key distinction is its focus on preserving the overall structure of the original Rust code while translating Rust-specific constructs into C equivalents.

Example of Code Conversion

The project demonstrates its approach by converting Rust functions for calculating the greatest common divisor (gcd) and least common multiple (lcm) into C. The resulting C code maintains a similar logical flow and variable naming, illustrating the 'readable' aspect of its output. For instance, a Rust `gcd` function with recursion is translated into a C `example_gcd` function with equivalent recursive calls and `uint64_t` types.