Reducing a uniform value modulo q

A uniform value below N, read in ZMod q, is close to uniform: each residue has ⌊N / q⌋ or ⌊N / q⌋ + 1 preimages, so the statistical distance to the uniform distribution on ZMod q is at most (N mod q) / N, and hence at most q / N (dist_map_natCast_uniformOfFintype_le). With N = 2 ^ ℓ fair bits this gives an efficient approximately uniform sampler for ZMod q, with distance at most q / 2 ^ ℓ; strict PPT machines cannot sample ZMod q exactly when q is not a power of two.

Main results

• Cslib.Probability.PMF.dist_map_natCast_uniformOfFintype_le: distance at most (N mod q) / N.
• Cslib.Probability.PMF.dist_map_natCast_uniformOfFintype_le_div: distance at most q / N.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Section 3.11.

theorem Cslib.Probability.PMF.dist_map_natCast_uniformOfFintype_le (N q : ℕ) [NeZero N] [NeZero q] : dist (PMF.map (fun (x : Fin N) => ↑↑x) (uniformOfFintype (Fin N))) (uniformOfFintype (ZMod q)) ≤ ↑(N % q) / ↑N

A uniform value reduced modulo q. A uniform value below N, read in ZMod q, is within statistical distance (N mod q) / N of the uniform distribution on ZMod q.

theorem Cslib.Probability.PMF.dist_map_natCast_uniformOfFintype_le_div (N q : ℕ) [NeZero N] [NeZero q] : dist (PMF.map (fun (x : Fin N) => ↑↑x) (uniformOfFintype (Fin N))) (uniformOfFintype (ZMod q)) ≤ ↑q / ↑N

A uniform value below N, read in ZMod q, is within statistical distance q / N of the uniform distribution on ZMod q.