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, making it easy to write and prove precise specifications, including pointer-stability properties. Because it only changes how 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.

翻译：大多数分离逻辑出于模块化考虑隐藏容器内部指针。这使得难以规范那些暂时向外部暴露这些指针的容器API，也难以验证使用这些API的程序。我们提出逻辑固定——一种适用于顺序程序的轻量级借用模型，允许用户在逻辑层面选择性地追踪容器内部指针。该模型推广了魔杖运算符，使得编写和证明精确规范（包括指针稳定性属性）变得容易。由于仅改变表示谓词和规范的书写方式，我们的方法兼容大多数分离逻辑变体。我们通过验证小型但具有代表性的指针操作程序，并推导常见容器规范的更精确版本，展示了逻辑固定的实用性。在此过程中，我们证明该方法涵盖了一些著名的证明模式，简化了部分复杂证明，并支持传统规范无法处理的程序模式推理。所有结果均在Rocq证明助手中使用CFML库实现机械化验证。