Independent additive resource certificates

The same semantic realization admits multiple resource interpretations. Additive measures of native evidence compose exactly; this does not model peak live space or cache replacement. Module potentials may depend on hidden intermediate representations, which are retained as existential witnesses rather than silently exposed to the client.

Main definitions

• total: additive interpretation of a native trace.
• Bound: a per-operation resource certificate, separate from semantic realization.

Main results

• Bound.client: resource bounds compose along an adaptive client.
• Module.bound: transport worst-case bounds through a semantic module.
• Module.amortized_client: telescope hidden-state potential through arbitrary executions.

References

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

def Cslib.Stateful.total {τ : Type x} (weight : τ → ℕ) : List τ → ℕ

An additive interpretation of recorded native executions. Only additive resources use this.

def Cslib.Stateful.Bound {D : Spec} {C τ : Type x} {exec : Execution D C τ} (R : Realization D exec) (weight : τ → ℕ) (charge : D.State → D.Op → ℕ) : Prop

A resource certificate is separate from the realization and can be supplied more than once.

theorem Cslib.Stateful.spec_total_const (D : Spec) (K : ℕ) (s : D.State) (os : List D.Op) : D.totalCost (fun (x : D.State) (x_1 : D.Op) => K) s os = os.length * K

A constant charge K per operation totals K times the length of the history.

theorem Cslib.Stateful.Bound.client {D : Spec} {C τ : Type x} {α : Type y} {exec : Execution D C τ} {R : Realization D exec} {weight : τ → ℕ} {charge : D.State → D.Op → ℕ} (B : Bound R weight charge) {p : D.Client α} {s : D.State} {c c' : C} {a : α} {traces : List τ} (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 ≤ D.totalCost charge s (D.runClient s p).2.2

Under a resource certificate, every native execution of a client whose history is admissible, from related states, has total weight at most the total charge of the specified history.

theorem Cslib.Stateful.Bound.run {D : Spec} {C τ : Type x} {α : Type y} {exec : Execution D C τ} {R : Realization D exec} {weight : τ → ℕ} {charge : D.State → D.Op → ℕ} (B : Bound R weight 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 τ), Executes exec p c (D.runClient s p).1 c' traces ∧ R.rep (D.runClient s p).2.1 c' ∧ total weight traces ≤ D.totalCost charge s (D.runClient s p).2.2

Existence and semantic correctness are inherited independently from the realization.

theorem Cslib.Stateful.Bound.client_const {D : Spec} {C τ : Type x} {α : Type y} {exec : Execution D C τ} {R : Realization D exec} {weight : τ → ℕ} {K : ℕ} (B : Bound R weight fun (x : D.State) (x_1 : D.Op) => K) {p : D.Client α} {s : D.State} {c c' : C} {a : α} {traces : List τ} (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 ≤ (D.runClient s p).2.2.length * K

Uniform constant per-operation bounds scale by the history length.

theorem Cslib.Stateful.Bound.run_const {D : Spec} {C τ : Type x} {α : Type y} {exec : Execution D C τ} {R : Realization D exec} {weight : τ → ℕ} {K : ℕ} (B : Bound R weight 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 τ), Executes exec p c (D.runClient s p).1 c' traces ∧ R.rep (D.runClient s p).2.1 c' ∧ total weight traces ≤ (D.runClient s p).2.2.length * K

Existence, correctness, and total cost for a uniform constant per-operation bound.

theorem Cslib.Stateful.Module.bound {D E : Spec} {C τ : Type x} (M : Module D E) {exec : Execution E C τ} (R : Realization E exec) {weight : τ → ℕ} {charge : E.State → E.Op → ℕ} (B : Bound R weight charge) (budget : D.State → D.Op → ℕ) (hbudget : ∀ {s : D.State} {e : E.State} (o : D.Op), M.rep s e → D.valid s o → E.totalCost charge e (E.runClient e (M.methods o)).2.2 ≤ budget s o) : Bound (M.realize R) (total weight) budget

A resource interpretation is transported afterwards, without changing semantic proofs.

theorem Cslib.Stateful.Module.amortized_client {D E : Spec} {C τ : Type x} {α : Type y} (M : Module D E) {exec : Execution E C τ} (R : Realization E exec) {weight : τ → ℕ} {lowerCharge : E.State → E.Op → ℕ} (B : Bound R weight lowerCharge) (potential : D.State → E.State → ℕ) (charge : D.State → D.Op → ℕ) (hstep : ∀ {s : D.State} {e : E.State} (o : D.Op), M.rep s e → D.valid s o → E.totalCost lowerCharge e (E.runClient e (M.methods o)).2.2 + potential (D.step s o).1 (E.runClient e (M.methods o)).2.1 ≤ charge s o + potential s e) {p : D.Client α} {s : D.State} {e : E.State} {c c' : C} {a : α} {chunks : List (List τ)} (hM : M.rep s e) (hR : R.rep e c) (hv : D.ValidHistory s (D.runClient s p).2.2) (he : Executes (fun (x : C) (o : D.Op) (a : D.Result o) (y : C) (ts : List τ) => Executes exec (M.methods o) x a y ts) p c a c' chunks) : ∃ (e' : E.State), M.rep (D.runClient s p).2.1 e' ∧ R.rep e' c' ∧ total (total weight) chunks + potential (D.runClient s p).2.1 e' ≤ D.totalCost charge s (D.runClient s p).2.2 + potential s e

Hidden representation credit telescopes along an arbitrary adaptive upper client. The intermediate abstract state remains existentially hidden in the conclusion.

theorem Cslib.Stateful.total_one {τ : Type x} (ts : List τ) : total (fun (x : τ) => 1) ts = ts.length

Unit weights total the length of the trace.

theorem Cslib.Stateful.spec_total_one (D : Spec) (s : D.State) (os : List D.Op) : D.totalCost (fun (x : D.State) (x_1 : D.Op) => 1) s os = os.length

A unit charge per operation totals the length of the history.

theorem Cslib.Stateful.total_append {τ : Type x} (weight : τ → ℕ) (xs ys : List τ) : total weight (xs ++ ys) = total weight xs + total weight ys

The total of a concatenation is the sum of the totals.

theorem Cslib.Stateful.total_flatten {τ : Type x} (weight : τ → ℕ) (chunks : List (List τ)) : total weight chunks.flatten = total (total weight) chunks

The total of a flattened list of chunks is the sum of the totals of the chunks.