Precise Reasoning About Container-Internal Pointers with Logical Pinning

TL;DR

The paper tackles the challenge of reasoning about container-internal pointers that containers expose temporarily, which many separation-logic frameworks struggle to support. It introduces logical pinning, a lightweight borrowing model with pointer-stability classifications and tagged multi-hole contexts, enabling precise, modular specifications that track which subparts are pinned or borrowed. A step-by-step proof discipline—identifying borrowable subparts, enriching APIs, and proving correctness with explicit borrow/return steps—underpins the approach, supported by borrowable data types and predicate transformers that compose ${}^{\flat}$ and ${}^{\ast}$. Case studies from flat containers to recursive structures demonstrate that logical pinning subsumes existing proof patterns, simplifies complex proofs, and enables reasoning about expose-then-mutate patterns, with all results mechanized in the Rocq proof assistant using CFML.

Abstract

Most separation logics hide container-internal pointers for modularity. This makes it difficult to specify container APIs that temporarily expose those pointers to the outside, and to verify programs that use these APIs. We present logical pinning, a lightweight borrowing model for sequential programs that allows users to selectively track container-internal pointers at the logical level. Our model generalizes the magic-wand operator for representing partial data structures, making it easy to write and prove precise specifications, including pointer-stability properties. Because it only changes the way representation predicates and specifications are written, our approach is compatible with most separation logic variants. We demonstrate the practicality of logical pinning by verifying small but representative pointer-manipulating programs, and deriving more precise versions of common container specifications. In doing so, we show that our approach subsumes some well-known proof patterns, simplifies some complex proofs, and enables reasoning about program patterns not supported by traditional specifications. All of our results are mechanized in the Rocq proof assistant, using the CFML library.

Figures (7)

• Figure 1: Left rotation of a binary tree.
• Figure 2: Two views of a container $c$ with elements $e_1 \dots e_4$ and exposed internal pointers $p_1$ and $p_3$. Left: $c$ owns all elements. Right: $e_1$ and $e_3$ are borrowed from $c$.
• Figure 3: An informal proof sketch of the functional correctness of the logger example. For simplicity, we assume the dictionary initially contains three key-logger pairs $(k_0, \, g_0)$, $(k_1, \, g_1)$ and $(k_2, \, g_2)$, where $k = k_1$. Each step is annotated with the corresponding abstract heap state, denoted $\{ \, \textit{state} \, \}$, together with a brief informal explanation (shown in blue). $[\mathit{lgr}]$ denotes an alias list with a single element $\mathit{lgr}$. Color markers: to change, just changed.
• Figure 4: Basic heap predicate combinators.
• Figure 5: Borrowing states and transitions.