Sound Borrow-Checking for Rust via Symbolic Semantics (Long Version)
Son Ho, Aymeric Fromherz, Jonathan Protzenko

TL;DR
This paper provides a formal foundation for Rust's borrow-checking mechanism by proving the soundness of a high-level borrow-centric model, LLBC, with respect to low-level semantics, enhancing understanding and tooling for Rust's safety guarantees.
Contribution
It introduces a new proof style using hybrid states to establish the soundness of LLBC's symbolic semantics and extends the Aeneas framework with loop support, improving Rust analysis tools.
Findings
LLBC is sound with respect to a low-level pointer-based language.
Symbolic semantics of LLBC correctly abstract program execution.
Adding join operation preserves borrow-checking and abstraction properties.
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsHorticultural and Viticultural Research · Postharvest Quality and Shelf Life Management · Berry genetics and cultivation research
