Eurydice 是一个从 Rust 到 C 的转译器，专为验证生态和遗留系统设计。它允许开发者使用 Rust 的安全特性和易验证性编写代码，同时生成独立 C 代码嵌入 C/C++ 项目，而无需 Rust 运行时或 std 库依赖。这解决了 Rust 采用中的关键痛点：某些嵌入式目标、旧工具链或分析工具不支持 Rust。
转译流程核心在于 MIR 级别介入，避免语法糖复杂性。Eurydice 通过 Charon 提取 Rust MIR，然后类型驱动翻译至 KaRaMeL 内部 AST。随后，30+ 纳米级优化逐步降级至 C：处理单态化（monomorphization）、模式匹配转标签联合、迭代器优化为 for 循环、数组初始化用 memset 等。
例如，Rust 中的 [u32; 8] 转译为 C struct { uint32_t data [8]; }，确保值语义。枚举使用标签联合，支持 DST 经柔性数组成员。整程序单态化导致 C 代码冗长，但通过配置控制函数实例放置，避免单一巨文件。
工程落地参数如下：
-
环境搭建：优先 Nix flake，确保工具版本一致。否则 opam init OCaml，cargo Rust，make setup-karamel/setup-charon/setup-libcrux。
-
配置 YAML：libcrux 示例中，按 SIMD 类型（如 __m256i AVX2）分文件：c.yaml 指定 monomorphized 函数路径与编译标志（如 -mavx2）。阈值：数组大小 >32 用 memset，<4 直接赋值。
-
编译命令：make test 验证输出（out/ 下 C 文件版控）。PR 前 make -B test/format-apply。生成标志：C11/C++20 用指定初始化，C++17 用成员指针。
-
嵌入清单：
- 头文件：include/eurydice_glue.h 提供宏如 Eurydice_array_eq (a1, a2, len, t) 展开 memcmp。
- 编译旗：-fno-strict-aliasing（DST 指针转换违例），-std=c11 或 C++20。
- 验证：diff Rust MIR 与 C 输出，静态分析 C 匹配 Rust 行为。
- 回滚：cfg 条件代码多平台需预处理展开所有变体。
监控要点：
- 代码体积：单态化后监控文件大小，配置拆分 >10k 行。
- 性能：基准 Rust vs C，优化 peephole 如 array::from_fn 原地初始化。
- 兼容：不支持 dyn trait（vtable 开发中），整数溢出不 panic（假设验证无 panic）。
- 布局差异：无 ABI 保证，需手动对齐或测试互操作。
实际案例：Kyber PQ 算法 Rust 验证后，经 Eurydice 转 C 集成 NSS。Symcrust 测试对比显示模式匹配高效转译。
风险：仅 Rust 子集（无高级 trait/GATs），C 代码需手动胶水宏。未来目标：std 库全提取、Charon 单态化。
来源：https://github.com/AeneasVerif/eurydice；https://jonathan.protzenko.fr/2025/10/28/eurydice.html。