A Direct Lazy Sampling Proof Technique in Probabilistic Relational Hoare Logic

Roberto Metere, Changyu Dong

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 prog…