Sampling bounded indices

sampleBinaryNat width interprets exactly width fair bits as a natural number, giving the uniform distribution below 2 ^ width. Its runtime certificate uses binary output.

sampleBoundedIndex bound uses log₂ bound + 1 fair bits. Each index strictly below bound has the same probability; the remaining probability is assigned to the sentinel bound. There is no unbounded rejection loop.

sampleModNat width modulus reduces such a value modulo modulus. Read in ZMod q, it is within statistical distance q / 2 ^ width of uniform (dist_map_natCast_eval_sampleModNat_le): strict PPT machines sample ZMod q only approximately, and enough extra bits make the error small.

sampleDyadicIndex bound instead samples exactly uniformly below the next power of two, whose range is at most 2 * (bound + 1). sampleDyadicCoin bound numerator compares such an index with numerator, sampling the exact capped fraction numerator / dyadicSize bound.

Main definitions

• sampleBinaryNat: exact uniform sampling from a specified bit width.
• sampleModNat: approximately uniform sampling of residues modulo a given modulus.
• sampleDyadicIndex: exact uniform sampling in the power-of-two range.
• sampleBoundedIndex: a capped uniform index with a rejection sentinel.
• sampleDyadicCoin: an exact capped dyadic acceptance probability.

Main results

• eval_sampleBinaryNat, mem_support_sampleBinaryNat_iff: the exact law and support.
• eval_sampleModNat, dist_map_natCast_eval_sampleModNat_le: the law of the residue sampler and its distance from uniform on ZMod q.
• eval_sampleDyadicIndex, eval_sampleBoundedIndex: exact distribution laws.
• eval_sampleDyadicCoin_true: exact acceptance mass, including zero and one.

References

Adapted from Languages/Probabilistic/UniformNat.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

noncomputable def Cslib.Probability.sampleBinaryNat (width : ℕ) : ProbComp ℕ

Interpret exactly width independent fair bits as a binary natural number.

@[simp]

theorem Cslib.Probability.sampleBinaryNat_zero : sampleBinaryNat 0 = pure 0

With width zero the sampler returns 0 without sampling.

theorem Cslib.Probability.eval_sampleBinaryNat (width : ℕ) : (sampleBinaryNat width).eval = PMF.map Fin.val (PMF.uniformOfFintype (Fin (2 ^ width)))

The sampled value is exactly uniform below 2 ^ width, including width zero.

noncomputable def Cslib.Probability.sampleModNat (width modulus : ℕ) : ProbComp ℕ

Reduce width fair bits, read as a binary natural number, modulo modulus.

theorem Cslib.Probability.eval_sampleModNat (width modulus : ℕ) : (sampleModNat width modulus).eval = PMF.map (fun (x : Fin (2 ^ width)) => ↑x % modulus) (PMF.uniformOfFintype (Fin (2 ^ width)))

The residue sampler reduces a uniform value below 2 ^ width.

theorem Cslib.Probability.dist_map_natCast_eval_sampleModNat_le (width q : ℕ) [NeZero q] : dist (PMF.map Nat.cast (sampleModNat width q).eval) (PMF.uniformOfFintype (ZMod q)) ≤ ↑q / 2 ^ width

Approximately uniform residues. Read in ZMod q, the residue of width fair bits is within statistical distance q / 2 ^ width of the uniform distribution on ZMod q.

theorem Cslib.Probability.mem_support_sampleBinaryNat_iff (width value : ℕ) : value ∈ (sampleBinaryNat width).eval.support ↔ value < 2 ^ width

Every value below 2 ^ width can occur, and no other value can occur.

noncomputable def Cslib.Probability.sampleDyadicIndex (bound : ℕ) : ProbComp ℕ

An exact uniform index in a power-of-two range, using a fixed number of fair bits.

theorem Cslib.Probability.eval_sampleDyadicIndex (bound : ℕ) : (sampleDyadicIndex bound).eval = PMF.map Fin.val (PMF.uniformOfFintype (Fin (dyadicSize bound)))

The dyadic sampler has no rejection or approximation error.

theorem Cslib.Probability.eval_bind_sampleDyadicIndex_guard {α β : Type} (source : ProbComp α) (bound : ℕ) (test : ℕ → α → ProbComp β) (fallback : β) : (do let value ← source let index ← sampleDyadicIndex bound if index < bound then test index value else pure fallback).eval = do let i ← PMF.uniformOfFintype (Fin (dyadicSize bound)) if ↑i < bound then (do let value ← source test (↑i) value).eval else PMF.pure fallback

Move an independent source inside a uniform index choice, with a fixed fallback for padding indices. This exposes the finite average used by random-coordinate reductions.

noncomputable def Cslib.Probability.sampleDyadicCoin (bound numerator : ℕ) : ProbComp Bool

An exact dyadic coin, saturated at probability one when the numerator exceeds the range.

theorem Cslib.Probability.eval_sampleDyadicCoin_true (bound numerator : ℕ) : (sampleDyadicCoin bound numerator).eval true = ↑(min (dyadicSize bound) numerator) / ↑(dyadicSize bound)

The dyadic coin's exact acceptance probability, including the endpoints zero and one.

theorem Cslib.Probability.eval_sampleDyadicCoin_true_toReal (bound numerator : ℕ) : ((sampleDyadicCoin bound numerator).eval true).toReal = ↑(min (dyadicSize bound) numerator) / ↑(dyadicSize bound)

The real-valued acceptance probability of the exact dyadic sampler.

theorem Cslib.Probability.inv_dyadicSize_le_eval_sampleDyadicCoin (bound numerator : ℕ) (hpositive : 0 < ((sampleDyadicCoin bound numerator).eval true).toReal) : 1 / ↑(dyadicSize bound) ≤ ((sampleDyadicCoin bound numerator).eval true).toReal

Every positive dyadic acceptance probability is at least one over its sampling range.

noncomputable def Cslib.Probability.sampleBoundedIndex (bound : ℕ) : ProbComp ℕ

A capped fair-bit index, with bound denoting rejection.

theorem Cslib.Probability.eval_sampleBoundedIndex (bound : ℕ) : (sampleBoundedIndex bound).eval = PMF.map (fun (i : Fin (2 ^ (Nat.log 2 bound + 1))) => min bound ↑i) (PMF.uniformOfFintype (Fin (2 ^ (Nat.log 2 bound + 1))))

The sampler's exact distribution, including its rejection mass.