There has recently been exciting progress in the realm of probabilistic separation logics. An important subclass of these-including PSL, Lilac, Bluebell, and pcOL-are distributional probabilistic logics (or DPLs, for short), meaning that they provide primitive Hoare-style assertions about probability distributions on the program state, along with powerful modularity principles like independence and conditioning. However, none of these logics support reasoning about dynamically allocated memory (i.e., pointers into a heap), let alone the more sophisticated resource algebra-based ghost state of modern separation logics like Iris. We argue that this is due to a fundamental obstacle: since the shape of memory (and identity of memory locations) may differ under different random outcomes, it is unclear how pointer ownership can be harmonized with probabilistic independence and conditioning. In this paper, we take substantial first steps towards a marriage of DPLs and modern separation logics like Iris, in the form of Amaryllis. Amaryllis is the first DPL to support independence and conditional reasoning while also handling dynamic memory allocation. To overcome the aforementioned obstacle, we propose a new indexed valuation-style model of probabilistic assertions, whereby ownership and composition of standard Iris-style resources (e.g., heaps) can be promoted to corresponding notions of ownership and composition at the level of distributions by interpreting them per random outcome. We then show how to adapt the central Iris notions of frame-preserving update, authoritative resource algebras, and the weakest precondition modality to be sound for probabilistic reasoning and validate dynamic allocation. Finally, we have mechanized all our results in the Rocq proof assistant and developed an Iris-based proof mode for conducting proofs within Amaryllis.

翻译：暂无翻译