Formal Verification of Borrow-Checking by Local Commutation Diagrams

The Rust programming language provides a safe alternative to C and C++ for system programming. In particular, it achieves memory safety with an ownership-based typing discipline, providing a notion of borrows as a restriction on aliasable pointers. The discipline of borrows is statically enforced by a component of the compiler called the borrow-checker. In their article published at the ICFP conference in 2024, Ho, Fromherz and Protzenko prove that LLBC, a borrow-centric model of Rust, can be equipped with a symbolic semantics that plays the role of a borrow-checker. They also prove that LLBC is a sound model with respect to an operational semantics over a standard memory model à la CompCert.<p>In this article, we initiate the formalization of this work in the Rocq proof assistant. In particular, we found a flaw in the proofs of some of their fundamental lemmas. We repair their methodology using techniques from rewriting theory. We finally present the current state of our formalization, and how we use a rewriting system to automate proofs.</p>

hal.science