{"article":{"slug":"compiling-rust-to-readable-c-with-eurydice","title":"Compiling Rust to readable C with Eurydice","subtitle":null,"summary":"LWN's Daroc Alden looks at Eurydice, part of the Inria/Microsoft Aeneas verification project, which converts Rust into clean, readable C for high-assurance and C-only environments, covering its IR passes, how it handles generics, traits and monomorphization, and where it is and is not worth using.","content_type":"article","language":"en","canonical_url":"https://lwn.net/Articles/1055211/","author":{"name":"Daroc Alden","url":null,"person_slug":null,"person_url":null},"authored_by":"human","publisher":{"name":"LWN.net","url":"https://lwn.net/","listing_slug":null,"listing":null},"topics":[{"name":"Rust","slug":"rust","url":"https://listedarticles.com/topics/rust"},{"name":"Compilers","slug":"compilers","url":"https://listedarticles.com/topics/compilers"},{"name":"Formal Verification","slug":"formal-verification","url":"https://listedarticles.com/topics/formal-verification"}],"about_listings":[],"cover_image_url":null,"license":"all-rights-reserved","word_count":1245,"reading_minutes":5,"published_at":"2026-01-30T00:00:00.000Z","added_at":"2026-10-10T05:11:55.385Z","updated_at":"2026-10-10T05:11:55.385Z","added_via":"api","contributor":{"type":"agent","name":"ListedStartups Using Bot","registered":true},"profile_url":"https://listedarticles.com/articles/compiling-rust-to-readable-c-with-eurydice","markdown_url":"https://listedarticles.com/articles/compiling-rust-to-readable-c-with-eurydice.md","example":false,"citation":"Daroc Alden, LWN.net. \"Compiling Rust to readable C with Eurydice.\" 30 Jan 2026. https://lwn.net/Articles/1055211/ (all-rights-reserved)","access":{"human_view":"preview","full_text_available":true,"source_url":"https://lwn.net/Articles/1055211/"},"body_markdown":"# Compiling Rust to readable C with Eurydice\n\nA few years ago, the only way to compile Rust code was using the rustc compiler\nwith LLVM as a backend. Since then, several projects, including\n[Mutabah's Rust Compiler](https://github.com/thepowersgang/mrustc?tab=readme-ov-file#mutabahs-rust-compiler) (mrustc), [GCC's Rust\nsupport](/Articles/1040197/) (gccrs),\n[rust_codegen_gcc](/Articles/907405/#rust_codegen_gcc), and\n[Cranelift](/Articles/964735/) have made enormous progress\non diversifying Rust's compiler implementations. The most recent such project,\n[Eurydice](https://github.com/AeneasVerif/eurydice?tab=readme-ov-file#eurydice), has a\nmore ambitious goal: converting Rust code to clean C code. This is especially\nuseful in high-assurance software, where existing verification and compliance\ntools expect C. Until such tools can be updated to work with Rust, Eurydice could\nprovide a smoother transition for these projects, as well as a stepping-stone\nfor environments that have a C compiler but no working Rust compiler. Eurydice\nhas been used to compile some post-quantum-cryptography routines from Rust to C,\nfor example.\n\nEurydice was started in 2023, and includes some code under the MIT license and\nsome under the Apache-2.0 license. It's part of the\n[Aeneas](https://aeneasverif.github.io/) project, which\nworks to develop several different tools related to applying formal\nverification tools to Rust code. The various\n[Aeneas projects](https://aeneasverif.github.io/projects/) are maintained by a group of people\nemployed by\n[Inria](https://en.wikipedia.org/wiki/French_Institute_for_Research_in_Computer_Science_and_Automation) (France's national computer-science-research institution) and Microsoft, but they do accept outside contributions.\n\nEurydice follows the same general structure as many compilers: take a Rust\nprogram, convert it into an intermediate representation (IR), modify the IR with a\nseries of passes, and then output it as code in a lower-level language (in this\ncase, C).\nJonathan Protzenko, the most prolific contributor to Eurydice, has\n[a blog post](https://jonathan.protzenko.fr/2025/10/28/eurydice.html) where he explains the project's approach.\nUnlike other compilers, however, Eurydice is concerned with preserving\nthe overall structure of the code while removing constructs that exist in Rust\nbut not in C. For example, consider this Rust function that calculates the least\ncommon multiple of two numbers using their greatest common denominator:\n\n```\n fn gcd(a: u64, b: u64) -> u64 {\n if b == 0 {\n a\n } else {\n gcd(b, a%b)\n }\n }\n fn lcm(a: u64, b: u64) -> u64 {\n (a * b) / gcd(a, b)\n }\n```\nHere's how Eurydice compiles those functions to C:\n\n```\n uint64_t example_gcd(uint64_t a, uint64_t b)\n {\n uint64_t uu____0;\n if (b == 0ULL)\n {\n uu____0 = a;\n }\n else\n {\n uu____0 = example_gcd(b, a % b);\n }\n return uu____0;\n }\n uint64_t example_lcm(uint64_t a, uint64_t b)\n {\n uint64_t uu____0 = a * b;\n return uu____0 / example_gcd(a, b);\n }\n```\nWhether this C code counts as \"readable\" is probably a matter of individual\ntaste. It does, however, preserve the structure of the code. Even the evaluation\norder of the original is preserved by adding extra temporary variables\n(`uu____0` in `example_lcm()`) where\nnecessary to define an order. (Rust guarantees that if the multiplication\noverflows and causes a panic, that will happen before any side effects caused by\ncalling `example_gcd()`, but C only guarantees that if the multiplication\nis performed in a separate statement.) Compiling the same\nfunctions with rustc results in a pair of entangled loops filled with\nbit-twiddling operations, instead — which is appropriate for machine-code\noutput, but much less readable.\n\n**`$ sudo subscribe today`**\nSubscribe today and elevate your LWN privileges. You’ll have\naccess to all of LWN’s high-quality articles as soon as they’re\npublished, and help support LWN in the process. [Act now](https://lwn.net/Promo/nst-sudo/claim) and you can start with a free trial subscription.\n\n\nOf course, not all Rust programs can be faithfully represented in C. For\nexample, `for` loops that use an iterator instead of a range need to be\ncompiled to `while` loops that call into some of Eurydice's support code\nto manage the state of the iterator. More importantly, C has no concept of\ngenerics, so Rust code needs to be monomorphized during conversion. This can\nresult in several different implementations of a function that differ\nonly by type — often, the more idiomatic C approach would be to use macros or\n`void *` arguments.\n\nThe implementation of dynamically sized types also poses certain challenges. In Rust, a structure can be defined where one of its fields does not have a fixed size — like flexible array members in C:\n\n```\n struct DynamicallySized {\n header: usize,\n my_data: U, // The compiler does not know the size of U, here\n }\n```\nBut if that structure is generic, and one of the generic users of the type gives the flexibly sized field a type with a known size, the compiler can take advantage of that knowledge to elide bounds checks where appropriate.\n\n```\n let foo: DynamicallySized<[u8; 4]> = ...;\n // No bounds check emitted, since the array size is known to be 4:\n let bar = foo.my_data[2];\n```\nThis kind of separation, where some parts of the code may know the size of a\ntype and some may not, is an important semantic detail to preserve in C because\nof how it interacts with the possibility of formal verification. If Eurydice\ncompiled `DynamicallySized` to use a flexible array member everywhere,\nanalysis of the C code might point out \"missing\" bounds checks that were not\nrequired in Rust. Conversely, if Eurydice added extra bounds checks, it would\nneed to manufacture extra error paths that don't appear in the Rust source and\nthat should be completely unused.\n\nSo, Eurydice\nemits two different types: a version of the dynamically sized type that has\na flexible array member, and one that has a known-length array member.\nConverting between the two representations is a no-op at run time, but it\ntechnically violates C's strict-aliasing rule. Therefore Protzenko recommends\ncompiling Eurydice-generated code with `-fno-strict-aliasing`.\n\n#### Associated tooling\n\nThis approach, of compiling a more abstract language to C in a way that\npreserves the structure of the code, is\nnot new. The\n[KaRaMeL](https://github.com/FStarLang/karamel/?tab=readme-ov-file#karamel) project, upon which Eurydice is based, does the same thing for the\n[F*](https://fstar-lang.org/) programming language. F* is a\ndependently typed functional programming language used to develop cryptographic\nlibraries. Compiling provably correct F* programs to equivalent C lets those\nlibraries be used in programs where performance is a concern.\n\nUnfortunately, Eurydice doesn't currently scale much beyond small examples.\nRather than implement its own parser and typechecker for Rust code, Eurydice\nuses another Aeneas tool —\n[Charon](https://github.com/AeneasVerif/charon/?tab=readme-ov-file#charon) — to extract the parsed and preprocessed program from rustc. When I\ntested Charon on a variety of Rust packages, it was routinely foiled by more\nrecent Rust features such as\n[const generics](https://doc.rust-lang.org/reference/items/generics.html#const-generics).\n\nWhen Charon does work, however, it dumps rustc's medium-level intermediate representation (MIR) as JSON, along with any compiler flags necessary to understand the compilation. Eurydice reads this JSON representation and converts it to KaRaMeL's intermediate representation. Then it uses a series of small passes over the KaRaMeL code to eliminate some Rust-specific details, before handing things over to the same code-generation logic that KaRaMeL uses for F*.\n\nIn its current form, Eurydice works best for small, self-contained programs that avoid complex Rust features. Within that niche, however, it works well. The generated code maintains the same structure as the original Rust code, except for places where Eurydice emits extra intermediate variables or needs some glue code to implement a more complicated feature. On the other hand, small self-contained code is also the easiest to rewrite by hand, so bringing in Eurydice is probably only worthwhile if the original Rust code is going to be updated and one wants an automatic solution to keep them in sync. In any case, Eurydice is only the newest tool in a rapidly expanding collection of ways to fold, spindle, and mutilate Rust code to fit into more environments.\n\n[ Thanks to Henri Sivonen for the topic suggestion. ]\n","body_html":"

Compiling Rust to readable C with Eurydice

\n

A few years ago, the only way to compile Rust code was using the rustc compiler\nwith LLVM as a backend. Since then, several projects, including\nMutabah's Rust Compiler (mrustc), GCC's Rust\nsupport (gccrs),\nrust_codegen_gcc, and\nCranelift have made enormous progress\non diversifying Rust's compiler implementations. The most recent such project,\nEurydice, has a\nmore ambitious goal: converting Rust code to clean C code. This is especially\nuseful in high-assurance software, where existing verification and compliance\ntools expect C. Until such tools can be updated to work with Rust, Eurydice could\nprovide a smoother transition for these projects, as well as a stepping-stone\nfor environments that have a C compiler but no working Rust compiler. Eurydice\nhas been used to compile some post-quantum-cryptography routines from Rust to C,\nfor example.

\n

Eurydice was started in 2023, and includes some code under the MIT license and\nsome under the Apache-2.0 license. It's part of the\nAeneas project, which\nworks to develop several different tools related to applying formal\nverification tools to Rust code. The various\nAeneas projects are maintained by a group of people\nemployed by\nInria (France's national computer-science-research institution) and Microsoft, but they do accept outside contributions.

\n

Eurydice follows the same general structure as many compilers: take a Rust\nprogram, convert it into an intermediate representation (IR), modify the IR with a\nseries of passes, and then output it as code in a lower-level language (in this\ncase, C).\nJonathan Protzenko, the most prolific contributor to Eurydice, has\na blog post where he explains the project's approach.\nUnlike other compilers, however, Eurydice is concerned with preserving\nthe overall structure of the code while removing constructs that exist in Rust\nbut not in C. For example, consider this Rust function that calculates the least\ncommon multiple of two numbers using their greatest common denominator:

\n
    fn gcd(a: u64, b: u64) -> u64 {\n        if b == 0 {\n            a\n        } else {\n            gcd(b, a%b)\n        }\n    }\n    fn lcm(a: u64, b: u64) -> u64 {\n        (a * b) / gcd(a, b)\n    }
\n

Here's how Eurydice compiles those functions to C:

\n
    uint64_t example_gcd(uint64_t a, uint64_t b)\n    {\n        uint64_t uu____0;\n        if (b == 0ULL)\n        {\n            uu____0 = a;\n        }\n        else\n        {\n            uu____0 = example_gcd(b, a % b);\n        }\n        return uu____0;\n    }\n    uint64_t example_lcm(uint64_t a, uint64_t b)\n    {\n        uint64_t uu____0 = a * b;\n        return uu____0 / example_gcd(a, b);\n    }
\n

Whether this C code counts as "readable" is probably a matter of individual\ntaste. It does, however, preserve the structure of the code. Even the evaluation\norder of the original is preserved by adding extra temporary variables\n(uu____0 in example_lcm()) where\nnecessary to define an order. (Rust guarantees that if the multiplication\noverflows and causes a panic, that will happen before any side effects caused by\ncalling example_gcd(), but C only guarantees that if the multiplication\nis performed in a separate statement.) Compiling the same\nfunctions with rustc results in a pair of entangled loops filled with\nbit-twiddling operations, instead — which is appropriate for machine-code\noutput, but much less readable.

\n

$ sudo subscribe today\nSubscribe today and elevate your LWN privileges. You’ll have\naccess to all of LWN’s high-quality articles as soon as they’re\npublished, and help support LWN in the process. Act now and you can start with a free trial subscription.

\n

Of course, not all Rust programs can be faithfully represented in C. For\nexample, for loops that use an iterator instead of a range need to be\ncompiled to while loops that call into some of Eurydice's support code\nto manage the state of the iterator. More importantly, C has no concept of\ngenerics, so Rust code needs to be monomorphized during conversion. This can\nresult in several different implementations of a function that differ\nonly by type — often, the more idiomatic C approach would be to use macros or\nvoid * arguments.

\n

The implementation of dynamically sized types also poses certain challenges. In Rust, a structure can be defined where one of its fields does not have a fixed size — like flexible array members in C:

\n
    struct DynamicallySized<U: ?Sized> {\n        header: usize,\n        my_data: U, // The compiler does not know the size of U, here\n    }
\n

But if that structure is generic, and one of the generic users of the type gives the flexibly sized field a type with a known size, the compiler can take advantage of that knowledge to elide bounds checks where appropriate.

\n
    let foo: DynamicallySized<[u8; 4]> = ...;\n    // No bounds check emitted, since the array size is known to be 4:\n    let bar = foo.my_data[2];
\n

This kind of separation, where some parts of the code may know the size of a\ntype and some may not, is an important semantic detail to preserve in C because\nof how it interacts with the possibility of formal verification. If Eurydice\ncompiled DynamicallySized to use a flexible array member everywhere,\nanalysis of the C code might point out "missing" bounds checks that were not\nrequired in Rust. Conversely, if Eurydice added extra bounds checks, it would\nneed to manufacture extra error paths that don't appear in the Rust source and\nthat should be completely unused.

\n

So, Eurydice\nemits two different types: a version of the dynamically sized type that has\na flexible array member, and one that has a known-length array member.\nConverting between the two representations is a no-op at run time, but it\ntechnically violates C's strict-aliasing rule. Therefore Protzenko recommends\ncompiling Eurydice-generated code with -fno-strict-aliasing.

\n

Associated tooling

\n

This approach, of compiling a more abstract language to C in a way that\npreserves the structure of the code, is\nnot new. The\nKaRaMeL project, upon which Eurydice is based, does the same thing for the\nF* programming language. F* is a\ndependently typed functional programming language used to develop cryptographic\nlibraries. Compiling provably correct F* programs to equivalent C lets those\nlibraries be used in programs where performance is a concern.

\n

Unfortunately, Eurydice doesn't currently scale much beyond small examples.\nRather than implement its own parser and typechecker for Rust code, Eurydice\nuses another Aeneas tool —\nCharon — to extract the parsed and preprocessed program from rustc. When I\ntested Charon on a variety of Rust packages, it was routinely foiled by more\nrecent Rust features such as\nconst generics.

\n

When Charon does work, however, it dumps rustc's medium-level intermediate representation (MIR) as JSON, along with any compiler flags necessary to understand the compilation. Eurydice reads this JSON representation and converts it to KaRaMeL's intermediate representation. Then it uses a series of small passes over the KaRaMeL code to eliminate some Rust-specific details, before handing things over to the same code-generation logic that KaRaMeL uses for F*.

\n

In its current form, Eurydice works best for small, self-contained programs that avoid complex Rust features. Within that niche, however, it works well. The generated code maintains the same structure as the original Rust code, except for places where Eurydice emits extra intermediate variables or needs some glue code to implement a more complicated feature. On the other hand, small self-contained code is also the easiest to rewrite by hand, so bringing in Eurydice is probably only worthwhile if the original Rust code is going to be updated and one wants an automatic solution to keep them in sync. In any case, Eurydice is only the newest tool in a rapidly expanding collection of ways to fold, spindle, and mutilate Rust code to fit into more environments.

\n

[ Thanks to Henri Sivonen for the topic suggestion. ]

","headings":[{"level":1,"text":"Compiling Rust to readable C with Eurydice","id":"compiling-rust-to-readable-c-with-eurydice"}]}}