Polynomial-time folds

The polynomial-time counterparts of Christian Reitwiessner's degree-bounded fold rules. A SizedListEncoding accounts for list lengths, elements and suffixes, leaving only a polynomial bound on the intermediate accumulator. The step may carry a fixed parameter. The basic folds come from the degree-bounded fold rules; the specification and growth contracts are the plain contracts of Turing.MultiTapeTM.ComputableInPolyTime (in Internal.PolyTimeLoops) with tidied conclusions.

Main definitions

• Turing.MultiTapeTM.encFoldStep: the encoding of the input of a fold step with a parameter.

Main results

• Turing.MultiTapeTM.ComputableTidilyInPolyTime.foldl': a fold with bounded accumulators.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.foldlWith: a fold with a fixed parameter.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.foldl_spec: one prefix invariant proves both polynomial-time computation and the final postcondition.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.foldlWith_spec: the same contract with a computed captured parameter.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.foldlWith_of_bounded_growth: input-dependent additive growth on the values occurring in the runtime list.
• Turing.MultiTapeTM.ComputableTidilyInPolyTime.foldlWithInput_of_bounded_growth: the same contract for a callback that captures the original input.

The specification interface is adapted from IsPolyTime.list_foldl_spec in the cslib crypto branch.

@[reducible, inline]

abbrev Turing.MultiTapeTM.encFoldStep {π β α : Type} (encP : π ↪ List Bool) (encB : β ↪ List Bool) (encA : α ↪ List Bool) : (π × β) × α ↪ List Bool

The encoding of the input ((p, b), a) of a fold step with a fixed parameter: the pair of the parameter p, framed, and the accumulator b, framed as a whole, then the element a.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.foldl' {γ α β : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} [ListEncoding encA encL] [SizedListEncoding encA encL] {list : γ → List α} {init : γ → β} {step : β → α → β} (hlist : ComputableTidilyInPolyTime list encIn encL) (hinit : ComputableTidilyInPolyTime init encIn encB) (hstep : ComputableTidilyInPolyTime (fun (p : β × α) => step p.1 p.2) (encPair encB encA) encB) {B : γ → ℕ} (hB : PolyBounded (fun (x : γ) => (encIn x).length) B) (hstates : ∀ (x : γ), ∀ i ≤ (list x).length, (encB (List.foldl step (init x) (List.take i (list x)))).length ≤ B x) : ComputableTidilyInPolyTime (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB

A left fold is polynomial-time when its step is polynomial-time and its intermediate accumulators have polynomially bounded encoded length.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.foldlWith {γ α β π : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} {encP : π ↪ List Bool} [ListEncoding encA encL] [SizedListEncoding encA encL] {par : γ → π} {list : γ → List α} {init : γ → β} {step : π → β → α → β} (hpar : ComputableTidilyInPolyTime par encIn encP) (hlist : ComputableTidilyInPolyTime list encIn encL) (hinit : ComputableTidilyInPolyTime init encIn encB) (hstep : ComputableTidilyInPolyTime (fun (p : (π × β) × α) => step p.1.1 p.1.2 p.2) (encFoldStep encP encB encA) encB) {B : γ → ℕ} (hB : PolyBounded (fun (x : γ) => (encIn x).length) B) (hstates : ∀ (x : γ), ∀ i ≤ (list x).length, (encB (List.foldl (step (par x)) (init x) (List.take i (list x)))).length ≤ B x) : ComputableTidilyInPolyTime (fun (x : γ) => List.foldl (step (par x)) (init x) (list x)) encIn encB

A polynomial-time fold whose step also uses a fixed, polynomial-time computable parameter.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.foldlWith_spec {γ α β π : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} {encP : π ↪ List Bool} [ListEncoding encA encL] [SizedListEncoding encA encL] {par : γ → π} {list : γ → List α} {init : γ → β} {step : π → β → α → β} (hpar : ComputableTidilyInPolyTime par encIn encP) (hlist : ComputableTidilyInPolyTime list encIn encL) (hinit : ComputableTidilyInPolyTime init encIn encB) (hstep : ComputableTidilyInPolyTime (fun (p : (π × β) × α) => step p.1.1 p.1.2 p.2) (encFoldStep encP encB encA) encB) (invariant : γ → List α → β → Prop) (hbase : ∀ (x : γ), invariant x [] (init x)) (hpreserve : ∀ (x : γ) (consumed : List α) (state : β) (value : α), consumed ++ [value] <+: list x → invariant x consumed state → invariant x (consumed ++ [value]) (step (par x) state value)) {size : γ → ℕ} (hsize : PolyBounded (fun (x : γ) => (encIn x).length) size) (hbound : ∀ (x : γ) (consumed : List α) (state : β), consumed <+: list x → invariant x consumed state → (encB state).length ≤ size x) : ComputableTidilyInPolyTime (fun (x : γ) => List.foldl (step (par x)) (init x) (list x)) encIn encB ∧ ∀ (x : γ), invariant x (list x) (List.foldl (step (par x)) (init x) (list x))

