Uniqueness is Separation

TL;DR

This paper explores how uniqueness type systems can be integrated with Separation Logic to enable reasoning about mutable programs with value independence, balancing efficiency and verification complexity.

Contribution

It formalizes the expression of value independence guarantees from uniqueness types within Separation Logic for reasoning about mutable programs.

Findings

Uniqueness types enable efficient, mutation-based code with value independence.

Most systems include 'escape hatches' that weaken value independence guarantees.

The paper proposes a formal method to express these guarantees in Separation 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.