Uniqueness is Separation

TL;DR

The paper addresses expressing value independence guaranteed by uniqueness types in the presence of imperative, mutable code. Its main approach encodes the frame guarantees with Separation Logic, notably using a heap footprint model and a single triple like $ \{ *_{\ell \in p} \exists v.\ \ell \mapsto v \} P \{ *_{\ell \in p'} \exists v.\ \ell \mapsto v \} $. Key contributions include deriving the three conventional frame conditions from Cogent's semantics, showing their expression via Separation Logic, and arguing for a language design that translates type-level assertions into Separation Logic for verification of low-level extensions. This work aims to enable scalable, modular verification of mixed Cogent-C systems by tying type-based reasoning to a formal program logic.

Abstract

Value independence is enormously beneficial for reasoning about software systems at scale. These benefits carry over into the world of formal verification. Reasoning about programs algebraically is a simple affair in a proof assistant, whereas programs with unconstrained mutation necessitate much more complex techniques, such as Separation Logic, where invariants about memory safety, aliasing, and state changes must be established by manual proof. Uniqueness type systems allow programs to be compiled to code that uses mutation for efficiency, while retaining a semantics that enjoys value independence for reasoning. The restrictions of these type systems, however, are often too onerous for realistic software. Thus, most uniqueness type systems include some "escape hatch" where the benefits of value independence for reasoning are lost, but the restrictions of uniqueness types are lifted. To formally verify a system with such mixed guarantees, the value independence guarantees from uniqueness types must be expressed in terms of imperative, mutable semantics. In other words, we ought to express value independence as an assertion in Separation Logic.