在 Rust 验证生态中，Eurydice 作为 Rust 到 C 编译器，提供了一种独特的 MIR 降阶策略，直接生成可读 C 代码。该策略的核心是通过 C 结构体和联合体精确模拟 Rust 的所有权模型，避免引入运行时开销，实现零成本抽象。这种方法特别适用于嵌入式 FFI 场景，因为它绕过了 LLVM 后端，直接输出纯 C，无需 Rust 工具链依赖。
Eurydice 的架构依赖 Charon 插件从 rustc 提取完整 MIR 表示，包括类型、函数、trait 和 MIR 函数体。随后，将 MIR 翻译为 KaRaMeL 内部 AST（约 3000 行 OCaml 代码），再经 30+ 个纳米级优化传递（约 5000 行 OCaml 代码）生成 C。这些传递处理单态化（monomorphization）、模式匹配到标签联合、迭代器到 for 循环等，确保代码可读性。
关键创新在于所有权模拟。Rust 结构体直接映射为 C 结构体，包括动态大小类型（DST）使用灵活数组成员（flexible array members）。例如，Rust 中的固定数组 [u32; 8] 被包装为 struct { uint32_t data [8]; }，赋予 C 中的值语义，避免指针拷贝的复杂性。切片（slice）则编译为自定义 struct { void *ptr; size_t len; }，支持借用语义而无需运行时检查。枚举（enum）生成标签联合（tagged union），但优化去除单变体标签，减少冗余。
这种降阶绕过 LLVM，确保零成本抽象：Rust 的借用检查在 MIR 中已静态化，C 输出保留原生性能，无需额外抽象层。例如，在 libcrux 的 Kyber 实现中，生成的 C 代码体积虽因单态化增大，但保持高效，且与原 Rust 性能无差异（LLVM 优化后）。“Eurydice 将 Rust 结构体转换为 C 结构体，包括 DST 通过灵活数组成员。”（Protzenko 博客）
为嵌入式 FFI，Eurydice 生成 C11/C++20 兼容代码，使用复合初始化器如 (Foo){ .tag = bar, .value = { .case_Foo = { .bar = baz } } }。C++17 备选使用成员指针模拟。手写胶水头文件提供宏，如 #define core_slice___Slice_T___copy_from_slice (dst, src, t) memcpy (dst.ptr, src.ptr, dst.len * sizeof (t))，处理多态操作，避免 N 个单态化拷贝。
落地参数与清单：
- 配置单态化：使用 cg.yaml 指定实例放置，如 AVX2 类型到单独文件（-mavx2）。阈值：数组大小 >32 时用 memset 初始化而非逐元赋值。
- 编译标志：-fno-strict-aliasing（DST 指针转换违反严格别名）；-std=c11 或 C++20；无整数溢出检查（假设验证无 panic）。
- 集成步骤：
- 运行 charon 提取 MIR.llbc。
- Eurydice 编译：make test 生成 out/ 下 C 文件（版本控制检查 diff）。
- 添加 include/eurydice_glue.h 宏。
- CI 验证 Rust/C 等价（测试向量）。
- 监控点：代码体积（单态化后 2-5x Rust）；布局差异（手动对齐 pragma）；回滚：保留 C 后备，渐进迁移。
- 阈值参数：迭代器识别 >80% 转为 for 循环；空 enum 转为 void；重复数组 [0u8; N] 优先零初始化器。
风险：C 布局 ≠ Rust（无 padding 匹配）；多平台 cfg 需预处理 MIR。该策略在 HACL*、SymCrypt、BoringSSL 已部署，后量子算法如 ML-KEM 从 Rust 验证直出 C。
来源：