Bounded repetition of probabilistic programs

OracleComp.replicate collects the results of an ordinary List.mapM traversal in execution order. Closed runs draw independent samples, even when the output type is infinite. Efficiency is certified separately in Computability.Probabilistic.Repeat.

Main definitions

• Cslib.OracleComp.replicate: collect a bounded number of runs.
• Cslib.OracleComp.countTrue, .testProbabilityLT: count successes and test rational thresholds.

Main results

• Cslib.OracleComp.replicate_add, .replicate_snoc: split an execution into segments.
• Cslib.ProbComp.eval_replicate: finite outputs have the independent product law.
• Cslib.ProbComp.eval_replicate_iid: the independent law on arbitrary output types.
• Cslib.ProbComp.eval_replicate_map: transport a sampling law through repeated draws.
• Cslib.ProbComp.eval_replicate_splice: draw one coordinate first without changing the joint law.
• Cslib.ProbComp.eval_countTrue: the success count is a sum of independent indicators.
• Cslib.ProbComp.countTrue_le: every supported success count respects the trial budget.
• Cslib.ProbComp.eval_replicate_of_uniform: realize the joint law from independent finite seeds.
• Cslib.ProbComp.eval_replicate_of_uniformList: collect independent draws from one flat bit list.

References

Adapted from Languages/Probabilistic/Repeat.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the existing typed program interface and list traversal.

def Cslib.OracleComp.replicate {Query : Type u} {spec : OracleSpec Query} {α : Type v} (count : ℕ) (program : OracleComp spec α) : OracleComp spec (List α)

Collect the results of a bounded number of runs in execution order.

@[simp]

theorem Cslib.OracleComp.replicate_zero {Query : Type u} {spec : OracleSpec Query} {α : Type v} (program : OracleComp spec α) : replicate 0 program = pure []

Zero runs return the empty list.

theorem Cslib.OracleComp.replicate_succ {Query : Type u} {spec : OracleSpec Query} {α : Type v} (count : ℕ) (program : OracleComp spec α) : replicate (count + 1) program = do let first ← program List.cons first <$> replicate count program

count + 1 runs make one run, then count more, and list its result first.

theorem Cslib.OracleComp.replicate_add {Query : Type u} {spec : OracleSpec Query} {α : Type v} (first second : ℕ) (program : OracleComp spec α) : replicate (first + second) program = do let front ← replicate first program let back ← replicate second program pure (front ++ back)

Split repeated runs into two consecutive segments.

theorem Cslib.OracleComp.replicate_snoc {Query : Type u} {spec : OracleSpec Query} {α : Type v} (count : ℕ) (program : OracleComp spec α) : replicate (count + 1) program = do let front ← replicate count program (fun (last : α) => front ++ [last]) <$> program

Split off the last draw of a repeated program.

theorem Cslib.OracleComp.replicate_map {Query : Type u} {spec : OracleSpec Query} {α β : Type v} (count : ℕ) (program : OracleComp spec α) (f : α → β) : replicate count (f <$> program) = List.map f <$> replicate count program

Deterministic postprocessing commutes with collecting the draws.

def Cslib.OracleComp.countTrue {Query : Type u} {spec : OracleSpec Query} (count : ℕ) (program : OracleComp spec Bool) : OracleComp spec ℕ

Count the true results of a bounded number of runs of a Boolean program.

def Cslib.OracleComp.testProbabilityLT {Query : Type u} {spec : OracleSpec Query} (count numerator denominator : ℕ) (program : OracleComp spec Bool) : OracleComp spec Bool

Compare an empirical acceptance rate with a rational threshold by natural cross-products. Accuracy theorems require a positive count and denominator; the program is total at zero.

theorem Cslib.ProbComp.mem_support_replicate_iff {α : Type} (count : ℕ) (program : ProbComp α) (values : List α) : values ∈ (eval (OracleComp.replicate count program)).support ↔ values.length = count ∧ ∀ value ∈ values, value ∈ program.eval.support

