Skip to content

Eurydice compiles (a modest subset of) Rust to C. Verify programs in Rust, still get C code for legacy environments.

License

Apache-2.0, MIT licenses found

Licenses found

Apache-2.0
LICENSE-APACHE
MIT
LICENSE-MIT
Notifications You must be signed in to change notification settings

AeneasVerif/eurydice

Repository files navigation

Orphée et Eurydice Nicolas Poussin, Orphée et Eurydice. Musée du Louvre. Source

Eurydice

Eurydice is a compiler from Rust to C. The purpose of Eurydice is to provide a backwards-compatibility story as the verification ecosystem gradually transitions to Rust. New programs can be written in Rust, in turn making them safer and easier to verify; but for legacy environments that cannot yet take a dependency on the Rust toolchain, Eurydice allows generating C code as a stopgap measure.

Currently (late 2023), the flagship example for Eurydice is Kyber, a Post-Quantum cryptographic algorithm authored and verified in Rust for the general public, and compiled to C via Eurydice for Mozilla's NSS library.

In terms of software architecture, Eurydice consumes Rust programs via the Charon infrastructure, then extracts Rust to KaRaMeL's internal AST via a type-driven translation. Once in the KaRaMeL AST, 30+ nano-passes allow going from Rust down to C code. About half of these passes were already implemented for KaRaMeL, the rest of the passes reuse the KaRaMeL infrastructure but were freshly written for Eurydice.

If you want to contribute or ask questions, we strongly encourage you to join the Zulip.

About

Eurydice compiles (a modest subset of) Rust to C. Verify programs in Rust, still get C code for legacy environments.

Resources

License

Apache-2.0, MIT licenses found

Licenses found

Apache-2.0
LICENSE-APACHE
MIT
LICENSE-MIT

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published