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_demonic: relational semantic refinement lifts through a demonically admissible adaptive client.
• Module.simulates_client: deterministic specialization of simulates_demonic for [D.HasStepFn fD] and [E.HasStepFn fE].
• link_comp: composing methods agrees with consecutive linking.

References

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

theorem Cslib.DataStructure.Module.simulates_demonic {D E : StateTransitionSpec} {α : Type w} (M : Module D E) (p : D.Client α) {s : D.State} {e : E.State} (hr : M.rep s e) (hv : D.DemonicValid s 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 → ∃ (s' : D.State) (tr_D : D.Transcript), D.ClientRun s p a s' tr_D ∧ M.rep s' e'

Per-operation relational simulations lift to any demonically admissible adaptive client.

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

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

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

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

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

Compose implementation proofs while hiding the intermediate representation.

theorem Cslib.DataStructure.link_comp {D E F : StateTransitionSpec} {α : 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.