Composing verified interface implementations

Modules compose by substituting method bodies and composing representation relations. The intermediate state remains hidden, so callers need not depend on either representation. This construction shares the same semantics across all backend and resource interpretations.

Main definitions

• Module.id: the identity implementation of an interface.
• Module.comp: composition of two verified interface implementations.

Main results

• Module.simulates_client: semantic refinement lifts through an adaptive client.
• link_comp: composing methods agrees with consecutive linking.

theorem Cslib.Stateful.Module.simulates_client {D E : Spec} {α : Type w} (M : Module D E) (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.ValidHistory e (E.runClient e (link M.methods p)).2.2 ∧ (E.runClient e (link M.methods p)).1 = (D.runClient s p).1 ∧ M.rep (D.runClient s p).2.1 (E.runClient e (link M.methods p)).2.1

Per-operation semantic simulations lift to the whole answer-dependent client.

def Cslib.Stateful.Module.id (D : Spec) : Module D D

Identity methods expose precisely one call and preserve the state representation.

def Cslib.Stateful.Module.comp {D E F : Spec} (M : Module D E) (N : Module E F) : Module D F

Compose implementation proofs while hiding the intermediate representation.

theorem Cslib.Stateful.link_comp {D E F : Spec} {α : Type w} (f : Methods D E) (g : Methods E F) (p : D.Client α) : link g (link f p) = link (fun (o : D.Op) => link g (f o)) p

Consecutive linking is the same program as linking the composed method table.