# Trace Properties from Separation Logic Specifications

## TL;DR

This paper formalizes how separation logic specifications enforce trace properties on client-library interactions, ensuring protocol adherence through resource discipline and trace invariants.

## Contribution

It introduces a formal framework connecting separation logic specifications with trace properties, using wrappers and extended logic to guarantee protocol enforcement.

## Key findings

- Separation logic specifications enforce interaction protocols.
- Wrapped library code maintains trace properties.
- Correct client-library pairs satisfy trace invariants.

## Abstract

We propose a formal approach for relating abstract separation logic library specifications with the trace properties they enforce on interactions between a client and a library. Separation logic with abstract predicates enforces a resource discipline that constrains when and how calls may be made between a client and a library. Intuitively, this can enforce a protocol on the interaction trace. This intuition is broadly used in the separation logic community but has not previously been formalised. We provide just such a formalisation. Our approach is based on using wrappers which instrument library code to induce execution traces for the properties under examination. By considering a separation logic extended with trace resources, we prove that when a library satisfies its separation logic specification then its wrapped version satisfies the same specification and, moreover, maintains the trace properties as an invariant. Consequently, any client and library implementation that are correct with respect to the separation logic specification will satisfy the trace properties.