Separation Logic of Generic Resources via Sheafeology
Abstract
Separation logic was conceived in order to make the verification of pointer programs scalable to large systems and it has proven extremely effective. The key idea is that programs typically access only small parts of memory, allowing for local reasoning. This idea is implemented in separation logic by extending first-order logic with separating connectives, which inspect local regions of memory. It turns that this approach not only applies to pointer programs, but also to programs involving other resource structures. Various theories have been put forward to extract and apply the ideas of separation logic more broadly. This resulted in algebraic abstractions of memory and many variants of separation logic for, e.g., concurrent programs and stochastic processes. However, none of the existing approaches formulate the combination of first-order logic with separating connectives in a theory that could immediately yield program logics for different resources. In this paper, we propose a framework based on the idea that separation logic can obtained by making first-order logic resource-aware. First-order logic can be understood in terms of categorical logic, specifically fibrations. Our contribution is to make these resource-aware by developing categorical logic internally in categories of sheaves, which is what we call sheafeology. The role of sheaves is to model views on resources, through which resources can be localised and combined, which enables the scalability promised by separation logic. We contribute constructions of an internal fibration in sheaf categories that models predicates on resources, and that admits first-order and separating connectives. Thereby, we attain a general framework of separation logic for generic resources, a claim we substantiate by instantiating our framework to various memory models and random variables.