Resource contracts across stateful interfaces

A client contract combines demonic admissibility, a postcondition and a bound on state-dependent operation charges across all permitted client runs. Semantic modules transport these contracts using separate method budgets; native implementations then interpret the charges as additive measures of execution evidence. This supports proofs at several interface levels without choosing a backend in the client proof.

These are operation-cost contracts. Pure results and host-language continuations incur no charge in this interpretation. A total machine-time theorem additionally needs certificates for the controller, argument preparation and result decoding.

Main definitions

• StateTransitionSpec.CostHoare: a demonic semantic client contract with an initial-state-dependent budget.
• Module.ChargeBound: lower method costs are bounded by upper operation charges.

Main results

• StateTransitionSpec.CostHoare.pure, StateTransitionSpec.CostHoare.call, StateTransitionSpec.CostHoare.call_ofFn, StateTransitionSpec.CostHoare.bind, StateTransitionSpec.CostHoare.consequence: compositional contract rules.
• StateTransitionSpec.costHoare_iff_ofFn: equivalence with the functional runClient formulation on deterministic specifications ([D.HasStepFn f]).
• Module.ChargeBound.demonic, Module.ChargeBound.client, Module.ChargeBound.comp, Module.ChargeBound.realize: transfer and compose method resource bounds across linked clients and implementations.
• StateTransitionSpec.CostHoare.link: transport a contract to a lower interface.
• StateTransitionSpec.CostHoare.realize, StateTransitionSpec.CostHoare.realize_amortized, StateTransitionSpec.CostHoare.exists_executes: native correctness, bounds and existence.

References

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

def Cslib.DataStructure.StateTransitionSpec.CostHoare {D : StateTransitionSpec} {α : Type y} (charge : D.State → D.Op → ℕ) (pre : D.State → Prop) (p : D.Client α) (post : α → D.State → Prop) (budget : D.State → ℕ) : Prop

Demonic CostHoare triple: strengthens D.Hoare with a worst-case abstract charge bound D.totalCostTranscript charge s tr ≤ budget s across every valid ClientRun. The budget is evaluated at the initial state; it does not charge pure Lean computation.

theorem Cslib.DataStructure.StateTransitionSpec.costHoare_iff_ofFn {D : StateTransitionSpec} {α : Type y} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (charge : D.State → D.Op → ℕ) (pre : D.State → Prop) (p : D.Client α) (post : α → D.State → Prop) (budget : D.State → ℕ) : CostHoare charge pre p post budget ↔ Hoare pre p post ∧ ∀ (s : D.State), pre s → D.totalCost charge s (D.clientHistory s p) ≤ budget s

On a deterministic specification ([D.HasStepFn f]), D.CostHoare is equivalent to D.Hoare pre p post ∧ ∀ s, pre s → D.totalCost charge s (D.clientHistory s p) ≤ budget s.

theorem Cslib.DataStructure.StateTransitionSpec.CostHoare.hoare {D : StateTransitionSpec} {α : Type y} {charge : D.State → D.Op → ℕ} {pre : D.State → Prop} {post : α → D.State → Prop} {budget : D.State → ℕ} {p : D.Client α} (h : CostHoare charge pre p post budget) : Hoare pre p post

Forget the resource bound while retaining semantic correctness.

theorem Cslib.DataStructure.StateTransitionSpec.CostHoare.pure {D : StateTransitionSpec} {α : Type y} {charge : D.State → D.Op → ℕ} {pre : D.State → Prop} {post : α → D.State → Prop} (a : α) (h : ∀ (s : D.State), pre s → post a s) : CostHoare charge pre (PFunctor.FreeM.pure a) post fun (x : D.State) => 0

Returning a value has zero operation cost.

