Independent additive resource certificates

The same semantic implementation 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 implementation.

Main results

• total_eq_sum_map, total_flatten: total agrees with (ts.map weight).sum and distributes over flattened trace chunks.
• Bound.demonic, Bound.exists_demonic: relational resource bounds and existence along a demonically admissible adaptive client.
• Bound.client, Bound.exists_executes, Bound.client_const, Bound.exists_executes_const: deterministic specializations for [D.HasStepFn f].
• Module.bound_demonic, Module.bound: transport worst-case bounds through a semantic module.
• Module.amortized_demonic, Module.amortized_client: telescope hidden-state potential through adaptive client executions.

References

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

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

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

@[simp]

theorem Cslib.DataStructure.total_nil {τ : Type x} (weight : τ → ℕ) : total weight [] = 0

The empty native trace has zero total weight.

@[simp]

theorem Cslib.DataStructure.total_cons {τ : Type x} (weight : τ → ℕ) (t : τ) (ts : List τ) : total weight (t :: ts) = weight t + total weight ts

Prepending a trace element adds its weight to the tail total.

theorem Cslib.DataStructure.total_eq_sum_map {τ : Type x} (weight : τ → ℕ) (ts : List τ) : total weight ts = (List.map weight ts).sum

total is the sum of the mapped weights.

def Cslib.DataStructure.Bound {D : StateTransitionSpec} {C τ : Type x} {exec : Execution D.signature C τ} (R : StateTransitionImpl D exec) (weight : τ → ℕ) (charge : D.State → D.Op → ℕ) : Prop

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

theorem Cslib.DataStructure.Bound.demonic {D : StateTransitionSpec} {C τ : Type x} {α : Type y} {exec : Execution D.signature C τ} {R : StateTransitionImpl 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.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 ≤ D.totalCostTranscript charge s tr

Under a resource certificate, every native execution of a demonically admissible client realizes a valid ClientRun transcript whose total charge bounds total weight traces.

theorem Cslib.DataStructure.Bound.exists_demonic {D : StateTransitionSpec} {C τ : Type x} {α : Type y} {exec : Execution D.signature C τ} {R : StateTransitionImpl 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.DemonicValid s p) : ∃ (a : α) (c' : C) (traces : List τ) (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 ≤ D.totalCostTranscript charge s tr

Under a resource certificate, every demonically admissible client admits a native execution meeting the total charge bound along its ClientRun transcript.

theorem Cslib.DataStructure.Bound.client {D : StateTransitionSpec} {C τ : Type x} {α : Type y} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {exec : Execution D.signature C τ} {R : StateTransitionImpl 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.clientHistory s p)) (he : Executes exec p c a c' traces) : total weight traces ≤ D.totalCost charge s (D.clientHistory s p)

Under a resource certificate on a deterministic specification ([D.HasStepFn f]), every native execution of a client whose history is admissible has total weight at most the total charge of the specified history.

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

Existence and semantic correctness are inherited independently from the implementation.

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

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

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

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

theorem Cslib.DataStructure.Module.bound_demonic {D E : StateTransitionSpec} {C τ : Type x} (M : Module D E) {exec : Execution E.signature C τ} (R : StateTransitionImpl 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) {a : D.Result o} {e' : E.State} {tr : E.Transcript}, M.rep s e → D.valid s o → E.ClientRun e (M.methods o) a e' tr → E.totalCostTranscript charge e tr ≤ budget s o) : Bound (M.realize R) (total weight) budget

Transport a worst-case resource bound through a relational semantic module.

theorem Cslib.DataStructure.Module.bound {D E : StateTransitionSpec} {C τ : Type x} (M : Module D E) {exec : Execution E.signature C τ} {fE : E.State → (o : E.Op) → E.State × E.Result o} [E.HasStepFn fE] (R : StateTransitionImpl 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.clientHistory e (M.methods o)) ≤ budget s o) : Bound (M.realize R) (total weight) budget

A resource interpretation is transported afterwards on deterministic lower specifications.

theorem Cslib.DataStructure.Module.amortized_demonic {D E : StateTransitionSpec} {C τ : Type x} {α : Type y} (M : Module D E) {exec : Execution E.signature C τ} (R : StateTransitionImpl 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) {a : D.Result o} {e' : E.State} {tr : E.Transcript}, M.rep s e → D.valid s o → E.ClientRun e (M.methods o) a e' tr → ∃ (s' : D.State), D.step s o s' a ∧ M.rep s' e' ∧ E.totalCostTranscript lowerCharge e tr + potential s' e' ≤ 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.DemonicValid s p) (he : Executes (fun (x : C) (o : D.signature.A) (a : D.signature.B o) (y : C) (ts : List τ) => Executes exec (M.methods o) x a y ts) p c a c' chunks) : ∃ (s' : D.State) (tr_D : D.Transcript) (e' : E.State), D.ClientRun s p a s' tr_D ∧ M.rep s' e' ∧ R.rep e' c' ∧ total (total weight) chunks + potential s' e' ≤ D.totalCostTranscript charge s tr_D + potential s e

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

theorem Cslib.DataStructure.Module.amortized_client {D E : StateTransitionSpec} {C τ : Type x} {α : Type y} (M : Module D E) {exec : Execution E.signature C τ} {fD : D.State → (o : D.Op) → D.State × D.Result o} {fE : E.State → (o : E.Op) → E.State × E.Result o} [D.HasStepFn fD] [E.HasStepFn fE] (R : StateTransitionImpl 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.clientHistory e (M.methods o)) + potential (D.stepFn s o).1 (E.clientState e (M.methods o)) ≤ 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.clientHistory s p)) (he : Executes (fun (x : C) (o : D.signature.A) (a : D.signature.B 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.clientState s p) e' ∧ R.rep e' c' ∧ total (total weight) chunks + potential (D.clientState s p) e' ≤ D.totalCost charge s (D.clientHistory s p) + potential s e

Hidden representation credit telescopes along an arbitrary adaptive upper client on deterministic specifications.

theorem Cslib.DataStructure.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.