The Rust programming language continues to rise in popularity, and as such, warrants the close attention of the programming languages community. In this work, we present a new foundational contribution towards the theoretical understanding of Rust's semantics. We prove that LLBC, a high-level, borrow-centric model previously proposed for Rust's semantics and execution, is sound with regards to a low-level pointer-based language \`a la CompCert. Specifically, we prove the following: that LLBC is a correct view over a traditional model of execution; that LLBC's symbolic semantics are a correct abstraction of LLBC programs; and that LLBC's symbolic semantics act as a borrow-checker for LLBC, i.e. that symbolically-checked LLBC programs do not get stuck when executed on a heap-and-addresses model of execution. To prove these results, we introduce a new proof style that considerably simplifies our proofs of simulation, which relies on a notion of hybrid states. Equipped with this reasoning framework, we show that a new addition to LLBC's symbolic semantics, namely a join operation, preserves the abstraction and borrow-checking properties. This in turn allows us to add support for loops to the Aeneas framework; we show, using a series of examples and case studies, that this unlocks new expressive power for Aeneas.

翻译：Rust编程语言持续流行，这值得编程语言学界对其予以密切关注。本文为理解Rust语义的理论基础做出了一项新贡献。我们证明：LLBC（一种先前为Rust语义和执行提出的高级、以借用为中心的模型）相对于类似CompCert的低层指针语言是可靠的。具体而言，我们证明以下结论：LLBC是传统执行模型的正确视图；LLBC的符号语义是LLBC程序的正确抽象；LLBC的符号语义可作为LLBC的借用检查器，即经符号检查的LLBC程序在堆-地址执行模型上运行时不会陷入停滞。为证明这些结果，我们引入了一种新的证明风格，该风格借助混合状态概念显著简化了模拟证明。借助这一推理框架，我们证明LLBC符号语义的新增操作（即连接操作）能够保持抽象性和借用检查属性。这进而使我们能够为Aeneas框架添加循环支持。通过一系列示例和案例研究，我们证明这为Aeneas释放了新的表达能力。