Polynomial-time iteration with invariants

The loop count is computed in unary, so its value is polynomially bounded in the encoded input. The caller certifies the step and bounds the encoded intermediate states. The captured-parameter rules are the plain rules of Turing.MultiTapeTM.ComputableInPolyTime (in Internal.PolyTimeLoops) with tidied conclusions. The specification interface is adapted from IsPolyTime.iterate_spec in the cslib crypto branch.

Main results

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.iterate: iteration with a size bound.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.iterateWith: the same bound with captured data.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.iterate_spec: a loop invariant gives both polynomial-time computation and the final postcondition.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.iterateWith_spec: capture a computed parameter while retaining a uniform joint certificate for the step.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.iterate_of_bounded_growth: constant additive state growth discharges intermediate-size obligations.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.iterateWith_of_bounded_growth: captured loops with a polynomial per-step growth bound depending on the original input.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.iterateWithInput_of_bounded_growth: the same growth contract with the original input captured directly, for certificate inference.

References

Adapted from Computability/Probabilistic/Iteration.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.iterateWith {α β : Type} {encIn : α ↪ List Bool} {encState : β ↪ List Bool} {π : Type} {encPar : π ↪ List Bool} {par : α → π} {count : α → ℕ} {init : α → β} {step : π → β → β} (hpar : ComputableTidilyInPolyTime par encIn encPar) (hcount : ComputableTidilyInPolyTime count encIn encUnary) (hinit : ComputableTidilyInPolyTime init encIn encState) (hstep : ComputableTidilyInPolyTime (fun (p : π × β) => step p.1 p.2) (encPair encPar encState) encState) {bound : α → ℕ} (hbound : PolyBounded (fun (x : α) => (encIn x).length) bound) (hstates : ∀ (x : α), ∀ i ≤ count x, (encState ((step (par x))^[i] (init x))).length ≤ bound x) : ComputableTidilyInPolyTime (fun (x : α) => (step (par x))^[count x] (init x)) encIn encState

Capture a computed parameter while bounding every intermediate loop state.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.iterate {α β : Type} {encIn : α ↪ List Bool} {encState : β ↪ List Bool} {count : α → ℕ} {init : α → β} {step : β → β} (hcount : ComputableTidilyInPolyTime count encIn encUnary) (hinit : ComputableTidilyInPolyTime init encIn encState) (hstep : ComputableTidilyInPolyTime step encState encState) {bound : α → ℕ} (hbound : PolyBounded (fun (x : α) => (encIn x).length) bound) (hstates : ∀ (x : α), ∀ i ≤ count x, (encState (step^[i] (init x))).length ≤ bound x) : ComputableTidilyInPolyTime (fun (x : α) => step^[count x] (init x)) encIn encState

A unary loop count and polynomially bounded intermediate states give a polynomial-time loop.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.iterateWith_spec {α β : Type} {encIn : α ↪ List Bool} {encState : β ↪ List Bool} {π : Type} {encPar : π ↪ List Bool} {par : α → π} {count : α → ℕ} {init : α → β} {step : π → β → β} (hpar : ComputableTidilyInPolyTime par encIn encPar) (hcount : ComputableTidilyInPolyTime count encIn encUnary) (hinit : ComputableTidilyInPolyTime init encIn encState) (hstep : ComputableTidilyInPolyTime (fun (p : π × β) => step p.1 p.2) (encPair encPar encState) encState) (invariant : α → ℕ → β → Prop) (hbase : ∀ (x : α), invariant x 0 (init x)) (hpreserve : ∀ (x : α) (i : ℕ) (state : β), i < count x → invariant x i state → invariant x (i + 1) (step (par x) state)) {size : α → ℕ} (hsize : PolyBounded (fun (x : α) => (encIn x).length) size) (hbound : ∀ (x : α) (i : ℕ) (state : β), i ≤ count x → invariant x i state → (encState state).length ≤ size x) : ComputableTidilyInPolyTime (fun (x : α) => (step (par x))^[count x] (init x)) encIn encState ∧ ∀ (x : α), invariant x (count x) ((step (par x))^[count x] (init x))

