We present Tachis, a higher-order separation logic to reason about the expected cost of probabilistic programs. Inspired by the uses of time credits for reasoning about the running time of deterministic programs, we introduce a novel notion of probabilistic cost credit. Probabilistic cost credits are a separation logic resource that can be used to pay for the cost of operations in programs, and that can be distributed across all possible branches of sampling instructions according to their weight, thus enabling us to reason about expected cost. The representation of cost credits as separation logic resources gives Tachis a great deal of flexibility and expressivity. In particular, it permits reasoning about amortized expected cost by storing excess credits as potential into data structures to pay for future operations. Tachis further supports a range of cost models, including running time and entropy usage. We showcase the versatility of this approach by applying our techniques to prove upper bounds on the expected cost of a variety of probabilistic algorithms and data structures, including randomized quicksort, hash tables, and meldable heaps. All of our results have been mechanized using Coq, Iris, and the Coquelicot real analysis library.

翻译：本文提出Tachis，一种用于推理概率程序期望成本的高阶分离逻辑。受确定性程序运行时间推理中时间信用机制的启发，我们引入了一种新颖的概率成本信用概念。概率成本信用作为分离逻辑资源，可用于支付程序中操作的成本，并能根据采样指令各分支的权重在所有可能分支间进行分配，从而实现对期望成本的推理。将成本信用表征为分离逻辑资源使Tachis具有高度的灵活性和表达力，特别是支持通过将超额信用作为势能存储于数据结构中以支付未来操作，从而实现摊销期望成本的推理。Tachis进一步支持包括运行时间和熵用量在内的多种成本模型。我们通过应用该技术证明多种概率算法与数据结构（包括随机快速排序、哈希表及可合并堆）的期望成本上界，展示了该方法的通用性。所有结果均已通过Coq、Iris及Coquelicot实分析库完成形式化验证。