Finite-attempt uniform interval and integer-box sampling

Draw a fixed number of capped fair-bit samples and retain the first valid index. Exhaustion is an explicit none, never an unbounded retry. Conditioned on success the result is uniform; the unconditional law retains its failure mass. Bounds and all attempt/coordinate counts are runtime inputs. The strict PPT implementation uses unary resource parameters.

At a positive interval bound, let p = (dyadicSize bound - bound) / dyadicSize bound. The exact failure mass is p ^ attempts; every valid index has mass (1 - p ^ attempts) / bound. The box success mass is (1 - p ^ attempts) ^ dimension, with bound = 2 * radius + 1, and every Boolean test has unconditional error at most dimension * (1 / 2) ^ attempts. No conditioning is part of the sampled program.

An empty interval always fails. Zero dimension returns some [] without drawing even when attempts is zero; radius zero is a singleton reference box but can still suffer retry failure. These samplers are only a foundation for cryptographic realizations: a simulator's full transcript/error and an extractor's implementation require separate proofs.

Main definitions

• Cslib.Probability.sampleUniformInterval: bounded retry with an explicit failure result.
• Cslib.Probability.intervalFailure, Cslib.Probability.intervalSuccess: exact event masses.
• Cslib.Probability.sampleIntegerBox: coordinatewise finite-attempt integer-box sampling.
• Cslib.Probability.integerBoxLaw: the exact mathematical uniform reference law.

Main results

• Cslib.Probability.eval_sampleUniformInterval_none, Cslib.Probability.eval_sampleUniformInterval_some_toReal: the full interval law.
• Cslib.Probability.sampleUniformInterval_conditional: conditional uniformity at observable success events.
• Cslib.Probability.sampleUniformInterval_test_error_le: unconditional interval error, including the binary-bound implementation.
• Cslib.Probability.eval_sampleIntegerBox_some, Cslib.Probability.eval_sampleIntegerBox_none: the full joint success/failure law.
• Cslib.Probability.sampleIntegerBox_test_error_le: explicit unconditional statistical error.
• Cslib.Probability.sampleIntegerBox_support: exact output dimension and integer bounds.

noncomputable def Cslib.Probability.intervalFailure (bound : ℕ) : NNReal

The probability that one capped draw is rejected. At bound zero every draw is rejected.

noncomputable def Cslib.Probability.sampleUniformInterval (bound attempts : ℕ) : ProbComp (Option ℕ)

Draw all attempts capped samples, then return their first index strictly below bound. Zero attempts and bound zero return none.

@[simp]

theorem Cslib.Probability.sampleUniformInterval_zero (bound : ℕ) : sampleUniformInterval bound 0 = pure none

With no attempts, exhaustion is immediate.

theorem Cslib.Probability.sampleBoundedIndex_eq_binary (bound : ℕ) : sampleBoundedIndex bound = (fun (x : ℕ) => min bound x) <$> sampleBinaryNat (Nat.log 2 bound + 1)

The capped sampler is also a binary natural sampler followed by binary capping. This identity permits a binary implementation without writing the numerical bound in unary.

theorem Cslib.Probability.eval_sampleBoundedIndex_lt (bound value : ℕ) (hvalue : value < bound) : (sampleBoundedIndex bound).eval value = (↑(dyadicSize bound))⁻¹

A capped draw has equal mass at each valid index.

theorem Cslib.Probability.eval_sampleBoundedIndex_sentinel (bound : ℕ) : (sampleBoundedIndex bound).eval bound = ↑(intervalFailure bound)

All the excess dyadic mass is the rejection sentinel.

theorem Cslib.Probability.eval_sampleUniformInterval_succ (bound attempts : ℕ) : (sampleUniformInterval bound (attempts + 1)).eval = (sampleBoundedIndex bound).eval.bind fun (value : ℕ) => if value < bound then PMF.pure (some value) else (sampleUniformInterval bound attempts).eval

The retry law, including the remaining failure event. All unused draws are integrated out.

theorem Cslib.Probability.le_bound_of_mem_support_sampleBoundedIndex {bound value : ℕ} (h : value ∈ (sampleBoundedIndex bound).eval.support) : value ≤ bound

A capped draw is never above its sentinel.

theorem Cslib.Probability.eval_sampleUniformInterval_none (bound attempts : ℕ) : (sampleUniformInterval bound attempts).eval none = ↑(intervalFailure bound) ^ attempts

The exact exhaustion probability after a finite number of attempts.

theorem Cslib.Probability.eval_sampleUniformInterval_some (bound attempts value : ℕ) : (sampleUniformInterval bound attempts).eval (some value) = if value < bound then (∑ j ∈ Finset.range attempts, ↑(intervalFailure bound) ^ j) / ↑(dyadicSize bound) else 0

