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. Plain and internal tidy goals use separate rules, with fixed machines and polynomial bounds across all encoded inputs. Plain search applies plain statements directly; it does not lower a goal or restate its hypotheses tidily. Unknown algorithms still require certificates. On ordinary failure, polytime includes one failed compositional attempt when the backend has reported one. This is a search hint, not a claim that the subterm is uncomputable. Resource-limit and interrupt exceptions are unchanged.

Plain search excludes rules that would start search in the internal tidy calculus. Whether an imported rule is excluded is decided once per file and shared by later calls (#1155); rules of the current module are classified by each call.

Goal preparation, shared with ppt, runs before the search. polytime [f, g] unfolds the hinted definitions in the goal and inlines the lets they expose. Every form replaces local encoding lets (let E := encPair encUnary encBits) by their values in the goal and the hypotheses, and adds the certificates stored in fields of local structures (a scheme's S.decrypt_polyTime, an admissibility hypothesis's h.guess, a conjunction's components) as local facts.

Main definitions

• polytime: prove a polynomial-time certificate using the PolyTime Aesop rule set.
• Cslib.Tactic.PolyTime.Internal.prepareGoal: the goal preparation shared with ppt.

References

Adapted from Cslib/Tactic/PolyTime.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8; deterministic search consumes the canonical plain calculus.

theorem Cslib.Tactic.PolyTime.Internal.plainBitsCons {α : Type} {encIn : α ↪ List Bool} {f : α → Bool} {g : α → List Bool} (hf : Turing.MultiTapeTM.ComputableInPolyTime f encIn Turing.MultiTapeTM.encBool) (hg : Turing.MultiTapeTM.ComputableInPolyTime g encIn Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => f a :: g a) encIn Turing.MultiTapeTM.encBits

Prepend a computed bit with both intermediate raw encodings fixed for the tactic.

theorem Cslib.Tactic.PolyTime.Internal.plainListAppend {α β : Type} {encIn : α ↪ List Bool} {enc : β ↪ List Bool} {f g : α → List β} (hf : Turing.MultiTapeTM.ComputableInPolyTime f encIn (Turing.MultiTapeTM.encList enc)) (hg : Turing.MultiTapeTM.ComputableInPolyTime g encIn (Turing.MultiTapeTM.encList enc)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => f a ++ g a) encIn (Turing.MultiTapeTM.encList enc)

Append computed framed lists with their element encoding fixed for the tactic.

theorem Cslib.Tactic.PolyTime.Internal.plainListCons {α β : Type} {encIn : α ↪ List Bool} {enc : β ↪ List Bool} {f : α → β} {g : α → List β} (hf : Turing.MultiTapeTM.ComputableInPolyTime f encIn enc) (hg : Turing.MultiTapeTM.ComputableInPolyTime g encIn (Turing.MultiTapeTM.encList enc)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => f a :: g a) encIn (Turing.MultiTapeTM.encList enc)

Prepend a computed element to a framed list with its element encoding fixed.

def Cslib.Tactic.PolyTime.Internal.applyLocalCertificates : Aesop.RuleTac

Retain Aesop's local application alternatives and priority, excluding only rules which would start raw search from a plain goal. Adapted from Aesop.BuiltinRules.applyHyps (Jannis Limperg).

def Cslib.Tactic.PolyTime.Internal.withPlainRuleMemo (action : Lean.Elab.Tactic.TacticM Unit) : Lean.Elab.Tactic.TacticM Unit

Reuse global classification answers across one invocation, and those of imported declarations across the file. Rule tables, certificate lookup, matching and local evidence are not projected or cached by this wrapper.

def Cslib.Tactic.PolyTime.Internal.withPlainRuleCache (action : Lean.Elab.Tactic.TacticM Unit) : Lean.Elab.Tactic.TacticM Unit

Apply the deterministic boundary using the current tables and scoped classification memo. Explicit raw construction entries and all named-certificate metadata retain their old policy.

def Cslib.Tactic.PolyTime.Internal.withFailureHint (tacticName : String) (action : Lean.Elab.Tactic.TacticM Unit) : Lean.Elab.Tactic.TacticM Unit

Collect one backend hint without rerunning search, reporting it as a failure of the tactic tacticName. Each invocation, including a nested one, has its own reference; withEnv restores the caller's environment even on resource exceptions. The ordinary catch does not intercept Lean's resource-limit or interrupt exceptions.

def Cslib.Tactic.PolyTime.Internal.funPropWithPlainBoundary (maxSteps : ℕ) : Lean.Elab.Tactic.TacticM Unit

Shared compositional backend with a fresh alias-aware raw-premise boundary. The standard assumption discharger and ordinary transition depth are retained; callers keep their step limit. Consumers can reuse the same boundary for nested plain deterministic goals.

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.

theorem Cslib.Tactic.PolyTime.Internal.plain_foldl_bits_rule {γ β : Type} {encIn : γ ↪ List Bool} {encB : β ↪ List Bool} {list : γ → List Bool} {init : γ → β} {step : β → Bool → β} (hlist : Turing.MultiTapeTM.ComputableInPolyTime list encIn Turing.MultiTapeTM.encBits) (hinit : Turing.MultiTapeTM.ComputableInPolyTime init encIn encB) (hstep : Turing.MultiTapeTM.ComputableInPolyTime (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.ComputableInPolyTime (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.Internal.plain_foldl_list_rule {γ α β : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {list : γ → List α} {init : γ → β} {step : β → α → β} (hlist : Turing.MultiTapeTM.ComputableInPolyTime list encIn (Turing.MultiTapeTM.encList encA)) (hinit : Turing.MultiTapeTM.ComputableInPolyTime init encIn encB) (hstep : Turing.MultiTapeTM.ComputableInPolyTime (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.ComputableInPolyTime (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB

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

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

The plain iteration rule retains the same constant additive growth contract.

def Cslib.Tactic.PolyTime.Internal.prepareGoal (hints : Array Lean.Ident) : Lean.Elab.Tactic.TacticM Unit

Prepare a certificate goal: unfold the hinted definitions in the goal and inline the lets they expose, unfold local encoding lets, and expose certificates stored in fields of local structures.

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

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

polytime [f, g] first unfolds the definitions f and g in the goal. Before searching, every form also replaces local encoding lets (let E := encPair encUnary encBits) by their values and adds the certificates stored in fields of local structures, such as S.encrypt_ppt for a scheme S or h.guess for an admissibility hypothesis h, as local facts.

def Cslib.Tactic.PolyTime.evalPolytime : Lean.Elab.Tactic.Tactic

Elaborate polytime: prepare the goal, then search with the PolyTime Aesop rule set.