Sampling bounded indices in strict polynomial time

Each sampler uses a fixed number of fair bits. sampleBinaryNat takes a unary bit width and returns the sampled value in binary. The bounded-index samplers instead saturate binary decoding at a computed cap, so both their intermediate states and their unary outputs remain polynomially bounded. The dyadic range is at most 2 * (bound + 1), including zero. No unbounded rejection loop is used.

Main results

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_dyadicSize: efficient unary range size.
• Cslib.Probability.isPPTOn_sampleBinaryNat: uniform sampling with binary output.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.sampleBinaryNat: sample a computed bit width.
• Cslib.Probability.isPPTOn_sampleModNat: approximately uniform residues, for a computed bit width and modulus.
• Cslib.Probability.isPPTOn_sampleDyadicIndex: exact uniform sampling in the dyadic range.
• Cslib.Probability.isPPTOn_sampleBoundedIndex: capped sampling with a rejection sentinel.
• Cslib.Probability.isPPTOn_sampleDyadicCoin: exact capped dyadic probabilities.

References

Adapted from Computability/Probabilistic/UniformNat.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the tidy machine calculus and shared bit folds.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.unary_dyadicSize : ComputableTidilyInPolyTime Cslib.Probability.dyadicSize encUnary encUnary

Compute the dyadic range in unary via capped binary decoding. Its exponential expression does not authorize exponential output: the proved linear cap supplies the implementation.

theorem Cslib.Probability.isPPTOn_sampleBinaryNat : IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat sampleBinaryNat

A unary bit width gives a uniformly strict PPT sampler with binary natural output.

theorem Cslib.Probability.isPPTOn_sampleDyadicIndex {α : Type} {input : α ↪ List Bool} {bound : α → ℕ} (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) : IsPPTOn input Turing.MultiTapeTM.encUnary fun (a : α) => sampleDyadicIndex (bound a)

An efficiently supplied unary bound gives a strict PPT exact dyadic sampler.

theorem Cslib.Probability.isPPTOn_sampleDyadicCoin {α : Type} {input : α ↪ List Bool} {bound numerator : α → ℕ} (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) (hnumerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime numerator input Turing.MultiTapeTM.encUnary) : IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => sampleDyadicCoin (bound a) (numerator a)

Efficient unary parameters give a strict PPT coin with the specified dyadic law.

theorem Cslib.Probability.isPPTOn_sampleBoundedIndex {α : Type} {input : α ↪ List Bool} {bound : α → ℕ} (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) : IsPPTOn input Turing.MultiTapeTM.encUnary fun (a : α) => sampleBoundedIndex (bound a)

An efficiently supplied unary bound gives a strict PPT capped index sampler.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.sampleBinaryNat {α : Type} {input : α ↪ List Bool} {width : α → ℕ} (hwidth : ComputableTidilyInPolyTime width input encUnary) : Cslib.Probability.IsPPTOn input encNat fun (a : α) => Cslib.Probability.sampleBinaryNat (width a)

Sample a binary natural using an efficiently computed unary bit width.

theorem Cslib.Probability.isPPTOn_sampleModNat {α : Type} {input : α ↪ List Bool} {width modulus : α → ℕ} (hwidth : Turing.MultiTapeTM.ComputableInPolyTime width input Turing.MultiTapeTM.encUnary) (hmodulus : Turing.MultiTapeTM.ComputableInPolyTime modulus input Turing.MultiTapeTM.encNat) : IsPPTOn input Turing.MultiTapeTM.encNat fun (a : α) => sampleModNat (width a) (modulus a)

Approximately uniform residues: reducing a computed number of fair bits modulo a computed modulus is uniformly strict PPT, with binary output.