Eurydice 是 AeneasVerif 生态中的 Rust 到 C 编译器，专为形式验证设计。它允许开发者用 Rust 编写安全、可验证代码，同时为遗留 C 环境生成兼容代码，避免 ABI 破坏。
核心流程从 Rust MIR 开始。rustc 生成 MIR 后，Charon 工具提取整个 crate 的语义数据，包括类型声明、函数体（简化的 MIR）、trait 实现等，输出 JSON 格式。随后，Eurydice 通过类型驱动翻译将这些数据映射到 KaRaMeL 的内部 AST。KaRaMeL 是 F* 到 C/ML 的代码生成器，这里复用其 30+ 个 nano-passes（微型转换），逐步去糖化 Rust 高阶构造为 C 等价物。
MIR 去糖化的关键在于处理 Rust 的借用与所有权模型。MIR 是 Rust 的中级表示，包含借用检查器生成的临时值、借用范围和移动语义。Eurydice 在 KaRaMeL passes 中将这些 desugar 为 C 中的指针操作与条件分支。例如，Rust 的 &mut borrow 转为 C 的非空指针传入，并在函数入口插入活借用检查（liveness check）：验证指针是否有效、非空且未被移动。证据可见项目测试套件，生成的 out/ 目录 C 文件精确匹配 MIR 语义，无 padding 引入的布局偏移。
结构体和联合体的布局保留所有权语义至关重要。Rust struct 默认布局按字段顺序打包，#[repr (C)] 确保 ABI 兼容。Eurydice 生成的 C typedef 严格复制此布局：字段偏移计算基于 Rust 类型大小（考虑 ZST zero-sized types），union 用于 enum 变体表示，嵌入 discriminant 字段追踪当前变体。针对所有权，union 布局避免重叠借用：运行时用 __validity_tag 检查字段是否初始化，避免 use-after-move。例如，对于 Option，union {T value; bool none;} 伴随 tag 位，确保 C 侧访问前验证。
运行时检查实现安全 Rust-C FFI。无这些检查，C 调用者可能违反 Rust 借用规则，导致 UB。Eurydice 插入宏级检查：
- 借用有效性：入口 eurydice_check_borrow (ptr, tag) 验证指针范围内 tag 匹配预期。
- 无别名突变：对 &mut，插入 noalias 属性（GCC/Clang），结合运行时 assert (!alias)。
- 生命周期：借用结束前插入 drop 检查，确保临时不泄露。
参数配置示例（基于 dune-project 和 Makefile）：
-
布局阈值：
参数 值 作用 field_alignment 自然对齐 匹配 Rust repr (Rust) 到 C union_discr_size usize enum 判别符大小 padding_zero_init true ZST padding 初始化为 0 -
检查强度：
- debug: 全 assert，覆盖 100% MIR 边。
- release: 仅关键借用（借用深度 >2），减少 30% 开销。
- 监控：__eurydice_stats () 返回检查失败计数，阈值>0 触发回滚。
落地清单：
- 准备：Nix flake 或 opam setup-charon/karamel/libcrux。
- 编译：charon mycrate.rs → JSON → eurydice --target C → out/my.c。
- 验证：diff 生成 C 与预期，CI 强制无变异。
- FFI 集成：暴露 extern "C" fn，C 侧链接 libeurydice_runtime.a（含检查）。
- 性能调优：nano-passes 顺序自定义，优先 desugar loops 前置 SIMD。
- 回滚：若 MIR 特性不支持（如高级 GAT），fallback 到手写 C。
风险控制：
- 子集限制：暂不支持 async/unsafe，高阶 trait；监控 GitHub issues（如 tuple struct 字段命名）。
- 开销：运行时检查～5-15% CPU，生产用 NDEBUG 剥离。
- ABI 兼容：固定 rustc 版本（1.80+），测试多平台（x86/arm）。
实际案例：Mozilla NSS 的 Kyber PQ 算法，用 Rust 验证后 Eurydice 生成 C，无 ABI 变更即插即用。微软 SymCrypt ML-KEM 预览分支亦采用此路径。
通过 Eurydice，Rust 验证无缝桥接到 C 生态，实现零 ABI 破坏的安全 FFI。未来扩展 MIR 支持，将覆盖更多生产场景。
资料来源：