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.
• Cslib.Probability.IsPPTOn.of_seeded: running a polynomial-time function on an input and an efficiently computed number of sampled fair bits is uniformly PPT.
• Turing.MultiTapeTM.ComputableInPolyTime.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 Cslib.Probability.IsPPTOn.of_seeded {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {count : α → ℕ} {f : α × List Bool → β} (hcount : Turing.MultiTapeTM.ComputableInPolyTime count input Turing.MultiTapeTM.encUnary) (hf : Turing.MultiTapeTM.ComputableInPolyTime f (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) output) : IsPPTOn input output fun (a : α) => (fun (w : List Bool) => f (a, w)) <$> BitString.sampleList (count a)

Running a deterministic polynomial-time function on the input paired with an efficiently computed unary count of independent fair bits is a uniform strict PPT program.

theorem Turing.MultiTapeTM.ComputableInPolyTime.sampleList {α : Type} {input : α ↪ List Bool} {count : α → ℕ} (hcount : ComputableInPolyTime 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.