LWN.net 報導了名為 Eurydice 的新專案，其目標是將 Rust 程式碼轉換為乾淨的 C 程式碼。與傳統編譯器不同，Eurydice 旨在保留程式碼的整體結構，同時移除 Rust 中存在但 C 語言不支援的構建。這對於高保證軟體特別有用，因為現有的驗證和合規工具通常預期輸入為 C 語言。Eurydice 已被用於將部分後量子密碼學例程從 Rust 編譯為 C。
Eurydice 於 2023 年啟動，包含 MIT 和 Apache-2.0 授權的程式碼，是 Aeneas 專案的一部分。Aeneas 專案由法國國家計算機科學研究機構 Inria 和 Microsoft 僱用的人員維護，但也接受外部貢獻。Eurydice 遵循標準編譯器結構：將 Rust 程式轉換為中間表示（IR），通過一系列遍歷修改 IR，然後輸出為 C 程式碼。
主要貢獻者 Jonathan Protzenko 解釋了該專案的方法。Eurydice 通過添加額外的臨時變數（如 `uu____0`）來保留原始程式碼的評估順序，以確保符合 Rust 的語義保證（例如，確保乘法溢出導致的 panic 發生在調用其他函數的副作用之前）。相比之下，使用 rustc 編譯相同的函數會產生充滿位元運算的糾纏迴圈，雖然適合機器碼輸出，但可讀性較差。
然而，並非所有 Rust 程式都能忠實地表示為 C。例如，使用迭代器的 `for` 迴圈需要編譯為調用 Eurydice 支援程式碼的 `while` 迴圈。此外，由於 C 語言沒有泛型概念，Rust 程式碼在轉換過程中必須進行單態化（monomorphization），這可能導致產生僅在類型上不同的多個函數實現。對於動態大小型別，Eurydice 會發出兩種不同的類型：一種具有彈性陣列成員，另一種具有已知長度的陣列成員。這種轉換在執行時是無操作的，但技術上違反了 C 語言的嚴格別名規則，因此建議使用 `-fno-strict-aliasing` 編譯標誌。
Eurydice 基於 KaRaMeL 專案，該專案將 F* 程式語言編譯為 C。Eurydice 目前無法擴展到大型範例，因為它依賴另一個 Aeneas 工具 Charon 從 rustc 提取解析和預處理後的程式。Charon 經常被較新的 Rust 功能（如 const generics）所阻礙。當 Charon 成功時，它會將 rustc 的中級中間表示（MIR）轉儲為 JSON，Eurydice 讀取此 JSON 並將其轉換為 KaRaMeL 的中間表示，然後使用 KaRaMeL 的程式碼生成邏輯輸出 C 程式碼。目前，Eurydice 最適合避免複雜 Rust 功能的小型、自包含程式。
事件背景
Eurydice 是 Aeneas 專案的一部分，該專案致力於開發將形式化驗證工具應用於 Rust 程式碼的各種工具。Aeneas 專案由 Inria（法國國家計算機科學研究機構）和 Microsoft 僱用的人員維護。Eurydice 基於 KaRaMeL 專案，後者將 F* 程式語言（一種用於開發加密庫的依賴類型函數式程式語言）編譯為 C。這種將更抽象語言編譯為保留結構的 C 碼的方法並非新創，KaRaMeL 已對 F* 執行了類似操作。
社群觀察
社群討論中，使用者 weinzierl 推薦查看 AeneasVerif 的其他專案，並提到有正在進行的工作將 Eurydice 生成的程式碼整合到 Microsoft 和 Google 的加密庫中。使用者 nlehuen 質疑生成的 C 程式碼的可讀性，特別是變數命名（如 `uu____0`），建議使用更具描述性的名稱如 `return_value`。使用者 stabbles 認為如果 C 碼可讀，這對於 Rust 編譯器的完整源碼自舉很有幫助。使用者 Neywiny 希望報導能涵蓋更多 Rust 特有的執行時安全特性（如邊界檢查）如何轉換回 C。使用者 chias 則對產品名稱 Eurydice 進行了諧音玩笑。
