6.1. Motivation🔗

In game-based cryptographic proofs, security reductions often require showing that two probabilistic computations produce the same distribution. After unfolding definitions and simplifying oracle implementations, these goals reduce to: both sides sample the same uniform draws but in different order, possibly with extra unused draws on one side. Proving this by hand requires computing the permutation between draw orders and emitting a sequence of adjacent transpositions, which is tedious and error-prone.

The perm_draws tactic automates this entirely.