  We present Lilac, a separation logic for reasoning about probabilistic
programs where separating conjunction captures probabilistic independence.
Inspired by an analogy with mutable state where sampling corresponds to dynamic
allocation, we show how probability spaces over a fixed, ambient sample space
appear to be the natural analogue of heap fragments, and present a new
combining operation on them such that probability spaces behave like heaps and
measurability of random variables behaves like ownership. This combining
operation forms the basis for our model of separation, and produces a logic
with many pleasant properties. In particular, Lilac has a frame rule identical
to the ordinary one, and naturally accommodates advanced features like
continuous random variables and reasoning about quantitative properties of
programs. Then we propose a new modality based on disintegration theory for
reasoning about conditional probability. We show how the resulting modal logic
validates examples from prior work, and give a formal verification of an
intricate weighted sampling algorithm whose correctness depends crucially on
conditional independence structure.
