一句话：证明 LLBC 及其符号语义是底层指针语言的正确抽象，可作为健全借用检查器，并使 Aeneas 支持循环。
本文研究 Rust 语义的理论基础，特别是高层、以借用为中心的 LLBC 模型与底层指针式执行模型之间的可靠关系。作者证明 LLBC 是传统堆与地址执行模型的正确视图，其符号语义正确抽象 LLBC 程序，并且符号检查可充当借用检查器：经符号检查的 LLBC 程序在底层模型上执行不会卡住。为证明这些结果，论文提出基于 hybrid states 的新证明风格，显著简化模拟证明，并表明 LLBC 符号语义新增的 join 操作保持抽象性与借用检查性质。最终，该工作为 Aeneas 框架加入循环支持，并通过示例与案例研究展示其新的表达力。
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 à 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{HoFP24,
title = {Sound Borrow-Checking for Rust via Symbolic Semantics},
author = {Son Ho and Aymeric Fromherz and Jonathan Protzenko},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674640}
}