Every valid index has the same geometric-series mass; invalid indices have zero mass.

theorem Cslib.Probability.intervalFailure_le_half {bound : ℕ} (hbound : 0 < bound) : intervalFailure bound ≤ 1 / 2

Positive bounds accept with probability at least one half on each attempt.

theorem Cslib.Probability.eval_sampleUniformInterval_none_le {bound : ℕ} (hbound : 0 < bound) (attempts : ℕ) : (sampleUniformInterval bound attempts).eval none ≤ (1 / 2) ^ attempts

Exhaustion is exponentially unlikely at a positive bound; zero remains a separate case.

theorem Cslib.Probability.eval_sampleUniformInterval_some_toReal {bound : ℕ} (hbound : 0 < bound) (attempts value : ℕ) : ((sampleUniformInterval bound attempts).eval (some value)).toReal = if value < bound then (1 - ↑(intervalFailure bound) ^ attempts) / ↑bound else 0

A real-valued form of the complete success law, with no conditioning away of failure.

theorem Cslib.Probability.eval_sampleUniformInterval_success (bound attempts : ℕ) : ((PMF.map Option.isSome (sampleUniformInterval bound attempts).eval) true).toReal = 1 - ↑(intervalFailure bound) ^ attempts

The denominator used for conditioning is exactly the probability of success.

theorem Cslib.Probability.sampleUniformInterval_conditional {bound attempts value : ℕ} (hbound : 0 < bound) (hattempts : 0 < attempts) (hvalue : value < bound) : ((sampleUniformInterval bound attempts).eval (some value)).toReal / ((PMF.map Option.isSome (sampleUniformInterval bound attempts).eval) true).toReal = 1 / ↑bound

Conditioned on the observable success event, every valid interval value has probability 1 / bound. Positivity of the attempt budget and bound makes this conditioning meaningful.

noncomputable def Cslib.Probability.intervalSuccess (bound attempts : ℕ) : NNReal

Total mass retained by the finite-attempt sampler.

theorem Cslib.Probability.eval_sampleUniformInterval_some_eq (bound attempts value : ℕ) [NeZero bound] : (sampleUniformInterval bound attempts).eval (some value) = ↑(intervalSuccess bound attempts) * (PMF.map Fin.val (PMF.uniformOfFintype (Fin bound))) value

The successful part of the full sampler law is its success mass times exact uniformity.

def Cslib.Probability.collectBox (values : List (Option ℤ)) : Option (List ℤ)

Gather successful coordinates, preserving the entire failure event.

theorem Cslib.Probability.collectBox_cons (value : Option ℤ) (values : List (Option ℤ)) : collectBox (value :: values) = do let z ← value let rest ← collectBox values pure (z :: rest)

Gathering coordinates agrees with ordinary option sequencing.

theorem Cslib.Probability.collectBox_eq_some (values : List (Option ℤ)) (out : List ℤ) : collectBox values = some out ↔ values = List.map some out

Successful gathering preserves every coordinate and cannot hide a failed coordinate.

noncomputable def Cslib.Probability.sampleIntegerBox (radius dimension attempts : ℕ) : ProbComp (Option (List ℤ))

Sample each coordinate of [-radius,radius]^dimension with its own finite attempt budget. The result is a list of exactly dimension integers on success. Radius is a unary resource in the strict PPT certificate; this definition makes no logarithmic-radius complexity claim.

@[simp]

theorem Cslib.Probability.sampleIntegerBox_zero_dimension (radius attempts : ℕ) : sampleIntegerBox radius 0 attempts = pure (some [])

An empty box has one point and needs no samples, even with no attempts.

noncomputable def Cslib.Probability.integerBoxLaw (radius dimension : ℕ) : PMF (List ℤ)

Reference uniform box law, represented as a list of independent uniform integer coordinates. This is a mathematical PMF, not an assertion of exact fair-bit realizability.

theorem Cslib.Probability.eval_sampleIntegerBox_some (radius dimension attempts : ℕ) (out : List ℤ) : (sampleIntegerBox radius dimension attempts).eval (some out) = ↑(intervalSuccess (2 * radius + 1) attempts) ^ dimension * (integerBoxLaw radius dimension) out

The full successful box law is the exact uniform box law scaled by the probability that all coordinate samplers succeed. It includes zero dimension and zero attempts.

theorem Cslib.Probability.eval_sampleIntegerBox_some_toReal (radius dimension attempts : ℕ) (out : List ℤ) : ((sampleIntegerBox radius dimension attempts).eval (some out)).toReal = (1 - ↑(intervalFailure (2 * radius + 1)) ^ attempts) ^ dimension * ((integerBoxLaw radius dimension) out).toReal

