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. Public sampler premises use plain deterministic certificates.

The scalar dyadic-size, logarithm, numeric-decoding and modulus helpers used in these proofs remain legacy-backed. The plain sampler interface does not establish their direct-machine internalization.

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.unary_dyadicSize: efficient unary range size.
• Cslib.Probability.isPPTOn_sampleBinaryNat: uniform sampling with binary output.
• Turing.MultiTapeTM.ComputableInPolyTime.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.ComputableInPolyTime.unary_dyadicSize : ComputableInPolyTime Cslib.Probability.dyadicSize encUnary encUnary

Compute the linearly capped dyadic range from a unary bound in plain polynomial time.

theorem Cslib.Probability.isPPTOn_sampleBinaryNat : IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat ProbComp.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.ComputableInPolyTime bound input Turing.MultiTapeTM.encUnary) : IsPPTOn input Turing.MultiTapeTM.encUnary fun (a : α) => ProbComp.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.ComputableInPolyTime bound input Turing.MultiTapeTM.encUnary) (hnumerator : Turing.MultiTapeTM.ComputableInPolyTime numerator input Turing.MultiTapeTM.encUnary) : IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => ProbComp.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.ComputableInPolyTime bound input Turing.MultiTapeTM.encUnary) : IsPPTOn input Turing.MultiTapeTM.encUnary fun (a : α) => ProbComp.sampleBoundedIndex (bound a)

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

theorem Turing.MultiTapeTM.ComputableInPolyTime.sampleBinaryNat {α : Type} {input : α ↪ List Bool} {width : α → ℕ} (hwidth : ComputableInPolyTime width input encUnary) : Cslib.Probability.IsPPTOn input encNat fun (a : α) => Cslib.ProbComp.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 : α) => ProbComp.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.