Sampling bit strings one fair bit at a time

BitString.sampleList n is an ordinary recursive program drawing n independent Boolean values. Its distribution is the uniform law on lists of exactly that length. Computational efficiency is certified separately in Computability.Probabilistic.Sampling.

Main definitions

• Cslib.BitString.sampleList: sample a word using only fair Boolean choices.

Main results

• Cslib.BitString.eval_sampleList: agreement with the finite uniform distribution.
• Cslib.ProbComp.eval_bind_of_uniformList: concatenate fixed-length seeds for sequential runs.

References

Adapted from Cslib/Languages/Probabilistic/BitString.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the typed PFunctor.FreeM program interface.

noncomputable def Cslib.BitString.sampleList : ℕ → ProbComp (List Bool)

Sample n independent fair bits, returned in sampling order.

@[simp]

theorem Cslib.BitString.eval_sampleList (n : ℕ) : (sampleList n).eval = uniformList n

The operational fair-bit sampler has the finite uniform word distribution.

theorem Cslib.ProbComp.eval_bind_of_uniformList {α β : Type} (first second : ℕ) (program : ProbComp α) (next : α → ProbComp β) (evaluate : List Bool → α) (evaluateNext : α → List Bool → β) (hprogram : program.eval = PMF.map evaluate (BitString.uniformList first)) (hnext : ∀ (a : α), (next a).eval = PMF.map (evaluateNext a) (BitString.uniformList second)) : (do let a ← program next a).eval = PMF.map (fun (tape : List Bool) => evaluateNext (evaluate (List.take first tape)) (List.drop first tape)) (BitString.uniformList (first + second))

Two fixed-length fair-bit seeds concatenate, including when the second program depends on the first result. This is an exact distribution law, without an efficiency assertion.