A supported collected result has the prescribed length and supported entries.

theorem Cslib.ProbComp.eval_replicate_congr {α : Type} {first second : ProbComp α} (h : first.eval = second.eval) (count : ℕ) : eval (OracleComp.replicate count first) = eval (OracleComp.replicate count second)

Repetition preserves equality of closed-program distributions, including infinite outputs.

theorem Cslib.ProbComp.eval_replicate_splice {α : Type} (source : ProbComp α) (before after : ℕ) : (do let middle ← source let front ← OracleComp.replicate before source let back ← OracleComp.replicate after source pure (front ++ middle :: back)).eval = eval (OracleComp.replicate (before + (after + 1)) source)

Draw one designated coordinate first, then insert it between independent prefix and suffix draws. This preserves the complete joint law, including repeated sample values.

theorem Cslib.ProbComp.eval_replicate_map {α β : Type} {source : ProbComp α} {encoded : ProbComp β} {encode : α → β} (h : encoded.eval = PMF.map encode source.eval) (count : ℕ) : eval (OracleComp.replicate count encoded) = PMF.map (List.map encode) (eval (OracleComp.replicate count source))

An encoded sampling law lifts to repeated draws without requiring either type to be finite or the encoding to be injective. The order and multiplicity of all draws are preserved.

theorem Cslib.ProbComp.eval_replicate_iid {α : Type} (count : ℕ) (program : ProbComp α) : eval (OracleComp.replicate count program) = PMF.map List.ofFn (Probability.PMF.iid program.eval count)

Independent repetition on arbitrary output types, including integers and failure options. Unlike the finite-product specialization, this law needs no finiteness assumption.

theorem Cslib.ProbComp.eval_replicate {α : Type} [Finite α] (count : ℕ) (program : ProbComp α) : eval (OracleComp.replicate count program) = PMF.map List.ofFn (Probability.PMF.pi fun (x : Fin count) => program.eval)

Repeated closed runs have the independent product law for any finite output distribution.

theorem Cslib.ProbComp.eval_countTrue (count : ℕ) (program : ProbComp Bool) : eval (OracleComp.countTrue count program) = PMF.map (fun (bits : Fin count → Bool) => ∑ i : Fin count, (bits i).toNat) (Probability.PMF.pi fun (x : Fin count) => program.eval)

Counting successful repeated trials is the sum of independent Boolean indicators.

theorem Cslib.ProbComp.countTrue_le (count : ℕ) (program : ProbComp Bool) {successes : ℕ} (h : successes ∈ (eval (OracleComp.countTrue count program)).support) : successes ≤ count

Every supported result is bounded by the number of trials, including zero trials.

theorem Cslib.ProbComp.eval_replicate_of_uniform {α Seed : Type} [Fintype Seed] [Nonempty Seed] (count : ℕ) (program : ProbComp α) (evaluate : Seed → α) (hlaw : program.eval = PMF.map evaluate (Probability.PMF.uniformOfFintype Seed)) : eval (OracleComp.replicate count program) = PMF.map (fun (seeds : Fin count → Seed) => List.ofFn fun (i : Fin count) => evaluate (seeds i)) (Probability.PMF.uniformOfFintype (Fin count → Seed))

Repeated closed runs use independent uniform seeds, including at count zero. The output type need not be finite.

theorem Cslib.ProbComp.eval_replicate_of_uniformList {α : Type} (count width : ℕ) (program : ProbComp α) (evaluate : List Bool → α) (hlaw : program.eval = PMF.map evaluate (BitString.uniformList width)) : eval (OracleComp.replicate count program) = PMF.map (fun (tape : List Bool) => List.map evaluate (BitString.listRows count width tape)) (BitString.uniformList (count * width))

One flat uniform bit list supplies independent seeds for every repeated run, including zero repetitions and zero-width seeds.