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

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