Most implementations of sampling algorithms for continuous distributions use floating-point numbers, which introduce round-off errors and approximations. These errors can be difficult to analyze, and can cause security issues when used in algorithms for differential privacy. An alternative is to use exact sampling algorithms based on computable reals, which can lazily generate the digits of a continuous sample to arbitrary precision. However, these algorithms are intricate, and implementing and using them involves a combination of semantically challenging language features, such as probabilistic choice, higher-order functions, and dynamically-allocated mutable state. In this paper we present Continuous-Eris, a higher-order separation logic for verifying the correctness of exact sampling algorithms for computable distributions. To demonstrate Continuous-Eris, we verify the correctness of computable samplers for the uniform, Gaussian, and Laplace distributions, as well as a library for exact real arithmetic for working with generated samples. All of the results in this paper have been verified in the Rocq proof assistant.

翻译：大多数连续分布采样算法的实现使用浮点数，这会引入舍入误差和近似。这些误差难以分析，并且在用于差分隐私算法时可能引发安全问题。一种替代方法是基于可计算实数的精确采样算法，该算法能惰性地生成连续样本的任意精度数字。然而，这些算法结构复杂，其实现和使用涉及多种语义上具有挑战性的语言特性，例如概率选择、高阶函数和动态分配的可变状态。本文提出了Continuous-Eris——一种用于验证可计算分布精确采样算法正确性的高阶分离逻辑。为演示Continuous-Eris，我们验证了均匀分布、高斯分布和拉普拉斯分布的可计算采样器的正确性，以及一个用于处理生成样本的精确实数算术库的正确性。本文的所有结果均已通过Rocq证明助手验证。