Safety, Relative Tightness and the Probabilistic Frame Rule

TL;DR

This paper develops a semantic formulation of probabilistic separation logic that simplifies the frame rule by incorporating safety and relative tightness, enabling modular reasoning about probabilistic programs.

Contribution

It introduces a new semantic approach that embeds safety into specifications, ensuring the soundness of the frame rule without additional side conditions.

Findings

The frame rule can be applied without extra side conditions.

Safety and relative tightness are key to the logic's soundness.

The approach simplifies reasoning about probabilistic independence.

Abstract

Probabilistic separation logic offers an approach to reasoning about imperative probabilistic programs in which a separating conjunction is used as a mechanism for expressing independence properties. Crucial to the effectiveness of the formalism is the frame rule, which enables modular reasoning about independent probabilistic state. We explore a semantic formulation of probabilistic separation logic, in which the frame rule has the same simple formulation as in separation logic, without further side conditions. This is achieved by building a notion of safety into specifications, using which we establish a crucial property of specifications, called relative tightness, from which the soundness of the frame rule follows.