RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code

Rust is a systems programming language that offers both lowlevel memory operations and high-level safety guarantees, via a strong ownership type system that prohibits mutation of aliased state. In prior work, Matsushita et al. developed RustHorn, a promising technique for functional verification of Rust code: it leverages the strong invariants of Rust types to express the behavior of stateful Rust code with first-order logic (FOL) formulas, whose verification is amenable to offthe-shelf automated techniques. RustHorn's key idea is to use prophecies to describe the behavior of mutable borrows. However, the soundness of RustHorn was only established for a safe subset of Rust, and it has remained unclear how to extend it to support various safe APIs that encapsulate unsafe code (i.e., code where Rust's aliasing discipline is relaxed).

In this paper, we present RustHornBelt, the first machinechecked proof of soundness for RustHorn-style verification which supports giving FOL specs to safe APIs implemented with unsafe code. RustHornBelt employs the approach of semantic typing used in Jung et al.'s RustBelt framework, but it extends RustBelt's model to reason not only about safety but also functional correctness. The key challenge in RustHornBelt is to develop a semantic model of RustHornstyle prophecies, which we achieve via a new separationlogic mechanism we call parametric prophecies.