Sound Borrow-Checking for Rust via Symbolic Semantics (Long Version)

TL;DR

This work addresses the challenge of giving a formal, sound semantic foundation for Rust’s borrow-checking by connecting LLBC, a borrow-centric core, to a traditional heap-based memory model via HLPL and the Pointer Language PL. It introduces LLBC#, a symbolic borrow-checker for LLBC, and proves that successful LLBC# executions imply safe LLBC (and hence PL) executions through a forward simulation, complemented by a backward simulation to PL for terminating cases. A novel join/collapse mechanism enables loop handling and composition of multiple control-flow branches, enabling loop-rich Rust programs to be analyzed within this framework. The results demonstrate a scalable, modular approach to proving semantic soundness and borrow-checking correctness, with implementations and case studies validating practical applicability and potential improvements to Rust’s borrow-checker.

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 à 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.

Figures (24)

• Figure 1: The architecture of our proof
• Figure 2: The Low-Level Borrow Calculus (LLBC): Syntax (Selected Constructs).
• Figure 3: Operational Semantics for LLBC (Selected Rules)
• Figure 4: Selected Rules for HLPL
• Figure 5: The $\le$ Relation on $\text{HLPL}^{+}$ states (Selected Rules)

Theorems & Definitions (11)

• definition 1: Forward Simulation
• theorem 1: Forward Simulation on Superset Language
• definition 2: Stability
• theorem 2: Eval-Preserves-HLPL+-Rel
• theorem 3: Forward Relation for $\text{HLPL}^{+}$ and HLPL
• theorem 4: Eval-LLBC-Preserve-Rel
• theorem 5
• theorem 6
• theorem 7: Backward Simulation Between PL and LLBC
• theorem 8: Join-Collapse-Le