Bounded adaptive probabilistic iteration

OracleComp.iterate count step initial repeats a state-dependent program a bounded number of times. Its invariant rule reasons only about supported transitions. A common finite seed realizing each reachable step presents the complete loop as a deterministic fold over independent uniform seeds. State types need not be finite. These are semantic laws; efficiency is separate.

Main definitions

• Cslib.OracleComp.iterate: bounded iteration of a state-dependent program.

Main results

• Cslib.OracleComp.iterate_map: a representation commuting with each step commutes with the loop.
• Cslib.OracleComp.run_interpret_iterate: stateful interpretation threads one shared hidden state through the loop.
• Cslib.OracleComp.interpret_iterate: replacing every call by a program iterates the replaced steps.
• Cslib.ProbComp.iterate_invariant: supported transitions preserve the final invariant.
• Cslib.ProbComp.iterate_failure_le, iterate_failure_toReal_le_mul: local failure bounds accumulate additively across adaptive rounds.
• Cslib.ProbComp.eval_iterate_of_uniform: exact evaluation from independent saved seeds.

References

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

def Cslib.OracleComp.iterate {ι : Type u} {spec : OracleSpec ι} {State : Type v} : ℕ → (State → OracleComp spec State) → State → OracleComp spec State

Repeat a state-dependent program a bounded number of times.

@[simp]

theorem Cslib.OracleComp.iterate_zero {ι : Type u} {spec : OracleSpec ι} {State : Type v} (step : State → OracleComp spec State) (initial : State) : iterate 0 step initial = pure initial

Zero iterations return the initial state.

theorem Cslib.OracleComp.iterate_succ {ι : Type u} {spec : OracleSpec ι} {State : Type v} (count : ℕ) (step : State → OracleComp spec State) (initial : State) : iterate (count + 1) step initial = iterate count step initial >>= step

count + 1 iterations run count iterations, then one more step.

theorem Cslib.OracleComp.iterate_succ_bind {ι : Type u} {spec : OracleSpec ι} {State : Type v} (count : ℕ) (step : State → OracleComp spec State) (initial : State) : iterate (count + 1) step initial = step initial >>= iterate count step

A bounded loop may expose its first transition as well as its last.

theorem Cslib.OracleComp.iterate_eq_pure {ι : Type u} {spec : OracleSpec ι} {State : Type v} (count : ℕ) (step : State → OracleComp spec State) (initial : State) (h : step initial = pure initial) : iterate count step initial = pure initial

Repeating a step that leaves the initial state unchanged has no effects.

theorem Cslib.OracleComp.iterate_map {ι : Type u} {spec : OracleSpec ι} {State Other : Type v} (count : ℕ) (step : State → OracleComp spec State) (next : Other → OracleComp spec Other) (f : State → Other) (hstep : ∀ (state : State), next (f state) = f <$> step state) (initial : State) : iterate count next (f initial) = f <$> iterate count step initial

A state representation commuting with one step commutes with the complete loop.

theorem Cslib.OracleComp.interpret_iterate {ι : Type u} {spec : OracleSpec ι} {State : Type v} {κ : Type w} {target : OracleSpec κ} (handler : (q : ι) → OracleComp target (spec q)) (count : ℕ) (step : State → OracleComp spec State) (initial : State) : interpret handler (iterate count step initial) = iterate count (fun (state : State) => interpret handler (step state)) initial

Replacing every call of a loop by a program over another interface iterates the replaced steps.

theorem Cslib.OracleComp.run_interpret_iterate {ι : Type u} {spec : OracleSpec ι} {State Hidden : Type v} {κ : Type w} {target : OracleSpec κ} (handler : (q : ι) → StateT Hidden (OracleComp target) (spec q)) (count : ℕ) (step : State → OracleComp spec State) (initial : State) (hidden : Hidden) : (interpret handler (iterate count step initial)).run hidden = iterate count (fun (pair : State × Hidden) => (interpret handler (step pair.1)).run pair.2) (initial, hidden)

