The Essence of Higher-Order Concurrent Separation Logic.

Concurrent separation logics CSLs have come of age, and with age they have accumulated a great deal of complexity. Previous work on the Iris logic attempted to reduce the complex logical mechanisms of modern CSLs to two orthogonal concepts: partial commutative monoids PCMs and invariants. However, the realization of these concepts in Iris still bakes in several complex mechanisms--such as weakest preconditions and mask-changing view shifts--as primitive notions. In this paper, we take the Iris story to its so to speak logical conclusion, applying the reductionist methodology of Iris to Iris itself. Specifically, we define a small, resourceful base logic, which distills the essence of Iris: it comprises only the assertion layer of vanilla separation logic, plus a handful of simple modalities. We then show how the much fancier logical mechanisms of Iris--in particular, its entire program specification layer--can be understood as merely derived forms in our base logic. This approach helps to explain the meaning of Iris's program specifications at a much higher level of abstraction than was previously possible. We also show that the step-indexed \"later\" modality of Iris is an essential source of complexity, in that removing it leads to a logical inconsistency. All our results are fully formalized in the Coq proof assistant.