The type system of Rust enforces the “shared xor mutable” principle, which forbids mutation of shared memory. This principle eases verification in Rust, but certain programs require circumventing it with the mechanism of \emph{interior mutability}. Thus, supporting interior mutability in a deductive verification tool is difficult. The Verus tool demonstrated the use of \emph{ghost resources} to that end. So far, this mechanism has only been applied to Verus in order to verify mainly system code.

We extend the deductive verification tool Creusot with support for linear ghost resources. We show how Creusot’s full support for mutable borrows enables better specifications for primitives of linear ghost code. We apply this methodology to the verification of two data structure using sharing and mutation: union-find and persistent arrays.