The Rust language offers a promising approach to safe systems programming based on the principle of \emph{aliasing XOR mutability}: a value may be \emph{either} aliased \emph{or} mutable, but not both at the same time. However, to implement pointer-based data structures with internal sharing, such as graphs or doubly-linked lists, we need to be able to mutate aliased state. To support such data structures, Rust provides a number of APIs that offer so-called \emph{interior mutability}: the ability to mutate data via method calls on a shared reference. Unfortunately, the existing APIs sacrifice flexibility, concurrent access, and/or performance, in exchange for safety.

In this paper, we propose a new Rust API called GhostCell which avoids such sacrifices by \emph{separating permissions from data}: it enables the user to safely synchronize access to a \emph{collection} of data via a single permission. GhostCell repurposes an old trick from typed functional programming: \emph{branded types} (as exemplified by Haskell's \texttt{ST} monad), which combine phantom types and rank-2 polymorphism to simulate a lightweight form of state-dependent types. We have formally proven the soundness of GhostCell by adapting and extending RustBelt, a semantic soundness proof for a representative subset of Rust, mechanized in Coq.