Sound Borrow-Checking for Rust via Symbolic Semantics
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要