Tachis: Higher-Order Separation Logic with Credits for Expected Costs

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进一步支持一系列成本模型，包括运行时间和熵用法。我们通过应用我们的技术来证明这种方法的多功能性，以证明各种概率算法和数据结构的预期成本（包括随机的QuickSort，Hash Tables和可融合的堆）的上限。我们所有的结果均已使用COQ，IRIS和COQUELICOT真实分析库进行了机械化。