Rust is a systems programming language that offers both low-level 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 off-the-shelf automated techniques. RustHorn’s key idea is to use \emph{prophecies} to describe the behavior of mutable borrows. However, the soundness of RustHorn was only established for a \emph{safe} subset of Rust, and it has remained unclear how to extend it to support various safe APIs that encapsulate \emph{unsafe} code (i.e. code where Rust’s aliasing discipline is relaxed).

In this paper, we present \textbf{RustHornBelt}, the first machine-checked proof of soundness for RustHorn-style verification which supports giving FOL specs to safe APIs implemented with unsafe code. RustHornBelt employs the approach of \emph{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 RustHorn-style prophecies, which we achieve via a new separation-logic mechanism we call \emph{parametric prophecies}.