@unpublished{ho2024sound,
author = {Ho, Son and Fromherz, Aymeric and Protzenko, Jonathan},
title = {Sound Borrow-Checking for Rust via Symbolic Semantics},
year = {2024},
month = {July},
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.},
url = {http://approjects.co.za/?big=en-us/research/publication/sound-borrow-checking-for-rust-via-symbolic-semantics/},
}