Separation logic is often praised for its ability to closely mimic the locality of state updates when reasoning about them at the level of assertions. The prover only needs to concern themselves with the footprint of the computation at hand, i.e., the part of the state that is actually being accessed and manipulated. Modern concurrent separation logics lift this local reasoning principle from the physical state to abstract ghost state. For instance, these logics allow one to abstract the state of a fine-grained concurrent data structure by a predicate that provides a client the illusion of atomic access to the underlying state. However, these abstractions inadvertently increase the footprint of a computation: when reasoning about a local low-level state update, one needs to account for its effect on the abstraction, which encompasses a possibly unbounded portion of the low-level state. Often this gives the reasoning a global character. We present context-aware separation logic (CASL) to provide new opportunities for local reasoning in the presence of rich ghost state abstractions. CASL introduces the notion of a context of a computation, the part of the concrete state that is only affected on the abstract level. Contexts give rise to a new proof rule that allows one to reduce the footprint by the context, provided the computation preserves the context as an invariant. The context rule complements the frame rule of separation logic by enabling more local reasoning in cases where the predicate to be framed is known in advance. We instantiate our developed theory for the flow framework, which enables local reasoning about global properties of heap graphs. We then use the instantiation to obtain a fully local proof of functional correctness for a sequential binary search tree implementation that is inspired by fine-grained concurrent search structures.

翻译：分离逻辑常因其在断言层面推理状态更新时，能够紧密模拟状态更新的局部性而备受赞誉。验证者只需关注当前计算所涉及的足迹，即实际被访问和操作的状态部分。现代并发分离逻辑将这一局部推理原则从物理状态提升到抽象幽灵状态。例如，这些逻辑允许通过谓词抽象细粒度并发数据结构的局部状态，该谓词为客户端提供对底层状态的原子访问的假象。然而，这些抽象无意中扩大了计算的足迹：在推理局部低级状态更新时，需要考虑其对抽象的影响，而抽象可能涵盖底层状态的无限部分。这往往使得推理具有全局特性。我们提出了**上下文感知分离逻辑（CASL）**，为在丰富的幽灵状态抽象存在下提供新的局部推理机会。CASL引入了**计算上下文**的概念，即仅在抽象层面上受影响的具象状态部分。上下文催生了一条新的证明规则，允许将足迹缩减至上下文范围，前提是计算将上下文保持为不变量。上下文规则补充了分离逻辑的帧规则，在预先已知待封装谓词的情况下实现更局部的推理。我们将所发展的理论实例化到流框架中，该框架支持对堆图全局属性的局部推理。随后，利用该实例化对受细粒度并发搜索结构启发的顺序二叉搜索树实现的功能正确性进行了完全局部的证明。