Real-valued joint success masses, using only the displayed retry-error parameters.

theorem Cslib.Probability.eval_sampleIntegerBox_none (radius dimension attempts : ℕ) : ((sampleIntegerBox radius dimension attempts).eval none).toReal = 1 - (1 - ↑(intervalFailure (2 * radius + 1)) ^ attempts) ^ dimension

The exact total box exhaustion probability. Failure is present in the joint law, rather than discarded by conditioning.

theorem Cslib.Probability.eval_sampleIntegerBox_none_le (radius dimension attempts : ℕ) : ((sampleIntegerBox radius dimension attempts).eval none).toReal ≤ ↑dimension * (1 / 2) ^ attempts

The unconditional failure error is at most the dimension times the per-coordinate dyadic retry error. In particular, dimension zero has zero error even when attempts is zero.

theorem Cslib.Probability.sampleIntegerBox_conditional (radius dimension attempts : ℕ) (hattempts : 0 < attempts) (out : List ℤ) : ((sampleIntegerBox radius dimension attempts).eval (some out)).toReal / ((PMF.map Option.isSome (sampleIntegerBox radius dimension attempts).eval) true).toReal = ((integerBoxLaw radius dimension) out).toReal

Given success, the box has exactly its uniform product law. A positive attempt budget makes that event observable; the empty box already has its separate exact no-draw law.

theorem Cslib.Probability.sampleIntegerBox_test_error (radius dimension attempts : ℕ) (test : Option (List ℤ) → Bool) : |((PMF.map test (sampleIntegerBox radius dimension attempts).eval) true).toReal - ((PMF.map (fun (out : List ℤ) => test (some out)) (integerBoxLaw radius dimension)) true).toReal| ≤ ((sampleIntegerBox radius dimension attempts).eval none).toReal

Any Boolean test changes acceptance probability by at most the explicit failure mass when compared with an exact uniform box. This is an unconditional statistical-error statement.

theorem Cslib.Probability.sampleUniformInterval_test_error_le (bound attempts : ℕ) [NeZero bound] (test : Option ℕ → Bool) : |((PMF.map test (sampleUniformInterval bound attempts).eval) true).toReal - ((PMF.map (fun (value : ℕ) => test (some value)) (PMF.map Fin.val (PMF.uniformOfFintype (Fin bound)))) true).toReal| ≤ (1 / 2) ^ attempts

For a positive interval, every Boolean test has unconditional error at most the dyadic retry-failure bound against exact uniformity. This applies to binary cryptographic bounds too; it neither discards failure nor asserts an exact non-dyadic fair-bit sampler.

theorem Cslib.Probability.sampleIntegerBox_test_error_le (radius dimension attempts : ℕ) (test : Option (List ℤ) → Bool) : |((PMF.map test (sampleIntegerBox radius dimension attempts).eval) true).toReal - ((PMF.map (fun (out : List ℤ) => test (some out)) (integerBoxLaw radius dimension)) true).toReal| ≤ ↑dimension * (1 / 2) ^ attempts

Explicit statistical error of the bounded box sampler for every Boolean test.

@[simp]

theorem Cslib.Probability.intervalFailure_zero : intervalFailure 0 = 1

The zero bound is an exact, total failure case.

@[simp]

theorem Cslib.Probability.eval_sampleUniformInterval_zero_bound (attempts : ℕ) : (sampleUniformInterval 0 attempts).eval = PMF.pure none

No attempt can produce a valid index for an empty interval.

theorem Cslib.Probability.integerBoxLaw_support {radius dimension : ℕ} {out : List ℤ} (h : out ∈ (integerBoxLaw radius dimension).support) : out.length = dimension ∧ ∀ z ∈ out, -↑radius ≤ z ∧ z ≤ ↑radius

Every supported reference output has the requested dimension and integer radius.

theorem Cslib.Probability.sampleIntegerBox_support {radius dimension attempts : ℕ} {out : List ℤ} (h : some out ∈ (sampleIntegerBox radius dimension attempts).eval.support) : out.length = dimension ∧ ∀ z ∈ out, -↑radius ≤ z ∧ z ≤ ↑radius

Every successful bounded sample lies in the intended integer box with the exact dimension.

theorem Cslib.Probability.integerBoxLaw_apply_index (radius dimension : ℕ) (v : Fin dimension → Fin (2 * radius + 1)) : (integerBoxLaw radius dimension) (List.ofFn fun (i : Fin dimension) => ↑↑(v i) - ↑radius) = (↑(2 * radius + 1))⁻¹ ^ dimension

Each indexed point of the reference integer box has the same product mass.