Creusot is a realistic deductive verifier, inspired by RustHorn, to efficiently encode Rust programs and offload proof obligations using SMT solvers, thanks to the Why3 framework. To demonstrate the soundness of Creusot, RustHornBelt has been developed, which is an extension of the RustBelt formal model, incorporating RustHorn features, notably functional correctness.Over time, Creusot has implemented extensions to enhance the user experience, moving away from the original proven model. Some unsound interactions have been discovered, and some restrictions have been proposed, but not yet formalised. These restrictions have been implemented in Creusot, and are expressive enough to prove Creusot’s extensive test suite. However, this implementation does not constitute a formal proof and could lead to other unsoundness when dealing with deeper interactions (e.g. unsafe Rust code).The main problem studied is the interaction between snapshots (a type of ghost code) and mutable borrows, which can result in unsoundness. Specifically, a causality loop occurs whereby the expected final value of a borrow depends on itself. The key issue is that without proper restrictions, the unsoundness reappears.We successfully proved that the restriction proposal is sound and expressive enough to prove each case that the initial model could solve. We also simplified the model, revealing that misunderstood complex interactions in RustHornBelt were necessary to avoid the same kind of unsound interactions encountered by Creusot.
Vincent Lafeychine (Wed,) studied this question.