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 *general-purpose probabilistic logics* (or GPLs, 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. Furthermore, none of the existing GPLs have been mechanized in a proof assistant. In this paper, we take a substantial first step towards a marriage of GPLs and modern separation logics like Iris, in the form of **Amaryllis**. Amaryllis is the first GPL 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 of a standard Iris-style resource (e.g., heaps) can be promoted to ownership at the level of distributions in a generic fashion. 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.

翻译：近年来，概率分离逻辑领域取得了令人瞩目的进展。其中一类重要的子逻辑（包括PSL、Lilac、Bluebell和pcOL）属于**通用概率逻辑**（简称GPL），它们提供了关于程序状态概率分布的原始Hoare风格断言，以及强大的模块化原则（如**独立性**和**条件化**）。然而，这些逻辑均不支持对动态分配内存（即指向堆的指针）的推理，更不用说现代分离逻辑（如Iris）中基于资源代数的复杂幻影状态。我们认为这源于一个根本性障碍：由于内存的形状（及内存位置的身份）在不同随机结果下可能不同，指针所有权如何与概率独立性和条件化相协调尚不明确。此外，现有GPL均未在证明助手中实现机械化。本文以**Amaryllis**的形式，向GPL与现代分离逻辑（如Iris）的结合迈出了实质性第一步。Amaryllis是首个在支持独立性与条件推理的同时处理动态内存分配的GPL。为克服上述障碍，我们提出了一种基于"索引赋值"（indexed valuation）的概率断言新模型，通过该模型，标准Iris风格资源（如堆）的所有权可以以通用方式提升至分布层面的所有权。随后，我们展示了如何调整Iris的核心概念——**框架保持更新**、**权威资源代数**和**最弱前置条件模态**——使其在概率推理中成立并验证动态分配。最后，我们在Rocq证明助手中实现了所有结果的机械化，并开发了基于Iris的证明模式，用于在Amaryllis内进行证明。