Compositional semantic implementations

A module implements one interface using operations of another. Linking uses the upstream free-monad interpreter. Behavior proofs neither choose a computational model nor assign costs. Module.realize composes representation relations and hides intermediate states existentially. Linking uses the upstream interpreter's common universe for operation answers and client results. Native execution itself permits an independent universe for client results.

Main definitions

• Methods: operation bodies over a lower interface.
• Module: demonic lower-call admissibility and angelic representation simulation for those bodies.
• Module.ofFn: constructor for deterministic upper and lower specifications.
• link: substitute lower method bodies into an adaptive client.

Main results

• Module.realize: implement a module with any implementation of its lower interface.
• link_exec, link_exec_decompose: exact correspondence of chunked and flattened executions.

References

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

@[reducible, inline]

abbrev Cslib.DataStructure.Methods (D E : StateTransitionSpec) : Type (max v w)

Interface methods are programs over another interface.

def Cslib.DataStructure.link {D E : StateTransitionSpec} {α : Type w} (methods : Methods D E) (p : D.Client α) : E.Client α

Substitution reuses upstream free-monad interpretation.

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

Purely semantic module correctness over relational specifications; neither an execution model nor a cost appears.

• methods : Methods D E

  Bodies implementing the upper interface using lower-interface calls.

• rep : D.State → E.State → Prop

  The relation between upper and lower mathematical states.

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

  Demonic admissibility of each method body from related states.

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

  Angelic correctness of each method body: every lower ClientRun realizes some permitted upper step D.step s o s' a maintaining rep s' e'.

@[reducible, inline]

abbrev Cslib.DataStructure.Module.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) (rep : D.State → E.State → Prop) (valid : ∀ {s : D.State} {e : E.State} (o : D.Op), rep s e → D.valid s o → E.ValidHistory e (E.clientHistory e (methods o))) (correct : ∀ {s : D.State} {e : E.State} (o : D.Op), rep s e → D.valid s o → E.clientResult e (methods o) = (D.stepFn s o).2 ∧ rep (D.stepFn s o).1 (E.clientState e (methods o))) : Module D E

Construct a Module D E for deterministic specifications ([D.HasStepFn fD], [E.HasStepFn fE]) from functional ValidHistory and runClient obligations.

def Cslib.DataStructure.Module.realize {D E : StateTransitionSpec} {C τ : Type x} (M : Module D E) {exec : Execution E.signature C τ} (R : StateTransitionImpl E exec) : StateTransitionImpl D fun (c : C) (o : D.signature.A) (a : D.signature.B o) (c' : C) (ts : List τ) => Executes exec (M.methods o) c a c' ts

Module implementation hides the intermediate representation and composes at any backend.

theorem Cslib.DataStructure.link_exec {D E : StateTransitionSpec} {C τ : Type x} {α : Type w} (methods : Methods D E) (exec : Execution E.signature C τ) {p : D.Client α} {c c' : C} {a : α} {chunks : List (List τ)} (he : Executes (fun (x : C) (o : D.signature.A) (a : D.signature.B o) (y : C) (ts : List τ) => Executes exec (methods o) x a y ts) p c a c' chunks) : Executes exec (link methods p) c a c' chunks.flatten

Linking expands every module call and preserves the complete flattened backend trace.

theorem Cslib.DataStructure.link_exec_decompose {D E : StateTransitionSpec} {C τ : Type x} {α : Type w} (methods : Methods D E) (exec : Execution E.signature C τ) {p : D.Client α} {c c' : C} {a : α} {ts : List τ} (he : Executes exec (link methods p) c a c' ts) : ∃ (chunks : List (List τ)), Executes (fun (x : C) (o : D.signature.A) (a : D.signature.B o) (y : C) (trace : List τ) => Executes exec (methods o) x a y trace) p c a c' chunks ∧ ts = chunks.flatten

Every flattened execution also decomposes into executions of its individual method calls.