AI 中文总结
研究针对概率程序验证框架局限于理想化语言的问题，提出基于Verus的Alerus框架，通过概率错误信用编码支持概率推理，可验证随机采样算法，还建立了健全性证明。
AI 中文摘要
近期工作已开发出许多形式验证概率程序的技术。然而，现有的概率程序验证框架局限于为验证设计的理想化语言，无法用于验证用标准语言编写的现成概率程序。相比之下，非概率程序已有不少验证工具支持验证如Go、C和Rust等常用语言编写的实际代码。本文提出Alerus，一个验证概率Rust程序的框架。它基于Verus，扩展支持概率推理，使用概率错误信用的轻量级编码，能验证随机采样算法的正确性，还通过改编VerusBelt建立了错误信用扩展的健全性证明。
英文摘要
Recent work has developed many techniques for formally verifying probabilistic programs. However, existing verification frameworks for probabilistic programs are restricted to idealized languages designed for verification. As a result, they cannot be used to verify off-the-shelf probabilistic programs written in standard languages. In contrast, for non-probabilistic programs, a number of verification tools now support verifying realistic code written in widely used languages such as Go, C, and Rust. To verify probabilistic programs written in these languages, it would be useful to be able to reuse, as much as possible, the extensive development work that has gone into such tools. This paper presents Alerus, a framework for verifying probabilistic Rust programs. Alerus is based on Verus, a verification tool for Rust that supports SMT-based automation and separation-logic-inspired reasoning features. Alerus extends Verus with support for probabilistic reasoning while retaining these expressive features. To do so, Alerus uses a lightweight encoding of probabilistic error credits, a form of ghost state for randomized reasoning introduced in the Eris program logic. By deriving an appropriate specification using error credits, Alerus supports verifying the correctness of randomized sampling algorithms. We use this technique to verify several sampling routines for discrete distributions, including samplers for the discrete Gaussian distributions, the alias method, and the fast loaded dice roller. We establish the soundness of our error credit extension by adapting VerusBelt, a recently developed logical relations model of Verus that encodes its features in terms of the Iris separation logic. To do so, we replace the use of Iris's standard weakest precondition in this model with Eris's probabilistic weakest precondition instead. The resulting soundness proof is fully mechanized in Rocq.