Iteration may capture a computed parameter. The joint step certificate must be uniform in that parameter; the invariant and size bound concern the original input. The bound need not be computable and may use properties of the input beyond its encoded length.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.iterate_spec {α β : Type} {encIn : α ↪ List Bool} {encState : β ↪ List Bool} {count : α → ℕ} {init : α → β} {step : β → β} (hcount : ComputableTidilyInPolyTime count encIn encUnary) (hinit : ComputableTidilyInPolyTime init encIn encState) (hstep : ComputableTidilyInPolyTime step encState encState) (invariant : α → ℕ → β → Prop) (hbase : ∀ (x : α), invariant x 0 (init x)) (hpreserve : ∀ (x : α) (i : ℕ) (state : β), i < count x → invariant x i state → invariant x (i + 1) (step state)) {size : α → ℕ} (hsize : PolyBounded (fun (x : α) => (encIn x).length) size) (hbound : ∀ (x : α) (i : ℕ) (state : β), i ≤ count x → invariant x i state → (encState state).length ≤ size x) : ComputableTidilyInPolyTime (fun (x : α) => step^[count x] (init x)) encIn encState ∧ ∀ (x : α), invariant x (count x) (step^[count x] (init x))

One invariant proves both the resource bound and the final loop postcondition.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.iterateWith_of_bounded_growth {α β : Type} {encIn : α ↪ List Bool} {encState : β ↪ List Bool} {π : Type} {encPar : π ↪ List Bool} {par : α → π} {count : α → ℕ} {init : α → β} {step : π → β → β} (hpar : ComputableTidilyInPolyTime par encIn encPar) (hcount : ComputableTidilyInPolyTime count encIn encUnary) (hinit : ComputableTidilyInPolyTime init encIn encState) (hstep : ComputableTidilyInPolyTime (fun (p : π × β) => step p.1 p.2) (encPair encPar encState) encState) {growth : α → ℕ} (hpoly : PolyBounded (fun (x : α) => (encIn x).length) growth) (hgrowth : ∀ (x : α) (state : β), (encState (step (par x) state)).length ≤ (encState state).length + growth x) : ComputableTidilyInPolyTime (fun (x : α) => (step (par x))^[count x] (init x)) encIn encState

A captured loop may add a polynomial amount of storage per iteration, measured against the original input. A bound depending only on the current state would not justify this rule.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.iterateWithInput_of_bounded_growth {α β : Type} {encIn : α ↪ List Bool} {encState : β ↪ List Bool} {count : α → ℕ} {init : α → β} {step : α → β → β} (hcount : ComputableTidilyInPolyTime count encIn encUnary) (hinit : ComputableTidilyInPolyTime init encIn encState) (hstep : ComputableTidilyInPolyTime (fun (p : α × β) => step p.1 p.2) (encPair encIn encState) encState) {growth : α → ℕ} (hbound : PolyBounded (fun (x : α) => (encIn x).length) growth ∧ ∀ (x : α) (state : β), (encState (step x state)).length ≤ (encState state).length + growth x) : ComputableTidilyInPolyTime (fun (x : α) => (step x)^[count x] (init x)) encIn encState

An iteration step may capture its original input. Paired growth obligations let automation select a common polynomial bound. The uniform joint step certificate charges the captured input on every iteration; the growth bound need not itself be computable.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.iterate_of_bounded_growth {α β : Type} {encIn : α ↪ List Bool} {encState : β ↪ List Bool} {count : α → ℕ} {init : α → β} {step : β → β} (hcount : ComputableTidilyInPolyTime count encIn encUnary) (hinit : ComputableTidilyInPolyTime init encIn encState) (hstep : ComputableTidilyInPolyTime step encState encState) {growth : ℕ} (hgrowth : ∀ (state : β), (encState (step state)).length ≤ (encState state).length + growth) : ComputableTidilyInPolyTime (fun (x : α) => step^[count x] (init x)) encIn encState

A loop with constant additive state growth has polynomially bounded intermediate states.