theorem Cslib.DataStructure.StateTransitionSpec.CostHoare.call {D : StateTransitionSpec} {charge : D.State → D.Op → ℕ} {pre : D.State → Prop} (o : D.Op) {post : D.Result o → D.State → Prop} (h : ∀ (s : D.State), pre s → D.valid s o ∧ ∀ (s' : D.State) (a : D.Result o), D.step s o s' a → post a s') : CostHoare charge pre (PFunctor.FreeM.liftBind o fun (a : D.signature.B o) => PFunctor.FreeM.pure a) post fun (s : D.State) => charge s o

Calling a single operation requires D.valid s o, establishes post a s' for every permitted outcome D.step s o s' a, and charges charge s o at the pre-state s.

theorem Cslib.DataStructure.StateTransitionSpec.CostHoare.call_ofFn {D : StateTransitionSpec} {charge : D.State → D.Op → ℕ} {pre : D.State → Prop} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (o : D.Op) {post : D.Result o → D.State → Prop} (h : ∀ (s : D.State), pre s → D.valid s o ∧ post (D.stepFn s o).2 (D.stepFn s o).1) : CostHoare charge pre (PFunctor.FreeM.liftBind o fun (a : D.signature.B o) => PFunctor.FreeM.pure a) post fun (s : D.State) => charge s o

On a deterministic specification ([D.HasStepFn f]), calling an operation exposes (D.stepFn s o) and charges charge s o.

theorem Cslib.DataStructure.StateTransitionSpec.CostHoare.bind {D : StateTransitionSpec} {α β : Type y} {charge : D.State → D.Op → ℕ} {pre : D.State → Prop} {budget : D.State → ℕ} {p : D.Client α} {mid : α → D.State → Prop} {post : β → D.State → Prop} {k : α → D.Client β} {first : D.State → ℕ} {next : α → D.State → ℕ} (hp : CostHoare charge pre p mid first) (hk : ∀ (a : α), CostHoare charge (mid a) (k a) post (next a)) (hb : ∀ (s : D.State), pre s → ∀ (a : α) (s' : D.State), mid a s' → first s + next a s' ≤ budget s) : CostHoare charge pre (PFunctor.FreeM.bind p k) post budget

Compose budgets at every intermediate abstract state satisfying mid.

theorem Cslib.DataStructure.StateTransitionSpec.CostHoare.consequence {D : StateTransitionSpec} {α : Type y} {charge : D.State → D.Op → ℕ} {pre : D.State → Prop} {post : α → D.State → Prop} {budget : D.State → ℕ} {p : D.Client α} {pre' : D.State → Prop} {post' : α → D.State → Prop} {budget' : D.State → ℕ} (h : CostHoare charge pre p post budget) (hp : ∀ (s : D.State), pre' s → pre s) (hq : ∀ (a : α) (s : D.State), post a s → post' a s) (hb : ∀ (s : D.State), pre' s → budget s ≤ budget' s) : CostHoare charge pre' p post' budget'

Strengthen the precondition and weaken the postcondition or budget.

theorem Cslib.DataStructure.StateTransitionSpec.CostHoare.realize_amortized {D : StateTransitionSpec} {α : Type y} {charge : D.State → D.Op → ℕ} {pre : D.State → Prop} {post : α → D.State → Prop} {budget : D.State → ℕ} {p : D.Client α} {C τ : Type x} {exec : Execution D.signature C τ} {R : StateTransitionImpl D exec} {weight : τ → ℕ} {potential : D.State → C → ℕ} (A : Amortized R weight potential charge) (h : CostHoare charge pre p post budget) {s : D.State} {c c' : C} {a : α} {traces : List τ} (hs : pre s) (hr : R.rep s c) (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' ∧ post a s' ∧ total weight traces + potential s' c' ≤ budget s + potential s c

Transport a demonic CostHoare triple through an Amortized certificate to bound native execution weight plus final potential by budget s + potential s c.

theorem Cslib.DataStructure.StateTransitionSpec.CostHoare.realize {D : StateTransitionSpec} {α : Type y} {charge : D.State → D.Op → ℕ} {pre : D.State → Prop} {post : α → D.State → Prop} {budget : D.State → ℕ} {p : D.Client α} {C τ : Type x} {exec : Execution D.signature C τ} {R : StateTransitionImpl D exec} {weight : τ → ℕ} (B : Bound R weight charge) (h : CostHoare charge pre p post budget) {s : D.State} {c c' : C} {a : α} {traces : List τ} (hs : pre s) (hr : R.rep s c) (he : Executes exec p c a c' traces) : (∃ (s' : D.State), R.rep s' c' ∧ post a s') ∧ total weight traces ≤ budget s

Every supplied native execution satisfies the contract and its interpreted resource bound.

theorem Cslib.DataStructure.StateTransitionSpec.CostHoare.exists_executes {D : StateTransitionSpec} {α : Type y} {charge : D.State → D.Op → ℕ} {pre : D.State → Prop} {post : α → D.State → Prop} {budget : D.State → ℕ} {p : D.Client α} {C τ : Type x} {exec : Execution D.signature C τ} {R : StateTransitionImpl D exec} {weight : τ → ℕ} (B : Bound R weight charge) (h : CostHoare charge pre p post budget) {s : D.State} {c : C} (hs : pre s) (hr : R.rep s c) : ∃ (a : α) (c' : C) (traces : List τ), Executes exec p c a c' traces ∧ (∃ (s' : D.State), R.rep s' c' ∧ post a s') ∧ total weight traces ≤ budget s

A represented initial state has a native execution meeting the contract and budget.

def Cslib.DataStructure.Module.ChargeBound {D E : StateTransitionSpec} (M : Module D E) (lower : E.State → E.Op → ℕ) (upper : D.State → D.Op → ℕ) : Prop

Per-method resource refinement, separate from the module's semantic certificate.

theorem Cslib.DataStructure.Module.ChargeBound.ofFn {D E : StateTransitionSpec} {fE : E.State → (o : E.Op) → E.State × E.Result o} [E.HasStepFn fE] {M : Module D E} {lower : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} (h : ∀ {s : D.State} {e : E.State} (o : D.Op), M.rep s e → D.valid s o → E.totalCost lower e (E.clientHistory e (M.methods o)) ≤ upper s o) : M.ChargeBound lower upper

Construct a ChargeBound on a deterministic lower specification ([E.HasStepFn fE]) from a functional totalCost inequality along clientHistory.

theorem Cslib.DataStructure.Module.ChargeBound.demonic {D E : StateTransitionSpec} {M : Module D E} {lower : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} (B : M.ChargeBound lower upper) {α : Type w} (p : D.Client α) {s : D.State} {e e' : E.State} {a : α} {tr_E : E.Transcript} (hr : M.rep s e) (hv : D.DemonicValid s p) (hrun_E : E.ClientRun e (link M.methods p) a e' tr_E) : ∃ (s' : D.State) (tr_D : D.Transcript), D.ClientRun s p a s' tr_D ∧ M.rep s' e' ∧ E.totalCostTranscript lower e tr_E ≤ D.totalCostTranscript upper s tr_D

Method budgets compose along any demonically admissible client execution.

theorem Cslib.DataStructure.Module.ChargeBound.client {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] {M : Module D E} {lower : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} (B : M.ChargeBound lower upper) {α : Type w} (p : D.Client α) {s : D.State} {e : E.State} (hr : M.rep s e) (hv : D.ValidHistory s (D.clientHistory s p)) : E.totalCost lower e (E.clientHistory e (link M.methods p)) ≤ D.totalCost upper s (D.clientHistory s p)

Method budgets compose along the actual answer-dependent history of a client on deterministic specifications.

theorem Cslib.DataStructure.Module.ChargeBound.comp {D E F : StateTransitionSpec} {M : Module D E} {N : Module E F} {lower : F.State → F.Op → ℕ} {middle : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} (B : M.ChargeBound middle upper) (C : N.ChargeBound lower middle) : (M.comp N).ChargeBound lower upper

Resource refinements compose while keeping the intermediate representation hidden.

theorem Cslib.DataStructure.Module.ChargeBound.realize {D E : StateTransitionSpec} {M : Module D E} {lower : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} (B : M.ChargeBound lower upper) {C τ : Type x} {exec : Execution E.signature C τ} (R : StateTransitionImpl E exec) {weight : τ → ℕ} (h : Bound R weight lower) : Bound (M.realize R) (total weight) upper

A method budget and a lower native certificate supply an upper native certificate.

theorem Cslib.DataStructure.StateTransitionSpec.CostHoare.link {D E : StateTransitionSpec} {α : Type w} {M : Module D E} {lower : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} (B : M.ChargeBound lower upper) {pre : D.State → Prop} {post : α → D.State → Prop} {p : D.Client α} {budget : D.State → ℕ} (h : CostHoare upper pre p post budget) (lowerBudget : E.State → ℕ) (hb : ∀ (s : D.State) (e : E.State), pre s → M.rep s e → budget s ≤ lowerBudget e) : CostHoare lower (fun (e : E.State) => ∃ (s : D.State), pre s ∧ M.rep s e) (DataStructure.link M.methods p) (fun (a : α) (e : E.State) => ∃ (s : D.State), post a s ∧ M.rep s e) lowerBudget

Transport a client contract and its budget across an interface implementation.