Sampling centered binomial integers

The sampler subtracts the true counts of two independent blocks of η fair bits. Its result is an integer, before any reduction modulo a ciphertext modulus. Every integer between -η and η, including both endpoints, has positive probability. The law is invariant under negation. This is the scalar centered-binomial construction of NIST, Section 4.2.2, Algorithm 8, extended to every natural parameter.

The exact distribution is specified by its finite fair-bit experiment. No Gaussian equivalence or encryption-security property is asserted. Native runtime is certified separately.

Main definitions

• sampleCenteredBinomial: subtract two independently sampled Boolean counts.

Main results

• eval_sampleCenteredBinomial: the exact two-word distribution.
• eval_sampleCenteredBinomial_eq_map: the same law from one word of 2 * η bits.
• mem_support_sampleCenteredBinomial_iff: support is exactly the closed integer interval.
• map_neg_eval_sampleCenteredBinomial: negation preserves the distribution.

References

• NIST, Module-Lattice-Based Key-Encapsulation Mechanism Standard, Section 4.2.2, Algorithm 8

noncomputable def Cslib.Probability.sampleCenteredBinomial (η : ℕ) : ProbComp ℤ

Subtract the true counts of two independent blocks of η fair bits.

@[simp]

theorem Cslib.Probability.sampleCenteredBinomial_zero : sampleCenteredBinomial 0 = pure 0

With η = 0 the centered binomial sampler returns 0 without sampling.

theorem Cslib.Probability.eval_sampleCenteredBinomial (η : ℕ) : (sampleCenteredBinomial η).eval = do let positive ← BitString.uniformList η let negative ← BitString.uniformList η pure (↑(List.count true positive) - ↑(List.count true negative))

The exact law is the difference of the true counts of two independent uniform words.

theorem Cslib.Probability.eval_sampleCenteredBinomial_eq_map (η : ℕ) : (sampleCenteredBinomial η).eval = PMF.map (fun (bits : List Bool) => ↑(List.count true (List.take η bits)) - ↑(List.count true (List.drop η bits))) (BitString.uniformList (2 * η))

One word of exactly 2 * η fair bits supplies the two independent counts.

theorem Cslib.Probability.mem_support_sampleCenteredBinomial_iff (η : ℕ) (z : ℤ) : z ∈ (sampleCenteredBinomial η).eval.support ↔ z.natAbs ≤ η

Every integer of magnitude at most η occurs, and no other integer does.

theorem Cslib.Probability.map_neg_eval_sampleCenteredBinomial (η : ℕ) : PMF.map Neg.neg (sampleCenteredBinomial η).eval = (sampleCenteredBinomial η).eval

Swapping the independent counts negates the result without changing its law.