Certified fair-bit and word sampling

The finite-uniform Boolean program has a one-instruction machine realization. This primitive is independent of the input and is registered with fun_prop. Uniform words are sampled by one fixed scanner with a linear clock. A runtime sample length must itself be computed in unary, so the certificate includes the cost of writing the sampled word. Finite uniformity alone does not imply strict fair-coin PPT.

Main results

• Cslib.Probability.isPPTOn_uniform_bool: one fair bit is uniformly PPT.
• Cslib.Probability.isPPTOn_sampleList: uniform words from a unary count.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.sampleList: sample an efficiently computed length.

References

Adapted from Cslib/Computability/Probabilistic/Sampling.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the existing encodings and common machine.

theorem Cslib.Probability.isPPTOn_uniform_bool {α : Type} (input : α ↪ List Bool) : IsPPTOn input Turing.MultiTapeTM.encBool fun (x : α) => ProbComp.uniform Bool

Sampling one fair bit is strict PPT for every fixed input encoding.

theorem Cslib.Probability.isPPTOn_sampleList : IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits BitString.sampleList

Uniform words have one finite fair-coin implementation for all unary input lengths.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.sampleList {α : Type} {input : α ↪ List Bool} {count : α → ℕ} (hcount : ComputableTidilyInPolyTime count input encUnary) : Cslib.Probability.IsPPTOn input encBits fun (a : α) => Cslib.BitString.sampleList (count a)

Sample an efficiently computed number of independent fair bits, charging the count in unary.