一句话：提出 EHL 的 hopping 证明规则，将概率程序的期望性质目标归约到相关程序，并在 EasyCrypt 中机验证其可靠性。
概率程序的期望性质（如期望复杂度）验证十分困难，现有语法导向证明系统难以处理需要改变程序结构的情形。本文提出 hopping 证明方法，将 EHL（一种语法导向的期望性质证明系统）与一条 hopping 规则结合：该规则把原程序的证明目标归约到另一个通过 pRHL 与原程序关联的程序的目标。作者证明了 EHL 对含过程调用与对抗计算的核语言的可靠性，并在无对抗片段上证明其完备性；同时将 EHL 实现进 EasyCrypt，与 pRHL 等程序逻辑紧密集成。借助该集成，作者给出了原地随机化快速选择与跳表的期望复杂度的机器化证明，并讨论了其在密码学证明中的应用与更广泛影响。
We propose, implement, and evaluate a hopping proof approach for proving expectation-based properties of probabilistic programs. Our approach combines EHL, a syntax-directed proof system for reducing proof goals of a program to proof goals of simpler programs, with a "hopping" proof rule for reducing proof goals of an original program to proof goal of a different program which is suitably related (by means of pRHL, a relational program logic for probabilistic program) to the original program. We prove that EHL is sound for a core language with procedure calls and adversarial computations, and complete for the adversary-free fragment of the language. We also provide an implementation of EHL into EasyCrypt, a proof assistant tailored for reasoning about relational properties of probabilistic programs. We provide a tight integration of EHL with other program logics supported by EasyCrypt, and in particular probabilistic Relational Hoare Logic (pRHL). Using this tight integration, we give mechanized proofs of expected complexity of in-place implementations of randomized quickselect and skip lists. We also sketch applications of our approach to cryptographic proofs and discuss the broader impact of EHL in the EasyCrypt proof assistant.
@article{paperbot2551,
title = {Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs},
author = {Martin Avanzini and Gilles Barthe and Benjamin Grégoire and Georg Moser and Gabriele Vanoni},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649839}
}