Sound Borrow-Checking for Rust via Symbolic Semantics (Long Version)
<|reference_start|>Sound Borrow-Checking for Rust via Symbolic Semantics (Long Version): 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.<|reference_end|>
@article{ho2024sound,
    title={Sound Borrow-Checking for Rust via Symbolic Semantics (Long Version)},
    author={Son Ho, Aymeric Fromherz, Jonathan Protzenko},
    journal={arXiv preprint arXiv:2404.02680},
    year={2024},
    archivePrefix={arXiv},
    eprint={2404.02680},
    primaryClass={cs.PL}
}