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 implementation; 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: an angelic native-resource potential certificate over a StateTransitionImpl.
• Amortized.ofFn: constructor for deterministic specifications ([D.HasStepFn f]).

Main results

• Amortized.demonic, Amortized.exists_demonic: every demonically admissible adaptive execution satisfies the telescoping potential bound along its ClientRun transcript.
• Amortized.client, Amortized.exists_executes: deterministic specializations for [D.HasStepFn f].
• Amortized.client_const, Amortized.exists_executes_const: specialization to uniform constant amortized charges.
• Amortized.of_bound, Amortized.of_worstCase: derive potential certificates from independent worst-case bounds.

References

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

structure Cslib.DataStructure.Amortized {D : StateTransitionSpec} {C Trace : Type x} {exec : Execution D.signature C Trace} (R : StateTransitionImpl D exec) (weight : Trace → ℕ) (potential : D.State → C → ℕ) (charge : D.State → D.Op → ℕ) : Prop

Angelic potential certificate over a StateTransitionImpl: every native operation execution from a represented state on an admissible operation realizes some permitted abstract post-state s' with D.step s o s' a ∧ R.rep s' c' and weight trace + potential s' c' ≤ charge s o + potential s c.

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

  Angelic step correctness coupled with the potential inequality.

theorem Cslib.DataStructure.Amortized.ofFn {D : StateTransitionSpec} {C Trace : Type x} {exec : Execution D.signature C Trace} {R : StateTransitionImpl D exec} {weight : Trace → ℕ} {potential : D.State → C → ℕ} {charge : D.State → D.Op → ℕ} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (hstep : ∀ {s : D.State} {c : C} {o : D.Op} {a : D.signature.B o} {c' : C} {trace : Trace}, R.rep s c → D.valid s o → exec c o a c' trace → weight trace + potential (D.stepFn s o).1 c' ≤ charge s o + potential s c) : Amortized R weight potential charge

Construct an Amortized certificate on a deterministic specification ([D.HasStepFn f]) from a single-step potential inequality at (D.stepFn s o).1.

theorem Cslib.DataStructure.Amortized.demonic {D : StateTransitionSpec} {C Trace : Type x} {α : Type y} {exec : Execution D.signature C Trace} {R : StateTransitionImpl 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.DemonicValid s p) (he : Executes exec p c a c' traces) : ∃ (s' : D.State) (tr : D.Transcript), D.ClientRun s p a s' tr ∧ R.rep s' c' ∧ traces.length = List.length tr ∧ total weight traces + potential s' c' ≤ D.totalCostTranscript charge s tr + potential s c

Amortized telescoping along demonically admissible adaptive clients (demonic). For any demonically admissible client p and native execution Executes exec p c a c' traces, there exist a final abstract state s' and transcript tr such that D.ClientRun s p a s' tr, R.rep s' c', and total weight traces + potential s' c' ≤ D.totalCostTranscript charge s tr + potential s c.

theorem Cslib.DataStructure.Amortized.exists_demonic {D : StateTransitionSpec} {C Trace : Type x} {α : Type y} {exec : Execution D.signature C Trace} {R : StateTransitionImpl 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.DemonicValid s p) : ∃ (a : α) (c' : C) (traces : List Trace) (s' : D.State) (tr : D.Transcript), Executes exec p c a c' traces ∧ D.ClientRun s p a s' tr ∧ R.rep s' c' ∧ traces.length = List.length tr ∧ total weight traces + potential s' c' ≤ D.totalCostTranscript charge s tr + potential s c

Existence, correctness, and amortized bound (exists_demonic). From related initial states, every demonically admissible client p admits a native execution satisfying D.ClientRun, R.rep, and the telescoping potential bound.

theorem Cslib.DataStructure.Amortized.client {D : StateTransitionSpec} {C Trace : Type x} {α : Type y} {exec : Execution D.signature C Trace} {R : StateTransitionImpl D exec} {weight : Trace → ℕ} {potential : D.State → C → ℕ} {charge : D.State → D.Op → ℕ} (A : Amortized R weight potential charge) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {p : D.Client α} {s : D.State} {c c' : C} {a : α} {traces : List Trace} (hr : R.rep s c) (hv : D.ValidHistory s (D.clientHistory s p)) (he : Executes exec p c a c' traces) : total weight traces + potential (D.clientState s p) c' ≤ D.totalCost charge s (D.clientHistory s p) + potential s c

Adaptive clients retain both initial and final representation credit on deterministic specifications.

theorem Cslib.DataStructure.Amortized.exists_executes {D : StateTransitionSpec} {C Trace : Type x} {α : Type y} {exec : Execution D.signature C Trace} {R : StateTransitionImpl D exec} {weight : Trace → ℕ} {potential : D.State → C → ℕ} {charge : D.State → D.Op → ℕ} (A : Amortized R weight potential charge) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (p : D.Client α) {s : D.State} {c : C} (hr : R.rep s c) (hv : D.ValidHistory s (D.clientHistory s p)) : ∃ (c' : C) (traces : List Trace), Executes exec p c (D.clientResult s p) c' traces ∧ R.rep (D.clientState s p) c' ∧ total weight traces + potential (D.clientState s p) c' ≤ D.totalCost charge s (D.clientHistory s p) + potential s c

Existence and semantic correctness are inherited independently from the implementation.

theorem Cslib.DataStructure.Amortized.client_const {D : StateTransitionSpec} {C Trace : Type x} {α : Type y} {exec : Execution D.signature C Trace} {R : StateTransitionImpl D exec} {weight : Trace → ℕ} {potential : D.State → C → ℕ} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {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.clientHistory s p)) (he : Executes exec p c a c' traces) : total weight traces + potential (D.clientState s p) c' ≤ (D.clientHistory s p).length * K + potential s c

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

theorem Cslib.DataStructure.Amortized.exists_executes_const {D : StateTransitionSpec} {C Trace : Type x} {α : Type y} {exec : Execution D.signature C Trace} {R : StateTransitionImpl D exec} {weight : Trace → ℕ} {potential : D.State → C → ℕ} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {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.clientHistory s p)) : ∃ (c' : C) (traces : List Trace), Executes exec p c (D.clientResult s p) c' traces ∧ R.rep (D.clientState s p) c' ∧ total weight traces + potential (D.clientState s p) c' ≤ (D.clientHistory s p).length * K + potential s c

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

theorem Cslib.DataStructure.Amortized.of_bound {D : StateTransitionSpec} {C Trace : Type x} {exec : Execution D.signature C Trace} {R : StateTransitionImpl D exec} {weight : Trace → ℕ} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {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.stepFn s o).1 ≤ charge s o + potential s) : Amortized R weight (fun (s : D.State) (x : C) => potential s) charge

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

theorem Cslib.DataStructure.Amortized.of_bound_demonic {D : StateTransitionSpec} {C Trace : Type x} {exec : Execution D.signature C Trace} {R : StateTransitionImpl 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) (s' : D.State) (a : D.Result o), D.valid s o → D.step s o s' a → cost s o + potential s' ≤ 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 relational abstract potential inequality across all permitted outcomes.

theorem Cslib.DataStructure.Amortized.of_worstCase {D : StateTransitionSpec} {C Trace : Type x} {exec : Execution D.signature C Trace} {R : StateTransitionImpl 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 a zero-potential certificate.