A prefix invariant supplies both the accumulator bound and the final postcondition for a fold with a captured parameter. The size bound may depend on the original input and need not be computable. The step certificate is uniform jointly in the parameter, accumulator and element.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.foldl_spec {γ α β : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} [ListEncoding encA encL] [SizedListEncoding encA encL] {list : γ → List α} {init : γ → β} {step : β → α → β} (hlist : ComputableTidilyInPolyTime list encIn encL) (hinit : ComputableTidilyInPolyTime init encIn encB) (hstep : ComputableTidilyInPolyTime (fun (p : β × α) => step p.1 p.2) (encPair encB encA) encB) (invariant : γ → List α → β → Prop) (hbase : ∀ (x : γ), invariant x [] (init x)) (hpreserve : ∀ (x : γ) (consumed : List α) (state : β) (value : α), consumed ++ [value] <+: list x → invariant x consumed state → invariant x (consumed ++ [value]) (step state value)) {size : γ → ℕ} (hsize : PolyBounded (fun (x : γ) => (encIn x).length) size) (hbound : ∀ (x : γ) (consumed : List α) (state : β), consumed <+: list x → invariant x consumed state → (encB state).length ≤ size x) : ComputableTidilyInPolyTime (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB ∧ ∀ (x : γ), invariant x (list x) (List.foldl step (init x) (list x))

A prefix invariant supplies both the accumulator bound and the final postcondition. The size bound may depend on the original input and need not be computable. The list and step must have uniform polynomial-time certificates.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.foldlWith_of_bounded_growth {γ α β π : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} {encP : π ↪ List Bool} [ListEncoding encA encL] [SizedListEncoding encA encL] {par : γ → π} {list : γ → List α} {init : γ → β} {step : π → β → α → β} (hpar : ComputableTidilyInPolyTime par encIn encP) (hlist : ComputableTidilyInPolyTime list encIn encL) (hinit : ComputableTidilyInPolyTime init encIn encB) (hstep : ComputableTidilyInPolyTime (fun (p : (π × β) × α) => step p.1.1 p.1.2 p.2) (encFoldStep encP encB encA) encB) {growth : γ → ℕ} (hpoly : PolyBounded (fun (x : γ) => (encIn x).length) growth) (hgrowth : ∀ (x : γ) (state : β), ∀ value ∈ list x, (encB (step (par x) state value)).length ≤ (encB state).length + growth x) : ComputableTidilyInPolyTime (fun (x : γ) => List.foldl (step (par x)) (init x) (list x)) encIn encB

A captured fold may add a polynomial amount of storage per element, measured against the original input. The growth bound covers every accumulator and each element in the runtime list; the joint step certificate still covers all parameters, accumulators and elements.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.foldlWithInput_of_bounded_growth {γ α β : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} {list : γ → List α} {init : γ → β} {step : γ → β → α → β} (hinit : ComputableTidilyInPolyTime init encIn encB) (hcompute : ComputableTidilyInPolyTime list encIn encL ∧ ComputableTidilyInPolyTime (fun (p : (γ × β) × α) => step p.1.1 p.1.2 p.2) (encFoldStep encIn encB encA) encB ∧ ListEncoding encA encL ∧ SizedListEncoding encA encL) {growth : γ → ℕ} (hbound : PolyBounded (fun (x : γ) => (encIn x).length) growth ∧ ∀ (x : γ) (state : β), ∀ value ∈ list x, (encB (step x state value)).length ≤ (encB state).length + growth x) : ComputableTidilyInPolyTime (fun (x : γ) => List.foldl (step x) (init x) (list x)) encIn encB

A fold callback may capture its original input. Growth is needed only on elements of the runtime list, for every accumulator. Joint computation and encoding evidence lets automation choose compatible list and callback certificates; paired growth obligations select a common polynomial bound. The general foldlWith_of_bounded_growth contract takes separate premises.

theorem Turing.MultiTapeTM.ComputableTidilyInPolyTime.foldl_of_bounded_growth {γ α β : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} [ListEncoding encA encL] [SizedListEncoding encA encL] {list : γ → List α} {init : γ → β} {step : β → α → β} (hlist : ComputableTidilyInPolyTime list encIn encL) (hinit : ComputableTidilyInPolyTime init encIn encB) (hstep : ComputableTidilyInPolyTime (fun (p : β × α) => step p.1 p.2) (encPair encB encA) encB) {growth : ℕ} (hgrowth : ∀ (state : β) (value : α), (encB (step state value)).length ≤ (encB state).length + growth) : ComputableTidilyInPolyTime (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB

Constant additive growth discharges the fold's intermediate-size obligation.