Statistical distance of Boolean games

Boolean distinguishing advantage equals the upstream finite-PMF metric. This bridge lets finite-source statistical bounds apply to every randomized Boolean test of an encoded output.

Main results

• Cslib.Crypto.Game.advantage_eq_nndist: Boolean advantage is statistical distance.

References

Copied from cslib PR #1072 at 1606f7e2fb50e15a8843c9a26a04a8d94cb424c3. Only the Boolean equality is included: the remaining arbitrary-type metric API requires #1065.

theorem Cslib.Crypto.Game.advantage_eq_nndist (game1 game2 : Game) : game1.advantage game2 = nndist game1 game2

The absolute difference of success probabilities is precisely statistical distance for Boolean experiments.