Transforming Rust into Human-Readable C via Eurydice

Historically, the path from Rust source code to an executable was a narrow one: developers relied almost exclusively on the rustc compiler utilizing an LLVM backend. That was the only way. Today, the ecosystem is far more diverse. Significant strides have been made by various projects to expand how Rust is compiled, including:

• mrustc (Mutabah's Rust Compiler)
• gccrs (GCC's native Rust support)
• rust_codegen_gcc
• Cranelift

Amidst this evolution, a new project called Eurydice has emerged with a distinct and ambitious objective: translating Rust code into clean, readable C.

Why Translate to C?

This capability is particularly vital for high-assurance software development. In these sectors, compliance and verification tools are often legacy systems that only "speak" C. Eurydice serves two primary purposes:

1. It acts as a bridge for projects transitioning to Rust while still requiring C-based verification.
2. It enables Rust code to run in restricted environments that possess a C compiler but lack a full Rust toolchain.

Real-world application: Eurydice has already been utilized to convert post-quantum-cryptography routines from Rust into C.

Project Origins and Governance

Launched in 2023, Eurydice is a hybrid-licensed project (utilizing both MIT and Apache-2.0). It is a component of the broader Aeneas project, which focuses on the intersection of formal verification and the Rust language. The project is primarily steered by researchers from Inria (the French national institute for computer science) and Microsoft, though they welcome contributions from the community.

The Compilation Pipeline

Eurydice operates on a standard compiler architecture, which can be visualized as follows:

While most compilers aim for maximum machine efficiency, Eurydice prioritizes the preservation of the original code's structure. It focuses on stripping away Rust-specific constructs while keeping the logic transparent.

Case Study: GCD and LCM

Consider the following Rust implementation for calculating the Greatest Common Divisor (GCD) and Least Common Multiple (LCM):

fn gcd(a: u64, b: u64) -> u64 {
    if b == 0 { a } else { gcd(b, a % b) }
}

fn lcm(a: u64, b: u64) -> u64 {
    (a * b) / gcd(a, b)
}

Eurydice translates this into the following C code:

uint64_t example_gcd(uint64_t a, uint64_t b) {
    uint64_t uu____0;
    if (b == 0ULL) {
        uu____0 = a;
    } else {
        uu____0 = example_gcd(b, a % b);
    }
    return uu____0;
}

uint64_t example_lcm(uint64_t a, uint64_t b) {
    uint64_t uu____0 = a * b;
    return uu____0 / example_gcd(a, b);
}

Analysis of the Output

The "readability" of this output is subjective, but the technical intent is clear. Eurydice introduces temporary variables (like uu____0) to strictly maintain the evaluation order.

In Rust, if the multiplication in $\text{lcm}(a, b) = \frac{a \times b}{\text{gcd}(a, b)}$ overflows and triggers a panic, that panic must occur before the gcd function is called. Because C does not guarantee this order within a single expression, Eurydice forces the multiplication into its own statement.

Technical Hurdles

Translating a high-level language like Rust to a low-level one like C is not without friction. Eurydice must solve several architectural mismatches:

• Iterators: Rust's iterator-based for loops are converted into C while loops, supported by a specialized runtime library to track iterator state.
• Generics: Since C lacks generics, Eurydice employs monomorphization. This creates unique function implementations for every type used, whereas a native C programmer might have used void * or macros.
• Dynamically Sized Types (DSTs): Handling types with unknown sizes (e.g., ?Sized) is complex.

The DST Dilemma

In Rust, a struct might contain a field of unknown size:

struct DynamicallySized<U: ?Sized> {
    header: usize,
    my_data: U, 
}

If a specific instance uses a known size (e.g., [u8; 4]), Rust can omit bounds checks: $\text{let bar} = \text{foo.my\_data}[2] \implies \text{No bounds check needed}$

To preserve this nuance for formal verification, Eurydice avoids a "one size fits all" approach. If it used a flexible array member everywhere, verification tools would flag "missing" bounds checks. If it added checks everywhere, it would create artificial error paths.

The Solution: Eurydice generates two distinct types: one with a flexible array and one with a fixed-length array. While converting between these is a runtime no-op, it technically violates C's strict-aliasing rules. Consequently, it is recommended to compile the resulting code with the flag: -fno-strict-aliasing.

Lineage and Related Tools

Eurydice is not a standalone invention but is built upon the foundations of the KaRaMeL project. KaRaMeL applies a similar "abstract-to-C" philosophy to F*, a dependently typed functional language frequently used for creating mathematically provable cryptographic libraries.