Eurydice es un compilador desarrollado dentro del proyecto Aeneas que traduce el código fuente de Rust a código C destinado a ser legible por humanos y adecuado para entornos donde las herramientas de verificación esperan C pero no hay una cadena de herramientas de Rust disponible. Originado de una colaboración entre Inria y Microsoft, el proyecto tiene como objetivo proporcionar una medida provisional mientras el ecosistema de verificación adopta gradualmente Rust, permitiendo que los nuevos programas Rust se usen en entornos heredados que aún dependen del análisis basado en C.
El compilador funciona empleando primero la herramienta Charon para extraer la representación intermedia de nivel medio (MIR) de Rust como JSON desde rustc, luego convirtiendo ese MIR al árbol sintáctico abstracto interno de KaRaMeL. Más de treinta pases nano operan sobre este AST para eliminar construcciones específicas de Rust que no tienen equivalentes directos en C, preservando el orden de evaluación y la estructura original del programa; por ejemplo, una función recursiva simple de GCD se compila a C con variables temporales adicionales (como uu____0) para hacer cumplir la misma secuencia de operaciones que en el origen de Rust. Para evitar optimizaciones no deseadas que romperían este orden, el código C generado debe compilarse con la bandera -fno-strict-aliasing.
La imagen muestra la página de GitHub del proyecto Eurydice, que describe cómo el compilador convierte Rust a C, coincidiendo con la explicación del artículo sobre el propósito de la herramienta.
Eurydice actualmente maneja solo un subconjunto de las características de Rust; funciona mejor con programas pequeños y autocontenidos, y puede fallar con características más nuevas del lenguaje como los genéricos const, que provocan que Charon falle al extraer el MIR. Además, debido a que el modelo de propiedad y préstamo de Rust no se asigna limpiamente al modelo de memoria de C, la traducción suele producir código que técnicamente viola las reglas de aliasing estricto de C, lo que exige la bandera del compilador mencionada anteriormente y, a veces, resulta en una salida de C menos idiomática, aunque el proyecto sostiene que el significado semántico del código Rust original se preserva para fines de verificación.