We present our ongoing work on developing an end-to-end verified Rust compiler based on CompCert. It provides two guarantees: one is semantics preservation from Rust to assembly, i.e., the behaviors of source code includes the behaviors of target code, with which the properties verified at the source can be preserved down to the target; the other is memory safety ensured by the verifying compilation -- the borrow checking pass, which can simplify the verification of Rust programs, e.g., by allowing the verification tools focus on the functional correctness.

翻译：本文介绍了我们基于CompCert开发端到端经验证的Rust编译器的持续研究工作。该编译器提供双重保证：其一是从Rust到汇编语言的语义保持性，即源代码行为包含目标代码行为，使得在源语言层面验证的性质能够保持至目标代码层面；其二是通过可验证编译过程（特别是借用检查阶段）确保内存安全性，该机制能够简化Rust程序的验证工作，例如使验证工具能够专注于功能正确性验证。