Bounded adaptive loops of clean oracle phases

A loop of clean phases is a clean phase when one invariant bounds the encoded size of every reachable state. Unlike closed loops, an adaptive loop with an external oracle cannot presample its randomness: every iteration may query the shared stateful oracle, and its replies may be arbitrarily long. The loop therefore runs the step machine itself, once per iteration, with a unary counter stored beside the state; the counter stops the loop after exactly the requested number of steps and the final round executes no step.

The invariant quantifies over every result possible for some stateful handler, so it holds for every shared oracle. Storage growth is controlled by the client's size bound, not assumed.

Main results

• Cslib.Probability.IsTidyOraclePPTOn.iterate_spec: certify a bounded loop and its final supported invariant.
• Cslib.Probability.IsTidyOraclePPTOn.iterateWith_spec: the step may capture the input.

References

Adapts Computability/Probabilistic/Adaptive.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to open oracles, running the probabilistic oracle version of the tidy iterateWhile loop instead of presampled coins.

theorem Cslib.Probability.IsTidyOraclePPTOn.iterate_spec {Operation α σ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {stateEncoding : σ ↪ List Bool} {initial : α → σ} {count : α → ℕ} {step : σ → WordOracleComp Operation σ} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hinitial : Turing.MultiTapeTM.ComputableTidilyInPolyTime initial input stateEncoding) (hstep : IsTidyOraclePPTOn stateEncoding stateEncoding step) (invariant : α → ℕ → σ → Prop) (hbase : ∀ (a : α), invariant a 0 (initial a)) (hpreserve : ∀ (a : α) (i : ℕ) (state : σ), i < count a → invariant a i state → ∀ next ∈ ProbOracleComp.support (step state), invariant a (i + 1) next) {size : α → ℕ} (hsize : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (input a).length) size) (hbound : ∀ (a : α) (i : ℕ) (state : σ), i ≤ count a → invariant a i state → (stateEncoding state).length ≤ size a) : (IsTidyOraclePPTOn input stateEncoding fun (a : α) => OracleComp.iterate (count a) step (initial a)) ∧ ∀ (a : α), ∀ state ∈ ProbOracleComp.support (OracleComp.iterate (count a) step (initial a)), invariant a (count a) state

A bounded loop of a clean step is clean when one invariant bounds every reachable state. The invariant holds for every possible result under every stateful oracle, and it is also established for the final state.

theorem Cslib.Probability.IsTidyOraclePPTOn.iterateWith_spec {Operation α σ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {stateEncoding : σ ↪ List Bool} {initial : α → σ} {count : α → ℕ} {step : α → σ → WordOracleComp Operation σ} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hinitial : Turing.MultiTapeTM.ComputableTidilyInPolyTime initial input stateEncoding) (hstep : IsTidyOraclePPTOn (Turing.MultiTapeTM.encPair input stateEncoding) stateEncoding fun (pair : α × σ) => step pair.1 pair.2) (invariant : α → ℕ → σ → Prop) (hbase : ∀ (a : α), invariant a 0 (initial a)) (hpreserve : ∀ (a : α) (i : ℕ) (state : σ), i < count a → invariant a i state → ∀ next ∈ ProbOracleComp.support (step a state), invariant a (i + 1) next) {size : α → ℕ} (hsize : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (input a).length) size) (hbound : ∀ (a : α) (i : ℕ) (state : σ), i ≤ count a → invariant a i state → (stateEncoding state).length ≤ size a) : (IsTidyOraclePPTOn input stateEncoding fun (a : α) => OracleComp.iterate (count a) (step a) (initial a)) ∧ ∀ (a : α), ∀ state ∈ ProbOracleComp.support (OracleComp.iterate (count a) (step a) (initial a)), invariant a (count a) state

The loop body may capture the original input. The joint step certificate charges for both that input and the changing state; the client invariant describes only the changing state.

theorem Cslib.Probability.IsTidyOraclePPTOn.iterateWith_of_bounded_growth {Operation α σ : Type} [DecidableEq Operation] {input : α ↪ List Bool} {stateEncoding : σ ↪ List Bool} {initial : α → σ} {count : α → ℕ} {step : α → σ → WordOracleComp Operation σ} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hinitial : Turing.MultiTapeTM.ComputableTidilyInPolyTime initial input stateEncoding) (hstep : IsTidyOraclePPTOn (Turing.MultiTapeTM.encPair input stateEncoding) stateEncoding fun (pair : α × σ) => step pair.1 pair.2) {growth : α → ℕ} (hpoly : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (input a).length) growth) (hgrowth : ∀ (a : α) (state next : σ), next ∈ ProbOracleComp.support (step a state) → (stateEncoding next).length ≤ (stateEncoding state).length + growth a) : IsTidyOraclePPTOn input stateEncoding fun (a : α) => OracleComp.iterate (count a) (step a) (initial a)

Captured-input steps may grow by a polynomially bounded amount depending on that input, for every possible next state under every stateful oracle.