在 Rust 验证生态向现代语言迁移的过程中，Eurydice 项目提供了一个关键桥梁：将 Rust 程序编译为可读 C 代码。通过 Charon 框架提取 Rust MIR（Mid-level Intermediate Representation），再经类型驱动翻译至 KaRaMeL 抽象语法树（AST），最终经 30 + 纳米级转换生成 C。这种上游管道确保了语义保真与代码可读性，避免了直接操作 rustc 内部的复杂性。
Charon 作为 Rust 分析框架，直接钩入 rustc 与 Cargo 构建系统，从 MIR 构建 ULLBC（无结构低级借用演算，CFG 视图）和 LLBC（低级借用演算，结构化 AST 视图）。相较原生 MIR，Charon 重建常量（从字节数组还原高阶结构）、解析 trait 实例（包括 where 子句与关联类型推导）、重构控制流（Relooper 算法恢复 for 循环与 if-then-else，避免 goto）。例如，trait 方法调用如 Vec::clone ()，Charon 显式暴露 TraitRef（TraitImplId + GenericArgs），精确追踪 CloneVec 与 T:Clone 组合，避免 rustc 查询的间接性与不完整性。“Charon acts as a swiss-army knife for analyzing Rust programs”（Charon 论文）。
从 LLBC 到 KaRaMeL AST 的翻译约 3000 行 OCaml 代码，类型驱动确保 Rust 借用语义（如 move/copy/reborrow）映射至 KaRaMeL 内部表示。关键挑战在于 trait 单态化：Rust 全程序单态化需处理类型 / 常量泛型参数，Eurydice 内置阶段（未来迁移 Charon）生成多份类型 / 函数副本。配置 yaml 控制实例放置，如 libcrux/c.yaml 中 monomorphizations_exact 分离 AVX2 类型至独立文件（编译时 - mavx2）。参数建议：阈值 > 16 泛型实例时拆文件；优先内联 static inline 宏（如 Eq trait 用 memcmp (a1,a2,len*sizeof (t))）。
模式匹配降阶是另一核心：LLBC 中 ML 式高阶 match 降至 C tagged union。Rust enum 如 Foo {Bar (baz) } 译为 struct Foo { uint8_t tag; union { struct { Baz bar; } case_Foo; } value; }。优化：单变体 enum 省略 tag；DST（动态大小类型）用 flexible array members（如 struct Slice { size_t len; uint8_t data []; }）。迭代器识别：array::from_fn 降为原位初始化（优于闭包通用方案）；Iterator 如 zip/map 链若可译 for 循环则替换，避免递归展开。清单：
| 优化类型 | 触发条件 | C 生成策略 | 阈值参数 |
|---|---|---|---|
| 数组重复初始化 | [0u8; N] | memset(buf, 0, N*sizeof(u8)); memcpy(ret, buf, ...) | N>32 用 memset |
| Eq trait | 平坦数组 / 切片 | Eurydice_array_eq 宏（!memcmp） | 全长 memcmp 优 |
| 模式匹配 | 单变体 | 无 tag struct | 始终应用 |
| 单态化 | 泛型深度 > 2 | 分文件 | yaml exact 条目 |
数组语义：Rust 数组为值，包装为 C struct {T data [N]; }，确保值语义而非指针 + memcpy。lvalue 约束需额外变量，如 &[0u32;1] 命名临时数组。评估顺序：C 松散定义用中间变量强制 Rust 顺序。
风险与回滚：布局不匹配（无 rustc 布局解析）；strict aliasing 违规（DST cast，编译 - fno-strict-aliasing）；cfg 多平台需 trick（如条件编译）。监控点：CI diff C 输出；格式化 ocamlformat/clang-format。部署：手写 glue 头文件（宏 /vtable），C11/C++20 兼容（designated init）或 C++17（member pointers）。
此管道落地参数：Charon 启用重建 pass（trait/const）；KaRaMeL nanopass 顺序（monomorphize→pattern_lower→cleanup2 迭代 opt）；阈值调优（小数组 < 4 直接赋，大用循环）。实例如 Kyber 后量子算法：Rust 验证后 C 集成 NSS/BoringSSL。
资料来源： [1] https://github.com/AeneasVerif/eurydice [2] https://jonathan.protzenko.fr/2025/10/28/eurydice.html “The design of Eurydice plugs in directly at the MIR level, using Charon” [3] https://arxiv.org/abs/2410.18042 Charon 框架论文