6.2. Usage🔗

After normalizing both sides of a distributional equality to bind chains of uniform draws (typically via simp and simp_all), a single call to perm_draws closes the goal:

private lemma passiveReal_eq_ddhExpReal
    (g : G) (adv : PassiveAdversary G SK) :
    evalDist (execGame (passiveReal g adv)) =
    evalDist (DiffieHellman.ddhExpReal g (ddhReduction adv)) := by
  unfold passiveReal passiveGame DiffieHellman.ddhExpReal ddhReduction execGame
  simp only [simulateQ_bind, simulateQ_query, ...]
  ext z; change Pr[= z | _] = Pr[= z | _]; simp_all
  perm_draws