Synthesizing polynomial-time certificates

Adapted from the cslib crypto branch: named certificates are tried before their implementations are unfolded. fun_prop handles composition; Aesop chooses loop rules and uses local growth contracts. Every rule proves the tidy machine predicate, with fixed machines and polynomial bounds across all encoded inputs. A plain Turing.MultiTapeTM.ComputableInPolyTime goal is reduced to the tidy predicate, and plain hypotheses are restated tidily, so plain statements use the same search. Unknown algorithms still require certificates.

Main definitions

• polytime: prove a polynomial-time certificate using the PolyTime Aesop rule set.

References

Adapted from Cslib/Tactic/PolyTime.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the existing tidy calculus.

theorem Cslib.Tactic.PolyTime.bool_not_rule {α : Type} {input : α ↪ List Bool} {guard : α → Bool} (hguard : Turing.MultiTapeTM.ComputableTidilyInPolyTime guard input Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => !guard a) input Turing.MultiTapeTM.encBool

Expose a negated guard to loop rules when compositional proof search needs their help.

theorem Cslib.Tactic.PolyTime.foldl_bits_rule {γ β : Type} {encIn : γ ↪ List Bool} {encB : β ↪ List Bool} {list : γ → List Bool} {init : γ → β} {step : β → Bool → β} (hlist : Turing.MultiTapeTM.ComputableTidilyInPolyTime list encIn Turing.MultiTapeTM.encBits) (hinit : Turing.MultiTapeTM.ComputableTidilyInPolyTime init encIn encB) (hstep : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : β × Bool) => step pair.1 pair.2) (Turing.MultiTapeTM.encPair encB Turing.MultiTapeTM.encBool) encB) {growth : ℕ} (hgrowth : ∀ (state : β), (encB (step state false)).length ≤ (encB state).length + growth ∧ (encB (step state true)).length ≤ (encB state).length + growth) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB

Fix a raw bit list's encoding and expose the two growth cases before proof search.

theorem Cslib.Tactic.PolyTime.foldl_list_rule {γ α β : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {list : γ → List α} {init : γ → β} {step : β → α → β} (hlist : Turing.MultiTapeTM.ComputableTidilyInPolyTime list encIn (Turing.MultiTapeTM.encList encA)) (hinit : Turing.MultiTapeTM.ComputableTidilyInPolyTime init encIn encB) (hstep : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : β × α) => step pair.1 pair.2) (Turing.MultiTapeTM.encPair encB encA) encB) {growth : ℕ} (hgrowth : ∀ (state : β) (value : α), (encB (step state value)).length ≤ (encB state).length + growth) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB

Fix a framed list's encoding before proof search infers the element encoding.

def Cslib.Tactic.PolyTime.tacticPolytime : Lean.ParserDescr

Prove a polynomial-time certificate from known routines and controlled loop rules.