Strict fair-bit implementations of bounded sampling

Every attempt is sampled and stored before searching, and all coordinates and output framing are charged. The unary certificates charge the numerical bound, radius, dimension and attempt count. They do not imply polynomial dependence on the logarithm of a cryptographic modulus. Failure remains in the certified program's output.

Main results

• Cslib.Probability.isPPTOn_sampleUniformInterval: unary-bound interval sampling.
• Cslib.Probability.isPPTOn_sampleUniformInterval_binary: binary bounds with an efficient unary sampling width and attempt budget, including exponentially large interval bounds.
• Cslib.Probability.isPPTOn_sampleIntegerBox: unary-radius runtime-dimensional boxes.
• Cslib.Probability.length_enc_sampleIntegerBox: a bound for the complete framed output.

theorem Cslib.Probability.isPPTOn_sampleUniformInterval {α : Type} {input : α ↪ List Bool} {bound attempts : α → ℕ} (hbound : Turing.MultiTapeTM.ComputableInPolyTime bound input Turing.MultiTapeTM.encUnary) (hattempts : Turing.MultiTapeTM.ComputableInPolyTime attempts input Turing.MultiTapeTM.encUnary) : IsPPTOn input (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encUnary) fun (a : α) => sampleUniformInterval (bound a) (attempts a)

Unary bounds and attempt counts give a uniform strict PPT sampler, including its failure result and every stored attempt.

theorem Cslib.Probability.isPPTOn_sampleUniformInterval_binary {α : Type} {input : α ↪ List Bool} {bound width attempts : α → ℕ} (hbound : Turing.MultiTapeTM.ComputableInPolyTime bound input Turing.MultiTapeTM.encNat) (hwidth : Turing.MultiTapeTM.ComputableInPolyTime width input Turing.MultiTapeTM.encUnary) (hattempts : Turing.MultiTapeTM.ComputableInPolyTime attempts input Turing.MultiTapeTM.encUnary) (hwidth_eq : ∀ (a : α), width a = Nat.log 2 (bound a) + 1) : IsPPTOn input (Turing.MultiTapeTM.encOption Turing.MultiTapeTM.encNat) fun (a : α) => sampleUniformInterval (bound a) (attempts a)

Binary bounds need only a unary sampling width and attempt count. The width is the existing sampler's computed log₂ bound + 1, not a unary copy of bound; exponential cryptographic bounds are therefore permitted when these binary/unary parameter functions are efficient.

theorem Cslib.Probability.isPPTOn_sampleIntegerBox {α : Type} {input : α ↪ List Bool} {radius dimension attempts : α → ℕ} (hradius : Turing.MultiTapeTM.ComputableInPolyTime radius input Turing.MultiTapeTM.encUnary) (hdimension : Turing.MultiTapeTM.ComputableInPolyTime dimension input Turing.MultiTapeTM.encUnary) (hattempts : Turing.MultiTapeTM.ComputableInPolyTime attempts input Turing.MultiTapeTM.encUnary) : IsPPTOn input (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encInt)) fun (a : α) => sampleIntegerBox (radius a) (dimension a) (attempts a)

A runtime-varying integer box is sampled in uniform strict PPT when the numerical radius, dimension and per-coordinate attempt budget are efficiently supplied in unary. The full optional, framed list output and all attempted coordinates are charged.

theorem Cslib.Probability.length_enc_sampleIntegerBox {radius dimension attempts : ℕ} {result : Option (List ℤ)} (h : result ∈ (sampleIntegerBox radius dimension attempts).eval.support) : ((Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encInt)) result).length ≤ dimension * (2 * radius + 3) + 1

The complete framed optional output has a direct linear bound in dimension and unary radius; failure encodes as the empty word.