Native centered binomial sampling

The actual two-count program has one strict fair-coin polynomial-time implementation for all unary parameters η. Its signed output uses the binary integer encoding. The certificate charges both blocks of independent trials, their counts, and signed subtraction.

Main results

• isPPTOn_sampleCenteredBinomial: the unary-input, binary-output sampler certificate.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.sampleCenteredBinomial: composition with an efficiently computed unary parameter.

References

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

theorem Cslib.Probability.isPPTOn_sampleCenteredBinomial : IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encIntBin sampleCenteredBinomial

The centered-binomial program is uniformly strict PPT, with a unary parameter and binary signed output. No fixed finite output type or finite-rank encoding is used.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.sampleCenteredBinomial {α : Type} {input : α ↪ List Bool} {parameter : α → ℕ} (hparameter : ComputableTidilyInPolyTime parameter input encUnary) : Cslib.Probability.IsPPTOn input encIntBin fun (a : α) => Cslib.Probability.sampleCenteredBinomial (parameter a)

Sample a centered-binomial integer using an efficiently computed unary parameter.