Amortized resource certificates over native executions

Potential credit can depend on both the mathematical state and the hidden concrete state. This layer attaches a potential inequality to an existing semantic realization; it does not modify execution or assign a machine cost to pure Lean computation. Endpoint credit is retained on the left of the bound, avoiding truncated subtraction.

Main definitions

• Amortized: a separate native-resource potential certificate.

Main results

• Amortized.client: every admissible adaptive execution satisfies the telescoping bound.
• Amortized.run: existence, correctness and the potential bound for an admissible client.
• Amortized.of_bound: derive potential certificates from independent worst-case bounds.

References

• Cormen, Leiserson, Rivest and Stein, Introduction to Algorithms, Chapter 17.

structure Cslib.Stateful.Amortized {D : Spec} {C Trace : Type x} {exec : Execution D C Trace} (R : Realization D exec) (weight : Trace → ℕ) (potential : D.State → C → ℕ) (charge : D.State → D.Op → ℕ) : Prop

Potential inequalities concern actual native evidence and may retain hidden-state credit.

• step {s : D.State} {c : C} {o : D.Op} {a : D.Result o} {c' : C} {trace : Trace} : R.rep s c → D.valid s o → exec c o a c' trace → weight trace + potential (D.step s o).1 c' ≤ charge s o + potential s c

theorem Cslib.Stateful.Amortized.client {D : Spec} {C Trace : Type x} {α : Type y} {exec : Execution D C Trace} {R : Realization D exec} {weight : Trace → ℕ} {potential : D.State → C → ℕ} {charge : D.State → D.Op → ℕ} (A : Amortized R weight potential charge) {p : D.Client α} {s : D.State} {c c' : C} {a : α} {traces : List Trace} (hr : R.rep s c) (hv : D.ValidHistory s (D.runClient s p).2.2) (he : Executes exec p c a c' traces) : total weight traces + potential (D.runClient s p).2.1 c' ≤ D.totalCost charge s (D.runClient s p).2.2 + potential s c

Adaptive clients retain both initial and final representation credit.

theorem Cslib.Stateful.Amortized.run {D : Spec} {C Trace : Type x} {α : Type y} {exec : Execution D C Trace} {R : Realization D exec} {weight : Trace → ℕ} {potential : D.State → C → ℕ} {charge : D.State → D.Op → ℕ} (A : Amortized R weight potential charge) (p : D.Client α) {s : D.State} {c : C} (hr : R.rep s c) (hv : D.ValidHistory s (D.runClient s p).2.2) : ∃ (c' : C) (traces : List Trace), Executes exec p c (D.runClient s p).1 c' traces ∧ R.rep (D.runClient s p).2.1 c' ∧ total weight traces + potential (D.runClient s p).2.1 c' ≤ D.totalCost charge s (D.runClient s p).2.2 + potential s c

Existence and semantic correctness are inherited independently from the realization.

theorem Cslib.Stateful.Amortized.client_const {D : Spec} {C Trace : Type x} {α : Type y} {exec : Execution D C Trace} {R : Realization D exec} {weight : Trace → ℕ} {potential : D.State → C → ℕ} {K : ℕ} (A : Amortized R weight potential fun (x : D.State) (x_1 : D.Op) => K) {p : D.Client α} {s : D.State} {c c' : C} {a : α} {traces : List Trace} (hr : R.rep s c) (hv : D.ValidHistory s (D.runClient s p).2.2) (he : Executes exec p c a c' traces) : total weight traces + potential (D.runClient s p).2.1 c' ≤ (D.runClient s p).2.2.length * K + potential s c

Adaptive client potential bound for a uniform constant per-operation amortized charge.

theorem Cslib.Stateful.Amortized.run_const {D : Spec} {C Trace : Type x} {α : Type y} {exec : Execution D C Trace} {R : Realization D exec} {weight : Trace → ℕ} {potential : D.State → C → ℕ} {K : ℕ} (A : Amortized R weight potential fun (x : D.State) (x_1 : D.Op) => K) (p : D.Client α) {s : D.State} {c : C} (hr : R.rep s c) (hv : D.ValidHistory s (D.runClient s p).2.2) : ∃ (c' : C) (traces : List Trace), Executes exec p c (D.runClient s p).1 c' traces ∧ R.rep (D.runClient s p).2.1 c' ∧ total weight traces + potential (D.runClient s p).2.1 c' ≤ (D.runClient s p).2.2.length * K + potential s c

Existence, correctness, and potential bound for a uniform constant amortized charge.

theorem Cslib.Stateful.Amortized.of_bound {D : Spec} {C Trace : Type x} {exec : Execution D C Trace} {R : Realization D exec} {weight : Trace → ℕ} {cost : D.State → D.Op → ℕ} (B : Bound R weight cost) (potential : D.State → ℕ) (charge : D.State → D.Op → ℕ) (h : ∀ (s : D.State) (o : D.Op), D.valid s o → cost s o + potential (D.step s o).1 ≤ charge s o + potential s) : Amortized R weight (fun (s : D.State) (x : C) => potential s) charge

Worst-case certificates give potential certificates whenever their charges satisfy the abstract potential inequality.

theorem Cslib.Stateful.Amortized.of_worstCase {D : Spec} {C Trace : Type x} {exec : Execution D C Trace} {R : Realization D exec} {weight : Trace → ℕ} {charge : D.State → D.Op → ℕ} (B : Bound R weight charge) : Amortized R weight (fun (x : D.State) (x_1 : C) => 0) charge

A worst-case bound is exactly a zero-potential certificate.