Strict PPT adaptive iteration

A bounded probabilistic loop is strict PPT when its step is strict PPT and one invariant bounds the encoded size of every reachable state. The same rule proves the final invariant. The step may capture the original input. Constant-growth and length-nonincreasing variants supply the size invariant automatically.

The efficiency proofs specialize the strict oracle iteration rules to empty external channels. Embedding a closed program preserves sampling and commutes with iteration; the shared oracle calculus supplies the clean realization and its polynomial clock. Support transport carries the client invariant to that realization. Clients supply ordinary programs and invariants, without machines, replay code or decoders.

Main results

• Cslib.Probability.IsPPTOn.iterate_spec: certify efficiency and the final supported invariant.
• Cslib.Probability.IsPPTOn.iterateWith_spec: allow the step to capture the original input.
• Cslib.Probability.IsPPTOn.iterateWith_of_bounded_growth: infer accumulated size from input-dependent growth of the full state.
• Cslib.Probability.IsPPTOn.iterate_of_bounded_growth, .iterate_of_length_le: automatic intermediate-size bounds.

References

Adapted from Computability/Probabilistic/Adaptive.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, reusing the tidy fold calculus.

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

One invariant proves both a polynomial resource bound and the final supported postcondition. The resource invariant must hold on every possible execution, not just with high probability. The bound may depend on the original input and need not be computable: the proof chooses one computable polynomial majorant for the compiled loop clock.

theorem Cslib.Probability.IsPPTOn.iterateWith_spec {α State : Type} {input : α ↪ List Bool} {stateEncoding : State ↪ List Bool} {initial : α → State} {count : α → ℕ} {step : α → State → ProbComp State} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hinitial : Turing.MultiTapeTM.ComputableTidilyInPolyTime initial input stateEncoding) (hstep : IsPPTOn (Turing.MultiTapeTM.encPair input stateEncoding) stateEncoding fun (pair : α × State) => step pair.1 pair.2) (invariant : α → ℕ → State → Prop) (hbase : ∀ (a : α), invariant a 0 (initial a)) (hpreserve : ∀ (a : α) (i : ℕ) (state : State), i < count a → invariant a i state → ∀ next ∈ (step a state).eval.support, invariant a (i + 1) next) {size : α → ℕ} (hsize : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (input a).length) size) (hbound : ∀ (a : α) (i : ℕ) (state : State), i ≤ count a → invariant a i state → (stateEncoding state).length ≤ size a) : (IsPPTOn input stateEncoding fun (a : α) => OracleComp.iterate (count a) (step a) (initial a)) ∧ ∀ (a : α), ∀ state ∈ (ProbComp.eval (OracleComp.iterate (count a) (step a) (initial a))).support, 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.IsPPTOn.iterateWith_of_bounded_growth {α State : Type} {input : α ↪ List Bool} {stateEncoding : State ↪ List Bool} {initial : α → State} {count : α → ℕ} {step : α → State → ProbComp State} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hinitial : Turing.MultiTapeTM.ComputableTidilyInPolyTime initial input stateEncoding) (hstep : IsPPTOn (Turing.MultiTapeTM.encPair input stateEncoding) stateEncoding fun (pair : α × State) => step pair.1 pair.2) {growth : α → ℕ} (hpoly : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (input a).length) growth) (hgrowth : ∀ (a : α) (state next : State), next ∈ (step a state).eval.support → (stateEncoding next).length ≤ (stateEncoding state).length + growth a) : IsPPTOn 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. The joint step certificate charges the captured input, and the growth bound covers every supported next state from every current state.

theorem Cslib.Probability.IsPPTOn.iterate_of_bounded_growth {α State : Type} {input : α ↪ List Bool} {stateEncoding : State ↪ List Bool} {initial : α → State} {count : α → ℕ} {step : State → ProbComp State} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hinitial : Turing.MultiTapeTM.ComputableTidilyInPolyTime initial input stateEncoding) (hstep : IsPPTOn stateEncoding stateEncoding step) {growth : ℕ} (hgrowth : ∀ (state next : State), next ∈ (step state).eval.support → (stateEncoding next).length ≤ (stateEncoding state).length + growth) : IsPPTOn input stateEncoding fun (a : α) => OracleComp.iterate (count a) step (initial a)

A strict PPT step with constant growth can be repeated a polynomial number of times.

theorem Cslib.Probability.IsPPTOn.iterate_of_length_le {α State : Type} {input : α ↪ List Bool} {stateEncoding : State ↪ List Bool} {initial : α → State} {count : α → ℕ} {step : State → ProbComp State} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hinitial : Turing.MultiTapeTM.ComputableTidilyInPolyTime initial input stateEncoding) (hstep : IsPPTOn stateEncoding stateEncoding step) (hshrink : ∀ (state next : State), next ∈ (step state).eval.support → (stateEncoding next).length ≤ (stateEncoding state).length) : IsPPTOn input stateEncoding fun (a : α) => OracleComp.iterate (count a) step (initial a)

Iteration of a step that never increases its encoded state needs no extra size invariant.