Resource contracts across stateful interfaces

A client contract combines admissibility, a postcondition and a bound on state-dependent operation charges. Semantic modules transport these contracts using separate method budgets; native realizations 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. Existence of native executions does not assert that every execution of a nondeterministic backend terminates.

Main definitions

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

Main results

• Spec.CostHoare.bind: compose contracts using an intermediate postcondition.
• Module.ChargeBound.client: transfer costs along an adaptive linked client.
• Module.ChargeBound.comp: compose resource certificates through hidden representations.
• Spec.CostHoare.link: transport a contract to a lower interface.
• Spec.CostHoare.realize, Spec.CostHoare.run: native correctness, bounds and existence.

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

Admissibility and a postcondition, together with a bound on charged operations. The budget is evaluated at the initial state; it does not charge pure Lean computation.

theorem Cslib.Stateful.Spec.CostHoare.hoare {D : Spec} {α : 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.Stateful.Spec.CostHoare.pure {D : Spec} {α : 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.Stateful.Spec.CostHoare.call {D : Spec} {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 ∧ post (D.step s o).2 (D.step 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

A call exposes its specified answer and charges the supplied operation budget.

theorem Cslib.Stateful.Spec.CostHoare.bind {D : Spec} {α β : 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 the intermediate abstract state, retaining answer-dependent costs.

theorem Cslib.Stateful.Spec.CostHoare.consequence {D : Spec} {α : 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.Stateful.Spec.CostHoare.realize {D : Spec} {α : 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 C τ} {R : Realization 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.Stateful.Spec.CostHoare.run {D : Spec} {α : 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 C τ} {R : Realization 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.Stateful.Module.ChargeBound {D E : Spec} (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.Stateful.Module.ChargeBound.client {D E : Spec} {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.runClient s p).2.2) : E.totalCost lower e (E.runClient e (link M.methods p)).2.2 ≤ D.totalCost upper s (D.runClient s p).2.2

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

theorem Cslib.Stateful.Module.ChargeBound.comp {D E F : Spec} {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.Stateful.Module.ChargeBound.realize {D E : Spec} {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 C τ} (R : Realization 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.Stateful.Spec.CostHoare.link {D E : Spec} {α : 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) (Stateful.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.