Programs using random values can either make all choices in advance (eagerly) or sample as needed (lazily). In formal proofs, we focus on indistinguishability between two lazy programs, a common requirement in the random oracle model (ROM). While rearranging sampling instructions often solves this, it gets complex when sampling is spread across procedures. The traditional approach, introduced by Bellare and Rogaway in 2004, converts programs to eager sampling, but requires assuming finite memory, a polynomial bound, and artificial resampling functions. We introduce a novel approach in probabilistic Relational Hoare Logic (pRHL) that directly proves indistinguishability, eliminating the need for conversions and the mentioned assumptions. We also implement this approach in the EasyCrypt theorem prover, showing that it can be a convenient alternative to the traditional method.

翻译：使用随机值的程序可以预先（急于）做出所有选择，也可以按需（惰性）进行采样。在形式化证明中，我们关注两个惰性程序之间的不可区分性，这是随机预言机模型（ROM）中的常见要求。虽然重新排列采样指令通常可以解决这一问题，但当采样分布在多个过程中时会变得复杂。贝尔（Bellare）和罗格威（Rogaway）在2004年提出的传统方法将程序转换为急于采样，但需要假设有限内存、多项式界限以及人为的重采样函数。我们在概率关系Hoare逻辑（pRHL）中引入了一种新方法，可以直接证明不可区分性，从而消除了转换和上述假设的必要性。我们还在EasyCrypt定理证明器中实现了该方法，表明它可以作为传统方法的便捷替代方案。