Interpreting a loop with a stateful handler is a loop on the joint program and handler state. The hidden state is retained between iterations, including effects of the last transition.

theorem Cslib.ProbComp.iterate_invariant {State : Type} (count : ℕ) (step : State → ProbComp State) (initial : State) (invariant : ℕ → State → Prop) (hinit : invariant 0 initial) (hpreserve : ∀ i < count, ∀ (state : State), invariant i state → ∀ next ∈ (step state).eval.support, invariant (i + 1) next) (state : State) : state ∈ (eval (OracleComp.iterate count step initial)).support → invariant count state

Every possible final state satisfies an invariant preserved by every supported transition.

theorem Cslib.ProbComp.iterate_failure_le {State : Type} (count : ℕ) (step : State → ProbComp State) (initial : State) (invariant : ℕ → State → Prop) (hinit : invariant 0 initial) (error : ℕ → ENNReal) (hstep : ∀ i < count, ∀ (state : State), invariant i state → (step state).eval.toOuterMeasure {next : State | ¬invariant (i + 1) next} ≤ error i) : (eval (OracleComp.iterate count step initial)).toOuterMeasure {state : State | ¬invariant count state} ≤ ∑ i ∈ Finset.range count, error i

Per-step failures of an invariant accumulate additively across an adaptive loop. The local bound is needed only at states where the preceding invariant holds.

theorem Cslib.ProbComp.iterate_failure_toReal_le {State : Type} (count : ℕ) (step : State → ProbComp State) (initial : State) (invariant : ℕ → State → Prop) (hinit : invariant 0 initial) (error : ℕ → ℝ) (herror : ∀ i < count, 0 ≤ error i) (hstep : ∀ i < count, ∀ (state : State), invariant i state → ((step state).eval.toOuterMeasure {next : State | ¬invariant (i + 1) next}).toReal ≤ error i) : ((eval (OracleComp.iterate count step initial)).toOuterMeasure {state : State | ¬invariant count state}).toReal ≤ ∑ i ∈ Finset.range count, error i

The real-valued form of the adaptive error rule.

theorem Cslib.ProbComp.iterate_failure_toReal_le_mul {State : Type} (count : ℕ) (step : State → ProbComp State) (initial : State) (invariant : ℕ → State → Prop) (hinit : invariant 0 initial) {error : ℝ} (herror : 0 ≤ error) (hstep : ∀ i < count, ∀ (state : State), invariant i state → ((step state).eval.toOuterMeasure {next : State | ¬invariant (i + 1) next}).toReal ≤ error) : ((eval (OracleComp.iterate count step initial)).toOuterMeasure {state : State | ¬invariant count state}).toReal ≤ ↑count * error

A uniform per-round error ε gives total error at most count * ε, including adaptive rounds and state spaces that are not finite.

theorem Cslib.ProbComp.eval_iterate_of_uniform {State Seed : Type} [Fintype Seed] [Nonempty Seed] (count : ℕ) (step : State → ProbComp State) (initial : State) (evaluate : State → Seed → State) (invariant : ℕ → State → Prop) (hinit : invariant 0 initial) (hpreserve : ∀ i < count, ∀ (state : State), invariant i state → ∀ next ∈ (step state).eval.support, invariant (i + 1) next) (hlaw : ∀ i < count, ∀ (state : State), invariant i state → (step state).eval = PMF.map (evaluate state) (Probability.PMF.uniformOfFintype Seed)) : eval (OracleComp.iterate count step initial) = PMF.map (fun (seeds : Fin count → Seed) => List.foldl evaluate initial (List.ofFn seeds)) (Probability.PMF.uniformOfFintype (Fin count → Seed))

Independent uniform seeds realize an adaptive loop when they realize each reachable step. The invariant allows the realization law to be restricted to reachable states.