Refinements by abstraction functions and stacked potentials

A Refinement D E is a Module D E whose representation is single-valued: an implementation invariant on lower states together with an abstraction function abs : E.State → D.State. Each method, run from a lower state satisfying the invariant, must realize the specified step at the abstract state, ending in a state satisfying the invariant. On deterministic specifications (Refinement.ofFn) the obligation reads D.stepFn (abs e) o = (abs e', a).

A single-valued representation is what makes amortized costs compose. Refinement.Amortized asks that every method satisfy the physicist's inequality lower cost + potential e' ≤ upper (abs e) o + potential e, with a potential on lower states. Composing two refinements adds their potentials, the upper one read through the lower abstraction (Refinement.Amortized.comp). A relational representation would leave the intermediate state existential, and the composed potential would not be a function of the lower state. For the same reason an amortized refinement over a native implementation whose representation is functional yields an Amortized certificate of the realized module (Refinement.Amortized.realize).

Products of refinements over one lower interface (Refinement.prod) need non-interference: the methods of each side leave the other side's abstraction, invariant and potential unchanged. A joint invariant, such as the disjointness of the memory the two sides use, may be part of the product's invariant. Memory.Framed.prod discharges these obligations from footprints.

Glue. A realization charges, besides each lower call, the glue code that consumes its answer. In a free-monad program every bind follows exactly one call, so glue charged per bind is a further charge per lower call, and Refinement.Amortized.glue absorbs it at a constant rate when it is at most proportional to the call's charge plus one. Work not attached to a lower call, such as a loop iteration that makes no call, is charged per call one level up and added with Refinement.Amortized.add.

Main definitions

• Refinement: a module given by methods, an implementation invariant and an abstraction function.
• Refinement.ofFn: the constructor for deterministic specifications.
• Refinement.toModule: the underlying relational module.
• Refinement.id, Refinement.comp, Refinement.prod: identity, composition, and products under non-interference.
• Methods.prod: the methods of both sides of a product.
• Refinement.Amortized: per-method amortized cost refinement with a potential on lower states.
• productCharge: componentwise charges of a product specification.

The transcript-cost lemmas StateTransitionSpec.totalCostTranscript_mono, StateTransitionSpec.totalCostTranscript_mul_left and StateTransitionSpec.totalCostTranscript_add sit here, beside their only clients, rather than in the widely imported StateTransition module.

Main results

• Refinement.simulates_demonic, Refinement.simulates_client: whole adaptive clients run through the abstraction function.
• Refinement.comp_rep_iff: composition agrees with Module.comp of the underlying modules.
• Refinement.Amortized.demonic, Refinement.Amortized.client: potentials telescope along adaptive clients.
• Refinement.Amortized.comp: potentials stack across composition.
• Refinement.Amortized.prod: potentials add across non-interfering products.
• Refinement.Amortized.realize: an amortized certificate for the realized module.
• Refinement.Amortized.id: the identity refinement passes charges through.
• Refinement.Amortized.mono, Refinement.Amortized.mul_left, Refinement.Amortized.add: weaken charges, exchange both currencies at a constant rate, and add certificates.
• Refinement.Amortized.glue, Refinement.Amortized.glue_of_one_le: absorb glue charged per lower call.
• StateTransitionSpec.totalCost_glue_le: the same on a history.
• productCharge_const: equal constant charges on a product.
• StateTransitionSpec.totalCostTranscript_mono, StateTransitionSpec.totalCostTranscript_mul_left, StateTransitionSpec.totalCostTranscript_add: monotonicity, scaling and additivity of transcript costs.
• Refinement.Amortized.chargeBound, Refinement.Amortized.of_chargeBound: with zero potential, the existing worst-case Module.ChargeBound.

References

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

structure Cslib.DataStructure.Refinement (D E : StateTransitionSpec) : Type (max (max u v) w)

A module whose representation is an implementation invariant inv together with an abstraction function abs. From a lower state satisfying inv, every run of a method on an admissible operation realizes a permitted step of the abstract state and preserves inv.

• methods : Methods D E

  Bodies implementing the upper interface using lower-interface calls.

• inv : E.State → Prop

  The implementation invariant on lower states.

• abs : E.State → D.State

  The abstraction function from lower states to upper states.

• valid {e : E.State} (o : D.Op) : self.inv e → D.valid (self.abs e) o → E.DemonicValid e (self.methods o)

  Each method is demonically admissible from a state satisfying the invariant.

• correct {e : E.State} (o : D.Op) {a : D.Result o} {e' : E.State} {tr : E.Transcript} : self.inv e → D.valid (self.abs e) o → E.ClientRun e (self.methods o) a e' tr → D.step (self.abs e) o (self.abs e') a ∧ self.inv e'

  Each method run realizes the specified step through abs and preserves inv.

def Cslib.DataStructure.Methods.prod {E D₁ D₂ : StateTransitionSpec} (m₁ : Methods D₁ E) (m₂ : Methods D₂ E) : Methods (product D₁ D₂) E

The methods of both sides of a product, over one lower interface.

def Cslib.DataStructure.productCharge {D₁ D₂ : StateTransitionSpec} (c₁ : D₁.State → D₁.Op → ℕ) (c₂ : D₂.State → D₂.Op → ℕ) : (product D₁ D₂).State → (product D₁ D₂).Op → ℕ

Componentwise charges of a product specification.

@[simp]

theorem Cslib.DataStructure.productCharge_const {D₁ D₂ : StateTransitionSpec} (K : ℕ) : (productCharge (fun (x : D₁.State) (x_1 : D₁.Op) => K) fun (x : D₂.State) (x_1 : D₂.Op) => K) = fun (x : (product D₁ D₂).State) (x_1 : (product D₁ D₂).Op) => K

Equal constant charges on both components are that constant charge on the product.

theorem Cslib.DataStructure.StateTransitionSpec.totalCostTranscript_mono {D : StateTransitionSpec} {c c' : D.State → D.Op → ℕ} (h : ∀ (s : D.State) (o : D.Op), c s o ≤ c' s o) (s : D.State) (tr : D.Transcript) : D.totalCostTranscript c s tr ≤ D.totalCostTranscript c' s tr

Smaller charges total less along any transcript.

theorem Cslib.DataStructure.StateTransitionSpec.totalCostTranscript_mul_left {D : StateTransitionSpec} (K : ℕ) (c : D.State → D.Op → ℕ) (s : D.State) (tr : D.Transcript) : D.totalCostTranscript (fun (s : D.State) (o : D.Op) => K * c s o) s tr = K * D.totalCostTranscript c s tr

Scaling every charge by K scales the total by K.

theorem Cslib.DataStructure.StateTransitionSpec.totalCostTranscript_add {D : StateTransitionSpec} (c c' : D.State → D.Op → ℕ) (s : D.State) (tr : D.Transcript) : D.totalCostTranscript (fun (s : D.State) (o : D.Op) => c s o + c' s o) s tr = D.totalCostTranscript c s tr + D.totalCostTranscript c' s tr

Charges add along a transcript.

theorem Cslib.DataStructure.StateTransitionSpec.totalCost_glue_le {D : StateTransitionSpec} {fD : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn fD] {lower glue : D.State → D.Op → ℕ} {K : ℕ} (hone : ∀ (s : D.State) (o : D.Op), 1 ≤ lower s o) (hglue : ∀ (s : D.State) (o : D.Op), glue s o ≤ K * (lower s o + 1)) (s : D.State) (os : List D.Op) : D.totalCost (fun (s : D.State) (o : D.Op) => lower s o + glue s o) s os ≤ (2 * K + 1) * D.totalCost lower s os

Glue on a history. Glue charged with each operation at most K times its charge plus K costs, together with the charges, at most 2 K + 1 times the charges, when every operation costs at least one unit.

@[reducible, inline]

abbrev Cslib.DataStructure.Refinement.ofFn {D E : StateTransitionSpec} {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] (methods : Methods D E) (inv : E.State → Prop) (abs : E.State → D.State) (valid : ∀ {e : E.State} (o : D.Op), inv e → D.valid (abs e) o → E.ValidHistory e (E.clientHistory e (methods o))) (correct : ∀ {e : E.State} (o : D.Op), inv e → D.valid (abs e) o → D.stepFn (abs e) o = (abs (E.clientState e (methods o)), E.clientResult e (methods o)) ∧ inv (E.clientState e (methods o))) : Refinement D E

The constructor for deterministic specifications: each method's history is admissible, and D.stepFn (abs e) o = (abs e', a) for its final state e' and result a.

def Cslib.DataStructure.Refinement.toModule {D E : StateTransitionSpec} (M : Refinement D E) : Module D E

The underlying relational module: s is represented by e when e satisfies the invariant and abstracts to s.

theorem Cslib.DataStructure.Refinement.simulates_demonic {D E : StateTransitionSpec} {α : Type w} (M : Refinement D E) (p : D.Client α) {e : E.State} (he : M.inv e) (hv : D.DemonicValid (M.abs e) p) : E.DemonicValid e (link M.methods p) ∧ ∀ (a : α) (e' : E.State) (tr_E : E.Transcript), E.ClientRun e (link M.methods p) a e' tr_E → M.inv e' ∧ ∃ (tr_D : D.Transcript), D.ClientRun (M.abs e) p a (M.abs e') tr_D

Every run of a linked admissible client corresponds to a run of the client at the abstract state, ending at the abstraction of the final lower state.

theorem Cslib.DataStructure.Refinement.simulates_client {D E : StateTransitionSpec} {α : Type w} (M : Refinement D E) {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] (p : D.Client α) {e : E.State} (he : M.inv e) (hv : D.ValidHistory (M.abs e) (D.clientHistory (M.abs e) p)) : E.ValidHistory e (E.clientHistory e (link M.methods p)) ∧ E.clientResult e (link M.methods p) = D.clientResult (M.abs e) p ∧ M.abs (E.clientState e (link M.methods p)) = D.clientState (M.abs e) p ∧ M.inv (E.clientState e (link M.methods p))

On deterministic specifications, a linked client returns the specified result, and its final lower state satisfies the invariant and abstracts to the specified final state.

def Cslib.DataStructure.Refinement.id (D : StateTransitionSpec) : Refinement D D

The identity refinement: each operation calls itself, with no invariant.

def Cslib.DataStructure.Refinement.comp {D E F : StateTransitionSpec} (M : Refinement D E) (N : Refinement E F) : Refinement D F

Composition: the upper methods are linked through the lower ones, the invariants conjoin, and the abstraction functions compose.

theorem Cslib.DataStructure.Refinement.comp_rep_iff {D E F : StateTransitionSpec} (M : Refinement D E) (N : Refinement E F) (s : D.State) (f : F.State) : (M.comp N).toModule.rep s f ↔ (M.toModule.comp N.toModule).rep s f

Composing refinements represents the same states as composing their modules.

theorem Cslib.DataStructure.Refinement.link_comp {D E F : StateTransitionSpec} {α : Type w} (M : Refinement D E) (N : Refinement E F) (p : D.Client α) : link (M.comp N).methods p = link N.methods (link M.methods p)

Linking through a composition links through each refinement in turn.

def Cslib.DataStructure.Refinement.prod {E D₁ D₂ : StateTransitionSpec} (M₁ : Refinement D₁ E) (M₂ : Refinement D₂ E) (J : E.State → Prop) (frame₁ : ∀ {e : E.State} (o : D₁.Op) {a : D₁.Result o} {e' : E.State} {tr : E.Transcript}, M₁.inv e → M₂.inv e → J e → D₁.valid (M₁.abs e) o → E.ClientRun e (M₁.methods o) a e' tr → M₂.abs e' = M₂.abs e ∧ M₂.inv e' ∧ J e') (frame₂ : ∀ {e : E.State} (o : D₂.Op) {a : D₂.Result o} {e' : E.State} {tr : E.Transcript}, M₁.inv e → M₂.inv e → J e → D₂.valid (M₂.abs e) o → E.ClientRun e (M₂.methods o) a e' tr → M₁.abs e' = M₁.abs e ∧ M₁.inv e' ∧ J e') : Refinement (product D₁ D₂) E

Two refinements over one lower interface implement the product of their specifications, provided the methods of each leave the other's abstraction and invariant unchanged. The joint invariant J holds of the shared lower state and is preserved by both sides; it records what keeps them apart, such as the disjointness of the memory each one uses.

Amortized costs

structure Cslib.DataStructure.Refinement.Amortized {D E : StateTransitionSpec} (M : Refinement D E) (lower : E.State → E.Op → ℕ) (upper : D.State → D.Op → ℕ) (potential : E.State → ℕ) : Prop

Amortized cost refinement: the lower charges of every method run, plus the potential after it, are at most the upper charge of the operation plus the potential before it. Potentials are natural numbers, hence nonnegative; a client bound subtracts nothing when the initial potential is zero.

• step {e : E.State} (o : D.Op) {a : D.Result o} {e' : E.State} {tr : E.Transcript} : M.inv e → D.valid (M.abs e) o → E.ClientRun e (M.methods o) a e' tr → E.totalCostTranscript lower e tr + potential e' ≤ upper (M.abs e) o + potential e

  The physicist's inequality for one method run.

theorem Cslib.DataStructure.Refinement.Amortized.ofFn {D E : StateTransitionSpec} {M : Refinement D E} {lower : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} {potential : E.State → ℕ} {fE : E.State → (o : E.Op) → E.State × E.Result o} [E.HasStepFn fE] (h : ∀ {e : E.State} (o : D.Op), M.inv e → D.valid (M.abs e) o → E.totalCost lower e (E.clientHistory e (M.methods o)) + potential (E.clientState e (M.methods o)) ≤ upper (M.abs e) o + potential e) : M.Amortized lower upper potential

The amortized inequality on a deterministic lower specification, along each method's history.

theorem Cslib.DataStructure.Refinement.Amortized.mono {D E : StateTransitionSpec} {M : Refinement D E} {lower : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} {potential : E.State → ℕ} (A : M.Amortized lower upper potential) {lower' : E.State → E.Op → ℕ} {upper' : D.State → D.Op → ℕ} (hlower : ∀ (e : E.State) (o : E.Op), lower' e o ≤ lower e o) (hupper : ∀ (s : D.State) (o : D.Op), D.valid s o → upper s o ≤ upper' s o) : M.Amortized lower' upper' potential

Weaker charges: cheaper lower charges and dearer upper charges on admissible operations.

theorem Cslib.DataStructure.Refinement.Amortized.mul_left {D E : StateTransitionSpec} {M : Refinement D E} {lower : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} {potential : E.State → ℕ} (A : M.Amortized lower upper potential) (K : ℕ) : M.Amortized (fun (e : E.State) (o : E.Op) => K * lower e o) (fun (s : D.State) (o : D.Op) => K * upper s o) fun (e : E.State) => K * potential e

Exchange at a constant rate. Scaling both currencies and the potential by K preserves the amortized inequality.

theorem Cslib.DataStructure.Refinement.Amortized.add {D E : StateTransitionSpec} {M : Refinement D E} {lower : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} {potential : E.State → ℕ} (A : M.Amortized lower upper potential) {lower' : E.State → E.Op → ℕ} {upper' : D.State → D.Op → ℕ} {potential' : E.State → ℕ} (B : M.Amortized lower' upper' potential') : M.Amortized (fun (e : E.State) (o : E.Op) => lower e o + lower' e o) (fun (s : D.State) (o : D.Op) => upper s o + upper' s o) fun (e : E.State) => potential e + potential' e

Two certificates of one refinement add: their lower charges, upper charges and potentials.

theorem Cslib.DataStructure.Refinement.Amortized.glue {D E : StateTransitionSpec} {M : Refinement D E} {lower : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} {potential : E.State → ℕ} (A : M.Amortized lower upper potential) {calls : D.State → D.Op → ℕ} {Ψ : E.State → ℕ} (B : M.Amortized (fun (x : E.State) (x_1 : E.Op) => 1) calls Ψ) {glue : E.State → E.Op → ℕ} {K : ℕ} (hglue : ∀ (e : E.State) (o : E.Op), glue e o ≤ K * (lower e o + 1)) : M.Amortized (fun (e : E.State) (o : E.Op) => lower e o + glue e o) (fun (s : D.State) (o : D.Op) => (K + 1) * upper s o + K * calls s o) fun (e : E.State) => (K + 1) * potential e + K * Ψ e

Glue charges. A realization of the lower interface charges, besides each lower call, the glue that consumes its answer: in a free-monad program every bind follows exactly one call. If the glue charged with a call is at most K times the call's charge plus K, a certificate for the charges and one for the number of calls give a certificate for the combined charge. Work that is not attached to a lower call, such as the iterations of a loop that makes no call, is a further per-call charge of the upper interface, added with Amortized.add one level up.

theorem Cslib.DataStructure.Refinement.Amortized.glue_of_one_le {D E : StateTransitionSpec} {M : Refinement D E} {lower : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} {potential : E.State → ℕ} (A : M.Amortized lower upper potential) (hone : ∀ (e : E.State) (o : E.Op), 1 ≤ lower e o) {glue : E.State → E.Op → ℕ} {K : ℕ} (hglue : ∀ (e : E.State) (o : E.Op), glue e o ≤ K * (lower e o + 1)) : M.Amortized (fun (e : E.State) (o : E.Op) => lower e o + glue e o) (fun (s : D.State) (o : D.Op) => (2 * K + 1) * upper s o) fun (e : E.State) => (2 * K + 1) * potential e

Glue charges, when every call costs at least one unit, as every memory operation does: then the calls are paid for by their charges, and the combined charge is amortized at 2 K + 1 times the upper charge.

theorem Cslib.DataStructure.Refinement.Amortized.demonic {D E : StateTransitionSpec} {α : Type w} {M : Refinement D E} {lower : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} {potential : E.State → ℕ} (A : M.Amortized lower upper potential) (p : D.Client α) {e e' : E.State} {a : α} {tr_E : E.Transcript} (he : M.inv e) (hv : D.DemonicValid (M.abs e) p) (hrun : E.ClientRun e (link M.methods p) a e' tr_E) : M.inv e' ∧ ∃ (tr_D : D.Transcript), D.ClientRun (M.abs e) p a (M.abs e') tr_D ∧ E.totalCostTranscript lower e tr_E + potential e' ≤ D.totalCostTranscript upper (M.abs e) tr_D + potential e

Potentials telescope along any run of a linked admissible client.

theorem Cslib.DataStructure.Refinement.Amortized.client {D E : StateTransitionSpec} {α : Type w} {M : Refinement D E} {lower : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} {potential : E.State → ℕ} {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] (A : M.Amortized lower upper potential) (p : D.Client α) {e : E.State} (he : M.inv e) (hv : D.ValidHistory (M.abs e) (D.clientHistory (M.abs e) p)) : E.totalCost lower e (E.clientHistory e (link M.methods p)) + potential (E.clientState e (link M.methods p)) ≤ D.totalCost upper (M.abs e) (D.clientHistory (M.abs e) p) + potential e

On deterministic specifications, the lower charges of a linked client plus the final potential are at most the upper charges of its history plus the initial potential.

theorem Cslib.DataStructure.Refinement.Amortized.comp {D E F : StateTransitionSpec} {M : Refinement D E} {upper : D.State → D.Op → ℕ} {N : Refinement E F} {lower : F.State → F.Op → ℕ} {middle : E.State → E.Op → ℕ} {Φ : E.State → ℕ} {Ψ : F.State → ℕ} (A : M.Amortized middle upper Φ) (B : N.Amortized lower middle Ψ) : (M.comp N).Amortized lower upper fun (f : F.State) => Φ (N.abs f) + Ψ f

Potentials stack across composition. If the upper refinement is amortized against the middle charges and the lower refinement is amortized from the middle charges, the composite is amortized with the sum of the upper potential, read through the lower abstraction, and the lower potential.

theorem Cslib.DataStructure.Refinement.Amortized.prod {E D₁ D₂ : StateTransitionSpec} {lower : E.State → E.Op → ℕ} {M₁ : Refinement D₁ E} {M₂ : Refinement D₂ E} {J : E.State → Prop} {frame₁ : ∀ {e : E.State} (o : D₁.Op) {a : D₁.Result o} {e' : E.State} {tr : E.Transcript}, M₁.inv e → M₂.inv e → J e → D₁.valid (M₁.abs e) o → E.ClientRun e (M₁.methods o) a e' tr → M₂.abs e' = M₂.abs e ∧ M₂.inv e' ∧ J e'} {frame₂ : ∀ {e : E.State} (o : D₂.Op) {a : D₂.Result o} {e' : E.State} {tr : E.Transcript}, M₁.inv e → M₂.inv e → J e → D₂.valid (M₂.abs e) o → E.ClientRun e (M₂.methods o) a e' tr → M₁.abs e' = M₁.abs e ∧ M₁.inv e' ∧ J e'} {upper₁ : D₁.State → D₁.Op → ℕ} {upper₂ : D₂.State → D₂.Op → ℕ} {Φ₁ Φ₂ : E.State → ℕ} (A₁ : M₁.Amortized lower upper₁ Φ₁) (A₂ : M₂.Amortized lower upper₂ Φ₂) (potential₁ : ∀ {e : E.State} (o : D₁.Op) {a : D₁.Result o} {e' : E.State} {tr : E.Transcript}, M₁.inv e → M₂.inv e → J e → D₁.valid (M₁.abs e) o → E.ClientRun e (M₁.methods o) a e' tr → Φ₂ e' = Φ₂ e) (potential₂ : ∀ {e : E.State} (o : D₂.Op) {a : D₂.Result o} {e' : E.State} {tr : E.Transcript}, M₁.inv e → M₂.inv e → J e → D₂.valid (M₂.abs e) o → E.ClientRun e (M₂.methods o) a e' tr → Φ₁ e' = Φ₁ e) : (M₁.prod M₂ J ⋯ ⋯).Amortized lower (productCharge upper₁ upper₂) fun (e : E.State) => Φ₁ e + Φ₂ e

Potentials add across non-interfering products, provided the methods of each side leave the other side's potential unchanged.

theorem Cslib.DataStructure.Refinement.Amortized.realize {D E : StateTransitionSpec} {M : Refinement D E} {lower : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} {potential : E.State → ℕ} (A : M.Amortized lower upper potential) {C τ : Type x} {exec : Execution E.signature C τ} {R : StateTransitionImpl E exec} {weight : τ → ℕ} {ψ : E.State → C → ℕ} (B : DataStructure.Amortized R weight ψ lower) (absR : C → E.State) (hR : ∀ {e : E.State} {c : C}, R.rep e c → e = absR c) : DataStructure.Amortized (M.toModule.realize R) (total weight) (fun (x : D.State) (c : C) => potential (absR c) + ψ (absR c) c) upper

Potentials stack through a realization. An amortized refinement over a native implementation with an amortized certificate yields an amortized certificate of the realized module, provided the native representation is functional: the represented lower state is absR c.

theorem Cslib.DataStructure.Refinement.Amortized.id {D : StateTransitionSpec} (charge : D.State → D.Op → ℕ) : (Refinement.id D).Amortized charge charge fun (x : D.State) => 0

The identity refinement passes each charge through unchanged.

theorem Cslib.DataStructure.Refinement.Amortized.chargeBound {D E : StateTransitionSpec} {M : Refinement D E} {lower : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} (A : M.Amortized lower upper fun (x : E.State) => 0) : M.toModule.ChargeBound lower upper

With zero potential, an amortized refinement is a worst-case Module.ChargeBound of its module.

theorem Cslib.DataStructure.Refinement.Amortized.of_chargeBound {D E : StateTransitionSpec} {M : Refinement D E} {lower : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} (B : M.toModule.ChargeBound lower upper) : M.Amortized lower upper fun (x : E.State) => 0

A worst-case Module.ChargeBound of the module is an amortized refinement with zero potential.